OAI/Combinatorics/ContingencyTables/Counting/CompanionBoundedWalkSemantics.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.CompanionBoundedWalkProgram.codeStep line 18
2. lemma OAI.ContingencyTables.CompanionBoundedWalkProgram.recordFold_eq line 21
3. lemma OAI.ContingencyTables.CompanionBoundedWalkProgram.history_eq_trace line 33
4. lemma OAI.ContingencyTables.CompanionBoundedWalkProgram.cap_encode line 42
5. theorem OAI.ContingencyTables.CompanionBoundedWalkProgram.codeStep_sameLaw line 54

   Source documentation

   The all-input clipping has no effect on a valid encoded transition; in particular its full row law agrees with the reference phase step.

   theorem codeStep_sameLaw (A : Instance (Fin m) (Fin n)) (C K j k : ℕ)
       (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

6. theorem OAI.ContingencyTables.CompanionBoundedWalkProgram.history_sameLaw line 80

   Source documentation

   The physical list recorder and the full reference state history have the same law, before any first-return scan or phase statistic is applied.

   theorem history_sameLaw (A : Instance (Fin m) (Fin n)) (C K j k : ℕ)
       (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