OAI/Geometry/NodalSets/Charts/SpherePreservingEquation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Yau.Target.intrinsicWeightedChartOperator_coefficients_eq line 14
2. lemma OAI.Yau.Target.intrinsic_eigenfunction_correction_residual_zero line 29
3. lemma OAI.Yau.Target.round_preserving_cancellation_smul line 52
4. theorem OAI.Yau.Target.sphere_equation_preserved_by_round_cancellation line 75