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

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

Harmonicity of weak derivatives

This is an internal closure lemma for the Calderon--Zygmund proof engine. Starting with a homogeneous scalar weak Poisson equation and the locally constructed weak-Hessian witness, it supplies the same homogeneous equation for every gradient coordinate. No regularity assumption is added to a Calderon--Zygmund statement: the witness is the one produced by the interior difference-quotient argument.

theorem HCPolySupport.WeakPoissonEquationOn.gradCoordH1Function_harmonic {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (hU : IsOpen U) (h : WeakPoissonEquationOn U u fun (x : Vec d) => 0) (H : HasWeakHessianOn U u) (i : Fin d) : WeakPoissonEquationOn U (H.gradCoordH1Function i) fun (x : Vec d) => 0

A zero-forcing weak Poisson equation is inherited by each gradient coordinate once the local weak Hessian has been constructed.

theorem HCPolySupport.WeakPoissonEquationOn.gradCoordH1Function_harmonic_restrict {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (h : WeakPoissonEquationOn U u fun (x : Vec d) => 0) {V : Set (Vec d)} (hVopen : IsOpen V) (hVU : V ⊆ U) (H : HasWeakHessianOn V (u.restrict hVopen hVU)) (i : Fin d) : WeakPoissonEquationOn V (H.gradCoordH1Function i) fun (x : Vec d) => 0

Strict-inner-domain form of gradCoordH1Function_harmonic. The scalar weak equation is restricted, while the local Hessian witness is consumed only on the inner domain.