High-contrast homogenization: Entry.Response.Rows.CarrierIntegrabilityConditions #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Side Conditions of the Cutoff-Mean Row at the Carriers #
Since a response maximizer's doubled optimizer field is determined, up to a null set, by the
coefficient sample alone, every cutoff-weighted average of a coordinate of that field over a
measurable subcell is measurable in the sample, and so is the weighted cell average of the
crossed pairing ⟨Y₂, ∇u⟩ + ⟨Y₁, a ∇u⟩ against a deterministic state Y.
Recentring by a constant skew matrix is a block congruence, so the entries of the pathwise coarse
block of a_- = a - g and a_+ = a^T + g are fixed linear combinations of the sample's own
coarse-block entries and inherit its integrability. The two-term head √(P · b P) + √(Q · S_*^{-1} Q) then inherits, from this and the nonnegativity of its two quadratic forms, the
integrability of its cross term and of its own square; it also records the P-integrability of
the annealed cell energy of the terminal optimizer on a descendant cell. These are the carrier
side conditions of the cutoff-mean row of p.response.transfer.
Weighted cell averages of the crossed pairing are measurable in the sample #
The oscillation half of the cutoff-mean row of p.response.transfer reads, on each cell V of a
triadic refinement of the terminal cell, the weighted cell average of the scalar crossed pairing
⟨Y₂, ∇u⟩ + ⟨Y₁, a ∇u⟩ of the terminal optimizer against the deterministic dual variable Y.
Because Y is deterministic, that scalar is a fixed linear combination of the 2d coordinates of
the doubled optimizer state, so its weighted cell average is the same linear combination of the
2d weighted coordinate averages, each of which is measurable in the sample by
DescendantFenchelProbe. The coordinate averages are finite by TerminalDeficitCarrierBound,
which needs
only continuity of the weight.
The weighted cell average of the crossed pairing is measurable in the sample, minus sign.
For a continuous weight whose indicator is square-integrable on the terminal cell and any
measurable subcell V, the V-average of eta · (⟨Y₂, ∇u⟩ + ⟨Y₁, a_- ∇u⟩) is a measurable
function of the coefficient sample, for an arbitrary family of terminal maximizers.
The weighted cell average of the crossed pairing is measurable in the sample, plus sign.
The adjoint twin of
measurable_volumeAverage_weighted_cross_optimizerField_respCoeffMinus.
The unweighted cell average of the crossed pairing is measurable in the sample, minus
sign. The constant-weight case of
measurable_volumeAverage_weighted_cross_optimizerField_respCoeffMinus; the indicator of a
measurable subcell by the constant 1 is square-integrable on the terminal cell.
The unweighted cell average of the crossed pairing is measurable in the sample, plus
sign. The adjoint twin of
measurable_volumeAverage_cross_optimizerField_respCoeffMinus.
Entrywise integrability of the recentred coarse block on an aligned cell #
The cell half of the cutoff-mean row of p.response.transfer needs, on every coarse subcell, the
P-integrability of the individual entries of the pathwise coarse block of the recentred
coefficients a_- = a - g and a_+ = aᵀ + g. Recentring by a constant skew matrix is a block
congruence, so those entries are fixed real linear combinations of the entries of the coarse block
of the sample itself, which HasIntegrableCoarseBlock supplies. This module records that
integrability for the four sub-block entries used by the annealed heads, together with the
AEStronglyMeasurable forms at the centred cell that the stationarity collapse consumes.
Integrability of the upper-left block of the recentred coarse block. For the unit grid
q = respGrid jStar F, a scale j and an aligned cell index w, if every entry of the coarse
block of the sample is P-integrable there, then every entry of the upper-left sub-block of the
pathwise coarse block of a_- = a - g is P-integrable.
Integrability of the lower-right block of the recentred coarse block. The lower-right twin
of integrable_coarseBlockMatrix_upperLeft_respCoeffMinus.
Integrability of the upper-left block of the adjoint recentred coarse block. For the unit
grid q = respGrid jStar F, a scale j and an aligned cell index w, if every entry of the
coarse block of the sample is P-integrable there, then every entry of the upper-left sub-block
of the pathwise coarse block of a_+ = aᵀ + g is P-integrable.
Integrability of the lower-right block of the adjoint recentred coarse block. The
lower-right twin of integrable_coarseBlockMatrix_upperLeft_respCoeffPlus.
The side conditions of the two-term head on the carriers #
The cell half of the cutoff-mean row of p.response.transfer carries, for each coarse cell, the
two-term head √(P · b P) + √(Q · (S_*)^{-1} Q) built from the two diagonal blocks of that cell's
pathwise coarse block. This module discharges the side conditions the head needs on the carriers:
the nonnegativity of its two quadratic forms, their integrability from the entrywise integrability
of the coarse block, and the integrability of the cross term and of the square of the head. The
last two are consequences of the arithmetic--geometric mean inequality and the nonnegativity of the
two summands: √α √β ≤ (α + β)/2 and (√α + √β)^2 ≤ 2(α + β).
Nonnegativity of the two diagonal coarse-block forms #
Integrability of the two diagonal coarse-block forms #
The upper-left diagonal coarse-block form is integrable from its entries. If every entry
of the upper-left block of 𝐀(V; b a) is P-integrable, then so is the quadratic form
Y.1 · (𝐀(V; b a).upperLeft Y.1): it is a finite sum of products of entries with the constants
Y.1 i, Y.1 j. This is the upper-left integrability input of the two-term head of
p.response.transfer.
The lower-right diagonal coarse-block form is integrable from its entries. The
lower-right twin of integrable_vecDot_coarseBlockMatrix_upperLeft: entrywise integrability of
the lower-right block makes the form Y.2 · (𝐀(V; b a).lowerRight Y.2) P-integrable, the second
integrability input of the two-term head of p.response.transfer.
Integrability of the cross term and of the square of the head #
Integrability of the square of the head (√α + √β)^2 for nonnegative integrable α, β.
From √α √β ≤ (α + β)/2 one gets (√α + √β)^2 ≤ 2(α + β), an integrable domination, with
measurability supplied by continuity of Real.sqrt. This is the squared-head integrability of
the two-term head of p.response.transfer.
Integrability of the square of the two-term head on the carriers. The square of the head
√(Y.1 · 𝐀(V; b a).upperLeft Y.1) + √(Y.2 · 𝐀(V; b a).lowerRight Y.2) is P-integrable
whenever its two diagonal coarse-block forms are nonnegative and integrable. This is the
squared-head side condition of p.response.transfer.
The annealed cell energy of the terminal optimizer on a descendant cell #
The oscillation half of the cutoff-mean row of p.response.transfer reads the cell energy of the
terminal optimizer on every descendant cell of the terminal cell.
TerminalHalfEnergyIntegrability makes that
readout P-integrable on the aligned cells of one fixed generation, from the integrability of the
terminal energy and the measurability of SubcellEnergyIntegrability; the descendant generation
t - (H + n + 1) is that statement at the shifted scale s - (n + 1) and the deeper index box,
because the terminal cell is the same cell either way.
The annealed cell energy on a descendant cell, minus sign. The cell energy of the terminal
optimizer on a cell of the generation t - (H+n+1) is P-integrable.
The annealed cell energy on a descendant cell, plus sign. The adjoint twin.