CubeTermBC

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

The Term BC positive Besov budget at a general triadic cube

Source: ABK26 (e.split.besov.stuff.begin through e.split.besov.stuff), stated at an arbitrary sub-cube R of the frozen unit-cube carrier.

Everything in the source estimate is scale covariant. At a cube of scale factor L = cubeScaleFactor R the three ingredients read

‖u‖_{L²(R)}                ≤ L · C · [∇u]^-_{B^{-3/8}_{2,2}(R)}   (zero-trace value)
[u]^+_{B^{3/8}_{2,2}(R),N} ≤ L · C · [∇u]^-_{B^{-3/8}_{2,2}(R)}   (function from gradient)
‖u ξ‖^+_{B^{3/8}_{2,2}(R)} ≤ C (L ‖∇ξ‖_∞ ‖u‖_{L²(R)} + ‖ξ‖_∞ [u]^+_{...})

so the whole Term BC budget carries exactly one factor L. Since every descendant of the unit cube has L ≤ 1, the surplus factor L produced by the first summand is discarded.

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

Scale-weight bookkeeping

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.cubeScaleFactor_pos_cube {d : ℕ} (R : HCPolySupport.TriadicCube d) : 0 < HCPolySupport.cubeScaleFactor R

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.cubeBesovScaleWeight_pos_cube {d : ℕ} (s : ℝ) (R : HCPolySupport.TriadicCube d) : 0 < HCPolySupport.cubeBesovScaleWeight s R

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.cubeBesovScaleWeight_neg_one_eq {d : ℕ} (R : HCPolySupport.TriadicCube d) : HCPolySupport.cubeBesovScaleWeight (-1) R = HCPolySupport.cubeScaleFactor R

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.cubeBesovScaleWeight_neg_half_sq {d : ℕ} (R : HCPolySupport.TriadicCube d) : HCPolySupport.cubeBesovScaleWeight (-(1 / 2)) R * HCPolySupport.cubeBesovScaleWeight (-(1 / 2)) R = HCPolySupport.cubeScaleFactor R

The zero-trace L² estimate at a general cube

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

The constant of the zero-trace L² estimate at the gauge exponent.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.Lambda.fluxZeroTraceConst d = Algsuperdiff.Section24.Sensitivity.Provider.PairingConstants.zeroTraceValueConst d

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.fluxZeroTraceConst_nonneg (d : ℕ) : 0 ≤ fluxZeroTraceConst d

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.cubeLpNorm_two_h10_cube_le {d : ℕ} [NeZero d] (R : HCPolySupport.TriadicCube d) (u : HCPolySupport.H10Function (HCPolySupport.Book.Ch02.cubeDomain R).carrier) : (HCPolySupport.cubeLpNorm R 2 fun (x : HCPolySupport.Vec d) => u.toFun x) ≤ HCPolySupport.cubeScaleFactor R * (fluxZeroTraceConst d * HCPolySupport.cubeBesovNegativeVectorSeminormTwo R (3 / 8) fun (x : HCPolySupport.Vec d) => u.grad x)

The zero-trace L² estimate at an arbitrary triadic cube. The scale factor of the cube appears once.

The function-from-gradient estimate at a general cube

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.fullVectorPoincareConstant_eq_origin {d : ℕ} (R : HCPolySupport.TriadicCube d) : HCPolySupport.Book.Ch01.Legacy.fullVectorPoincareConstant R = HCPolySupport.Book.Ch01.Legacy.fullVectorPoincareConstant (HCPolySupport.originCube d 0)

The multiscale Poincaré constant of CoarseGraining does not depend on the cube.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.cubeBesovPositiveScalarPartialSeminormTwo_h1_cube_le {d : ℕ} (R : HCPolySupport.TriadicCube d) (M : ℕ) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet R)) (hBdd : BddAbove (Set.range fun (N : ℕ) => HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo R (3 / 8) N fun (x : HCPolySupport.Vec d) => u.grad x)) : (HCPolySupport.cubeBesovPositiveScalarPartialSeminormTwo R (3 / 8) M fun (x : HCPolySupport.Vec d) => u.toFun x) ≤ HCPolySupport.cubeScaleFactor R * (DhBound.Discharge.depthDowngradeConst d * HCPolySupport.cubeBesovNegativeVectorSeminormTwo R (3 / 8) fun (x : HCPolySupport.Vec d) => u.grad x)

The function-from-gradient estimate at an arbitrary triadic cube, in the ℓ² form. The scale factor of the cube appears once.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.depthDowngradeConst_nonneg' (d : ℕ) : 0 ≤ DhBound.Discharge.depthDowngradeConst d

Nonnegativity of the origin-cube function-from-gradient constant.

Elementary vector bookkeeping

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.sqrt_vecNormSq_le_sqrt_card_mul_norm' {d : ℕ} (w : HCPolySupport.Vec d) : √(HCPolySupport.vecNormSq w) ≤ √↑d * ‖w‖

The Term BC field at a general cube

def Algsuperdiff.Section24.Sensitivity.Provider.Lambda.fluxTermBCField {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) {R : HCPolySupport.TriadicCube d} (u : HCPolySupport.H10Function (HCPolySupport.Book.Ch02.cubeDomain R).carrier) : HCPolySupport.Vec d → HCPolySupport.Vec d

The Term BC field x ↦ u(x) (∇·h)(x) on a sub-cube.

Equations

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.memLp_u_two_cube {d : ℕ} {R : HCPolySupport.TriadicCube d} (u : HCPolySupport.H10Function (HCPolySupport.Book.Ch02.cubeDomain R).carrier) : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => u.toFun x) 2 (HCPolySupport.normalizedCubeMeasure R)

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.memLp_fluxTermBCField_two {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) : MeasureTheory.MemLp (fluxTermBCField h u) 2 (HCPolySupport.normalizedCubeMeasure R)

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.cubeBesovPositiveVectorPartialSeminormTwo_fluxTermBCField_le {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) (N : ℕ) : HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo R (3 / 8) N (fluxTermBCField h u) ≤ DhBound.Besov.besovMultConst (3 / 8) * ((HCPolySupport.cubeScaleFactor R * (↑d ^ 2 * h.gradientW1Infinity) * HCPolySupport.cubeLpNorm R 2 fun (x : HCPolySupport.Vec d) => u.toFun x) + ↑d * h.gradientW1Infinity * HCPolySupport.cubeBesovPositiveScalarPartialSeminormTwo R (3 / 8) N fun (x : HCPolySupport.Vec d) => u.toFun x)

The finite-depth Besov product estimate for the Term BC field on a sub-cube.

The Term BC budget

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

The explicit Term B constant at the pure-flux loading.

Equations

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.fluxTermBCConst_nonneg (d : ℕ) : 0 ≤ fluxTermBCConst d

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.scaleNormalizedPositiveBesovVectorNormTwo_fluxTermBCField_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) (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.scaleNormalizedPositiveBesovVectorNormTwo R (3 / 8) (fluxTermBCField h u) ≤ fluxTermBCConst d * h.gradientW1Infinity * (HCPolySupport.cubeScaleFactor R * HCPolySupport.cubeBesovNegativeVectorSeminormTwo R (3 / 8) fun (x : HCPolySupport.Vec d) => u.grad x)

The Term BC positive Besov budget on a sub-cube of the frozen carrier.

The bound carries exactly one factor of cubeScaleFactor R; the surplus factor produced by the product rule is discarded using L ≤ 1.