High-contrast homogenization: Provider.PolynomialHomogenization.Root.RowSupply.L2RowAlgebra #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Normalized L² algebra for ruled Whitney rows #
Every physical full-dual Whitney cell energy is priced by the normalized L²
average of its own field on the same cell. That
bridge is linear in the field on the left and quadratic on the right, so a
pointwise splitting H = F + G of a cell-indexed family costs a factor two at
the level of normalized L² cell averages and therefore a factor two at the
level of normalized rows — no dual-norm triangle inequality is needed, and none
is available: cubeBesovDualFullNorm is a sSup whose value set is bounded
above only under MemLp hypotheses.
This module collects
- additivity, scalar homogeneity and monotonicity of
normalizedWhitneyRowEnergy; - the same three for the
L²-priced cell energy of unit 28; - the pointwise
L²splitting⨍|F+G|² ≤ 2⨍|F|² + 2⨍|G|²on a cube; and - the resulting row join: a family that splits pointwise into two families
with priced normalized
L²cell averages has its full-dual row under twice the sum of the two priced rows.
Cube averages #
Row algebra #
theorem
HCPolySupport.HighContrast.RowSupply.normalizedWhitneyRowEnergy_mono
{d : ℕ}
{U : Set (Vec d)}
{rho Rad : ℝ}
(system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad)
{X Y : system.CellIndex → ENNReal}
(hXY : ∀ (i : system.CellIndex), X i ≤ Y i)
:
Normalized rows are monotone.
theorem
HCPolySupport.HighContrast.RowSupply.normalizedWhitneyRowEnergy_const_mul
{d : ℕ}
{U : Set (Vec d)}
{rho Rad : ℝ}
(system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad)
(c : ENNReal)
(X : system.CellIndex → ENNReal)
:
(normalizedWhitneyRowEnergy system fun (i : system.CellIndex) => c * X i) = c * normalizedWhitneyRowEnergy system X
Normalized rows are homogeneous.