MatchedTrace

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Matched-trace truncation

memH10_max_sub_matched: if w₁ − w₂ ∈ H¹₀(U) then the truncated difference (w₁ − c)₊ − (w₂ − c)₊ is again in H¹₀(U).

With h := w₁ − w₂ and its smooth compactly supported H¹₀ approximants φ_n := W.approx n, set Ψ_n := (w₂ + φ_n − c)₊ − (w₂ − c)₊. Each Ψ_n is H¹ and vanishes off tsupport φ_n (compact ⊆ U), hence lies in H¹₀. The target T := (w₁ − c)₊ − (w₂ − c)₊ is H¹; along an a.e.-convergent subsequence of φ_n → h, both Ψ_n → T and ∇Ψ_n → ∇T in L² (the level-set term vanishes), so the H¹₀-limit lemma concludes.

theorem HCPolySupport.memH10_max_sub_matched {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (w₁ w₂ : H1Function U) (hmatch : MemH10 U fun (x : Vec d) => w₁.toFun x - w₂.toFun x) (c : ℝ) : MemH10 U fun (x : Vec d) => max (w₁.toFun x - c) 0 - max (w₂.toFun x - c) 0

Matched-trace truncation. If w₁ − w₂ ∈ H¹₀(U) then the truncated difference (w₁ − c)₊ − (w₂ − c)₊ is again in H¹₀(U).