SourceAveraging.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Constructed near-uniform averaging at the actual rounded source scale.

theorem OAI.LipschitzHilbert.source_step_tendsto_atTop line 17

theorem OAI.LipschitzHilbert.exists_source_averaging_constant line 27

Source documentation

At every sufficiently large source parameter and every finite line interval, the Fourier-gap averaging law is an actual convex mixture of the uniform interval law and a probability remainder.

theorem exists_source_averaging_constant :
    ∃ C : ℝ, 1 ≤ C ∧ ∀ᶠ L : ℝ in atTop, ∀ a b : ℝ, a < b →
      ∃ (eta : ℝ) (remainder : Measure ℝ),
        0 < eta ∧ eta ≤ C * SourceParameters.step L ^ (-(1 / 16 : ℝ)) ∧
        eta < 1 / 2 ∧ IsProbabilityMeasure remainder ∧
        FourierGap (predictionMixture (intervalProbability a b) remainder eta)
          (1 / ((b - a) * SourceParameters.step L ^ (-(1 / 8 : ℝ)))) := by
…

Mentions: OAI.LipschitzHilbert.SourceParameters.step, OAI.LipschitzHilbert.predictionMixture, OAI.LipschitzHilbert.intervalProbability