OAI/Geometry/CAT0Fillings/Sobolev/CriticalNorm.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.AnalyticMinimizer.lpNorm_sq_eq_integral line 12
2. lemma OAI.CAT0Fillings.AnalyticMinimizer.no_loss line 22
3. lemma OAI.CAT0Fillings.AnalyticMinimizer.concentration_inequality line 31
4. lemma OAI.CAT0Fillings.AnalyticMinimizer.lpNorm_congr_ae line 57
5. def OAI.CAT0Fillings.AnalyticMinimizer.criticalNorm line 61
6. def OAI.CAT0Fillings.AnalyticMinimizer.criticalMass line 64
7. lemma OAI.CAT0Fillings.AnalyticMinimizer.criticalNorm_nonneg line 67
8. lemma OAI.CAT0Fillings.AnalyticMinimizer.criticalMass_nonneg line 70
9. lemma OAI.CAT0Fillings.AnalyticMinimizer.criticalNorm_smul line 74
10. lemma OAI.CAT0Fillings.AnalyticMinimizer.criticalNorm_sq line 80
11. lemma OAI.CAT0Fillings.AnalyticMinimizer.criticalMass_eq line 84
12. lemma OAI.CAT0Fillings.AnalyticMinimizer.criticalMass_sub line 91
13. lemma OAI.CAT0Fillings.AnalyticMinimizer.criticalMass_integrable line 100