OAI/Geometry/NodalSets/Spectral/MetricProjectionBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Yau.Geometry.metricPerpProjection line 9
2. lemma OAI.Yau.Geometry.metricPerpProjection_orthogonal line 12
3. lemma OAI.Yau.Geometry.metricPerpProjection_difference_bound line 16
4. lemma OAI.Yau.Geometry.metric_normalization_near_unit line 36
5. theorem OAI.Yau.Geometry.normalized_projection_stability line 66