OAI/Geometry/CAT0Fillings/Chord/Identity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.AnalyticMinimizer.quotient_bound_real line 14
2. lemma OAI.CAT0Fillings.AnalyticMinimizer.critical_quotient_bound line 21
3. lemma OAI.CAT0Fillings.AnalyticMinimizer.critical_ratio_product line 28
4. lemma OAI.CAT0Fillings.AnalyticMinimizer.critical_scalar_start line 40
5. lemma OAI.CAT0Fillings.Conformal.bubble_derivative_square line 70
6. lemma OAI.CAT0Fillings.Conformal.profile_substitution line 77
7. lemma OAI.CAT0Fillings.Conformal.profile_scalar_identity line 119