TermARefined

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

The scale-damped Term A Besov budget on a sub-cube

Source: ABK26, together with its mesoscopic bookkeeping.

Provider.BigLambda.CubeTermA prices the positive Besov norm of the Term A field hᵀ p against ‖h‖_{W^{1,∞}(□₀)}, uniformly in the cube. That bound is too weak for the unconditional aggregation: the Term A error is aggregated over 3^{dH} mesoscopic cubes against the root L² value norm, and the undamped W^{1,∞} bound loses the whole gain of the mesoscopic depth.

This module proves the sharp replacement

‖hᵀ p‖_{B^{3/8}_{2,2}(R)} ≤ C(d) |p| ( ‖h‖_{L²(R)} + |R| ‖∇h‖_{W^{1,∞}(□₀)} ) ,

whose two halves are:

• the mean half, bounded by the normalized L¹ average of |h| on R and hence, by Cauchy-Schwarz, by the cube-local L² value budget Provider.ResponseUnconditional.valueBudget;
• the oscillation half, bounded by cubeScaleFactor R times the Lipschitz constant of the gradient-Lipschitz representative of the value field, i.e. by |R| ‖∇h‖_{W^{1,∞}}.

At a cube of depth H below the unit cube cubeScaleFactor R = 3^{-H}, so the second half is damped exactly as the frozen statement requires.

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

The pointwise Term A bound by the Euclidean matrix norm

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.abs_termAField_le_matrixNormField {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (p x : HCPolySupport.Vec d) (i : Fin d) : |DhBound.Discharge.termAField h p x i| ≤ ↑d * HCPolySupport.Book.Ch02.vecNorm p * UnitCubeSkewW2Infinity.matrixNormField h x

The mean half

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.abs_cubeAverage_termAField_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) (p : HCPolySupport.Vec d) (i : Fin d) : |HCPolySupport.cubeAverage R fun (x : HCPolySupport.Vec d) => DhBound.Discharge.termAField h p x i| ≤ ↑d * HCPolySupport.Book.Ch02.vecNorm p * HCPolySupport.cubeAverage R (UnitCubeSkewW2Infinity.matrixNormField h)

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.sqrt_vecNormSq_cubeAverageVec_termAField_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) (p : HCPolySupport.Vec d) : √(HCPolySupport.vecNormSq (HCPolySupport.cubeAverageVec R (DhBound.Discharge.termAField h p))) ≤ √↑d * (↑d * HCPolySupport.Book.Ch02.vecNorm p * √(valueBudget h R))

The oscillation half

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.memLp_gradTermARep_top_cube {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) (p : HCPolySupport.Vec d) : MeasureTheory.MemLp (gradTermARep h p) ⊤ (HCPolySupport.normalizedCubeMeasure R)

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.cubeBesovPositiveVectorPartialSeminormTwo_termAField_damped_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) (p : HCPolySupport.Vec d) (N : ℕ) : HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo R (3 / 8) N (DhBound.Discharge.termAField h p) ≤ DhBound.Besov.besovPerturbConst (3 / 8) * (HCPolySupport.cubeScaleFactor R * (↑d ^ 2 * h.gradientW1Infinity * HCPolySupport.Book.Ch02.vecNorm p))

The scale-damped oscillation half. The cubeScaleFactor is kept: it is the mesoscopic damping factor of the unconditional estimate.

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.cubeBesovPositiveVectorSeminormTwo_termAField_damped_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) (p : HCPolySupport.Vec d) : HCPolySupport.cubeBesovPositiveVectorSeminormTwo R (3 / 8) (DhBound.Discharge.termAField h p) ≤ DhBound.Besov.besovPerturbConst (3 / 8) * (HCPolySupport.cubeScaleFactor R * (↑d ^ 2 * h.gradientW1Infinity * HCPolySupport.Book.Ch02.vecNorm p))

The refined budget

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

The constant of the scale-damped Term A budget.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.termARefinedConst d = √↑d * ↑d + Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Besov.besovPerturbConst (3 / 8) * ↑d ^ 2

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.termARefinedConst_nonneg (d : ℕ) : 0 ≤ termARefinedConst d

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.scaleNormalizedPositiveBesovVectorNormTwo_termAField_refined_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) (p : HCPolySupport.Vec d) : HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorNormTwo R (3 / 8) (DhBound.Discharge.termAField h p) ≤ termARefinedConst d * HCPolySupport.Book.Ch02.vecNorm p * (√(valueBudget h R) + HCPolySupport.cubeScaleFactor R * h.gradientW1Infinity)

The scale-damped Term A positive Besov budget on a sub-cube.