SupportedModeBounds.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Weighted seminorm bounds for the actual first geometric parametrix and its conjugated metric residual.

lemma OAI.ClosedSurfaceR4.SmallModes.forcedModeLM_zero_bound line 16
lemma OAI.ClosedSurfaceR4.SmallModes.geometric_defect_bound line 39
Source documentation
One geometric correction gains the factor τ / s with one derivative of the forcing. This is the actual differential operator residual.
```
lemma geometric_defect_bound (τ : ℝ) (hG : ContDiff ℝ ∞ G) (h : ModeDomain G U)
    (K : Compacts Base) (hKU : (K : Set Base) ⊆ U) {s : ℝ≥0} {B : ℝ}
    (hτ : 0 < τ) (hs : 0 < (s : ℝ)) (hs1 : s ≤ 1) (hB : 0 ≤ B)
    (m : ℕ) (hc : ModeCoefficientBound G U s (m + 1) B)
    (f : SupportedField (F := Fin 3 → ℂ) K) :
…
```
Mentions: OAI.ClosedSurfaceR4.SmallModes.ModeDomain, OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.SmallModes.ModeCoefficientBound