Choose a positive perturbation threshold on each geometric patch before the perturbation is specified, using the existing numerical thresholds.

noncomputable def KamProject.Arnold1963.HamiltonianPatch.seed {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} (c : HamiltonianPatch n H₀ ambient) (ρ : NNReal) (κ : ℝ) : NNReal

The initial smallness seed selected from a Hamiltonian patch's numerical bounds.

Equations

• c.seed ρ κ = (KamProject.Arnold1963.threshold5 n (↑c.lower) (↑c.upper) (↑ρ) κ c.typeConstant / 2).toNNReal

noncomputable def KamProject.Arnold1963.HamiltonianPatch.threshold {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} (c : HamiltonianPatch n H₀ ambient) (ρ : NNReal) (κ : ℝ) : ℝ

The positive perturbation threshold associated with a Hamiltonian patch.

Equations

• c.threshold ρ κ = KamProject.Arnold1963.initialPerturbationThreshold n (↑c.lower) (↑c.upper) (↑ρ) κ c.typeConstant

theorem KamProject.Arnold1963.HamiltonianPatch.threshold_pos {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} (c : HamiltonianPatch n H₀ ambient) (hn : 0 < n) {ρ : NNReal} {κ : ℝ} (hρ : 0 < ρ) (hκ : 0 < κ) : 0 < c.threshold ρ κ

theorem KamProject.Arnold1963.HamiltonianPatch.seed_coe {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} (c : HamiltonianPatch n H₀ ambient) (hn : 0 < n) {ρ : NNReal} {κ : ℝ} (hρ : 0 < ρ) (hκ : 0 < κ) : ↑(c.seed ρ κ) = threshold5 n (↑c.lower) (↑c.upper) (↑ρ) κ c.typeConstant / 2

theorem KamProject.Arnold1963.HamiltonianPatch.parameters {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} (c : HamiltonianPatch n H₀ ambient) (hn : 0 < n) {ρ : NNReal} {κ : ℝ} (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hκ : 0 < κ) (hκ1 : κ < 1) : Iteration.InitialParameters n (c.seed ρ κ) c.lower c.upper ρ κ c.typeConstant

theorem KamProject.Arnold1963.HamiltonianPatch.threshold_eq_initial_bound {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} (c : HamiltonianPatch n H₀ ambient) (hn : 0 < n) {ρ : NNReal} {κ : ℝ} (hρ : 0 < ρ) (hκ : 0 < κ) : c.threshold ρ κ = Iteration.perturbation n (c.seed ρ κ) 0

def KamProject.Arnold1963.HamiltonianPatch.initialData {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} (c : HamiltonianPatch n H₀ ambient) (hn : 0 < n) {ρ σ : NNReal} {κ : ℝ} (hρ : 0 < ρ) (hκ : 0 < κ) (f : AnalyticPhaseFunction n ambient σ) (hρσ : ρ ≤ σ) (hf : f.uniformNorm ≤ c.threshold ρ κ) : Iteration.InitialData n c.frequencyDomain (c.seed ρ κ) c.lower c.upper ρ c.typeConstant

Initial iteration data constructed by restricting a sufficiently small global perturbation.

Equations

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

theorem KamProject.Arnold1963.HamiltonianPatch.local_result {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} (c : HamiltonianPatch n H₀ ambient) (hn : 0 < n) {ρ σ : NNReal} {κ : ℝ} (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hκ : 0 < κ) (hκ1 : κ < 1) (f : AnalyticPhaseFunction n ambient σ) (hρσ : ρ ≤ σ) (hf : f.uniformNorm ≤ c.threshold ρ κ) : LocalKAMResult ⋯ (c.initialData hn hρ hκ f hρσ hf)

theorem KamProject.Arnold1963.HamiltonianPatch.exists_common_threshold {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} (s : Finset (HamiltonianPatch n H₀ ambient)) (hn : 0 < n) {ρ : NNReal} {κ : ℝ} (hρ : 0 < ρ) (hκ : 0 < κ) : ∃ (M : ℝ), 0 < M ∧ ∀ c ∈ s, M ≤ c.threshold ρ κ