OAI/Analysis/LipschitzHilbert/Estimates/SmoothPrincipalValueBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform truncation bounds pass to the symmetric principal value. Fatou's lemma yields the strong bound, and Chebyshev's inequality gives its weak (2,2) consequence.

  1. theorem OAI.LipschitzHilbert.smoothPrincipalValue_eLpNorm_le line 16
  2. theorem OAI.LipschitzHilbert.smoothPrincipalValue_memLp line 44
  3. theorem OAI.LipschitzHilbert.smoothPrincipalValue_weak_two line 53