OAI/Probability/InvariantIsing/Pressure/AlmostSure.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.ae_tendsto_zero_of_exponential_tail line 21

   Source documentation

   Summable exponential tails imply almost-sure convergence to zero. No independence between the random variables is required.

   lemma ae_tendsto_zero_of_exponential_tail {Ω : Type*} [MeasurableSpace Ω]
       (μ : Measure Ω) [IsProbabilityMeasure μ] (f : ℕ → Ω → ℝ)
       (htail : ∀ ε : ℝ, 0 < ε → ∃ C a : ℝ, 0 ≤ C ∧ 0 < a ∧
         ∀ n, μ.real {ω | ε ≤ |f n ω|} ≤ C * Real.exp (-a * (n : ℝ))) :
       ∀ᵐ ω ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 0) := by
   …

2. theorem OAI.InvariantIsing.ae_pressure_sub_median_tendsto_zero line 57

   Source documentation

   For an arbitrary joint realization of the Haar matrices, pressure is almost surely close to a deterministic sequence of medians.

   theorem ae_pressure_sub_median_tendsto_zero (hpub : HaarConcentrationInput)
       {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
       (U : (n : ℕ) → Ω → SpecialOrthogonal (n + 3))
       (hU : ∀ n, Measurable (U n))
       (hHaar : ∀ n, (P.map (U n)).IsMulLeftInvariant)
       (eig c : (n : ℕ) → Fin (n + 3) → ℝ)
       (K : ℝ) (hK : 0 < K) (heig : ∀ n i, |eig n i| ≤ K) :
       ∃ m : ℕ → ℝ, ∀ᵐ ω ∂P,
         Tendsto (fun n => rotatedPressure (eig n) (specialRotation (U n ω)) (c n) - m n)
           atTop (𝓝 0) := by
   …

   Mentions: OAI.InvariantIsing.HaarConcentrationInput, OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.specialRotation