FiniteLawDecidableEq.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ContingencyTables.FirstSuccess.mapLaw_decidableEq_irrel line 18
Source documentation
The output equality decision only computes the same finite fibres; it does not change the mapped probability law. Keeping the decisions explicit avoids reducing a large concrete state type to match instances.
```
theorem mapLaw_decidableEq_irrel (d e : DecidableEq Y)
    (p : RationalLaw X) (f : X → Y) :
    @mapLaw X Y _ _ d p f=@mapLaw X Y _ _ e p f := by
…
```
Mentions: OAI.ContingencyTables.FirstSuccess.mapLaw
theorem OAI.ContingencyTables.FirstSuccess.mapLaw_mass_decidableEq_irrel line 24
theorem OAI.ContingencyTables.FairBits.subsetBitDraw_mass_decidableEq line 42
Source documentation
The actual subset bit draw has its exact dyadic mass with any chosen output equality decision. The draw and its embedding are unchanged.
```
theorem subsetBitDraw_mass_decidableEq (d : DecidableEq (Option X))
    (p : X → Prop) (k : ℕ) (h : Fintype.card {x // p x} ≤ 2^k) (x : X) :
    (@mapLaw (Fin k → Bool) (Option X) _ _ d
      (uniformLaw (α := Fin k → Bool)) (subsetBitDraw p k h)).mass (some x)=
…
```
Mentions: OAI.ContingencyTables.FairBits.subsetBitDraw