Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch05.Theorems.Section53.WeakNormsMaximizer.RawIdentities

Coarse-graining support: Support.Book.Ch05.Theorems.Section53.WeakNormsMaximizer.RawIdentities #

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

Raw identities for scalar-response weak norms #

These deterministic identities connect the Ch4 scalar-response weak-norm objects used by the first Section 5.3 lemma to the raw Chapter 2 canonical maximizer fields used in the second lemma proof.

source
theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.canonicalScalarResponseGradientWeakNormCubeSet_eq_raw {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (s : ℝ) (p q p0 : Vec d) :
Ch04.canonicalScalarResponseGradientWeakNormCubeSet Q s p q p0 a.toFun = cubeBesovNegativeVectorSeminorm Q s (JUpperBoundWeakNorms.canonicalMaximizerGradientDefectOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0)
source
theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.canonicalScalarResponseFluxWeakNormCubeSet_eq_raw {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (s : ℝ) (p q q0 : Vec d) :
Ch04.canonicalScalarResponseFluxWeakNormCubeSet Q s p q q0 a.toFun = cubeBesovNegativeVectorSeminorm Q s (JUpperBoundWeakNorms.canonicalMaximizerFluxDefectOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q q0)