Real symplectic Jacobians. Real derivatives commute with complexification, and the symplectic matrix determinant theorem gives the real change-of-variables identity.

noncomputable def KamProject.Arnold1963.realPhaseBasis (n : ℕ) : Module.Basis (Fin n ⊕ Fin n) ℝ (RealPhaseCover n)

The coordinate basis of unwrapped real action-angle phase space.

Equations

• KamProject.Arnold1963.realPhaseBasis n = (Pi.basisFun ℝ (Fin n)).prod (Pi.basisFun ℝ (Fin n))

theorem KamProject.Arnold1963.complexifyPhase_realPhaseBasis {n : ℕ} (j : Fin n ⊕ Fin n) : complexifyPhase ((realPhaseBasis n) j) = phaseDirection j

theorem KamProject.Arnold1963.realPhase_det_eq_one {n : ℕ} (L : ComplexPhaseSpace n →L[ℂ] ComplexPhaseSpace n) (A : RealPhaseCover n →L[ℝ] RealPhaseCover n) (hL : IsSymplecticLinear ↑L) (hA : ∀ (v : RealPhaseCover n), complexifyPhase (A v) = L (complexifyPhase v)) : LinearMap.det ↑A = 1

theorem KamProject.Arnold1963.realPhaseDerivative_commutes {n : ℕ} {f : ComplexPhaseSpace n → ComplexPhaseSpace n} {x : RealPhaseCover n} (hf : DifferentiableAt ℂ f (complexifyPhase x)) (hr : ∀ᶠ (y : RealPhaseCover n) in nhds x, complexifyPhase (realPhaseRestriction f y) = f (complexifyPhase y)) (v : RealPhaseCover n) : complexifyPhase ((realPhaseDerivative (fderiv ℂ f (complexifyPhase x))) v) = (fderiv ℂ f (complexifyPhase x)) (complexifyPhase v)

theorem KamProject.Arnold1963.Iteration.InitialData.cumulative_real_near {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) {x : RealPhaseCover n} (hx : x.1 ∈ realSlice (limitDomain b h)) : ∀ᶠ (y : RealPhaseCover n) in nhds x, complexifyPhase (realPhaseRestriction (cumulative b h s) y) = cumulative b h s (complexifyPhase y)

theorem KamProject.Arnold1963.Iteration.InitialData.cumulative_real_det {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) {x : RealPhaseCover n} (hx : x.1 ∈ realSlice (limitDomain b h)) : LinearMap.det ↑(fderiv ℝ (realPhaseRestriction (cumulative b h s)) x) = 1

theorem KamProject.Arnold1963.Iteration.InitialData.cumulative_real_volume {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) {K : Set (RealPhaseCover n)} (hK : MeasurableSet K) (hsub : ∀ x ∈ K, x.1 ∈ realSlice (limitDomain b h)) : MeasureTheory.volume (realPhaseRestriction (cumulative b h s) '' K) = MeasureTheory.volume K