OAI/Analysis/RieszRectifiability/Kernel/HeightPairingRegions.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Regional height pairings

The height pairing on a set combines the symmetric interior fractional bilinear integral with a renormalized cross-region term. For affine normal heights and mean-zero tests on a ball, cancellation of the far contribution identifies this regional expression with the scalar Riesz pairing.

  1. def OAI.RieszRectifiability.heightRawCrossIntegrand line 21
  2. def OAI.RieszRectifiability.heightPairingOn line 25
  3. theorem OAI.RieszRectifiability.fractionalBilinear_swap line 31
  4. theorem OAI.RieszRectifiability.height_pairing_split line 39
  5. theorem OAI.RieszRectifiability.height_far_integral_eq_raw_of_mean_zero line 67
  6. theorem OAI.RieszRectifiability.finite_height_pairing_eq_renormalized line 86
  7. theorem OAI.RieszRectifiability.heightPairingOn_height_div line 102
  8. theorem OAI.RieszRectifiability.heightPairingOn_ball_eq_rieszScalarPairing line 119