High-contrast homogenization: Entry.Response.Kernel.RecentredCarrierHypotheses #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The recentred per-cell hypotheses at the estimate's own carriers #
For the recentred coefficient a_- = a - g, this file supplies the two per-cell hypotheses the
diagonal weak-norm estimate needs at its own carriers: the older-scale tail's per-cell bound,
controlling the metric square of a transported parent-cell average by the printed geometric square
times twice the subcell energy average, and the head's per-cell bound, obtained by carrying a
pointwise elliptic representative of the recentred coefficient since IsEllipticFieldOn is
pointwise while a point of CoeffSpace is only an almost-everywhere class. It then bounds the
finite-window head of the cell-average estimate l.weaknorms.moreproto by two finite defect sums,
using a per-cell metric bound for the recent parent/child optimizer difference together with an
averaged bound on the difference energies, both now available at the estimate's own grid.
The tail's per-cell hypothesis at the estimate's own carriers #
scaleTail_carrier (CentredVarianceTailRoute.lean) is the per-scale older-scale bound
at the estimate's carriers. Its only analytic input is hcell: for every aligned depth-n
subcell, the metric square of the transported cell average of the parent optimizer field is
bounded by the printed geometric square times twice the subcell energy average.
parentEnergyMap_port (ParentEnergyMapPort.lean) proves exactly that shape, but
at a pointwise elliptic representative of the recentred coefficient and with the subcell energy
written through the restricted Chapter-2 solution z. This module supplies that data from the
parent harmonic optimizer and transports the port's conclusion back to the estimate's carrier.
The transport uses the pointwise elliptic representative of the recentred field on the parent
cell (exists_globally_elliptic_representative_ae_eq_on): it is the same field on every aligned
subcell, so the parent optimizer is harmonic against it there, and it is a.e. equal to
respCoeffMinus F a on the parent cell, so the cell average and the energy density are unchanged.
Book.Ch02.Solution.ofAEEq / Response.aHarmonicOfAEEq and the restriction
exists_restrict_solution_adaptedCellAtCenter produce the restricted Chapter-2 solution. Finally
weakOptimizerEnergy_sq and a.e. invariance replace the port's energy square by the
estimate's volume average.
The per-cell hypothesis of the older-scale tail. For an invertible selected grid, a
generation t, a depth n, and a parent harmonic optimizer attached to the recentred response
coefficient, every aligned depth-n subcell satisfies the per-cell metric bound of
scaleTail_carrier: the transported cell-average metric square of the parent optimizer field
is at most the printed geometric square times twice its energy average. The bound is the
port parentEnergyMap_port at a pointwise elliptic representative, transported back along the
a.e. equality of the representative with respCoeffMinus F a; the cell-average step and the energy
step are both a.e. invariant.
The head's per-cell hypothesis at the estimate's own carriers #
tailCell_of_bridge supplies the per-cell hypothesis of the older-scale tail by carrying a
pointwise elliptic representative of the recentred coefficient: IsEllipticFieldOn is
pointwise, while a point of CoeffSpace d is only an a.e. class, so the recentred field cannot be
fed to the port directly. This module performs the same representative transport for the
recent difference instead of the parent state.
The port is recentEnergyMap_port, whose data are the parent optimizer restricted to each
aligned subcell and a child optimizer attached to the same coefficient there. The difference of
the two optimizer fields is a single doubled state on the subcell, and on the subcell the
pointwise block identity X · 𝐀 X = 2 ξ · a ξ converts the port's Chapter-2 difference energy
into the estimate's 2 * volumeAverage shape. Both the cell average and the energy average are
a.e. invariant under the representative, so the conclusion returns to respCoeffMinus F a.
The per-cell hypothesis of the head's recent difference. For an invertible selected grid,
a generation t, a depth n, a parent harmonic optimizer attached to the recentred response
coefficient and a child optimizer on every aligned depth-n subcell, the transported cell-average
metric square of the difference of their optimizer fields is at most the printed geometric square
times twice the difference energy average there.
The bound is the recent-difference port recentEnergyMap_port at a pointwise elliptic
representative of respCoeffMinus F a, transported back along the a.e. equality of the
representative with respCoeffMinus F a. The port's right-hand side, the Chapter-2 average of the
doubled block energy density of the difference, is converted to the estimate's 2 * volumeAverage
through the pointwise identity for a doubled state (ξ, a ξ); both the cell average and the energy
average are a.e. invariant, so the conclusion is stated at respCoeffMinus F a.
The finite-window head of the cell-average estimate, at the estimate's own carriers #
The recent head of l.weaknorms.moreproto is bounded by the two finite defect sums once two
analytic facts are supplied at each depth: a per-cell metric bound for the recent difference of
the parent optimizer and a child optimizer, and an averaged bound for the difference energies.
Both are now available at the estimate's own grid, sample, metric and maximizer, so the head
carries no analytic hypothesis of its own: the coefficient's positive definiteness comes from the
law-integrability of the coarse block on the cell, and every geometric input from invertibility of
the selected grid.
The finite-window head of the cell-average estimate, at the carriers. On the branch
where the all-scale maximum does not exceed 1, the 3^{-n/2}-weighted sum over the window
n ≤ H of the normalized L² averages of the recentred transported subcell averages is bounded
by 16 K L times the sum of the two finite defect sums, where K is the square root of the
printed spectral bound of the normalized reference block and L the square root of the response
load.