CenterNoDefaultMass.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem310.CenterFailureBound.noDefaultEvent_eq_spatial line 15

Source documentation

The atom-averaging bad event and the spatial router's no-default event are identical, including their terminal-table coordinate.

theorem noDefaultEvent_eq_spatial {M d : ℕ}
    (bS : Node M d → Fin M → ℕ) (bT : Leaf M d → ℕ) (x : ℝ) :
    noDefaultEvent bS bT x =
      {ω : SelectorTable bS × TerminalTable bT | ∀ k < d,
        selectorChoice bS ω.1
          (RoutingPath.routeFrom (selectorChoice bS ω.1) k [] x) x ≠ Fin.last M} := by
…

Mentions: OAI.Problem310.CenterFailureBound.noDefaultEvent, OAI.Problem310.RoutingPath.routeFrom

theorem OAI.Problem310.CenterFailureBound.outcomeLaw_noDefaultEvent line 28

Source documentation

Exact mass of the bad event in the concrete center-atom averaging theorem. No probability or independence premises remain.

theorem outcomeLaw_noDefaultEvent {M d : ℕ}
    (bS : Node M d → Fin M → ℕ) (bT : Leaf M d → ℕ)
    (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (x : ℝ) :
    ConcreteLabels.outcomeLaw (SelectorAddress bS) (TerminalAddress bT) p hp0 hp1
      (noDefaultEvent bS bT x) = (1 - ((2 : ENNReal)⁻¹) ^ M) ^ d := by
…

Mentions: OAI.Problem310.ConcreteLabels.outcomeLaw, OAI.Problem310.CenterFailureBound.noDefaultEvent

theorem OAI.Problem310.CenterFailureBound.raw_failure_le_of_outcome_center_atoms line 38

Source documentation

Concrete raw-failure assembly: only the numeric depth budget and the per-good-atom local-trial estimate are required.

theorem raw_failure_le_of_outcome_center_atoms {M d : ℕ}
    (bS : Node M d → Fin M → ℕ) (bT : Leaf M d → ℕ)
    (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1)
    (B : SelectorTable bS × TerminalTable bT → Set ℝ) (N : Set ℕ) (x : ℝ)
    (htail : (1 - ((2 : ENNReal)⁻¹) ^ M) ^ d ≤ ENNReal.ofReal p)
    (hatom : ∀ ξ : Node M d × Fin M → Bool, GoodExposure bS x ξ →
      ConcreteLabels.outcomeLaw (SelectorAddress bS) (TerminalAddress bT) p hp0 hp1
        ({ω | x ∈ Auxiliary.exceptionalCenters (B ω) N (fun n => (2 : ℝ)⁻¹ ^ n)} ∩
          centerAtom bS bT x ξ) ≤
        ENNReal.ofReal p *
          ConcreteLabels.outcomeLaw (SelectorAddress bS) (TerminalAddress bT) p hp0 hp1
            (centerAtom bS bT x ξ)) :
…

Mentions: OAI.Problem310.ConcreteLabels.outcomeLaw, OAI.Problem310.Auxiliary.exceptionalCenters, OAI.Problem310.CenterFailureBound.centerAtom