OAI/Combinatorics/ContingencyTables/Transport/PowerOfTwoApproximation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.PowerOfTwoApproximation.numerator line 14
2. def OAI.ContingencyTables.PowerOfTwoApproximation.rounded line 16
3. def OAI.ContingencyTables.PowerOfTwoApproximation.approximation line 18
4. lemma OAI.ContingencyTables.PowerOfTwoApproximation.rounded_bounds line 20
5. lemma OAI.ContingencyTables.PowerOfTwoApproximation.rounded_power_root line 36
6. lemma OAI.ContingencyTables.PowerOfTwoApproximation.rounded_power_error line 46

   Source documentation

   Rounding downward loses at most 1/s in relative value. The proof uses only the tangent bound for exp and log 2 ≤ 1.

   lemma rounded_power_error (beta : ℚ) (s : ℕ) (hs : 0 < s) :
       0 ≤ (2:ℝ)^(beta:ℝ)-(2:ℝ)^rounded beta s ∧
         (2:ℝ)^(beta:ℝ)-(2:ℝ)^rounded beta s ≤ (2:ℝ)^(beta:ℝ)/(s:ℝ) := by
   …

   Mentions: OAI.ContingencyTables.PowerOfTwoApproximation.rounded

7. theorem OAI.ContingencyTables.PowerOfTwoApproximation.approximation_error line 68

   Source documentation

   The only non-rational quantity in the proof is the target. The returned value is the midpoint of a fixed number of rational comparisons.

   theorem approximation_error (beta : ℚ) (hlo : -2 ≤ beta) (hhi : beta ≤ 2)
       (s n : ℕ) (hs : 0 < s) (sigma : ℝ)
       (hbudget : 1/(s:ℝ)+32/(2:ℝ)^n ≤ sigma) :
       |(approximation beta s n:ℝ)-(2:ℝ)^(beta:ℝ)| ≤ sigma*(2:ℝ)^(beta:ℝ) := by
   …

   Mentions: OAI.ContingencyTables.PowerOfTwoApproximation.approximation

8. def OAI.ContingencyTables.PowerOfTwoApproximation.rootDegree line 103
9. def OAI.ContingencyTables.PowerOfTwoApproximation.depth line 105
10. def OAI.ContingencyTables.PowerOfTwoApproximation.approximate line 107
11. lemma OAI.ContingencyTables.PowerOfTwoApproximation.degree_positive line 109
12. lemma OAI.ContingencyTables.PowerOfTwoApproximation.degree_le line 115
13. lemma OAI.ContingencyTables.PowerOfTwoApproximation.error_budget line 119
14. theorem OAI.ContingencyTables.PowerOfTwoApproximation.approximate_error line 140
15. theorem OAI.ContingencyTables.PowerOfTwoApproximation.approximate_positive line 145