ShiftedSmoothingBounds.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Smoothing bounds with an unweighted finite derivative prefix. In the correction scheme the map has prefix order two and the metric defect order zero.

def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ShiftedBound line 16
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ShiftedBound.deriv_le line 19

lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ShiftedBound.prefix line 26

Source documentation

An unweighted prefix of any lower order is controlled by a shifted bound.

lemma ShiftedBound.prefix {q m : ℕ} {s C : ℝ} {f : Base → V}
    (h : ShiftedBound q m s C f) (hs : 0 < s) (hs1 : s ≤ 1) (hC : 0 ≤ C)
    {j : ℕ} (hj : j ≤ q + m) :
    WeightedBound Set.univ 1 j (C / s ^ (j - q)) f := by
…

Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ShiftedBound

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finiteSmooth_shifted_gain line 37
Source documentation
No derivative in the unweighted prefix incurs a smoothing-scale loss.
```
theorem finiteSmooth_shifted_gain (r q m : ℕ) {s C : ℝ} (hs : 0 < s)
    (hC : 0 ≤ C) {f : Base → V} (hf : ContDiff ℝ ∞ f) (hc : HasCompactSupport f)
    (hb : WeightedBound Set.univ 1 q C f) :
    ShiftedBound q m s
      (((1 + (1 + ∫ y, ‖kernel 0 y‖) ^ r) + weightedGainConstant r m) * C)
      (finiteSmooth r s f) := by
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ShiftedBound, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.kernel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.weightedGainConstant, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finiteSmooth
theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finiteSmooth_shifted_bounded line 67
Source documentation
The original shifted norm remains bounded independently of the smoothing scale.
```
theorem finiteSmooth_shifted_bounded (r q m : ℕ) {s t C : ℝ}
    (hs : 0 < s) (ht : 0 < t) {f : Base → V}
    (hf : ContDiff ℝ ∞ f) (hc : HasCompactSupport f)
    (hb : ShiftedBound q m t C f) :
    ShiftedBound q m t ((1 + (1 + ∫ y, ‖kernel 0 y‖) ^ r) * C)
      (finiteSmooth r s f) := by
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ShiftedBound, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.kernel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finiteSmooth

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.shifted_smoothing_tail line 84

Source documentation

A finite shifted input order suffices for the approximation term. Higher input derivatives occur linearly, with the two-scale decaying factor.

theorem shifted_smoothing_tail (r q m : ℕ) {s t τ B C : ℝ}
    (hτ : 0 < τ) (hτs : τ ≤ s) (hst : s ≤ t) (ht1 : t ≤ 1)
    (hB : 0 ≤ B) (hC : 0 ≤ C) {f : Base → V}
    (hf : ContDiff ℝ ∞ f) (hfc : HasCompactSupport f)
    (hBr : ShiftedBound q r t B f) (hCm : ShiftedBound q m t C f) :
    ShiftedBound q m τ
      (tailConstant r * (B * (s / t) ^ r + C * (τ / t) ^ r))
      (f - finiteSmooth r s f) := by
…

Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ShiftedBound, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.tailConstant, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finiteSmooth