OAI/Analysis/IntegralMeans/AreaTransport.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Brennan.fiberSum line 21
  2. lemma OAI.Brennan.BorelBranches.fiberSum_eq line 24
  3. lemma OAI.Brennan.BorelBranches.measurable_fiberSum line 53
  4. lemma OAI.Brennan.weighted_area_formula_regular line 60
  5. lemma OAI.Brennan.fiberSum_mono_injective line 93
  6. lemma OAI.Brennan.contDiffAt_criticalMap line 106
  7. lemma OAI.Brennan.measurableSet_halfPlane_pred line 114
  8. def OAI.Brennan.jacobianRegion line 123
  9. lemma OAI.Brennan.measurableSet_jacobianRegion line 126
  10. lemma OAI.Brennan.jacobianRegion_regular line 133
  11. def OAI.Brennan.transportDensity line 141
  12. def OAI.Brennan.targetDensity line 144
  13. lemma OAI.Brennan.measurable_targetDensity line 149
  14. lemma OAI.Brennan.transportDensity_jacobian line 161
  15. lemma OAI.Brennan.transport_area line 180
  16. lemma OAI.Brennan.targetDensity_eq_height line 211
  17. lemma OAI.Brennan.targetDensity_le_pair line 219