BesovNorms #

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

The four-term negative-norm display of Section 3.5 #

This module assembles the display e.Besov.norms.gradient of ABK26 for the canonical maximizer on \cu_m from the four estimates already available in this directory: the multiscale Poincare bridge, the per-scale defect estimate, the summed large-scale split and the small-scale tail. Nothing about the status of the lemma l.Besov.norms is asserted here.

The left-hand side is Carriers.scaledNegHMinusOne of the maximizer gradient defect, that is 3^{-m} \| \nabla v(\cdot,\cu_m,p,q;\a) - (\s_*^{-1}(\cu_m)(q+\k(\cu_m)p)-p) \|_{\Hminusul(\cu_m)}, and the right-hand side is the printed four-term sum with one dimension-only constant besovNormsConstant d.

Route #

sqrt_sum_sq_sum_le_sum_mul_sqrt_sum_sq is the Minkowski conversion (\sum_i (\sum_j w_j a_{ij})^2)^{1/2} \le \sum_j w_j (\sum_i a_{ij}^2)^{1/2} for nonnegative weights, proved by induction on the j-range from the two-term \ell^2 triangle inequality, itself proved from the Cauchy--Schwarz inequality for finite sums. This is the conversion that MultiscalePoincareBridge.lean states but does not formalize: its conclusion aggregates the coordinates in \ell^2, while the printed display e.msp.plus.split.begin is the \ell^1-of-\ell^2 form.
At (s,p,q) = (1,2,1) the depth-N entry of the negative circ norm is the partial sum \sum_{j \le N+1} 3^{m-j} (\avsum_R |(u)_R|^2)^{1/2} (cubeBesovCircNormEntry_one_two_one, with the weight identified by MultiscalePoincareBridge.cubeBesovCircDepthWeight_one), so after the scale factor 3^{-m} the summand is the printed 3^{-(m-n)} term with n = m-j.
sum_cubeBesovCircDepthAverage_maximizerGradientDefect identifies the coordinate sum of the depth-j circ averages of the gradient defect with descendantsAverage Q j (parentCoarseScaleSeparationDeviationSq ...), the carrier of LargeScaleSplit.lean. Averaging is linear in the coordinate, so the Euclidean length of the average vector is the coordinate sum of the squared scalar averages; the upstream Chapter 5 identity cubeAverageVec_canonicalMaximizerGradientDefectOnDependentFamily_eq_ch04 supplies the Chapter 4 representative on each descendant.
sum_range_multiscaleTerm_le_fourTerm splits the depth range at the base scale: depths j \le m-L_0 are the scales n \in [L_0,m] and are bounded by LargeScaleSplit.sum_Icc_weighted_..., while depths j > m-L_0 are the scales n < L_0 and are bounded by SmallScaleTail.sum_range_smallScale_multiscaleTerm_le. The two upstream statements are on the identical summand, so the split is exact; the bound is uniform in the depth cutoff N.
mul_sqrt_sum_sq_ciSup_le passes from the partial circ norms to the circ norm itself. The circ norm is the supremum of the partial sums, which are monotone and, by the previous step, uniformly bounded; the limit therefore obeys the same bound. This is where the manuscript's bi-infinite sum \sum_{n=-\infty}^m is realized.
scaledNegHMinusOne_maximizerGradientDefect_le_besovNormsSum composes the above with the bridge of MultiscalePoincareBridge.lean and converts the ℝ≥0∞-valued left-hand side by ENNReal.ofReal.

Correspondence with the printed display #

C \lambda_{s,r}^{-1/2}(\cu_m;\a) \sum_{n=L_0}^m 3^{-(1-s)(m-n)} (\avsum_z J(z+\cu_n,p,q;\a) - J(\cu_m,p,q;\a))^{1/2}, realized with WeakNormsMaximizer.responseDefectAverageAtScale m n p q a for the bracket;
C \sum_{n=L_0}^m 3^{-(m-n)} (\avsum_z | \s_*^{-1}(\cu_m)(q+\k(\cu_m)p) - \s_*^{-1}(z+\cu_n)(q+\k(z+\cu_n)p) |^2)^{1/2}, realized with LargeScaleSplit.coarseMatrixVariationSq;
C \lambda_{s,r}^{-1/2}(\cu_m;\a) 3^{-(1-s)(m-L_0)} \| \s^{1/2} \nabla v \|_{\underline L^2(\cu_m)}, realized with SmallScaleTail.maximizerEnergyL2Norm;
C 3^{-(m-L_0)} | \s_*^{-1}(\cu_m)(q+\k(\cu_m)p) - p |, realized as the square root of vecNormSq (coarseScaleSeparation a ha (originCube d m) p q).

The manuscript constant C(d) is given the explicit value besovNormsConstant d = 2\sqrt 2 \cdot multiscalePoincareConstant d, which dominates the four constants produced by the chain: 2 on the defect leg (\sqrt 2 from the split times \sqrt 2 from the defect estimate), \sqrt 2 on the coarse-matrix leg, and 2\sqrt 2 on both tails (\sqrt 2 from the triangle step times 2 from the geometric tail \rho/(1-\rho) \le 2). All four are multiplied by the multiscale Poincare constant of the bridge.

Formalization readings #

The readings of Carriers.lean (the dual pairing is volume normalized; a vector field's dual seminorm is the Euclidean \ell^2 aggregate of the scalar seminorms of its coordinates) and of PerScaleDefect.lean (the manuscript index set z \in 3^n\Zd \cap \cu_m is the set of triadic descendants at depth m-n, and \avsum is descendantsAverage) are inherited unchanged. Two further readings are specific to this module.

The multiscale sum is the negative circ norm at (s,p,q) = (1,2,1). The manuscript's right-hand side is \sum_{n=-\infty}^m 3^{-(m-n)} (\avsum_z |(f)_{z+\cu_n}|^2)^{1/2}. Here 3^{-m} \cdot cubeBesovCircNorm Q 1 2 1 f is that sum: item 2 of the route proves that each partial sum of the circ norm is the printed sum truncated at a finite depth, with the same weight and the same average, and the circ norm is the supremum of those partial sums. Unlike in MultiscalePoincareBridge.lean, where only the weight half was formalized, the depth average and the depth sum are identified here in Lean, for the maximizer gradient defect.
The bi-infinite sum is a supremum of partial sums. The manuscript sums over all n \le m. The upstream circ norm is sSup of the set of partial sums, which for a nonnegative summand is the value of the series, finite or not. The passage from the uniform bound on partial sums to the bound on the supremum is mul_sqrt_sum_sq_ciSup_le and uses monotone convergence of a bounded monotone real sequence; no summability is assumed, it is a consequence of the four-term bound.

The per-depth identification #

source

theorem Algsuperdiff.Section3.Provider.Besov.sum_cubeBesovCircDepthAverage_maximizerGradientDefect {d : ℕ} [NeZero d] (a : HCPolySupport.RegCoeffField d) (ha : HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField a) (Q : HCPolySupport.TriadicCube d) (p q : HCPolySupport.Vec d) (j : ℕ) :

∑ i : Fin d, HCPolySupport.cubeBesovCircDepthAverage Q 2 (fun (x : HCPolySupport.Vec d) => maximizerGradientDefect a ha Q p q x i) j = HCPolySupport.descendantsAverage Q j (parentCoarseScaleSeparationDeviationSq a ha Q p q)

The per-depth identification. Summing the depth-j circ averages of the coordinates of the maximizer gradient defect over the coordinate index gives the descendant average of the squared deviation from the parent comparison vector. It is public because the l.J.bound.by.Besov assembly re-enters the chain at this depth, before the coordinate aggregation.

The depth-indexed multiscale term #

Splitting the depth range at the base scale #

Reindexing the two ranges #

The four-term bound at every depth cutoff #