OAI/GroupTheory/PolycyclicRecognition/Analysis/MeanProbabilityConverse.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.bad_probability_tendsto_zero_of_mean line 14

   Source documentation

   Markov's inequality gives the probability direction for an integrable nonnegative profile error, without a global bound off its sampling cell.

   theorem bad_probability_tendsto_zero_of_mean
       {X : Type*} [MeasurableSpace X] (μ : ℕ → ProbabilityMeasure X)
       (f : ℕ → X → ℝ) (hi : ∀ n, Integrable (f n) (μ n : Measure X))
       (hf : ∀ n, 0 ≤ᵐ[(μ n : Measure X)] f n)
       (hm : Tendsto (fun n => ∫ x, f n x ∂(μ n : Measure X)) atTop (𝓝 0))
       {ε : ℝ} (hε : 0 < ε) :
       Tendsto (fun n => (μ n : Measure X) {x | ε ≤ f n x}) atTop (𝓝 0) := by
   …