CubeEllipticity

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

The coarse ellipticity chain at a general triadic cube

Source: ABK26, the loading half of e.split.besov.stuff.begin.

Provider.DhBound.Discharge.EllipticityOrdered already proves the chain

|p|² ≤ |σ_*^{-1}(U; a)| · 2 (J(U, p, q; a) + p·q)

at an arbitrary Chapter 2 domain, and CoarseGraining's Ch02.oneCube_sigmaStarInv_le_lambdaSq_finite_inv bounds |σ_*^{-1}(R; a)| by λ_{s,q}^{-1}(R; a) at an arbitrary triadic cube. This module combines the two at the pure-potential loading q = 0, where the cross term p·q vanishes and the chain becomes the clean budget

|p| ≤ √2 · λ_{3/8,2}^{-1/2}(R; a) · J(R, p, 0; a)^{1/2} .

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.lambdaSq_sensitivity_pos {d : ℕ} [NeZero d] (R : HCPolySupport.TriadicCube d) (G : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) : 0 < HCPolySupport.Book.Ch02.lambdaSq R (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) G

The coarse gauge of a compatible family at any triadic cube is positive.

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.lambdaSq_inv_nonneg {d : ℕ} [NeZero d] (R : HCPolySupport.TriadicCube d) (G : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) : 0 ≤ (HCPolySupport.Book.Ch02.lambdaSq R (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) G)⁻¹

λ_{3/8,2}^{-1}(R; a) ≥ 0.

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.vecNormSq_le_lambdaSq_inv_mul_two_mul_responseJ {d : ℕ} [NeZero d] (R : HCPolySupport.TriadicCube d) (G : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (b : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain R)) (hG : (G.coeffOn R).AEEq b) (p : HCPolySupport.Vec d) : HCPolySupport.vecNormSq p ≤ (HCPolySupport.Book.Ch02.lambdaSq R (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) G)⁻¹ * (2 * HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) b p 0)

The ellipticity chain at a general triadic cube, pure-potential loading.

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.vecNorm_le_sqrt_two_mul_sqrt_lambdaSq_inv_mul_sqrt_responseJ {d : ℕ} [NeZero d] (R : HCPolySupport.TriadicCube d) (G : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (b : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain R)) (hG : (G.coeffOn R).AEEq b) (p : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.vecNorm p ≤ √2 * (√(HCPolySupport.Book.Ch02.lambdaSq R (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) G)⁻¹ * √(HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) b p 0))

The loading budget at a general triadic cube, pure-potential loading.