OAI/GroupTheory/PolycyclicRecognition/Analysis/MeasurePreservingLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.map_le_of_measurePreserving_limit line 18

   Source documentation

   Fatou's lemma on open sets: a pointwise limit of measure preserving maps cannot increase an outer regular target measure.

   theorem map_le_of_measurePreserving_limit
       {X Y : Type*} [MeasurableSpace X] [TopologicalSpace Y]
       [MeasurableSpace Y] [OpensMeasurableSpace Y]
       (μ : Measure X) (ν : Measure Y) [ν.OuterRegular]
       (g : X → Y) (hg : Measurable g) (gn : ℕ → X → Y)
       (hgn : ∀ n, MeasurePreserving (gn n) μ ν)
       (hlim : ∀ x, Tendsto (fun n => gn n x) atTop (𝓝 (g x))) :
       Measure.map g μ ≤ ν := by
   …

2. theorem OAI.PolycyclicRecognition.measurePreserving_homeomorph_limit line 54

   Source documentation

   For homeomorphisms, applying the preceding estimate to both the map and its inverse proves exact measure preservation of the pointwise limit.

   theorem measurePreserving_homeomorph_limit
       {X : Type*} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X]
       (μ : Measure X) [μ.OuterRegular] (e : X ≃ₜ X) (en : ℕ → X ≃ₜ X)
       (hen : ∀ n, MeasurePreserving (en n) μ μ)
       (hlim : ∀ x, Tendsto (fun n => en n x) atTop (𝓝 (e x)))
       (hlimInv : ∀ x, Tendsto (fun n => (en n).symm x) atTop (𝓝 (e.symm x))) :
       MeasurePreserving e μ μ := by
   …