OAI/MeasureTheory/DyadicAvoidance/RawRepair.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem310.Auxiliary.periodic_hitting_of_raw_construction line 18

   Source documentation

   Complete analytic passage from a finite random periodic grid construction to an open periodic hitting set. The hypotheses are precisely the density, stability, and raw-failure estimates supplied by the combinatorial construction.

   theorem periodic_hitting_of_raw_construction
       {Ω : Type u_Ω} [Fintype Ω] [MeasurableSpace Ω] [MeasurableSingletonClass Ω]
       (μ : Measure Ω) [IsProbabilityMeasure μ]
       (p : ℝ) (hp : 0 < p) (B : Ω → Set ℝ)
       (hBp : ∀ ω x, x + 1 ∈ B ω ↔ x ∈ B ω)
       (N : Set ℕ) (hN : ∀ n ∈ N, 1 ≤ n)
       (G : Set ℝ) (hG : MeasurableSet G)
       (hbad : volume (Gᶜ ∩ Icc (0 : ℝ) 1) ≤ ENNReal.ofReal p)
       (hBmean : (∫⁻ ω, volume (B ω ∩ Icc (0 : ℝ) 1) ∂μ) ≤ ENNReal.ofReal p)
       (hgood : ∀ x ∈ G,
         μ {ω | x ∈ exceptionalCenters (B ω) N (fun n => (2 : ℝ)⁻¹ ^ n)}
           ≤ ENNReal.ofReal (2 * p)) :
   …

   Mentions: OAI.Problem310.Auxiliary.exceptionalCenters