OAI/Combinatorics/SumProduct/Alignment/PairTail04.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PairTail.squareFiltration line 28
  2. lemma OAI.PairTail.squareFiltration_zero line 42
  3. lemma OAI.PairTail.squareFiltration_one line 51
  4. lemma OAI.PairTail.squareFiltration_eq_pairLevel line 56
  5. lemma OAI.PairTail.squareFiltration_last line 73
  6. lemma OAI.PairTail.level_last_central line 82
  7. def OAI.PairTail.reducedSquareFiltration line 95
  8. lemma OAI.PairTail.reducedSquareFiltration_zero line 101
  9. lemma OAI.PairTail.reducedSquareFiltration_one line 107
  10. lemma OAI.PairTail.reducedSquareFiltration_last line 113
  11. lemma OAI.PairTail.reducedSquareFiltration_level line 118
  12. lemma OAI.PairTail.filtration_cutoff_monotone line 138
  13. lemma OAI.PairTail.square_tail_equation line 165
  14. theorem OAI.PairTail.exists_adapted_reducedCoordinates line 172
  15. lemma OAI.RationalLattice.pullCoordinates_axis line 236
  16. lemma OAI.RationalLattice.pullCoordinates_secondKind line 242
  17. theorem OAI.LeibmanSquare.exists_adapted_sourceReducedCoordinates line 269