OAI/Geometry/Cannon/Modulus/Weights.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CannonDuality.Weights line 16
  2. def OAI.CannonDuality.Nonnegative line 18
  3. def OAI.CannonDuality.Admissible line 20
  4. def OAI.CannonDuality.Modulus line 23
  5. lemma OAI.CannonDuality.inner_bound_convexHull line 26
  6. lemma OAI.CannonDuality.nonnegative_convexHull line 40
  7. theorem OAI.CannonDuality.exists_dual_minimizer line 48
  8. lemma OAI.CannonDuality.normalized_admissible line 73
  9. lemma OAI.CannonDuality.normalized_energy line 89
  10. lemma OAI.CannonDuality.admissible_energy_lower line 95
  11. theorem OAI.CannonDuality.modulus_eq_inverse_dual_energy line 106
  12. theorem OAI.CannonDuality.crossing_dual_weights line 128
  13. def OAI.CannonCells.indices line 150
  14. def OAI.CannonCells.weight line 154
  15. def OAI.CannonCells.incidence line 158
  16. def OAI.CannonCells.familyVectors line 161
  17. lemma OAI.CannonCells.mem_indices line 164
  18. lemma OAI.CannonCells.mem_familyVectors line 169
  19. lemma OAI.CannonCells.incidence_nonnegative line 179
  20. lemma OAI.CannonCells.incidence_at line 185
  21. lemma OAI.CannonCells.incidence_positive line 191
  22. lemma OAI.CannonCells.incidence_cross line 200
  23. def OAI.CannonCells.modulus line 213
  24. lemma OAI.CannonCells.admissible_iff line 216
  25. lemma OAI.CannonCells.familyVectors_nonempty line 235
  26. theorem OAI.CannonCells.modulus_minimum line 240
  27. theorem OAI.CannonCells.transverse_weights line 261