OAI/Analysis/RieszRectifiability/Foundations/SourceDensityConstant.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Constant planar densities

An almost-everywhere constant density pushes forward under a linear isometry to a scalar multiple of planar volume. The compact fractional equation and bounded-density rigidity identify this constant for reflectionless weak limits, retaining its positive lower and finite upper bounds.

  1. theorem OAI.RieszRectifiability.ae_constant_planar_density_measure line 22
  2. theorem OAI.RieszRectifiability.source_planar_density_ae_constant line 33