Basic

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

Positive-part truncation and compact support in H¹

• exists_h1_max_sub_const: the positive-part truncation (u − c)₊ lies in H¹(U) with weak gradient 1_{u>c} ∇u, via the C¹ chain rule applied to the one-sided approximants GApprox c δₙ and an L² limit.
• memH10_of_compactSupport: an H¹ function vanishing off a compact K ⊆ U lies in H¹₀(U), via a smooth cutoff ≡ 1 on K.

Both are stated on IsOpenBoundedConvexDomain U, the hypothesis the ambient mollification tools require.

theorem HCPolySupport.exists_h1_max_sub_const {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (u : H1Function U) (c : ℝ) : ∃ (v : H1Function U), (v.toFun = fun (x : Vec d) => max (u.toFun x - c) 0) ∧ ∀ᵐ (x : Vec d) ∂volumeMeasureOn U, v.grad x = {y : Vec d | c < u.toFun y}.indicator u.grad x

Positive-part truncation. For u ∈ H¹(U) and a level c, the truncation (u − c)₊ = max (u − c) 0 is again in H¹(U), with weak gradient 1_{u > c} ∇u almost everywhere.

Proof: apply the C¹ chain rule (hasWeakGradientOn_comp_of_deriv_bounded) to the one-sided smooth approximants GApprox c δₙ (δₙ = 1/(n+1)), then pass to the limit with the L²-limit closure keystone; the two convergences are dominated (tendsto_eLpNorm_two_of_tendsto_ae_of_dominated) using GApprox → (·−c)₊ and gStep → 𝟙_{·>c} pointwise everywhere.

theorem HCPolySupport.memH10_of_compactSupport {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (u : H1Function U) {K : Set (Vec d)} (hK : IsCompact K) (hKU : K ⊆ U) (hzero : ∀ x ∉ K, u.toFun x = 0) : MemH10 U u.toFun

Compact support implies H¹₀. An H¹(U) function that vanishes off a compact K ⊆ U lies in H¹₀(U).

Proof: pick a smooth cutoff χ ≡ 1 on K with tsupport χ ⊆ U; then χ·u is in H¹₀ by the library's cutoff-membership lemma, and χ·u = u since u vanishes off K.