High-contrast homogenization: Entry.Response.Direct.FirstErrorRowArithmetic #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The scalar arithmetic and abstract bookkeeping behind the first error row #
Bounding the pointwise defect |E - J| ≤ D + 2√(J D) between the terminal response and half the
restricted terminal-optimizer energy needs the square root replaced by the family
2√(JD) ≤ εJ + D/ε, integrated for each ε > 0 and optimized afterward; this file proves the
scalar inequalities making that work, then bounds, in abstract bookkeeping terms, the aligned-cell
average of the weighted energy defect once each subcell carries a response, a half-energy, and a
deficit obeying the pointwise bound. Separately, the cutoff's within-cell oscillation against the
terminal-optimizer energy on each aligned subcell is bounded by the cutoff class's Lipschitz gain
3^{-H} times that energy, twice the pathwise response at a maximizer. Finally, the modulus of the
cutoff pairing of the cutoff estimate is shown almost-everywhere strongly measurable in the
coefficient sample for an arbitrary maximizer family, as the signed cutoff-pairing row needs for
integrability. Altogether this is the scalar and abstract bookkeeping core of the first error row
of p.response.transfer.
The cutoff pairing is measurable in the sample without its absolute value #
CutoffQuadraticReadout records that the MODULUS of the cutoff pairing of
e.response.cutoff.estimate is almost-everywhere strongly measurable in the coefficient sample for
an arbitrary family of response maximizers. The row assembly
abs_respCenteredJ{Minus,Plus}_le_cutoffRows_of_obligations needs the P-integrability of the
SIGNED pairing, which the modulus alone does not give: an integrable modulus supplies the finite
integral but not the measurability of the signed function.
The signed measurability follows by the same route, and with no further input. The doubled
optimizer state of an arbitrary response maximizer agrees almost everywhere on the terminal cell
with the measurable canonical Chapter-2 selection, so the signed pairing agrees with the canonical
signed pairing; and the canonical signed pairing is measurable by
aestronglyMeasurable_pairing_canonical_of_quadratic, whose quadratic input is discharged with no
hypothesis beyond the cutoff class by
measurable_volumeAverage_cutoff_quadratic_canonicalRespCoeff{Minus,Plus}_full. Together with the
integrability of the modulus, which p.response.transfer already carries, this closes
the hA side condition of the row assembly.
The canonical signed cutoff pairing is measurable, minus recentring. With no hypothesis beyond the cutoff class: the three linear readouts of the canonical optimizer state are measurable, and so is the quadratic one.
The canonical signed cutoff pairing is measurable, plus recentring. The adjoint twin of
aestronglyMeasurable_canonical_cutoff_pairing_respCoeffMinus.
The signed cutoff pairing of an arbitrary maximizer family is measurable, minus recentring. The doubled optimizer state of the maximizer agrees almost everywhere on the terminal cell with the canonical Chapter-2 selection, so the two pairings agree sample by sample.
The signed cutoff pairing of an arbitrary maximizer family is measurable, plus
recentring. The adjoint twin of
aestronglyMeasurable_cutoffPairingOnCell_respCoeffMinus.
The hA side condition of the row assembly, minus recentring. The half-weighted signed
cutoff pairing is P-integrable: its modulus is integrable by the premise that
p.response.transfer already carries, and the signed function is measurable. The modulus is
stated through cutoffPairingOnCellAux, which is the same function as the kernel's
hc3CutoffPairingOnCell -- the two definitions have identical bodies, so the premise
discharges habs directly.
The hA side condition of the row assembly, plus recentring. The adjoint twin of
integrable_half_cutoffPairingOnCell_respCoeffMinus.
The cutoff oscillation against the terminal-optimizer energy #
In the terminal-optimizer replacement of p.response.transfer, the cutoff fluctuation φ - 1 is
split on each aligned subcell of the coarse scale into its subcell mean and its oscillation there.
The oscillation part costs the Lipschitz gain 3^{-H} of the cutoff class times the energy of the
terminal optimizer, which at a maximizer is twice the pathwise response. This module records that
step for the optimizer's energy density, replacing the general nonnegative density of the
oscillation split by the concrete one the estimate uses.
Paper: p.response.transfer.
The cutoff oscillation of the terminal-optimizer energy. On the adapted cell ⋄_t^q, for
a cutoff φ of the response class and a response maximizer u of the loads (p, r), the
(φ − 1)-weighted optimizer energy differs from the normalized sum of the products of the subcell
means of φ − 1 and of the energy by at most the oscillation cost
32 d² responseCutoffProfileConst 3^{-n} times twice the pathwise response J(⋄_t^q; p, r; b).
The variation energy of the terminal optimizer is nonnegative only on the cell, so the oscillation
split is applied to its positive part, which agrees with it there, and at a maximizer the
cell-average energy is exactly 2 J. This is the scale-gain step of the cutoff estimate of
p.response.transfer.
Scalar arithmetic for the first error row #
The first error row of p.response.transfer is assembled by integrating a pointwise bound
|E - J| ≤ D + 2 √(J D). Because the square root carries no measurability hypothesis, the
integrand is replaced by the one-parameter family 2 √(J D) ≤ ε J + D / ε, integrated for each
ε > 0, and optimized only at the end. This module supplies the scalar inequalities behind that
replacement together with the subadditivity that turns √(τ (E + τ)) into √(τ E) + τ.
two_mul_sqrt_mul_le_eps_add_div— the one-parameter Young bound on the cross term.le_add_two_mul_sqrt_of_forall_pos— optimization of the parameter at the end.sqrt_mul_add_le_sqrt_mul_add— splitting the terminal-scale annealed response.
Paper: the first error row of p.response.transfer.
The first error row in abstract bookkeeping form #
The terminal-optimizer replacement of p.response.transfer, after the terminal cell is subdivided
into the aligned coarse cells, reduces to the following bookkeeping. Each subcell carries three
sample functions: the response J, half the restricted terminal optimizer energy E, and the
nonnegative deficit D between them, compared pointwise by |E - J| ≤ D + 2 √(J D). The weights
c are the subcell means of the cutoff fluctuation and average to zero, stationarity makes the
annealed response ∫ J the same cJ on every subcell, and the annealed flat average of the
deficits is the scale defect τ.
The weighted average of the half-energies then has expectation at most τ + 2 √(τ cJ): the
J-part is annihilated by the mean-zero weights, and the remainder is controlled by the deficits
through the one-parameter Cauchy--Schwarz bound 2 √(J D) ≤ ε J + D / ε.
Paper: p.response.transfer.
The abstract first error row. Under the pointwise comparison |E - J| ≤ D + 2 √(J D), a
common annealed response ∫ J w = cJ, a mean-zero normalized weighting c, and an annealed
flat deficit τ, the expectation of the weighted average of the half-energies is at most
τ + 2 √(τ cJ). This is the bookkeeping content of the terminal-optimizer replacement of the
first error row of p.response.transfer.