OAI/Geometry/TamingCompatibility/Charts/ChartMetric.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.ManifoldVolume.chartMetric line 27
  2. lemma OAI.TamingCompatibility.ManifoldVolume.chartMetric_apply line 31
  3. lemma OAI.TamingCompatibility.ManifoldVolume.chartMetric_symm line 51
  4. lemma OAI.TamingCompatibility.ManifoldVolume.chartMetric_pos line 57
  5. def OAI.TamingCompatibility.ManifoldVolume.chartDensity line 71
  6. lemma OAI.TamingCompatibility.ManifoldVolume.chartDensity_pos line 75
  7. lemma OAI.TamingCompatibility.ManifoldVolume.chartDensity_smooth line 81
  8. lemma OAI.TamingCompatibility.ManifoldVolume.inverseChart_derivative line 91
  9. lemma OAI.TamingCompatibility.ManifoldVolume.chartMetric_derivative line 101
  10. lemma OAI.TamingCompatibility.ManifoldVolume.inverseChart_comp_transition line 110
  11. lemma OAI.TamingCompatibility.ManifoldVolume.chartMetric_transition line 131
  12. lemma OAI.TamingCompatibility.ManifoldVolume.chartDensity_transition line 152
  13. def OAI.TamingCompatibility.ManifoldVolume.chartOverlap line 162
  14. def OAI.TamingCompatibility.ManifoldVolume.transition line 165
  15. lemma OAI.TamingCompatibility.ManifoldVolume.chartOverlap_open line 169
  16. lemma OAI.TamingCompatibility.ManifoldVolume.transition_injOn line 174
  17. lemma OAI.TamingCompatibility.ManifoldVolume.transition_image_overlap line 180
  18. lemma OAI.TamingCompatibility.ManifoldVolume.transition_differentiableAt line 199
  19. lemma OAI.TamingCompatibility.ManifoldVolume.integral_overlap line 211
  20. def OAI.TamingCompatibility.ManifoldVolume.chartWeight line 230
  21. lemma OAI.TamingCompatibility.ManifoldVolume.chartWeight_smooth_compact line 235
  22. lemma OAI.TamingCompatibility.ManifoldVolume.chartWeight_nonneg line 254
  23. def OAI.TamingCompatibility.ManifoldVolume.chartInverse line 262
  24. lemma OAI.TamingCompatibility.ManifoldVolume.chartInverse_measurable line 267
  25. def OAI.TamingCompatibility.ManifoldVolume.chartMeasure line 272
  26. lemma OAI.TamingCompatibility.ManifoldVolume.chartMeasure_finite line 277
  27. def OAI.TamingCompatibility.ManifoldVolume.geometricVolume line 289
  28. lemma OAI.TamingCompatibility.ManifoldVolume.geometricVolume_finite line 293
  29. lemma OAI.TamingCompatibility.ManifoldVolume.integral_chartMeasure line 301