Angle correction bounds, derivative smallness, and injectivity on a thinner complex strip.

theorem KamProject.Arnold1963.norm_imagPart_le {n : ℕ} (z : ComplexSpace n) : ‖imagPart z‖ ≤ ‖z‖

theorem KamProject.Arnold1963.convex_angleStrip (n : ℕ) (r : NNReal) : Convex ℝ (angleStrip n r)

theorem KamProject.Arnold1963.Iteration.InitialParameters.beta_width_budget {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) : 48 * ↑(beta δ₁ 0) < ↑ρ₀

theorem KamProject.Arnold1963.Iteration.InitialParameters.angle_derivative_budget {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) : 2 * ↑(beta δ₁ 0) / (↑ρ₀ / 12) < 1 / 2

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

The angle component of the limiting phase transformation at a fixed action label.

Equations

• KamProject.Arnold1963.Iteration.InitialData.angleMap b h p q = (KamProject.Arnold1963.Iteration.InitialData.limitMap b h (p, q)).2

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

The displacement of the limiting angle map from the identity.

Equations

• KamProject.Arnold1963.Iteration.InitialData.angleCorrection b h p q = KamProject.Arnold1963.Iteration.InitialData.angleMap b h p q - q

theorem KamProject.Arnold1963.Iteration.InitialData.angleCorrection_analytic {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : ComplexSpace n} (hp : p ∈ limitDomain b h) : AnalyticOnNhd ℂ (angleCorrection b h p) (commonAngleStrip n ρ₀)

theorem KamProject.Arnold1963.Iteration.InitialData.angleCorrection_bound {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 ∈ commonAngleStrip n ρ₀) : ‖angleCorrection b h p q‖ < 2 * ↑(beta δ₁ 0)

theorem KamProject.Arnold1963.Iteration.InitialData.thinAngleStrip_subset {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) : angleStrip n (ρ₀ / 6) ⊆ commonAngleStrip n ρ₀

theorem KamProject.Arnold1963.Iteration.InitialData.thinAngleStrip_buffer {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) {q : ComplexSpace n} (hq : q ∈ angleStrip n (ρ₀ / 6)) : q ∈ erosion (commonAngleStrip n ρ₀) (ρ₀ / 12)

theorem KamProject.Arnold1963.Iteration.InitialData.angleCorrection_derivative {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 ℂ (angleCorrection b h p) q‖ < 1 / 2

theorem KamProject.Arnold1963.Iteration.InitialData.angleCorrection_lipschitz {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : ComplexSpace n} (hp : p ∈ limitDomain b h) : LipschitzOnWith (1 / 2) (angleCorrection b h p) (angleStrip n (ρ₀ / 6))

theorem KamProject.Arnold1963.Iteration.InitialData.angleMap_injOn {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : ComplexSpace n} (hp : p ∈ limitDomain b h) : Set.InjOn (angleMap b h p) (angleStrip n (ρ₀ / 6))