OAI/Analysis/RieszRectifiability/Kernel/BoundedBoxHeight.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Projection-height control on bounded boxes

Convergence to a coordinate-plane measure, together with local lower mass bounds, forces the restricted measures into arbitrarily thin tubes about the coordinate plane. The height estimate is stated almost everywhere for the bounded projection measures used in boxwise kernel comparisons.

  1. theorem OAI.RieszRectifiability.boundedProjectionFiniteMeasure_height line 23
  2. theorem OAI.RieszRectifiability.eventual_lower_ball_mass_of_AD_lower line 49
  3. theorem OAI.RieszRectifiability.boundedProjectionFiniteMeasure_height_of_AD_lower line 66