High-contrast homogenization: Entry.Response.Kernel.RecentCellDefectBound #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Measurability and the recent-cell defect bound #
Under RawOutput, the all-scale maximum respAllScaleMax - a countable supremum over
coarse-block quantities, each measurable through the integrable-coarse-block fields of
RawOutput - is AEStronglyMeasurable and L^Q-integrable (p.response.transfer). Because
respAllScaleMax is built from the one-sided spectral positive part and so majorizes the
recent-cell defect only from above, a bound at the sharp exponent η^{2/Q} cannot follow from it
alone; this file records that obstruction and develops the two-sided quantity respAllScaleAbs
in its place, together with the measurability of the recent-defect block for both signs and the
resulting one-sided bound ‖normalizedBlock‖ ≤ (weight) · respAllScaleAbs the genuine two-sided
estimate is built from.
Measurability and L^Q-integrability of M under RawOutput. NOTE: the
hypothesis ∫ M^Q ∂P ≤ C_m η is a Bochner integral with no integrability side condition, so this
is genuinely needed to use it (else the integral is the junk 0). M is an sSup over the
countable family (n, z), each term measurable in a through the coarse blocks (RawOutput
integrable-coarse-block fields); the bound comes from a.e. ellipticity.
FIRST CONJUNCT: proved by
respAllScaleMax_measurable above — the countable-sSup route, with blockSpecBound shown
continuous by an attained-infimum/Lipschitz argument that needs no semidefiniteness of its
(indefinite) argument normalizedBlock A E_t − I.
SECOND CONJUNCT: not derivable from the statement's previous binder set, in which Csrc was
universally quantified: every route to an integrable majorant for M^Q goes through the
deep scales k < j_*, and the only tools for those are
Source.source_multiplier_and_adapted_bound (AdaptedBound.lean) and
Annealed.adaptedMean_refBlock_normalization (ReferenceNormalization.lean), each of which
produces a positive Csrc_i and demands the threshold ⌈Csrc_i · logb 3 (2 K)⌉ ≤ j_*.
RawOutput.hsrc supplies that threshold only for the Csrc of the binder, which under a ∀
may be zero or negative, and RawOutput.hj gives only 2d ≤ 3^{j_*}. Three premises are
therefore carried, each of them forced and each of them already carried by the all-scale
maximum bound, whose machinery this proof reuses:
Csrcis produced (∃ Csrc, 0 < Csrc ∧ …) rather than taken, exactly asSource.source_multiplierand every other Source consumer in the tree produces it. The assembly consuming this statement reconciles itsCsrcwith that of the all-scale maximum bound and with those of the other estimates it combines by the tree's ownmax-ing idiom (HCPoly/Entry/OneGridPropagation.lean).ε ∈ Ioc 0 S.eps0andσ ∈ Ioc 0 ε:SelectionData.one_le_B0holds only on that range, and without itrespAllScale_window'sj_* < t— needed even on the fluctuation side — is unavailable.0 ≤ Cglob: needed to drop the first summand ofraw.hsrcwhen specialising it to the source threshold.
The strengthened statement's satisfiability is exhibited inside the proof itself —
the ∃ Csrc witness is max Csrc₁ Csrc₂ > 0, and the source-smallness pair is chosen here as
Cs := 1, η := (1 + Y)^Q, so that the RespSourceSmall inequality holds by construction
(Y ≤ 1 + Y). No RespSourceSmall premise and no η ∈ Ioo 0 (1/2) premise is added:
integrability, unlike the quantitative bound ∫ M^Q ≤ C η, does not care about the constant. No
new
constraint is placed on SelectionData or on Selects, so no separate selection-satisfiability
obligation arises.
The helpers this proof needs are public declarations of
HCPoly/Entry/Response/Core/EnergyDefectBound.lean (respAllScale_window) and of
HCPoly/Entry/Response/Core/PathwiseFluctuationBound.lean (add3_pow_le and pathwise_bound_max),
with no statement and no proof changed. fluctuation_term_le_max and source_term_le_max stay
private in HCPoly/Entry/Response/Core/PathwiseFluctuationBound.lean; scale_index_le and
respAllScaleMax_le_of_forall are public in HCPoly/Entry/Response/Core/EnergyDefectBound.lean.
respAllScaleMax_nonneg is public in
HCPoly/Entry/Response/Kernel/DepthZeroEnergyExtraction.lean, which this file imports, and it is
the one used here.
The recent-cell differences (p.response.transfer) #
The η-kernel's hypothesis is one-sided. #
respAllScaleMax is built from blockSpecBound, i.e. from the spectral positive part
|(E_t^{-1/2}A_k(z)E_t^{-1/2} - I)_+| of the paper (p.response.transfer). It
therefore majorizes the recent-cell defect only from ABOVE. The conclusion of the η-kernel asks for
∫ ‖D_{n,w}‖^2 ≤ K_n η^{2/Q} from ∫ M^Q ≤ C_m η alone; the theorem below shows that this
implication is FALSE, and that the reachable exponent from a one-sided majorant is η^{1/Q},
not η^{2/Q}.
The paper does not claim otherwise: at p.response.transfer the recent cell differences
V_{k,t}(z) - V_t + (P_{k,t} - I) are bounded in L^2 by C_H η^{1/Q} using the fluctuation
history (two-sided, fluctuationHistory) for the first two terms and the mean history
(meanPenalty_Q(P_{k,t}) ≤ 3^{α(t-1-k)}η) for the third. Neither carrier is present in the
hypotheses of integral_recentDefect_sq_le_minus/plus.
Local helpers for the η-kernel #
These close the FIRST conjunct (AEStronglyMeasurable) of both η-kernel twins, and are
independent of the η exponent.
isOpenBoundedConvexDomain_adaptedCellAtCenter and volume_adaptedCellAtCenter_toReal_pos
are private in DiagonalDefectCarriers.lean), which IS in this
file's import closure. The two proofs are three lines each over public CoarseGraining lemmas,
so they are restated here with citations.
HasQuadraticMu on every ALIGNED adapted cell.
the η-kernel measurability layer #
Entrywise measurability is preserved by a fixed two-sided matrix product.
The congruence bridge on an ALIGNED adapted cell, minus sign.
Entrywise measurability of the recentred coarse block on an aligned cell, minus sign.
The measurability conjunct of the η-kernel (minus).
The congruence bridge on an ALIGNED adapted cell, plus sign.
Entrywise measurability of the recentred coarse block on an aligned cell, plus sign.
The measurability conjunct of the η-kernel (plus).
The two-sided carrier #
The ONE-SIDED hypothesis ∫ respAllScaleMax ^ Q ∂P ≤ Cm * η cannot imply the η-kernel's conclusion
∫ ‖D_{n,w}‖ ^ 2 ≤ K n * η ^ (2/Q) for ANY constant sequence K. The conclusion is unchanged,
and the hypothesis carrier is replaced by its two-sided twin respAllScaleAbs
(ResponseBlockObjects.lean), which is respAllScaleMax with blockSpecBound (the spectral
positive
part) replaced by blockOpNorm; the premise's route already runs through the TWO-SIDED
blockOpNorm (normalizedFluctuation …).
The lemmas below are the comparison layer that keeps every EXISTING respAllScaleMax consumer
(coarseBlock_le_one_add_respAllScaleMax among them) available under the new hypothesis:
respAllScaleMax ≤ respAllScaleAbs pointwise.
The comparison, termwise, UNCONDITIONAL. blockSpecBound N ≤ blockOpNorm N for
every doubled block: blockSpecBound N = sInf {c ≥ 0 | N ≼ c I} and ‖N‖ is a member of that
set by blockMatLoewnerLE_blockScale_blockOpNorm_self. This is the inequality that makes
respAllScaleAbs
(ResponseBlockObjects.lean) a genuine strengthening of respAllScaleMax, so every existing
respAllScaleMax consumer -- in particular
coarseBlock_le_one_add_respAllScaleMax -- remains available.
A normalized block of a positive semidefinite block is positive semidefinite.
The reverse comparison on a PSD block: the two-sided operator norm of N - I exceeds
its spectral positive part by at most 2. N ≼ (1 + s) I with s = blockSpecBound (N - I)
by le_one_add_specBound, hence ‖N‖ ≤ 1 + s by blockOpNorm_le_of_loewner, hence
‖N - I‖ ≤ ‖N‖ + ‖I‖ ≤ s + 2.
This is what turns the EXISTING one-sided envelope pathwise_envelope into an envelope
for the two-sided carrier respAllScaleAbs, i.e. it discharges the BddAbove side condition
of respAllScaleMax_le_respAllScaleAbs and of the le_csSup step the η-kernel needs.
respAllScaleMax ≤ respAllScaleAbs pointwise.
One side condition, genuine:
hbdd--BddAboveof the defining set ofrespAllScaleAbs.Real.sSuptakes the junk value0on an unbounded set, so WITHOUT this the inequality is false; the existingrespAllScaleMaxlemmas carry exactly the same side condition (le_csSup hbddincoarseBlock_le_one_add_respAllScaleMax, whosehbddcomes frompathwise_envelope). Stated, not assumed away.
The coarse block of an ALIGNED adapted cell is positive semidefinite. The w-general
form of Annealed.coarseBlock_adaptedCell_posSemidef (ParentChildRecurrence.lean, stated only
for w = 0); adaptedCellAtCenter q j w is by definition adaptedCellTranslate q j (adaptedCellCenter q j w) (HCPoly/Entry/Setup/AdaptedGridCells.lean), which is exactly what
Annealed.blockPosDef_coarseBlock_adapted (AdaptedDomainLocality.lean) takes.
Congruence invariance of the normalized operator norm. Applying the SAME congruence
blockCongr G to a block AND to its normalizer leaves the normalized block orthogonally
similar, so its operator norm does not increase:
U := matSqrt E * G * matSqrt (Gᵀ E G)⁻¹ satisfies Uᵀ U = 1 and
normalizedBlock (blockCongr G Z) (blockCongr G E) = Uᵀ · normalizedBlock Z E · U.
This is the step that carries weighted_blockOpNorm_le_respAllScaleAbs from the
E_t-picture of respAllScaleAbs to the Ehat^∓-picture of recentDefect: recall
respEhatMinus = blockCongr (respG F) (respMean …) (ResponseBlockObjects.lean) and that
coarseBlockMatrix_respCoeffMinus_at puts the numerator in the matching blockCongr
form.
The respAllScaleAbs envelope. The two-sided defining set is a.e. bounded above, by
C + 2 where C is the constant of the ONE-SIDED pathwise_envelope: the weights
3 ^ (-(ρ n)) are at most 1, and blockOpNorm_sub_id_le_specBound_add_two costs 2.
This is the respAllScaleAbs analogue of pathwise_envelope, and it is
what lets le_csSup be applied to respAllScaleAbs -- so the junk value 0 of Real.sSup on
an unbounded set is excluded, exactly as for respAllScaleMax.
The le_csSup step for the two-sided carrier. Every weighted term of the defining set
of respAllScaleAbs is at most respAllScaleAbs itself, a.e. This is the pathwise input the
η-kernel needs on BOTH sides, and the exact analogue of the le_csSup hbdd hmem step of
coarseBlock_le_one_add_respAllScaleMax.