OAI/Combinatorics/SumProduct/Alignment/RoughProduct02.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RoughProductRemoval.consPair line 23
  2. lemma OAI.RoughProductRemoval.consPair_injective line 25
  3. lemma OAI.RoughProductRemoval.productTimes_succ line 35
  4. lemma OAI.RoughProductRemoval.card_productTimes_succ line 49
  5. lemma OAI.RoughProductRemoval.filter_card_product_left line 55
  6. lemma OAI.RoughProductRemoval.filter_card_product_right line 60
  7. theorem OAI.RoughProductRemoval.product_exception_bound line 69
  8. lemma OAI.RoughProductRemoval.time_positive_rough line 102
  9. lemma OAI.RoughProductRemoval.productTimes_nonempty_eventually line 109
  10. lemma OAI.RoughProductRemoval.residue_normalize line 140
  11. lemma OAI.RoughProductRemoval.physicalResidueBox_congr line 154
  12. lemma OAI.RoughProductRemoval.nestedBox_congr line 164
  13. def OAI.RoughProductRemoval.firstBad line 173
  14. lemma OAI.RoughProductRemoval.badProduct_succ_split line 185
  15. theorem OAI.RoughProductRemoval.firstBad_reduction line 218