A volume-preserving map of the real cylinder cover which commutes with deck translations induces a measure-preserving cylinder map. The proof compares genuine fundamental domains; it does not integrate a nonzero periodic function over the whole real cover.

@[instance_reducible]

def EulerCylinderMeasureDescent.deckVAdd (P : ℝ) : VAdd (↥(AddSubgroup.zmultiples P)) EulerLiftedGradientSpace.LiftTangent

Deck translation adds an integral multiple of the period to the lifted angle.

Equations

• EulerCylinderMeasureDescent.deckVAdd P = { vadd := fun (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent) => (z.1, ↑c + z.2) }

@[instance_reducible]

def EulerCylinderMeasureDescent.deckAction (P : ℝ) : AddAction (↥(AddSubgroup.zmultiples P)) EulerLiftedGradientSpace.LiftTangent

The AddAction (AddSubgroup.zmultiples P) LiftTangent structure used in cylinder measure descent.

Equations

• EulerCylinderMeasureDescent.deckAction P = { vadd := fun (x1 : ↥(AddSubgroup.zmultiples P)) (x2 : EulerLiftedGradientSpace.LiftTangent) => x1 +ᵥ x2, add_vadd := ⋯, zero_vadd := ⋯ }

theorem EulerCylinderMeasureDescent.deck_apply (P : ℝ) (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent) : c +ᵥ z = (z.1, ↑c + z.2)

theorem EulerCylinderMeasureDescent.deckMeasurable (P : ℝ) : MeasurableConstVAdd (↥(AddSubgroup.zmultiples P)) EulerLiftedGradientSpace.LiftTangent

theorem EulerCylinderMeasureDescent.deckInvariant (P : ℝ) : MeasureTheory.VAddInvariantMeasure (↥(AddSubgroup.zmultiples P)) EulerLiftedGradientSpace.LiftTangent MeasureTheory.volume

theorem EulerCylinderMeasureDescent.coveringMap_deck (P : ℝ) (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent) : EulerLiftedGradientSpace.coveringMap P (c +ᵥ z) = EulerLiftedGradientSpace.coveringMap P z

def EulerCylinderMeasureDescent.strip (P : ℝ) : Set EulerLiftedGradientSpace.LiftTangent

Strip, given by Prod.snd ⁻¹' Ioc (0 : ℝ) P.

Equations

• EulerCylinderMeasureDescent.strip P = Prod.snd ⁻¹' Set.Ioc 0 P

theorem EulerCylinderMeasureDescent.strip_measurable (P : ℝ) : MeasurableSet (strip P)

theorem EulerCylinderMeasureDescent.strip_fundamental (P : ℝ) [Fact (0 < P)] : MeasureTheory.IsAddFundamentalDomain (↥(AddSubgroup.zmultiples P)) (strip P) MeasureTheory.volume

theorem EulerCylinderMeasureDescent.coveringMap_measurePreserving (P : ℝ) [Fact (0 < P)] : MeasureTheory.MeasurePreserving (EulerLiftedGradientSpace.coveringMap P) (MeasureTheory.volume.restrict (strip P)) (EulerLiftedGradientSpace.liftMeasure P)

theorem EulerCylinderMeasureDescent.quotient_set_measure (P : ℝ) [Fact (0 < P)] (s : Set (EulerLiftedGradientSpace.LiftDomain P)) (hs : MeasurableSet s) : (EulerLiftedGradientSpace.liftMeasure P) s = MeasureTheory.volume (EulerLiftedGradientSpace.coveringMap P ⁻¹' s ∩ strip P)

theorem EulerCylinderMeasureDescent.measurePreserving_of_cover (P : ℝ) [Fact (0 < P)] (f : EulerLiftedGradientSpace.LiftTangent → EulerLiftedGradientSpace.LiftTangent) (g : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.LiftDomain P) (hf : MeasureTheory.MeasurePreserving f MeasureTheory.volume MeasureTheory.volume) (hg : Measurable g) (hdeck : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = ((f z).1, ↑c + (f z).2)) (hcover : ∀ (z : EulerLiftedGradientSpace.LiftTangent), EulerLiftedGradientSpace.coveringMap P (f z) = g (EulerLiftedGradientSpace.coveringMap P z)) : MeasureTheory.MeasurePreserving g (EulerLiftedGradientSpace.liftMeasure P) (EulerLiftedGradientSpace.liftMeasure P)