OAI/GroupTheory/PolycyclicRecognition/Algebra/FactorOccupationLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.invariant_of_weak_factor_occupation_limit line 14

   Source documentation

   Separate right-translation estimates in the two factors suffice for full invariance. Factorizations may be nonunique.

   theorem invariant_of_weak_factor_occupation_limit
       {G X ι : Type*} [Group G] [MetricSpace X] [CompactSpace X]
       [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X]
       [MulAction G X] [ContinuousConstSMul G X]
       (N D : Subgroup G)
       (hgen : ∀ g : G, ∃ n : N, ∃ d : D, g = (n : G) * d)
       {l : Filter ι} [l.NeBot]
       (μs : ι → ProbabilityMeasure X) (μ : ProbabilityMeasure X)
       (hlim : Tendsto μs l (𝓝 μ))
       (hN : ∀ (n : N) (f : C(X, ℝ)), Tendsto
         (fun i => (∫ x, f ((n : G) • x) ∂(μs i : Measure X)) -
           ∫ x, f x ∂(μs i : Measure X)) l (𝓝 0))
   …