OAI/MeasureTheory/DyadicAvoidance/ExpectedRepair.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem310.Auxiliary.periodic_hitting_of_expected_exceptional line 15

   Source documentation

   First-moment selection followed by deterministic open-neighborhood repair.

   theorem periodic_hitting_of_expected_exceptional
       {Ω : Type u_Ω} [Fintype Ω] [MeasurableSpace Ω] [MeasurableSingletonClass Ω]
       (μ : Measure Ω) [IsProbabilityMeasure μ]
       (p : ℝ) (hp : 0 < p) (B : Ω → Set ℝ)
       (hBo : ∀ ω, IsOpen (B ω))
       (hBp : ∀ ω x, x + 1 ∈ B ω ↔ x ∈ B ω)
       (N : Set ℕ) (hN : ∀ n ∈ N, 1 ≤ n)
       (hBmean : (∫⁻ ω, volume (B ω ∩ Icc (0 : ℝ) 1) ∂μ) ≤ ENNReal.ofReal (2 * p))
       (hRmean : (∫⁻ ω, volume
         (exceptionalCenters (B ω) N (fun n => (2 : ℝ)⁻¹ ^ n) ∩ Icc (0 : ℝ) 1) ∂μ)
           ≤ ENNReal.ofReal (3 * p)) :
       ∃ H : Set ℝ, IsOpen H ∧
   …

   Mentions: OAI.Problem310.Auxiliary.exceptionalCenters

2. theorem OAI.Problem310.Auxiliary.periodic_hitting_of_pointwise_failure_bound line 48

   Source documentation

   Full analytic repair interface from pointwise failure probabilities on stable centers.

   theorem periodic_hitting_of_pointwise_failure_bound
       {Ω : Type u_Ω} [Fintype Ω] [MeasurableSpace Ω] [MeasurableSingletonClass Ω]
       (μ : Measure Ω) [IsProbabilityMeasure μ]
       (p : ℝ) (hp : 0 < p) (B : Ω → Set ℝ)
       (hBo : ∀ ω, IsOpen (B ω))
       (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 (2 * p))
       (hgood : ∀ x ∈ G,
         μ {ω | x ∈ exceptionalCenters (B ω) N (fun n => (2 : ℝ)⁻¹ ^ n)}
   …

   Mentions: OAI.Problem310.Auxiliary.exceptionalCenters