OAI/GroupTheory/PolycyclicRecognition/Analysis/SkewMeasureFiber.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Recovering a fiber measure from a measure-preserving skew map

  1. theorem OAI.PolycyclicRecognition.measurePreserving_fiber_of_right_skew line 20

    Source documentation

    Cancel the base translation and the right fiber translation, then test on a rectangle of finite positive base measure.

    theorem measurePreserving_fiber_of_right_skew
    (ν : Measure Q) (μ : Measure I) [SFinite ν] [SFinite μ]
    [ν.IsMulLeftInvariant] [μ.IsMulRightInvariant]
    (g : Q) (C : I → I) (hC : Measurable C) (a : Q → I) (ha : Measurable a)
    (hskew : MeasurePreserving (fun p : Q × I => (g * p.1, C p.2 * a p.1))
      (ν.prod μ) (ν.prod μ))
    {B : Set Q} (hB : MeasurableSet B) (hB0 : ν B ≠ 0) (hBtop : ν B ≠ ∞) :
    MeasurePreserving C μ μ := by
…