Aggregation #

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Mesoscale aggregation for the unconditional response estimate #

Source: ABK26, the aggregation half of the J statement of l.J.sensitivity.no.conditions.

The source proof of e.J.sensitivity.no.conditions has two halves.

A per-mesoscopic-cube conditional estimate: on every triadic cube R of the mesoscopic depth H, the response of the perturbed field at the loading ((mu sigma0)^{-1/2} e, (mu sigma0)^{1/2} e) is bounded by 6 mu^{-1} times the response of the base field at the sigma0-normalized loading, plus three error families carrying the R-local coarse gauge lambda_{3/8,2}^{-1}(R;a).
An aggregation: subadditivity at depth H, the homogenization-error bridge for the main term, the descendant scaling of the coarse gauge for the gauge terms, and the Young/min bookkeeping of Provider.Mesoscale.ScaleSelection for the gradient terms.

This module contains only the aggregation half, in the exact shape of the frozen conclusion. The per-cube estimate enters as the hypothesis hcube of responseJ_le_frozen_of_mesoscale_cube_bound; nothing here proves or assumes any part of it. The gauge-free arithmetic is in Provider.ResponseUnconditional.MesoscaleArithmetic.

Consumption points #

hcube. The per-mesoscopic-cube conditional estimate. It is written with the root family F on the right-hand side (so the main term is exactly the quantity fed to Provider.HomogBridge.Bridge), the R-local coarse gauge lambda_{3/8,2}^{-1}(R; F), and the constant scale factor 3^{-2H} of the mesoscopic depth (which equals cubeScaleFactor R ^ 2 on every cube of descendantsAtDepth (originCube d 0) H).
hV. An abstract nonnegative value budget V whose depth-H descendant average is at most h.valueL2 ^ 2. For the concrete D_h route V R is the normalized L^2 average of |h|^2 over R, and hV is then the exact tower identity cubeAverage_eq_descendantsAverage_cubeAverage_of_integrableOn.

Every declaration in this module is an internal helper for the Section 2.4 sensitivity providers.

The pointwise fold of the per-cube right-hand side #

Pure real arithmetic: the three gauge-carrying families of the per-cube estimate are bounded by their values at the uniform gauge bound WL, leaving only the main term and the value budget inside the descendant average.

The uniform mesoscopic gauge bound #

source

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.lambdaSq_inv_le_rpow_mul_unitCubeLambda_inv {d : ℕ} [NeZero d] (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (hF : (F.coeffOn (HCPolySupport.originCube d 0)).AEEq a) {s : ℝ} (hs0 : 0 < s) (hs : s ≤ 1 / 4) (H : ℕ) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d 0) H) :

(HCPolySupport.Book.Ch02.lambdaSq R (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) F)⁻¹ ≤ Real.rpow 3 (2 * s * ↑H) * (Frozen.Section24.unitCubeLambda s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹

The descendant scaling of the coarse gauge at the mesoscopic depth. For every triadic cube R of depth H below the unit cube,

λ_{3/8,2}^{-1}(R; a) ≤ λ_{s,2}^{-1}(R; a) ≤ 3^{2 s H} λ_{s,2}^{-1}(□₀; a) .

This is the display of ABK26; the first step uses 2 s ≤ 1/2 < 3/4.

The aggregation #

source

The mesoscale aggregation of the unconditional response estimate.

Given the per-mesoscopic-cube conditional estimate hcube at the mesoscopic depth H = mesoscaleDepth s (1 + C₀ ‖∇h‖ λ_{s,2}^{-1}), the four families of terms aggregate to exactly the four terms of the frozen conclusion Algsuperdiff.Frozen.Section24.responseJ_sensitivity_unconditional, with the explicit constant aggConst C₀ K.

This is ABK26.