OAI/Geometry/NodalSets/Charts/FixedChartAmbientLaplacian.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Yau.Target.sphere_coordinate_linear_sum line 14
2. lemma OAI.Yau.Target.sphere_restriction_second_trace_at line 19
3. theorem OAI.Yau.Target.fixed_chart_round_operator_ambient_restriction line 46