OAI/Geometry/NodalSets/Charts/SphereWeightedChartL2.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Yau.Target.sphereWeightedMeasure_ae_iff line 12
  2. theorem OAI.Yau.Target.sphereWeightedMeasure_ae_chart_iff line 17
  3. theorem OAI.Yau.Target.sphereWeightedMeasure_integrable_iff line 25
  4. theorem OAI.Yau.Target.sphereWeightedL2_test_pairing line 33
  5. theorem OAI.Yau.Target.sphereWeightedL2_test_chart line 56