OAI/Analysis/Mahler/EqualityMedians.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SymmetricMahler.mem_convexHull_zero_fiber line 13
2. lemma OAI.SymmetricMahler.isCompact_convexHull_of_isCompact line 34
3. lemma OAI.SymmetricMahler.mem_convexHull_zero_fiber_of_tendsto line 82
4. lemma OAI.SymmetricMahler.pow_mul_one_sub_le_inv line 95
5. def OAI.SymmetricMahler.rowPair line 113
6. lemma OAI.SymmetricMahler.continuous_rowPair line 115
7. def OAI.SymmetricMahler.rowComplex line 120
8. lemma OAI.SymmetricMahler.continuous_rowComplex line 123
9. theorem OAI.SymmetricMahler.common_boundary_witness_of_concentration line 129
10. lemma OAI.SymmetricMahler.rowPair_neg line 222
11. lemma OAI.SymmetricMahler.rowComplex_neg line 225
12. lemma OAI.SymmetricMahler.planarPrimitive_nonneg_iff line 230
13. lemma OAI.SymmetricMahler.exists_positive_strip_sample line 236
14. lemma OAI.SymmetricMahler.strip_weights_bound line 257
15. lemma OAI.SymmetricMahler.strip_concentration_bound line 270
16. lemma OAI.SymmetricMahler.exists_fast_strip_degrees line 296
17. lemma OAI.SymmetricMahler.rowPair_sum_smul line 326
18. theorem OAI.SymmetricMahler.common_boundary_witness_of_unnormalized line 338
19. lemma OAI.SymmetricMahler.rowComplex_eq_stripCoordinate line 393
20. lemma OAI.SymmetricMahler.push_eq_sum_smul line 397
21. lemma OAI.SymmetricMahler.strip_prefix_compact line 402
22. lemma OAI.SymmetricMahler.closed_lens_constraints_of_dense_prefix_limit line 412
23. theorem OAI.SymmetricMahler.equality_common_lens_witness line 432
24. def OAI.SymmetricMahler.RealNormData.segmentEquiv line 513
25. lemma OAI.SymmetricMahler.RealNormData.segmentEquiv_apply line 517
26. lemma OAI.SymmetricMahler.RealNormData.lifted_pair line 520
27. theorem OAI.SymmetricMahler.RealNormData.optimal_lift_of_equality line 526
28. theorem OAI.SymmetricMahler.RealNormData.medians_of_equality line 596
29. theorem OAI.SymmetricMahler.equality_polar_gauge_medians line 606