OAI/Geometry/Perimeter/Regularity/GeoComposition.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.RPISingularHarnack.GeoC.constline 11 - theorem
OAI.RPISingularHarnack.GeoC.clm_of_applyline 19 - theorem
OAI.RPISingularHarnack.GeoC.fderivline 40 - theorem
OAI.RPISingularHarnack.GeoC.gradientline 45 - theorem
OAI.RPISingularHarnack.geoC_compline 49