OAI/Analysis/RieszRectifiability/Kernel/CutoffEnergyIntegral.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Integral estimates for cutoff energies

Bounded multipliers preserve the square-integrability needed for cutoff estimates. An almost-everywhere diameter bound makes the near-pair error estimate global, while the fractional energy identity separates the bilinear contribution from the cutoff error.

  1. theorem OAI.RieszRectifiability.bounded_multiplier_memLp line 22
  2. theorem OAI.RieszRectifiability.cutoffError_integrable_and_bound_of_ae_diameter line 31
  3. theorem OAI.RieszRectifiability.cutoff_fractionalEnergy_identity line 45
  4. theorem OAI.RieszRectifiability.truncated_cutoff_integral_identity line 53
  5. theorem OAI.RieszRectifiability.cutoff_energy_from_interior_pairing_bound line 85
  6. theorem OAI.RieszRectifiability.cutoff_energy_from_integrable_interior_pairing line 115