FourierAveragingScale.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The source scales for the near-uniform averaging probability

Write h = G^(-1/16). The expansion padding is H*h/2 and the physical kernel scale is H*h². The resulting loss is exactly h + 4*M*h², hence at most a fixed constant times h.

theorem OAI.LipschitzHilbert.averaging_loss_at_source_scales line 21
theorem OAI.LipschitzHilbert.averaging_source_loss_bound line 27

theorem OAI.LipschitzHilbert.exists_source_scale_averaging_constant line 36

Source documentation

A universal averaging constant and a genuine probability remainder at every source scale. This discharges the probability-mixture existence obligation used by the graph prediction argument.

theorem exists_source_scale_averaging_constant :
    ∃ C : ℝ, 1 ≤ C ∧ ∀ (a b h : ℝ), a < b → 0 < h → h ≤ 1 → C * h < 1 / 2 →
      ∃ (η : ℝ) (τ : Measure ℝ), 0 < η ∧ η ≤ C * h ∧ η < 1 / 2 ∧
        IsProbabilityMeasure τ ∧
        FourierGap (predictionMixture (intervalProbability a b) τ η)
          (1 / ((b - a) * h ^ 2)) := by
…

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

theorem OAI.LipschitzHilbert.fourierGap_mono line 62

theorem OAI.LipschitzHilbert.exists_power_scale_averaging_constant line 68

Source documentation

The manuscript's powers of G, with a universal error coefficient.

theorem exists_power_scale_averaging_constant :
    ∃ C : ℝ, 1 ≤ C ∧ ∀ (a b G : ℝ), a < b → 1 ≤ G →
      C * G ^ (-(1 / 16 : ℝ)) < 1 / 2 →
      ∃ (η : ℝ) (τ : Measure ℝ), 0 < η ∧ η ≤ C * G ^ (-(1 / 16 : ℝ)) ∧
        η < 1 / 2 ∧ IsProbabilityMeasure τ ∧
        FourierGap (predictionMixture (intervalProbability a b) τ η)
          (1 / ((b - a) * G ^ (-(1 / 8 : ℝ)))) := by
…

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