OAI/Analysis/StrictMeans/AreaTransport.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictInverseFirstPower.chart_measurable_fiberSum line 11
  2. lemma OAI.StrictInverseFirstPower.chart_area_formula line 28
  3. lemma OAI.StrictInverseFirstPower.regular_area_formula line 50
  4. def OAI.StrictInverseFirstPower.unsignedTargetWeight line 105
  5. def OAI.StrictInverseFirstPower.jacobianPart line 108
  6. def OAI.StrictInverseFirstPower.sourceMassDensity line 112
  7. def OAI.StrictInverseFirstPower.signedJacobianLocus line 116
  8. lemma OAI.StrictInverseFirstPower.continuous_unsignedTargetWeight line 120
  9. lemma OAI.StrictInverseFirstPower.continuous_jacobianPart line 125
  10. lemma OAI.StrictInverseFirstPower.continuous_sourceMassDensity line 131
  11. lemma OAI.StrictInverseFirstPower.measurableSet_signedJacobianLocus line 137
  12. lemma OAI.StrictInverseFirstPower.criticalMap_det_eq line 162
  13. lemma OAI.StrictInverseFirstPower.sourceMassDensity_eq_targetWeight_det line 171
  14. lemma OAI.StrictInverseFirstPower.sourceMassDensity_zero_of_not_sign line 191
  15. lemma OAI.StrictInverseFirstPower.source_area_formula line 206