Global real angle inverses, local complex analytic inverses, and closed torus embeddings. Analyticity concerns the complex angle lift for a fixed action label.

theorem KamProject.Arnold1963.Iteration.InitialData.instFactLtRealOfNatHMulPi_1 : Fact (0 < 2 * Real.pi)

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

The real angle component of the limiting phase transformation.

Equations

• KamProject.Arnold1963.Iteration.InitialData.realAngleMap b h p q = (KamProject.Arnold1963.Iteration.InitialData.realLimitMap b h (p, q)).2

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

The real-coordinate restriction of the limiting angle displacement.

Equations

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

theorem KamProject.Arnold1963.Iteration.InitialData.realAngleMap_eq {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (p q : RealSpace n) : realAngleMap b h p q = q + realAngleCorrection b h p q

theorem KamProject.Arnold1963.Iteration.InitialData.realAngleCorrection_lipschitz {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : RealSpace n} (hp : p ∈ realSlice (limitDomain b h)) : LipschitzWith (1 / 2) (realAngleCorrection b h p)

theorem KamProject.Arnold1963.Iteration.InitialData.realAngleCorrection_bound {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : RealSpace n} (hp : p ∈ realSlice (limitDomain b h)) (q : RealSpace n) : ‖realAngleCorrection b h p q‖ < 2 * ↑(beta δ₁ 0)

theorem KamProject.Arnold1963.Iteration.InitialData.realAngleMap_bijective {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : RealSpace n} (hp : p ∈ realSlice (limitDomain b h)) : Function.Bijective (realAngleMap b h p)

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

A function inverse of the real limiting angle map at a fixed action label.

Equations

• KamProject.Arnold1963.Iteration.InitialData.realAngleInverse b h p = Function.invFun (KamProject.Arnold1963.Iteration.InitialData.realAngleMap b h p)

theorem KamProject.Arnold1963.Iteration.InitialData.realAngleInverse_left {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : RealSpace n} (hp : p ∈ realSlice (limitDomain b h)) (q : RealSpace n) : realAngleInverse b h p (realAngleMap b h p q) = q

theorem KamProject.Arnold1963.Iteration.InitialData.realAngleInverse_right {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : RealSpace n} (hp : p ∈ realSlice (limitDomain b h)) (Q : RealSpace n) : realAngleMap b h p (realAngleInverse b h p Q) = Q

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

A set-restricted inverse of the limiting complex angle map on the narrower strip.

Equations

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

theorem KamProject.Arnold1963.Iteration.InitialData.angleMap_derivative_near_id {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : ComplexSpace n} (hp : p ∈ limitDomain b h) {q : ComplexSpace n} (hq : q ∈ angleStrip n (ρ₀ / 6)) : ‖fderiv ℂ (angleMap b h p) q - ContinuousLinearMap.id ℂ (ComplexSpace n)‖ < 1 / 2

theorem KamProject.Arnold1963.Iteration.InitialData.complexAngleInverse_analytic {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : ComplexSpace n} (hp : p ∈ limitDomain b h) (q : RealSpace n) : AnalyticAt ℂ (complexAngleInverse b h p) (angleMap b h p (complexify q)) ∧ complexAngleInverse b h p (angleMap b h p (complexify q)) = complexify q ∧ ∀ᶠ (Q : ComplexSpace n) in nhds (angleMap b h p (complexify q)), angleMap b h p (complexAngleInverse b h p Q) = Q

theorem KamProject.Arnold1963.Iteration.InitialData.angleMap_derivative_injective {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : ComplexSpace n} (hp : p ∈ limitDomain b h) {q : ComplexSpace n} (hq : q ∈ angleStrip n (ρ₀ / 6)) : Function.Injective ⇑(fderiv ℂ (angleMap b h p) q)

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

The limiting phase map at a fixed real action label, regarded as a torus embedding.

Equations

• KamProject.Arnold1963.Iteration.InitialData.torusEmbedding b h p Q = KamProject.Arnold1963.Iteration.InitialData.torusLimitMap b h (p, Q)

theorem KamProject.Arnold1963.Iteration.InitialData.torusEmbedding_lift {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : RealSpace n} (hp : p ∈ realSlice (limitDomain b h)) (q : RealSpace n) : (torusEmbedding b h p fun (j : Fin n) => ↑(q j)) = torusProjection (realPartPhase (limitMap b h (complexify p, complexify q)))

theorem KamProject.Arnold1963.Iteration.InitialData.torusEmbedding_range {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (p : RealSpace n) : Set.range (torusEmbedding b h p) = invariantTorus b h p

theorem KamProject.Arnold1963.Iteration.InitialData.torusEmbedding_continuous {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : RealSpace n} (hp : p ∈ realSlice (limitDomain b h)) : Continuous (torusEmbedding b h p)

theorem KamProject.Arnold1963.Iteration.InitialData.torusEmbedding_isClosedEmbedding {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : RealSpace n} (hp : p ∈ realSlice (limitDomain b h)) : Topology.IsClosedEmbedding (torusEmbedding b h p)

theorem KamProject.Arnold1963.Iteration.InitialData.angleMap_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)) (q : RealSpace n) : complexify (realAngleMap b h p q) = angleMap b h (complexify p) (complexify q)

theorem KamProject.Arnold1963.Iteration.InitialData.complexAngleInverse_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)) (Q : RealSpace n) : complexAngleInverse b h (complexify p) (complexify Q) = complexify (realAngleInverse b h p Q)

theorem KamProject.Arnold1963.Iteration.InitialData.complexAngleInverse_analytic_at_real {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : RealSpace n} (hp : p ∈ realSlice (limitDomain b h)) (Q : RealSpace n) : AnalyticAt ℂ (complexAngleInverse b h (complexify p)) (complexify Q)

theorem KamProject.Arnold1963.Iteration.InitialData.torusLift_derivative_injective {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : ComplexSpace n} (hp : p ∈ limitDomain b h) {q : ComplexSpace n} (hq : q ∈ angleStrip n (ρ₀ / 6)) : Function.Injective ⇑(fderiv ℂ (fun (q : ComplexSpace n) => limitMap b h (p, q)) q)

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

The angle component of the embedded torus, with angles reduced modulo 2π.

Equations

• KamProject.Arnold1963.Iteration.InitialData.torusAngleMap b h p Q = (KamProject.Arnold1963.Iteration.InitialData.torusEmbedding b h p Q).2

theorem KamProject.Arnold1963.Iteration.InitialData.torusAngleMap_projection {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : RealSpace n} (hp : p ∈ realSlice (limitDomain b h)) (q : RealSpace n) : (torusAngleMap b h p fun (j : Fin n) => ↑(q j)) = fun (j : Fin n) => ↑(realAngleMap b h p q j)

theorem KamProject.Arnold1963.Iteration.InitialData.torusAngleMap_bijective {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : RealSpace n} (hp : p ∈ realSlice (limitDomain b h)) : Function.Bijective (torusAngleMap b h p)

noncomputable def KamProject.Arnold1963.Iteration.InitialData.torusAngleHomeomorph {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : RealSpace n} (hp : p ∈ realSlice (limitDomain b h)) : RealTorus n ≃ₜ RealTorus n

The homeomorphism of the real angle torus induced by a retained action label.

Equations

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

theorem KamProject.Arnold1963.Iteration.InitialData.torusAngleHomeomorph_inverse_lift {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : RealSpace n} (hp : p ∈ realSlice (limitDomain b h)) (Q : RealSpace n) : ((torusAngleHomeomorph b h hp).symm fun (j : Fin n) => ↑(Q j)) = fun (j : Fin n) => ↑(realAngleInverse b h p Q j)