CorrectionMetricBounds.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Weighted estimates for the bilinear smoothing-tail error.

def OAI.ClosedSurfaceR4.ExactCorrection.crossBilinear line 19
Source documentation
The symmetric mixed metric coefficient as a bounded bilinear map of the two differentials.
```
def crossBilinear (v w : E) :
    (E →L[ℝ] V) →L[ℝ] (E →L[ℝ] V) →L[ℝ] ℝ := by
…
```
lemma OAI.ClosedSurfaceR4.ExactCorrection.crossBilinear_apply line 38

theorem OAI.ClosedSurfaceR4.ExactCorrection.weighted_metricCrossTerm line 43

Source documentation

Higher derivatives of the metric comparison depend linearly on the smoothing tail when the new increment has its fixed weighted bound.

theorem weighted_metricCrossTerm
    {O : Set E} (hO : UniqueDiffOn ℝ O) {τ C D : ℝ} {m : ℕ}
    (hτ : 0 ≤ τ) (hC : 0 ≤ C) (hD : 0 ≤ D)
    {G U : E → V}
    (hG : ContDiffOn ℝ ∞ (fderiv ℝ G) O)
    (hU : ContDiffOn ℝ ∞ (fderiv ℝ U) O)
    (hbG : WeightedEstimates.WeightedBound O τ m C (fderiv ℝ G))
    (hbU : WeightedEstimates.WeightedBound O τ m D (fderiv ℝ U))
    (v w : E) :
    WeightedEstimates.WeightedBound O τ m
      (2 * ‖v‖ * ‖w‖ * (2 ^ m * C * D))
      (fun x => metricCrossTerm G U x v w) := by
…

Mentions: OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound, OAI.ClosedSurfaceR4.ExactCorrection.metricCrossTerm