HomogeneousFourthMoment.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Homogeneous fourth-moment bounds

The normalized combinatorial fourth-moment estimate is homogeneous of degree three in the ℓ^(4/3) coefficient masses. These lemmas restore the arbitrary coefficient normalization used in §7.

theorem OAI.LipschitzHilbert.PhaseCombinatorics.resonanceSum_smul line 22
theorem OAI.LipschitzHilbert.PhaseCombinatorics.resonanceSum_le_mass_cube line 41
theorem OAI.LipschitzHilbert.PhaseCombinatorics.fourth_moment_le_mass_cube line 75
theorem OAI.LipschitzHilbert.PhaseCombinatorics.resonanceSum_quantile_gap_mass_cube line 84
theorem OAI.LipschitzHilbert.PhaseCombinatorics.fourth_moment_quantile_gap_mass_cube line 115
theorem OAI.LipschitzHilbert.PhaseCombinatorics.fourth_moment_quantile_gap_mass_cube_simplified line 127

theorem OAI.LipschitzHilbert.PhaseCombinatorics.finiteFourier_dominant_bound line 144

Source documentation

Application of the dominant estimate to an actual finite Fourier remainder. The two coefficient inequalities are supplied by the exponent-comparison step.

theorem finiteFourier_dominant_bound (ν : Measure ℝ) [IsProbabilityMeasure ν]
    (frequency : ι → ℝ) (a : ι → ℂ) {gap b r : ℝ}
    (hgap : 0 < gap) (hsep : Separated frequency gap) (hν : FourierGap ν gap)
    (hzero : ∀ i, gap / 4 ≤ |frequency i|)
    (hb : 0 ≤ b) (hsmall : b ≤ 1 / 64) (hr : 0 < r) (hrupper : r ≤ 3 / 2)
    (hsecond : ∑ i, ‖a i‖ ^ 2 ≤ b ^ 2)
    (hfourth : (∑ i, coefficientMass a i) ^ 3 ≤ 2 * b ^ 4) :
    (∫ t, ‖1 + finiteFourierSum frequency a t‖ ^ 4 ∂ν) ≤
      (1 + b ^ r) ^ (4 / r) := by
…

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