OAI/Analysis/RieszRectifiability/Rigidity/FiniteFractionalHeightPairing.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Symmetrization of finite fractional height pairings

The distance cutoff defines a measurable, bounded kernel invariant under swapping its two variables. Applying the symmetric height-kernel identity and rewriting the cutoff as an indicator identifies the bilinear pairing with an iterated integral over the closed exterior region.

  1. def OAI.RieszRectifiability.symmetricFractionalCutoffKernel line 21
  2. theorem OAI.RieszRectifiability.symmetricFractionalCutoffKernel_measurable line 25
  3. theorem OAI.RieszRectifiability.symmetricFractionalCutoffKernel_bound line 32
  4. theorem OAI.RieszRectifiability.symmetricFractionalCutoffKernel_swap line 42
  5. theorem OAI.RieszRectifiability.finite_fractional_height_pairing_symmetrization line 47