OAI/Geometry/NodalSets/Charts/SphereChartVolume.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Yau.Target.BaseModel line 10
  2. def OAI.Yau.Target.sphereChartDerivative line 12
  3. def OAI.Yau.Target.sphereChartFrame line 16
  4. lemma OAI.Yau.Target.sphereChartFrame_apply line 20
  5. lemma OAI.Yau.Target.sphereChartFrame_mulVec line 25
  6. lemma OAI.Yau.Target.sphereChartDerivative_injective line 32
  7. lemma OAI.Yau.Target.sphereChartFrame_injective line 40
  8. lemma OAI.Yau.Target.sphereChartFrame_orthogonal line 49
  9. lemma OAI.Yau.Target.sphere_radial_dot line 61
  10. def OAI.Yau.Target.sphereRoundChartMatrix line 68
  11. def OAI.Yau.Target.sphereWeightedChartMatrix line 71
  12. lemma OAI.Yau.Target.sphereRoundChartMatrix_posDef line 75
  13. lemma OAI.Yau.Target.sphereWeightedChartMatrix_posDef line 81
  14. lemma OAI.Yau.Target.sphere_chart_determinant_ratio line 88
  15. lemma OAI.Yau.Target.sphere_chart_volume_ratio line 99