OAI/Analysis/LipschitzHilbert/Phase/DominantNormalization.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Exact removal of a dominant Fourier carrier in §7.

  1. abbrev OAI.LipschitzHilbert.PhaseCombinatorics.RemainderIndex line 19
  2. def OAI.LipschitzHilbert.PhaseCombinatorics.remainderFrequency line 21
  3. def OAI.LipschitzHilbert.PhaseCombinatorics.remainderCoefficient line 24
  4. theorem OAI.LipschitzHilbert.PhaseCombinatorics.remove_carrier_identity line 27
  5. theorem OAI.LipschitzHilbert.PhaseCombinatorics.remainderFrequency_separated line 48
  6. theorem OAI.LipschitzHilbert.PhaseCombinatorics.remainderFrequency_away_zero line 57
  7. theorem OAI.LipschitzHilbert.PhaseCombinatorics.remainder_coefficientMass line 63
  8. theorem OAI.LipschitzHilbert.PhaseCombinatorics.sum_remainder_coefficientMass line 68
  9. theorem OAI.LipschitzHilbert.PhaseCombinatorics.sum_norm_remainder_rpow line 78
  10. theorem OAI.LipschitzHilbert.PhaseCombinatorics.coefficient_norm_power_decomposition line 88
  11. theorem OAI.LipschitzHilbert.PhaseCombinatorics.restore_coefficient_fourth_power line 97
  12. theorem OAI.LipschitzHilbert.PhaseCombinatorics.dominant_coefficient_ne_zero line 108
  13. theorem OAI.LipschitzHilbert.PhaseCombinatorics.dominant_remainder_mass_le line 119
  14. theorem OAI.LipschitzHilbert.PhaseCombinatorics.remove_carrier_norm line 130
  15. theorem OAI.LipschitzHilbert.PhaseCombinatorics.remove_carrier_fourth_moment line 136