OAI/RingTheory/BassTrace/AffineCoarea.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Affine coarea from product measure and one-dimensional Lebesgue scaling. The transverse measure may be s-finite; orthonormal coordinates specialize this to affine polyhedral area.

  1. lemma OAI.BassTrace.Sparse.lintegral_affine_change line 14
  2. def OAI.BassTrace.Sparse.productSlice line 31
  3. lemma OAI.BassTrace.Sparse.measurable_productSlice line 34
  4. lemma OAI.BassTrace.Sparse.affine_product_coarea line 38
  5. lemma OAI.BassTrace.Sparse.affine_product_coarea_le line 67
  6. def OAI.BassTrace.Sparse.normalParamIsometry line 88
  7. lemma OAI.BassTrace.Sparse.normalParamIsometry_apply line 96
  8. lemma OAI.BassTrace.Sparse.normalParam_measurePreserving line 101
  9. lemma OAI.BassTrace.Sparse.inner_normalParam line 109
  10. def OAI.BassTrace.Sparse.euclideanSliceArea line 116
  11. lemma OAI.BassTrace.Sparse.euclidean_affine_coarea line 119
  12. lemma OAI.BassTrace.Sparse.euclidean_affine_coarea_le line 143