OAI/Analysis/RieszRectifiability/Rigidity/LimitReflectionlessness.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Reflectionlessness of limits with vanishing oscillation

The scalar Riesz pairing scales linearly in its direction. This extends the normalized-direction limit test to arbitrary directions and yields scalar reflectionlessness when compact-test convergence and vanishing oscillation hold.

  1. theorem OAI.RieszRectifiability.rieszScalarPairing_smul_direction line 22
  2. theorem OAI.RieszRectifiability.limit_scalarReflectionlessAt_of_oscillation line 40
  3. theorem OAI.RieszRectifiability.ScalarReflectionlessAt.change_center line 112