OAI/Combinatorics/ContingencyTables/Dense/DenseNormalizeSemantics.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Correctness of computed maximal-margin normalization

  1. lemma OAI.ContingencyTables.DensePrograms.marginCode_ofFn line 14
  2. def OAI.ContingencyTables.DensePrograms.marginPosition line 19
  3. def OAI.ContingencyTables.DensePrograms.indexPermutation line 22
  4. def OAI.ContingencyTables.DensePrograms.normalizedMargin line 25
  5. lemma OAI.ContingencyTables.DensePrograms.finSuccEquiv_symm_none line 28
  6. lemma OAI.ContingencyTables.DensePrograms.normalizedMargin_max line 32
  7. lemma OAI.ContingencyTables.DensePrograms.normalizedMargin_lower line 38
  8. lemma OAI.ContingencyTables.DensePrograms.normalizedMargin_total line 41
  9. lemma OAI.ContingencyTables.DensePrograms.marginPosition_val line 44
  10. lemma OAI.ContingencyTables.DensePrograms.marginCode_swap line 49
  11. lemma OAI.ContingencyTables.DensePrograms.indexPermutation_finSucc line 56
  12. lemma OAI.ContingencyTables.DensePrograms.indexPermutation_symm_finSucc line 61
  13. lemma OAI.ContingencyTables.DensePrograms.tableOutput_swap line 66
  14. lemma OAI.ContingencyTables.DensePrograms.tableOutput_inverse_swap line 78
  15. lemma OAI.ContingencyTables.DensePrograms.drawIndices_code line 91
  16. lemma OAI.ContingencyTables.DensePrograms.permuteDrawData_code line 96
  17. def OAI.ContingencyTables.DensePrograms.normalizedDrawBits line 106
  18. def OAI.ContingencyTables.DensePrograms.normalizedBooleanDraw line 109
  19. theorem OAI.ContingencyTables.DensePrograms.normalizedDenseCode_eq line 122

    Source documentation

    The computed maximum and both physical permutations agree with the finite table-valued experiment on every Boolean input.

    theorem normalizedDenseCode_eq {m n d : ℕ} (R : Option (Fin m) → ℕ) (P : Option (Fin n) → ℕ)
    (hd : 14≤d) (hR : ∀ i,d^12≤R i) (hP : ∀ j,d^12≤P j)
    (htotal : ∑ i,R i=∑ j,P j) (h : ℕ)
    (a : Grid (I := Fin (m*n)) (4*d^8)) (fallback : Table R P)
…

    Mentions: OAI.ContingencyTables.Table

  20. theorem OAI.ContingencyTables.DensePrograms.normalizedBooleanDraw_variation line 144

    Source documentation

    The computed choice of maximal rows and columns retains the dense sampler's uniform-error guarantee for arbitrary original row order.

    theorem normalizedBooleanDraw_variation {m n d : ℕ}
    (R : Option (Fin m) → ℕ) (P : Option (Fin n) → ℕ)
    (hd : 14≤d) (hR : ∀ i,d^12≤R i) (hP : ∀ j,d^12≤P j)
    (hdimR : Fintype.card (Option (Fin m))≤d) (hdimP : Fintype.card (Option (Fin n))≤d)
    (hfree : Fintype.card (Fin m×Fin n)≤d) (htotal : ∑ i,R i=∑ j,P j)
    (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (m*n))
    (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin (m*n)) (4*d^8)))
…

    Mentions: OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.FiniteCheeger

  21. theorem OAI.ContingencyTables.DensePrograms.normalizedDrawBits_polynomial line 180