Summable weighted transformation increments and separate unweighted frequency tails.

theorem KamProject.Arnold1963.Iteration.InitialParameters.beta_eighth {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s : ℕ) : ↑(beta δ₁ (s + 1)) ≤ ↑(beta δ₁ s) / 8

theorem KamProject.Arnold1963.Iteration.InitialParameters.beta_geometric {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s j : ℕ) : ↑(beta δ₁ (j + s)) ≤ ↑(beta δ₁ s) * (1 / 8) ^ j

theorem KamProject.Arnold1963.Iteration.InitialParameters.beta_summable {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) : Summable fun (s : ℕ) => ↑(beta δ₁ s)

theorem KamProject.Arnold1963.Iteration.InitialParameters.beta_tail_le {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s : ℕ) : ∑' (j : ℕ), ↑(beta δ₁ (j + s)) ≤ 8 / 7 * ↑(beta δ₁ s)

theorem KamProject.Arnold1963.Iteration.InitialParameters.weighted_beta_bound {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s : ℕ) : 2 ^ s * ↑(beta δ₁ s) ≤ ↑(beta δ₁ 0) * (1 / 4) ^ s

theorem KamProject.Arnold1963.Iteration.InitialParameters.weighted_beta_summable {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) : Summable fun (s : ℕ) => 2 ^ s * ↑(beta δ₁ s)

theorem KamProject.Arnold1963.Iteration.InitialParameters.weighted_beta_tsum_lt {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) : ∑' (s : ℕ), 2 ^ s * ↑(beta δ₁ s) < 2 * ↑(beta δ₁ 0)

theorem KamProject.Arnold1963.Iteration.InitialParameters.weighted_beta_tendsto_zero {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) : Filter.Tendsto (fun (s : ℕ) => 2 ^ s * ↑(beta δ₁ s)) Filter.atTop (nhds 0)

theorem KamProject.Arnold1963.Iteration.InitialParameters.frequency_budget_summable {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) : Summable fun (s : ℕ) => ↑(beta δ₁ s) * ↑(delta δ₁ s)

theorem KamProject.Arnold1963.Iteration.InitialParameters.frequency_tail_lt {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s : ℕ) : ∑' (j : ℕ), ↑(beta δ₁ (j + s)) * ↑(delta δ₁ (j + s)) < ↑(beta δ₁ s) / 2