OAI/Analysis/LipschitzHilbert/Estimates/ConditionalSlopePrincipalValue.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The full principal-value bound for small bounded slope fields follows from the proved global band theorem and the precise published reduction.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.sharpBandOperator_add_profile line 13
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.global_narrow_band_operator_norm line 27
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.conditional_slope_principalValue line 41