BesovPairing

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

Besov pairing against a response gradient

Source: ABK26 (e.sensitivity.basic.split1 and e.split.besov.stuff.begin). Both terms of the D_h split are estimated by the same mechanism: |⨍_Q F · H| ≤ C ‖H‖_{B^{3/8}_{2,2}(Q)} ‖F‖_{B^{-3/8}_{2,2}(Q)},

applied with F = ∇v and then combined with the coarse Poincaré inequality ‖∇v‖_{B^{-3/8}_{2,2}} ≤ C λ_{3/8,2}^{-1/2} J^{1/2}.

This module packages that combination once and for all: given any second factor H with a positive-Besov budget B, the averaged pairing against the gradient of a response maximizer is bounded by C(d) · B · λ^{-1/2} · J^{1/2}.

Term A of the source proof is this lemma with H x = hᵀ(x) p; Term BC is this lemma with H x = (w + w* + ℓ_p)(x) (∇·h)(x).

Everything is stated at an arbitrary triadic cube Q and an arbitrary CoarseGraining coefficient family F, as required by the descendant-cube consumers.

Average bridges

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Assembly.average_cubeDomain_eq_cubeAverage {d : ℕ} (Q : HCPolySupport.TriadicCube d) (f : HCPolySupport.Vec d → ℝ) : HCPolySupport.Book.Ch02.average (HCPolySupport.Book.Ch02.cubeDomain Q) f = HCPolySupport.cubeAverage Q f

The Chapter 2 average over cubeDomain Q is the Chapter 3 cube average.

Transporting the coarse Poincaré bound to the duality hypothesis

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Assembly.memVectorL2_cubeSet_grad {d : ℕ} [NeZero d] {Q : HCPolySupport.TriadicCube d} (u : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain Q).carrier) : HCPolySupport.MemVectorL2 (HCPolySupport.cubeSet Q) u.grad

The gradient of a public H¹ function on cubeDomain Q is square integrable on the closed cube.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Assembly.cubeBesovNegativeVectorPartialSeminormTwo_le_scaleNormalizedNegativeBesovVectorNorm {d : ℕ} (Q : HCPolySupport.TriadicCube d) {s : ℝ} (hs : 0 < s) (G : HCPolySupport.Vec d → HCPolySupport.Vec d) (hG : HCPolySupport.MemVectorL2 (HCPolySupport.cubeSet Q) G) (N : ℕ) : HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N G ≤ HCPolySupport.Book.Ch03.scaleNormalizedNegativeBesovVectorNorm Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) G

Every partial negative Besov seminorm of a field is dominated by the frozen concrete negative Besov norm at exponent q = 2.

The pairing estimate

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Assembly.abs_cubeAverage_vecDot_grad_le_of_positiveBesov_bound {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (F : HCPolySupport.Book.Ch03.CoeffFamily d) {p q : HCPolySupport.Vec d} {v : HCPolySupport.Book.Ch03.CubeSolution Q F} (hv : HCPolySupport.Book.Ch02.IsResponseMaximizer (HCPolySupport.Book.Ch02.cubeDomain Q) (F.coeffOn Q) p q v) (H : HCPolySupport.Vec d → HCPolySupport.Vec d) {B : ℝ} (hH : HCPolySupport.Book.Ch03.ForceBesovRegularity Q (3 / 8) H) (hHnorm : HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorNormTwo Q (3 / 8) H ≤ B) : |HCPolySupport.cubeAverage Q fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (v.toH1.grad x) (H x)| ≤ (1 + ↑d * Real.rpow 3 (↑d + 1)) * (2 * HCPolySupport.Book.Ch03.poincareDiscountFactor (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2)) * B * (√(HCPolySupport.Book.Ch02.lambdaSq Q (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) F)⁻¹ * √(HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain Q) (F.coeffOn Q) p q))

Besov pairing against a response gradient.

For every field H with positive Besov budget B at smoothness 3/8, |⨍_Q ∇v · H| ≤ (1 + d 3^{d+1}) · (2 c_{3/8,2}^{-1/2}) · B · λ_{3/8,2}^{-1/2} · J^{1/2},

where v is any response maximizer for (a, p, q) on Q.

This is the common engine of e.sensitivity.basic.split1 (Term A) and e.split.besov.stuff.begin (Term BC). The positive Besov budget B is the only input not proved here.