The compact intersection of actual iteration domains, with positive measure and strict loss bounds obtained from the summable budget.
theorem
KamProject.Arnold1963.Iteration.InitialData.step_measure
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
(s : ℕ)
:
realVolume (actionDomain b h s \ actionDomain b h (s + 1)) ≤ lossBudget n δ₁ θ₀ Θ₀ κ D s * realVolume h.domain
def
KamProject.Arnold1963.Iteration.InitialData.limitDomain
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
:
Set (ComplexSpace n)
The intersection of all action domains retained during the iteration.
Equations
Instances For
theorem
KamProject.Arnold1963.Iteration.InitialData.limit_subset
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
(s : ℕ)
:
limitDomain b h ⊆ actionDomain b h s
theorem
KamProject.Arnold1963.Iteration.InitialData.limit_compact
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
:
IsCompact (limitDomain b h)
theorem
KamProject.Arnold1963.Iteration.InitialData.limit_loss
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
:
theorem
KamProject.Arnold1963.Iteration.InitialData.limit_volume_pos
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
:
theorem
KamProject.Arnold1963.Iteration.InitialData.limit_realSlice_nonempty
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
:
(realSlice (limitDomain b h)).Nonempty
theorem
KamProject.Arnold1963.Iteration.InitialData.finite_loss
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
(s : ℕ)
:
theorem
KamProject.Arnold1963.Iteration.InitialData.domain_realSlice_nonempty
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
(s : ℕ)
:
(realSlice (actionDomain b h s)).Nonempty
theorem
KamProject.Arnold1963.Iteration.InitialData.phase_nonempty
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
(s : ℕ)
:
theorem
KamProject.Arnold1963.Iteration.InitialData.limit_volume_gt
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
: