Documentation

LeanPool.HighContrastHomogenization.Entry.Response.Cutoff.ResponseCutoffExistence

High-contrast homogenization: Entry.Response.Cutoff.ResponseCutoffExistence #

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Existence of the Response Cutoff #

HC bridge III, Step 6 of the cutoff estimate e.response.cutoff.estimate (AK.HC Lemma A.1 and (3.45)-(3.54)): a response cutoff φ is a function supported in the adapted cell, taking values in [0, 2], of volume average one, and satisfying first- and second-derivative bounds at the scale 3^t in the grid's coordinates. This file proves that such a cutoff exists, building it from the canonical product cube cutoff pushed forward along the grid map and normalized by its own cell average, and records the elementary estimates the construction needs: a Bernoulli-type bound, smoothness and continuity of the associated linear maps, and the norm bound on the second iterated derivative of a scaled function.

HC bridge III: the cutoff kernel of Step 6 (AK.HC Lemma A.1 and (3.45)-(3.54)) #

This file contains four statements, each re-typing the same estimates onto the carriers respTauMinus/respEJMinus/respLsMinus/respWMinus/IsResponseCutoff/... of ResponseBlockObjects.lean. No definition of ResponseBlockObjects.lean is changed; the definition below (cutoffPairingOnCellAux) is local to this file. The first is the only statement carried on the CoarseGraining reference geometry Book.Ch02.cubeDomain Q; the second transports it to the adapted cell U_t (ScaleAverageSeminorm.lean), the third is the variational calculation, and the fourth combines them into the payload RespCutoffBound used at ResponseCutoffEstimate.lean. Paper: p.response.transfer, Step 6.

The reference-cube cutoff bound. AK.HC Lemma A.1 / (A.4) on the reference cube domain #

cubeDomain Q.

AK.HC Lemma A.1 / (A.4) -- the cutoff product-term weak-norm bound on the reference cube -- is stated with the same signature as HCPoly/Provider/Response/DivCurlWeakNormTerm.lean. Each name in the signature was checked in the pinned CoarseGraining rev 8ec687c:

NO SIGNATURE DRIFT was found: all eight are argument-for-argument what the old declaration used, and the Mathlib spelling ContDiff ℝ (⊤ : ℕ∞) is still the one the pinned CG package itself uses (.../JUpperBoundWeakNorms/Product/Bound.lean). The old proof discharges this from abs_cubeAverage_vecDot_centered_scalar_cutoff_le_scaledWeakNormProduct (.../JUpperBoundWeakNorms/Product/Bridge.lean), which is present in the pinned rev.

source
theorem HCPolySupport.HighContrast.Multiscale.exists_isResponseCutoff {d : ℕ} [NeZero d] {q : Mat d} (hq : IsUnit q) (t : ℤ) :
∃ (φ : Vec d → ℝ), IsResponseCutoff q t φ

The cutoff class IsResponseCutoff (ResponseBlockObjects.lean) is nonempty on every invertible grid.

A pullback Lipschitz constant 3^(-t) carrying no dimensional factor is too small: a point of a cube of side 3^t is at sup-distance at most 3^t/2 from the complement, so such a cutoff is at most 1/2 everywhere and cannot have mean one. The constant 32 * d ^ 2 * 3 ^ (-t) repairs this, and a PIECEWISE-LINEAR witness attains it.

The class also carries the four conjuncts that the reference-cube cutoff bound consumes -- ContDiff R (top : N-infty) phi, HasCompactSupport phi, tsupport phi subseteq adaptedCell q t and the second-derivative bound 1024 * d ^ 4 * Theta ^ 2 * 3 ^ (-2 * t), with the universal profile factor Theta (see the docstring of IsResponseCutoff) -- and the witness is built here as a genuinely smooth one.

The witness is the adapted avatar of the construction in HCPoly/Provider/Response/CutoffBasic.lean, adaptedPreYoungCutoff, assembled from the same two objects of the pinned CoarseGraining package: the canonical product cube cutoff QuantitativeCubeCutoff.canonicalFun Q rho1 rho2 (HCPolySupport/Sobolev/Foundations/QuantitativeCutoff.lean) built on smoothTransitionProfile (.../Cutoff/Profile.lean), taken on the reference cube Q = originCube d t at rho1 = 1 - 1/(2d), rho2 = 1 - 1/(4d), normalized by its own cell average A and pushed forward by q.

The five constants come out exactly as in the earlier construction. The collar is (rho2 - rho1) * cubeRadius Q = 3^t / (8 d), so canonicalFun_gradient_bound gives ‖D phi_0‖ <= 16 d^2 Theta 3^(-t) and canonicalFun_hessian_bound gives ‖D^2 phi_0‖ <= 512 d^4 Theta^2 3^(-2t); the normalization costs a factor A⁻¹ <= 2, since phi_0 = 1 on the inner cube of relative radius rho1 and (1 - 1/(2d))^d >= 1/2 by Bernoulli (cutoff_bernoulli_bound), which also bounds the cutoff by 2. Doubling the two bounds gives precisely the class constants 32 d^2 Theta 3^(-t) and 1024 d^4 Theta^2 3^(-2t). Compact support and tsupport phi subseteq adaptedCell q t come from rho2 < 1.

Reduction helpers for the transport. #

Four reductions that are independent of the analytic transport:

Together they reduce the transport to the PATHWISE analytic estimate.

Transport of the reference-cube cutoff bound to the adapted cell U_t. #

This is the composition of ofReal_partialSeminorm_metricPullback_fst_le_separate / …_snd_le_separate (HCPoly/Provider/Response/AdaptedWeakProduct.lean and) with the reference-cube cutoff product-term weak-norm bound above and explicitRoundedGrid_metricFrobenius_product_le (AdaptedWeakProduct.lean). In the present vocabulary the first two are partialSeminorm_pullback_fst_le / …_snd_le and the third is explicitRoundedGrid_metricFrobenius_product_le, all three stated in HCPoly/Entry/Response/Kernel/ScaleAverageSeminorm.lean.

The three ingredients of integrable_besovSeminorm_sq_respCell. #

integrable_besovSeminorm_sq_respCell below is proved from three named private lemmas by the reduction (Integrable = AEStronglyMeasurable ∧ HasFiniteIntegral, the finite integral by domination). Two of the three are analytic; the third, hc3_aestronglyMeasurable_besovSeminorm_sq, is a statement-level gap recorded in its own docstring.