OAI/Analysis/LipschitzHilbert/Estimates/ProductSlopePVTruncation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A finite sharp truncation is the difference of two actual principal values; the identity is proved using the continuous symmetric quotient.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.symmetric_regularized_continuous line 11
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.productSymmetricTruncation_eq_pv_sub line 26
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.shortSharp_eq_pv_sub line 48