Coarse-graining support: Support.Sobolev.Foundations.CubeCalderonZygmund.WeakPoissonDerivative

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Weak equation for a derivative of a Poisson solution

Differentiating -Delta u = F in one coordinate does not require a derivative of F: the forcing is retained in divergence form as the vector field with F in that coordinate and zero in the others. This file establishes that identity from the scalar weak equation and an internally constructed weak Hessian witness.

theorem HCPolySupport.CubeCalderonZygmund.memVectorL2_singleCoordinate {d : ℕ} {U : Set (Vec d)} {F : Vec d → ℝ} (hF : MemScalarL2 U F) (i : Fin d) : MemVectorL2 U fun (x : Vec d) (j : Fin d) => if j = i then F x else 0

Inserting a scalar L² field into one coordinate gives a vector L² field.

theorem HCPolySupport.WeakPoissonEquationOn.gradCoordH1Function_weakDivergence {d : ℕ} {U : Set (Vec d)} {u : H1Function U} {F : Vec d → ℝ} (hU : IsOpen U) (hF : MemScalarL2 U F) (h : WeakPoissonEquationOn U u F) (H : HasWeakHessianOn U u) (i : Fin d) (φ : Vec d → ℝ) : ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ U → ∫ (x : Vec d) in U, vecDot ((H.gradCoordH1Function i).grad x) (euclideanGradient φ x) = -∫ (x : Vec d) in U, vecDot (fun (j : Fin d) => if j = i then F x else 0) (euclideanGradient φ x)

A scalar weak Poisson equation yields the divergence-form weak equation for every gradient coordinate. The datum is F in the differentiated coordinate and zero in all other coordinates; in particular, the conclusion assumes neither a weak derivative of F nor a trace for ∂ᵢu.

The MemScalarL2 hypothesis records that this coordinate datum is admissible as an L² vector field, via CubeCalderonZygmund.memVectorL2_singleCoordinate.

theorem HCPolySupport.WeakPoissonEquationOn.gradCoordH1Function_weakDivergence_constCoeff {d : ℕ} {U : Set (Vec d)} {u : H1Function U} {F : Vec d → ℝ} {sigma0 : ℝ} (hU : IsOpen U) (hsigma0 : sigma0 ≠ 0) (hF : MemScalarL2 U F) (h : ∀ (φ : Vec d → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ U → sigma0 * ∫ (x : Vec d) in U, vecDot (u.grad x) (euclideanGradient φ x) = ∫ (x : Vec d) in U, F x * φ x) (H : HasWeakHessianOn U u) (i : Fin d) (φ : Vec d → ℝ) : ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ U → sigma0 * ∫ (x : Vec d) in U, vecDot ((H.gradCoordH1Function i).grad x) (euclideanGradient φ x) = -∫ (x : Vec d) in U, vecDot (fun (j : Fin d) => if j = i then F x else 0) (euclideanGradient φ x)

Constant-coefficient form of WeakPoissonEquationOn.gradCoordH1Function_weakDivergence. If -sigma0 * Delta u = F, then ∂ᵢu has divergence datum F eᵢ with the coefficient and sign left unchanged.