Supporting results for the analytic Hamiltonian KAM construction.
theorem
KamProject.Arnold1963.realVolume_pos_of_loss_lt
{n : ℕ}
{G S : Set (ComplexSpace n)}
(hloss : realVolume (G \ S) < realVolume G)
:
theorem
KamProject.Arnold1963.realSlice_nonempty_of_realVolume_pos
{n : ℕ}
{G : Set (ComplexSpace n)}
(hG : 0 < realVolume G)
:
theorem
KamProject.Arnold1963.FrequencyChangeInput.iterationE_nonempty_iff
{n : ℕ}
{A g Δ : ComplexSpace n → ComplexSpace n}
{G Ω : Set (ComplexSpace n)}
{β κ θ Θ : NNReal}
(h : FrequencyChangeInput A g Δ G Ω β κ θ Θ)
(K N : ℝ)
:
theorem
KamProject.Arnold1963.FrequencyChangeInput.iteration_nonempty_of_measure_budget
{n : ℕ}
{A g Δ : ComplexSpace n → ComplexSpace n}
{G Ω : Set (ComplexSpace n)}
{β κ θ Θ : NNReal}
(h : FrequencyChangeInput A g Δ G Ω β κ θ Θ)
{K N : ℝ}
{L : ENNReal}
(hloss : realVolume (G \ h.iterationDomain K N) ≤ L)
(hL : L < realVolume G)
:
theorem
KamProject.Arnold1963.frequency_measure_to_action_budget
{n : ℕ}
{G S G₀ Ω₀ : Set (ComplexSpace n)}
{A₀ g₀ : ComplexSpace n → ComplexSpace n}
(c₀ : AnalyticFrequencyChart A₀ g₀ G₀ Ω₀)
{θ Θ₀ B : ℝ}
(_hθ : 0 < θ)
(hΘ₀ : 0 ≤ Θ₀)
(hupper : ∀ p ∈ G₀, ‖fderiv ℂ A₀ p‖ ≤ Θ₀)
(hloss : realVolume (G \ S) ≤ ENNReal.ofReal (θ⁻¹ ^ n) * (ENNReal.ofReal B * realVolume Ω₀))
:
theorem
KamProject.Arnold1963.frequency_measure_to_uniform_action_budget
{n : ℕ}
{G S G₀ Ω₀ : Set (ComplexSpace n)}
{A₀ g₀ : ComplexSpace n → ComplexSpace n}
(c₀ : AnalyticFrequencyChart A₀ g₀ G₀ Ω₀)
{θ θ₀ Θ₀ B : ℝ}
(hθ₀ : 0 < θ₀)
(hθ : θ₀ / 2 ≤ θ)
(hΘ₀ : 0 ≤ Θ₀)
(hupper : ∀ p ∈ G₀, ‖fderiv ℂ A₀ p‖ ≤ Θ₀)
(hloss : realVolume (G \ S) ≤ ENNReal.ofReal (θ⁻¹ ^ n) * (ENNReal.ofReal B * realVolume Ω₀))
: