OAI/Combinatorics/ContingencyTables/Counting/CompanionMetropolisLaw.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual computed proposal and two oracle calls have the phase law

  1. abbrev OAI.ContingencyTables.CompanionMetropolisProgram.Fields line 21
  2. def OAI.ContingencyTables.CompanionMetropolisProgram.programInput line 25
  3. def OAI.ContingencyTables.CompanionMetropolisProgram.codeAccept line 32
  4. lemma OAI.ContingencyTables.CompanionMetropolisProgram.output_programInput line 41
  5. theorem OAI.ContingencyTables.CompanionMetropolisProgram.sameLaw_fields line 67

    Source documentation

    Every computed step has the complete reference phase-step law. The proposal and both query outcomes are transported, including failures.

    theorem sameLaw_fields (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