FourierAveragingConvolution.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Convolution and the exact averaging mixture

Convolution preserves the proved Fourier gap. A central mass of the kernel minorizes the uniform law on a smaller interval. The remaining measure is normalized into the probability used in the prediction-mixture argument.

theorem OAI.LipschitzHilbert.fourierMoment_eq_charFun line 25
theorem OAI.LipschitzHilbert.fourierGap_conv_left line 31
theorem OAI.LipschitzHilbert.convolution_apply_as_translations line 37

theorem OAI.LipschitzHilbert.convolution_minorization line 53

Source documentation

Only a central part of the convolution law is needed for minorization.

theorem convolution_minorization (μ ν ω : Measure ℝ) [SFinite μ] [SFinite ν]
    {S : Set ℝ} (hS : MeasurableSet S) {c : ℝ≥0∞}
    (hshift : ∀ y ∈ S, c • ω ≤ μ.map (fun x => x + y)) :
    (ν S * c) • ω ≤ μ ∗ ν := by
…

def OAI.LipschitzHilbert.intervalProbability line 73
Source documentation
The normalized Lebesgue law on a closed interval. Endpoints have zero mass.
```
def intervalProbability (a b : ℝ) : Measure ℝ :=
…
```
theorem OAI.LipschitzHilbert.intervalProbability_isProbability line 76
theorem OAI.LipschitzHilbert.interval_restrict_le_translated line 84

theorem OAI.LipschitzHilbert.intervalProbability_le_translated line 102

Source documentation

Dividing the smaller and larger interval lengths gives the precise minorization constant for each shift in the central kernel window.

theorem intervalProbability_le_translated {a b pad y : ℝ} (hab : a < b)
    (hpad : 0 ≤ pad) (hy : |y| ≤ pad) :
    (ENNReal.ofReal ((b - a) / (b - a + 2 * pad))) • intervalProbability a b ≤
      (intervalProbability (a - pad) (b + pad)).map (fun x => x + y) := by
…

Mentions: OAI.LipschitzHilbert.intervalProbability

theorem OAI.LipschitzHilbert.probability_mixture_of_minorization line 125

Source documentation

The averaging law is an exact probability mixture once its uniform part has been minorized. This introduces no new analytic hypothesis.

theorem probability_mixture_of_minorization (ν ω : Measure ℝ)
    [IsProbabilityMeasure ν] [IsProbabilityMeasure ω] {η : ℝ}
    (hη0 : 0 < η) (hη1 : η < 1)
    (hminor : ENNReal.ofReal (1 - η) • ω ≤ ν) :
    ∃ τ : Measure ℝ, IsProbabilityMeasure τ ∧ predictionMixture ω τ η = ν := by
…

Mentions: OAI.LipschitzHilbert.predictionMixture