FiniteFourierGain.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The scalar finite Fourier gain for every real exponent p ≥ 4.

theorem OAI.LipschitzHilbert.PhaseCombinatorics.normalized_finite_fourier_power_gain line 18
theorem OAI.LipschitzHilbert.PhaseCombinatorics.finite_fourier_power_gain line 31
theorem OAI.LipschitzHilbert.PhaseCombinatorics.finite_fourier_gain line 44
Source documentation
The scalar form of Proposition phase:finite-fourier, with its exact constant one and its logarithmic improvement in the coefficient exponent.
```
theorem finite_fourier_gain (ν : Measure ℝ) [IsProbabilityMeasure ν]
    (frequency : ι → ℝ) (a : ι → ℂ) {gap D p : ℝ}
    (hgap : 0 < gap) (hsep : Separated frequency gap) (hν : FourierGap ν gap)
    (hD : 1 ≤ D) (hcard : (Fintype.card ι : ℝ) ≤ D) (hp : 4 ≤ p) :
    (∫ t, ‖finiteFourierSum frequency a t‖ ^ p ∂ν) ^ (1 / p) ≤
      sequenceNorm a (fourierInterpolationExponent D p) := by
…
```
Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.Separated, OAI.LipschitzHilbert.PhaseCombinatorics.FourierGap, OAI.LipschitzHilbert.PhaseCombinatorics.finiteFourierSum, OAI.LipschitzHilbert.PhaseCombinatorics.sequenceNorm, OAI.LipschitzHilbert.PhaseCombinatorics.fourierInterpolationExponent