OAI/Combinatorics/ContingencyTables/Transport/RealKernelApproximation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Accumulating rational implementation errors against a real kernel

The exact companion weights may be real. The implemented probabilities are rational; comparison takes place after their canonical real cast.

  1. def OAI.ContingencyTables.RealKernelApproximation.distance line 19
  2. lemma OAI.ContingencyTables.RealKernelApproximation.distance_nonneg line 21
  3. lemma OAI.ContingencyTables.RealKernelApproximation.distance_triangle line 24
  4. lemma OAI.ContingencyTables.RealKernelApproximation.distance_event line 30
  5. lemma OAI.ContingencyTables.RealKernelApproximation.distance_push line 44
  6. lemma OAI.ContingencyTables.RealKernelApproximation.distance_push_rows line 61
  7. lemma OAI.ContingencyTables.RealKernelApproximation.distance_push_two line 77
  8. def OAI.ContingencyTables.RealKernelApproximation.rationalKernel line 90
  9. lemma OAI.ContingencyTables.RealKernelApproximation.rationalKernel_push line 97
  10. theorem OAI.ContingencyTables.RealKernelApproximation.walk_distance line 107

    Source documentation

    Each realized step may use fresh approximate oracle calls. A uniform real row error adds once per actual step against the exact real chain.

    theorem walk_distance (Q : X → RationalLaw X) (K : FiniteKernel X X)
    (η : ℝ) (hη : ∀ x,distance ((rationalKernel Q).P x) (K.P x) ≤ η)
    (x : X) (n : ℕ) :
    distance (fun y => ((walkLaw Q x n).mass y:ℝ)) ((K.power n).P x) ≤ n*η := by
…

    Mentions: OAI.ContingencyTables.RealKernelApproximation.distance, OAI.ContingencyTables.RealKernelApproximation.rationalKernel