CubePotentialDh

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

The pure-potential D_h bound on a sub-cube of the frozen carrier

Source: ABK26 (l.Dh.bound), specialized to the pure-potential loading q = 0 and stated at an arbitrary sub-cube R of the frozen unit-cube carrier.

Both terms of the splitting identity survive at q = 0:

• Term A is -2 p·⨍_R h ∇v, controlled by the general-cube Besov budget of BigLambda.CubeTermA — coefficient ‖h‖_{W^{1,∞}(□₀)} |p|, no scale factor;
• Term BC is -2 ⨍_R u (∇·h)·∇v, controlled by Provider.Lambda.CubeTermBC together with the pure-potential witness budget of BigLambda.CubeWitness — coefficient ‖∇h‖_{W^{1,∞}(□₀)} and exactly one factor cubeScaleFactor R.

The resulting bound is

|D_h(R; b)[(p,0)]| ≤ C |p| ‖h‖_{W^{1,∞}} λ_{3/8,2}^{-1/2}(R) J(R,p,0)^{1/2}
                    + C ‖∇h‖_{W^{1,∞}} · cubeScaleFactor R ·
                        λ_{3/8,2}^{-1}(R) J(R,p,0) ,

whose second coefficient is exactly the combination 3^k λ^{-1}(R) that the descendant scaling of Provider.Lambda.Closure converts into the root gauge.

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

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

The D_h quadratic form at the pure-potential loading P = (p, -0).

Equations

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

Besov regularity of the Term BC field at the pure-potential loading

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.forceBesovRegularity_potTermBCField {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) (u : HCPolySupport.H10Function (HCPolySupport.Book.Ch02.cubeDomain R).carrier) (hBdd : BddAbove (Set.range fun (N : ℕ) => HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo R (3 / 8) N fun (x : HCPolySupport.Vec d) => u.grad x)) : HCPolySupport.Book.Ch03.ForceBesovRegularity R (3 / 8) (Lambda.fluxTermBCField h u)

The explicit constants

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.potCubeConstA (d : ℕ) : ℝ

The Term A coefficient of the pure-potential sub-cube D_h bound.

Equations

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

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.potCubeConstB (d : ℕ) : ℝ

The Term BC coefficient of the pure-potential sub-cube D_h bound.

Equations

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.potCubeConstA_nonneg (d : ℕ) : 0 ≤ potCubeConstA d

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.potCubeConstB_nonneg (d : ℕ) : 0 ≤ potCubeConstB d

The sub-cube D_h bound at the pure-potential loading

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.abs_dhPotentialForm_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 : HCPolySupport.Vec d) : |dhPotentialForm (HCPolySupport.Book.Ch02.cubeDomain R) b (Multiscale.restrictLInfSkewMatrixFieldOn hsub h.toLInfSkewMatrixFieldOn) p| ≤ potCubeConstA d * h.w1Infinity * HCPolySupport.Book.Ch02.vecNorm p * (√(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)) + potCubeConstB 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 0

The pure-potential D_h bound on a sub-cube of the frozen carrier.