Local analytic invariant tori and the physical measure decomposition within one initial frequency chart, obtained from the actual infinite iteration.

theorem KamProject.Arnold1963.instFactLtRealOfNatHMulPi_leanPool_3 : Fact (0 < 2 * Real.pi)

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

The initial real action-angle phase set of a local iteration.

Equations

• h.localPhase = KamProject.Arnold1963.realSlice h.domain ×ˢ Set.univ

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

The image of the limiting action domain and real torus under the limiting transformation.

Equations

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

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

The complement of the local good set inside the initial local phase set.

Equations

• KamProject.Arnold1963.Iteration.InitialData.localF2 b h = h.localPhase \ KamProject.Arnold1963.Iteration.InitialData.localF1 b h

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

theorem KamProject.Arnold1963.Iteration.InitialData.localF1_eq_union {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) : localF1 b h = ⋃ p ∈ realSlice (limitDomain b h), invariantTorus b h p

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

theorem KamProject.Arnold1963.Iteration.InitialData.local_partition {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) : localF1 b h ∪ localF2 b h = h.localPhase ∧ Disjoint (localF1 b h) (localF2 b h)

theorem KamProject.Arnold1963.Iteration.InitialData.localPhase_volume_finite {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {D : ℝ} (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) : MeasureTheory.volume h.localPhase ≠ ⊤

theorem KamProject.Arnold1963.Iteration.InitialData.localF2_volume_lt {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) : MeasureTheory.volume (localF2 b h) < ENNReal.ofReal κ * MeasureTheory.volume h.localPhase

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

The invariant torus associated with a complex frequency via its real action label.

Equations

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

theorem KamProject.Arnold1963.Iteration.InitialData.localF1_eq_frequency_union {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) : localF1 b h = ⋃ ω ∈ retainedRealFrequencies b h, frequencyTorus b h ω

theorem KamProject.Arnold1963.Iteration.InitialData.frequencyTorus_disjoint {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {ω ω' : ComplexSpace n} (hω : ω ∈ retainedRealFrequencies b h) (hω' : ω' ∈ retainedRealFrequencies b h) (hne : ω ≠ ω') : Disjoint (frequencyTorus b h ω) (frequencyTorus b h ω')

theorem KamProject.Arnold1963.Iteration.InitialData.frequency_orbit {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {ω : ComplexSpace n} (hω : ω ∈ retainedRealFrequencies b h) (q : RealSpace n) : (∀ (t : ℝ), orbit b h (realFrequencyLabel b h ω) q t = frequencyParameterization b h ω (complexify q + ↑t • ω)) ∧ (∀ (t : ℝ), HasDerivAt (orbit b h (realFrequencyLabel b h ω) q) (vectorField b h 0 (orbit b h (realFrequencyLabel b h ω) q t)) t) ∧ (∀ (t : ℝ), torusProjection (realPartPhase (orbit b h (realFrequencyLabel b h ω) q t)) ∈ frequencyTorus b h ω) ∧ ∀ (k : FourierIndex n), k ≠ 0 → indexPairing k ω ≠ 0

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

The local KAM conclusion, including nonempty limiting domains and disjoint embedded tori.

• nonempty : (realSlice (Iteration.InitialData.limitDomain b h)).Nonempty
• frequency_injective : Set.InjOn (Iteration.InitialData.limitFrequency b h) (Iteration.InitialData.limitDomain b h)
• embedding (p : RealSpace n) : p ∈ realSlice (Iteration.InitialData.limitDomain b h) → Topology.IsClosedEmbedding (Iteration.InitialData.torusEmbedding b h p)
• analytic_lift (p : ComplexSpace n) : p ∈ Iteration.InitialData.limitDomain b h → AnalyticOnNhd ℂ (fun (q : ComplexSpace n) => Iteration.InitialData.limitMap b h (p, q)) (Iteration.InitialData.commonAngleStrip n ρ₀)
• immersion (p : ComplexSpace n) : p ∈ Iteration.InitialData.limitDomain b h → ∀ q ∈ angleStrip n (ρ₀ / 6), Function.Injective ⇑(fderiv ℂ (fun (q : ComplexSpace n) => Iteration.InitialData.limitMap b h (p, q)) q)
• angle_bijective (p : RealSpace n) : p ∈ realSlice (Iteration.InitialData.limitDomain b h) → Function.Bijective (Iteration.InitialData.torusAngleMap b h p)
• inverse_analytic (p : RealSpace n) : p ∈ realSlice (Iteration.InitialData.limitDomain b h) → ∀ (Q : RealSpace n), AnalyticAt ℂ (Iteration.InitialData.complexAngleInverse b h (complexify p)) (complexify Q)
• corrections_small (p : ComplexSpace n) : p ∈ Iteration.InitialData.limitDomain b h → ∀ q ∈ Iteration.InitialData.commonAngleStrip n ρ₀, ‖Iteration.InitialData.actionCorrection b h p q‖ < κ ∧ ‖Iteration.InitialData.angleCorrection b h p q‖ < κ
• disjoint (p : RealSpace n) : p ∈ realSlice (Iteration.InitialData.limitDomain b h) → ∀ p' ∈ realSlice (Iteration.InitialData.limitDomain b h), p ≠ p' → Disjoint (Iteration.InitialData.invariantTorus b h p) (Iteration.InitialData.invariantTorus b h p')
• invariant_orbits (p : RealSpace n) : p ∈ realSlice (Iteration.InitialData.limitDomain b h) → ∀ (q : RealSpace n) (t : ℝ), HasDerivAt (Iteration.InitialData.orbit b h p q) (Iteration.InitialData.vectorField b h 0 (Iteration.InitialData.orbit b h p q t)) t ∧ torusProjection (realPartPhase (Iteration.InitialData.orbit b h p q t)) ∈ Iteration.InitialData.invariantTorus b h p
• nonresonance (p : ComplexSpace n) : p ∈ Iteration.InitialData.limitDomain b h → ∀ (k : FourierIndex n), k ≠ 0 → indexPairing k (Iteration.InitialData.limitFrequency b h p) ≠ 0
• union_eq : Iteration.InitialData.localF1 b h = ⋃ ω ∈ Iteration.InitialData.retainedRealFrequencies b h, Iteration.InitialData.frequencyTorus b h ω
• compact : IsCompact (Iteration.InitialData.localF1 b h)
• partition : Iteration.InitialData.localF1 b h ∪ Iteration.InitialData.localF2 b h = h.localPhase ∧ Disjoint (Iteration.InitialData.localF1 b h) (Iteration.InitialData.localF2 b h)
• large_measure : ENNReal.ofReal (1 - κ) * MeasureTheory.volume h.localPhase < MeasureTheory.volume (Iteration.InitialData.localF1 b h)
• small_complement : MeasureTheory.volume (Iteration.InitialData.localF2 b h) < ENNReal.ofReal κ * MeasureTheory.volume h.localPhase

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