OAI/Analysis/Mahler/Diamonds.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SymmetricMahler.IsParallelPair.square line 15
  2. lemma OAI.SymmetricMahler.facial_diamond line 29
  3. def OAI.SymmetricMahler.HasMaximalMRank line 175
  4. lemma OAI.SymmetricMahler.maximal_mface_child_parallel line 179
  5. theorem OAI.SymmetricMahler.maximal_mface_children_parallel line 273
  6. lemma OAI.SymmetricMahler.IsParallelFace.refl line 289
  7. lemma OAI.SymmetricMahler.IsParallelPair.square_sides line 292
  8. theorem OAI.SymmetricMahler.maximal_mface_parallel line 308
  9. lemma OAI.SymmetricMahler.IsFace.exists_generator line 486
  10. lemma OAI.SymmetricMahler.faceHull_midpoint_eq line 510
  11. lemma OAI.SymmetricMahler.IsFace.exposed_generator line 528
  12. lemma OAI.SymmetricMahler.faceHull_radial line 582
  13. lemma OAI.SymmetricMahler.finrank_strongDual line 638
  14. def OAI.SymmetricMahler.finiteBidual line 642
  15. lemma OAI.SymmetricMahler.finiteBidual_apply line 646
  16. lemma OAI.SymmetricMahler.LinearIsometryEquiv.image_extreme_unit line 649
  17. lemma OAI.SymmetricMahler.extreme_unit_neg line 654
  18. lemma OAI.SymmetricMahler.dual_disjoint_faces_primal_vertex line 662
  19. lemma OAI.SymmetricMahler.IsParallelPair.square_points line 674
  20. lemma OAI.SymmetricMahler.maximal_unit_face_support line 687
  21. lemma OAI.SymmetricMahler.dual_vertex_maximal_support line 700
  22. lemma OAI.SymmetricMahler.vertex_in_two_vertex_face line 710
  23. def OAI.SymmetricMahler.IsSplitPair line 728
  24. def OAI.SymmetricMahler.IsSplitFace line 731
  25. lemma OAI.SymmetricMahler.disjoint_span_insert line 734
  26. theorem OAI.SymmetricMahler.split_of_no_vertex_parallelogram line 749
  27. theorem OAI.SymmetricMahler.nonsplit_vertex_parallelogram line 823