OAI/Geometry/CAT0Fillings/Chord/ProfileBound.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.CAT0Fillings.Conformal.weighted_kernel_average_le_oneline 12 - lemma
OAI.CAT0Fillings.Conformal.profile_boundline 23 - lemma
OAI.CAT0Fillings.Conformal.profile_term_boundline 28 - lemma
OAI.CAT0Fillings.Conformal.bubbleProfile_continuousline 47 - lemma
OAI.CAT0Fillings.Conformal.profile_integrableline 55 - lemma
OAI.CAT0Fillings.Conformal.profile_averageline 70