FiniteTableFirstDefault.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem310.FirstDefault.measure_no_default_finite_table line 15
Source documentation
Transport of the finite-depth survival law to actual finite spatial selector tables. The center lookup need only select distinct coordinates; unused table entries are integrated out automatically.
```
theorem measure_no_default_finite_table {M d : ℕ} {K : Type u_K} [Fintype K]
    (ν : Measure Bool) [IsProbabilityMeasure ν]
    (hfair : ∀ b, ν {b} = (2 : ENNReal)⁻¹)
    (center : BoundedAddress M d → K) (hinj : Function.Injective center) :
    (Measure.pi (fun _ : K => ν))
        (⋃ f : Path M d, {ω | ∀ i : Tests f,
          ω (center (boundedAddress f i)) = requiredBit f i}) =
      (1 - ((2 : ENNReal)⁻¹) ^ M) ^ d := by
…
```
Mentions: OAI.Problem310.FirstDefault.BoundedAddress, OAI.Problem310.FirstDefault.Path, OAI.Problem310.FirstDefault.Tests, OAI.Problem310.FirstDefault.boundedAddress, OAI.Problem310.FirstDefault.requiredBit