OAI/Analysis/LipschitzHilbert/Phase/DominantCoefficient.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The dominant-coefficient case of the finite phase estimate

These are the mean-zero fourth-moment and elementary exponent estimates in §7, proof of Proposition phase:finite-fourier. A quadratic Young inequality absorbs the cubic cross term before integration.

  1. theorem OAI.LipschitzHilbert.PhaseCombinatorics.finiteFourierSum_bound line 23
  2. theorem OAI.LipschitzHilbert.PhaseCombinatorics.continuous_finiteFourierSum line 31
  3. theorem OAI.LipschitzHilbert.PhaseCombinatorics.integral_finiteFourierSum line 36
  4. theorem OAI.LipschitzHilbert.PhaseCombinatorics.integral_finiteFourierSum_eq_zero line 48
  5. theorem OAI.LipschitzHilbert.PhaseCombinatorics.finiteFourierSum_second_expansion line 57
  6. theorem OAI.LipschitzHilbert.PhaseCombinatorics.integral_finiteFourierSum_second line 75
  7. theorem OAI.LipschitzHilbert.PhaseCombinatorics.one_add_norm_fourth_le line 108
  8. theorem OAI.LipschitzHilbert.PhaseCombinatorics.bounded_norm_power_integrable line 128
  9. theorem OAI.LipschitzHilbert.PhaseCombinatorics.bounded_one_add_fourth_integrable line 139
  10. theorem OAI.LipschitzHilbert.PhaseCombinatorics.mean_zero_fourth_moment_le line 154
  11. theorem OAI.LipschitzHilbert.PhaseCombinatorics.dominant_exponent_bound line 194
  12. theorem OAI.LipschitzHilbert.PhaseCombinatorics.dominant_fourth_moment_bound line 223