OAI/Combinatorics/ContingencyTables/Counting/CompanionComputedInitial.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Initialization from the computed small-cell catalog

The proof-level equivalence follows the actual catalog program. It is used only to identify the output of the binary list initializer with a paired transversal and to transfer its distributional error bound.

  1. abbrev OAI.ContingencyTables.CompanionComputedInitial.ProgramInput line 21
  2. def OAI.ContingencyTables.CompanionComputedInitial.initialProgram line 23
  3. def OAI.ContingencyTables.CompanionComputedInitial.initialProgramRealizer line 26
  4. theorem OAI.ContingencyTables.CompanionComputedInitial.polynomial_initialProgram line 31
  5. def OAI.ContingencyTables.CompanionComputedInitial.cellOrder line 41
  6. def OAI.ContingencyTables.CompanionComputedInitial.capacities line 44
  7. def OAI.ContingencyTables.CompanionComputedInitial.wordLength line 47
  8. def OAI.ContingencyTables.CompanionComputedInitial.initialDraw line 49
  9. def OAI.ContingencyTables.CompanionComputedInitial.copyOrder line 54
  10. def OAI.ContingencyTables.CompanionComputedInitial.pairOrder line 56
  11. def OAI.ContingencyTables.CompanionComputedInitial.coordinateOrder line 59
  12. lemma OAI.ContingencyTables.CompanionComputedInitial.encodeSet_reindex line 62
  13. lemma OAI.ContingencyTables.CompanionComputedInitial.draw_preimage line 67
  14. theorem OAI.ContingencyTables.CompanionComputedInitial.initialProgram_eq line 87

    Source documentation

    The complete program computes the semantic initializer with the coordinate order recovered from the program's own catalog.

    theorem initialProgram_eq (B : ℕ) (hB : 0<B) (bits : Fin (wordLength A B) → Bool) :
    initialProgram ((CompanionCellCatalog.input A,B),List.ofFn bits)=
      encodeSet (coordinateOrder A) (initialDraw A B bits).val.val := by
…

    Mentions: OAI.ContingencyTables.CompanionComputedInitial.wordLength, OAI.ContingencyTables.CompanionComputedInitial.initialProgram, OAI.ContingencyTables.CompanionCellCatalog.input, OAI.ContingencyTables.CompanionComputedInitial.coordinateOrder, OAI.ContingencyTables.CompanionComputedInitial.initialDraw

  15. lemma OAI.ContingencyTables.CompanionComputedInitial.catalog_count_le line 95
  16. theorem OAI.ContingencyTables.CompanionComputedInitial.wordLength_bound line 99
  17. theorem OAI.ContingencyTables.CompanionComputedInitial.initialDraw_error line 107

    Source documentation

    The computed-order initializer has the same μ₀ reference law and error guarantee as the abstract-order initializer.

    theorem initialDraw_error (B : ℕ) :
    variation (mapLaw (uniformLaw (α := Fin (wordLength A B) → Bool)) (initialDraw A B))
…

    Mentions: OAI.ContingencyTables.CompanionComputedInitial.wordLength, OAI.ContingencyTables.CompanionComputedInitial.initialDraw

  18. theorem OAI.ContingencyTables.CompanionComputedInitial.initialDraw_precision line 123