Supporting results for the analytic Hamiltonian KAM construction.
theorem
KamProject.Arnold1963.InductiveResult.delta_lt_one
{n : ℕ}
{G Ω : Set (ComplexSpace n)}
{ρ β δ γ θ Θ : NNReal}
{K M : ℝ}
{a : ComplexSpace n → ℂ}
{f : AnalyticPhaseFunction n G ρ}
(r : InductiveResult a f Ω β δ γ θ Θ K M)
:
theorem
KamProject.Arnold1963.InductiveResult.realSlice_nonempty_of_budget
{n : ℕ}
{G Ω : Set (ComplexSpace n)}
{ρ β δ γ θ Θ : NNReal}
{K M : ℝ}
{a : ComplexSpace n → ℂ}
{f : AnalyticPhaseFunction n G ρ}
(r : InductiveResult a f Ω β δ γ θ Θ K M)
{L : ENNReal}
(hloss : realVolume (G \ r.domain) ≤ L)
(hL : L < realVolume G)
:
theorem
KamProject.Arnold1963.InductiveResult.nextInput
{n : ℕ}
{G Ω : Set (ComplexSpace n)}
{ρ β δ γ θ Θ : NNReal}
{K M : ℝ}
{a : ComplexSpace n → ℂ}
{f : AnalyticPhaseFunction n G ρ}
(r : InductiveResult a f Ω β δ γ θ Θ K M)
{β₁ δ₁ γ₁ : NNReal}
(hb : IterationParameters n (ρ - 3 * γ) β₁ δ₁ γ₁ (θ * (1 - δ)) (Θ * (1 + δ)) K (iterationRemainderBound n M ↑δ ↑β))
:
IterationInput (f.averagedHamiltonian a) r.perturbation r.inverseFrequency β₁ δ₁ γ₁ (θ * (1 - δ)) (Θ * (1 + δ)) K
(iterationRemainderBound n M ↑δ ↑β)
theorem
KamProject.Arnold1963.IterationInput.result_chart_next
{n : ℕ}
{G Ωbase : Set (ComplexSpace n)}
{ρ β δ γ θ Θ : NNReal}
{K M N₀ : ℝ}
{a : ComplexSpace n → ℂ}
{f : AnalyticPhaseFunction n G ρ}
{g : ComplexSpace n → ComplexSpace n}
(s : ResonanceDomainState n K N₀)
(i : IterationInput a f g β δ γ θ Θ K M)
(hNN : N₀ ≤ fundamentalCutoff (↑γ) (2 * M))
:
AnalyticFrequencyChart (actionFrequency (f.averagedHamiltonian a)) i.result.inverseFrequency i.result.domain
((s.next ⋯ hNN ((5 + 7 * Θ) * β)).domain Ωbase)
theorem
KamProject.Arnold1963.IterationInput.result_measure_budget
{n : ℕ}
{G Ωbase : Set (ComplexSpace n)}
{ρ β δ γ θ Θ : NNReal}
{K M N₀ D : ℝ}
{a : ComplexSpace n → ℂ}
{f : AnalyticPhaseFunction n G ρ}
{g : ComplexSpace n → ComplexSpace n}
(s : ResonanceDomainState n K N₀)
(i : IterationInput a f g β δ γ θ Θ K M)
(hD : TypeD Ωbase D)
(hN₀ : 1 ≤ N₀)
(hNN : N₀ ≤ fundamentalCutoff (↑γ) (2 * M))
:
realVolume (G \ i.result.domain) ≤ ENNReal.ofReal ((↑θ)⁻¹ ^ n) * (ENNReal.ofReal
(resonanceLossConstant n * D * (K * newShellBudget N₀ (fundamentalCutoff (↑γ) (2 * M)) + ↑((6 + 7 * Θ) * β) * fundamentalCutoff (↑γ) (2 * M) ^ n)) * realVolume Ωbase)
theorem
KamProject.Arnold1963.IterationInput.result_measure_uniform
{n : ℕ}
{G Ωbase : Set (ComplexSpace n)}
{ρ β δ γ θ Θ : NNReal}
{K M N₀ D : ℝ}
{a : ComplexSpace n → ℂ}
{f : AnalyticPhaseFunction n G ρ}
{g : ComplexSpace n → ComplexSpace n}
(s : ResonanceDomainState n K N₀)
(i : IterationInput a f g β δ γ θ Θ K M)
{G₀ : Set (ComplexSpace n)}
{A₀ g₀ : ComplexSpace n → ComplexSpace n}
(c₀ : AnalyticFrequencyChart A₀ g₀ G₀ Ωbase)
{θ₀ Θ₀ : ℝ}
(hθ₀ : 0 < θ₀)
(hθ : θ₀ / 2 ≤ ↑θ)
(hΘ₀ : 0 ≤ Θ₀)
(hupper : ∀ p ∈ G₀, ‖fderiv ℂ A₀ p‖ ≤ Θ₀)
(hD : TypeD Ωbase D)
(hN₀ : 1 ≤ N₀)
(hNN : N₀ ≤ fundamentalCutoff (↑γ) (2 * M))
:
realVolume (G \ i.result.domain) ≤ ENNReal.ofReal ((2 * Θ₀ / θ₀) ^ n) * (ENNReal.ofReal
(resonanceLossConstant n * D * (K * newShellBudget N₀ (fundamentalCutoff (↑γ) (2 * M)) + ↑((6 + 7 * Θ) * β) * fundamentalCutoff (↑γ) (2 * M) ^ n)) * realVolume G₀)