Uniform convergence of the actual frequencies on the common action domain, with strict tail bounds on the scale of the next action loss.
noncomputable def
KamProject.Arnold1963.Iteration.InitialData.frequency
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
(s : ℕ)
:
ComplexSpace n → ComplexSpace n
The action-frequency map at the specified iteration stage.
Equations
Instances For
noncomputable def
KamProject.Arnold1963.Iteration.InitialData.limitFrequency
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
:
ComplexSpace n → ComplexSpace n
The telescoping limit of the iteration's action-frequency maps.
Equations
Instances For
theorem
KamProject.Arnold1963.Iteration.InitialData.frequency_uniform
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
:
TendstoUniformlyOn (frequency b h) (limitFrequency b h) Filter.atTop (limitDomain b h)
theorem
KamProject.Arnold1963.Iteration.InitialData.limitFrequency_tail
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
{p : ComplexSpace n}
(hp : p ∈ limitDomain b h)
(s : ℕ)
:
theorem
KamProject.Arnold1963.Iteration.InitialData.limitFrequency_continuous
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
:
ContinuousOn (limitFrequency b h) (limitDomain b h)
theorem
KamProject.Arnold1963.Iteration.InitialData.limitFrequency_real
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
{p : ComplexSpace n}
(hp : p ∈ limitDomain b h)
:
theorem
KamProject.Arnold1963.Iteration.InitialData.limitFrequency_real_value
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
{p : RealSpace n}
(hp : p ∈ realSlice (limitDomain b h))
: