PenalizedBoundaryComparison

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

Boundary-collar comparison for potential equations

The whole-space penalization interchange compares two Dirichlet solutions on nested cubes. This module isolates the weak maximum-principle step: if the larger solution is at most eps on a collar of the smaller boundary, then it is at most the smaller solution plus eps throughout the smaller domain.

def DivergenceFormProcess.Form.h1FunctionWithAeRepresentative {d : ℕ} {U : Set (HCPolySupport.Vec d)} (u : HCPolySupport.H1Function U) (v : HCPolySupport.Vec d → ℝ) (hvu : v =ᵐ[HCPolySupport.volumeMeasureOn U] u.toFun) : HCPolySupport.H1Function U

Replace the pointwise representative of an H¹ function without changing its weak gradient or its equivalence class on the domain.

Equations

• DivergenceFormProcess.Form.h1FunctionWithAeRepresentative u v hvu = { toFun := v, grad := u.grad, memL2 := ⋯, gradMemL2 := ⋯, hasWeakGradient := ⋯ }

theorem DivergenceFormProcess.Form.IsScalarForcedWeakSolution.withAeRepresentative {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {g g' : HCPolySupport.Vec d → ℝ} {u : HCPolySupport.H1Function U} (hu : IsScalarForcedWeakSolution a U g u) (v : HCPolySupport.Vec d → ℝ) (hvu : v =ᵐ[HCPolySupport.volumeMeasureOn U] u.toFun) (hgg' : g' =ᵐ[HCPolySupport.volumeMeasureOn U] g) : IsScalarForcedWeakSolution a U g' (h1FunctionWithAeRepresentative u v hvu)

A scalar-forced equation is unchanged when both its solution and forcing are replaced by almost-everywhere equal representatives.

theorem DivergenceFormProcess.Form.IsScalarForcedWeakSolution.restrictToOpen {d : ℕ} {U W : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {g : HCPolySupport.Vec d → ℝ} {u : HCPolySupport.H1Function W} (hu : IsScalarForcedWeakSolution a W g u) (hW : IsOpen W) (hU : IsOpen U) (hUW : U ⊆ W) : IsScalarForcedWeakSolution a U g (u.restrict hU hUW)

A scalar-forced weak equation restricts to an open subdomain.

theorem DivergenceFormProcess.Form.isScalarForcedWeakSolution_sub_same_potential {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {lam Lam alpha : ℝ} (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (q f : HCPolySupport.Vec d → ℝ) (u v : HCPolySupport.H1Function U) (hu : IsScalarForcedWeakSolution a U (fun (x : HCPolySupport.Vec d) => f x - (alpha + q x) * u.toFun x) u) (hv : IsScalarForcedWeakSolution a U (fun (x : HCPolySupport.Vec d) => f x - (alpha + q x) * v.toFun x) v) : IsScalarForcedWeakSolution a U (fun (x : HCPolySupport.Vec d) => -((alpha + q x) * (u - v).toFun x)) (u - v)

Subtracting two equations with the same source produces the homogeneous potential equation for their difference.

theorem DivergenceFormProcess.Form.ae_le_add_of_homogeneous_difference_boundary {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {a : HCPolySupport.CoeffField d} {lam Lam alpha eps : ℝ} (halpha : 0 < alpha) (heps : 0 ≤ eps) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) {q : HCPolySupport.Vec d → ℝ} (hq : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ q x) (u v : HCPolySupport.H1Function U) (hsol : IsScalarForcedWeakSolution a U (fun (x : HCPolySupport.Vec d) => -((alpha + q x) * (u - v).toFun x)) (u - v)) {K : Set (HCPolySupport.Vec d)} (hK : IsCompact K) (hKU : K ⊆ U) (hcollar : ∀ x ∉ K, u.toFun x ≤ v.toFun x + eps) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, u.toFun x ≤ v.toFun x + eps

A homogeneous potential difference with a compactly supported positive part is bounded by its boundary-collar level.

theorem DivergenceFormProcess.Form.le_add_of_homogeneous_difference_boundary {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {a : HCPolySupport.CoeffField d} {lam Lam alpha eps : ℝ} (halpha : 0 < alpha) (heps : 0 ≤ eps) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) {q : HCPolySupport.Vec d → ℝ} (hq : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ q x) (u v : HCPolySupport.H1Function U) (hu : ContinuousOn u.toFun U) (hv : ContinuousOn v.toFun U) (hsol : IsScalarForcedWeakSolution a U (fun (x : HCPolySupport.Vec d) => -((alpha + q x) * (u - v).toFun x)) (u - v)) {K : Set (HCPolySupport.Vec d)} (hK : IsCompact K) (hKU : K ⊆ U) (hcollar : ∀ x ∉ K, u.toFun x ≤ v.toFun x + eps) (x : HCPolySupport.Vec d) : x ∈ U → u.toFun x ≤ v.toFun x + eps

Continuous representatives upgrade the boundary-collar comparison from almost everywhere to every point of the open domain.