OAI/Combinatorics/ContingencyTables/Machines/FractionMetropolisProgram.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContingencyTables.FractionMetropolisProgram.Input line 12
2. def OAI.ContingencyTables.FractionMetropolisProgram.ratio line 14
3. def OAI.ContingencyTables.FractionMetropolisProgram.ratioRealizer line 15
4. lemma OAI.ContingencyTables.FractionMetropolisProgram.polynomial_ratio line 18
5. def OAI.ContingencyTables.FractionMetropolisProgram.belowOne line 22
6. def OAI.ContingencyTables.FractionMetropolisProgram.belowOneRealizer line 23
7. lemma OAI.ContingencyTables.FractionMetropolisProgram.polynomial_belowOne line 26
8. def OAI.ContingencyTables.FractionMetropolisProgram.probability line 29
9. def OAI.ContingencyTables.FractionMetropolisProgram.probabilityRealizer line 30
10. lemma OAI.ContingencyTables.FractionMetropolisProgram.polynomial_probability line 31
11. def OAI.ContingencyTables.FractionMetropolisProgram.accept line 36
12. def OAI.ContingencyTables.FractionMetropolisProgram.acceptRealizer line 37
13. lemma OAI.ContingencyTables.FractionMetropolisProgram.polynomial_accept line 40
14. lemma OAI.ContingencyTables.FractionMetropolisProgram.probability_value line 44
15. lemma OAI.ContingencyTables.FractionMetropolisProgram.accept_ofFn line 60
16. theorem OAI.ContingencyTables.FractionMetropolisProgram.sameLaw_accept line 71

    Source documentation

    Independent exact observable laws suffice for the implemented coin; no finite type of rational weight values is required.

    theorem sameLaw_accept {X Y U V : Type*} [Fintype X] [Fintype Y] [Fintype U] [Fintype V]
        (current : X → TreeFraction.Fraction) (target : U → TreeFraction.Fraction)
        (f : Y → ℚ) (g : V → ℚ)
        (hf : SameLaw (fun x => TreeFraction.val (current x)) f)
        (hg : SameLaw (fun u => TreeFraction.val (target u)) g) (B : ℕ) :
        SameLaw (fun z : (X × U) × (Fin B → Bool) =>
          accept ((current z.1.1,target z.1.2),List.ofFn z.2))
          (fun z : (Y × V) × (Fin B → Bool) =>
            decide (FairBits.rationalThresholdAccept B (min 1 (g z.1.2/f z.1.1)) z.2)) := by
    …

    Mentions: OAI.ContingencyTables.FractionMetropolisProgram.accept, OAI.ContingencyTables.FairBits.rationalThresholdAccept