OAI/Geometry/NodalSets/Charts/ProductChartPullback.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Yau.Target.productFrame line 11
  2. def OAI.Yau.Target.productMetricMatrix line 15
  3. lemma OAI.Yau.Target.product_chart_target line 21
  4. lemma OAI.Yau.Target.product_chart_inverse_derivative line 27
  5. lemma OAI.Yau.Target.product_chart_embedding_derivative line 44
  6. lemma OAI.Yau.Target.sphereWeightedChartMatrix_apply line 52
  7. lemma OAI.Yau.Target.independentAmbientMetric_productMatrix line 64