High-contrast homogenization: Entry.Response.Kernel.QuadraticResponseRecombination #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Quadratic response, recombined over an almost-everywhere partition #
The averaging identity for an exact finite cover is restated here for an almost-everywhere cover,
since the adapted grid's cells meet their parent only up to the Lebesgue-null grid seams. On a
domain carrying a pointwise elliptic coefficient, the quadratic part of the response functional
evaluated at a response maximizer against any competitor obtained by restricting a harmonic
function from a larger set equals twice the response deficit between them; this file recombines
that identity, first over a single partition and then over an almost-everywhere one, and evaluates
the scalar response ResponseJ U p r a of AK.HC (2.9) at the canonical coarse-block quadratic
expression on an aligned adapted cell and subcell. The module serves the response-transfer
proposition p.response.transfer.
Averaging over an almost-everywhere finite partition #
The partition identity holds for an exact cover
U = ⋃ w ∈ Z, V w. The cells produced by the adapted grid are open, so they meet their
parent cell only up to the grid seams, a Lebesgue-null set; the exact cover is therefore
not available. This file restates the identity for an almost-everywhere cover: U and the
disjoint union of the V w agree up to a null set, and the integral over U may be
replaced by the integral over that union.
The identity survives volume (V w) = 0 for no w ∈ Z: hvolw with hUpos and
Z.card > 0 gives (volume (V w)).toReal = (volume U).toReal / |Z| > 0, so every cell
has nonzero (and, in particular, non-infinite) volume and volumeAverage never divides by
zero.
Averaging over an almost-everywhere finite equal-volume partition. If the
measurable sets V w (w ∈ Z) are pairwise disjoint and contained in U, if U
differs from their union by a null set, and if every cell has the same volume
|V w| = |U| / |Z| (stated in toReal form), then for any g integrable on U
the flat average over Z of the cell averages ⨍_{V w} g equals the average
⨍_U g:
|Z|⁻¹ ∑_{w ∈ Z} ⨍_{V w} g = ⨍_U g.
The null-set hypothesis is what the open adapted cells supply: they cover the parent
only up to the grid seams. The integral over U is transferred to the union with
setIntegral_congr_set, whose two sides have the same restricted measure; the union is
then split with integral_biUnion_finset exactly as in the exact-cover statement.
Quadratic response: the difference energy is twice the response deficit #
On a domain V carrying a pointwise elliptic coefficient a, let v be a
response maximizer for the load (p, q) and let uV be any other admissible
competitor (the restriction of a harmonic function from a larger set U ⊇ V).
Writing X = (∇w, a ∇w) for the doubled state of a field w, the quadratic
part of the response functional is exact at a maximizer: the first variation
vanishes, so the difference energy of the two states is
⨍_V (X_{uV} − X_v) · A (X_{uV} − X_v) = 4 (J(V) − ⨍_V g_V(uV))
with A the pointwise block of a and g_V the response integrand. Because
the pointwise block energy is twice the symmPart variation energy
(X · A X = 2 ∇w · symmPart(a) ∇w), this is equivalently the statement below:
the variation energy of the difference equals twice the response deficit.
The deficit is measured against the value of the competitor on V, not
against the parent-domain supremum J(U): the two differ in general, since the
average of the parent integrand over a proper subset need not equal its average
over U. The identity is the single-domain engine behind the recent-cell
response estimate; the recombination over a partition of U is a separate
step.
Quadratic response on one domain pair. Let V ⊆ U be open sets, a be
pointwise elliptic on V, v a response maximizer on V for the load
(p, q), and u any a-harmonic function on U. Then the symmPart
variation energy on V of the difference between the restricted parent u and
the maximizer v is twice the response deficit of the restricted parent:
⨍_V (∇u − ∇v) · symmPart(a) (∇u − ∇v) = 2 (J(V) − ⨍_V g_V(u)).
Only the maximizer on V is used; the parent need not be a maximizer on U.
The four integrability side conditions are those required by the first- and
second-variation identities.
Quadratic response recombined over the cells #
On a single child cell V of a parent U, the variation energy of the
difference between the parent field and the cell maximizer equals twice the
response deficit of the parent field on that cell
(difference_energy_eq_response_deficit). The present file averages that
identity over the finitely many cells of a partition and uses
average_over_aePartition to turn the flat average of the per-cell parent
integrands into the parent average. When the parent field is itself the
maximizer on U, responseJ_eq_of_isResponseMaximizer identifies that parent
average with ResponseJ U p q a, so the flat average of the cell difference
energies equals twice the difference between the flat average of the cell
responses and the parent response.
The per-cell average of the parent integrand depends on the cell, so the abstract
recombination below carries gavg : iota → ℝ, not a single constant. A constant
gavg would be correct only when every cell has the same parent integrand,
which the partition step does not provide, and it would not typecheck against
average_over_aePartition, whose right-hand side is the parent average.
Averaging a per-cell deficit identity over a finite index set. Suppose
the cells are indexed by the nonempty finite set Z, each cell carries the
deficit identity Eng w = 2 (Jchild w − gavg w) for its own parent average
gavg w, and the flat average of those parent averages is Jparent. Then the
flat average of Eng is twice the difference between the flat average of
Jchild and Jparent. The index set is required nonempty only so that the
inverse cardinality behaves; the statement is an identity in the sums.
The recombined quadratic-response identity on an almost-everywhere partition #
The recombined quadratic-response identity is stated over an exact finite cover
U = ⋃ w ∈ Z, V w with equal cell volumes. The adapted
cells the response estimate uses are open, so they meet their parent cell only up to the grid
seams; the exact cover is not available at those carriers and the identity cannot be
instantiated there. This file restates the two statements with the almost-everywhere
hypotheses of average_over_aePartition: the cells are contained in U, U differs from
their union by a null set, and the equal-volume condition is stated through .toReal.
The new hypotheses are implied by the old ones — hcover gives containment and a null
difference, and the equal-volume identity in ℝ≥0∞ gives its .toReal form once U has
finite measure — so these statements are strictly stronger than the exact-cover originals.
The per-cell average of the parent integrand depends on the cell, so the abstract recombination
carries gavg : iota → ℝ; the right-hand side is the parent average.
Averaging a per-cell deficit identity over an almost-everywhere finite equal-volume
partition. Suppose the measurable cells V w (w ∈ Z) are pairwise disjoint and contained
in U, that U differs from their union by a null set, and that each cell has the same volume
|V w| = |U| / |Z| stated in .toReal form. If each cell carries the deficit identity
Eng w = 2 (Jchild w − gavg w) for its own parent average gavg w, and the flat average of
those parent averages is Jparent, then the flat average of Eng is twice the difference
between the flat average of Jchild and Jparent. The exact equal-volume cover is replaced
here by the almost-everywhere cover average_over_aePartition.
The cell instance of the quadratic response recombination over an almost-everywhere
partition. The exact cover of the recombination is replaced here by the almost-everywhere
hypotheses: the cells V w (w ∈ Z) are contained in U,
U differs from their union by a null set, and the equal-volume condition is stated through
.toReal. The result is the flat average of the cell difference energies in terms of the flat
average of the cell responses and the parent response:
|Z|⁻¹ ∑_w ⨍_{V w} (∇u − ∇v_w) · symmPart(a) (∇u − ∇v_w) = 2 (|Z|⁻¹ ∑_w J(V w) − J(U)).
Because the difference energy is written with the parent gradient ∇u, the gradients of the
restrictions of u agree with ∇u definitionally and no separate rewriting hypothesis is
needed.
The recombined quadratic-response identity at the aligned adapted cells. For an
invertible grid q, generation t and depth n, the partition geometry of
avg_difference_energy_eq_responseJ_deficit_ae is supplied by the tree's cell lemmas: the
depth-n subcells of HighContrast.adaptedCell q t are open hence measurable, pairwise disjoint,
contained in the parent, omit only the null grid seams, and have equal volume, and the parent
cell has positive finite volume. The elliptic, maximizer and integrability data are not
available from IsUnit q alone and remain explicit hypotheses.
The response functional as a coarse-block quadratic form on an aligned subcell #
The scalar response ResponseJ U p r a of AK.HC (2.9) is evaluated at the canonical
coarse-block quadratic expression p·(A(-p, r))/2 - p·r whenever U is an open bounded
convex domain carrying an elliptic representative of a, by
responseJ_eq_block_quadratic_of_isOpenBoundedConvexDomain
(HCPoly/Entry/CG/Proofs/AdaptedDomainRecovery.lean). The recentred coefficients a_- = a - g and
a_+ = aᵀ + g carry such a representative on the parent adapted cell ⋄_t^q and, via
exists_elliptic_representative_respCoeffMinusAt / …PlusAt, on every aligned triadic
subcell adaptedCellAtCenter q k w.
This module exposes that evaluation publicly, for the parent cell and for each aligned subcell, so that the cell-average estimate of AK.HC (2.15) can be consumed downstream. Nothing new is proved here: each statement is the general bounded-convex-domain formula transported along the a.e. equality of the elliptic representative.
The aligned subcell #
AK.HC (2.15) on an aligned subcell, minus sign. For the recentred coefficient
a_- = a - g, the response functional on the aligned adapted subcell adaptedCellAtCenter q k w
equals the coarse-block quadratic expression (-p, r)·(A_{kw}(-p, r))/2 - p·r, where
A_{kw} is the coarse block matrix of a_- on that subcell.
AK.HC (2.15) on an aligned subcell, plus sign. The adjoint twin for the transposed
recentred coefficient a_+ = aᵀ + g.
The parent adapted cell #
AK.HC (2.15) on the parent adapted cell, minus sign. The public counterpart of the
parent-cell evaluation, for the recentred coefficient a_- = a - g.
AK.HC (2.15) on the parent adapted cell, plus sign. The adjoint twin for the
transposed recentred coefficient a_+ = aᵀ + g.