OAI/Analysis/LipschitzHilbert/Estimates/LocalizedEnvelope.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Local line integrals of a packet envelope, retaining both center-box offsets. This is the positive estimate for the square-function argument.

  1. theorem OAI.LipschitzHilbert.local_lineEnvelope_weighted line 13
  2. theorem OAI.LipschitzHilbert.local_tileEnvelope line 41