Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch02.Theorems.CoarseGrainingEstimates

Coarse-graining support: Support.Book.Ch02.Theorems.CoarseGrainingEstimates #

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

source
theorem HCPolySupport.Book.Ch02.responseCoarseGrainingEstimatesTheory {d : ℕ} (U : Domain d) (a : CoeffOn U) :
ResponseCoarseGrainingEstimatesTheory U a

Public theorem for l.cg.response.estimates.basic.definitions.

source
theorem HCPolySupport.Book.Ch02.vecNormSq_averageGradient_le_matrixNorm_sigmaStarInvCoarse_mul_variationEnergyValue {d : ℕ} (U : Domain d) (a : CoeffOn U) (w : Solution U a) :
vecNormSq (averageGradient U a w) ≤ matrixNorm (sigmaStarInvCoarse U a) * variationEnergyValue U a w

The averaged gradient is controlled by the σ_*^{-1} operator norm times the quadratic variation energy.

source
theorem HCPolySupport.Book.Ch02.vecNormSq_averageFlux_le_matrixNorm_bCoarse_mul_variationEnergyValue {d : ℕ} (U : Domain d) (a : CoeffOn U) (w : Solution U a) :
vecNormSq (averageFlux U a w) ≤ matrixNorm (bCoarse U a) * variationEnergyValue U a w

The averaged flux is controlled by the b operator norm times the quadratic variation energy.