Injectivity of limit frequency labels. Inverse mean-value estimates are taken on contained frequency balls, without assuming convexity of the limiting action domain.

@[simp]

theorem KamProject.Arnold1963.Iteration.InitialData.frequencyDomain_zero {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) : frequencyDomain b h 0 = Ω₀

theorem KamProject.Arnold1963.Iteration.InitialData.limitFrequency_ball_subset {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : ComplexSpace n} (hp : p ∈ limitDomain b h) (s : ℕ) : Metric.closedBall (limitFrequency b h p) ↑(beta δ₁ s) ⊆ frequencyDomain b h s

theorem KamProject.Arnold1963.Iteration.InitialData.limitFrequency_injOn {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) : Set.InjOn (limitFrequency b h) (limitDomain b h)

def KamProject.Arnold1963.Iteration.InitialData.retainedFrequencies {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) : Set (ComplexSpace n)

The image of the limiting action domain under the limiting frequency map.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def KamProject.Arnold1963.Iteration.InitialData.frequencyLabel {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) : ComplexSpace n → ComplexSpace n

A set-restricted inverse assigning action labels to retained limiting frequencies.

Equations

• One or more equations did not get rendered due to their size.

theorem KamProject.Arnold1963.Iteration.InitialData.frequencyLabel_left {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : ComplexSpace n} (hp : p ∈ limitDomain b h) : frequencyLabel b h (limitFrequency b h p) = p

theorem KamProject.Arnold1963.Iteration.InitialData.frequencyLabel_mem {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {ω : ComplexSpace n} (hω : ω ∈ retainedFrequencies b h) : frequencyLabel b h ω ∈ limitDomain b h

theorem KamProject.Arnold1963.Iteration.InitialData.frequencyLabel_right {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {ω : ComplexSpace n} (hω : ω ∈ retainedFrequencies b h) : limitFrequency b h (frequencyLabel b h ω) = ω

def KamProject.Arnold1963.Iteration.InitialData.unperturbedCenter {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {D : ℝ} (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (ω : ComplexSpace n) : ComplexSpace n

The original action center corresponding to a frequency through the initial inverse chart.

Equations

• h.unperturbedCenter ω = h.inverseFrequency ω

theorem KamProject.Arnold1963.Iteration.InitialData.unperturbedCenter_mem {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : ComplexSpace n} (hp : p ∈ limitDomain b h) : h.unperturbedCenter (limitFrequency b h p) ∈ h.domain

theorem KamProject.Arnold1963.Iteration.InitialData.unperturbedCenter_displacement {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : ComplexSpace n} (hp : p ∈ limitDomain b h) : ‖h.unperturbedCenter (limitFrequency b h p) - p‖ < (↑θ₀)⁻¹ * (↑(beta δ₁ 0) / 2)