Physical quotient volume for finite cumulative transformations, using their injectivity.

theorem KamProject.Arnold1963.Iteration.InitialData.instFactLtRealOfNatHMulPi : Fact (0 < 2 * Real.pi)

noncomputable def KamProject.Arnold1963.Iteration.InitialData.realCumulative {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) : RealPhaseCover n → RealPhaseCover n

The cumulative phase transformation restricted to unwrapped real coordinates.

Equations

• KamProject.Arnold1963.Iteration.InitialData.realCumulative b h s = KamProject.Arnold1963.realPhaseRestriction (KamProject.Arnold1963.Iteration.InitialData.cumulative b h s)

theorem KamProject.Arnold1963.Iteration.InitialData.real_mem_phase {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)) : complexifyPhase x ∈ phase b h s

theorem KamProject.Arnold1963.Iteration.InitialData.realCumulative_continuous {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) : ContinuousOn (realCumulative b h s) (realSlice (limitDomain b h) ×ˢ Set.univ)

theorem KamProject.Arnold1963.Iteration.InitialData.realCumulative_injOn {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) : Set.InjOn (realCumulative b h s) (realSlice (limitDomain b h) ×ˢ Set.univ)

theorem KamProject.Arnold1963.Iteration.InitialData.realCumulative_shift {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)) (k : FourierIndex n) : realCumulative b h s (realPhaseShift k x) = realPhaseShift k (realCumulative b h s x)

def KamProject.Arnold1963.Iteration.InitialData.retainedCell {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) : Set (RealPhaseCover n)

The limiting real action domain paired with a half-open fundamental angle cell.

Equations

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

theorem KamProject.Arnold1963.Iteration.InitialData.retainedCell_measurable {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) : MeasurableSet (retainedCell b h)

theorem KamProject.Arnold1963.Iteration.InitialData.realCumulative_image_projection_injOn {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) : Set.InjOn torusProjection (realCumulative b h s '' retainedCell b h)

theorem KamProject.Arnold1963.Iteration.InitialData.cumulative_torus_volume {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) : MeasureTheory.volume (torusProjection ∘ realCumulative b h s '' retainedCell b h) = MeasureTheory.volume (retainedCell b h)