RoutedFirstDefault.lean`

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem310.FiniteTableModel.outcomeLaw_routed_no_default line 12
Source documentation
Exact no-default probability for the actual depth-d spatial router under the finite selector/terminal outcome law. All randomness is instantiated.
```
theorem outcomeLaw_routed_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)
      {ω : SelectorTable bS × TerminalTable bT |
        Fin.last M ∉ RoutingPath.routeFrom
          (fun P y => OrderedRouting.chooseChild (fun i => selectorValue bS ω.1 P i y))
          d [] x} = (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.FiniteTableModel.SelectorTable, OAI.Problem310.FiniteTableModel.TerminalTable, OAI.Problem310.RoutingPath.routeFrom, OAI.Problem310.OrderedRouting.chooseChild, OAI.Problem310.FiniteTableModel.selectorValue
theorem OAI.Problem310.FiniteTableModel.outcomeLaw_no_default_steps line 36
Source documentation
The same exact law stated with the step-by-step absence of a default. This form pairs directly with first-default decomposition of the exposure atoms.
```
theorem outcomeLaw_no_default_steps {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)
      {ω : SelectorTable bS × TerminalTable bT |
        ∀ k < d,
          OrderedRouting.chooseChild (fun i => selectorValue bS ω.1
            (RoutingPath.routeFrom
              (fun P y => OrderedRouting.chooseChild (fun i => selectorValue bS ω.1 P i y))
              k [] x) i x) ≠ Fin.last M} =
      (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.FiniteTableModel.SelectorTable, OAI.Problem310.FiniteTableModel.TerminalTable, OAI.Problem310.OrderedRouting.chooseChild, OAI.Problem310.FiniteTableModel.selectorValue, OAI.Problem310.RoutingPath.routeFrom