OAI/Combinatorics/SquareDifference/OutsideFourier.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SquareDifference.PairBridge.outsideExtend line 19
  2. lemma OAI.SquareDifference.PairBridge.outsideExtend_neg line 22
  3. lemma OAI.SquareDifference.PairBridge.outsideExtend_disjoint line 33
  4. lemma OAI.SquareDifference.PairBridge.outsideExtend_char line 44
  5. lemma OAI.SquareDifference.PairBridge.outsideExtend_denominator line 56
  6. lemma OAI.SquareDifference.PairBridge.expect_outside line 78
  7. def OAI.SquareDifference.PairBridge.assembleOutside line 86
  8. lemma OAI.SquareDifference.PairBridge.assembleOutside_freeze line 89
  9. lemma OAI.SquareDifference.PairBridge.frozenFourier_outside line 100
  10. lemma OAI.SquareDifference.PairBridge.sequenceCoeff_outside line 108
  11. lemma OAI.SquareDifference.PairBridge.actual_frozen_outside_coefficient line 113
  12. lemma OAI.SquareDifference.PairBridge.outside_fiber_second_moment line 122