High-contrast homogenization: Entry.Response.Cutoff.PathwiseCutoffBoundReduction

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

The pathwise cutoff bound, landed and reduced to integrability

This file proves the inequality half of the pathwise cutoff bound of e.response.cutoff.estimate (AK.HC Lemma A.1, (A.4)): pairing the centred pulled-back potential against the pulled-back flux defect with the pulled-back cutoff weight field, it bounds the two negative-Besov inputs by the scale-average seminorm of the M_0^{1/2}-transported, recentred cell averages, and the four coefficients by the dimension and the grid data. It lands this estimate as a single existential in the dimension: for every selected grid, response cutoff, positive-definite block, and almost-everywhere elliptic coefficient, the pathwise cutoff pairing bound holds on the adapted cell respCell jStar F t. It closes by reducing the resulting pairing's integrability over the coefficient law to its measurability, since the bound dominates the pairing, sample by sample, by a fixed multiple of the integrable scale-weighted squared seminorm.

The inequality half of the pathwise cutoff bound

The negative-Besov duality bound of the cutoff argument (AK.HC Lemma A.1, (A.4)) pairs the centred pulled-back potential against the pulled-back flux defect with the pulled-back cutoff weight field. Its two negative-Besov inputs are bounded by the scale-average seminorm of the M_0^{1/2}-transported, recentred cell averages, and its four coefficients are bounded by the cutoff class, the scale weights of the reference cube and the dimensional Frobenius product Frob₁ · Frob₂ ≤ 3 d². The present file carries out the whole bookkeeping and concludes the pathwise estimate e.response.cutoff.estimate in the exact shape consumed by the annealed reduction: an explicit dimensional constant (depending only on the dimension and the universal cutoff profile constant) times the scale weight 3^{-t} times the square of the scale-average seminorm of the recentred doubled optimizer state.

The constant is kept explicit and no existential is introduced.

theorem HCPolySupport.HighContrast.Multiscale.abs_cubeAverage_pullback_pairing_le_besov_sq {d : ℕ} [NeZero d] {jStar : ℕ} (hjStar : 2 * d ≤ 3 ^ jStar) {F : BlockMat d} (hm : Matrix.PosDef (explicitCanonicalMetric F)) (t : ℤ) {b : CoeffField d} (hb : ∃ (lam : ℝ) (Lam : ℝ) (f : CoeffField d), 0 < lam ∧ lam ≤ Lam ∧ IsEllipticFieldOn lam Lam (respCell jStar F t) f ∧ b =ᵐ[volumeMeasureOn (respCell jStar F t)] f) (u : AHarmonicFunction b (respCell jStar F t)) (Y : BlockVec d) {φ : Vec d → ℝ} (hφ : IsResponseCutoff (respGrid jStar F) t φ) : |cubeAverage (originCube d t) fun (y : Vec d) => vecDot (matVecMul (respGrid jStar F)⁻¹ (optimizerField b u (matVecMul (respGrid jStar F) y) - Y).2) (((respCenteredPullbackH1 hjStar hm t b u Y).toFun y - cubeAverage (originCube d t) fun (z : Vec d) => (respCenteredPullbackH1 hjStar hm t b u Y).toFun z) • scalarCutoffGradientField (fun (y : Vec d) => φ (matVecMul (respGrid jStar F) y)) y)| ≤ (2048 * ↑d ^ 4 * responseCutoffProfileConst ^ 2 + 96 * ↑d ^ 2 * responseCutoffProfileConst) * (↑d * Legacy.cubeNeumannW22CalderonZygmundConstant d * 3 ^ (↑d + 1) * ↑d * (↑d * 3 ^ (↑d + 1 / 2))) * (3 * ↑d ^ 2) * (3 ^ (-↑t) * (besovSeminorm t fun (n : ℕ) (z : Fin d → ℤ) => blockMatVecMul (blockSqrt (respM0 F)) (cellAverage (adaptedCellAtCenter (respGrid jStar F) (t - ↑n) z) (optimizerField b u) - Y)) ^ 2)

The pathwise cutoff pairing bound in the shape of the annealed estimate. For a doubled block F whose canonical metric is positive definite, a reference cube Q = originCube d t, a cutoff φ in the response cutoff class, and a coefficient b that agrees almost everywhere on the adapted cell with a uniformly elliptic field, the absolute cube average of the pulled-back flux defect against the centred pulled-back potential times the pulled-back cutoff gradient is bounded by an explicit dimensional constant times the scale weight 3^{-t} times the square of the scale-average seminorm of the recentred M_0^{1/2}-transported doubled optimizer state. This is the inequality half of the pathwise form of e.response.cutoff.estimate; it is the duality bound AK.HC Lemma A.1, (A.4) with all four coefficient families and both negative-Besov inputs discharged.

The pathwise cutoff pairing bound with every hypothesis discharged

The annealed cutoff bound e.response.cutoff.estimate is reduced by the frame theorems to the deterministic pathwise estimate hpath on the adapted cell respCell jStar F t. This file lands that estimate as a single existential in the dimension: for every selected grid, every response cutoff, every positive-definite block and every a.e.-elliptic representative of the coefficient, the absolute volume average of the cutoff times the pairing of the centred doubled optimizer state is at most a dimension-only constant times the scale weight 3 ^ (-t) times the square of the scale-average seminorm of the M_0 ^ (1/2)-transported recentred state.

The volume average is first identified with the centred cube average on the reference cube by the integration by parts of the cutoff pairing (AK.HC Lemma A.1, (A.4)), the change of variables x = (respGrid jStar F) y and the vanishing of the flux defect against the cutoff gradient; the resulting cube average is then bounded by the negative-Besov duality bound with all four coefficient families discharged. The integrability side conditions of the identification are supplied here: the flux defect against the cutoff gradient is L² on the reference cube because the flux defect is L² and the cutoff gradient is essentially bounded, the centred potential multiplied by that pairing is integrable because the pulled-back potential is L², and the centred-potential pairing on the cell is its change of variables. The constant is the explicit dimension-only constant of abs_cubeAverage_pullback_pairing_le_besov_sq, so it depends on no other datum.

theorem HCPolySupport.HighContrast.Multiscale.exists_pathwise_cutoff_pairing_bound (d : ℕ) [NeZero d] : ∃ (C₀ : ℝ), 0 ≤ C₀ ∧ ∀ (jStar : ℕ) (F : BlockMat d) (t : ℤ) (φ : Vec d → ℝ), 2 * d ≤ 3 ^ jStar → IsResponseCutoff (respGrid jStar F) t φ → Matrix.PosDef (explicitCanonicalMetric F) → ∀ (b : CoeffField d) (Y : BlockVec d) (u : AHarmonicFunction b (respCell jStar F t)), (∃ (lam : ℝ) (Lam : ℝ) (f : CoeffField d), 0 < lam ∧ lam ≤ Lam ∧ IsEllipticFieldOn lam Lam (respCell jStar F t) f ∧ b =ᵐ[volumeMeasureOn (respCell jStar F t)] f) → |volumeAverage (respCell jStar F t) fun (x : Vec d) => φ x * vecDot ((optimizerField b u x).1 - Y.1) ((optimizerField b u x).2 - Y.2)| ≤ C₀ * (3 ^ (-↑t) * (besovSeminorm t fun (n : ℕ) (z : Fin d → ℤ) => blockMatVecMul (blockSqrt (respM0 F)) (cellAverage (adaptedCellAtCenter (respGrid jStar F) (t - ↑n) z) (optimizerField b u) - Y)) ^ 2)

The pathwise cutoff pairing bound e.response.cutoff.estimate (AK.HC Lemma A.1, (A.4)) with every hypothesis discharged, in the exact shape of the hpath hypothesis of exists_integral_abs_pairing_le_respWeak_of_pathwise. There is a dimension-only constant C₀ such that, for every grid depth jStar, block F, scale t, response cutoff φ, positive definite canonical metric, coefficient b with an a.e.-elliptic representative on the adapted cell and b-harmonic optimizer u, the absolute volume average on respCell jStar F t of the cutoff times the pairing of the centred doubled optimizer state with Y is at most C₀ times the scale weight 3 ^ (-t) times the square of the scale-average seminorm of the M_0 ^ (1/2)-scaled recentred state.

Integrability of the cutoff pairing, reduced to its measurability

The pathwise cutoff pairing bound e.response.cutoff.estimate (AK.HC Lemma A.1, (A.4)) dominates the absolute cutoff pairing, sample by sample, by a fixed multiple of the scale-weighted squared scale-average seminorm of the M_0 ^ (1/2)-transported recentred optimizer state. Consequently the pairing is integrable over the law as soon as it is measurable and that seminorm square is integrable, which isolates measurability as the only remaining obstruction to the integrability premise of the cutoff rows.

theorem HCPolySupport.HighContrast.Multiscale.integrable_abs_pairing_of_measurable_of_integrable_besov {d : ℕ} [NeZero d] (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (φ : Vec d → ℝ) (hjStar : 2 * d ≤ 3 ^ jStar) (hφ : IsResponseCutoff (respGrid jStar F) t φ) (hm : Matrix.PosDef (explicitCanonicalMetric F)) (c : CoeffSpace d → CoeffField d) (hc : ∀ (a : CoeffSpace d), ∃ (lam : ℝ) (Lam : ℝ) (f : CoeffField d), 0 < lam ∧ lam ≤ Lam ∧ IsEllipticFieldOn lam Lam (respCell jStar F t) f ∧ c a =ᵐ[volumeMeasureOn (respCell jStar F t)] f) (Y : BlockVec d) (u : (a : CoeffSpace d) → AHarmonicFunction (c a) (respCell jStar F t)) (hmeas : MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => |volumeAverage (respCell jStar F t) fun (x : Vec d) => φ x * vecDot ((optimizerField (c a) (u a) x).1 - Y.1) ((optimizerField (c a) (u a) x).2 - Y.2)|) P) (hbesov : MeasureTheory.Integrable (fun (a : CoeffSpace d) => (besovSeminorm t fun (n : ℕ) (z : Fin d → ℤ) => blockMatVecMul (blockSqrt (respM0 F)) (cellAverage (adaptedCellAtCenter (respGrid jStar F) (t - ↑n) z) (optimizerField (c a) (u a)) - Y)) ^ 2) P) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => |volumeAverage (respCell jStar F t) fun (x : Vec d) => φ x * vecDot ((optimizerField (c a) (u a) x).1 - Y.1) ((optimizerField (c a) (u a) x).2 - Y.2)|) P

The cutoff pairing is P-integrable whenever it is P-a.e.-strongly measurable and the scale-weighted squared scale-average seminorm of the M_0 ^ (1/2)-scaled recentred optimizer state is P-integrable. The pathwise bound e.response.cutoff.estimate (AK.HC Lemma A.1, (A.4)) dominates the absolute pairing by a fixed multiple of that seminorm square, so the finite-integral half of Integrable follows by domination, while the measurability half is supplied as the hypothesis. The elliptic-representative hypothesis on the coefficient family is exactly the hypothesis consumed by the pathwise bound, and no further regularity of the pairing is required.