OAI/GroupTheory/PolycyclicRecognition/Analysis/SampledProfileIncrements.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.sampled_profile_increment_mem line 18

   Source documentation

   The two-limit occupation estimate implies the increment constraint for every supported profile. Sampling, the exact cocycle identity, and domination are stated separately so that all are checked on the actual chart.

   theorem sampled_profile_increment_mem
       {U V W A G ι : Type*}
       [TopologicalSpace U] [LocallyCompactSpace U] [SecondCountableTopology U]
       [TopologicalSpace V] [LocallyCompactSpace V]
       [NormedAddCommGroup W] [NormedSpace ℝ W]
       [Group G] [MetricSpace G] [ProperSpace G] [IsTopologicalGroup G]
       [IsIsometricSMul G G] [MeasurableSpace A]
       {Λ Kπ : ℝ≥0} [MeasurableSpace (NormalizedPair G Λ)]
       [BorelSpace (NormalizedPair G Λ)]
       (S : Set C(V, W)) (hS : IsCompact S) (K : Set U) (hK : IsCompact K)
       [MeasurableSpace S] [BorelSpace S] [MeasurableSpace K] [BorelSpace K]
       (π : G →* Multiplicative W) (hπ : LipschitzWith Kπ (fun g => (π g).toAdd))
   …

   Mentions: OAI.PolycyclicRecognition.NormalizedPair