OAI/Analysis/RieszRectifiability/Kernel/VectorNormalizedEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The normal cutoff pairing is identified with a Riesz scalar pairing for a centered Lipschitz height test, using local L² integrability and cutoff support control.

  1. theorem OAI.RieszRectifiability.normalCutoffPairing_eq_riesz_of_lipschitz line 19
  2. theorem OAI.RieszRectifiability.normalized_energy_from_vector_pairing line 49