OAI/Geometry/TamingCompatibility/DifferentialForms/MetricDensity.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.MetricDensity.gram line 25
  2. lemma OAI.TamingCompatibility.MetricDensity.gram_posDef line 28
  3. def OAI.TamingCompatibility.MetricDensity.density line 48
  4. lemma OAI.TamingCompatibility.MetricDensity.density_pos line 50
  5. lemma OAI.TamingCompatibility.MetricDensity.density_sq line 53
  6. lemma OAI.TamingCompatibility.MetricDensity.density_transform line 56
  7. lemma OAI.TamingCompatibility.MetricDensity.contDiffOn_det line 63
  8. lemma OAI.TamingCompatibility.MetricDensity.contDiffOn_density line 72
  9. lemma OAI.TamingCompatibility.MetricDensity.contDiffOn_gram_density line 78
  10. def OAI.TamingCompatibility.MetricDensity.pullMetric line 90
  11. lemma OAI.TamingCompatibility.MetricDensity.pullMetric_apply line 94
  12. lemma OAI.TamingCompatibility.MetricDensity.gram_pullMetric line 97
  13. lemma OAI.TamingCompatibility.MetricDensity.density_pullMetric line 114