OAI/GroupTheory/PolycyclicRecognition/Analysis/PairMeanApproximation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.normalizedPairMean_coboundary_approximation line 19

   Source documentation

   The published reduced-cohomology input supplies measurable compact-uniform transfers for the concrete mean, whose metric control is already proved.

   theorem normalizedPairMean_coboundary_approximation
       {G W : Type*} [Group G] [MetricSpace G] [ProperSpace G]
       [IsTopologicalGroup G] [IsIsometricSMul G G]
       [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W]
       [SecondCountableTopology W] [MeasurableSpace W] [BorelSpace W] {Λ : ℝ≥0}
       [MeasurableSpace (NormalizedPair G Λ)] [BorelSpace (NormalizedPair G Λ)]
       (μ : Measure (NormalizedPair G Λ)) [IsProbabilityMeasure μ]
       [ErgodicSMul G (NormalizedPair G Λ) μ] [μ.InnerRegularCompactLTTop]
       (hvan : ReducedCohomologyInput G (ZeroMeanL2 (W := W) μ))
   …

   Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.ReducedCohomologyInput, OAI.PolycyclicRecognition.ZeroMeanL2