OAI/Analysis/RieszRectifiability/Foundations/GlobalLowerDiameter.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A nonzero measure finite on compact sets cannot have bounded support if a positive-dimensional lower growth bound holds at every positive radius: bounded support would force finite total mass.

  1. theorem OAI.RieszRectifiability.global_lower_growth_support_ediam_top line 18