BoundProvider

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

The provider result for the frozen D_h bound

Source: ABK26 (l.Dh.bound).

This module assembles the completed proof of the frozen target Algsuperdiff.Frozen.Section24.coarseMatrixDerivative_bound:

• the splitting identity with the H¹₀ premise discharged, consumed here through the zero-trace witness itself (Adjoint.exists_h10Function_grad_ae_eq_halfSum_add_const_unitCube);
• the two-budget assembly Assembly.abs_quadForm_coarseMatrixDerivative_le_of_positiveBesov_budgets;
• the Term A budget Discharge.InputA;
• the Term BC budget Discharge.InputBC;
• the arithmetic fold Assembly.abs_le_frozen_shape_of_budget_bounds.

The constant is explicit:

C(d) = 2 (1 + d 3^{d+1}) (2 c_{3/8,2}^{-1/2}) ( termABesovConst d + termBCBesovConst d ).

The explicit constant

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.DhBound.dhPairingConst (d : ℕ) : ℝ

The Besov pairing constant of the D_h assembly.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.DhBound.dhPairingConst d = Algsuperdiff.Section24.Sensitivity.Provider.PairingConstants.besovPairingConstant d

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.dhPairingConst_pos (d : ℕ) : 0 < dhPairingConst d

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.termABesovConst_pos {d : ℕ} (hd : 2 ≤ d) : 0 < Discharge.termABesovConst d

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.DhBound.dhBoundConst (d : ℕ) : ℝ

The explicit constant of the frozen D_h bound.

Equations

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.dhBoundConst_pos {d : ℕ} (hd : 2 ≤ d) : 0 < dhBoundConst d

The provider result

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.coarseMatrixDerivative_bound {d : ℕ} (dimension : 2 ≤ d) : ∃ (C : ℝ), 0 < C ∧ ∀ (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (p q : HCPolySupport.Vec d), |HCPolySupport.blockVecDot (p, -q) (HCPolySupport.blockMatVecMul (Frozen.Section24.coarseMatrixDerivative (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a ↑h.toLInfSkewMatrixFieldOn) (p, -q))| ≤ C * (HCPolySupport.Book.Ch02.vecNorm p * h.w1Infinity * √(Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹ + √|HCPolySupport.vecDot p q| * h.gradientW1Infinity * (Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹) * √(HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a p q) + C * h.gradientW1Infinity * (Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹ * HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a p q

The unit-cube sensitivity estimate for the coarse-matrix derivative.

This is the provider form of the frozen target Algsuperdiff.Frozen.Section24.coarseMatrixDerivative_bound, with exactly the frozen binders.