Construct new domains from the selected corrected inverse and prove all buffer inclusions.

def KamProject.Arnold1963.frequencyOuterRadius (Θ β : NNReal) : NNReal

The outer frequency erosion required for the corrected chart construction.

Equations

• KamProject.Arnold1963.frequencyOuterRadius Θ β = (5 + Θ) * β

def KamProject.Arnold1963.frequencyLossRadius (Θ β b : NNReal) : NNReal

The total frequency erosion budgeting a domain restriction and the corrected chart.

Equations

• KamProject.Arnold1963.frequencyLossRadius Θ β b = 2 * Θ * b + KamProject.Arnold1963.frequencyOuterRadius Θ β

structure KamProject.Arnold1963.FrequencyChangeInput {n : ℕ} (A g Δ : ComplexSpace n → ComplexSpace n) (G Ω : Set (ComplexSpace n)) (β κ θ Θ : NNReal) : Prop

The analytic chart, small correction and derivative bounds required for frequency change.

• chart : AnalyticFrequencyChart A g G Ω
• radius_pos : 0 < β
• contraction : κ < 1
• lower_pos : 0 < θ
• lower_le_upper : θ ≤ Θ
• lower (p : ComplexSpace n) : p ∈ G → ∀ (v : ComplexSpace n), ↑θ * ‖v‖ ≤ ‖(fderiv ℂ A p) v‖
• upper (p : ComplexSpace n) : p ∈ G → ‖fderiv ℂ A p‖ ≤ ↑Θ
• analytic : AnalyticOnNhd ℂ Δ (erosion G β)
• bounded : NormBoundOn Δ (erosion G β) ↑β
• derivative (p : ComplexSpace n) : p ∈ erosion G β → ‖fderiv ℂ Δ p‖ ≤ ↑κ * ↑θ
• conj (p : ComplexSpace n) : p ∈ erosion G β → Δ (conjVec p) = conjVec (Δ p)

def KamProject.Arnold1963.FrequencyChangeInput.oldImage {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} : FrequencyChangeInput A g Δ G Ω β κ θ Θ → Set (ComplexSpace n)

The old frequency image of the once-eroded action domain.

Equations

• x✝.oldImage = A '' KamProject.Arnold1963.erosion G β

noncomputable def KamProject.Arnold1963.FrequencyChangeInput.newInverse {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) : ComplexSpace n → ComplexSpace n

The corrected inverse chart on the old frequency image.

Equations

• h.newInverse = KamProject.Arnold1963.correctedFrequencyInverse g Δ h.oldImage β

def KamProject.Arnold1963.FrequencyChangeInput.outerFrequency {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} : FrequencyChangeInput A g Δ G Ω β κ θ Θ → Set (ComplexSpace n)

The outer eroded frequency domain retained by the corrected chart.

Equations

• x✝.outerFrequency = KamProject.Arnold1963.erosion Ω (KamProject.Arnold1963.frequencyOuterRadius Θ β)

def KamProject.Arnold1963.FrequencyChangeInput.outerDomain {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) : Set (ComplexSpace n)

The corrected action domain obtained from the outer frequency domain.

Equations

• h.outerDomain = h.newInverse '' h.outerFrequency

def KamProject.Arnold1963.FrequencyChangeInput.innerFrequency {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} : FrequencyChangeInput A g Δ G Ω β κ θ Θ → (Ω₀ : Set (ComplexSpace n)) → (b : NNReal) → Set (ComplexSpace n)

The inner frequency domain with the additional localization loss budget.

Equations

• x✝.innerFrequency Ω₀ b = KamProject.Arnold1963.erosion Ω₀ (KamProject.Arnold1963.frequencyLossRadius Θ β b)

def KamProject.Arnold1963.FrequencyChangeInput.innerDomain {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) (Ω₀ : Set (ComplexSpace n)) (b : NNReal) : Set (ComplexSpace n)

The corrected action domain obtained from the inner frequency domain.

Equations

• h.innerDomain Ω₀ b = h.newInverse '' h.innerFrequency Ω₀ b

theorem KamProject.Arnold1963.FrequencyChangeInput.oldImage_subset {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) : h.oldImage ⊆ Ω

theorem KamProject.Arnold1963.FrequencyChangeInput.oldInverse_maps {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) : Set.MapsTo g h.oldImage (erosion G β)

theorem KamProject.Arnold1963.FrequencyChangeInput.oldImage_conj {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) : ConjInvariant h.oldImage

theorem KamProject.Arnold1963.FrequencyChangeInput.shiftData {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) : FrequencyShiftData (Δ ∘ g) h.oldImage β κ

theorem KamProject.Arnold1963.FrequencyChangeInput.outer_subset_target {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) : h.outerFrequency ⊆ frequencyInverseTarget h.oldImage β

theorem KamProject.Arnold1963.FrequencyChangeInput.outer_subset {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) : h.outerDomain ⊆ erosion G β

theorem KamProject.Arnold1963.FrequencyChangeInput.outerChart {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) : AnalyticFrequencyChart (fun (p : ComplexSpace n) => A p + Δ p) h.newInverse h.outerDomain h.outerFrequency

theorem KamProject.Arnold1963.FrequencyChangeInput.new_derivative_bounds {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) {p : ComplexSpace n} (hp : p ∈ h.outerDomain) (v : ComplexSpace n) : ↑θ * (1 - ↑κ) * ‖v‖ ≤ ‖(fderiv ℂ (fun (x : ComplexSpace n) => A x + Δ x) p) v‖ ∧ ‖(fderiv ℂ (fun (x : ComplexSpace n) => A x + Δ x) p) v‖ ≤ ↑Θ * (1 + ↑κ) * ‖v‖

theorem KamProject.Arnold1963.FrequencyChangeInput.new_upper {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) {p : ComplexSpace n} (hp : p ∈ h.outerDomain) : ‖fderiv ℂ (fun (x : ComplexSpace n) => A x + Δ x) p‖ ≤ 2 * ↑Θ

theorem KamProject.Arnold1963.FrequencyChangeInput.new_upper_sharp {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) {p : ComplexSpace n} (hp : p ∈ h.outerDomain) : ‖fderiv ℂ (fun (x : ComplexSpace n) => A x + Δ x) p‖ ≤ ↑Θ * (1 + ↑κ)

theorem KamProject.Arnold1963.FrequencyChangeInput.new_lower_pos {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) : 0 < ↑θ * (1 - ↑κ)

theorem KamProject.Arnold1963.FrequencyChangeInput.inner_subset_buffer {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) {Ω₀ : Set (ComplexSpace n)} (hΩ₀ : Ω₀ ⊆ Ω) (b : NNReal) : h.innerFrequency Ω₀ b ⊆ erosion h.outerFrequency (2 * Θ * b)

theorem KamProject.Arnold1963.FrequencyChangeInput.inner_subset_outerFrequency {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) {Ω₀ : Set (ComplexSpace n)} (hΩ₀ : Ω₀ ⊆ Ω) (b : NNReal) : h.innerFrequency Ω₀ b ⊆ h.outerFrequency

theorem KamProject.Arnold1963.FrequencyChangeInput.inner_subset_outerDomain {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) {Ω₀ : Set (ComplexSpace n)} (hΩ₀ : Ω₀ ⊆ Ω) (b : NNReal) : h.innerDomain Ω₀ b ⊆ h.outerDomain

theorem KamProject.Arnold1963.FrequencyChangeInput.innerChart {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) {Ω₀ : Set (ComplexSpace n)} (hΩ₀ : Ω₀ ⊆ Ω) (hc : IsCompact Ω₀) (hj : ConjInvariant Ω₀) (b : NNReal) : AnalyticFrequencyChart (fun (p : ComplexSpace n) => A p + Δ p) h.newInverse (h.innerDomain Ω₀ b) (h.innerFrequency Ω₀ b)

theorem KamProject.Arnold1963.FrequencyChangeInput.inner_subset_erosion {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) {Ω₀ : Set (ComplexSpace n)} (hΩ₀ : Ω₀ ⊆ Ω) (b : NNReal) : h.innerDomain Ω₀ b ⊆ erosion h.outerDomain b

theorem KamProject.Arnold1963.FrequencyChangeInput.neighborhood_subset {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) {Ω₀ : Set (ComplexSpace n)} (hΩ₀ : Ω₀ ⊆ Ω) (b : NNReal) : closedBallNeighborhood (h.innerDomain Ω₀ b) b ⊆ h.outerDomain

theorem KamProject.Arnold1963.FrequencyChangeInput.neighborhood_maps {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) {Ω₀ : Set (ComplexSpace n)} (hΩ₀ : Ω₀ ⊆ Ω) (b : NNReal) : Set.MapsTo (fun (p : ComplexSpace n) => A p + Δ p) (closedBallNeighborhood (h.innerDomain Ω₀ b) b) Ω₀

theorem KamProject.Arnold1963.FrequencyChangeInput.old_image_covers_inner_erosion {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) {Ω₀ : Set (ComplexSpace n)} (hΩ₀ : Ω₀ ⊆ Ω) (b : NNReal) : erosion (h.innerFrequency Ω₀ b) β ⊆ A '' h.innerDomain Ω₀ b

theorem KamProject.Arnold1963.FrequencyChangeInput.measure_loss {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) {Ω₀ : Set (ComplexSpace n)} (hΩ₀ : Ω₀ ⊆ Ω) (hc : IsCompact Ω₀) (b : NNReal) : realVolume (G \ h.innerDomain Ω₀ b) ≤ ENNReal.ofReal ((↑θ)⁻¹ ^ n) * realVolume (Ω \ erosion Ω₀ (frequencyLossRadius Θ β b + β))