CenterFailureBound.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem310.CenterFailureBound.centerAtom line 16

Source documentation

The actual full-outcome fiber of the center selector exposure.

def centerAtom {M d : ℕ} (bS : Node M d → Fin M → ℕ) (bT : Leaf M d → ℕ)
    (x : ℝ) (ξ : Node M d × Fin M → Bool) :
    Set (SelectorTable bS × TerminalTable bT) :=
…

def OAI.Problem310.CenterFailureBound.noDefaultEvent line 23
Source documentation
No default occurs on the actual center path. Terminal coordinates do not enter this event, but are retained in the probability space.
```
def noDefaultEvent {M d : ℕ} (bS : Node M d → Fin M → ℕ) (bT : Leaf M d → ℕ)
    (x : ℝ) : Set (SelectorTable bS × TerminalTable bT) :=
…
```

theorem OAI.Problem310.CenterFailureBound.raw_failure_le_of_center_atoms line 31

Source documentation

Concrete assembly of the atom bounds into the raw 2p failure estimate. All exposure fibers, their measurability, and their total mass are discharged here for the canonical finite selector/terminal table model.

theorem raw_failure_le_of_center_atoms {M d : ℕ}
    (bS : Node M d → Fin M → ℕ) (bT : Leaf M d → ℕ)
    (μ : Measure (SelectorTable bS × TerminalTable bT)) [IsProbabilityMeasure μ]
    (p : ℝ) (hp : 0 ≤ p) (B : SelectorTable bS × TerminalTable bT → Set ℝ)
    (N : Set ℕ) (x : ℝ)
    (hbad : μ (noDefaultEvent bS bT x) ≤ ENNReal.ofReal p)
    (hatom : ∀ ξ : Node M d × Fin M → Bool, GoodExposure bS x ξ →
      μ ({ω | x ∈ Auxiliary.exceptionalCenters (B ω) N (fun n => (2 : ℝ)⁻¹ ^ n)} ∩
          centerAtom bS bT x ξ) ≤
        ENNReal.ofReal p * μ (centerAtom bS bT x ξ)) :
    μ {ω | x ∈ Auxiliary.exceptionalCenters (B ω) N (fun n => (2 : ℝ)⁻¹ ^ n)} ≤
      ENNReal.ofReal (2 * p) := by
…

Mentions: OAI.Problem310.CenterFailureBound.noDefaultEvent, OAI.Problem310.Auxiliary.exceptionalCenters, OAI.Problem310.CenterFailureBound.centerAtom