Skeleton

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

Assembly skeleton for the frozen D_h bound

Source: ABK26 (proof of l.Dh.bound).

The proof of the frozen target Algsuperdiff.Frozen.Section24.coarseMatrixDerivative_bound is assembled from

• the splitting identity quadForm_coarseMatrixDerivative_unitCube_eq_split (e.sensitivity.basic.split);
• the Besov pairing engine abs_cubeAverage_vecDot_grad_le_of_positiveBesov_bound (e.sensitivity.basic.split1, e.split.besov.stuff.begin), which already contains the coarse Poincaré inequality e.w.wstar.to.energy;
• two positive Besov budgets, one for each factor of the split.

This module performs the algebraic assembly of the first two, leaving the two budgets as explicit premises of an internal helper. B_A bounds the positive B^{3/8}_{2,2} norm of x ↦ hᵀ(x) p, B_BC bounds the positive B^{3/8}_{2,2} norm of x ↦ (w + w* + ℓ_p)(x) (∇·h)(x).

The helper is deliberately internal: it is never re-exported as a provider result while its premises are undischarged.

Moving the fixed factor to the second slot of the pairing

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Assembly.vecDot_matVecMul_eq_vecDot_matTranspose {d : ℕ} (M : HCPolySupport.Mat d) (x y : HCPolySupport.Vec d) : HCPolySupport.vecDot x (HCPolySupport.matVecMul M y) = HCPolySupport.vecDot y (HCPolySupport.matVecMul (HCPolySupport.matTranspose M) x)

Adjoint form of the matrix pairing: x · (M y) = y · (Mᵀ x).

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Assembly.mul_vecDot_eq_vecDot_smul {d : ℕ} (c : ℝ) (D g : HCPolySupport.Vec d) : c * HCPolySupport.vecDot D g = HCPolySupport.vecDot g (c • D)

Scalar multiple form of the pairing: c (D · g) = g · (c • D).

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Assembly.average_congr_funext {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} {f g : HCPolySupport.Vec d → ℝ} (hfg : ∀ (x : HCPolySupport.Vec d), f x = g x) : HCPolySupport.Book.Ch02.average U f = HCPolySupport.Book.Ch02.average U g

Pointwise congruence for the Chapter 2 average.

The assembly helper

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Assembly.abs_quadForm_coarseMatrixDerivative_le_of_positiveBesov_budgets {d : ℕ} [NeZero d] (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (p q : HCPolySupport.Vec d) (F : HCPolySupport.Book.Ch03.CoeffFamily d) (hF : (F.coeffOn (HCPolySupport.originCube d 0)).AEEq a) (vAdj : HCPolySupport.Book.Ch02.Solution (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a.transpose) (v : HCPolySupport.Book.Ch02.Solution (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a) (hvAdj : HCPolySupport.Book.Ch02.IsResponseMaximizer (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a.transpose p (-q) vAdj) (hv : HCPolySupport.Book.Ch02.IsResponseMaximizer (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a p q v) (u : HCPolySupport.H10Function (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier) (hu : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier, u.grad x = 2⁻¹ • (vAdj.toH1.grad x + v.toH1.grad x) + p) {BA BBC : ℝ} (hHA : HCPolySupport.Book.Ch03.ForceBesovRegularity (HCPolySupport.originCube d 0) (3 / 8) fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul (HCPolySupport.matTranspose (↑↑h.toLInfSkewMatrixFieldOn x)) p) (hHAle : (HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorNormTwo (HCPolySupport.originCube d 0) (3 / 8) fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul (HCPolySupport.matTranspose (↑↑h.toLInfSkewMatrixFieldOn x)) p) ≤ BA) (hHBC : HCPolySupport.Book.Ch03.ForceBesovRegularity (HCPolySupport.originCube d 0) (3 / 8) fun (x : HCPolySupport.Vec d) => u.toFun x • matWeakDiv (unitCubeDerivData h) x) (hHBCle : (HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorNormTwo (HCPolySupport.originCube d 0) (3 / 8) fun (x : HCPolySupport.Vec d) => u.toFun x • matWeakDiv (unitCubeDerivData h) x) ≤ BBC) : |HCPolySupport.blockVecDot (p, -q) (HCPolySupport.blockMatVecMul (Frozen.Section24.coarseMatrixDerivative (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a ↑h.toLInfSkewMatrixFieldOn) (p, -q))| ≤ 2 * ((1 + ↑d * Real.rpow 3 (↑d + 1)) * (2 * HCPolySupport.Book.Ch03.poincareDiscountFactor (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2))) * (BA + BBC) * (√(Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹ * √(HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a p q))

Internal assembly helper for the frozen D_h bound.

Given the splitting witness u and the two positive Besov budgets B_A, B_BC, the frozen quadratic form is bounded by 4 K(d) (B_A + B_BC) λ_{3/8,2}^{-1/2} J^{1/2}, K(d) = (1 + d 3^{d+1}) c_{3/8,2}^{-1/2}.

The Young/triangle fold into the frozen right-hand side

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Assembly.abs_le_frozen_shape_of_budget_bounds {X K CA CBC np w g sl spq sJ BA BBC : ℝ} (hK : 0 ≤ K) (hCA : 0 ≤ CA) (hCBC : 0 ≤ CBC) (hnp : 0 ≤ np) (hw : 0 ≤ w) (hg : 0 ≤ g) (hsl : 0 ≤ sl) (hspq : 0 ≤ spq) (hsJ : 0 ≤ sJ) (hX : |X| ≤ 2 * K * (BA + BBC) * (sl * sJ)) (hBA : BA ≤ CA * np * w) (hBBC : BBC ≤ CBC * g * sl * (sJ + spq)) : |X| ≤ 2 * K * (CA + CBC) * (np * w * sl + spq * g * (sl * sl)) * sJ + 2 * K * (CA + CBC) * g * (sl * sl) * (sJ * sJ)

Arithmetic fold. The abstract inequality behind the last two lines of the source proof: substituting the two budget bounds into |X| ≤ 2K(B_A + B_BC) √(λ⁻¹) √J and expanding (P · 𝐀 P)^{1/2} = (2(J + p·q))^{1/2} ≤ √2 (√J + √|p·q|) (e.J.by.means.of.bfA) produces exactly the frozen right-hand side.