Documentation

LeanPool.ArnoldKAM.Arnold1963.Iteration.InitialParameters

Initial numerical hypotheses and their consequences at every iteration stage.

structure KamProject.Arnold1963.Iteration.InitialParameters (n : ℕ) (δ₁ θ₀ Θ₀ ρ₀ : NNReal) (κ D : ℝ) :

Positive initial parameters satisfying every smallness and measure-budget constraint.

dimension_pos : 0 < n
delta_pos : 0 < δ₁
lower_pos : 0 < θ₀
lower_lt_one : θ₀ < 1
upper_gt_one : 1 < Θ₀
width_pos : 0 < ρ₀
width_le_one : ρ₀ ≤ 1
fraction_pos : 0 < κ
fraction_lt_one : κ < 1
type_constant_pos : 0 < D
small : ↑δ₁ < threshold5 n (↑θ₀) (↑Θ₀) (↑ρ₀) κ D

Instances For

theorem KamProject.Arnold1963.Iteration.threshold1_mono {n : ℕ} {θ θ' Θ Θ' : ℝ} (hθ : θ ≤ θ') (hΘ : 0 < Θ') (hΘΘ : Θ' ≤ Θ) :

threshold1 n θ Θ ≤ threshold1 n θ' Θ'

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

δ₁ < 1 / 4

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

δ₁ < 1

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

0 < delta δ₁ s

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

delta δ₁ s ≤ δ₁

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

0 < gamma n δ₁ s

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

gamma n δ₁ s ≤ gamma n δ₁ 0

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

↑(gamma n δ₁ s) < 1 / 4

theorem KamProject.Arnold1963.Iteration.InitialParameters.lower_step_le (θ₀ δ₁ : NNReal) (s : ℕ) :

lower θ₀ δ₁ s ≤ θ₀

theorem KamProject.Arnold1963.Iteration.InitialParameters.upper_step_ge (Θ₀ δ₁ : NNReal) (s : ℕ) :

Θ₀ ≤ upper Θ₀ δ₁ s

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

↑(delta δ₁ s) < threshold1 n ↑(lower θ₀ δ₁ s) ↑(upper Θ₀ δ₁ s)

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

StrictAnti (delta δ₁)