OAI/Analysis/RieszRectifiability/Kernel/RieszExteriorAdjoint.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Renormalized exterior adjoints

Mean-zero cancellation removes the constant kernel term from the capped transform. The far-kernel difference is integrable against bounded densities and integrable compactly supported tests, so Fubini and kernel antisymmetry give the exterior adjoint identity with its minus sign.

  1. theorem OAI.RieszRectifiability.mean_zero_centered_capped_integral line 22
  2. theorem OAI.RieszRectifiability.density_renormalized_cross_product_integrable line 33
  3. theorem OAI.RieszRectifiability.density_renormalized_exterior_adjoint line 74