Coarse-graining support: Support.Book.Ch02.Theorems.SolutionIntegrability #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.Book.Ch02.Solution.flux_memVectorL2
{d : ℕ}
{U : Domain d}
{a : CoeffOn U}
(u : Solution U a)
:
MemVectorL2 U.carrier fun (x : Vec d) => matVecMul (a.toCoeffField x) (u.toH1.grad x)
Public solutions have L² flux on their Chapter 2 domain.
The public coefficient object is only a.e.-elliptic. The proof changes to the
internal pointwise-good representative, applies the deterministic flux L²
bound there, and transports the result back across the a.e. equality of
coefficient representatives.