OAI/Analysis/LipschitzHilbert/Fourier/FourierHomogeneity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Restoring arbitrary coefficients after a unit sequence-norm estimate.

  1. def OAI.LipschitzHilbert.PhaseCombinatorics.normalizedCoefficient line 16
  2. theorem OAI.LipschitzHilbert.PhaseCombinatorics.sequenceNorm_pos_of_nonzero line 19
  3. theorem OAI.LipschitzHilbert.PhaseCombinatorics.normalizedCoefficient_unit line 28
  4. theorem OAI.LipschitzHilbert.PhaseCombinatorics.finiteFourierSum_normalized line 40
  5. theorem OAI.LipschitzHilbert.PhaseCombinatorics.restore_normalized_fourier_norm line 49
  6. theorem OAI.LipschitzHilbert.PhaseCombinatorics.homogeneous_fourier_power_bound line 58