High-contrast homogenization: Entry.Response.Kernel.ParentEnergyMapPort #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The parent-optimizer energy map, and the adjoint tail-cell hypothesis #
This file proves the per-cell bookkeeping of the diagonal weak-norm estimate for a single parent
optimizer field: the metric square of the cell average of the parent state is bounded by the
square of the printed geometric factor times the Chapter-2 block energy of the aligned subcell,
first for the recentred sample and then, tracking the extra congruence the flux flip introduces,
for its adjoint twin. It then records the resulting per-scale older-scale bound at the estimate's
own carriers, adjoint sign: 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's response size. It serves the weak-norm estimate
e.response.weak.estimate.
The parent-optimizer energy map on an aligned cell #
This is the per-cell bookkeeping of the weak-norm estimate for the single parent optimizer field instead of a difference. The metric square of the cell average of the parent state is bounded by the square of the printed geometric factor times the Chapter-2 block energy of the aligned subcell, the energy carried by the restricted solution whose gradient agrees with the parent's.
The proof is the recent-difference bookkeeping with the recent-difference metric input replaced by the cell energy bound for the parent optimizer on an aligned subcell.
The parent-optimizer energy map on an aligned cell. For every index w in the triadic box,
the metric square of the cell average of the parent optimizer field on the aligned subcell is
bounded by the printed geometric square times twice the Chapter-2 block energy of the restricted
solution there; that energy is the actual state energy on the subcell, not a difference energy.
The hypothesis hcoarse identifies the Chapter-2 coarse block of the recentred coefficient with
the shear congruence of the subcell's coarse block, exactly as in the recent-difference map.
The parent-optimizer energy map, adjoint sign #
The parent-optimizer energy map of ParentEnergyMapPort is stated for the recentred
sample respEhatMinus. The adjoint copy is needed for the a_+ per-scale input, whose sample is
respEhatPlus = blockAdjoint (respEhatMinus …). Because the adjoint adds one congruence by the
flux flip D, the response-size input is no longer a bound for the shear factor respG F alone:
it is the composed factor D ∘ respG F.
As in the recent-difference adjoint twin, the map is split so that the large block terms are
elaborated once each: the per-cell step carries the two Loewner constants abstract and is the
aligned-subcell instance of the Chapter-2 block energy bound for the parent optimizer, and the
second theorem feeds it the adjoint size inputs. The remaining input of the second theorem is the
identification of the Chapter-2 coarse block of the recentred adjoint field with the composed
congruence of the cell's coarse block; the two coarse-block carriers used here — the Chapter-2
coarseBlockMatrix on a Domain and the set-level coarseBlock on the cell — are not identified
by any declaration in this module's import closure, so that identification is carried as an
explicit hypothesis, exactly as for the minus sign.
The per-cell step of the parent-optimizer energy map for the adjoint sample, with the two
Loewner constants abstract. This is the aligned-subcell Chapter-2 block energy bound for the
parent optimizer u, whose gradient agrees with the restricted solution z: the metric square of
the cell average of the parent state is bounded by the product k * e of the two Loewner sizes
times twice the actual state energy carried by z. The reference sample is respEhatPlus, the
root is blockSqrt (respM0 F), and the response sample and the two Loewner hypotheses are those of
the weak-norm estimate (e.response.weak.estimate).
The parent-optimizer energy map on an aligned cell for the adjoint sample. This is the adjoint
twin of parentEnergyMap_port (ParentEnergyMapPort.lean): the sample is
respEhatPlus, and the response-size input hcoarse identifies the Chapter-2 coarse block of the
recentred field with the composed congruence D ∘ respG F, the factor the adjoint carries. The
per-cell step is parentEnergyMap_cell_plus above.
The tail's per-cell hypothesis at the estimate's own carriers, adjoint sign #
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.
This module is the adjoint twin of tailCell_of_bridge: the parent optimizer is attached to
the transposed recentred response coefficient a_+ = aᵀ + g, and the reference sample is the
adjoint block respEhatPlus. The adjoint parent energy map
parentEnergyMap_port_plus proves the per-cell shape at a pointwise elliptic representative of
the adjoint recentred coefficient and with the subcell energy written through the restricted
Chapter-2 solution. 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 adjoint recentred field on the
parent cell (exists_globally_elliptic_representative_ae_eq_on, which is transposed and shifted by
the skew Schur coefficient): 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 respCoeffPlus 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, adjoint sign. For an invertible selected
grid, a generation t, a depth n, and a parent harmonic optimizer attached to the transposed
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 adjoint
port parentEnergyMap_port_plus at a pointwise elliptic representative, transported back along
the a.e. equality of the representative with respCoeffPlus F a; the cell-average step and the
energy step are both a.e. invariant.