OAI/Geometry/NodalSets/Charts/SphereReferenceMeasureInvariance.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Yau.Target.sphereChartCoordMap_measurableEmbedding line 13
2. lemma OAI.Yau.Target.roundChartDensity_coord_eq line 16
3. lemma OAI.Yau.Target.sphereReferenceMeasure_lintegral_chart_change line 20
4. theorem OAI.Yau.Target.sphereReferenceMeasure_eq_chart line 41
5. lemma OAI.Yau.Target.sphereReferenceMeasure_integral_chart line 57
6. lemma OAI.Yau.Target.sphereReferenceMeasure_integrable_chart line 67