High-contrast homogenization: Entry.Response.Kernel.WeakIntegrandDomination #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Almost-Sure Domination of the Weak-Quantity Integrand #
This file shows that, for an arbitrary family of response maximizers and either sign of the
recentring, the square of the scale-average seminorm of the recentred, canonically metric-scaled
cell averages of the doubled optimizer state is almost-surely dominated by the all-scale envelope
entering the weak quantity W^\pm of e.response.weak.estimate. It records the elementary
measure-theoretic fact that a measurable nonnegative function almost-surely dominated by an
integrable envelope is itself integrable, and applies it to the squared seminorm. It assembles
these into the integrability of the weak-quantity integrand directly from the standing law
premises, for both signs.
Almost-sure domination of the weak-quantity integrand by the all-scale envelope #
The weak quantity W^\pm of e.response.weak.estimate is the sample expectation of the square of
the scale-average seminorm besovSeminorm of the recentred, canonically-metric-scaled cell averages
of the doubled optimizer state X_t^\pm. This file bounds that integrand, for an arbitrary family
of response maximizers, almost surely by an explicit multiple of the all-scale envelope
1 + respAllScaleMax times the recentred response J of AK.HC (2.15), plus one.
The bound is the almost-sure consequence of the pathwise scale-average seminorm bound of
AK.HC (2.130): the optimizer field is replaced, cell average by cell average, by the Chapter-2
canonical maximizer of an elliptic representative of the recentred coefficient; the pathwise bound
is applied to that representative with the subcell quadratic-form envelope read off the all-scale
Loewner bound; and the energy--response identity of e.response.weak.estimate converts the cell
energy into twice the recentred response. The constant is allowed to depend on the sample law and
the fixed data, but not on the sample.
The a.e. domination of the weak-quantity integrand, recentred sign. For the recentred
coefficient family a_- = a - g and an arbitrary family of response maximizers, the squared
scale-average seminorm of the M_0 ^ (1/2)-transported recentred optimizer state is dominated
almost surely by an explicit constant times (1 + ℳ) J^- + 1, with ℳ the all-scale envelope and
J^- the recentred pathwise response of AK.HC (2.15). This is the almost-sure input of the weak
quantity W^- of e.response.weak.estimate.
The a.e. domination of the weak-quantity integrand, adjoint sign. The adjoint twin of
ae_besovSeminorm_sq_le_envelope_minus: for the adjoint recentred coefficient family
a_+ = aᵀ + g and an arbitrary family of response maximizers, the squared scale-average seminorm
of the M_0 ^ (1/2)-transported recentred optimizer state is dominated almost surely by an
explicit constant times (1 + ℳ) J^+ + 1, with J^+ the adjoint recentred pathwise response of
AK.HC (2.15). This is the almost-sure input of the weak quantity W^+ of
e.response.weak.estimate.
Integrability of the squared weak-quantity seminorm #
The weak-quantity estimate e.response.weak.estimate bounds the squared scale-average Besov
seminorm of the M_0 ^ (1/2)-transported recentred optimizer state by a sample-dependent
envelope. This file records the elementary measure-theoretic consequence used to discharge the
integrability premise of the cutoff rows: a measurable nonnegative function dominated almost
everywhere by an integrable function is integrable.
The generic domination statement is specialised to the all-scale envelope
respAllScaleMax of HCPoly.Entry.Response.Core.ResponseBlockObjects, whose
Q-th moment is controlled by e.response.weak.estimate; because the law is a probability
measure, the additive constant 1 in the envelope is integrable and the envelope itself is
integrable whenever its response factor is.
Integrability of the squared weak-quantity seminorm by domination. Let P be a
probability law on the coefficient space and let
`f a = besovSeminorm t (fun n z => M_0 ^ (1/2) (cellAverage U_{t-n,z} (optimizerField (c a) (u a))
- Y)) ^ 2`
be the squared scale-average seminorm of the M_0 ^ (1/2)-transported recentred optimizer state,
as in e.response.weak.estimate. If f is P-a.e.-strongly measurable and is dominated
P-a.e. by an integrable function g, then f is P-integrable: the finite-integral half of
Integrable follows from HasFiniteIntegral.mono' after replacing ‖f a‖ by f a through the
nonnegativity of the square, and the measurability half is the hypothesis.
Integrability of the squared weak-quantity seminorm from the recentred all-scale envelope.
The generic domination statement with g a = C * ((1 + respAllScaleMax P γ jStar F t a) * respJ (respGrid jStar F) t p q' (respCoeffMinus F a) + 1). The response factor
(1 + respAllScaleMax) * respJ is P-integrable by hint and the constant 1 is P-integrable
because P is a probability measure, so C times their sum is integrable and the squared
seminorm inherits integrability from the domination hypothesis.
Integrability of the squared weak-quantity seminorm from the adjoint all-scale envelope.
The adjoint twin of integrable_besovSeminorm_sq_of_ae_envelope: the same domination argument
applies with the adjoint recentred response respJ (respGrid jStar F) t p q' (respCoeffPlus F a)
in place of the recentred response.
Integrability of the weak-quantity integrand from the standing law premises #
The weak quantity W^\pm of e.response.weak.estimate is the sample expectation of the square of
the scale-average seminorm besovSeminorm of the recentred, canonically-metric-scaled cell averages
of the doubled optimizer state X_t^\pm, for an arbitrary family of response maximizers. This file
assembles the three landed ingredients into the integrability of that integrand, starting from the
standing law premises IsStationaryLaw and the coarse-ellipticity dagger.
The ingredients are:
- almost-everywhere strong measurability of the integrand, from the measurable canonical selection and the countable sum defining the seminorm;
- almost-sure domination of the integrand by a constant multiple of the all-scale envelope
(1 + respAllScaleMax) * respJ + 1, from the pathwise scale-average seminorm bound AK.HC (2.130) and the energy--response identity ofe.response.weak.estimate; - integrability of that envelope, from the
Q-th envelope moment with2 ≤ Qsupplied bye.response.weak.estimateand Hölder's inequality, together with the elementary domination argument closing the square.
Integrability of the squared weak-quantity seminorm from the standing law premises, recentred
sign. Let P be a stationary probability law with coarse-ellipticity dagger, let F be a block
with positive-definite canonical metric, and let u be an arbitrary family of response maximizers
for the recentred coefficient a_-. Assume the all-scale envelope ℳ = respAllScaleMax is
measurable with Q-th moment P-integrable and J^- ^ 2 is P-integrable. Then the squared
scale-average seminorm of the M_0 ^ (1/2)-transported recentred optimizer state is P-integrable.
This is the integrability of the integrand of the weak quantity W^- of
e.response.weak.estimate; the a.e. domination is supplied by AK.HC (2.130) and the closing
domination argument by Hölder.
Integrability of the squared weak-quantity seminorm from the standing law premises, adjoint
sign. The adjoint twin of integrable_besovSeminorm_sq_of_raw_minus: with the adjoint recentred
coefficient a_+ and an arbitrary family u of response maximizers for it, the same hypotheses on
the all-scale envelope and on J^+ ^ 2 give P-integrability of the squared scale-average seminorm
of the M_0 ^ (1/2)-transported adjoint optimizer state. This is the integrability of the
integrand of the weak quantity W^+ of e.response.weak.estimate.