OAI/Probability/GammaPassage/BKLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.BK.ae_eventual_measure_le line 12

   Source documentation

   Generic outer-measure limit with AE support capture. No measurability of an uncountable witness-label union or monotonicity of Rounded_t is assumed.

   lemma ae_eventual_measure_le (P : Measure Ω) (A : Set Ω) (R : ℕ → Set Ω)
       (C : ℝ≥0∞) (hcap : ∀ᵐ ω ∂P, ω ∈ A → ∀ᶠ t in atTop, ω ∈ R t)
       (hbound : ∀ t, P (R t) ≤ C) : P A ≤ C := by
   …