OAI/Analysis/LipschitzHilbert/Fourier/PolynomialLineFamily.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Apply a common horizontal top weight to actual line packets. The coefficient budget is unchanged, and the packet order is fixed by the weight degree, independently of the moment order.

  1. def OAI.LipschitzHilbert.LinePacketFamily.localizationConstant line 18
  2. theorem OAI.LipschitzHilbert.LinePacketFamily.localizationConstant_pos line 21
  3. theorem OAI.LipschitzHilbert.LinePacketFamily.localizationConstant_ge line 26
  4. theorem OAI.LipschitzHilbert.LinePacketFamily.localized_wave_bound line 35
  5. theorem OAI.LipschitzHilbert.LinePacketFamily.localized_derivative_bound line 57
  6. def OAI.LipschitzHilbert.LinePacketFamily.localized line 82
  7. theorem OAI.LipschitzHilbert.LinePacketFamily.localized_budget line 95
  8. theorem OAI.LipschitzHilbert.LinePacketFamily.localized_packets line 99
  9. theorem OAI.LipschitzHilbert.LinePacketFamily.cubicVariation_smul_nonneg line 113
  10. theorem OAI.LipschitzHilbert.LinePacketFamily.localized_variation line 122