PositivePart

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

Positive-part truncation on the zero-trace Sobolev carrier

This file establishes positive-part truncation after subtracting a nonnegative constant on ZeroTraceSobolev, including its almost-everywhere value and gradient characterizations.

theorem DivergenceFormProcess.Form.ZeroTraceSobolev.existsUnique_positivePartSubConst {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (u : ZeroTraceSobolev U) (c : ℝ) (hc : 0 ≤ c) : ∃! v : ZeroTraceSobolev U, (∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, ↑↑(toL2 v) x = max (↑↑(toL2 u) x - c) 0) ∧ ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, ↑↑(gradient v) x = {y : HCPolySupport.Vec d | c < ↑↑(toL2 u) y}.indicator (↑↑(gradient u)) x

Positive-part truncation after subtracting a nonnegative constant exists uniquely in ZeroTraceSobolev, subject to the stated almost-everywhere value and gradient characterizations.