OAI/Analysis/LipschitzHilbert/Packets/LinePacketReplacement.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Replacement synthesis waves retain the already proved analyzing coefficient budget. This is used for polynomially weighted sums and their demodulated vertical derivatives.

  1. def OAI.LipschitzHilbert.LinePacketFamily.replaceWaves line 18
  2. theorem OAI.LipschitzHilbert.LinePacketFamily.replaceWaves_budget line 33