High-contrast homogenization: Entry.Response.Kernel.AdjointHeadEnergyCarrier #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The adjoint head hypothesis, and the degenerate-metric discharge #
For the adjoint recentred coefficient, this file supplies the averaged-energy hypothesis the
diagonal weak-norm estimate's finite-window head needs at its own carriers: an
almost-everywhere-equal elliptic representative transports the parent and child maximizers to it,
and the resulting bound back, leaving no pointwise ellipticity or coefficient-dependent
integrability hypothesis in the conclusion. It then discharges, at the level of the cell-average
lemma itself, the first of the degenerate-metric branches of the estimate's primal bound: when the
underlying grid fails to be a unit, the coarse block's canonical metric and its response matrix
respM0 fail to be positive definite together, so the pointwise estimate continues to make sense.
It serves the weak-norm estimate e.response.weak.estimate and the cell-average estimate
l.weaknorms.moreproto.
The averaged-energy hypothesis of the cell-average estimate at the estimate's carriers, adjoint #
sign
The cell-average estimate of the weak-norm bound (e.response.weak.estimate) consumes, at each
depth n, a per-cell family whose flat average over the triadic index box is bounded by the
printed product of the response load and the operator norm of the averaged normalized block
defect. The per-cell half of that estimate produces G w as twice the scalar difference energy
of the maximizers u and v w on the aligned subcell
adaptedCellAtCenter (respGrid jStar F) (t - n) w:
G w = 2 ⨍_{V w} (∇u − ∇v_w) · symmPart(a_+) (∇u − ∇v_w).
The response identity that turns the flat average of those difference energies into the averaged
response deficit is stated for a coefficient that is pointwise elliptic on the cell. The
transposed recentred coefficient a_+ = respCoeffPlus F a is only an almost-everywhere class and
is never elliptic pointwise, so the identity cannot be instantiated at it directly. This module
runs the identity at an almost-everywhere-equal elliptic representative of a_+, transports the
maximizers to that representative, and transports the conclusion back: every quantity in the
conclusion is almost-everywhere invariant in the coefficient. The result therefore carries none
of the pointwise ellipticity or coefficient-dependent integrability hypotheses that the
representative argument removes.
The algebraic tail is the printed chain: the pointwise identity
optimizerField b u − optimizerField b v = (∇u − ∇v, b (∇u − ∇v)) turns the doubled optimizer
difference energy into the symmetric scalar difference energy, the recombined quadratic-response
identity rewrites the flat average of the difference energies as twice the deficit of the response
functional, each response value is the coarse-block quadratic form of its cell, and the averaged
response deficit is the quadratic form of the averaged block defect, bounded by the normalized
Loewner comparison through the response load and the operator norm of the averaged normalized
defect. See e.response.weak.estimate.
The averaged-energy hypothesis of the cell-average estimate, with no pointwise ellipticity
hypothesis. For the per-cell family that is twice the scalar difference energy of the
maximizers u and v w on the aligned subcells
adaptedCellAtCenter (respGrid jStar F) (t - n) w, the flat average over the triadic index box is
bounded by twice the response load times the operator norm of the averaged normalized block
defect weakAverageDefect.
The identity is run at an almost-everywhere-equal representative f of respCoeffPlus F a that
is pointwise elliptic on the parent adapted cell; the parent and child maximizers are transported
to f along the almost-everywhere equality, and the resulting identity is transported back
because both the scalar difference energy and each response value depend on the coefficient only
through its almost-everywhere class. No pointwise ellipticity and no coefficient-dependent
integrability hypothesis remains. See e.response.weak.estimate.
The cell-average lemma on the degenerate metric branch #
The cell-average estimate l.weaknorms.moreproto is stated for an arbitrary doubled block F,
so its metric m = explicitCanonicalMetric F may degenerate. DiagonalDefectCarriers.lean
classifies the degenerations; this file cashes the first of them in at the level of the estimate
itself.
Two statements:
- the right-hand side of the estimate is nonnegative for every
γ ∈ [0,1)— every factor is a square root, a nonnegative weight, or one of the two nonnegative finite sums, and the only hypothesis used isγ < 1, which makes the printed coefficient16 / (1 - ρ(γ))positive; - when the metric vanishes the estimate holds outright, because
M₀^{1/2}annihilates every doubled vector, so the whole left-hand side is0.
Together these close the branch ¬ IsUnit (explicitCanonicalMetric F).det of the estimate, which by
explicitCanonicalMetric_eq_zero_of_not_isUnit is exactly the branch explicitCanonicalMetric F = 0.
Two further statements record that, at the estimate's own binders, that branch is in fact EMPTY:
the estimate carries IsUnit (respGrid jStar F), and the metric dichotomy
explicitCanonicalMetric_posDef_or_det_roundedGrid_eq_zero — which holds for an arbitrary F,
with no
symmetry and no positivity — turns a unit grid into a positive definite metric, hence into a
positive definite M₀. So the M₀ positivity that the recent-head chain asks for is free at
the estimate, and the degenerate metric branches never arise there.
The metric of F is positive definite as soon as the selected grid is a unit. The metric
dichotomy holds for an arbitrary doubled block, so no symmetry or positivity of F is needed:
a degenerate metric forces a singular grid, which a unit grid excludes.