High-contrast homogenization: Entry.Response.Cutoff.PathwiseToAnnealedAssembly #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Assembling the Annealed Cutoff Bound From Its Pathwise Form #
This file completes the reduction of the annealed cutoff-pairing bound of
e.response.cutoff.estimate to its pathwise form: the elementary integration step that turns a
pathwise domination by the weak response energy respWeakEnergy into a bound on its expectation,
and the resulting pathwise-to-annealed frames for both signs of the recentring, combined into a
single positive constant bounding the annealed pairing for either sign. It records the weak
quantities W^- and W^+ - the weak energies of the two recentred coefficients at the two
response loads on the selected grid - together with W^-'s defining equation and both signs'
nonnegativity. It closes with two measurability prerequisites the sample-dependent weak quantity
needs: cell averages of the canonical optimizer state are measurable in the sample, and a
countable sum such as the scale-average seminorm is measurable whenever its summands are.
Passing a pathwise cutoff bound through the law #
The weak response energy respWeakEnergy bounds the scale-weighted squared scale-average
seminorm of the doubled optimizer state, uniformly over admissible families of cell
maximizers. This file records the elementary integration step that turns a bound holding at
each sample into a bound on the expectation: if a pathwise quantity is dominated by a
nonnegative multiple of that seminorm square, and the seminorm square is Bochner integrable,
then the expectation of the absolute value of the quantity is bounded by the same multiple of
the weak response energy. This is the integration in the sample variable a of the weak
estimate e.response.weak.estimate.
If a pathwise quantity G is dominated, sample by sample, by C₀ times the
scale-weighted squared scale-average seminorm of the doubled optimizer state of an admissible
family of cell maximizers, with C₀ ≥ 0, and that seminorm square is Bochner integrable, then
the expectation of |G| is at most C₀ times the weak response energy W. The integrability
hypothesis is what makes the dominating function Bochner integrable, so that monotonicity of the
integral applies; the branch where |G| is not integrable is handled by the junk value of the
Bochner integral and the nonnegativity of W. This is the annealed form of
e.response.weak.estimate.
The annealed cutoff pairing bound from its pathwise form #
The cutoff pairing of the response estimate e.response.cutoff.estimate is the expectation, over
the sample law, of the absolute value of the volume average over the selected cell of the
cutoff-weighted pairing of the centred optimizer field with the recentring vector. This file
reduces the annealed bound to its pathwise form: assuming the deterministic estimate at every
sample, the singular-grid branch is discharged by the degeneration of the adapted cell (every
volume average collapses to the junk value 0) and the positive-definite branch by monotonicity
of the Bochner integral, so that only the pathwise estimate remains as a hypothesis. This is the
annealed form of e.response.cutoff.estimate.
The annealed cutoff pairing bound e.response.cutoff.estimate, reduced to the pathwise
estimate hpath: if at every sample and for every elliptic data the pairing average is dominated
by C₀ times the scale-weighted squared scale-average seminorm of the doubled optimizer state,
and that seminorm square is Bochner integrable, then the expectation of the absolute pairing is at
most C₀ times the weak response energy W^-. The dichotomy
metric_posDef_or_respGrid_det_eq_zero splits the proof: on the singular-grid branch the adapted
cell is Lebesgue null and the integral vanishes, while on the positive-definite branch the
pathwise bound is integrated against the law.
The annealed plus-sign cutoff pairing bound from its pathwise form #
The cutoff pairing bound e.response.cutoff.estimate is an expectation, over the law of the
coefficient field, of the absolute volume average of the cutoff times the centred doubled
optimizer state. This file reduces that annealed estimate to its deterministic pathwise form on
the plus-sign branch: the metric dichotomy splits off the singular-grid branch, where every
volume average is the junk value 0, and on the positive definite branch a pathwise estimate at
each sample is passed through the integral by monotonicity together with the nonnegativity of the
weak response energy. What remains is a single deterministic inequality, hypothesis hpath.
The annealed cutoff pairing bound of e.response.cutoff.estimate, reduced to its pathwise
form. Suppose that, for every doubled block on the positive definite branch of the canonical
metric and every admissible coefficient, the cutoff pairing of the centred doubled optimizer
state obeys the deterministic estimate with constant C₀. Then for every probability law of the
coefficient field and every admissible family of cell maximizers, the expectation of the absolute
pairing is at most C₀ times the weak response energy W^+. The probabilistic content and the
singular-grid branch of the metric dichotomy are discharged here, so the only remaining input is
the pathwise estimate.
The weak quantities of the two signs #
The weak response quantities W^- and W^+ of the response estimate are the weak energies of
the two recentred coefficients a_- = a - g and a_+ = a^t + g at the two response loads
q^- and q^+, evaluated on the selected grid with the self-dual metric M_0. This file
records W^-'s defining equation (respWMinus_eq; respWPlus_eq lives with respWPlus's own
definition) and their nonnegativity, the two elementary facts used whenever W^± is consumed.
These are the elementary parts of the weak estimate e.response.weak.estimate.
W^- is the weak energy of the recentred coefficient a_- = a - g at the load q^-: by
definition W^- = W(U_t, p, q^-; a_-, Y^-) for the weak response energy W.
The weak response quantity W^- is nonnegative: it is the weak energy of the recentred
coefficient a_- at the load q^-.
The weak response quantity W^+ is nonnegative: it is the weak energy of the recentred
coefficient a_+ at the load q^+.
The annealed cutoff pairing bound for both signs under one constant #
The cutoff pairing bound e.response.cutoff.estimate is an expectation, over the law of the
coefficient field, of the absolute volume average of the cutoff times the centred doubled optimizer
state. The two signs of the recentring are handled by the separate frames
exists_integral_abs_pairing_le_respWeak_of_pathwise and
exists_integral_abs_pairing_le_respWeakPlus_of_pathwise, each with its own constant C₀. This
file combines the two into a single statement carrying one strictly positive constant valid for
both signs simultaneously; the constant is max C₀ 1, which is positive and dominates the constant
of either frame, so each row is obtained by integrating the same pathwise hypothesis at C₀ and
then relaxing it with the nonnegativity of the corresponding weak response energy W^±.
The annealed cutoff pairing bound of e.response.cutoff.estimate for both signs under one
constant. Given a nonnegative constant C₀ and the deterministic pathwise estimate, at every
doubled block on the positive definite branch of the canonical metric and every admissible
coefficient, bounding the cutoff pairing of the centred doubled optimizer state by C₀ times the
scale-weighted squared scale-average seminorm of the doubled optimizer state, there is a strictly
positive constant C such that for every probability law of the coefficient field, every selected
cell and cutoff, and every admissible family of cell maximizers for either recentring, the
expectation of the absolute pairing is at most C times the weak response energy W^- for the
minus sign and at most C times W^+ for the plus sign. The constant may be taken to be
max C₀ 1.
Cell averages of the canonical optimizer depend measurably on the sample #
The weak quantity W^\pm of the response estimate e.response.weak.estimate is a volume
average, over a measurable subcell, of a coordinate of the canonical optimizer state of a
recentred coefficient sample. This file records the specialization of the localized weighted
readout to the constant weight 1, so that a plain cell average is measurable in the sample;
the indicator of a measurable set by a constant is bounded and therefore locally L².
The indicator of a measurable set by the constant 1 is square-integrable on every open
bounded convex domain: it is measurable, bounded by 1, and the restricted Lebesgue measure is
finite. This is the constant-weight input to the cell averages of the weak quantity
e.response.weak.estimate.
The cell average of a coordinate of the canonical minus optimizer state is measurable in the
coefficient sample, for every measurable subcell of the adapted cell. This is the
constant-weight case of the localized weighted readout entering the weak quantity W^- of
e.response.weak.estimate.
The cell average of a coordinate of the canonical plus optimizer state is measurable in the
coefficient sample, for every measurable subcell of the adapted cell. This is the
constant-weight case of the localized weighted readout entering the weak quantity W^+ of
e.response.weak.estimate.
Measurability of the scale-average seminorm #
The scale-average seminorm besovSeminorm is a countable sum whose summands are built from the
sample-dependent cell averages of a doubled field. This file records that such a sum is a
measurable function of the sample whenever its summands are, and applies this to
besovSeminorm.
The only point requiring care is that the real tsum is defined by a junk value 0 where the
series is not summable; the summability set is nevertheless measurable, because for real series it
agrees with the boundedness of the partial sums of the absolute values.
A pointwise countable sum of measurable real-valued functions is measurable. No summability
hypothesis is needed: the series is summable on a measurable set, where the real tsum is the
limit of the partial sums, and takes the junk value 0 off that set.
The scale-average seminorm besovSeminorm of AK.HC (2.130) is a measurable function of the
sample. Each summand is a constant times the square root of a finite sum of products of the
coordinates of the sample-dependent cell averages, hence measurable; the countable sum is
measurable by measurable_tsum_of_measurable.