High-contrast homogenization: Entry.Response.Kernel.RecentDefectCongruenceBound #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The pointwise two-sided recent-defect bound via congruence #
Continuing the reduction of the recent-cell defect to the two-sided quantity respAllScaleAbs,
this file proves the pointwise bound ‖N_{n,w} - N_0‖ ≤ (3^{ρn} + 1) · respAllScaleAbs a on the
normalized block defect, using that the recentred and adjoint normalizers are the same congruence
of the E_t-picture as the coarse block itself, so a congruence applied to both leaves the
normalized operator norm unchanged (p.response.transfer). It also records the
positive-definiteness of the recentred and adjoint response matrices and the measurability and
integrability of respAllScaleAbs that the bound needs.
Congruence is linear over blockSub.
The pointwise η-kernel bound, E_t-picture. With N_k = normalizedBlock A_k E_t,
‖N_{n,w} - N_0‖ ≤ (3 ^ (ρ n) + 1) · respAllScaleAbs a, a.e. Both summands come from
weighted_blockOpNorm_le_respAllScaleAbs, the depth-n one after multiplying by
3 ^ (ρ n) and the depth-0 one at z = 0, where triadicIndexBox d 0 = {0} and
adaptedCellAtCenter q t 0 = adaptedCell q t.
Ehat^+ = D Ehat^- D is the congruence of E_t by respGPlus = respG · D
(ResponseBlockObjects.lean, blockCongr_blockCongr), i.e. the plus sign is the same
picture with the same congruence that coarseBlockMatrix_respCoeffPlus_at produces.
Ehat^- is positive definite.
Ehat^+ is positive definite.
THE η-KERNEL POINTWISE BOUND, minus sign — the inequality the η-kernel's conjunct 3 is built
on, and the one the ONE-SIDED respAllScaleMax provably cannot give:
recentDefect q t n w Ehat^- (a_-) ≤ (3 ^ (ρ n) + 1) · respAllScaleAbs a, P-a.e., uniformly
in n and in the aligned index w.
Route, exactly the paper's (p.response.transfer): the recentred field a_- and the
normalizer Ehat^- = blockCongr (respG F) E_t are the SAME congruence of the E_t-picture
(coarseBlockMatrix_respCoeffMinus_at), congruence does not increase the
normalized operator norm (blockOpNorm_normalizedBlock_blockCongr_le), and in the
E_t-picture the defect splits as (N_{n,w} - I) - (N_0 - I)
(blockOpNorm_normalizedBlock_sub_le).
Positive definiteness of Ehat^- is DISCHARGED here, not assumed:
respEhatMinus_posDef above, from blockCongr_posDef and the unit block shear
respG F = ⟨1, 0, respg F, 1⟩ (ResponseBlockObjects.lean).
THE η-KERNEL POINTWISE BOUND, plus sign. The twin of
recentDefect_le_respAllScaleAbs_minus, with respGPlus in place of respG.
The two-sided carrier really is the strengthening it is meant to be, with
its side condition discharged a.e. from RawOutput-level data: respAllScaleMax ≤ respAllScaleAbs holds P-a.e., so every existing consumer of the one-sided carrier survives
the η-kernel restatement.
JENSEN / the power-mean step for the η-kernel. On a probability measure, for a
nonnegative f and 2 ≤ Q,
∫ f ^ 2 ∂P ≤ (∫ f ^ Q ∂P) ^ (2/Q).
Elementary route, no eLpNorm machinery: with I = ∫ f ^ Q ∂P and θ = 2/Q ∈ (0, 1], the
weighted AM-GM Real.geom_mean_le_arith_mean2_weighted at p₁ = f a ^ Q, p₂ = I gives
pointwise f a ^ 2 · I ^ (1-θ) ≤ θ · f a ^ Q + (1-θ) · I; integrating over the PROBABILITY
measure the right side is I, and dividing by I ^ (1-θ) leaves I ^ θ. This is the last
analytic ingredient of the η-kernel's conjunct 3.
Measurability of the two-sided all-scale maximum: the respAllScaleAbs twin of
respAllScaleMax_measurable above, with blockOpNorm in place of blockSpecBound (the norm is
continuous, so no attained-infimum argument is needed here).
The two-sided carrier. Measurability and
L^Q-integrability of A = respAllScaleAbs under RawOutput: the respAllScaleAbs twin of
respAllScaleMax_aestronglyMeasurable_integrable above.
Why this is needed. The η-kernel twins integral_recentDefect_sq_le_minus / _plus below carry
TWO premises about the carrier: Integrable (fun a => A a ^ Q) P and
∫ A ^ Q ∂P ≤ Cm η. The second has a producer -- response_allscale_abs
-- but the first had none, since it is produced above only
for the ONE-SIDED respAllScaleMax, and neither premise follows from the other. With this
theorem both premises of the η-kernel estimate have producers.
Route, the one-sided twin with the two-sided ingredients: respAllScaleAbs_measurable for the
measurable half; for the integrable half, the SAME own choice of the source-smallness pair
(C_s, η) = (1, (1 + Y)^Q) (the explicit witness making the strengthened binder
set satisfiable), pathwise_bound in place of pathwise_bound_max, and
add4_pow_le in place of add3_pow_le because the two-sided pathwise bound carries
the one extra summand η^{1/Q} / C_s -- which at C_s = 1 is the CONSTANT 1 + Y, so it costs
only two more constant terms in the majorant and no new integrability input.
From the pointwise η-kernel bound to conjuncts 2 and 3. If 0 ≤ g ≤ c · A a.e. with
A ≥ 0, A ^ Q integrable and ∫ A ^ Q ∂P ≤ Cm · η on a probability measure with 2 ≤ Q,
then g ^ 2 is integrable and ∫ g ^ 2 ∂P ≤ c ^ 2 · Cm ^ (2/Q) · η ^ (2/Q).
A ^ 2 ≤ 1 + A ^ Q pointwise (split at A = 1) gives integrability with no smallness;
integral_sq_le_rpow (Jensen) gives the exponent. The last analytic step.