OAI/Analysis/Mahler/Splitting.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SymmetricMahler.maximal_unit_face_vertex_sign line 15
  2. lemma OAI.SymmetricMahler.supporting_sum_eval line 24
  3. lemma OAI.SymmetricMahler.crossing_support line 35
  4. theorem OAI.SymmetricMahler.mface_split_core line 87
  5. def OAI.SymmetricMahler.fourSum line 238
  6. abbrev OAI.SymmetricMahler.ZeroSumFour line 241
  7. def OAI.SymmetricMahler.ZeroSumFour.entry line 245
  8. lemma OAI.SymmetricMahler.ZeroSumFour.entry_add line 247
  9. lemma OAI.SymmetricMahler.ZeroSumFour.entry_sub line 249
  10. lemma OAI.SymmetricMahler.ZeroSumFour.entry_smul line 251
  11. lemma OAI.SymmetricMahler.ZeroSumFour.entry_zero line 253
  12. lemma OAI.SymmetricMahler.ZeroSumFour.sum_entry line 255
  13. lemma OAI.SymmetricMahler.ZeroSumFour.norm_eq_sum line 261
  14. def OAI.SymmetricMahler.ZeroSumFour.pair line 264
  15. lemma OAI.SymmetricMahler.ZeroSumFour.entry_pair line 268
  16. lemma OAI.SymmetricMahler.ZeroSumFour.pair_norm_add line 272
  17. lemma OAI.SymmetricMahler.ZeroSumFour.pair_additive_of_extreme line 287
  18. theorem OAI.SymmetricMahler.ZeroSumFour.extreme_four_norms line 313
  19. lemma OAI.SymmetricMahler.IsCompact.exists_extreme_ge line 361
  20. lemma OAI.SymmetricMahler.normalized_mem_exposed line 371
  21. def OAI.SymmetricMahler.ZeroSumFour.entryL line 383
  22. lemma OAI.SymmetricMahler.ZeroSumFour.entryL_apply line 388
  23. lemma OAI.SymmetricMahler.ZeroSumFour.coordinate_extreme line 390
  24. lemma OAI.SymmetricMahler.faceHull_union_generators line 434
  25. def OAI.SymmetricMahler.ZeroSumFour.ofFour line 451
  26. lemma OAI.SymmetricMahler.ZeroSumFour.entry_ofFour line 456
  27. theorem OAI.SymmetricMahler.two_face_exchange line 460
  28. lemma OAI.SymmetricMahler.proper_unit_face_not_neg line 616
  29. lemma OAI.SymmetricMahler.IsParallelPair.restrict_support line 627
  30. theorem OAI.SymmetricMahler.mface_split_precore line 634
  31. theorem OAI.SymmetricMahler.maximal_mface_split line 769
  32. lemma OAI.SymmetricMahler.faceRank_singleton_le line 842
  33. lemma OAI.SymmetricMahler.mface_pair_obstruction line 845
  34. lemma OAI.SymmetricMahler.IsFace.neg line 952
  35. lemma OAI.SymmetricMahler.IsMaximalProperFace.neg line 961
  36. lemma OAI.SymmetricMahler.HasMFaceStructure.neg line 974
  37. lemma OAI.SymmetricMahler.neg_unitBall line 984
  38. lemma OAI.SymmetricMahler.IsMaximalProperFace.neg_unit line 988
  39. lemma OAI.SymmetricMahler.maximal_unit_face_span line 1001
  40. lemma OAI.SymmetricMahler.dual_eq_on_maximal_face line 1008
  41. lemma OAI.SymmetricMahler.dual_vertex_eq_of_supports line 1016
  42. lemma OAI.SymmetricMahler.dual_mface_obstruction_at_vertex line 1035
  43. theorem OAI.SymmetricMahler.not_primal_dual_maximal_mfaces line 1116
  44. lemma OAI.SymmetricMahler.face_rank_gt_one_vertices line 1144
  45. lemma OAI.SymmetricMahler.face_rank_two_pair line 1159
  46. lemma OAI.SymmetricMahler.exists_rank_two_face line 1201
  47. lemma OAI.SymmetricMahler.exists_maximal_unit_face line 1218
  48. lemma OAI.SymmetricMahler.exists_maximal_mface line 1228
  49. lemma OAI.SymmetricMahler.proper_split_of_no_maximal_mface line 1246