SourceMotionBudget.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The quantitative small factors in predictable motion. Fixed powers and constants are absorbed only after the packet and weight estimates.

theorem OAI.LipschitzHilbert.source_moving_weight_factor_le line 14

theorem OAI.LipschitzHilbert.source_predictable_coefficient_le line 35

Source documentation

The two summation-by-parts errors have a common inverse-square-root factor as soon as their independent packet and weight bounds do.

theorem source_predictable_coefficient_le {V A E d W J G : ℝ}
    (hV : 0 ≤ V) (hA : 0 ≤ A) (hE : 0 ≤ E) (hW : 0 ≤ W) (hG : 1 ≤ G)
    (hd : d ≤ W/Real.sqrt G) (hpacket : E ≤ J/Real.sqrt G) :
    V*((1+d)*E+d*A) ≤ (V*((1+W)*J+W*A))/Real.sqrt G := by
…

theorem OAI.LipschitzHilbert.eventually_source_polynomial_motion line 55
Source documentation
Every fixed polynomial prefactor in the exact source motion bounds is dominated by a quarter-power gain of the actual rounded dyadic step.
```
theorem eventually_source_polynomial_motion (C p : ℝ) :
    ∀ᶠ L : ℝ in atTop,
      C*L^p/Real.sqrt (SourceParameters.step L) ≤
        SourceParameters.step L^(-(1/4:ℝ)) := by
…
```
Mentions: OAI.LipschitzHilbert.SourceParameters.step