SourcePredictionDecay.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The smaller fixed power gain used after mass normalization in the prediction argument. The constants and polynomial exponents remain fixed.

theorem OAI.LipschitzHilbert.relative_exponential_error_le line 13

theorem OAI.LipschitzHilbert.eventually_source_rescaled_motion line 19

Source documentation

Packet motion of order G^(-1/4) and any fixed polynomial times G^(-1/2) from the mass factors leave a uniform G^(-1/8) gain.

theorem eventually_source_rescaled_motion (B b c : ℝ) (hB : 0 ≤ B) (hc : 0 ≤ c) :
    ∀ᶠ L : ℝ in atTop, ∀ η q C : ℝ,
      0 ≤ η → η ≤ SourceParameters.step L^(-(1/4:ℝ)) →
      0 ≤ q → q ≤ B*L^b/Real.sqrt (SourceParameters.step L) →
      0 ≤ C → C ≤ L^c →
      (1+q)*η+q*C ≤ SourceParameters.step L^(-(1/8:ℝ)) := by
…

Mentions: OAI.LipschitzHilbert.SourceParameters.step