OAI/Combinatorics/ContingencyTables/Rooted/RootedReturnHistoryLaw.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The executed return scan has the reference capped-return law

  1. theorem OAI.ContingencyTables.RootedReturnHistoryLaw.trace_return_sameLaw line 22
  2. theorem OAI.ContingencyTables.RootedReturnHistoryLaw.flatReturn_sameLaw line 67

    Source documentation

    The physical flat-return program can replace the literal reference return in every subsequent restart or adaptive phase experiment.

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