OAI/Combinatorics/SquareDifference/IntervalLift.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SquareDifference.intervalInput line 15
  2. lemma OAI.SquareDifference.intervalInput_bound line 18
  3. lemma OAI.SquareDifference.interval_sum_mask line 25
  4. def OAI.SquareDifference.intervalPiece line 37
  5. def OAI.SquareDifference.intervalLift line 40
  6. lemma OAI.SquareDifference.intervalPiece_shift line 43
  7. lemma OAI.SquareDifference.intervalLift_shift line 59
  8. lemma OAI.SquareDifference.intervalPiece_exactSupport line 64
  9. lemma OAI.SquareDifference.intervalPiece_global line 77
  10. lemma OAI.SquareDifference.intervalLift_global line 93
  11. lemma OAI.SquareDifference.intervalPiece_moment line 98
  12. lemma OAI.SquareDifference.blockPiece_decomposition line 104
  13. lemma OAI.SquareDifference.blockLift_decomposition line 126
  14. lemma OAI.SquareDifference.uniform_interval_moments line 136