OAI/MeasureTheory/DyadicAvoidance/Construction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem310.Construction.periodic_hitting_of_window_failure line 18

   Source documentation

   The analytic conclusion for the actual finite window-table model. All regularity and first-moment obligations are discharged here; only the geometric good-center set and its raw failure estimate remain as inputs.

   theorem periodic_hitting_of_window_failure
       {M d g r₀ : ℕ} (W : WindowData (M + 1) d g r₀)
       (p : ℝ) (hp : 0 < p) (hp1 : p < 1)
       (G : Set ℝ) (hG : MeasurableSet G)
       (hbad : volume (Gᶜ ∩ Icc (0 : ℝ) 1) ≤ ENNReal.ofReal p)
       (hgood : ∀ x ∈ G,
         ConcreteLabels.outcomeLaw (SelectorAddress (selectorEndpoints W))
           (TerminalAddress (terminalEndpoints W)) p hp.le hp1.le
           {ω | x ∈ Auxiliary.exceptionalCenters
             (RoutedSetDensity.routedSet (selectorEndpoints W) (terminalEndpoints W) ω)
             (Ici 1) (fun n => (2 : ℝ)⁻¹ ^ n)} ≤ ENNReal.ofReal (2 * p)) :
       ∃ H : Set ℝ, IsOpen H ∧
   …

   Mentions: OAI.Problem310.WindowData, OAI.Problem310.ConcreteLabels.outcomeLaw, OAI.Problem310.Auxiliary.exceptionalCenters, OAI.Problem310.RoutedSetDensity.routedSet