High-contrast homogenization: Entry.Response.Rows.CutoffEnergyDefectRowObligations #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The first error row as a named, monotone obligation #
The first error row of p.response.transfer, proved in the adjoint configuration from a list of
pathwise and sample-side hypotheses, is discharged here on the response's own data for that sign:
every pathwise ingredient — the energy-defect identity, the oscillation split, the subcell
comparison, the two cutoff-weight facts, and the relevant signs — is supplied directly. The cutoff
estimate consumes this replacement bound in the predicate form of two named obligations, one per
sign, and on the response's own data that obligation is exactly the replacement bound already
proved, once its three remaining sample-side integrability hypotheses — the subcell deficits, the
subcell energies, and the cutoff-weighted terminal energy — are shown to follow from the data the
row already carries. Because the energy-defect row and the cutoff-mean row are produced with
different constants, a final pair of monotonicity lemmas records that raising either constant
preserves the corresponding bound, so both rows can be read at one common constant.
The first error row on the carriers, side conditions discharged (adjoint sign) #
The first error row of p.response.transfer is proved in the adjoint configuration by
abs_integral_cutoffHalfEnergy_sub_respJ_le_rowPlus from fifteen hypotheses. Every one of them
that is a pathwise statement — the energy-defect identity, the oscillation split, the subcell
comparison, the two cutoff-weight facts, the three signs, the stationarity of the annealed subcell
response and the scale-defect identity — is available on the carriers of the cutoff estimate
without any pointwise ellipticity hypothesis, because a coefficient of the carrier is elliptic only
almost everywhere and the transport along an a.e.-elliptic representative has been built. This
module assembles those statements and leaves only the sample integrabilities as hypotheses:
- the terminal and coarse pathwise responses are
P-integrable; - the subcell response deficits and the averaged optimizer energies are
P-integrable; - the cutoff-weighted optimizer energy is
P-integrable.
The conclusion is the printed bound
C (τ^+ + (τ^+ E[J_t^+])^{1/2} + 3^{-H} E[J_t^+]) with the explicit dimensional constant
C = max 3 (32 d^2 responseCutoffProfileConst).
Paper: p.response.transfer.
The terminal-optimizer replacement row on the cutoff carriers, adjoint sign, side
conditions discharged. Under a stationary probability law on the coefficient carrier, let uP
be a terminal optimizer for the adjoint recentred coefficient a_+ = aᵗ + g, φ a cutoff of the
response class, and suppose the annealed pathwise responses at the terminal and coarse scales are
P-integrable, the subcell response deficits, the averaged subcell optimizer energies and the
cutoff-weighted optimizer energy are P-integrable. Then the law-integral of the cutoff
half-energy of uP minus the terminal response is at most
max 3 (32 d^2 responseCutoffProfileConst) times
τ^+ + (τ^+ E[J_t^+])^{1/2} + 3^{-H} E[J_t^+]. All pathwise side conditions are supplied by the
a.e.-elliptic representative transport, so no pointwise ellipticity is assumed. This is the first
error row of p.response.transfer on the carriers of the cutoff estimate.
The first error row of p.response.transfer as the named obligation #
The cutoff estimate of e.response.cutoff.estimate consumes the first error row of
p.response.transfer — the cost of replacing the terminal optimizer by the coarse-cell
optimizers — in the predicate form CutoffEnergyDefectRowMinus, and its adjoint twin
CutoffEnergyDefectRowPlus. On the response carriers that row is the replacement bound with the
explicit dimensional constant max 3 (32 d^2 responseCutoffProfileConst).
The two declarations here restate the carrier bounds of OptimizerRowSideConditions and
CutoffEnergyDefectRowObligations directly as those predicates, so that the row assembly of the
cutoff
estimate can consume them without unfolding the predicate at each use site.
The first error row of p.response.transfer on the response carriers, as
CutoffEnergyDefectRowMinus. Under the hypotheses of the carrier bound, the law-integral of the
cutoff half-energy of the terminal optimizer minus the terminal response is at most
max 3 (32 d^2 responseCutoffProfileConst) times
τ^- + (τ^- E[J_t^-])^{1/2} + 3^{-H} E[J_t^-], which is exactly the named obligation
CutoffEnergyDefectRowMinus used by e.response.cutoff.estimate.
The first error row of p.response.transfer on the response carriers, as
CutoffEnergyDefectRowPlus. This is the adjoint-sign twin of
cutoffEnergyDefectRowMinus_of_carriers: under the hypotheses of the carrier bound for the
terminal optimizer uP of the adjoint recentred coefficient, the law-integral of the cutoff
half-energy of uP minus the terminal response is at most
max 3 (32 d^2 responseCutoffProfileConst) times
τ^+ + (τ^+ E[J_t^+])^{1/2} + 3^{-H} E[J_t^+], which is exactly the named obligation
CutoffEnergyDefectRowPlus used by e.response.cutoff.estimate.
The terminal-optimizer replacement row with no sample-side residue #
The terminal-optimizer replacement row of p.response.transfer — the first error row of
e.response.cutoff.estimate — was stated on the response carriers with three sample-side
integrability hypotheses left open: the subcell deficits, the subcell energies, and the
cutoff-weighted terminal energy. All three follow from the data the row already carries, so the
row holds with no sample-side residue beyond the measurability of the subcell energies.
The two declarations below restate cutoffEnergyDefectRowMinus_of_carriers and its adjoint twin
with those three integrability hypotheses removed, discharging them from the subcell-energy
measurability as an almost-everywhere strong measurability.
The first error row of p.response.transfer on the response carriers with no sample-side
residue, minus sign. Under the hypotheses of the carrier bound for the terminal optimizer uM
of the recentred coefficient a_- = a - g, only the subcell-energy measurability
(hmeasE) is assumed: the integrability of the subcell deficits, of the subcell energies and of
the cutoff-weighted terminal energy follows from it, together with the annealed data already
carried. The conclusion is the named obligation
CutoffEnergyDefectRowMinus at the explicit constant
max 3 (32 d^2 responseCutoffProfileConst).
The first error row of p.response.transfer on the response carriers with no sample-side
residue, plus sign. This is the adjoint twin of
cutoffEnergyDefectRowMinus_of_carriers_of_measurable: the coefficient family a_+ = aᵀ + g, the
dual load q^+ and the terminal optimizer family uP replace their minus-sign counterparts, and
the subcell-energy measurability discharges the same three sample-side integrabilities. The
conclusion is the named obligation CutoffEnergyDefectRowPlus at the explicit constant
max 3 (32 d^2 responseCutoffProfileConst).
The terminal-optimizer replacement row of p.response.transfer on the carriers, minus
sign. The row holds with no sample-side hypothesis beyond the annealed data it already carries:
the measurability of the subcell energies is supplied by the canonical selection, and the three
integrabilities of the subcell deficits, of the subcell energies and of the cutoff-weighted
terminal energy follow by domination.
The terminal-optimizer replacement row of p.response.transfer on the carriers, plus
sign. The adjoint twin of cutoffEnergyDefectRowMinus_of_carriers_clean.
The two named error rows are monotone in their constant #
The energy-defect row and the cutoff-mean row of p.response.transfer are produced with different
constants — max 3 (32 d² Θ) and max 1 (respCutoffOscConst d) — while the row assembly consumes
both at one common constant. Both right-hand sides are the constant times a nonnegative quantity,
so raising the constant preserves the bound.
The energy-defect row weakens as the constant grows.
The adjoint energy-defect row weakens as the constant grows.
The cutoff-mean row weakens as the constant grows.
The adjoint cutoff-mean row weakens as the constant grows.