PartDomainSubsolution

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

Weak subsolutions from part-domain resolvents

This module proves that the zero extension of a nonnegative part-domain resolvent is a weak subsolution on a larger bounded open convex domain, and records the resulting nonnegative supersolution remainder and resolvent estimate.

theorem DivergenceFormProcess.Form.partDomainZeroExtension_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 : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (f : ↥(HCPolySupport.ScalarL2 U)) (hf : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑f x) : IsAlphaShiftedWeakSubsolution a U α f (ZeroTraceSobolev.extendByZeroToPartSuperset hV ⋯ hVU ((alphaShiftedSolution a hα hlam ⋯) (restrictScalarL2ToPart ⋯ f)))

The zero extension of the part-domain resolvent is a weak subsolution on the larger domain for nonnegative forcing. The general-open case is not asserted.

theorem DivergenceFormProcess.Form.partDomainRemainder_nonneg_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 : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (f : ↥(HCPolySupport.ScalarL2 U)) (hf : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑f x) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑(ZeroTraceSobolev.toL2 ((alphaShiftedSolution a hα hlam hEll) f - ZeroTraceSobolev.extendByZeroToPartSuperset hV ⋯ hVU ((alphaShiftedSolution a hα hlam ⋯) (restrictScalarL2ToPart ⋯ f)))) x

The difference between the full-domain resolvent solution and the zero-extended part-domain solution is nonnegative almost everywhere. The general-open case is not asserted.

theorem DivergenceFormProcess.Form.partDomainRemainder_isSupersolution {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (hVU : V ⊆ U) {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (f : ↥(HCPolySupport.ScalarL2 U)) (hf : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑f x) : IsAlphaShiftedWeakSupersolution a U α 0 ((alphaShiftedSolution a hα hlam hEll) f - ZeroTraceSobolev.extendByZeroToPartSuperset hV ⋯ hVU ((alphaShiftedSolution a hα hlam ⋯) (restrictScalarL2ToPart ⋯ f)))

The full-domain resolvent solution minus the zero-extended part-domain solution is a weak supersolution with zero right-hand side. The general-open case is not asserted.

theorem DivergenceFormProcess.Form.partDomainRemainder_resolvent_le_ae {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (hVU : V ⊆ U) {alpha beta lam Lam : ℝ} (hAlpha : 0 < alpha) (hAlphaBeta : alpha < beta) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (f : ↥(HCPolySupport.ScalarL2 U)) (hf : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑f x) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, beta * ↑↑((alphaShiftedResolvent a ⋯ hlam hEll) (ZeroTraceSobolev.toL2 ((alphaShiftedSolution a hAlpha hlam hEll) f - ZeroTraceSobolev.extendByZeroToPartSuperset hV ⋯ hVU ((alphaShiftedSolution a hAlpha hlam ⋯) (restrictScalarL2ToPart ⋯ f))))) x ≤ beta / (beta - alpha) * ↑↑(ZeroTraceSobolev.toL2 ((alphaShiftedSolution a hAlpha hlam hEll) f - ZeroTraceSobolev.extendByZeroToPartSuperset hV ⋯ hVU ((alphaShiftedSolution a hAlpha hlam ⋯) (restrictScalarL2ToPart ⋯ f)))) x

Resolvent estimate for the nonnegative supersolution remainder generated by nested bounded open convex domains. The general-open case is not asserted.