OAI/GroupTheory/PolycyclicRecognition/Algebra/OccupationWeakLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.invariant_of_weak_occupation_limit line 21

   Source documentation

   Vanishing translation errors pass through weak convergence on the compact section. This theorem does not assume invariance of the limiting measure.

   theorem invariant_of_weak_occupation_limit
       {G X ι : Type*} [Group G] [MetricSpace X] [CompactSpace X]
       [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X]
       [MulAction G X] [ContinuousConstSMul G X]
       {l : Filter ι} [l.NeBot]
       (μs : ι → ProbabilityMeasure X) (μ : ProbabilityMeasure X)
       (hlim : Tendsto μs l (𝓝 μ))
       (herror : ∀ (g : G) (f : C(X, ℝ)), Tendsto
         (fun i => (∫ x, f (g • x) ∂(μs i : Measure X)) -
           ∫ x, f x ∂(μs i : Measure X)) l (𝓝 0)) :
       SMulInvariantMeasure G X (μ : Measure X) := by
   …

2. theorem OAI.PolycyclicRecognition.eq_zero_on_support_of_lintegral_eq_zero line 54

   Source documentation

   A continuous nonnegative error with zero integral vanishes on every supported profile, not merely almost everywhere.

   theorem eq_zero_on_support_of_lintegral_eq_zero
       {X : Type*} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X]
       (μ : Measure X) (f : X → ℝ≥0∞) (hf : Continuous f)
       (hzero : ∫⁻ x, f x ∂μ = 0) {x : X} (hx : x ∈ μ.support) : f x = 0 := by
   …