OAI/Analysis/RieszRectifiability/Kernel/RegionOscillation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Oscillation bounds on localized regions

Lipschitz height functions give integrable far pairings on regions containing a ball. Localization identifies each such height pairing with the scalar Riesz pairing, transferring its oscillation estimate to the normalized height.

  1. theorem OAI.RieszRectifiability.region_far_integrable_of_lipschitz_height line 23
  2. theorem OAI.RieszRectifiability.heightPairingOn_region_eq_riesz line 39
  3. theorem OAI.RieszRectifiability.normalized_region_pairing_oscillation_bound line 97