OAI/Analysis/RieszRectifiability/Kernel/SupportedExteriorPairing.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Supported exterior pairings

Support in a measurable subset allows the left factor of a product measure to be restricted without changing integrability or the integral. These identities bound the absolute renormalized pairing over a complement by its exterior integral when the original set contains a ball.

  1. theorem OAI.RieszRectifiability.prod_restrict_left_subset line 21
  2. theorem OAI.RieszRectifiability.integrable_prod_iff_of_left_support line 28
  3. theorem OAI.RieszRectifiability.integral_prod_eq_of_left_support line 43
  4. theorem OAI.RieszRectifiability.renormalized_pairing_complement_bound line 58