OAI/Combinatorics/ContingencyTables/Counting/CompanionMetropolisWordSemantics.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The flat physical transition has the proved phase-step law

  1. def OAI.ContingencyTables.CompanionMetropolisWordProgram.packed line 20
  2. lemma OAI.ContingencyTables.CompanionMetropolisWordProgram.fields_ofFn line 23
  3. lemma OAI.ContingencyTables.CompanionMetropolisWordProgram.proposalWidth_code line 44
  4. lemma OAI.ContingencyTables.CompanionMetropolisWordProgram.queryWidth_config line 53
  5. lemma OAI.ContingencyTables.CompanionMetropolisWordProgram.output_ofFn line 60
  6. theorem OAI.ContingencyTables.CompanionMetropolisWordProgram.sameLaw_flat line 87

    Source documentation

    The actual polynomial flat-step implementation has exactly the reference kernel used by the trajectory and return estimates.

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