OAI/Analysis/RieszRectifiability/Foundations/BoundedPlanarDensity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Bounded densities for measures supported on planes

Domination by a scalar multiple of a reference measure bounds the Radon–Nikodym derivative and gives a measurable, everywhere bounded density. Intrinsic upper growth applies this construction to Euclidean volume and to measures supported on the range of a linear isometry.

  1. theorem OAI.RieszRectifiability.rnDeriv_le_of_nnreal_domination line 22
  2. theorem OAI.RieszRectifiability.exists_bounded_density_of_domination line 30
  3. theorem OAI.RieszRectifiability.exists_bounded_intrinsic_density line 49
  4. theorem OAI.RieszRectifiability.exists_bounded_planar_density line 58