Physical quotient volume with angle Haar mass 2 * pi. Countably many half-open cells transfer covering-space volume to the quotient for sets on which projection is injective.

theorem KamProject.Arnold1963.instFactLtRealOfNatHMulPi_leanPool_1 : Fact (0 < 2 * Real.pi)

def KamProject.Arnold1963.phaseCell (n : ℕ) : Set (RealPhaseCover n)

All real actions paired with one half-open fundamental angle cell.

Equations

• KamProject.Arnold1963.phaseCell n = Set.univ ×ˢ KamProject.Arnold1963.realAngleCell n (2 * Real.pi)

theorem KamProject.Arnold1963.measurableSet_phaseCell (n : ℕ) : MeasurableSet (phaseCell n)

theorem KamProject.Arnold1963.continuous_torusProjection {n : ℕ} : Continuous torusProjection

theorem KamProject.Arnold1963.torusProjection_injOn_cell {n : ℕ} : Set.InjOn torusProjection (phaseCell n)

theorem KamProject.Arnold1963.torusRepresentative_mem_cell {n : ℕ} (x : RealPhaseSpace n) : torusRepresentative x ∈ phaseCell n

theorem KamProject.Arnold1963.torusProjection_measurePreserving (n : ℕ) : MeasureTheory.MeasurePreserving torusProjection (MeasureTheory.volume.restrict (phaseCell n)) MeasureTheory.volume

theorem KamProject.Arnold1963.realPhaseShift_eq_add {n : ℕ} (k : FourierIndex n) (x : RealPhaseCover n) : realPhaseShift k x = x + (0, realAngleShift k)

noncomputable def KamProject.Arnold1963.phaseShiftEquiv {n : ℕ} (k : FourierIndex n) : RealPhaseCover n ≃ᵐ RealPhaseCover n

The measurable equivalence translating unwrapped phase space by an integer angle-period shift.

Equations

• KamProject.Arnold1963.phaseShiftEquiv k = MeasurableEquiv.addRight (0, KamProject.Arnold1963.realAngleShift k)

@[simp]

theorem KamProject.Arnold1963.phaseShiftEquiv_apply {n : ℕ} (k : FourierIndex n) (x : RealPhaseCover n) : (phaseShiftEquiv k) x = realPhaseShift k x

theorem KamProject.Arnold1963.phaseShift_measurePreserving {n : ℕ} (k : FourierIndex n) : MeasureTheory.MeasurePreserving (⇑(phaseShiftEquiv k)) MeasureTheory.volume MeasureTheory.volume

def KamProject.Arnold1963.translatedPhaseCell {n : ℕ} (k : FourierIndex n) : Set (RealPhaseCover n)

The translated fundamental phase cell associated with an integer angle-period shift.

Equations

• KamProject.Arnold1963.translatedPhaseCell k = ⇑(KamProject.Arnold1963.phaseShiftEquiv k) '' KamProject.Arnold1963.phaseCell n

theorem KamProject.Arnold1963.measurableSet_translatedPhaseCell {n : ℕ} (k : FourierIndex n) : MeasurableSet (translatedPhaseCell k)

theorem KamProject.Arnold1963.translatedPhaseCell_cover (n : ℕ) : ⋃ (k : FourierIndex n), translatedPhaseCell k = Set.univ

theorem KamProject.Arnold1963.translatedPhaseCell_disjoint (n : ℕ) : Pairwise (Function.onFun Disjoint translatedPhaseCell)

theorem KamProject.Arnold1963.torusProjection_translated_measurePreserving {n : ℕ} (k : FourierIndex n) : MeasureTheory.MeasurePreserving torusProjection (MeasureTheory.volume.restrict (translatedPhaseCell k)) MeasureTheory.volume

theorem KamProject.Arnold1963.torusProjection_injOn_translated {n : ℕ} (k : FourierIndex n) : Set.InjOn torusProjection (translatedPhaseCell k)

theorem KamProject.Arnold1963.torusProjection_volume_piece {n : ℕ} {A : Set (RealPhaseCover n)} (hA : MeasurableSet A) (k : FourierIndex n) (hsub : A ⊆ translatedPhaseCell k) : MeasureTheory.volume (torusProjection '' A) = MeasureTheory.volume A

theorem KamProject.Arnold1963.torusProjection_volume {n : ℕ} {A : Set (RealPhaseCover n)} (hA : MeasurableSet A) (hi : Set.InjOn torusProjection A) : MeasureTheory.volume (torusProjection '' A) = MeasureTheory.volume A

theorem KamProject.Arnold1963.torusProjection_lipschitz {n : ℕ} : LipschitzWith 1 torusProjection