ShiftedResidualBound

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Bounded scalar residuals for the shifted resolvent

This file removes the zeroth-order term from the shifted weak resolvent equation. If the scalar forcing is almost everywhere bounded by C, then its unshifted residual is almost everywhere bounded by 2 * C.

The conclusions concern the chosen Sobolev representative only almost everywhere. No pointwise measurability or continuity is asserted.

theorem DivergenceFormProcess.Form.abs_sub_alpha_mul_toFun_le_two_mul_ae {d : ℕ} {U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {alpha lam Lam C : ℝ} (hAlpha : 0 < alpha) (hLam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (f : ↥(HCPolySupport.ScalarL2 U)) (hC : 0 ≤ C) (hf : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, |↑↑f x| ≤ C) (u : HCPolySupport.H10Function U) (hu : u.toScalarL2 = (alphaShiftedResolvent a hAlpha hLam hEll) f) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, |↑↑f x - alpha * u.toFun x| ≤ 2 * C

The scalar residual of an H¹₀ representative of the shifted resolvent is almost everywhere bounded by twice the forcing bound.

theorem DivergenceFormProcess.Form.exists_h10Function_scalarForced_residual_bound {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (a : HCPolySupport.CoeffField d) {alpha lam Lam C : ℝ} (hAlpha : 0 < alpha) (hLam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (f : ↥(HCPolySupport.ScalarL2 U)) (hC : 0 ≤ C) (hf : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, |↑↑f x| ≤ C) : ∃ (u : HCPolySupport.H10Function U), u.toScalarL2 = (alphaShiftedResolvent a hAlpha hLam hEll) f ∧ IsAlphaShiftedWeakSolution a U alpha f (ZeroTraceSobolev.ofH10Function u) ∧ IsScalarForcedWeakSolution a U (fun (x : HCPolySupport.Vec d) => ↑↑f x - alpha * u.toFun x) u.toH1Function ∧ ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, |↑↑f x - alpha * u.toFun x| ≤ 2 * C

A bounded forcing admits an H¹₀ representative of its shifted resolvent which solves the unshifted scalar equation with almost everywhere bounded residual.