OAI/Geometry/NodalSets/Charts/SphereReferenceMeasurePositive.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Yau.Target.roundCoordMeasure_openPos line 13
  2. lemma OAI.Yau.Target.sphereReferenceMeasure_openPos line 21
  3. def OAI.Yau.Target.sphereWeightedPairing line 32
  4. lemma OAI.Yau.Target.sphereWeightedPairing_integrable line 35
  5. lemma OAI.Yau.Target.sphereWeightedPairing_self_pos line 40
  6. lemma OAI.Yau.Target.sphereWeightedPairing_symm line 57
  7. lemma OAI.Yau.Target.sphereWeightedPairing_smul_left line 62
  8. lemma OAI.Yau.Target.sphereWeightedPairing_add_left line 71