OAI/Combinatorics/SumProduct/Alignment/ScalarDifference01.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubeMaxFiltration.level line 28
  2. lemma OAI.CubeMaxFiltration.face_mem line 31
  3. lemma OAI.CubeMaxFiltration.antitone line 36
  4. lemma OAI.CubeMaxFiltration.level_zero line 42
  5. lemma OAI.CubeMaxFiltration.level_one line 45
  6. lemma OAI.CubeMaxFiltration.max_union_degree line 53
  7. lemma OAI.CubeMaxFiltration.normalizes line 58
  8. lemma OAI.CubeMaxFiltration.face_commutator_mem line 87
  9. lemma OAI.CubeMaxFiltration.commutator_mem line 101
  10. def OAI.CubeMaxFiltration.ambient line 116
  11. def OAI.CubeMaxFiltration.filtration line 122
  12. lemma OAI.CubeMaxFiltration.filtration_zero line 130
  13. lemma OAI.CubeMaxFiltration.filtration_one line 135
  14. lemma OAI.CubeMaxFiltration.level_bot line 140
  15. lemma OAI.CubeMaxFiltration.filtration_bot line 147
  16. lemma OAI.CubeMaxFiltration.taylor_face_mem line 155
  17. def OAI.ScalarDifferenceDegree.diff line 173
  18. def OAI.ScalarDifferenceDegree.DegreeAtMost line 175
  19. lemma OAI.ScalarDifferenceDegree.constant line 179
  20. lemma OAI.ScalarDifferenceDegree.add line 189
  21. lemma OAI.ScalarDifferenceDegree.mul_const line 200
  22. lemma OAI.ScalarDifferenceDegree.mono_step line 211
  23. lemma OAI.ScalarDifferenceDegree.mono line 216
  24. lemma OAI.ScalarDifferenceDegree.shift line 221
  25. lemma OAI.ScalarDifferenceDegree.mul line 232
  26. lemma OAI.ScalarDifferenceDegree.pow line 256
  27. lemma OAI.ScalarDifferenceDegree.sum line 263
  28. lemma OAI.ScalarDifferenceDegree.prod line 272
  29. lemma OAI.ScalarDifferenceDegree.hom line 282
  30. lemma OAI.ScalarDifferenceDegree.eval_monomial line 288
  31. lemma OAI.ScalarDifferenceDegree.eval_polynomial line 303
  32. def OAI.ScalarDifferenceDegree.iterDiff line 314
  33. lemma OAI.ScalarDifferenceDegree.iterDiff_zero_function line 318
  34. lemma OAI.ScalarDifferenceDegree.iterDiff_zero line 325
  35. theorem OAI.ScalarDifferenceDegree.polynomial_power line 341