High-contrast homogenization: Entry.Response.Rows.CutoffEstimateRowClosure #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Closing the cutoff estimate's mean row from its cell and oscillation halves #
Once the pathwise cutoff-pairing identity is available for a genuine cutoff of the response class,
the three-row bound on the centred responses Jtilde^±(e) holds outright, reducing what the
cutoff estimate still needs to two named analytic obligations: a bound on the energy-defect row and
a bound on the cutoff-mean row, for each sign. The cutoff-mean row bounds the crossed pairing of the
cutoff-mean defect against the dual variable by C(τ L_s)^{1/2} + C 3^{-H}(E[J_t] L_s)^{1/2}
(p.response.transfer), and this file supplies that bound by splitting the defect into a cell
part, costing (2 τ L_s)^{1/2}, and an oscillation part, already of the printed size
c₂ 3^{-H}(E[J_t] L_s)^{1/2}. Together the two obligations close the row decomposition down to the
four elementary quantities τ^±, E[J_t^±], L_s^±, and the expected absolute cutoff pairing.
The centred response against its three cutoff rows, with the pathwise identity discharged #
The centred responses Jtilde^±(e) of e.response.cutoff.estimate are bounded by the three cutoff
rows of the printed variational calculation once the cutoff pairing is decomposed pathwise into the
cutoff half-energy, the two cutoff-mean pairings and half the self-pairing of the annealed mean.
For a cutoff of the response class — in particular one of cell average one — that decomposition is
not an extra assumption: it follows from the integrability of the cutoff-weighted optimizer state
against the cell. These two statements therefore replace the pathwise identity of
RecentredResponseEnergyBound by the membership of the cutoff and the indicated cell
integrabilities.
The centred response against its three cutoff rows (e.response.cutoff.estimate,
AK.HC (3.45)-(3.54)), minus carriers, with the pathwise identity discharged from cutoff
membership. The cutoff φ is a response cutoff on the cell U_t — so in particular it has cell
average one — and the cutoff-weighted optimizer state is integrable against that cell. Under these
hypotheses the half-pairing (1/2) * cutoffPairingOnCellAux is pathwise the affine combination
of the cutoff half-energy, the two cutoff-mean coordinates and half the self-pairing of the
annealed mean Y^-, so |Jtilde^-(e)| is bounded by the sum of the expected absolute cutoff
pairing, the absolute cutoff energy defect E[cutoffHalfEnergy - J], and the CENTRED cutoff-mean
row (1/2) |<E[M₁] - Y₁^-, Y₂^-> + <Y₁^-, E[M₂] - Y₂^->|.
The centred response against its three cutoff rows (e.response.cutoff.estimate,
AK.HC (3.45)-(3.54)), plus carriers, with the pathwise identity discharged from cutoff
membership. The cutoff φ is a response cutoff on the cell U_t — so in particular it has cell
average one — and the cutoff-weighted optimizer state is integrable against that cell. Under these
hypotheses the half-pairing (1/2) * cutoffPairingOnCellAux is pathwise the affine combination
of the cutoff half-energy, the two cutoff-mean coordinates and half the self-pairing of the
annealed mean Y^+, so |Jtilde^+(e)| is bounded by the sum of the expected absolute cutoff
pairing, the absolute cutoff energy defect E[cutoffHalfEnergy - J], and the CENTRED cutoff-mean
row (1/2) |<E[M₁] - Y₁^+, Y₂^+> + <Y₁^+, E[M₂] - Y₂^+>|.
The two analytic rows behind the cutoff estimate #
The cutoff estimate of e.response.cutoff.estimate bounds the centred response Jtilde^±(e) by
the sum of its three error rows and the expected absolute cutoff pairing. The integrated cutoff
decomposition already exhibits those three rows; what the printed proof still supplies are the two
bounds on the energy defect and on the centred cutoff mean. This module names them as the
predicates CutoffEnergyDefectRowMinus and CutoffMeanRowMinus (and their Plus twins) and shows
that the printed right-hand side of the estimate follows from them together with the decomposition,
by linear arithmetic on the half-weighted pairing row.
The first error row of the estimate, as a named obligation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The second and third error rows of the estimate, as a named obligation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The three-row decomposition of e.response.cutoff.estimate and the two bounds on its error
rows assemble into the printed right-hand side: if the cutoff energy defect obeys its bound and the
centred cutoff mean obeys its two-row bound, then |Jtilde^-(e)| is bounded by the two rows, the
half-weighted cutoff pairing, and the expected absolute cutoff pairing carried at coefficient one.
The first error row of the adjoint estimate, as a named obligation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The second and third error rows of the adjoint estimate, as a named obligation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The three-row decomposition of e.response.cutoff.estimate and the two bounds on its adjoint
error rows assemble into the printed right-hand side: if the adjoint cutoff energy defect obeys its
bound and the adjoint centred cutoff mean obeys its two-row bound, then |Jtilde^+(e)| is bounded
by the two rows, the half-weighted cutoff pairing, and the expected absolute cutoff pairing carried
at coefficient one.
The cutoff-mean row from its cell and oscillation halves #
The cutoff-mean row of p.response.transfer bounds the crossed pairing of the cutoff-mean defect
against the dual variable by C (tau L_s)^{1/2} + C 3^{-H} (E[J_t] L_s)^{1/2}. The defect splits
into a cell part and an oscillation part: the cell part costs (2 tau L_s)^{1/2}, while the
oscillation part is already of the printed size c₂ 3^{-H} (E[J_t] L_s)^{1/2}. This module is the
purely scalar assembly of the row from those two halves, for both signs, with the coefficient
max 1 c₂.
The cutoff-mean row for the negative sign from its two halves. The coordinatewise mean
defect splits as N = Ncell + Nosc. Bilinearity of vecDot splits the crossed pairing along the
two coordinates into the cell and oscillation halves; the triangle inequality bounds the total by
the sum of the two half-bounds; √L √(2τ) = √2 √(τ L) with √2 / 2 ≤ 1 absorbs the cell factor;
and 1 ≤ max 1 c₂ together with (1 / 2) c₂ ≤ max 1 c₂ absorbs the row's factor 1 / 2.
The cutoff-mean row for the positive sign from its two halves. The adjoint coordinatewise
mean defect splits as N = Ncell + Nosc. Bilinearity of vecDot splits the crossed pairing along
the two coordinates into the cell and oscillation halves; the triangle inequality bounds the total
by the sum of the two half-bounds; √L √(2τ) = √2 √(τ L) with √2 / 2 ≤ 1 absorbs the cell
factor; and 1 ≤ max 1 c₂ together with (1 / 2) c₂ ≤ max 1 c₂ absorbs the row's factor 1 / 2.