FourierAveragingMixture.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Near-uniform Fourier-supported averaging

The averaging probability in §9 is the convolution of the uniform law on an expanded interval with a dilated, fixed Fourier-square probability. Its explicit loss is expansion/length plus a second-moment tail.

theorem OAI.LipschitzHilbert.interval_convolution_minorization line 23
theorem OAI.LipschitzHilbert.expansion_tail_loss line 45

theorem OAI.LipschitzHilbert.interval_fourier_mixture line 65

Source documentation

Explicit near-uniform probability and exact remainder. The only input about the base kernel is its proved probability, Fourier gap, and moment.

theorem interval_fourier_mixture (μ : Measure ℝ) [IsProbabilityMeasure μ]
    (hmoment : Integrable (fun t : ℝ => t ^ 2) μ)
    {a b pad scale gap : ℝ} (hab : a < b) (hpad : 0 < pad) (hscale : 0 < scale)
    (hgap : FourierGap μ gap)
    (hsmall : 2 * pad / (b - a) +
      scale ^ 2 * (∫ t : ℝ, t ^ 2 ∂μ) / pad ^ 2 < 1) :
    let η := 2 * pad / (b - a) + scale ^ 2 * (∫ t : ℝ, t ^ 2 ∂μ) / pad ^ 2
…

theorem OAI.LipschitzHilbert.exists_fixed_fourier_averaging_kernel line 101
Source documentation
A fixed actual Schwartz-square kernel suffices for all interval lengths and dilation parameters. Its second moment is a single finite constant.
```
theorem exists_fixed_fourier_averaging_kernel :
    ∃ μ : Measure ℝ, IsProbabilityMeasure μ ∧ FourierGap μ 1 ∧
      Integrable (fun t : ℝ => t ^ 2) μ := by
…
```