FiniteWordDependent.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.ContingencyTables.FirstSuccess.mapLaw_product_bind line 17
theorem OAI.ContingencyTables.FirstSuccess.mapLaw_dependent_product line 28
Source documentation
Fresh terminal bits are independent of the bits used to obtain the state, even though the completion space depends on that state.
```
theorem mapLaw_dependent_product {Y : X → Type*} [∀ x,Fintype (Y x)]
    [DecidableEq X] [∀ x,DecidableEq (Y x)]
    (p : RationalLaw A) (q : RationalLaw B) (f : A → X) (g : (x : X) → B → Y x) :
    mapLaw (productLaw p q) (fun ab => (⟨f ab.1,g (f ab.1) ab.2⟩ : Sigma Y))=
      dependentJointLaw (mapLaw p f) (fun x => mapLaw q (g x)) := by
…
```
Mentions: OAI.ContingencyTables.FirstSuccess.mapLaw, OAI.ContingencyTables.FirstSuccess.productLaw, OAI.ContingencyTables.FirstSuccess.dependentJointLaw
theorem OAI.ContingencyTables.FirstSuccess.mapLaw_product_finish line 49
Source documentation
First drawing a state and then applying a fresh common word to that state gives the corresponding composition of output laws.
```
theorem mapLaw_product_finish [DecidableEq X] [DecidableEq Z]
    (p : RationalLaw A) (q : RationalLaw B) (f : A → X) (finish : X → B → Z) :
    mapLaw (productLaw p q) (fun ab => finish (f ab.1) ab.2)=
      bindLaw (mapLaw p f) (fun x => mapLaw q (finish x)) := by
…
```
Mentions: OAI.ContingencyTables.FirstSuccess.mapLaw, OAI.ContingencyTables.FirstSuccess.productLaw, OAI.ContingencyTables.FirstSuccess.bindLaw