Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.GradientSplit

GradientSplit #

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

The negative Besov budget of the zero-trace witness gradient #

Source: ABK26 (e.split.besov.stuff.begin). The Term BC multiplicand of the D_h split is the zero-trace witness u with

∇u = ∇w + ∇w^* + ℓ_p' = ½ (∇v(·,□₀,p,q;a) + ∇v(·,□₀,p,-q;aᵗ)) + p ,

and every Besov estimate for u is fed by the concrete negative Besov seminorm of ∇u at the gauge exponent 3/8. This module produces that budget, in the frozen shape

[∇u]_{B^{-3/8}_{2,2}(□₀)} ≤ C λ_{3/8,2}^{-1/2} ( J^{1/2} + |p·q|^{1/2} ) .

The three summands are handled by

the coarse Poincaré inequality (Assembly.GaugeBridge) for ∇v;
the same inequality for ∇v^* at the transposed coefficient, combined with the transpose invariance of the gauge (Discharge.TransposeGauge) and the adjoint response identity (Discharge.AdjointResponse);
the constant-field bound (Discharge.ConstantBesov) together with the ellipticity chain (Discharge.EllipticityOrdered) for the affine piece p.

The elementary negative-Besov calculus (a.e. congruence and scalar homogeneity at finite depth) is not available upstream and is proved here.

Almost-everywhere congruence for the negative `q = 2` quantities #

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeBesovNegativeVectorDepthAverage_congr_ae {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j : ℕ) {f g : HCPolySupport.Vec d → HCPolySupport.Vec d} (h : f =ᵐ[HCPolySupport.normalizedCubeMeasure Q] g) :

HCPolySupport.cubeBesovNegativeVectorDepthAverage Q f j = HCPolySupport.cubeBesovNegativeVectorDepthAverage Q g j

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeBesovNegativeVectorDepthSeminorm_congr_ae {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (j : ℕ) {f g : HCPolySupport.Vec d → HCPolySupport.Vec d} (h : f =ᵐ[HCPolySupport.normalizedCubeMeasure Q] g) :

HCPolySupport.cubeBesovNegativeVectorDepthSeminorm Q s f j = HCPolySupport.cubeBesovNegativeVectorDepthSeminorm Q s g j

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeBesovNegativeVectorPartialSeminormTwo_congr_ae {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (N : ℕ) {f g : HCPolySupport.Vec d → HCPolySupport.Vec d} (h : f =ᵐ[HCPolySupport.normalizedCubeMeasure Q] g) :

HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N f = HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N g

Scalar homogeneity of the negative `q = 2` quantities #

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeAverageVec_const_smul {d : ℕ} (Q : HCPolySupport.TriadicCube d) (c : ℝ) (f : HCPolySupport.Vec d → HCPolySupport.Vec d) :

(HCPolySupport.cubeAverageVec Q fun (x : HCPolySupport.Vec d) => c • f x) = c • HCPolySupport.cubeAverageVec Q f

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.descendantsAverage_const_mul {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j : ℕ) (c : ℝ) (F : HCPolySupport.TriadicCube d → ℝ) :

(HCPolySupport.descendantsAverage Q j fun (R : HCPolySupport.TriadicCube d) => c * F R) = c * HCPolySupport.descendantsAverage Q j F

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeBesovNegativeVectorDepthAverage_const_smul {d : ℕ} (Q : HCPolySupport.TriadicCube d) (c : ℝ) (f : HCPolySupport.Vec d → HCPolySupport.Vec d) (j : ℕ) :

HCPolySupport.cubeBesovNegativeVectorDepthAverage Q (fun (x : HCPolySupport.Vec d) => c • f x) j = c ^ 2 * HCPolySupport.cubeBesovNegativeVectorDepthAverage Q f j

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeBesovNegativeVectorDepthSeminorm_const_smul {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s c : ℝ) (f : HCPolySupport.Vec d → HCPolySupport.Vec d) (j : ℕ) :

HCPolySupport.cubeBesovNegativeVectorDepthSeminorm Q s (fun (x : HCPolySupport.Vec d) => c • f x) j = |c| * HCPolySupport.cubeBesovNegativeVectorDepthSeminorm Q s f j

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeBesovNegativeVectorPartialSeminormTwo_const_smul {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (N : ℕ) (c : ℝ) (f : HCPolySupport.Vec d → HCPolySupport.Vec d) :

(HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : HCPolySupport.Vec d) => c • f x) = |c| * HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N f

`L²` bookkeeping on triadic cubes #

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.isFiniteMeasure_volumeMeasureOn_cubeSet {d : ℕ} (Q : HCPolySupport.TriadicCube d) :

MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn (HCPolySupport.cubeSet Q))

Shared finite-depth witness estimates #

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeBesovNegativeVectorPartialSeminormTwo_smul_add_le {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s c : ℝ) (f g : HCPolySupport.Vec d → HCPolySupport.Vec d) (hfL2 : HCPolySupport.MemVectorL2 (HCPolySupport.cubeSet Q) f) (hgL2 : HCPolySupport.MemVectorL2 (HCPolySupport.cubeSet Q) g) (hfBdd : BddAbove (Set.range fun (N : ℕ) => HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N f)) (hgBdd : BddAbove (Set.range fun (N : ℕ) => HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N g)) {A B : ℝ} (hf : HCPolySupport.cubeBesovNegativeVectorSeminormTwo Q s f ≤ A) (hg : HCPolySupport.cubeBesovNegativeVectorSeminormTwo Q s g ≤ B) (N : ℕ) :

(HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : HCPolySupport.Vec d) => c • (f x + g x)) ≤ |c| * √2 * (A + B)

A scalar multiple of a sum has a uniform finite-depth budget whenever both summands have bounded partial seminorms and the stated full-seminorm budgets.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeBesovNegativeVectorSeminormTwo_add_const_le {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (f h : HCPolySupport.Vec d → HCPolySupport.Vec d) (p : HCPolySupport.Vec d) (hfL2 : HCPolySupport.MemVectorL2 (HCPolySupport.cubeSet Q) f) (hae : h =ᵐ[HCPolySupport.normalizedCubeMeasure Q] fun (x : HCPolySupport.Vec d) => f x + p) {A B : ℝ} (hf : ∀ (N : ℕ), HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N f ≤ A) (hp : ∀ (N : ℕ), (HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : HCPolySupport.Vec d) => p) ≤ B) :

HCPolySupport.cubeBesovNegativeVectorSeminormTwo Q s h ≤ √2 * (A + B)

Adding a constant field combines two uniform partial-seminorm budgets. The target may be any representative equal to the sum almost everywhere.

The two maximizer-gradient budgets #

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeBesovNegativeVectorSeminormTwo_maximizerGrad_le {d : ℕ} [NeZero d] (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) {p q : HCPolySupport.Vec d} {v : HCPolySupport.Book.Ch02.Solution (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a} (hv : HCPolySupport.Book.Ch02.IsResponseMaximizer (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a p q v) :

(HCPolySupport.cubeBesovNegativeVectorSeminormTwo (HCPolySupport.originCube d 0) (3 / 8) fun (x : HCPolySupport.Vec d) => v.toH1.grad x) ≤ HCPolySupport.Book.Ch03.poincareDiscountFactor (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) * √(Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹ * (2 * √(HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a p q))

The negative Besov budget of a response-maximizer gradient at the frozen unit cube, in the concrete q = 2 spelling.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.bddAbove_cubeBesovNegativeVectorPartialSeminormTwo_h1Grad {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (w : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain Q).carrier) :

BddAbove (Set.range fun (N : ℕ) => HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q (3 / 8) N fun (x : HCPolySupport.Vec d) => w.grad x)

The negative Besov partial seminorms of any H¹ gradient on a cube are bounded above.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeBesovNegativeVectorSeminormTwo_adjointGrad_le {d : ℕ} [NeZero d] (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) {p q : HCPolySupport.Vec d} {vAdj : HCPolySupport.Book.Ch02.Solution (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a.transpose} (hvAdj : HCPolySupport.Book.Ch02.IsResponseMaximizer (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a.transpose p (-q) vAdj) :

(HCPolySupport.cubeBesovNegativeVectorSeminormTwo (HCPolySupport.originCube d 0) (3 / 8) fun (x : HCPolySupport.Vec d) => vAdj.toH1.grad x) ≤ HCPolySupport.Book.Ch03.poincareDiscountFactor (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) * √(Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹ * (2 * √2 * (√(HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a p q) + √|HCPolySupport.vecDot p q|))

The adjoint budget: the transposed gauge equals the frozen one, and the transposed response is shifted by 2 p·q.

The witness-gradient budget #

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.gradSplitConst :

The explicit constant of the witness-gradient negative Besov budget.

Equations

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

Instances For

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.gradSplitConst_nonneg :

0 ≤ gradSplitConst

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeBesovNegativeVectorSeminormTwo_witnessGrad_le {d : ℕ} [NeZero d] (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (p q : HCPolySupport.Vec d) {vAdj : HCPolySupport.Book.Ch02.Solution (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a.transpose} {v : HCPolySupport.Book.Ch02.Solution (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a} (hvAdj : HCPolySupport.Book.Ch02.IsResponseMaximizer (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a.transpose p (-q) vAdj) (hv : HCPolySupport.Book.Ch02.IsResponseMaximizer (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a p q v) (u : HCPolySupport.H10Function (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier) (hu : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier, u.grad x = 2⁻¹ • (vAdj.toH1.grad x + v.toH1.grad x) + p) :

(HCPolySupport.cubeBesovNegativeVectorSeminormTwo (HCPolySupport.originCube d 0) (3 / 8) fun (x : HCPolySupport.Vec d) => u.grad x) ≤ gradSplitConst * (√(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) + √|HCPolySupport.vecDot p q|))

The negative Besov budget of the zero-trace witness gradient.