CubeRatio

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

From a pure-flux response ratio to a sigma_*^{-1} operator-norm ratio

Source: ABK26: the conditional lambda_{s,q} sensitivity estimate applies the D_h bound specialized to the bottom right entry of A(cube), i.e. to the pure-flux matrix sigma_*^{-1}, on every triadic descendant of the unit cube.

The bottom-right specialization is purely algebraic. sigma_*^{-1}(U; a) is defined entrywise from the pure-flux response J(U, a, 0, ·) (Book.Ch02.sigmaStarInvEntry), and its quadratic form is exactly

q · sigma_*^{-1}(U; a) q = 2 J(U, a, 0, q) .

Hence a ratio estimate J(U, b1, 0, q) ≤ rho * J(U, b0, 0, q) valid for every loading q is precisely a Löwner comparison sigma_*^{-1}(U; b1) ≤ rho * sigma_*^{-1}(U; b0), and since both matrices are positive semidefinite the Euclidean operator norm Book.Ch02.matrixNorm is monotone along that order. No polarization of the off-diagonal entries is needed: the quadratic form determines the comparison.

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

Scaling of the Euclidean operator matrix norm

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.matrixNorm_smul {d : ℕ} (c : ℝ) (A : HCPolySupport.Mat d) : HCPolySupport.Book.Ch02.matrixNorm (c • A) = |c| * HCPolySupport.Book.Ch02.matrixNorm A

The Euclidean operator matrix norm is absolutely homogeneous.

The pure-flux quadratic form

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.vecDot_matVecMul_sigmaStarInvCoarse {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (q : HCPolySupport.Vec d) : HCPolySupport.vecDot q (HCPolySupport.matVecMul (HCPolySupport.Book.Ch02.sigmaStarInvCoarse U a) q) = 2 * HCPolySupport.Book.Ch02.responseJ U a 0 q

The quadratic form of sigma_*^{-1}(U; a) is twice the pure-flux response.

The Löwner comparison

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.matLoewnerLE_smul_of_responseJ_le {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (b₀ b₁ : HCPolySupport.Book.Ch02.CoeffOn U) {ρ : ℝ} (hJ : ∀ (q : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.responseJ U b₁ 0 q ≤ ρ * HCPolySupport.Book.Ch02.responseJ U b₀ 0 q) : HCPolySupport.MatLoewnerLE (HCPolySupport.Book.Ch02.sigmaStarInvCoarse U b₁) (ρ • HCPolySupport.Book.Ch02.sigmaStarInvCoarse U b₀)

A pure-flux response ratio at every loading is a Löwner comparison of the pure-flux matrices.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.posSemidef_smul_of_nonneg {d : ℕ} {A : HCPolySupport.Mat d} (hA : Matrix.PosSemidef A) {ρ : ℝ} (hρ : 0 ≤ ρ) : Matrix.PosSemidef (ρ • A)

A scalar multiple of a positive semidefinite matrix by a nonnegative scalar is positive semidefinite, in the ambient Mat d spelling.

The one-cube ratio

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.matrixNorm_sigmaStarInvCoarse_le_of_responseJ_le {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (b₀ b₁ : HCPolySupport.Book.Ch02.CoeffOn U) {ρ : ℝ} (hρ : 0 ≤ ρ) (hJ : ∀ (q : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.responseJ U b₁ 0 q ≤ ρ * HCPolySupport.Book.Ch02.responseJ U b₀ 0 q) : HCPolySupport.Book.Ch02.matrixNorm (HCPolySupport.Book.Ch02.sigmaStarInvCoarse U b₁) ≤ ρ * HCPolySupport.Book.Ch02.matrixNorm (HCPolySupport.Book.Ch02.sigmaStarInvCoarse U b₀)

The one-cube sigma_*^{-1} ratio from a pure-flux response ratio.

If the pure-flux response of b₁ is at most rho times that of b₀ at every loading, the same ratio holds for the Euclidean operator norms of the pure-flux matrices. This is the bottom-right specialization used at every triadic descendant in the proof of the conditional lambda_{s,q} sensitivity estimate.