OAI/Combinatorics/ContingencyTables/Counting/CompanionRepeatedReturnLaw.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The physical return loop has the actual repeated-return law

  1. def OAI.ContingencyTables.CompanionRepeatedReturnProgram.fixedData line 21
  2. def OAI.ContingencyTables.CompanionRepeatedReturnProgram.data line 28
  3. def OAI.ContingencyTables.CompanionRepeatedReturnProgram.codeStep line 35
  4. lemma OAI.ContingencyTables.CompanionRepeatedReturnProgram.walk_eq line 38
  5. lemma OAI.ContingencyTables.CompanionRepeatedReturnProgram.blockWidth_data line 45
  6. lemma OAI.ContingencyTables.CompanionRepeatedReturnProgram.words_data line 56
  7. theorem OAI.ContingencyTables.CompanionRepeatedReturnProgram.codeStep_sameLaw line 70
  8. lemma OAI.ContingencyTables.CompanionRepeatedReturnProgram.wordWalk_fold line 94
  9. theorem OAI.ContingencyTables.CompanionRepeatedReturnProgram.output_sameLaw line 105

    Source documentation

    Independent physical return blocks preserve the entire repeated return distribution, including fallback events in every block.

    theorem output_sameLaw (A : Instance (Fin m) (Fin n)) (C K j k cap t : ℕ)
    (hC : 0 < C) (hj : j ≤ rationalHeight A C) (hK : 1 ≤ K)
    (hW : 100*A.d*K ≤ A.W) (hB : (K:ℝ)=CompanionOracleDensity.binWidth A C)
    (xi : ℚ) (hxi : 0 < xi) (z : View A → ℕ)
    (v : Grid (I := Fin (RootedCatalogGrid.freeCount A)) K) (degree depth : List Bool)
…

    Mentions: OAI.ContingencyTables.CompanionOracleDensity.binWidth, OAI.ContingencyTables.RootedCatalogGrid.freeCount