FourierAveragingMeasure.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

An actual Fourier-supported averaging probability

Normalize the positive Fourier-square kernel and instantiate its compact frequency bump. This constructs a probability satisfying FourierGap for every positive gap, rather than assuming existence of an averaging law.

def OAI.LipschitzHilbert.fourierAveragingDensity line 23
def OAI.LipschitzHilbert.fourierAveragingMeasure line 26
theorem OAI.LipschitzHilbert.fourierAveragingDensity_nonneg line 29
theorem OAI.LipschitzHilbert.fourierAveragingDensity_continuous line 33
theorem OAI.LipschitzHilbert.fourierAveragingDensity_integrable line 36
theorem OAI.LipschitzHilbert.fourierAveragingDensity_integral line 39
theorem OAI.LipschitzHilbert.fourierAveragingMeasure_isProbability line 44

theorem OAI.LipschitzHilbert.fourierAveragingMeasure_moment line 54

Source documentation

Fourier moments of the probability are the normalized kernel moments.

theorem fourierAveragingMeasure_moment (h : SchwartzMap ℝ ℂ) (s : ℝ) :
    fourierMoment (fourierAveragingMeasure h) s =
      ((∫ x, fourierSquare h x : ℝ) : ℂ)⁻¹ *
        ∫ t, (fourierSquare h t : ℂ) * character s t := by
…

Mentions: OAI.LipschitzHilbert.fourierAveragingMeasure, OAI.LipschitzHilbert.fourierSquare

theorem OAI.LipschitzHilbert.fourierAveragingMeasure_fourierGap line 72
Source documentation
A bump of radius r gives a probability with the required Fourier gap whenever 16πr ≤ gap.
```
theorem fourierAveragingMeasure_fourierGap (h : SchwartzMap ℝ ℂ) {r gap : ℝ}
    (hsupport : ∀ x, r ≤ |x| → h x = 0) (hband : 16 * Real.pi * r ≤ gap) :
    FourierGap (fourierAveragingMeasure h) gap := by
…
```
Mentions: OAI.LipschitzHilbert.fourierAveragingMeasure
theorem OAI.LipschitzHilbert.exists_compact_frequency_bump line 88
Source documentation
A genuine compactly supported smooth bump for the kernel construction.
```
theorem exists_compact_frequency_bump {r : ℝ} (hr : 0 < r) :
    ∃ h : SchwartzMap ℝ ℂ, h 0 ≠ 0 ∧ ∀ x, r ≤ |x| → h x = 0 := by
…
```
theorem OAI.LipschitzHilbert.exists_fourierAveragingMeasure line 112
Source documentation
Every positive gap admits an explicitly constructed averaging probability with smooth nonnegative density and exactly vanishing outside moments.
```
theorem exists_fourierAveragingMeasure {gap : ℝ} (hgap : 0 < gap) :
    ∃ h : SchwartzMap ℝ ℂ, h 0 ≠ 0 ∧
      IsProbabilityMeasure (fourierAveragingMeasure h) ∧
      FourierGap (fourierAveragingMeasure h) gap := by
…
```
Mentions: OAI.LipschitzHilbert.fourierAveragingMeasure