OAI/Geometry/SurfaceImmersion/Correction/SmoothingTailBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.tailConstant line 13
2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.approximationConstant_le_tail line 17
3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.residualConstant_le_tail line 26
4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.tailConstant_nonneg line 30
5. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.weighted_smoothing_tail line 37

   Source documentation

   Only the finite order r is used in the approximation term; uncontrolled higher input derivatives enter linearly, multiplied by (τ/t)^r.

   theorem weighted_smoothing_tail (r m : ℕ) {s t τ B C : ℝ}
       (hτ : 0 < τ) (hτs : τ ≤ s) (hst : s ≤ t)
       {f : Base → E} (hf : ContDiff ℝ ∞ f) (hfc : HasCompactSupport f)
       (hBr : WeightedBound Set.univ t r B f)
       (hCm : WeightedBound Set.univ t m C f) :
       WeightedBound Set.univ τ m
         (tailConstant r * (B * (s / t) ^ r + C * (τ / t) ^ r))
         (f - finiteSmooth r s f) := by
   …

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