CenterFirstDefault.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem310.FiniteTableModel.centerTableAddress line 16
Source documentation
Center-table coordinate in the bounded-address convention used by the first-default probability theorem.
```
def centerTableAddress {M d : ℕ} (b : Node M d → Fin M → ℕ) (x : ℝ)
    (a : FirstDefault.BoundedAddress M d) : SelectorAddress b :=
…
```
Mentions: OAI.Problem310.FiniteTableModel.Node, OAI.Problem310.FirstDefault.BoundedAddress, OAI.Problem310.FiniteTableModel.SelectorAddress
lemma OAI.Problem310.FiniteTableModel.centerTableAddress_injective line 20
theorem OAI.Problem310.FiniteTableModel.measure_center_no_default line 31
Source documentation
Exact no-default probability for the canonical spatial selector tables, at every real center and every choice of deterministic grid resolutions.
```
theorem measure_center_no_default {M d : ℕ} (b : Node M d → Fin M → ℕ)
    (ν : Measure Bool) [IsProbabilityMeasure ν]
    (hfair : ∀ bit, ν {bit} = (2 : ENNReal)⁻¹) (x : ℝ) :
    (Measure.pi (fun _ : SelectorAddress b => ν))
      (⋃ f : FirstDefault.Path M d, {ω | ∀ i : FirstDefault.Tests f,
        selectorValue b ω (FirstDefault.address f i).1 (FirstDefault.address f i).2 x =
          FirstDefault.requiredBit f i}) =
      (1 - ((2 : ENNReal)⁻¹) ^ M) ^ d := by
…
```
Mentions: OAI.Problem310.FiniteTableModel.Node, OAI.Problem310.FiniteTableModel.SelectorAddress, OAI.Problem310.FirstDefault.Path, OAI.Problem310.FirstDefault.Tests, OAI.Problem310.FiniteTableModel.selectorValue, OAI.Problem310.FirstDefault.address, OAI.Problem310.FirstDefault.requiredBit

theorem OAI.Problem310.FiniteTableModel.measure_center_no_default_prod line 46

Source documentation

Adding the independent terminal tables does not change the center-path survival probability. This is the full outcome-space form used by repair.

theorem measure_center_no_default_prod {M d : ℕ}
    {T : Type u_T} [MeasurableSpace T] (τ : Measure T) [IsProbabilityMeasure τ]
    (b : Node M d → Fin M → ℕ)
    (ν : Measure Bool) [IsProbabilityMeasure ν]
    (hfair : ∀ bit, ν {bit} = (2 : ENNReal)⁻¹) (x : ℝ) :
    ((Measure.pi (fun _ : SelectorAddress b => ν)).prod τ)
      (⋃ f : FirstDefault.Path M d, {ω : SelectorTable b × T |
        ∀ i : FirstDefault.Tests f,
        selectorValue b ω.1 (FirstDefault.address f i).1 (FirstDefault.address f i).2 x =
          FirstDefault.requiredBit f i}) =
      (1 - ((2 : ENNReal)⁻¹) ^ M) ^ d := by
…

Mentions: OAI.Problem310.FiniteTableModel.Node, OAI.Problem310.FiniteTableModel.SelectorAddress, OAI.Problem310.FirstDefault.Path, OAI.Problem310.FiniteTableModel.SelectorTable, OAI.Problem310.FirstDefault.Tests, OAI.Problem310.FiniteTableModel.selectorValue, OAI.Problem310.FirstDefault.address, OAI.Problem310.FirstDefault.requiredBit

theorem OAI.Problem310.FiniteTableModel.outcomeLaw_center_no_default line 73
Source documentation
The survival estimate with all probability measures instantiated, including the Bernoulli terminal labels in the canonical complete outcome space.
```
theorem outcomeLaw_center_no_default {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)
      (⋃ f : FirstDefault.Path M d, {ω : SelectorTable bS × TerminalTable bT |
        ∀ i : FirstDefault.Tests f,
        selectorValue bS ω.1 (FirstDefault.address f i).1 (FirstDefault.address f i).2 x =
          FirstDefault.requiredBit f i}) =
      (1 - ((2 : ENNReal)⁻¹) ^ M) ^ d := by
…
```
Mentions: OAI.Problem310.FiniteTableModel.Node, OAI.Problem310.FiniteTableModel.Leaf, OAI.Problem310.ConcreteLabels.outcomeLaw, OAI.Problem310.FiniteTableModel.SelectorAddress, OAI.Problem310.FiniteTableModel.TerminalAddress, OAI.Problem310.FirstDefault.Path, OAI.Problem310.FiniteTableModel.SelectorTable, OAI.Problem310.FiniteTableModel.TerminalTable, OAI.Problem310.FirstDefault.Tests, OAI.Problem310.FiniteTableModel.selectorValue, OAI.Problem310.FirstDefault.address, OAI.Problem310.FirstDefault.requiredBit