OAI/Geometry/NodalSets/Spectral/SphereResolventFormBounds.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Yau.Target.sphere_resolvent_smooth_variationalline 12 - theorem
OAI.Yau.Target.sphere_resolvent_quadratic_to_form_lowerline 26 - theorem
OAI.Yau.Target.sphere_smooth_rayleigh_of_resolvent_boundline 47