OAI/Analysis/LipschitzHilbert/Packets/TopCovariantPacket.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The scaled covariant derivative of a top-weighted packet is another Schwartz packet. Its extra scalar factor is bounded by 8q independently of the top size and the vertical carrier frequency.

  1. def OAI.LipschitzHilbert.topCovariantFactor line 14
  2. theorem OAI.LipschitzHilbert.topCovariantFactor_bound line 17
  3. def OAI.LipschitzHilbert.topCovariantWave line 30
  4. theorem OAI.LipschitzHilbert.topCovariantWave_bound line 35
  5. theorem OAI.LipschitzHilbert.topCovariantWave_derivative_bound line 59
  6. theorem OAI.LipschitzHilbert.topWeightedWave_covariant line 92
  7. theorem OAI.LipschitzHilbert.topCovariantWave_low line 125
  8. theorem OAI.LipschitzHilbert.topCovariantWave_high line 143