Construct the inverse of a frequency shift from derivative smallness, including a consistent analytic branch on the target domain.

def KamProject.Arnold1963.frequencyShift {n : ℕ} (a : ComplexSpace n → ComplexSpace n) (x : ComplexSpace n) : ComplexSpace n

The identity frequency map plus the specified correction.

Equations

• KamProject.Arnold1963.frequencyShift a x = x + a x

def KamProject.Arnold1963.frequencyInverseSource {n : ℕ} (V : Set (ComplexSpace n)) (β : NNReal) : Set (ComplexSpace n)

The thrice-eroded source on which the frequency shift is inverted.

Equations

• KamProject.Arnold1963.frequencyInverseSource V β = KamProject.Arnold1963.erosion V (β + β + β)

def KamProject.Arnold1963.frequencyInverseTarget {n : ℕ} (V : Set (ComplexSpace n)) (β : NNReal) : Set (ComplexSpace n)

The five-times-eroded target used to control the frequency inverse.

Equations

• KamProject.Arnold1963.frequencyInverseTarget V β = KamProject.Arnold1963.erosion V (β + β + β + β + β)

noncomputable def KamProject.Arnold1963.frequencyInverse {n : ℕ} (a : ComplexSpace n → ComplexSpace n) (V : Set (ComplexSpace n)) (β : NNReal) (b : ComplexSpace n) : ComplexSpace n

A set-restricted inverse of the frequency shift on its eroded source.

Equations

• KamProject.Arnold1963.frequencyInverse a V β = Function.invFunOn (KamProject.Arnold1963.frequencyShift a) (KamProject.Arnold1963.frequencyInverseSource V β)

structure KamProject.Arnold1963.FrequencyShiftData {n : ℕ} (a : ComplexSpace n → ComplexSpace n) (V : Set (ComplexSpace n)) (β κ : NNReal) : Prop

Analyticity, boundedness and contraction data for inverting a small frequency shift.

• radius_pos : 0 < β
• contraction : κ < 1
• analytic : AnalyticOnNhd ℂ a V
• bounded : NormBoundOn a V ↑β
• derivative (x : ComplexSpace n) : x ∈ V → ‖fderiv ℂ a x‖ ≤ ↑κ

theorem KamProject.Arnold1963.FrequencyShiftData.lipschitz_ball {n : ℕ} {a : ComplexSpace n → ComplexSpace n} {V : Set (ComplexSpace n)} {β κ : NNReal} (d : FrequencyShiftData a V β κ) {x : ComplexSpace n} {r : NNReal} (hx : x ∈ erosion V r) : LipschitzOnWith κ a (Metric.closedBall x ↑r)

theorem KamProject.Arnold1963.FrequencyShiftData.shift_injOn {n : ℕ} {a : ComplexSpace n → ComplexSpace n} {V : Set (ComplexSpace n)} {β κ : NNReal} (d : FrequencyShiftData a V β κ) : Set.InjOn (frequencyShift a) (frequencyInverseSource V β)

theorem KamProject.Arnold1963.FrequencyShiftData.shift_analytic {n : ℕ} {a : ComplexSpace n → ComplexSpace n} {V : Set (ComplexSpace n)} {β κ : NNReal} (d : FrequencyShiftData a V β κ) {x : ComplexSpace n} (hx : x ∈ V) : AnalyticAt ℂ (frequencyShift a) x

theorem KamProject.Arnold1963.FrequencyShiftData.shift_derivative {n : ℕ} {a : ComplexSpace n → ComplexSpace n} {V : Set (ComplexSpace n)} {β κ : NNReal} (d : FrequencyShiftData a V β κ) {x : ComplexSpace n} (hx : x ∈ V) : fderiv ℂ (frequencyShift a) x = ContinuousLinearMap.id ℂ (ComplexSpace n) + fderiv ℂ a x

theorem KamProject.Arnold1963.FrequencyShiftData.inverse_spec {n : ℕ} {a : ComplexSpace n → ComplexSpace n} {V : Set (ComplexSpace n)} {β κ : NNReal} (d : FrequencyShiftData a V β κ) {y : ComplexSpace n} (hy : y ∈ frequencyInverseTarget V β) : frequencyInverse a V β y ∈ erosion V (β + β + β + β) ∧ frequencyShift a (frequencyInverse a V β y) = y ∧ ‖frequencyInverse a V β y - y‖ ≤ ↑β

theorem KamProject.Arnold1963.FrequencyShiftData.inverse_analytic_right {n : ℕ} {a : ComplexSpace n → ComplexSpace n} {V : Set (ComplexSpace n)} {β κ : NNReal} (d : FrequencyShiftData a V β κ) {y : ComplexSpace n} (hy : y ∈ frequencyInverseTarget V β) : AnalyticAt ℂ (frequencyInverse a V β) y ∧ ∀ᶠ (z : ComplexSpace n) in nhds y, frequencyShift a (frequencyInverse a V β z) = z

theorem KamProject.Arnold1963.FrequencyShiftData.target_subset_image {n : ℕ} {a : ComplexSpace n → ComplexSpace n} {V : Set (ComplexSpace n)} {β κ : NNReal} (d : FrequencyShiftData a V β κ) : frequencyInverseTarget V β ⊆ frequencyShift a '' frequencyInverseSource V β

theorem KamProject.Arnold1963.FrequencyShiftData.inverse_conj {n : ℕ} {a : ComplexSpace n → ComplexSpace n} {V : Set (ComplexSpace n)} {β κ : NNReal} (d : FrequencyShiftData a V β κ) (hV : ConjInvariant V) (ha : ∀ x ∈ V, a (conjVec x) = conjVec (a x)) {y : ComplexSpace n} (hy : y ∈ frequencyInverseTarget V β) : frequencyInverse a V β (conjVec y) = conjVec (frequencyInverse a V β y)

theorem KamProject.Arnold1963.FrequencyShiftData.inverse_real {n : ℕ} {a : ComplexSpace n → ComplexSpace n} {V : Set (ComplexSpace n)} {β κ : NNReal} (d : FrequencyShiftData a V β κ) (hV : ConjInvariant V) (ha : ∀ x ∈ V, a (conjVec x) = conjVec (a x)) {y : RealSpace n} (hy : complexify y ∈ frequencyInverseTarget V β) : complexify (realPart (frequencyInverse a V β (complexify y))) = frequencyInverse a V β (complexify y)

theorem KamProject.Arnold1963.FrequencyShiftData.derivative_bounds {n : ℕ} {a : ComplexSpace n → ComplexSpace n} {V : Set (ComplexSpace n)} {β κ : NNReal} (d : FrequencyShiftData a V β κ) {x : ComplexSpace n} (hx : x ∈ V) (v : ComplexSpace n) : (1 - ↑κ) * ‖v‖ ≤ ‖(fderiv ℂ (frequencyShift a) x) v‖ ∧ ‖(fderiv ℂ (frequencyShift a) x) v‖ ≤ (1 + ↑κ) * ‖v‖