ExactMatrixTableLaw.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact weighted matrix selection realizes a table law

lemma OAI.ContingencyTables.ExactMatrixTrial.normalized_counts line 17
lemma OAI.ContingencyTables.ExactMatrixTrial.count_weight_pos line 23

lemma OAI.ContingencyTables.ExactMatrixTrial.table_normalized_event line 30

Source documentation

An integer law's full original-box vector pushes back to precisely that table law under the executed matrix lookup.

lemma table_normalized_event {m n Q : ℕ} (r : Fin m → ℕ) (c : Fin n → ℕ)
    (p : IntegerLaw (Table r c) Q) (hQ : 0<Q) (fallback X : Table r c) :
    (∑ i : Index m n (∑ j,r j),
      if lookup ((originalCandidates (List.ofFn r,List.ofFn c),matrixCode fallback.val),i.val)=
          matrixCode X.val then normalized (p.push (index r c le_rfl)).count i else 0)=
      (p.toRational hQ).mass X := by
…

Mentions: OAI.ContingencyTables.IntegerLaw, OAI.ContingencyTables.Table, OAI.ContingencyTables.ExactMatrixTrial.lookup

theorem OAI.ContingencyTables.ExactMatrixTrial.table_prefix_limit line 60
Source documentation
The finite prefixes of the actual exact matrix loop converge to the input table law.
```
theorem table_prefix_limit {m n Q : ℕ} (r : Fin m → ℕ) (c : Fin n → ℕ)
    (p : IntegerLaw (Table r c) Q) (hQ : 0<Q) (fallback X : Table r c) :
    Filter.Tendsto (fun N =>
      ((OnlineIntegerRetry.prefixExperiment (f := trial)
…
```
Mentions: OAI.ContingencyTables.IntegerLaw, OAI.ContingencyTables.Table, OAI.ContingencyTables.OnlineIntegerRetry.prefixExperiment, OAI.ContingencyTables.ExactMatrixTrial.trial