High-contrast homogenization: Entry.Response.Cutoff.ResponseCutoffEstimate #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The cutoff estimate #
The cutoff decomposition of the centred response, before the final scalar inequality, bounds
|Jtilde^Β±(e)| by the three error rows β the energy-defect row, the cutoff-mean row, and the
cutoff-oscillation row β plus the cutoff pairing term; combining that bound with the constant
32 d^2 3^{-t} needed to construct a genuine cutoff, in place of the naive class's vacuous one,
closes it under a weak-pairing hypothesis on the maximizer family. This file then states and
proves the cutoff estimate e.response.cutoff.estimate itself, one of the inputs to the response
decomposition adapted_response_core: the bound on the centred response Jtilde^Β±(e) in terms of
the energy-defect row, the cutoff-mean row, and the cutoff pairing term, closed on the response's
own concrete data.
The variational calculation of AK.HC (3.45)-(3.54) with the cutoff decomposition #
(3.46) and the mean cancellation of p.response.transfer.
The two cutoff-mean terms e2 below are exactly the two rows re-typed here onto the current
carriers respTauMinus/Plus (ResponseBlockObjects.lean), respEJMinus/Plus,
respLsMinus/Plus, the paper's π_s^Β±, built from respSourceLoad).
The three error terms of p.response.transfer are, in order:
e1β replacing the terminal optimizer by its scale-scell optimizers:C (Ο^Β± + (Ο^Β± E[J_t^Β±])^{1/2} + 3^{-H} E[J_t^Β±]);e2β the two cutoff-mean terms, after subtracting the cell average ofΟ. The constant cell means cancel after expectation because the scale-stranslations are integral and(Ο)_{U_t} = 1; what is left costsC (Ο^Β± π_s^Β±)^{1/2};e3β pairing the within-cell oscillations with the gradient and the flux and summing the descendants with weights3^{3(k-s)/2}:C 3^{-H} (E[J_t^Β±] π_s^Β±)^{1/2}.
The fourth summand on the right is the cutoff pairing term e4, bounded by C W^Β±; the
mean-cancellation assertion is exactly that NO further term (the difference between
the inserted means P^Β±, Q^Β± and the actual annealed means) appears in this decomposition.
Cutoff rows (p.response.transfer; AK.HC (3.45)-(3.54) and (3.46)). The cutoff
decomposition of the centred response, before Young's inequality: |Jtilde^Β±(e)| is bounded by
the three error rows e1 + e2 + e3 plus the cutoff pairing term e4.
The original formulation of IsResponseCutoff was vacuous: it asked a function supported in a
cube of side 3^t to have mean one while its pullback was only 3β»α΅-Lipschitz, and such a
function is at most 1 / 2 everywhere. With the cutoff constant 32 * d ^ 2 * 3 ^ (-t),
exists_isResponseCutoff above constructs a member of the class, and what remains is the genuine
variational calculation of AK.HC (3.45)-(3.54).
Without the additional integrability hypotheses the theorem is false: three of the
four summands on each right-hand side are Bochner integrals whose integrands have no
sample-uniform bound (respJ is an sSup over an uncountable admissible class, and a point of
CoeffSpace d is only QUALITATIVELY elliptic -- see the collapse diagnostics above), so on a law
where they fail to be P-integrable the junk value 0 zeroes every error row and the statement
forces Jtilde^Β±(e) = 0, which the purely algebraic left-hand side does not satisfy. That
implication is machine-checked above by hc3_h8c_minus_row_forces_centeredJ_eq_zero.
The CONCLUSION is unchanged, character for character. Eight premises are ADDED, all of them
raw-derivable at the sole call site response_cutoff_estimate (ResponseCutoffEstimate.lean),
and every
one of them is discharged there:
| new premise | discharged at the call site from |
|---|---|
IsStationaryLaw P | raw.stat |
IsUnit (respGrid jStar F) | raw.hj, raw.symm, raw.pos (the existing hq) |
(jStar : β€) β€ s | raw.hs_lo plus the two range hypotheses Ξ΅ β (0, S.eps0], `Ο β (0, |
Ξ΅], which response_cutoff_estimate` now carries -- see below | |
the two Summable (respSourceLoadSummand...) | hLB, i.e. RespLoadBound, which now carries |
the summability of the source-load family as two further conjuncts. Without them respSourceLoad | |
is the junk value 0 of a divergent tsum and the two cutoff-mean rows assert that the centred | |
| cutoff mean vanishes | |
HasIntegrableCoarseBlock P (respCell jStar F k) on [jStar, t] | |
Annealed.hasIntegrableCoarseBlock_adapted from raw.stat, raw.ell, raw.hj | |
(toFullBlockMat (respMean P jStar F k)).PosDef on [jStar, t] | Annealed.adaptedMean_posDef |
| from the same three fields | |
the four Integrable (fun a => respJ... u... (respCoeffΒ± F a)) P, u β {s, t} | the |
raw-consuming lemma integrable_respJ_respCell above | |
the two Integrable (fun a => |cutoffPairingOnCellAux...|) P | the raw-consuming lemma |
integrable_abs_cutoffPairingOnCell above |
IsStationaryLaw P is not decoration. The mean-cancellation sentence this decomposition rests on
(p.response.transfer, "The constant cell means cancel after expectation, BECAUSE the
scale-s translations are integral and (Ο)_{U_t} = 1") is a stationarity argument:
E[(X)_{z+U_s}] is independent of the translation z only for a stationary law, which in this
checkout is Annealed.annealedBlock_adaptedCellAtCenter
(HCPoly/Entry/Annealed/AnnealedBlockOrder.lean, whose
hypotheses are exactly hstat, raw.hj and (jStar : β€) β€ j -- hence also the third premise
above). Without it the e2 row has no reason to close.
hjs : jStar β€ s is not directly available in raw as raw.hs_lo: as respAllScale_window
(HCPoly/Entry/Response/Core/EnergyDefectBound.lean) records, raw.hs_lo reads
jStar + βB log_3(2 + Pi)β β€ s and is VACUOUS unless 1 β€ B, which comes only from
SelectionData.one_le_B0, which is stated only for Ξ΅ β (0, S.eps0] and Ο β (0, Ξ΅].
response_cutoff_estimate did not carry those two ranges. They have therefore been ADDED to it,
in the same position and with the same names as its siblings
response_energy_and_defect and response_load_and_mean, and the one
place that applies it (AdaptedResponseAssembly.lean, inside adapted_response_core_of_holes)
passes the
hΞ΅/hΟΞ΅ it already has in context. No statement is changed: adapted_response_core is
untouched.
Seven further premises complete the variational calculation. The
variational calculation e1 + e2 + e3 is closed: the energy-defect row e1 by
CutoffEnergyDefectRowObligations, the cutoff-mean rows e2 + e3 by CutoffMeanRowCarriers, and
the assembly by
CutoffEstimateRowClosure. Seven premises are ADDED, all raw-derivable at the sole call site
response_cutoff_estimate and all discharged there:
| new premise | discharged at the call site from |
|---|---|
2 β€ d (on the theorem itself) | _hd |
2 * d β€ 3 ^ jStar | raw.hj (already used there for hq) |
(explicitCanonicalMetric F).PosDef | `Geometry.explicitCanonicalMetric_posDef raw.symm |
raw.pos(already in scope ashm`) | |
(toFullBlockMat F).PosDef | posDef_toFullBlockMat raw.symm raw.pos |
β Ξ³ E Ξ¨ Kg Src, CoarseEllipticityDagger P Ξ³ E Ξ¨ Kg Src | raw.ell |
the two β Y, Summable (respSourceLoadSummand β¦ Y) | |
exists_summable_respSourceLoadSummand_all (OptimizerMeanRowCarriers) from raw.stat, | |
raw.ell, raw.hj, raw.hsrc, raw.cube, raw.hst and RespCalibrated | |
the two 0 β€ respTauβ | RespEnergyDefect (hED), which response_cutoff_estimate already |
| carries |
The β Y summability is what the 2d coordinate instantiations of the oscillation half need:
RespLoadBound supplies the source-load convergence only at Y = Y^β, and at Y = (0, Ξ΄_i) the
generation layer is not dominated by the Y^β layer. Supplying it forced
response_cutoff_estimate to EXPORT its own source threshold Csrc, in the sibling pattern of
response_source_load_bound and response_weak_estimate; AdaptedResponseAssembly takes the
maximum, so
nothing downstream sees the change. The conclusion of this theorem is unchanged, character for
character, and RespCutoffBound is untouched.
The final combination of the cutoff rows and the weak pairing. #
The two branches combine the primal and adjoint rows of the cutoff decomposition against the
weak quantity under one common constant. The conclusion is LITERALLY RespCutoffBound
(CenteredEnergyIdentity.lean), i.e. exactly the payload of response_cutoff_estimate
(ResponseCutoffEstimate.lean).
Cutoff bound from the rows and the weak pairing (p.response.transfer,
e.response.cutoff.estimate). The three error rows of the cutoff decomposition plus the bound
on the cutoff pairing term combine, under the common constant max Cβ Cβ, into
RespCutoffBound.
eM/eP stand for the two expected cutoff pairing terms e4^β, so that hrowsMinus/hrowsPlus
are the cutoff-row conclusions and hweakMinus/hweakPlus the weak-pairing conclusions. The
nonnegativity hypotheses are the ones needed to collect the rows under a single constant; each is
available in the calling context (RespLoadBound CenteredEnergyIdentity.lean and RespWeakBound
already assert nonnegativity of π_s^Β± and of W^Β±).
The cutoff estimate #
The cutoff estimate e.response.cutoff.estimate, one part of the proof of
adapted_response_core.
The cutoff estimate #
The cutoff estimate (e.response.cutoff.estimate):
`|Jtilde^Β±(e)| <= C(tau^Β± + (tau^Β± E[J_t^Β±])^{1/2} + (tau^Β± L_s^Β±)^{1/2}
- 3^{-H}(E[J_t^Β±] + (E[J_t^Β±] L_s^Β±)^{1/2}) + W^Β±)`.
-- KERNEL. This is the second true analytic kernel: the variational calculation of
\cite[(3.45)--(3.54)]{AK.HC} before Young's inequality, with \cite[(3.46)]{AK.HC} and
\cite[Lemma A.1, (A.4)]{AK.HC}, is never reproved in the paper.
Route (p.response.transfer): choose a cutoff phi of the class IsResponseCutoff. The
cutoff compares the terminal optimizer with its scale-s cell optimizers, and the
quadratic-response identity measures the mean energy of their difference by 2 tau^Β±. Insert
P^Β±, Q^Β± into the cutoff decomposition; the term containing the difference between these
means and the actual annealed means is zero. Integration by parts and the direct
full-dual pairing give
E[|avg_{U_t} phi (grad v - P).(a grad v - Q)|] <= C W^Β±. The rounded/unrounded
metric comparison costs only a dimensional constant, since
|m^{-1/2}q||q^{-1}m^{1/2}| <= 3. Keeping the last product is essential.
The proof combines the pieces of the variational calculation:
exists_isResponseCutoff (HCPoly/Entry/Response/Cutoff/ResponseCutoffExistence.lean) discharges
the
choice of cutoff at p.response.transfer, the maximizer-existence lemmas supply the two maximizer
families, the cutoff-rows estimate gives the three error rows, the weak-pairing estimate gives
the cutoff pairing term, and the two are collected under max Cβ Cβ. The invertibility of the
selected grid comes from RawOutput.hj/symm/pos, and 0 β€ W^Β± from the weak-pairing estimate
itself (its left-hand side is an integral of absolute values).
The proof invokes abs_respCenteredJ_le_cutoffRows,
integral_abs_cutoffPairingOnCell_le_respWeak, and the two raw-consuming integrability
lemmas integrable_besovSeminorm_sq_respCell and integrable_abs_cutoffPairingOnCell. The
theorem is axiom-clean.
It exports its own source threshold Csrc, in the same pattern as
response_source_load_bound and response_weak_estimate. Two inputs need one: the
measurability and L^Q(P)-integrability of the all-scale maximum, which the two
raw-consuming lemmas consume, and the convergence of the source-load series at every dual
vector, which the 2d coordinate readouts need and which is a theorem of
annealedBlock_le_adaptedMean, whose threshold on j_* is not implied by an arbitrary
Csrc. The exported threshold is the maximum of the two. AdaptedResponseAssembly in turn
takes the
maximum of the thresholds exported by the inputs it combines, so the interface seen by consumers
is unchanged; the extra binder 0 β€ Cglob matches response_source_load_bound's.