OAI/Analysis/LipschitzHilbert/Packets/TopWeightedPacket.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Both factors of a fixed top polynomial can be absorbed into the original packet orders, uniformly in the horizontal reference line.

  1. def OAI.LipschitzHilbert.topWeightedWave line 15
  2. theorem OAI.LipschitzHilbert.topWeightedWave_apply line 18
  3. theorem OAI.LipschitzHilbert.topWeightedWave_bound line 25
  4. theorem OAI.LipschitzHilbert.topWeightedWave_derivative_bound line 48
  5. theorem OAI.LipschitzHilbert.packetSynthesis_topWeighted line 79
  6. theorem OAI.LipschitzHilbert.partialBandSum_topWeighted line 90
  7. theorem OAI.LipschitzHilbert.hilbertPartialBandSum_topWeighted line 102
  8. theorem OAI.LipschitzHilbert.topWeightedWave_low line 111
  9. theorem OAI.LipschitzHilbert.topWeightedWave_high line 121