EquationRestrictionZeroExtension

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

Zero extension of an H¹₀ test function to a superset

The Support-grade primitive needed to restrict a divergence-form weak equation from a set W to a subset V: every H¹₀(V) test function is, after extension by zero, an H¹₀(W) test function with gradient the zero extension of the original gradient.

CoarseGraining proves exactly this (H10Function.extendByZeroToOpenSuperset in Homogenization/Sobolev/W1p/ZeroExtensionGraph.lean) but through the finite-exponent graph closure of Homogenization/Sobolev/W1p/WeakGradientClosure, neither of which is available in this repository's pinned upstream build tree (no .olean; recompiling upstream is forbidden). The construction is therefore re-derived here at the single exponent p = 2 that the §4.3 leg needs, on the built L² closure HasWeakGradientOn.of_tendsto_eLpNorm_two (Homogenization/Sobolev/Truncation/WeakGradientLimit.lean).

Why the extension is a theorem and not bookkeeping

The zero extension of an H¹(V) function need not have a weak gradient across ∂V; it does exactly because an H¹₀(V) function carries an approximating sequence of smooth functions with compact support inside V. Each approximant is a legitimate global test function, its classical integration by parts is valid on all of W, and both sides are L²-continuous, so the identity survives the limit. That is the content below.

Deviation from CoarseGraining's version (weaker hypotheses)

CoarseGraining's extendByZeroToOpenSuperset asks for IsOpen W; the version here does not (openness of W is only used by CoarseGraining's route through the whole-space graph and its subsequent restriction). MeasurableSet V and V ⊆ W suffice.

References

• CoarseGraining, Homogenization/Sobolev/W1p/ZeroExtensionGraph.lean (the unavailable finite-p original; the four indicator identities below are its private helpers at p = 2), Homogenization/Sobolev/Truncation/WeakGradientLimit.lean (HasWeakGradientOn.of_tendsto_eLpNorm_two), Homogenization/Sobolev/H1/BasicLemmas.lean (HasWeakGradientOn.of_contDiff).

1. The zero extensions

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.h10ZeroExtension {d : ℕ} {V : Set (HCPolySupport.Vec d)} (phi : HCPolySupport.H10Function V) : HCPolySupport.Vec d → ℝ

The literal zero extension of the value of an H¹₀ function.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.h10ZeroExtension phi = V.indicator phi.toFun

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.h10ZeroExtensionGrad {d : ℕ} {V : Set (HCPolySupport.Vec d)} (phi : HCPolySupport.H10Function V) : HCPolySupport.Vec d → HCPolySupport.Vec d

The literal zero extension of the gradient of an H¹₀ function.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.h10ZeroExtensionGrad phi = V.indicator phi.grad

theorem Algsuperdiff.Section4.Provider.ExcessDecay.h10ZeroExtension_of_mem {d : ℕ} {V : Set (HCPolySupport.Vec d)} (phi : HCPolySupport.H10Function V) {x : HCPolySupport.Vec d} (hx : x ∈ V) : h10ZeroExtension phi x = phi.toFun x

theorem Algsuperdiff.Section4.Provider.ExcessDecay.h10ZeroExtension_of_not_mem {d : ℕ} {V : Set (HCPolySupport.Vec d)} (phi : HCPolySupport.H10Function V) {x : HCPolySupport.Vec d} (hx : x ∉ V) : h10ZeroExtension phi x = 0

theorem Algsuperdiff.Section4.Provider.ExcessDecay.h10ZeroExtensionGrad_of_mem {d : ℕ} {V : Set (HCPolySupport.Vec d)} (phi : HCPolySupport.H10Function V) {x : HCPolySupport.Vec d} (hx : x ∈ V) : h10ZeroExtensionGrad phi x = phi.grad x

theorem Algsuperdiff.Section4.Provider.ExcessDecay.h10ZeroExtensionGrad_of_not_mem {d : ℕ} {V : Set (HCPolySupport.Vec d)} (phi : HCPolySupport.H10Function V) {x : HCPolySupport.Vec d} (hx : x ∉ V) : h10ZeroExtensionGrad phi x = 0

2. The four indicator identities of the approximating sequence

theorem Algsuperdiff.Section4.Provider.ExcessDecay.h10_approx_sub_zeroExtension {d : ℕ} {V : Set (HCPolySupport.Vec d)} (phi : HCPolySupport.H10Function V) (n : ℕ) : (fun (x : HCPolySupport.Vec d) => phi.approx n x - h10ZeroExtension phi x) = V.indicator fun (x : HCPolySupport.Vec d) => phi.approx n x - phi.toFun x

theorem Algsuperdiff.Section4.Provider.ExcessDecay.h10_fderiv_approx_sub_zeroExtensionGrad {d : ℕ} {V : Set (HCPolySupport.Vec d)} (phi : HCPolySupport.H10Function V) (n : ℕ) (i : Fin d) : (fun (x : HCPolySupport.Vec d) => (fderiv ℝ (phi.approx n) x) (HCPolySupport.basisVec i) - h10ZeroExtensionGrad phi x i) = V.indicator fun (x : HCPolySupport.Vec d) => (fderiv ℝ (phi.approx n) x) (HCPolySupport.basisVec i) - phi.grad x i

3. L² control of the extensions

theorem Algsuperdiff.Section4.Provider.ExcessDecay.memL2On_h10ZeroExtension {d : ℕ} {V W : Set (HCPolySupport.Vec d)} (phi : HCPolySupport.H10Function V) (hV : MeasurableSet V) : HCPolySupport.MemL2On W (h10ZeroExtension phi)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.gradMemL2On_h10ZeroExtensionGrad {d : ℕ} {V W : Set (HCPolySupport.Vec d)} (phi : HCPolySupport.H10Function V) (hV : MeasurableSet V) : HCPolySupport.GradMemL2On W (h10ZeroExtensionGrad phi)

4. The weak gradient of the zero extension

theorem Algsuperdiff.Section4.Provider.ExcessDecay.hasWeakGradientOn_h10ZeroExtension {d : ℕ} {V W : Set (HCPolySupport.Vec d)} (phi : HCPolySupport.H10Function V) (hV : MeasurableSet V) (hVW : V ⊆ W) : HCPolySupport.HasWeakGradientOn W (h10ZeroExtension phi) (h10ZeroExtensionGrad phi)

The zero extension of an H¹₀ pair is a weak-gradient pair on any superset. The L²-limit closure applied to the H¹₀ approximants, each of which is smooth with compact support inside V ⊆ W.

5. The extension as an H¹₀ function of the superset

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.h10ExtendToSuperset {d : ℕ} {V W : Set (HCPolySupport.Vec d)} (phi : HCPolySupport.H10Function V) (hV : MeasurableSet V) (hVW : V ⊆ W) : HCPolySupport.H10Function W

Every H¹₀(V) function is an H¹₀(W) function for V ⊆ W, by literal zero extension of both value and gradient. Re-derivation at p = 2 of CoarseGraining's H10Function.extendByZeroToOpenSuperset, without the IsOpen W hypothesis.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.h10ExtendToSuperset_toFun {d : ℕ} {V W : Set (HCPolySupport.Vec d)} (phi : HCPolySupport.H10Function V) (hV : MeasurableSet V) (hVW : V ⊆ W) : (h10ExtendToSuperset phi hV hVW).toFun = h10ZeroExtension phi

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.h10ExtendToSuperset_grad {d : ℕ} {V W : Set (HCPolySupport.Vec d)} (phi : HCPolySupport.H10Function V) (hV : MeasurableSet V) (hVW : V ⊆ W) : (h10ExtendToSuperset phi hV hVW).grad = h10ZeroExtensionGrad phi