High-contrast homogenization: Entry.Response.Cutoff.CanonicalReadoutMeasurability #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Measurability of the canonical readout, and law-integrability of the response #
This file proves the almost-sure strong measurability of the cutoff-weighted quadratic readout
evaluated at the canonical optimizer state, for both the recentred and adjoint coefficients,
completing the quadratic term of the expansion AK.HC Lemma A.1 (A.4) that the cutoff pairing
of e.response.cutoff.estimate rests on. It also records that the pathwise response
J(U; a_-) of the recentred coefficient is integrable under the coefficient law, using that the
recentring shear G congruence-transports the coarse block of a_- from that of a.
Measurability of the cutoff-weighted quadratic readout of the canonical optimizer #
The cutoff pairing of the response estimate e.response.cutoff.estimate expands, in the notation of
AK.HC Lemma A.1, (A.4), into one quadratic term and three linear terms. The quadratic term is the
cutoff-weighted volume average of the Euclidean pairing of the two slots of the canonical optimizer
state,
a ↦ ⨍_{adaptedCell} φ · ⟨Z(a).1, Z(a).2⟩.
The canonical optimizer state is not the Chapter-2 doubled minimizer: the almost-everywhere
extraction identity reads Z(a).α = X(a).α + (B_a X(a)).α.swap. The cutoff-weighted pairing of Z
is therefore the cutoff-weighted block energy of the minimizer together with twice the plain pairing
of the minimizer. Reading the canonical state directly as the minimizer loses the weighted energy,
so the quadratic readout is not the manifestly continuous functional z ↦ ⨍ φ ⟨z₁, z₂⟩.
This file proves the measurability of the quadratic readout in the coefficient sample for the two
recentred response coefficient families of e.response.cutoff.estimate, with no hypothesis beyond
the cutoff class. The proof runs the Galerkin selection machine on the response cell with the
continuous readout
z ↦ ⨍ ⟨z, B_a z⟩ + 2 · ⨍ φ ⟨z₁, z₂⟩,
whose first summand is the doubled energy bilinear form of the slice evaluated on z and its
pointwise φ-multiple (continuous by continuous_weightedEnergy_add_cutoffQuadReadout), and whose
second summand is the continuous cutoffQuadReadout. The almost-everywhere extraction identity of
CutoffQuadraticReadout identifies this readout on the minimizer with the canonical quadratic
readout. The two statements are exactly the hquadMinus/hquadPlus hypotheses under which
aestronglyMeasurable_abs_pairing_of_maximizer closes the measurability of the cutoff pairing.
A block state whose two slots are multiplied pointwise by a scalar field. This is the
algebraic packaging of the φ-weighted block field used by the weighted energy term of the cutoff
quadratic readout.
Equations
- HCPolySupport.HighContrast.Multiscale.blockStateSmulField φ X = { potential := fun (x : HCPolySupport.Vec d) => φ x • X.potential x, flux := fun (x : HCPolySupport.Vec d) => φ x • X.flux x }
Instances For
The cutoff-weighted quadratic readout of the canonical minus optimizer state of
e.response.cutoff.estimate is measurable in the coefficient sample, with no hypothesis beyond the
cutoff class. This is the hquadMinus hypothesis of the family reduction of the cutoff pairing
(AK.HC Lemma A.1, (A.4)).
The cutoff-weighted quadratic readout of the canonical plus optimizer state of
e.response.cutoff.estimate is measurable in the coefficient sample, with no hypothesis beyond the
cutoff class. This is the hquadPlus hypothesis of the family reduction of the cutoff pairing
(AK.HC Lemma A.1, (A.4)).
The quadratic readout of the canonical minus optimizer state of e.response.cutoff.estimate
against an arbitrary essentially bounded weight is measurable in the coefficient sample. The weight
is bounded by 2 in norm, which is the only property of the cutoff class that the fixed-slice
readout argument consumes; the statement is the hquadMinus hypothesis of the family reduction of
the cutoff pairing (AK.HC Lemma A.1, (A.4)).
The quadratic readout of the canonical plus optimizer state of e.response.cutoff.estimate
against an arbitrary essentially bounded weight is measurable in the coefficient sample. The weight
is bounded by 2 in norm, which is the only property of the cutoff class that the fixed-slice
readout argument consumes; the statement is the hquadPlus hypothesis of the family reduction of
the cutoff pairing (AK.HC Lemma A.1, (A.4)).
Law integrability of the recentred pathwise response #
The recentring of the self-dual splitting sends the sample a to a_- = a - g, with g the
skew Schur coefficient of the canonical mean and G = ((1, 0), (g, 1)) the constant shear.
Because g is constant and skew, the coarse block of a_- is the fixed congruence
Gᵀ 𝐀(U; a) G of the coarse block of a; the response J(U; a_-) is the corresponding block
quadratic minus the constant p·q'. Consequently the law integrability of J(U; a_-(·))
follows from the entrywise law integrability of the recentred coarse block, which is itself a
fixed linear combination of the entries of 𝐀(U; ·).
This file records those two steps: the pathwise block identity (AK.HC (2.15) with the recentred
coefficient) and the reduction of the P-integrability of the response to the entrywise
P-integrability of the recentred coarse block.
The recentred coarse block is the shear congruence of the coarse block. For the recentring
a_- = a - g of the self-dual splitting, the coarse block on an adapted cell is
Gᵀ 𝐀(U_u; a) G with the constant shear G = ((1, 0), (g, 1)) whose off-diagonal block g is
the skew Schur coefficient of the canonical mean. The proof uses only the skewness of g and
the quadraticity of the variational quantity on the cell.
The recentred response is the block quadratic of its coarse block, AK.HC (2.15) for the
recentred coefficient a_- = a - g. The two sides agree after passing to a pointwise
elliptic representative of a_- on the adapted cell and invoking the canonical
response--coarse-block identity on a bounded open convex domain.
Law integrability of the recentred response from its pathwise block-quadratic form. If
b is any coefficient family whose response is the block quadratic of its own coarse block, and
every entry of that coarse block is P-integrable, then the response is P-integrable. The
quadratic form is expanded in the canonical block basis, so it is a finite real combination of
the entries of the coarse block, and the constant p·q' is integrable because P is a finite
measure.
Law integrability of the recentred response for the response coefficient a_- = a - g:
the pathwise representation respJ_respCoeffMinus_eq together with the transport of the
entrywise integrability of the coarse block across the constant shear congruence yields
P-integrability of a ↦ J(U_u; a_-(a)).