OAI/Combinatorics/ContingencyTables/Transport/FiniteProductAccuracy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Relative accuracy of the finite product used by the weight oracle

  1. lemma OAI.ContingencyTables.FiniteProductAccuracy.relative_log line 14
  2. lemma OAI.ContingencyTables.FiniteProductAccuracy.product_log line 23
  3. theorem OAI.ContingencyTables.FiniteProductAccuracy.product_relative line 36

    Source documentation

    The source has j+1 factors, each observed to the same tolerance. This scalar budget is sufficient for its requested relative interval.

    theorem product_relative (x y : J → ℝ) (hy : ∀ j,0 < y j) (epsilon : ℝ)
    (he0 : 0 < epsilon) (he1 : epsilon < 1)
    (herr : ∀ j,|x j-y j| ≤ (epsilon/(200*(Fintype.card J:ℝ)))*y j)
    (hcard : 0 < Fintype.card J) :
    (1-epsilon/4)*(∏ j,y j) ≤ ∏ j,x j ∧
      (∏ j,x j) ≤ (1+epsilon/4)*(∏ j,y j) := by
…