OAI/Analysis/RieszRectifiability/Limits/BoundedBoxConvergence.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Compact-test convergence to a coordinate-plane measure yields weak convergence of finite measures on bounded projection regions, using compact closures and null frontiers.

  1. theorem OAI.RieszRectifiability.boundedProjectionFiniteMeasure_tendsto line 19
  2. theorem OAI.RieszRectifiability.coordinatePlaneMeasure_ae_section line 40
  3. theorem OAI.RieszRectifiability.projectionHeight_lipschitz line 48