OAI/Analysis/LipschitzHilbert/Estimates/WeakTwoIntegral.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The restricted L1 estimate needed for mask removal, derived from an actual weak (2,2) distribution estimate by layer cake.

  1. theorem OAI.LipschitzHilbert.lintegral_inverse_square_tail line 15
  2. theorem OAI.LipschitzHilbert.weak_two_lintegral_split line 31
  3. theorem OAI.LipschitzHilbert.weak_two_lintegral line 49