Derivative bounds for finite cumulative transformations on the real cover. Restricting to real coordinates and taking real parts does not increase the operator norm.

noncomputable def KamProject.Arnold1963.complexifyPhaseCLM (n : ℕ) : RealPhaseCover n →L[ℝ] ComplexPhaseSpace n

Complexification of action and angle coordinates as a real continuous linear map.

Equations

• KamProject.Arnold1963.complexifyPhaseCLM n = (KamProject.Arnold1963.complexifyCLM n).prodMap (KamProject.Arnold1963.complexifyCLM n)

noncomputable def KamProject.Arnold1963.realPartPhaseCLM (n : ℕ) : ComplexPhaseSpace n →L[ℝ] RealPhaseCover n

Real-part projection of phase coordinates as a real continuous linear map.

Equations

• KamProject.Arnold1963.realPartPhaseCLM n = (KamProject.Arnold1963.realPartCLM n).prodMap (KamProject.Arnold1963.realPartCLM n)

@[simp]

theorem KamProject.Arnold1963.complexifyPhaseCLM_apply {n : ℕ} (x : RealPhaseCover n) : (complexifyPhaseCLM n) x = complexifyPhase x

@[simp]

theorem KamProject.Arnold1963.realPartPhaseCLM_apply {n : ℕ} (z : ComplexPhaseSpace n) : (realPartPhaseCLM n) z = realPartPhase z

@[simp]

theorem KamProject.Arnold1963.norm_complexifyPhase {n : ℕ} (x : RealPhaseCover n) : ‖complexifyPhase x‖ = ‖x‖

theorem KamProject.Arnold1963.norm_realPartPhase_le {n : ℕ} (z : ComplexPhaseSpace n) : ‖realPartPhase z‖ ≤ ‖z‖

def KamProject.Arnold1963.realPhaseRestriction {n : ℕ} (f : ComplexPhaseSpace n → ComplexPhaseSpace n) : RealPhaseCover n → RealPhaseCover n

Restriction of a complex phase map to real input and real output coordinates.

Equations

• KamProject.Arnold1963.realPhaseRestriction f = KamProject.Arnold1963.realPartPhase ∘ f ∘ KamProject.Arnold1963.complexifyPhase

noncomputable def KamProject.Arnold1963.realPhaseDerivative {n : ℕ} (L : ComplexPhaseSpace n →L[ℂ] ComplexPhaseSpace n) : RealPhaseCover n →L[ℝ] RealPhaseCover n

The real continuous linear derivative induced by a complex phase derivative.

Equations

• KamProject.Arnold1963.realPhaseDerivative L = KamProject.Arnold1963.realPartPhaseCLM n ∘SL ContinuousLinearMap.restrictScalars ℝ L ∘SL KamProject.Arnold1963.complexifyPhaseCLM n

theorem KamProject.Arnold1963.hasFDerivAt_realPhaseRestriction {n : ℕ} {f : ComplexPhaseSpace n → ComplexPhaseSpace n} {x : RealPhaseCover n} (hf : DifferentiableAt ℂ f (complexifyPhase x)) : HasFDerivAt (realPhaseRestriction f) (realPhaseDerivative (fderiv ℂ f (complexifyPhase x))) x

theorem KamProject.Arnold1963.norm_realPhaseDerivative_le {n : ℕ} (L : ComplexPhaseSpace n →L[ℂ] ComplexPhaseSpace n) : ‖realPhaseDerivative L‖ ≤ ‖L‖

theorem KamProject.Arnold1963.Iteration.InitialData.cumulative_realPhase_value {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) {x : RealPhaseCover n} (hx : complexifyPhase x ∈ phase b h s) : complexifyPhase (realPhaseRestriction (cumulative b h s) x) = cumulative b h s (complexifyPhase x)

theorem KamProject.Arnold1963.Iteration.InitialData.cumulative_real_derivative {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) {x : RealPhaseCover n} (hx : complexifyPhase x ∈ phase b h s) : ‖fderiv ℝ (realPhaseRestriction (cumulative b h s)) x‖ ≤ 2 ^ s