OAI/Analysis/LipschitzHilbert/Estimates/ProductSlopePrincipalValueBound.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Fatou passage from uniform actual sharp truncations to the pointwise symmetric principal value in product coordinates.

  1. def OAI.LipschitzHilbert.PacketRepresentation.pvInnerRadius line 13
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.pvInnerRadius_pos line 15
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.pvInnerRadius_lt line 19
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.pvInnerRadius_tendsto line 24
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.shortSharp_tendsto_productSlopePrincipalValue line 35
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.productSlopePrincipalValue_measurable line 46
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.productSlopePrincipalValue_eLpNorm_le line 53