OAI/Combinatorics/ContingencyTables/Transport/FiniteLawMoments.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.FiniteLawMoments.expectation line 15
2. lemma OAI.ContingencyTables.FiniteLawMoments.expectation_map line 17
3. lemma OAI.ContingencyTables.FiniteLawMoments.expectation_uniform line 32
4. lemma OAI.ContingencyTables.FiniteLawMoments.word_expectation line 39
5. theorem OAI.ContingencyTables.FiniteLawMoments.expectation_difference line 45

   Source documentation

   Bounded real observables may be evaluated after a rational finite experiment. Their expectation error follows from the actual output TV.

   theorem expectation_difference (p q : RationalLaw X) (g : X → ℝ) (U : ℝ)
       (hg : ∀ x,|g x| ≤ U) :
       |expectation p g-expectation q g| ≤ 2*U*(variation p q:ℝ) := by
   …

   Mentions: OAI.ContingencyTables.FiniteLawMoments.expectation

6. lemma OAI.ContingencyTables.FiniteLawMoments.expectation_bounds line 67