Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.RoundedFiniteEnergyENNRealBridge

High-contrast homogenization: Provider.Regularity.RoundedFiniteEnergyENNRealBridge #

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

ENNReal realization of the finite centered energy row #

The Step-4 recurrence is real-valued, while the root weighted norm is ENNReal-valued. This file identifies the exact cube restrictions and lifts the finite inequality without changing either carrier.

source
theorem HCPolySupport.HighContrast.weightedGradNorm_eq_ofReal_finiteCenteredCubeSolutionEnergy {d : ℕ} (a : Book.Ch03.CoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) (h : ℤ) (hhm : h ≤ m) :
weightedGradNorm (a.coeffOn (originCube d h)).toCoeffField (openCubeSet (originCube d h)) u.toH1.grad = ENNReal.ofReal (finiteCenteredCubeSolutionEnergy a m u h)

The weighted norm on an inner centered cube is exactly the ENNReal realization of the finite centered energy row.