CubeBound

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

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

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

At p = 0 the splitting identity degenerates: its Term A is -2 p · ⨍_R h ∇v, which vanishes identically, so only Term BC survives. The resulting bound is

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

with the one factor of cubeScaleFactor R produced by the Term BC budget of Provider.Lambda.CubeTermBC and the two half-powers of λ^{-1} J produced by the Besov pairing engine together with the pure-flux witness budget of Provider.Lambda.WitnessBudget.

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

Besov regularity of the Term BC field on a sub-cube

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.forceBesovRegularity_fluxTermBCField {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) (fluxTermBCField h u)

The explicit constants

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.Lambda.fluxPairingConst (d : ℕ) : ℝ

The Besov pairing constant.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.Lambda.fluxPairingConst d = Algsuperdiff.Section24.Sensitivity.Provider.PairingConstants.besovPairingConstant d

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.fluxPairingConst_nonneg (d : ℕ) : 0 ≤ fluxPairingConst d

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.Lambda.fluxCubeConst (d : ℕ) : ℝ

The explicit constant of the pure-flux sub-cube D_h bound.

Equations

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.fluxCubeConst_nonneg (d : ℕ) : 0 ≤ fluxCubeConst d

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.abs_dhFluxForm_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.Ch03.CoeffFamily d) (hG : (G.coeffOn R).AEEq b) (w : HCPolySupport.Vec d) : |dhFluxForm (HCPolySupport.Book.Ch02.cubeDomain R) b (Multiscale.restrictLInfSkewMatrixFieldOn hsub h.toLInfSkewMatrixFieldOn) w| ≤ fluxCubeConst 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 0 w

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

b is an arbitrary coefficient on the sub-cube and G any CoarseGraining family representing it there.