PartDomainTruncationTest #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Truncated tests for part-domain weak solutions #
This module constructs an admissible zero-trace truncation of a nonnegative ambient Sobolev test and proves the quantitative limiting estimate that extends the weak equation to that test.
theorem
DivergenceFormProcess.Form.exists_part_truncation
{d : ℕ}
{V : Set (HCPolySupport.Vec d)}
(hV : HCPolySupport.IsOpenBoundedConvexDomain V)
(φ : HCPolySupport.H1Function V)
(u : ZeroTraceSobolev V)
(K : ℝ)
(hK : 0 ≤ K)
(hφ : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn V, 0 ≤ φ.toFun x)
(hu : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn V, 0 ≤ ↑↑(ZeroTraceSobolev.toL2 u) x)
:
∃ (q : ZeroTraceSobolev V),
(∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn V, ↑↑(ZeroTraceSobolev.toL2 q) x = min (φ.toFun x) (K * ↑↑(ZeroTraceSobolev.toL2 u) x)) ∧ ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn V, ↑↑(ZeroTraceSobolev.gradient q) x = if φ.toFun x ≤ K * ↑↑(ZeroTraceSobolev.toL2 u) x then HCPolySupport.HilbertVec.ofVec (φ.grad x)
else K • ↑↑(ZeroTraceSobolev.gradient u) x
A nonnegative Sobolev test function truncated against a nonnegative zero-trace function.
theorem
DivergenceFormProcess.Form.part_solution_test_inequality
{d : ℕ}
{V : Set (HCPolySupport.Vec d)}
(a : HCPolySupport.CoeffField d)
(hV : HCPolySupport.IsOpenBoundedConvexDomain V)
{α lam Lam : ℝ}
(hα : 0 < α)
(hlam : 0 < lam)
(hEll : HCPolySupport.IsEllipticFieldOn lam Lam V a)
(f : ↥(HCPolySupport.ScalarL2 V))
(u : ZeroTraceSobolev V)
(huSol : IsAlphaShiftedWeakSolution a V α f u)
(hf : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn V, 0 ≤ ↑↑f x)
(hu : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn V, 0 ≤ ↑↑(ZeroTraceSobolev.toL2 u) x)
(φ : HCPolySupport.H1Function V)
(hφ : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn V, 0 ≤ φ.toFun x)
:
α * inner ℝ (ZeroTraceSobolev.toL2 u) φ.toScalarL2 + coefficientPairing a V (ZeroTraceSobolev.gradient u) φ.gradToHilbertVectorL2 ≤ inner ℝ f φ.toScalarL2
The weak equation extends to nonnegative ambient Sobolev test functions.