OAI/Combinatorics/SquareDifference/IntervalTruncation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SquareDifference.retainedFamily line 19
  2. lemma OAI.SquareDifference.retainedFamily_sub line 22
  3. lemma OAI.SquareDifference.retainedFamily_tail_den line 33
  4. def OAI.SquareDifference.retainedIntervalLift line 45
  5. lemma OAI.SquareDifference.retainedInterval_diff line 49
  6. lemma OAI.SquareDifference.uniform_marginal_moment line 56
  7. lemma OAI.SquareDifference.interval_tail_energy line 71
  8. lemma OAI.SquareDifference.uniform_truncation_error line 86
  9. lemma OAI.SquareDifference.tensor_all_marginals line 101
  10. lemma OAI.SquareDifference.tensorGood_uniform_marginal line 107
  11. lemma OAI.SquareDifference.interval_full_moment line 113
  12. lemma OAI.SquareDifference.interval_retained_moment line 119
  13. lemma OAI.SquareDifference.interval_two_moment line 127
  14. lemma OAI.SquareDifference.interval_truncation_error line 133