OAI/MeasureTheory/DyadicAvoidance/ConcreteWindowAtom.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem310.ConcreteWindowAtom.localMiss line 21

   Source documentation

   The concrete center atom together with all child-window trial misses.

   def localMiss (W : WindowData (M + 1) d g r₀) (U : Node M d)
       (x t : ℝ) (ξ : Node M d × Fin M → Bool) :
       Set (SelectorTable (selectorEndpoints W) × TerminalTable (terminalEndpoints W)) :=
   …

   Mentions: OAI.Problem310.WindowData

2. lemma OAI.Problem310.ConcreteWindowAtom.centerAtom_mass line 28
3. theorem OAI.Problem310.ConcreteWindowAtom.localMiss_mass line 49

   Source documentation

   Exact mass of the actual local Boolean failure event, with no remaining address-injectivity or leaf-prefix obligations.

   theorem localMiss_mass (W : WindowData (M + 1) d g r₀) (U : Node M d)
       (x t : ℝ) (ht : t ∈ Set.Icc (1 : ℝ) 2)
       (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1)
       (ξ : Node M d × Fin M → Bool) :
       ConcreteLabels.outcomeLaw (SelectorAddress (selectorEndpoints W))
         (TerminalAddress (terminalEndpoints W)) p hp0 hp1 (localMiss W U x t ξ) =
       (ENNReal.ofReal (1 - p / 2)) ^ (M * W.r (d - U.val.length)) *
         ConcreteLabels.outcomeLaw (SelectorAddress (selectorEndpoints W))
           (TerminalAddress (terminalEndpoints W)) p hp0 hp1
           (centerAtom (selectorEndpoints W) (terminalEndpoints W) x ξ) := by
   …

   Mentions: OAI.Problem310.WindowData, OAI.Problem310.ConcreteLabels.outcomeLaw, OAI.Problem310.ConcreteWindowAtom.localMiss

4. theorem OAI.Problem310.ConcreteWindowAtom.raw_failure_on_good_atom line 82

   Source documentation

   The final good-atom bound for the actual window router. The only numerical input is precisely the uniform entropy budget returned by RoutingBudget.

   theorem raw_failure_on_good_atom
       (W : WindowData (M + 1) d g r₀) (hM : 1 ≤ M)
       (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1)
       (hbudget : ∀ r : ℕ, r₀ ≤ r → ∀ N : ℕ,
         N ≤ 1 + M * r * 2 ^ (2 * r + 2) →
         (N : ENNReal) * (ENNReal.ofReal (1 - p / 2)) ^ (M * r) ≤ ENNReal.ofReal p)
       (x : ℝ) (hstable : StableAt W x)
       (ξ : Node M d × Fin M → Bool) (hgood : GoodExposure (selectorEndpoints W) x ξ) :
       ConcreteLabels.outcomeLaw (SelectorAddress (selectorEndpoints W))
         (TerminalAddress (terminalEndpoints W)) p hp0 hp1
         ({ω | x ∈ Auxiliary.exceptionalCenters
           (routedSet (selectorEndpoints W) (terminalEndpoints W) ω)
   …

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