OAI/Analysis/RieszRectifiability/Kernel/IsometricRieszPairing.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Isometric transport of Riesz pairings

Linear isometries intertwine the Riesz kernel and preserve its scalar interior and far-field integrands. Pulling back balls and closed exteriors then transports the corresponding scalar pairing to the lower-dimensional ambient space.

  1. theorem OAI.RieszRectifiability.kernel_linearIsometry line 21
  2. theorem OAI.RieszRectifiability.rieszInteriorIntegrand_linearIsometry line 26
  3. theorem OAI.RieszRectifiability.rieszFarIntegrand_linearIsometry line 33
  4. theorem OAI.RieszRectifiability.linearIsometry_pair_integral line 40
  5. theorem OAI.RieszRectifiability.rieszScalarPairing_linearIsometry line 53