Summable total action-domain loss, including resonance shells and boundary layers.

noncomputable def KamProject.Arnold1963.Iteration.rawLoss (n : ℕ) (δ₁ Θ₀ : NNReal) (κ : ℝ) (s : ℕ) : ℝ

The frequency-space loss budget combining new resonance shells and geometric erosion.

Equations

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

noncomputable def KamProject.Arnold1963.Iteration.actionLossFactor (n : ℕ) (θ₀ Θ₀ : NNReal) (D : ℝ) : ℝ

The coefficient transporting the frequency-space loss budget to real action volume.

Equations

• KamProject.Arnold1963.Iteration.actionLossFactor n θ₀ Θ₀ D = (2 * ↑Θ₀ / ↑θ₀) ^ n * KamProject.Arnold1963.resonanceLossConstant n * D

noncomputable def KamProject.Arnold1963.Iteration.lossBudget (n : ℕ) (δ₁ θ₀ Θ₀ : NNReal) (κ D : ℝ) (s : ℕ) : ENNReal

The extended nonnegative action-volume loss budget for one iteration stage.

Equations

• KamProject.Arnold1963.Iteration.lossBudget n δ₁ θ₀ Θ₀ κ D s = ENNReal.ofReal (KamProject.Arnold1963.Iteration.actionLossFactor n θ₀ Θ₀ D * KamProject.Arnold1963.Iteration.rawLoss n δ₁ Θ₀ κ s)

theorem KamProject.Arnold1963.Iteration.InitialParameters.tube_budget {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s : ℕ) : ↑((6 + 7 * upper Θ₀ δ₁ s) * beta δ₁ s) * cutoff n δ₁ s ^ n < ↑(delta δ₁ s)

theorem KamProject.Arnold1963.Iteration.InitialParameters.rawLoss_nonneg {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s : ℕ) : 0 ≤ rawLoss n δ₁ Θ₀ κ s

theorem KamProject.Arnold1963.Iteration.InitialParameters.rawLoss_le {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s : ℕ) : rawLoss n δ₁ Θ₀ κ s ≤ κ * ↑δ₁ * newShellBudget (previousCutoff n δ₁ s) (cutoff n δ₁ s) + ↑(delta δ₁ s)

theorem KamProject.Arnold1963.Iteration.InitialParameters.rawLoss_summable {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) : Summable (rawLoss n δ₁ Θ₀ κ)

theorem KamProject.Arnold1963.Iteration.InitialParameters.rawLoss_tsum_lt {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) : ∑' (s : ℕ), rawLoss n δ₁ Θ₀ κ s < 4 * ↑δ₁

theorem KamProject.Arnold1963.Iteration.InitialParameters.actionLossFactor_pos {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) : 0 < actionLossFactor n θ₀ Θ₀ D

theorem KamProject.Arnold1963.Iteration.InitialParameters.initial_measure_budget {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) : 4 * ↑δ₁ * actionLossFactor n θ₀ Θ₀ D < κ

theorem KamProject.Arnold1963.Iteration.InitialParameters.total_budget {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) : actionLossFactor n θ₀ Θ₀ D * ∑' (s : ℕ), rawLoss n δ₁ Θ₀ κ s < κ

theorem KamProject.Arnold1963.Iteration.InitialParameters.lossBudget_tsum_lt {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) : ∑' (s : ℕ), lossBudget n δ₁ θ₀ Θ₀ κ D s < ENNReal.ofReal κ