OAI/Analysis/LipschitzHilbert/Phase/ImprovedFourthMoment.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The improved fourth moment: assembly of the quantitative gap and the dominant-coefficient alternative from §7.

  1. def OAI.LipschitzHilbert.PhaseCombinatorics.phaseParameter line 20
  2. def OAI.LipschitzHilbert.PhaseCombinatorics.fourthExponent line 22
  3. theorem OAI.LipschitzHilbert.PhaseCombinatorics.nondominant_fourth_moment_bound line 24
  4. theorem OAI.LipschitzHilbert.PhaseCombinatorics.mass_cube_le_two_sequenceNorm_fourth line 51
  5. theorem OAI.LipschitzHilbert.PhaseCombinatorics.small_remainder_fourth_moment_bound line 69
  6. theorem OAI.LipschitzHilbert.PhaseCombinatorics.finite_fourth_moment_gain line 96

    Source documentation

    The constant-one fourth-moment estimate with the improved coefficient exponent, for arbitrary complex coefficients. This is the p = 4 endpoint of the manuscript's finite Fourier gain proposition.

    theorem finite_fourth_moment_gain (ν : Measure ℝ) [IsProbabilityMeasure ν]
    (frequency : ι → ℝ) (a : ι → ℂ) {gap D : ℝ}
    (hgap : 0 < gap) (hsep : Separated frequency gap) (hν : FourierGap ν gap)
    (hD : 1 ≤ D) (hcard : (Fintype.card ι : ℝ) ≤ D) :
    (∫ t, ‖finiteFourierSum frequency a t‖ ^ 4 ∂ν) ≤
      (∑ i, ‖a i‖ ^ fourthExponent D) ^ (4 / fourthExponent D) := by
…

    Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.Separated, OAI.LipschitzHilbert.PhaseCombinatorics.FourierGap, OAI.LipschitzHilbert.PhaseCombinatorics.finiteFourierSum, OAI.LipschitzHilbert.PhaseCombinatorics.fourthExponent

  7. theorem OAI.LipschitzHilbert.PhaseCombinatorics.finite_fourier_l4_gain line 131