Documentation

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

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

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

Splitting for the weak-norm maximizer lemma #

Finite-depth high/low Besov splits for the raw scalar-response maximizer fields. The high-depth terms are still deterministic analytic terms; later files bound them by the energy defect and multiscale ellipticity factors.

source
theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.canonicalScalarResponseGradientWeakNormPartialCubeSet_le_highLowSplit {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (s : ℝ) (N L : ℕ) (hs : 0 < s) (p q p0 : Vec d) :
Ch04.canonicalScalarResponseGradientWeakNormPartialCubeSet Q s N p q p0 a.toFun ≤ ∑ j ∈ Finset.range (N + 1) with j < L, 2 * (Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (Ch04.canonicalScalarResponseGradientAverageCubeSet R R p q a.toFun - p0)) + Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (Ch04.canonicalScalarResponseGradientAverageCubeSet Q R p q a.toFun - Ch04.canonicalScalarResponseGradientAverageCubeSet R R p q a.toFun)) + Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (_R : TriadicCube d) => vecNormSq 0) + Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (_R : TriadicCube d) => vecNormSq 0)) + 2 * (∑ j ∈ Finset.range (N + 1) with ¬j < L, cubeBesovNegativeVectorDepthSeminorm Q s (JUpperBoundWeakNorms.canonicalMaximizerGradientOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q) j + Real.rpow 3 (-s * ↑L) * (1 - Real.rpow 3 (-s))⁻¹ * √(vecNormSq (-p0)))

Finite-depth gradient split for the second Section 5.3 lemma. Depths j < L are split into the child maximizer average and the parent-child mismatch. Depths L ≤ j are left as the raw parent-gradient low-scale term plus the affine p0 tail.

source
theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.canonicalScalarResponseFluxWeakNormPartialCubeSet_le_highLowSplit {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (t : ℝ) (N L : ℕ) (ht : 0 < t) (p q q0 : Vec d) :
Ch04.canonicalScalarResponseFluxWeakNormPartialCubeSet Q t N p q q0 a.toFun ≤ ∑ j ∈ Finset.range (N + 1) with j < L, 2 * (Real.rpow 3 (-t * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (Ch04.canonicalScalarResponseFluxAverageCubeSet R R p q a.toFun - q0)) + Real.rpow 3 (-t * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (Ch04.canonicalScalarResponseFluxAverageCubeSet Q R p q a.toFun - Ch04.canonicalScalarResponseFluxAverageCubeSet R R p q a.toFun)) + Real.rpow 3 (-t * ↑j) * √(descendantsAverage Q j fun (_R : TriadicCube d) => vecNormSq 0) + Real.rpow 3 (-t * ↑j) * √(descendantsAverage Q j fun (_R : TriadicCube d) => vecNormSq 0)) + 2 * (∑ j ∈ Finset.range (N + 1) with ¬j < L, cubeBesovNegativeVectorDepthSeminorm Q t (JUpperBoundWeakNorms.canonicalMaximizerFluxOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q) j + Real.rpow 3 (-t * ↑L) * (1 - Real.rpow 3 (-t))⁻¹ * √(vecNormSq (-q0)))

Finite-depth flux split for the second Section 5.3 lemma. This is the flux analogue of canonicalScalarResponseGradientWeakNormPartialCubeSet_le_highLowSplit.