LargeScaleSplit

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

The large-scale split of the Section 3.5 negative-norm lemma

This module establishes the deterministic estimates behind the large-scale part of the multiscale sum that occurs in the proof of l.Besov.norms. Fix a cube Q = \cu_m and a scale n with L_0 \le n \le m. The manuscript compares the descendant averages (\nabla v)_{z+\cu_n} with the parent comparison vector \s_*^{-1}(\cu_m)(q+\k(\cu_m)p) - p, and splits that deviation into

• the local deviation from the comparison vector of the descendant itself, which is coarseScaleSeparationDeviationSq of PerScaleDefect.lean; and
• the coarse-matrix variation \s_*^{-1}(\cu_m)(q+\k(\cu_m)p) - \s_*^{-1}(z+\cu_n)(q+\k(z+\cu_n)p).

The two summed right-hand sides produced here have the shape of the first two right-hand terms of e.Besov.norms.gradient. Nothing about the left-hand side of that display, and nothing about the status of the lemma, is asserted here.

Formalization readings

1. The manuscript constant C. ABK26 prints an unspecified C in front of both legs of the split. The explicit value obtained from the pointwise Euclidean inequality |x-y|^2 \le 2(|x|^2+|y|^2) is \sqrt 2, and that literal value is carried here; every statement below is therefore an instance of the printed display with C given a value.
2. The index set. The manuscript sums over z \in 3^n\Zd \cap \cu_m, which is the set of triadic descendants of \cu_m at depth m-n, and \avsum is descendantsAverage. The outer sum over n from L_0 to m is Finset.Icc L₀ m in \Z.
3. The coarse-matrix variation. ABK26 prints \s_*^{-1}(\cu_m)(q+\k(\cu_m)p) - \s_*^{-1}(z+\cu_n)(q+\k(z+\cu_n)p), without the -p that both comparison vectors carry. Since the -p cancels in the difference, coarseMatrixVariationSq is the difference of the two coarseScaleSeparation vectors, which is literally the printed vector.

The two squared deviations of the split

noncomputable def Algsuperdiff.Section3.Provider.Besov.parentCoarseScaleSeparationDeviationSq {d : ℕ} (a : HCPolySupport.RegCoeffField d) (ha : HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField a) (Q : HCPolySupport.TriadicCube d) (p q : HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) : ℝ

The comparison vector is the one attached to the parent cube Q, and is constant in R.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Besov.coarseMatrixVariationSq {d : ℕ} (a : HCPolySupport.RegCoeffField d) (ha : HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField a) (Q : HCPolySupport.TriadicCube d) (p q : HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) : ℝ

The manuscript quantity `| \s_^{-1}(\cu_m)(q + \k(\cu_m)p) - \s_^{-1}(R)(q

• \k(R)p) |^2, written as the squared length of the difference of the two Carriers.leancomparison vectors. The-p` carried by each of them cancels in the difference, so this is literally the printed vector.

Equations

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

theorem Algsuperdiff.Section3.Provider.Besov.coarseMatrixVariationSq_nonneg {d : ℕ} (a : HCPolySupport.RegCoeffField d) (ha : HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField a) (Q : HCPolySupport.TriadicCube d) (p q : HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) : 0 ≤ coarseMatrixVariationSq a ha Q p q R

The per-scale two-term split

theorem Algsuperdiff.Section3.Provider.Besov.sqrt_descendantsAverage_parentCoarseScaleSeparationDeviationSq_le {d : ℕ} (a : HCPolySupport.RegCoeffField d) (ha : HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField a) (Q : HCPolySupport.TriadicCube d) (j : ℕ) (p q : HCPolySupport.Vec d) : √(HCPolySupport.descendantsAverage Q j (parentCoarseScaleSeparationDeviationSq a ha Q p q)) ≤ √2 * √(HCPolySupport.descendantsAverage Q j (coarseScaleSeparationDeviationSq a ha Q p q)) + √2 * √(HCPolySupport.descendantsAverage Q j (coarseMatrixVariationSq a ha Q p q))

The per-scale split. At a fixed depth the root of the descendant average of the deviation from the parent comparison vector is at most \sqrt 2 times the root of the descendant average of the deviation from the local comparison vector, plus \sqrt 2 times the root of the descendant average of the coarse-matrix variation.

The literal \sqrt 2 is the explicit value of the manuscript constant C printed; it comes from the pointwise Euclidean inequality |x-y|^2 \le 2(|x|^2+|y|^2).

The weighted per-scale display

theorem Algsuperdiff.Section3.Provider.Besov.rpow_neg_mul_rpow_mul (s x : ℝ) : 3 ^ (-x) * 3 ^ (s * x) = 3 ^ (-(1 - s) * x)

Weight arithmetic: the multiscale weight 3^{-(m-n)} composed with the ellipticity factor 3^{s(m-n)} is the manuscript discount 3^{-(1-s)(m-n)}.

theorem Algsuperdiff.Section3.Provider.Besov.weighted_sqrt_descendantsAverage_parentCoarseScaleSeparationDeviationSq_le_atScale {d : ℕ} [NeZero d] (a : HCPolySupport.RegCoeffField d) (ha : HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField a) {m n : ℤ} (hnm : n ≤ m) {s : ℝ} (hs : 0 < s) {r : HCPolySupport.Book.Ch02.MultiscaleExponent} (hr : r.IsAdmissible) (p q : HCPolySupport.Vec d) : 3 ^ (-↑(m - n)) * √(HCPolySupport.descendantsAverage (HCPolySupport.originCube d m) (m - n).toNat (parentCoarseScaleSeparationDeviationSq a ha (HCPolySupport.originCube d m) p q)) ≤ 2 * √(HCPolySupport.Book.Ch04.lambdaSqCoeffField (HCPolySupport.originCube d m) s r a)⁻¹ * (3 ^ (-(1 - s) * ↑(m - n)) * √(HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.responseDefectAverageAtScale m n p q a)) + √2 * (3 ^ (-↑(m - n)) * √(HCPolySupport.descendantsAverage (HCPolySupport.originCube d m) (m - n).toNat (coarseMatrixVariationSq a ha (HCPolySupport.originCube d m) p q)))

The constant 2 of the first summand is \sqrt 2 from the split times \sqrt 2 from the defect estimate.

The summed large-scale display

theorem Algsuperdiff.Section3.Provider.Besov.sum_Icc_weighted_sqrt_descendantsAverage_parentCoarseScaleSeparationDeviationSq_le {d : ℕ} [NeZero d] (a : HCPolySupport.RegCoeffField d) (ha : HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField a) (m L₀ : ℤ) {s : ℝ} (hs : 0 < s) {r : HCPolySupport.Book.Ch02.MultiscaleExponent} (hr : r.IsAdmissible) (p q : HCPolySupport.Vec d) : ∑ n ∈ Finset.Icc L₀ m, 3 ^ (-↑(m - n)) * √(HCPolySupport.descendantsAverage (HCPolySupport.originCube d m) (m - n).toNat (parentCoarseScaleSeparationDeviationSq a ha (HCPolySupport.originCube d m) p q)) ≤ 2 * √(HCPolySupport.Book.Ch04.lambdaSqCoeffField (HCPolySupport.originCube d m) s r a)⁻¹ * ∑ n ∈ Finset.Icc L₀ m, 3 ^ (-(1 - s) * ↑(m - n)) * √(HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.responseDefectAverageAtScale m n p q a) + √2 * ∑ n ∈ Finset.Icc L₀ m, 3 ^ (-↑(m - n)) * √(HCPolySupport.descendantsAverage (HCPolySupport.originCube d m) (m - n).toNat (coarseMatrixVariationSq a ha (HCPolySupport.originCube d m) p q))

The summed large-scale display. Summing the weighted per-scale display over n \in [L_0,m] \cap \Z produces exactly the first two right-hand terms of e.Besov.norms.gradient, with the manuscript constant C given the explicit values 2 and \sqrt 2.