ScalarWeakSolutionRestriction

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

Restriction and differences of scalar-forced weak solutions

Two structural operations on the pointwise weak equation -div (a grad u) = g are recorded.

Restriction to an open subset. A test function of the subset extends by zero to a test function of the ambient domain, so the equation on the larger set implies the equation on the smaller one for the restricted H¹ function. The zero extension is the p = 2 construction of EquationRestrictionZeroExtension.lean.

Differences. The equation is affine in the pair (forcing, solution), so the difference of two solutions solves the equation with the difference of the forcings. Splitting the integrals uses the L² control of the fluxes, which is where the ellipticity certificate enters.

Both are needed to compare the Dirichlet resolvents of two exhaustion cubes on a common smaller cube: their difference solves the homogeneous shifted equation there.

Zero-extended tests

The two operations

theorem DivergenceFormProcess.Form.IsScalarForcedWeakSolution.restrictSubset {d : ℕ} {W V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (hVW : V ⊆ W) {a : HCPolySupport.CoeffField d} {g : HCPolySupport.Vec d → ℝ} {u : HCPolySupport.H1Function W} (h : IsScalarForcedWeakSolution a W g u) : IsScalarForcedWeakSolution a V g (u.restrict hV hVW)

The scalar-forced weak equation restricts to every open subset.

theorem DivergenceFormProcess.Form.IsScalarForcedWeakSolution.sub {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {lam Lam : ℝ} (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) {g₁ g₂ : HCPolySupport.Vec d → ℝ} {u₁ u₂ : HCPolySupport.H1Function U} (h₁ : IsScalarForcedWeakSolution a U g₁ u₁) (h₂ : IsScalarForcedWeakSolution a U g₂ u₂) : IsScalarForcedWeakSolution a U (fun (x : HCPolySupport.Vec d) => g₁ x - g₂ x) (u₁ - u₂)

The difference of two scalar-forced weak solutions solves the equation with the difference of the forcings.