OAI/Combinatorics/SumProduct/Alignment/CoordinateSubspace01.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RationalNilmanifoldMeasure.nilpotent_of_series line 25
  2. theorem OAI.RationalNilmanifoldMeasure.existsUnique_invariant line 35
  3. theorem OAI.RationalLattice.existsUnique_coordinateHaar line 72
  4. def OAI.PairTail.squareLattice line 103
  5. lemma OAI.PairTail.mem_squareLattice line 106
  6. def OAI.PairTail.reducedLattice line 109
  7. theorem OAI.PairTail.reducedLattice_iff line 119
  8. theorem OAI.PairTail.reducedLattice_discrete line 159
  9. theorem OAI.PairTail.reducedHaar_existsUnique line 165
  10. def OAI.CoordinateSubspace.lift line 187
  11. lemma OAI.CoordinateSubspace.lift_embed line 190
  12. lemma OAI.CoordinateSubspace.lift_outside line 197
  13. lemma OAI.CoordinateSubspace.lift_continuous line 200
  14. lemma OAI.CoordinateSubspace.lift_polynomial line 208
  15. def OAI.CoordinateSubspace.coordinates line 217
  16. lemma OAI.CoordinateSubspace.coord_lift line 220
  17. def OAI.CoordinateSubspace.rebuild line 227
  18. lemma OAI.CoordinateSubspace.coordinates_rebuild line 232
  19. lemma OAI.CoordinateSubspace.rebuild_coordinates line 237
  20. def OAI.CoordinateSubspace.subspaceHomeomorph line 243
  21. def OAI.CoordinateSubspace.lowerLift line 252
  22. lemma OAI.CoordinateSubspace.lowerLift_polynomial line 256
  23. lemma OAI.CoordinateSubspace.lowerLift_coordinates line 264
  24. lemma OAI.CoordinateSubspace.correction_exists line 280
  25. def OAI.CoordinateSubspace.correction line 295
  26. lemma OAI.CoordinateSubspace.mul_coord line 299
  27. def OAI.CoordinateSubspace.restrictedCoordinates line 317
  28. lemma OAI.CoordinateSubspace.restricted_lattice line 323