OAI/Analysis/RieszRectifiability/Flatness/BoundedAffineConstant.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded affine functions are constant

A nonzero linear part grows along a suitable ray, contradicting any global bound on its affine translate. Density of volume-almost-everywhere sets extends an almost-everywhere affine bound to every point, so a bounded function that is almost everywhere affine is almost everywhere constant.

  1. theorem OAI.RieszRectifiability.bounded_affine_linear_part_zero line 21
  2. theorem OAI.RieszRectifiability.ae_bounded_affine_is_constant line 35