Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch03.ABK26.FluxComparisonLocalization

Coarse-graining support: Support.Book.Ch03.ABK26.FluxComparisonLocalization #

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

Root-to-descendant localization for the Chapter 3 flux defect #

This is the exact localization step which identifies the generic smooth-dual negative-norm descendant average with the source-facing flux-defect average.

source
theorem HCPolySupport.Book.Ch03.ABK26.centeredCubeRootFluxDefectL2Field_negativeWspSmoothDual_localize {d : ℕ} (m n : ℤ) (hnm : n < m) (a : Ch02.CoeffOn (Ch02.cubeDomain (originCube d m))) (sigma0 : ℝ) (u : H1Function (openCubeSet (originCube d m))) (s : ↑FractionalOrder) (p : FiniteLpExponent) :
cubeEuclideanNegativeWspSmoothDualENorm (originCube d m) s p (centeredCubeRootFluxDefectL2Field m a sigma0 u) ≤ ENNReal.ofReal (Real.rpow 3 (↑s * ↑(m - n))) * centeredCubeLocalFluxDefectSmoothDualLpAverage m n hnm a sigma0 u s p

The root scalar-comparator defect localizes to the exact normalized average of its descendant flux defects.