CubeDhPQ

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

The D_h bound at a general loading on a sub-cube, with the scale-damped Term A

Source: ABK26 (l.Dh.bound) at the general loading (p, q) and at an arbitrary sub-cube R of the frozen unit-cube carrier.

This is the general-loading counterpart of Provider.BigLambda.CubePotentialDh.abs_dhPotentialForm_cube_le, with two changes:

• Term A uses the scale-damped budget of Provider.ResponseUnconditional.TermARefined, so its coefficient is |p| (‖h‖_{L²(R)} + |R| ‖∇h‖_{W^{1,∞}}) rather than |p| ‖h‖_{W^{1,∞}};
• Term BC uses the general-loading witness budget of Provider.ResponseUnconditional.CubeWitnessPQ, so it carries the extra |p·q|^{1/2} summand.

Both the splitting identity Provider.DhBound.Assembly.SplitIdentity and the Besov pairing Provider.DhBound.Assembly.BesovPairing are already stated at a general loading, so nothing else has to change.

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

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.dhLoadForm {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (p q : HCPolySupport.Vec d) : ℝ

The D_h quadratic form at the general loading P = (p, -q).

Equations

• One or more equations did not get rendered due to their size.

The explicit constants

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.pqCubeConstA (d : ℕ) : ℝ

The Term A coefficient of the general-loading sub-cube D_h bound.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.pqCubeConstB (d : ℕ) : ℝ

The Term BC coefficient of the general-loading sub-cube D_h bound.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.pqCubeConstA_nonneg (d : ℕ) : 0 ≤ pqCubeConstA d

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.pqCubeConstB_nonneg (d : ℕ) : 0 ≤ pqCubeConstB d

The sub-cube D_h bound at a general loading

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.abs_dhLoadForm_cube_le {d : ℕ} [NeZero d] (h : Frozen.Section24.UnitCubeSkewW2Infinity d) {R : HCPolySupport.TriadicCube d} (hsub : (HCPolySupport.Book.Ch02.cubeDomain R).carrier ⊆ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier) (hL : HCPolySupport.cubeScaleFactor R ≤ 1) (b : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain R)) (G : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (hG : (G.coeffOn R).AEEq b) (p q : HCPolySupport.Vec d) : |dhLoadForm (HCPolySupport.Book.Ch02.cubeDomain R) b (Multiscale.restrictLInfSkewMatrixFieldOn hsub h.toLInfSkewMatrixFieldOn) p q| ≤ pqCubeConstA d * (HCPolySupport.Book.Ch02.vecNorm p * (√(valueBudget h R) + HCPolySupport.cubeScaleFactor R * h.gradientW1Infinity)) * (√(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 q)) + pqCubeConstB d * (h.gradientW1Infinity * HCPolySupport.cubeScaleFactor R) * (√(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 q) * (√(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 q) + √(HCPolySupport.Book.Ch02.lambdaSq R (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) G)⁻¹ * √|HCPolySupport.vecDot p q|))

The general-loading D_h bound on a sub-cube of the frozen carrier, with the scale-damped Term A budget.