PotentialDomainMonotonicity

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

Domain monotonicity for bounded nonnegative potentials

The ordinary part-domain truncation theorem applies after replacing a potential bounded by C with an added shift C and the nonnegative forcing f + (C-q)u. This gives comparison of potential resolvents on nested open bounded convex domains.

theorem DivergenceFormProcess.Form.potentialPartDomainZeroExtension_isSubsolution {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (hVU : V ⊆ U) {α lam Lam C : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hC : 0 ≤ C) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (q : HCPolySupport.Vec d → ℝ) (hqU : IsBoundedNonnegativePotential U q C) (f : ↥(HCPolySupport.ScalarL2 U)) (hf : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑f x) : IsPotentialWeakSubsolution a α q U (ZeroTraceSobolev.extendByZeroToPartSuperset hV ⋯ hVU ((potentialSolution a hα hlam ⋯ q ⋯) (restrictScalarL2ToPart ⋯ f))) f

The zero extension of a part-domain potential resolvent is a potential weak subsolution on the larger bounded convex domain.

theorem DivergenceFormProcess.Form.potentialPartDomainResolvent_le_ae {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (hVU : V ⊆ U) {α lam Lam C : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hC : 0 ≤ C) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (q : HCPolySupport.Vec d → ℝ) (hqU : IsBoundedNonnegativePotential U q C) (f : ↥(HCPolySupport.ScalarL2 U)) (hf : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑f x) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn V, ↑↑((potentialResolvent a hα hlam ⋯ q ⋯) (restrictScalarL2ToPart ⋯ f)) x ≤ ↑↑((potentialResolvent a hα hlam hEll q hqU) f) x

Potential Dirichlet resolvents increase under inclusion of bounded open convex domains for nonnegative forcing.

theorem DivergenceFormProcess.Form.potentialPartDomainResolvent_le_ae_of_ellipticityWitness {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (hVU : V ⊆ U) {alpha lamV LamV lamU LamU CV CU : ℝ} (halpha : 0 < alpha) (hlamV : 0 < lamV) (hlamU : 0 < lamU) (hCU : 0 ≤ CU) (hEllV : HCPolySupport.IsEllipticFieldOn lamV LamV V a) (hEllU : HCPolySupport.IsEllipticFieldOn lamU LamU U a) (q : HCPolySupport.Vec d → ℝ) (hqV : IsBoundedNonnegativePotential V q CV) (hqU : IsBoundedNonnegativePotential U q CU) (f : ↥(HCPolySupport.ScalarL2 U)) (hf : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑f x) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn V, ↑↑((potentialResolvent a halpha hlamV hEllV q hqV) (restrictScalarL2ToPart ⋯ f)) x ≤ ↑↑((potentialResolvent a halpha hlamU hEllU q hqU) f) x

Potential domain monotonicity with independently supplied ellipticity and potential-bound certificates on the two domains. The weak equation, hence the represented resolvent, is independent of those certificates.