OAI/Analysis/Mahler/Classification.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SymmetricMahler.LDecomposition line 14
  2. lemma OAI.SymmetricMahler.maximal_unit_face_hull line 24
  3. lemma OAI.SymmetricMahler.norm_add_of_split line 40
  4. lemma OAI.SymmetricMahler.HasMetricMedians.of_retract line 121
  5. lemma OAI.SymmetricMahler.HasMetricMedians.linearIsometryEquiv line 140
  6. lemma OAI.SymmetricMahler.continuousLinearMap_dist_le line 146
  7. lemma OAI.SymmetricMahler.dual_comp_dist_le line 152
  8. def OAI.SymmetricMahler.LDecomposition.swap line 171
  9. lemma OAI.SymmetricMahler.LDecomposition.finrank_add line 179
  10. lemma OAI.SymmetricMahler.LDecomposition.left_lt line 183
  11. lemma OAI.SymmetricMahler.LDecomposition.right_lt line 188
  12. def OAI.SymmetricMahler.LDecomposition.leftInclusion line 193
  13. def OAI.SymmetricMahler.LDecomposition.leftProjection line 196
  14. lemma OAI.SymmetricMahler.LDecomposition.leftProjection_leftInclusion line 199
  15. lemma OAI.SymmetricMahler.LDecomposition.norm_leftInclusion line 204
  16. lemma OAI.SymmetricMahler.LDecomposition.norm_leftProjection_le line 208
  17. lemma OAI.SymmetricMahler.LDecomposition.left_medians line 214
  18. lemma OAI.SymmetricMahler.LDecomposition.left_dual_medians line 219
  19. lemma OAI.SymmetricMahler.LDecomposition.right_medians line 228
  20. lemma OAI.SymmetricMahler.LDecomposition.right_dual_medians line 231
  21. def OAI.SymmetricMahler.HannerSpace line 239
  22. lemma OAI.SymmetricMahler.HannerSpace.linearIsometryEquiv line 246
  23. lemma OAI.SymmetricMahler.hannerSpace_one line 253
  24. def OAI.SymmetricMahler.coordinateDual line 275
  25. lemma OAI.SymmetricMahler.coordinateDual_apply line 280
  26. lemma OAI.SymmetricMahler.dual_norm_le_one_iff line 293
  27. lemma OAI.SymmetricMahler.HannerSpace.dual line 308
  28. def OAI.SymmetricMahler.normData line 327
  29. lemma OAI.SymmetricMahler.normData_apply line 333
  30. lemma OAI.SymmetricMahler.normData_unit line 336
  31. lemma OAI.SymmetricMahler.LDecomposition.unitBall line 343
  32. lemma OAI.SymmetricMahler.LDecomposition.hannerSpace line 353
  33. theorem OAI.SymmetricMahler.median_decomposition line 387
  34. theorem OAI.SymmetricMahler.hannerSpace_of_medians_rank line 419
  35. theorem OAI.SymmetricMahler.hannerSpace_of_medians line 454
  36. lemma OAI.SymmetricMahler.RealNormData.coordinateDual_space_apply line 461
  37. def OAI.SymmetricMahler.RealNormData.IsDual.dualIsometry line 467
  38. lemma OAI.SymmetricMahler.RealNormData.hannerSpace_iff_linearHanner line 498
  39. theorem OAI.SymmetricMahler.equality_implies_linearHanner line 518
  40. theorem OAI.SymmetricMahler.symmetric_mahler_equality line 534

    Distinct definitions of this name: ComparatorChallenges/SymmetricMahlerEquality.lean:43 (same statement text; different proof or body). Qualify references as OAI.SymmetricMahler.symmetric_mahler_equality@path.