Aggregation

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

The descendant b-matrix estimate and its geometric resummation

Source: ABK26.

Provider.Multiscale.GeometricResummation already performs the resummation

Lambda_{s,2}(cu_0; a₁) ≤ 4 Lambda_{s,2}(cu_0; a₀)
                            + K (3/8 - s)^{-1} lambda_{s,2}^{-1}(cu_0; a₀)

from the per-descendant estimate with the fixed same-index factor 4. The free-δ statement needs the same resummation with a general coefficient c.

coarseBMatrixNorm_perturb_le is the per-descendant input: the pure-potential J-sensitivity of BigLambda.CubeJSensitivity combined with the identity 2 J(R,p,0;a) = p·b(R;a)p of BigLambda.BMatrix.

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

The resummation with a general same-index coefficient

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.LambdaSq_two_le_of_descendant_bound_coeff {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (A₀ A₁ : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {K c s : ℝ} (hK : 0 ≤ K) (hc : 0 ≤ c) (hs0 : 0 < s) (hs : s < 3 / 8) (hdesc : ∀ (n : ℕ), ∀ R ∈ HCPolySupport.descendantsAtScale Q (Q.scale - ↑n), HCPolySupport.Book.Ch02.coarseBMatrixNorm R A₁ ≤ c * HCPolySupport.Book.Ch02.coarseBMatrixNorm R A₀ + K * (HCPolySupport.Book.Ch02.lambdaSq R (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A₀)⁻¹) : HCPolySupport.Book.Ch02.LambdaSq Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A₁ ≤ c * HCPolySupport.Book.Ch02.LambdaSq Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A₀ + K * (3 / 8 - s)⁻¹ * (HCPolySupport.Book.Ch02.lambdaSq Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A₀)⁻¹

The Lambda_{s,2} endpoint with a general same-index coefficient.

The descendant b-matrix estimate

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.coarseBMatrixNorm_perturb_le {d : ℕ} [NeZero d] (dimension : 2 ≤ d) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (hgate : h.gradientW1Infinity ≤ (bigLambdaGateConst d)⁻¹ * Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a) (F G : HCPolySupport.Book.Ch03.CoeffFamily d) (hF : (F.coeffOn (HCPolySupport.originCube d 0)).AEEq a) (hG : (G.coeffOn (HCPolySupport.originCube d 0)).AEEq (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a h.toLInfSkewMatrixFieldOn 1)) {k : ℤ} (hk : k ≤ (HCPolySupport.originCube d 0).scale) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d 0) k) {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ ≤ 1) : HCPolySupport.Book.Ch02.coarseBMatrixNorm R G ≤ (1 + δ + 2 * (potCubeConstB d * h.gradientW1Infinity * (Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹)) * HCPolySupport.Book.Ch02.coarseBMatrixNorm R F + 2 * δ⁻¹ * potCubeConstA d ^ 2 * h.w1Infinity ^ 2 * (HCPolySupport.Book.Ch02.lambdaSq R (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) F)⁻¹

The descendant b-matrix estimate, the display of ABK26 in its free-δ form. The constant is cube-independent.