OAI/Analysis/FiniteFactor/Sampling/SecondLevelAE.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.samplingTestedSecond_level_exists line 13

   Source documentation

   The interval endpoints depend only on the weight and level, and work simultaneously for every atomless law carried by [0,1).

   theorem samplingTestedSecond_level_exists (h α : ℝ) (G : Set ℝ) (a c s r : ℝ)
       (hh : 0 < h) (hh1 : h < 1) (hα : 0 < α)
       (hs : s ∈ Set.Ico (0 : ℝ) 1) (hr : 0 < r) :
       ∃ A B : Fin 2 → ℝ, ∀ (ν : Measure ℝ) [NullSingletonClass ν],
         (∀ᵐ t ∂ν, t ∈ Set.Ico (0 : ℝ) 1) →
         (fun t => if r ≤ samplingTestedSecondWeight h α (Set.Icc a c) G s t then (1 : ℝ) else 0) =ᵐ[ν]
           (fun t => ∑ j, samplingClosedIndicator (A j) (B j) t) := by
   …

   Mentions: OAI.FiniteFactor.samplingTestedSecondWeight, OAI.FiniteFactor.samplingClosedIndicator