InputA

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

Term A: the positive Besov budget of x ↦ hᵀ(x) p

Source: ABK26, the second inequality of e.sensitivity.basic.split1:

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

This module discharges the two Term-A premises of Provider.DhBound.Assembly.Skeleton:

• Ch03.ForceBesovRegularity (originCube d 0) (3/8) (fun x => hᵀ(x) p);
• Ch03.scaleNormalizedPositiveBesovVectorNormTwo (originCube d 0) (3/8) … ≤ termABesovConst d * vecNorm p * h.w1Infinity.

The route is: each entry of h has a d · w1Infinity-Lipschitz representative (Provider.DhBound.Lipschitz.UnitCube), so the vector field hᵀ p has a d² · w1Infinity · |p|-Lipschitz representative; the positive Besov seminorm of a Lipschitz vector field is controlled by Discharge.VectorPerturbation, and the mean term by the frozen L^∞ half of w1Infinity. All Besov quantities are a.e. insensitive (Discharge.BesovCongr), so the bound transfers back to the actual field.

The Lipschitz matrix representative

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.valueRep {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (x : HCPolySupport.Vec d) : HCPolySupport.Mat d

The entrywise Lipschitz representative of the frozen matrix field.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.valueRep h x i j = ⋯.choose x

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.valueRep_lipschitz {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (i j : Fin d) (x y : HCPolySupport.Vec d) : |valueRep h x i j - valueRep h y i j| ≤ ↑d * h.w1Infinity * ‖x - y‖

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.valueRep_ae_eq {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (i j : Fin d) : (fun (x : HCPolySupport.Vec d) => valueRep h x i j) =ᵐ[HCPolySupport.normalizedCubeMeasure (HCPolySupport.originCube d 0)] fun (x : HCPolySupport.Vec d) => ↑↑h.toLInfSkewMatrixFieldOn x i j

The Term A field and its representative

def Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.termAField {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (p : HCPolySupport.Vec d) : HCPolySupport.Vec d → HCPolySupport.Vec d

The Term A field x ↦ hᵀ(x) p.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.termAField h p x = HCPolySupport.matVecMul (HCPolySupport.matTranspose (↑↑h.toLInfSkewMatrixFieldOn x)) p

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.termARep {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (p : HCPolySupport.Vec d) : HCPolySupport.Vec d → HCPolySupport.Vec d

The Lipschitz representative of the Term A field.

Equations

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.termAField_apply {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (p x : HCPolySupport.Vec d) (i : Fin d) : termAField h p x i = ∑ j : Fin d, ↑↑h.toLInfSkewMatrixFieldOn x j i * p j

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.termARep_apply {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (p x : HCPolySupport.Vec d) (i : Fin d) : termARep h p x i = ∑ j : Fin d, valueRep h x j i * p j

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.termARep_ae_eq {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (p : HCPolySupport.Vec d) : termARep h p =ᵐ[HCPolySupport.normalizedCubeMeasure (HCPolySupport.originCube d 0)] termAField h p

The Lipschitz constant of the Term A representative

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.abs_apply_le_vecNorm {d : ℕ} (p : HCPolySupport.Vec d) (j : Fin d) : |p j| ≤ HCPolySupport.Book.Ch02.vecNorm p

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.termARep_lipschitz {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (p x y : HCPolySupport.Vec d) : ‖termARep h p x - termARep h p y‖ ≤ ↑d ^ 2 * h.w1Infinity * HCPolySupport.Book.Ch02.vecNorm p * ‖x - y‖

L^∞ and L² membership

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.memLp_value_entry {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (i j : Fin d) (q : ENNReal) : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => ↑↑h.toLInfSkewMatrixFieldOn x i j) q (HCPolySupport.normalizedCubeMeasure (HCPolySupport.originCube d 0))

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.memLp_termAField_component {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (p : HCPolySupport.Vec d) (i : Fin d) (q : ENNReal) : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => termAField h p x i) q (HCPolySupport.normalizedCubeMeasure (HCPolySupport.originCube d 0))

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.memLp_termAField {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (p : HCPolySupport.Vec d) (q : ENNReal) : MeasureTheory.MemLp (termAField h p) q (HCPolySupport.normalizedCubeMeasure (HCPolySupport.originCube d 0))

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.memLp_termARep_top {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (p : HCPolySupport.Vec d) : MeasureTheory.MemLp (termARep h p) ⊤ (HCPolySupport.normalizedCubeMeasure (HCPolySupport.originCube d 0))

The a.e. componentwise bound

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.ae_abs_termAField_le {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (p : HCPolySupport.Vec d) (i : Fin d) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.normalizedCubeMeasure (HCPolySupport.originCube d 0), |termAField h p x i| ≤ ↑d * h.w1Infinity * HCPolySupport.Book.Ch02.vecNorm p

The Term A Besov budget

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

The explicit Term A Besov constant.

Equations

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.termABesovConst_nonneg (d : ℕ) : 0 ≤ termABesovConst d

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeBesovPositiveVectorPartialSeminormTwo_termAField_le {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (p : HCPolySupport.Vec d) (N : ℕ) : HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo (HCPolySupport.originCube d 0) (3 / 8) N (termAField h p) ≤ Besov.besovPerturbConst (3 / 8) * (↑d ^ 2 * h.w1Infinity * HCPolySupport.Book.Ch02.vecNorm p)

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.forceBesovRegularity_termAField {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (p : HCPolySupport.Vec d) : HCPolySupport.Book.Ch03.ForceBesovRegularity (HCPolySupport.originCube d 0) (3 / 8) fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul (HCPolySupport.matTranspose (↑↑h.toLInfSkewMatrixFieldOn x)) p

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.scaleNormalizedPositiveBesovVectorNormTwo_termAField_le {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (p : HCPolySupport.Vec d) : (HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorNormTwo (HCPolySupport.originCube d 0) (3 / 8) fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul (HCPolySupport.matTranspose (↑↑h.toLInfSkewMatrixFieldOn x)) p) ≤ termABesovConst d * HCPolySupport.Book.Ch02.vecNorm p * h.w1Infinity