SmoothingMetricCrossBounds.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual smoothing-tail contribution to the induced metric update. The dependence on uncontrolled higher input derivatives is linear.

lemma OAI.ClosedSurfaceR4.ExactCorrection.fderiv_smoothing_error line 18

theorem OAI.ClosedSurfaceR4.ExactCorrection.weighted_smoothing_metricCrossTerm line 30

Source documentation

In the mixed metric term, all higher derivatives of the true map occur only in the small factor (τ/t)^r multiplying C.

theorem weighted_smoothing_metricCrossTerm (r m : ℕ) {s t τ B C D : ℝ}
    (hτ : 0 < τ) (hτs : τ ≤ s) (hst : s ≤ t)
    {G U : Base → V} (hG : ContDiff ℝ ∞ G) (hc : HasCompactSupport G)
    (hU : ContDiff ℝ ∞ U)
    (hBr : WeightedBound Set.univ t r B (fderiv ℝ G))
    (hCm : WeightedBound Set.univ t m C (fderiv ℝ G))
    (hDu : WeightedBound Set.univ τ m D (fderiv ℝ U)) (v w : Base) :
    WeightedBound Set.univ τ m
      (2 * ‖v‖ * ‖w‖ * (2 ^ m *
        (tailConstant r * (B * (s / t) ^ r + C * (τ / t) ^ r)) * D))
      (fun x => metricCrossTerm (G - finiteSmooth r s G) U x v w) := by
…

Mentions: OAI.ClosedSurfaceR4.ExactCorrection.metricCrossTerm