OAI/Combinatorics/EuclideanRamsey/LatticeMoments.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.EuclideanRamsey.Lattice line 21
  2. abbrev OAI.EuclideanRamsey.RationalSpace line 22
  3. abbrev OAI.EuclideanRamsey.LatticeRing line 23
  4. def OAI.EuclideanRamsey.rationalize line 25
  5. def OAI.EuclideanRamsey.latticeSpan line 30
  6. def OAI.EuclideanRamsey.matrixTensor line 33
  7. def OAI.EuclideanRamsey.quotientTensor line 37
  8. def OAI.EuclideanRamsey.mass line 40
  9. def OAI.EuclideanRamsey.firstMoment line 42
  10. def OAI.EuclideanRamsey.secondMoment line 45
  11. def OAI.EuclideanRamsey.cosetPushforward line 48
  12. def OAI.EuclideanRamsey.FiniteLatticeIdentity line 51
  13. instance OAI.EuclideanRamsey.latticeNoetherian line 62
  14. def OAI.EuclideanRamsey.augmentation line 65
  15. def OAI.EuclideanRamsey.augmentationIdeal line 68
  16. lemma OAI.EuclideanRamsey.augmentation_eq_mass line 70
  17. lemma OAI.EuclideanRamsey.augmentation_monomial line 73
  18. lemma OAI.EuclideanRamsey.monomial_sub_one_mem line 77
  19. def OAI.EuclideanRamsey.coefficientFunctional line 82
  20. lemma OAI.EuclideanRamsey.coefficientFunctional_apply line 85
  21. lemma OAI.EuclideanRamsey.coefficientFunctional_single line 88
  22. lemma OAI.EuclideanRamsey.mass_linear line 92
  23. lemma OAI.EuclideanRamsey.firstMoment_linear line 96
  24. lemma OAI.EuclideanRamsey.secondMoment_linear line 99
  25. lemma OAI.EuclideanRamsey.mass_add line 105
  26. lemma OAI.EuclideanRamsey.mass_smul line 107
  27. lemma OAI.EuclideanRamsey.mass_zero line 109
  28. lemma OAI.EuclideanRamsey.mass_single line 110
  29. lemma OAI.EuclideanRamsey.mass_mul line 112
  30. lemma OAI.EuclideanRamsey.firstMoment_add line 114
  31. lemma OAI.EuclideanRamsey.firstMoment_smul line 118
  32. lemma OAI.EuclideanRamsey.firstMoment_zero line 122
  33. lemma OAI.EuclideanRamsey.firstMoment_single line 124
  34. lemma OAI.EuclideanRamsey.secondMoment_add line 126
  35. lemma OAI.EuclideanRamsey.secondMoment_smul line 130
  36. lemma OAI.EuclideanRamsey.secondMoment_zero line 134
  37. lemma OAI.EuclideanRamsey.secondMoment_single line 137
  38. lemma OAI.EuclideanRamsey.firstMoment_mul line 142
  39. lemma OAI.EuclideanRamsey.secondMoment_mul line 153
  40. lemma OAI.EuclideanRamsey.mass_sub line 165
  41. lemma OAI.EuclideanRamsey.firstMoment_sub line 167
  42. lemma OAI.EuclideanRamsey.secondMoment_sub line 170
  43. lemma OAI.EuclideanRamsey.mass_one line 174
  44. lemma OAI.EuclideanRamsey.firstMoment_one line 177
  45. lemma OAI.EuclideanRamsey.secondMoment_one line 180
  46. lemma OAI.EuclideanRamsey.mem_augmentationIdeal line 184
  47. def OAI.EuclideanRamsey.jetOne line 189
  48. def OAI.EuclideanRamsey.jetTwo line 197
  49. lemma OAI.EuclideanRamsey.augmentation_sq_le_jetOne line 205
  50. lemma OAI.EuclideanRamsey.augmentation_cube_le_jetTwo line 214
  51. lemma OAI.EuclideanRamsey.moments_eq_of_sub_mem_cube line 223
  52. lemma OAI.EuclideanRamsey.mass_sum line 231
  53. lemma OAI.EuclideanRamsey.firstMoment_sum line 234
  54. lemma OAI.EuclideanRamsey.secondMoment_sum line 237
  55. def OAI.EuclideanRamsey.quadraticStencil line 242
  56. lemma OAI.EuclideanRamsey.quadraticStencil_moments line 245