Coarse-graining support: Support.Deterministic.CoarseFluxResponse.PrivateLemmas #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Deterministic coarse-grained flux-response inequalities #
This file packages the Chapter-3 q = 1 weak-norm estimate for the coarse
flux defect under an explicit one-cube response hypothesis.
At the current checkpoint we isolate the genuinely local linear-response input
from the downstream multiscale summation argument. The local hypothesis is the
square bound on descendant cube averages that the note proof produces on each
cube, and the main theorem turns it into a note-normalized negative Besov
seminorm estimate with HomogenizationErrorOnCube.
theorem
HCPolySupport.blockJ_le_normalizedBlockResponseMax_mul_blockQuadratic_of_isEllipticMatrix
{d : ℕ}
(R : TriadicCube d)
(a : CoeffField d)
(a0 : Mat d)
{lam Lam lam0 Lam0 : ℝ}
(hEll : IsEllipticFieldOn lam Lam (cubeSet R) a)
(ha0 : IsEllipticMatrix lam0 Lam0 a0)
(P : BlockVec d)
:
BlockJ (cubeSet R) P (blockMatVecMul (blockMatrixOfCoeff a0) P) a ≤ normalizedBlockResponseMax R a a0 * blockVecDot P (blockMatVecMul (blockMatrixOfCoeff a0) P)