High-contrast homogenization: Provider.Transport.FillingSubadditivity #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Subadditivity of the coarse block over a sub-partition, with its residual #
The moving finite exhaustion of e.two.grid.whitney.average reads
e.fixed.geometry.parent.child along a family that is not a partition: the
maximal q-filling of a target cell W, cut off at a finite scale J, is a
finite disjoint family of cells inside W whose union misses a residual R_J of
positive measure. The partition lemmas of
HCPoly.Provider.Recurrence.AdaptedPartitionAverage therefore do not apply, and
the printed argument does not ask them to: it triangulates the residual, pays for
it, and lets J → -∞.
This file pays for the residual once and for all, without triangulating it. Two observations do the work.
Finite additivity with a residual. The integral over W of any function
integrable there is the sum of the integrals over the selected cells plus the
integral over the residual, and the relative volumes |c_i| / |W| together with
|R| / |W| sum to one. No null hypothesis and no infinite sum enters; this is
the split that subadditivity over a finite cross-grid exhaustion makes before the
triangulation.
A uniform bound on the response integrand. On any measurable subset of W,
and uniformly over the a-harmonic competitors, the scalar response integrand of
the variational definition of the coarse block is at most
λ^{-1}(Λ²|p|² + |q|²): ellipticity bounds the energy from below, the two
linear terms are absorbed by Young's
inequality, and no convexity or maximizer is involved. This is
scalarResponseIntegrand_le_plainUpperBound_of_isEllipticFieldOn upstream; the
only thing added here is that it is used on the residual, where nothing else is
known.
Together they give the response functional of the parent below the weighted sum
of the responses of the selected cells plus the residual weight times one
constant, and hence the same for the block quadratic form: the leftover affine
term -p·q of responseJ_eq_blockQuadratic, which cancels exactly against a
full partition, survives here multiplied by the residual weight and is folded
into the same constant. Because the residual weight is what the residual volume
of the Whitney selection drives to zero, the value of that constant
is irrelevant downstream, and the coefficient-space forms below record only that
one exists.
Finite additivity with a residual #
The volume of the parent is the sum of the volumes of the cells plus the volume of the residual. The cells are disjoint and inside the parent, and the residual is what the parent has left; no null hypothesis is used.
The integral over the parent splits off the residual. This is the finite additivity that subadditivity over a finite cross-grid exhaustion uses before its triangulation.
The weights of a sub-partition, together with the residual weight, sum to
one. This is the printed normalization Σ|V|/|W| + |R|/|W| = 1 of the split
exhaustion.
The response functional over a sub-partition #
Subadditivity of the response functional over a sub-partition. Every
competitor on the parent restricts to a competitor on each selected cell, and on
the residual the integrand is below the uniform elliptic majorant
λ^{-1}(Λ²|p|² + |q|²), which is all that is known there.
The block quadratic form over a sub-partition #
Subadditivity of the coarse block over a sub-partition, in the quadratic
form that defines the Loewner order. This is the first display of
e.fixed.geometry.parent.child along a family that covers the parent only
partially: the deficit is charged to the residual weight, at one constant that
depends on the ellipticity of the field and on the doubled vector alone.
The affine term -p·q of responseJ_eq_blockQuadratic no longer cancels, the
cell weights summing to 1 - |R|/|W| rather than to one; what it leaves is
exactly the residual weight times -X_1·X_2, which is why that term appears
inside the same bracket.
The coefficient-space forms #
The coarse response is positive, the first clause of
e.two.grid.whitney.average: its quadratic form is nonnegative at every
doubled vector, on every bounded open convex domain of positive volume.