CompletionKernelIdentification.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Identifying a complete transition law from its off-diagonal probabilities

theorem OAI.ContingencyTables.FirstSuccess.law_ext_except line 15
Source documentation
Normalization determines the remaining holding probability.
```
theorem law_ext_except (p q : RationalLaw X) (x : X)
    (h : ∀ y,y≠x → p.mass y=q.mass y) : p=q := by
…
```
lemma OAI.ContingencyTables.CompletionTranslation.completionStepLaw_proposal_at line 44
Source documentation
Only the proposal distribution at the current state is observed.
```
lemma completionStepLaw_proposal_at (p q : X → RationalLaw (Option X))
    (draw : (z : X) → RationalLaw (Table (R z) (P z))) (x : X) (h : p x=q x) :
    completionStepLaw R P p draw x=completionStepLaw R P q draw x := by
…
```
Mentions: OAI.ContingencyTables.Table, OAI.ContingencyTables.CompletionTranslation.completionStepLaw
theorem OAI.ContingencyTables.CompletionTranslation.uniformCompletionStep_eq line 52
Source documentation
This identifies the actual draw-and-test transition, including holds; no independent reversibility or stationarity assertion is imposed on it.
```
theorem uniformCompletionStep_eq (w : X → ℚ) (hw : ∀ y,0 ≤ w y)
    (htotal : ∑ y,w y ≤ 1) (x : X) (K : RationalLaw X)
    (hK : ∀ y,y≠x → K.mass y=w y*(acceptedCount R P x y:ℚ)/(blockCount R P x:ℚ)) :
    completionStepLaw R P (fun _ => proposalLaw w hw htotal)
      (fun z => uniformLaw (α := Table (R z) (P z))) x=K := by
…
```
Mentions: OAI.ContingencyTables.CompletionTranslation.acceptedCount, OAI.ContingencyTables.CompletionTranslation.blockCount, OAI.ContingencyTables.CompletionTranslation.completionStepLaw, OAI.ContingencyTables.CompletionTranslation.proposalLaw, OAI.ContingencyTables.Table