OAI/Probability/InvariantIsing/Haar/MedianMean.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.abs_median_le_bound line 14
2. lemma OAI.InvariantIsing.abs_integral_sub_le_deviation_tail line 43

   Source documentation

   A bounded deviation has mean at most r plus its bound times the r-tail.

   lemma abs_integral_sub_le_deviation_tail {Ω : Type*} [MeasurableSpace Ω]
       (μ : Measure Ω) [IsProbabilityMeasure μ] (f : Ω → ℝ) (hf : Measurable f)
       (hfi : Integrable f μ) (m B r : ℝ) (hr : 0 ≤ r)
       (hB : ∀ ω, |f ω - m| ≤ B) :
       |(∫ ω, f ω ∂μ) - m| ≤ r + B * μ.real {ω | r ≤ |f ω - m|} := by
   …

3. theorem OAI.InvariantIsing.tendsto_mean_sub_median_zero line 73

   Source documentation

   Uniformly bounded observables with exponential tails about their medians have means and medians asymptotically equal.

   theorem tendsto_mean_sub_median_zero {Ω : Type*} [MeasurableSpace Ω]
       (μ : Measure Ω) [IsProbabilityMeasure μ] (f : ℕ → Ω → ℝ) (hf : ∀ n, Measurable (f n))
       (m : ℕ → ℝ) (B : ℝ) (hB : 0 ≤ B) (hbound : ∀ n ω, |f n ω| ≤ B)
       (hl : ∀ n, (1 / 2 : ℝ) ≤ μ.real {ω | f n ω ≤ m n})
       (hu : ∀ n, (1 / 2 : ℝ) ≤ μ.real {ω | m n ≤ f n ω})
       (htail : ∀ r : ℝ, 0 < r → ∃ C a : ℝ, 0 ≤ C ∧ 0 < a ∧
         ∀ n, μ.real {ω | r ≤ |f n ω - m n|} ≤ C * Real.exp (-a * (n : ℝ))) :
       Tendsto (fun n => (∫ ω, f n ω ∂μ) - m n) atTop (𝓝 0) := by
   …