Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.CorrectorDecay.ContinuousKH1Interpolation

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.CorrectorDecay.ContinuousKH1Interpolation

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Continuous interpolation for coordinatewise H1 fields #

An exact coordinatewise H1 representative is an admissible competitor for the continuous K-functional. Its zero residual and weak-gradient energy give the endpoint needed to interpolate between normalized L2 and H1.

source
theorem HCPolySupport.continuousKSeminorm_le_gradientNorm_of_eq_toField {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) (G : ContinuousKCompetitor d) (hFG : F.toField = G.toField) :
continuousKSeminorm s F ≤ ENNReal.ofReal (2 - 2 * ↑s)⁻¹ ^ 2⁻¹ * ENNReal.ofReal (continuousKGradientNorm G)

A coordinatewise H1 representative controls the continuous interpolation seminorm by its normalized weak-gradient energy.