FourthMoment.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

Fourth moments of separated finite Fourier sums

The exact finite expansion and Fourier-support reduction used in §7, proof of Proposition phase:finite-fourier. The annihilation hypothesis is a property of the averaging probability measure, not a new axiom.

def OAI.LipschitzHilbert.PhaseCombinatorics.character line 27
theorem OAI.LipschitzHilbert.PhaseCombinatorics.norm_character line 29
theorem OAI.LipschitzHilbert.PhaseCombinatorics.character_mul line 32
theorem OAI.LipschitzHilbert.PhaseCombinatorics.character_conj line 39
theorem OAI.LipschitzHilbert.PhaseCombinatorics.character_four line 45
theorem OAI.LipschitzHilbert.PhaseCombinatorics.continuous_character line 51
theorem OAI.LipschitzHilbert.PhaseCombinatorics.integrable_character line 55
def OAI.LipschitzHilbert.PhaseCombinatorics.finiteFourierSum line 60
theorem OAI.LipschitzHilbert.PhaseCombinatorics.sum_four_product line 63
theorem OAI.LipschitzHilbert.PhaseCombinatorics.norm_fourth_as_product line 77
theorem OAI.LipschitzHilbert.PhaseCombinatorics.fourth_power_sum_expansion line 86
def OAI.LipschitzHilbert.PhaseCombinatorics.coefficientProduct line 95
def OAI.LipschitzHilbert.PhaseCombinatorics.frequencyDifference line 98
theorem OAI.LipschitzHilbert.PhaseCombinatorics.finiteFourierSum_fourth_expansion line 102
Source documentation
Exact fourth-power expansion with all cross terms retained.
```
theorem finiteFourierSum_fourth_expansion (frequency : ι → ℝ) (a : ι → ℂ) (t : ℝ) :
    ((‖finiteFourierSum frequency a t‖ ^ 4 : ℝ) : ℂ) =
      ∑ q : Quadruple ι, coefficientProduct a q * character (frequencyDifference frequency q) t := by
…
```
Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.finiteFourierSum, OAI.LipschitzHilbert.PhaseCombinatorics.Quadruple, OAI.LipschitzHilbert.PhaseCombinatorics.coefficientProduct, OAI.LipschitzHilbert.PhaseCombinatorics.character, OAI.LipschitzHilbert.PhaseCombinatorics.frequencyDifference
theorem OAI.LipschitzHilbert.PhaseCombinatorics.integrable_fourth_power line 118
def OAI.LipschitzHilbert.PhaseCombinatorics.fourierMoment line 128
theorem OAI.LipschitzHilbert.PhaseCombinatorics.norm_fourierMoment_le_one line 130
theorem OAI.LipschitzHilbert.PhaseCombinatorics.integral_fourth_expansion line 137
Source documentation
The integral of the finite expansion is the finite sum of Fourier moments.
```
theorem integral_fourth_expansion (ν : Measure ℝ) [IsFiniteMeasure ν]
    (frequency : ι → ℝ) (a : ι → ℂ) :
    (∫ t, ((‖finiteFourierSum frequency a t‖ ^ 4 : ℝ) : ℂ) ∂ν) =
      ∑ q : Quadruple ι, coefficientProduct a q * fourierMoment ν (frequencyDifference frequency q) := by
…
```
Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.finiteFourierSum, OAI.LipschitzHilbert.PhaseCombinatorics.Quadruple, OAI.LipschitzHilbert.PhaseCombinatorics.coefficientProduct, OAI.LipschitzHilbert.PhaseCombinatorics.fourierMoment, OAI.LipschitzHilbert.PhaseCombinatorics.frequencyDifference
def OAI.LipschitzHilbert.PhaseCombinatorics.FourierGap line 151
Source documentation
A measure with Fourier support in the open interval (-gap/4,gap/4) annihilates all the moments specified in this condition.
```
def FourierGap (ν : Measure ℝ) (gap : ℝ) : Prop :=
…
```
theorem OAI.LipschitzHilbert.PhaseCombinatorics.fourth_moment_le_resonant_sum line 154
theorem OAI.LipschitzHilbert.PhaseCombinatorics.norm_product_eq_weight_rpow line 188
theorem OAI.LipschitzHilbert.PhaseCombinatorics.fourth_moment_le_resonanceSum line 197
def OAI.LipschitzHilbert.PhaseCombinatorics.coefficientMass line 211
theorem OAI.LipschitzHilbert.PhaseCombinatorics.coefficientMass_nonneg line 214
theorem OAI.LipschitzHilbert.PhaseCombinatorics.coefficientMass_rpow line 218
theorem OAI.LipschitzHilbert.PhaseCombinatorics.normalized_fourth_moment_le_one line 225
Source documentation
The ordinary constant-one fourth-moment estimate at unit ℓ^(4/3) norm.
```
theorem normalized_fourth_moment_le_one (ν : Measure ℝ) [IsProbabilityMeasure ν]
    (frequency : ι → ℝ) (a : ι → ℂ) {gap : ℝ}
    (hgap : 0 < gap) (hsep : Separated frequency gap) (hν : FourierGap ν gap)
    (hunit : ∑ i, coefficientMass a i = 1) :
    (∫ t, ‖finiteFourierSum frequency a t‖ ^ 4 ∂ν) ≤ 1 :=
…
```
Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.Separated, OAI.LipschitzHilbert.PhaseCombinatorics.FourierGap, OAI.LipschitzHilbert.PhaseCombinatorics.coefficientMass, OAI.LipschitzHilbert.PhaseCombinatorics.finiteFourierSum

theorem OAI.LipschitzHilbert.PhaseCombinatorics.normalized_fourth_moment_quantile_gap line 236

Source documentation

The strict quantitative fourth-moment gap when no coefficient carries almost all of the normalized ℓ^(4/3) mass.

theorem normalized_fourth_moment_quantile_gap (ν : Measure ℝ) [IsProbabilityMeasure ν]
    (frequency : ι → ℝ) (a : ι → ℂ) {gap κ : ℝ}
    (hgap : 0 < gap) (hsep : Separated frequency gap) (hν : FourierGap ν gap)
    (hκ : 0 < κ) (hκ1 : κ < 1)
    (hunit : ∑ i, coefficientMass a i = 1)
    (hatom : ∀ i, coefficientMass a i ≤ 1 - κ) :
    (∫ t, ‖finiteFourierSum frequency a t‖ ^ 4 ∂ν) ≤
      1 - κ ^ 4 * (1 - κ / 2) ^ 2 / 4096 :=
…

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

theorem OAI.LipschitzHilbert.PhaseCombinatorics.normalized_fourth_moment_quantile_gap_simplified line 249