OAI/GroupTheory/PolycyclicRecognition/Analysis/StationaryIntegralMicrosteps.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.stationary_integral_microsteps line 17

   Source documentation

   Restrict the stationary real-time estimate to integer times and put it into the real integral form used by the dominated microstep argument.

   theorem stationary_integral_microsteps
       {G W : Type*} [Group G] [MetricSpace G] [ProperSpace G]
       [IsTopologicalGroup G] [IsIsometricSMul G G]
       [NormedAddCommGroup W] [NormedSpace ℝ W]
       {Λ : ℝ≥0} [MeasurableSpace (NormalizedPair G Λ)] [BorelSpace (NormalizedPair G Λ)]
       (π : G →* Multiplicative W) (hπ : Continuous (fun g => (π g).toAdd))
       (d : ℝ → G) (S : Set W) (μ : Measure (NormalizedPair G Λ))
       (hstat : Tendsto (fun r : ℝ => ∫⁻ p,
         ENNReal.ofReal (infDist (r⁻¹ • pairHeight π (d r) p) S) ∂μ) atTop (𝓝 0)) :
       Tendsto (fun L : ℕ => ∫ p,
         infDist ((L : ℝ)⁻¹ • pairHeight π (d L) p) S ∂μ) atTop (𝓝 0) := by
   …

   Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairHeight