OAI/Combinatorics/ContingencyTables/Rooted/RootedCorrectionSampleLaw.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact law of the executed correction sample

The two coordinate enumerations need not agree on a fixed bit string. Their independent finite-word laws agree, which preserves every real observable of the computed rational sample.

  1. lemma OAI.ContingencyTables.RootedCorrectionSampleLaw.bind_equiv line 29
  2. abbrev OAI.ContingencyTables.RootedCorrectionSampleLaw.Words line 38
  3. def OAI.ContingencyTables.RootedCorrectionSampleLaw.integerDraw line 41
  4. lemma OAI.ContingencyTables.RootedCorrectionSampleLaw.integerDraw_law line 48
  5. def OAI.ContingencyTables.RootedCorrectionSampleLaw.sample line 76
  6. theorem OAI.ContingencyTables.RootedCorrectionSampleLaw.sample_average line 85

    Source documentation

    Equality for arbitrary observables is exact equality in distribution of the executed rational sample and the analysed correction sample.

    theorem sample_average (A : Instance (Fin m) (Fin n)) (C a K : ℕ)
    (hC : 0 < C) (haH : a ≤ rationalHeight A C) (hK : 1 ≤ K)
    (hW : 100*A.d*K ≤ A.W) (hKB : (K:ℝ) ≤ binWidth A C)
    (z : View A → ℕ) (hz : BalancedBox.InBox (bounds A) z) (sigma : ℚ)
    (v : Grid (I := Fin (RootedCatalogGrid.freeCount A)) K) (N h : ℕ) (g : ℚ → ℝ) :
…

    Mentions: OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.RootedCatalogGrid.freeCount

  7. theorem OAI.ContingencyTables.RootedCorrectionSampleLaw.program_sample line 105