OAI/Analysis/FourierExtension/LocalizedFourier.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Uniform Fourier decay and localized Taylor amplitudes.

  1. theorem OAI.DiagonalExtension.UniformFourierDecay.weighted_fourier_bound line 19
  2. lemma OAI.DiagonalExtension.UniformFourierDecay.iteratedFDeriv_section line 61
  3. lemma OAI.DiagonalExtension.UniformFourierDecay.continuous_section_derivative line 80
  4. theorem OAI.DiagonalExtension.UniformFourierDecay.compact_uniform_decay line 89
  5. def OAI.DiagonalExtension.SmoothCompactIntegral.paramDeriv line 137
  6. lemma OAI.DiagonalExtension.SmoothCompactIntegral.smooth_partial line 140
  7. lemma OAI.DiagonalExtension.SmoothCompactIntegral.partial_hasFDerivAt line 144
  8. lemma OAI.DiagonalExtension.SmoothCompactIntegral.hasFDerivAt_integral line 153
  9. lemma OAI.DiagonalExtension.SmoothCompactIntegral.smooth_integral_nat line 173
  10. theorem OAI.DiagonalExtension.SmoothCompactIntegral.contDiff_integral line 189
  11. def OAI.DiagonalExtension.PacketTaylor.remainder line 201
  12. lemma OAI.DiagonalExtension.PacketTaylor.smooth_remainder line 205
  13. lemma OAI.DiagonalExtension.PacketTaylor.taylor_identity line 221
  14. abbrev OAI.DiagonalExtension.PacketTaylor.Param line 239
  15. def OAI.DiagonalExtension.PacketTaylor.amplitude line 241
  16. lemma OAI.DiagonalExtension.PacketTaylor.smooth_amplitude line 245
  17. theorem OAI.DiagonalExtension.PacketTaylor.normalized_locality line 260