Supporting results for the analytic Hamiltonian KAM construction.

noncomputable def KamProject.Arnold1963.fundamentalRawBound (n : ℕ) (M K Θ δ β : ℝ) : ℝ

The sum of separate error estimates before applying the final remainder budget.

Equations

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

noncomputable def KamProject.Arnold1963.FundamentalInput.remainder {n : ℕ} {G E : Set (ComplexSpace n)} {ρ β δ γ : NNReal} {K M Θ : ℝ} {h : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} (i : FundamentalInput h f) (z : ComplexPhaseSpace n) : ℂ

The transformed total Hamiltonian minus the original integrable Hamiltonian.

Equations

• i.remainder z = h (i.transform z).1 + f.toFun (i.transform z) - h z.1

theorem KamProject.Arnold1963.FundamentalInput.first_variation_cancel {n : ℕ} {G E : Set (ComplexSpace n)} {ρ β δ γ : NNReal} {K M Θ : ℝ} {h : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} (i : FundamentalInput h f) {z : ComplexPhaseSpace n} (hz : z ∈ phaseDomain (erosion E (β + β)) (ρ - (γ + γ))) : (fderiv ℂ h z.1) ((i.transform z).1 - z.1) + fourierTruncation (f.fourierCoeff z.1) (fundamentalCutoff (↑γ) M) (i.transform z).2 = 0

theorem KamProject.Arnold1963.FundamentalInput.taylor_bound {n : ℕ} {G E : Set (ComplexSpace n)} {ρ β δ γ : NNReal} {K M Θ : ℝ} {h : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} (i : FundamentalInput h f) {z : ComplexPhaseSpace n} (hz : z ∈ phaseDomain (erosion E (β + β)) (ρ - (γ + γ))) : ‖h (i.transform z).1 - h z.1 - (fderiv ℂ h z.1) ((i.transform z).1 - z.1)‖ ≤ 1 / 2 * ↑n ^ 2 * Θ * (homologicalBound n M K ↑δ / ↑δ) ^ 2

theorem KamProject.Arnold1963.FundamentalInput.tail_bound {n : ℕ} {G E : Set (ComplexSpace n)} {ρ β δ γ : NNReal} {K M Θ : ℝ} {h : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} (i : FundamentalInput h f) {z : ComplexPhaseSpace n} (hz : z ∈ phaseDomain (erosion E (β + β)) (ρ - (γ + γ))) : ‖f.toFun (z.1, (i.transform z).2) - fourierTruncation (f.fourierCoeff z.1) (fundamentalCutoff (↑γ) M) (i.transform z).2‖ ≤ (2 * ↑n / Real.exp 1) ^ n * M ^ 2 / ↑δ ^ (n + 1)

theorem KamProject.Arnold1963.FundamentalInput.perturbation_composition_bound {n : ℕ} {G E : Set (ComplexSpace n)} {ρ β δ γ : NNReal} {K M Θ : ℝ} {h : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} (i : FundamentalInput h f) {z : ComplexPhaseSpace n} (hz : z ∈ phaseDomain (erosion E (β + β)) (ρ - (γ + γ))) : ‖f.toFun (i.transform z) - f.toFun (z.1, (i.transform z).2)‖ ≤ ↑n * M / ↑β * (homologicalBound n M K ↑δ / ↑δ)

theorem KamProject.Arnold1963.FundamentalInput.remainder_decomposition {n : ℕ} {G E : Set (ComplexSpace n)} {ρ β δ γ : NNReal} {K M Θ : ℝ} {h : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} (i : FundamentalInput h f) {z : ComplexPhaseSpace n} (hz : z ∈ phaseDomain (erosion E (β + β)) (ρ - (γ + γ))) : i.remainder z = h (i.transform z).1 - h z.1 - (fderiv ℂ h z.1) ((i.transform z).1 - z.1) + (f.toFun (z.1, (i.transform z).2) - fourierTruncation (f.fourierCoeff z.1) (fundamentalCutoff (↑γ) M) (i.transform z).2) + (f.toFun (i.transform z) - f.toFun (z.1, (i.transform z).2))

theorem KamProject.Arnold1963.FundamentalInput.remainder_norm_bound {n : ℕ} {G E : Set (ComplexSpace n)} {ρ β δ γ : NNReal} {K M Θ : ℝ} {h : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} (i : FundamentalInput h f) : NormBoundOn i.remainder (phaseDomain (erosion E (β + β)) (ρ - (γ + γ))) (fundamentalRawBound n M K Θ ↑δ ↑β)