OAI/RingTheory/BassTrace/HausdorffArea.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Actual Euclidean Hausdorff area, so slices and lower-dimensional interfaces are measured in the common ambient space, with Mathlib's exact normalization.

  1. lemma OAI.BassTrace.Sparse.euclideanArea_zero_finset line 19
  2. lemma OAI.BassTrace.Sparse.orthogonal_unit_rank line 25
  3. lemma OAI.BassTrace.Sparse.euclideanSliceArea_eq_area line 32
  4. lemma OAI.BassTrace.Sparse.euclidean_area_affine_coarea line 63
  5. lemma OAI.BassTrace.Sparse.euclidean_area_affine_coarea_le line 73
  6. lemma OAI.BassTrace.Sparse.euclidean_area_constant_slices line 84
  7. lemma OAI.BassTrace.Sparse.euclidean_area_gradient_coarea_le line 91
  8. lemma OAI.BassTrace.Sparse.measurable_euclidean_area_slices line 110
  9. lemma OAI.BassTrace.Sparse.euclidean_area_finite_piece_coarea line 141
  10. lemma OAI.BassTrace.Sparse.exists_restricted_gradient line 210
  11. lemma OAI.BassTrace.Sparse.euclidean_area_embedded_coarea line 233
  12. lemma OAI.BassTrace.Sparse.measurable_embedded_slices line 259
  13. lemma OAI.BassTrace.Sparse.euclidean_area_embedded_finite_coarea line 277
  14. lemma OAI.BassTrace.Sparse.extend_subspace_dimension line 340
  15. lemma OAI.BassTrace.Sparse.simplex_in_affine_isometry line 353
  16. lemma OAI.BassTrace.Sparse.simplex_piece_coarea line 381
  17. lemma OAI.BassTrace.Sparse.measurable_simplex_piece_slices line 401
  18. lemma OAI.BassTrace.Sparse.finite_polyhedral_coarea line 421
  19. lemma OAI.BassTrace.Sparse.finite_affine_coarea line 472
  20. lemma OAI.BassTrace.Sparse.finite_max_coarea line 490
  21. lemma OAI.BassTrace.Sparse.measurable_finite_polyhedral_slices line 534
  22. lemma OAI.BassTrace.Sparse.measurable_finite_affine_slices line 570
  23. lemma OAI.BassTrace.Sparse.measurable_finite_max_slices line 586