SourcePhaseParameters.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform phase and amplitude estimates at the actual source parameters.

theorem OAI.LipschitzHilbert.phaseMu_positive_le line 17
theorem OAI.LipschitzHilbert.source_phaseMu_small line 25
theorem OAI.LipschitzHilbert.source_phase_mass_bound line 38
Source documentation
The source's global top-mass bound grows by at most exp(3 sqrt L) after taking the phase power, uniformly in the direction-count parameter.
```
theorem source_phase_mass_bound {D L N : ℝ}
    (hD : 1 ≤ D) (hL : 1 ≤ L) (hN : 0 < N) (hlogN : Real.log N ≤ 2 * L) :
    N ^ phaseMu D (Real.sqrt L) ≤ Real.exp (3 * Real.sqrt L) := by
…
```
theorem OAI.LipschitzHilbert.eventually_source_subpower_amplitude line 60
Source documentation
The amplitude scale L^C (1+N^mu) is smaller than every fixed positive power of the actual rounded dyadic step. This is the source's subpower estimate used to absorb all marked-cell comparison errors.
```
theorem eventually_source_subpower_amplitude (C δ : ℝ) (hδ : 0 < δ) :
    ∀ᶠ L : ℝ in atTop, ∀ D N : ℝ, 1 ≤ D → 0 < N → Real.log N ≤ 2 * L →
      L ^ C * (1 + N ^ phaseMu D (Real.sqrt L)) ≤ SourceParameters.step L ^ δ := by
…
```
Mentions: OAI.LipschitzHilbert.SourceParameters.step

theorem OAI.LipschitzHilbert.eventually_source_amplitude_squared_decay line 104

Source documentation

Squaring the actual amplitude scale still leaves a fixed power gain against every source prediction error G^(-gamma).

theorem eventually_source_amplitude_squared_decay (C γ : ℝ) (hγ : 0 < γ) :
    ∀ᶠ L : ℝ in atTop, ∀ D N : ℝ, 1 ≤ D → 0 < N → Real.log N ≤ 2 * L →
      (L ^ C * (1 + N ^ phaseMu D (Real.sqrt L))) ^ 2 *
        SourceParameters.step L ^ (-γ) ≤ SourceParameters.step L ^ (-γ / 2) := by
…

Mentions: OAI.LipschitzHilbert.SourceParameters.step