EllipticityOrdered

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

The loading is controlled by the coarse gauge and the response

Source: ABK26, the last summand of the three-way split of the source combination ∇w + ∇w^* + ℓ_p: the affine piece contributes the constant gradient p, and the proof of l.Dh.bound estimates |p| by the ellipticity chain e.cg.bounds.basic.definitions together with e.J.by.means.of.bfA,

|p|² ≤ |σ_*^{-1}| (p · σ_* p) ≤ |σ_*^{-1}| (p · σ p) ≤ λ_{3/8,2}^{-1} · 2 (J + p·q) .

The three inequalities are, in order,

• Book.Ch02.vecNormSq_le_matrixNorm_mul_vecDot_matVecMul_of_posSemidef_of_leftInverse applied with the (unconditionally invertible) pair σ_*, σ_*^{-1};
• the Löwner order Book.Ch02.sigmaStarCoarse_le_sigmaCoarse;
• the canonical coarse-matrix formula Book.Ch02.responseJ_eq_coarseMatrices_formula_canonical, whose middle term is a nonnegative quadratic form in q + κ p.

The one-cube ellipticity bound Book.Ch02.oneCube_sigmaStarInv_le_lambdaSq_finite_inv then replaces |σ_*^{-1}| by the coarse gauge, which is transported to the frozen unitCubeLambda by the characterization theorem, exactly as in Provider.DhBound.Assembly.GaugeBridge.

The general-domain chain

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.matVecMul_sigmaStarInvCoarse_sigmaStarCoarse {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (ξ : HCPolySupport.Vec d) : HCPolySupport.matVecMul (HCPolySupport.Book.Ch02.sigmaStarInvCoarse U a) (HCPolySupport.matVecMul (HCPolySupport.Book.Ch02.sigmaStarCoarse U a) ξ) = ξ

σ_*^{-1} is a left inverse of σ_* at every Chapter 2 domain.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.vecNormSq_le_matrixNorm_mul_vecDot_sigmaStarCoarse {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (p : HCPolySupport.Vec d) : HCPolySupport.vecNormSq p ≤ HCPolySupport.Book.Ch02.matrixNorm (HCPolySupport.Book.Ch02.sigmaStarInvCoarse U a) * HCPolySupport.vecDot p (HCPolySupport.matVecMul (HCPolySupport.Book.Ch02.sigmaStarCoarse U a) p)

The first link of the ellipticity chain.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.vecDot_sigmaStarCoarse_le_vecDot_sigmaCoarse {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (p : HCPolySupport.Vec d) : HCPolySupport.vecDot p (HCPolySupport.matVecMul (HCPolySupport.Book.Ch02.sigmaStarCoarse U a) p) ≤ HCPolySupport.vecDot p (HCPolySupport.matVecMul (HCPolySupport.Book.Ch02.sigmaCoarse U a) p)

The second link: the Löwner order σ_* ≤ σ.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.vecDot_sigmaCoarse_le_two_mul_add {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (p q : HCPolySupport.Vec d) : HCPolySupport.vecDot p (HCPolySupport.matVecMul (HCPolySupport.Book.Ch02.sigmaCoarse U a) p) ≤ 2 * (HCPolySupport.Book.Ch02.responseJ U a p q + HCPolySupport.vecDot p q)

The third link: the pure-gradient quadratic form is at most 2 (J + p·q).

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.vecNormSq_le_matrixNorm_sigmaStarInvCoarse_mul_two_mul_add {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (p q : HCPolySupport.Vec d) : HCPolySupport.vecNormSq p ≤ HCPolySupport.Book.Ch02.matrixNorm (HCPolySupport.Book.Ch02.sigmaStarInvCoarse U a) * (2 * (HCPolySupport.Book.Ch02.responseJ U a p q + HCPolySupport.vecDot p q))

The ellipticity chain at a general Chapter 2 domain.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.zero_le_two_mul_responseJ_add_vecDot {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (p q : HCPolySupport.Vec d) : 0 ≤ 2 * (HCPolySupport.Book.Ch02.responseJ U a p q + HCPolySupport.vecDot p q)

The right-hand quadratic budget of the ellipticity chain is nonnegative.

The frozen unit-cube gauge

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.unitCubeLambda_sensitivity_pos {d : ℕ} [NeZero d] (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) : 0 < Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a

The frozen coarse gauge at the sensitivity exponents is positive.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.vecNormSq_le_unitCubeLambda_inv_mul_two_mul_add {d : ℕ} [NeZero d] (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (p q : HCPolySupport.Vec d) : HCPolySupport.vecNormSq p ≤ (Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹ * (2 * (HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a p q + HCPolySupport.vecDot p q))

The ellipticity chain at the frozen unit-cube carrier.

The budget shape consumed by the Term BC assembly

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.vecNorm_le_sqrt_two_mul_sqrt_unitCubeLambda_inv_mul_add {d : ℕ} [NeZero d] (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (p q : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.vecNorm p ≤ √2 * √(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) + √|HCPolySupport.vecDot p q|)

The frozen budget shape for the loading.

|p| ≤ √2 · λ_{3/8,2}^{-1/2} · ( J^{1/2} + |p·q|^{1/2} ).