OAI/GroupTheory/PolycyclicRecognition/Analysis/BoundedProbabilityMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.bounded_mean_tendsto_zero_of_bad_probabilities line 16

   Source documentation

   The compact profile bounds turn a vanishing bad-event probability into vanishing mean error, even when the sampling law changes with the scale.

   theorem bounded_mean_tendsto_zero_of_bad_probabilities
       {X : Type*} [MeasurableSpace X]
       (μ : ℕ → ProbabilityMeasure X) (f : ℕ → X → ℝ)
       (hf : ∀ n, Measurable (f n)) {C : ℝ}
       (hbound : ∀ n x, 0 ≤ f n x ∧ f n x ≤ C)
       (hbad : ∀ ε : ℝ, 0 < ε →
         Tendsto (fun n => (μ n : Measure X) {x | ε ≤ f n x}) atTop (𝓝 0)) :
       Tendsto (fun n => ∫ x, f n x ∂(μ n : Measure X)) atTop (𝓝 0) := by
   …