OAI/Analysis/RieszRectifiability/Rigidity/LocalReflectionlessTransform.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Local constancy from reflectionlessness

A renormalized local transform annihilates mean-zero Lipschitz tests under reflectionlessness. A normalized ball bump and local L² integrability then identify the transform with a constant almost everywhere on the inner ball.

  1. theorem OAI.RieszRectifiability.local_transform_constant_of_reflectionless line 23
  2. theorem OAI.RieszRectifiability.exists_local_constant_transform_of_source_L2 line 55