Supporting results for the analytic Hamiltonian KAM construction.

theorem KamProject.Arnold1963.mem_erosion_angleStrip {n : ℕ} {q : ComplexSpace n} {σ r : NNReal} (hq : ‖imagPart q‖ + ↑r ≤ ↑σ) : q ∈ erosion (angleStrip n σ) r

theorem KamProject.Arnold1963.FundamentalParameters.double_gamma_le {n : ℕ} {ρ β δ γ : NNReal} {K M Θ : ℝ} (b : FundamentalParameters n ρ β δ γ K M Θ) : γ + γ ≤ ρ

theorem KamProject.Arnold1963.FundamentalParameters.beta_delta_le_gamma {n : ℕ} {ρ β δ γ : NNReal} {K M Θ : ℝ} (b : FundamentalParameters n ρ β δ γ K M Θ) : β + δ ≤ γ

theorem KamProject.Arnold1963.FundamentalParameters.triple_beta_le {n : ℕ} {ρ β δ γ : NNReal} {K M Θ : ℝ} (b : FundamentalParameters n ρ β δ γ K M Θ) : β + β + β ≤ ρ - (δ + δ)

theorem KamProject.Arnold1963.FundamentalParameters.action_buffer_loss_lt {n : ℕ} {ρ β δ γ : NNReal} {K M Θ : ℝ} (b : FundamentalParameters n ρ β δ γ K M Θ) : 2 * ↑δ + (3 * ↑β + ↑δ) < 2 * ↑γ

theorem KamProject.Arnold1963.FundamentalParameters.target_angle_buffer {n : ℕ} {ρ β δ γ : NNReal} {K M Θ : ℝ} (b : FundamentalParameters n ρ β δ γ K M Θ) {q : ComplexSpace n} (hq : q ∈ angleStrip n (ρ - (γ + γ))) : q ∈ erosion (angleStrip n (ρ - (δ + δ))) (β + β + β + δ)

theorem KamProject.Arnold1963.FundamentalParameters.target_subset {n : ℕ} {ρ β δ γ : NNReal} {K M Θ : ℝ} (b : FundamentalParameters n ρ β δ γ K M Θ) (E : Set (ComplexSpace n)) : phaseDomain (erosion E (β + β)) (ρ - (γ + γ)) ⊆ generatingTarget E (angleStrip n (ρ - (δ + δ))) β

theorem KamProject.Arnold1963.FundamentalParameters.shifted_angle_tail {n : ℕ} {ρ β δ γ : NNReal} {K M Θ : ℝ} (b : FundamentalParameters n ρ β δ γ K M Θ) {q Q : ComplexSpace n} (hQ : Q ∈ angleStrip n (ρ - (γ + γ))) (hd : dist q Q ≤ ↑β) : q ∈ angleStrip n (ρ - (δ + γ))

theorem KamProject.Arnold1963.segment_subset_erosion_of_displacement {n : ℕ} {E : Set (ComplexSpace n)} {P p : ComplexSpace n} {β : NNReal} (hP : P ∈ erosion E (β + β)) (hp : ‖p - P‖ ≤ ↑β) : segment ℝ P p ⊆ erosion E β