SmoothedMetricStepBounds.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The full one-step defect bound with the constructed coordinate smoother.

theorem OAI.ClosedSurfaceR4.ExactCorrection.smoothed_metric_step_bound line 17

Source documentation

Substituting the actual smoothing estimates into the metric identity keeps the dependence on both uncontrolled higher input norms linear.

theorem smoothed_metric_step_bound (r m : ℕ)
    {target : Base → ℝ} (htarget : ContDiff ℝ ∞ target)
    {G U : Base → V} (hG : ContDiff ℝ ∞ G) (hGc : HasCompactSupport G)
    (hU : ContDiff ℝ ∞ U) (v w : Base)
    {s t τ δ δ' BH CH BG CG D BE : ℝ}
    (hτ : 0 < τ) (hτs : τ ≤ s) (hst : s ≤ t) (hδ : δ ≠ 0) (hδ' : δ' ≠ 0)
    (hHc : HasCompactSupport (normalizedMetricDefect target δ G v w))
    (hbH : WeightedBound Set.univ t r BH (normalizedMetricDefect target δ G v w))
    (hcH : WeightedBound Set.univ t m CH (normalizedMetricDefect target δ G v w))
    (hbG : WeightedBound Set.univ t r BG (fderiv ℝ G))
    (hcG : WeightedBound Set.univ t m CG (fderiv ℝ G))
    (hbU : WeightedBound Set.univ τ m D (fderiv ℝ U))
…

Mentions: OAI.ClosedSurfaceR4.ExactCorrection.normalizedMetricDefect