OAI/Analysis/RieszRectifiability/Kernel/NearPairWeight.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RieszRectifiability.nearPairSet line 12
  2. theorem OAI.RieszRectifiability.nearPairSet_measurable line 15
  3. def OAI.RieszRectifiability.nearPairWeight line 19
  4. theorem OAI.RieszRectifiability.nearPairWeight_measurable line 22
  5. theorem OAI.RieszRectifiability.nearPairWeight_nonneg line 28
  6. theorem OAI.RieszRectifiability.nearPairWeight_section line 32
  7. theorem OAI.RieszRectifiability.nearPairWeight_section_integrable line 43
  8. theorem OAI.RieszRectifiability.nearPairWeight_section_norm_bound line 51
  9. theorem OAI.RieszRectifiability.nearPairWeight_integrable line 59
  10. theorem OAI.RieszRectifiability.nearPairWeight_integral_bound line 72