OAI/Analysis/RieszRectifiability/Packing/NormalFrameSourceEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Source energy in a normal frame

Convergence of frame centers gives a common bound for their normal coordinates at the origin. Applying the scalar source estimates coordinatewise supplies local L² and fractional pair-energy bounds for normalized normal heights on every fixed ball.

  1. theorem OAI.RieszRectifiability.normalCoordinate_abs_at_zero_le_norm line 22
  2. theorem OAI.RieszRectifiability.normalCoordinates_uniform_center_bound line 29
  3. theorem OAI.RieszRectifiability.normal_frame_source_data_on_ball line 39