Connect the analytic single-step result to the exact iteration parameter recurrence.
theorem
KamProject.Arnold1963.Iteration.remainder_eq_next_parameter
{δ₁ : NNReal}
(hδ : 0 < δ₁)
(n s : ℕ)
:
iterationRemainderBound n (perturbation n δ₁ s) ↑(delta δ₁ s) ↑(beta δ₁ s) = perturbation n δ₁ (s + 1)
theorem
KamProject.Arnold1963.Iteration.result_measure_uniform
{n s : ℕ}
{G Ωbase G₀ : Set (ComplexSpace n)}
{A₀ g₀ : ComplexSpace n → ComplexSpace n}
{ρ δ₁ θ₀ Θ₀ : NNReal}
{K N₀ D : ℝ}
{a : ComplexSpace n → ℂ}
{f : AnalyticPhaseFunction n G ρ}
{g : ComplexSpace n → ComplexSpace n}
(r : ResonanceDomainState n K N₀)
(i :
IterationInput a f g (beta δ₁ s) (delta δ₁ s) (gamma n δ₁ s) (lower θ₀ δ₁ s) (upper Θ₀ δ₁ s) K (perturbation n δ₁ s))
(c₀ : AnalyticFrequencyChart A₀ g₀ G₀ Ωbase)
(hθ₀ : 0 < θ₀)
(hδ₁ : δ₁ < 1 / 4)
(hupper : ∀ p ∈ G₀, ‖fderiv ℂ A₀ p‖ ≤ ↑Θ₀)
(hD : TypeD Ωbase D)
(hN₀ : 1 ≤ N₀)
(hNN : N₀ ≤ fundamentalCutoff (↑(gamma n δ₁ s)) (2 * perturbation n δ₁ s))
:
realVolume (G \ i.result.domain) ≤ ENNReal.ofReal ((2 * ↑Θ₀ / ↑θ₀) ^ n) * (ENNReal.ofReal
(resonanceLossConstant n * D * (K * newShellBudget N₀ (fundamentalCutoff (↑(gamma n δ₁ s)) (2 * perturbation n δ₁ s)) + ↑((6 + 7 * upper Θ₀ δ₁ s) * beta δ₁ s) * fundamentalCutoff (↑(gamma n δ₁ s)) (2 * perturbation n δ₁ s) ^ n)) * realVolume G₀)