GridWeights

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

Grid weights, the triadic grid maximum, and the e.maxy.bound lift

The tex objects

Lambda_{s,q}(cu_m; a) is (c_{sq} sum_{k <= m} 3^{-sq(m-k)} max_{z in 3^k Z^d cap cu_m} |b(z+cu_k;a)|^{q/2})^{2/q}. Two objects occur:

• the grid maximum max_{z in 3^k Z^d cap cu_m} |b(z+cu_k; a)|, which is exactly a supremum of absolute values over a finite index set --- here gridSupAbs, instantiated at Homogenization.descendantsAtScale, whose members are exactly the triadic subcubes z + cu_k of cu_m;
• the grid weight 3^{-rho(m-k)} carrying the scale decay. Following the proof's own indexing (the binder n <= m-1 is printed, and in p.bfA.multiscalebound itself, so m - n = k+1 for k : ℕ), gridWeight rho k = (3^{-rho})^{k+1}. S: this family covers gaps >= 1 only; the source sum's gap-0 term (CoarseGraining's LambdaSqFinite at n = 0) is outside it, and the identification theorem below is likewise stated at scale m-1-k only.

The proof needs three quantitative facts about these:

1. the polynomial-times-geometric sum, because e.maxy.bound costs a factor (3 log N)^{1/sigma} at N = 3^{d(m-n)} cubes, i.e. a factor polynomial in m - n (gridNetConst_rpow_eq);
2. the pole order of that sum, which is what turns per-scale amplitudes into the printed (2s - gamma)^{-p} poles (polyGridWeight_tsum_le, one_sub_rpow_neg_inv_le);
3. the collar absorption gridWeight a k * 3^{g(k+1)} = gridWeight (a-g) k, which is how the per-scale factor 3^{gamma(m-n)} of e.bL.multiscale moves the pole from 2s to 2s - gamma.

Main results

• gridWeight, gridWeight_summable, gridWeight_tsum_le.
• polyGridWeight_summable, polyGridWeight_tsum_le --- the scale sum with the explicit constant p ! * ((1 - 3^{-rho})^{-1})^{p+1}.
• one_sub_rpow_neg_inv_le --- (1 - 3^{-rho})^{-1} <= 1 + rho^{-1}, the conversion of the geometric pole into the printed algebraic pole.
• gridSupAbs and its nonnegativity, measurability, and two-sided sup' A.
• gridSupAbs_isBigOWith --- e.maxy.bound for an arbitrary nonempty finite index set, using this repository's proved local implementation of l.maximums.Gamma.s.
• card_descendantsAtScale_originCube --- the grid has exactly 3^{d(k+1)} members, the cardinality the source's N refers to.
• gridSupAbs_descendants_isBigOWith --- the e.maxy.bound lift at the triadic grid: a common per-cube Gamma_sigma bound over the grid 3^{m-1-k} Z^d cap cu_m lifts to the grid maximum at the amplitude gridNetConst d sigma * (k+1)^{1/sigma} * A.

Divergences from the source, disclosed

• The source writes (3 log N)^{1/sigma}; the proved l.maximums.Gamma.s of this repository (Provider/Orlicz/Maximum.lean) writes (3 max 1 (log N))^{1/sigma}, an enlargement that removes the source proof's N >= 2 restriction. On the triadic grid N = 3^{d(k+1)} >= 3, so max 1 (log N) = log N and the two agree; this is proved here (gridNetConst_rpow_eq is applied to the bare log).
• The k-independent constant (3 d log 3)^{1/sigma} is made explicit as gridNetConst; the source leaves it inside a generic C.
• S: gridNetConst_rpow_eq emits ((k:ℝ)+1) ^ (sigma⁻¹ : ℝ) (Real.rpow) while polyGridWeight_tsum_le consumes ((k:ℝ)+1) ^ (p : ℕ) (Monoid.npow); no bridge lemma is proved here.
• (CoarseGraining carries a second, Frobenius-normed LambdaSqFinite in Deterministic/MultiscaleQuantities; the identification here fully qualifies Book.Ch02.*, so it is unambiguous despite the open Homogenization.)

References

• ABK26, l.maximums.Gamma.s (e.maxy.bound).
• ABK26, coarse-grained ellipticity constants.
• ABK26, p.cg.ellipticity.bounds proof from p.bfA.multiscalebound.

1. The grid weight

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.one_lt_log_three : 1 < Real.log 3

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.gridWeight (rho : ℝ) (k : ℕ) : ℝ

The grid weight 3^{-rho(m-n)} at m - n = k + 1.

The proof of p.cg.ellipticity.bounds sums over n <= m - 1, so the scale gap m - n runs over the positive integers; k is the shifted index.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.gridWeight rho k = (3 ^ (-rho)) ^ (k + 1)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.rpow_neg_lt_one {rho : ℝ} (hrho : 0 < rho) : 3 ^ (-rho) < 1

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.rpow_neg_nonneg (rho : ℝ) : 0 ≤ 3 ^ (-rho)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.rpow_neg_pos (rho : ℝ) : 0 < 3 ^ (-rho)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gridWeight_pos (rho : ℝ) (k : ℕ) : 0 < gridWeight rho k

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gridWeight_nonneg (rho : ℝ) (k : ℕ) : 0 ≤ gridWeight rho k

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.one_sub_rpow_neg_pos {rho : ℝ} (hrho : 0 < rho) : 0 < 1 - 3 ^ (-rho)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.one_sub_rpow_neg_inv_le {rho : ℝ} (hrho : 0 < rho) : (1 - 3 ^ (-rho))⁻¹ ≤ 1 + rho⁻¹

The geometric pole is bounded by the printed algebraic pole: (1 - 3^{-rho})^{-1} <= 1 + rho^{-1}.

This is the step that converts the summation constant into the source's (2s - gamma)^{-p} shape.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gridWeight_summable {rho : ℝ} (hrho : 0 < rho) : Summable (gridWeight rho)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gridWeight_tsum_le {rho : ℝ} (hrho : 0 < rho) : ∑' (k : ℕ), gridWeight rho k ≤ rho⁻¹

The deterministic lane's collapse: the full grid weight sums to at most rho^{-1}.

2. The polynomial-times-geometric scale sum

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.polyGridWeight_summable (p : ℕ) {rho : ℝ} (hrho : 0 < rho) : Summable fun (k : ℕ) => (↑k + 1) ^ p * gridWeight rho k

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.polyGridWeight_tsum_le (p : ℕ) {rho : ℝ} (hrho : 0 < rho) : ∑' (k : ℕ), (↑k + 1) ^ p * gridWeight rho k ≤ ↑p.factorial * (1 - 3 ^ (-rho))⁻¹ ^ (p + 1)

The scale summation. The polynomial cost of e.maxy.bound against the grid weight, with the explicit pole order p + 1.

3. The grid net constant of e.maxy.bound

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.gridNetConst (d : ℕ) (sigma : ℝ) : ℝ

The dimension-only constant of e.maxy.bound at a triadic grid: (3 d log 3)^{1/sigma}. The source hides it inside a generic C.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.gridNetConst d sigma = (3 * ↑d * Real.log 3) ^ sigma⁻¹

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gridNetConst_nonneg (d : ℕ) (sigma : ℝ) : 0 ≤ gridNetConst d sigma

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gridNetConst_rpow_eq (sigma : ℝ) (d k : ℕ) : (3 * Real.log (3 ^ (d * (k + 1)))) ^ sigma⁻¹ = gridNetConst d sigma * (↑k + 1) ^ sigma⁻¹

The e.maxy.bound factor at N = 3^{d(k+1)} cubes, split into the k-independent net constant and the polynomial (k+1)^{1/sigma}.

4. The triadic grid and its cardinality

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.card_descendantsAtScale_originCube (d : ℕ) (m : ℤ) (k : ℕ) : (HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)).card = 3 ^ (d * (k + 1))

The grid 3^{m-1-k} Z^d cap cu_m of the proof, represented as the finite set of triadic subcubes of cu_m at scale m - 1 - k.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.descendantsAtScale_originCube_nonempty (d : ℕ) (m : ℤ) (k : ℕ) : (HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)).Nonempty

5. gridSupAbs: the grid maximum

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.gridSupAbs {Omega : Type u_1} {ι : Type u_2} (sfin : Finset ι) (hs : sfin.Nonempty) (X : ι → Omega → ℝ) (omega : Omega) : ℝ

The grid maximum max_{z in 3^k Z^d cap cu_m} |X_z| of the coarse-grained ellipticity definition, for an arbitrary nonempty finite index set.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.gridSupAbs sfin hs X omega = sfin.sup' hs fun (y : ι) => |X y omega|

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gridSupAbs_nonneg {Omega : Type u_1} {ι : Type u_2} (sfin : Finset ι) (hs : sfin.Nonempty) (X : ι → Omega → ℝ) (omega : Omega) : 0 ≤ gridSupAbs sfin hs X omega

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.le_gridSupAbs {Omega : Type u_1} {ι : Type u_2} {sfin : Finset ι} (hs : sfin.Nonempty) {X : ι → Omega → ℝ} {y : ι} (hy : y ∈ sfin) (omega : Omega) : |X y omega| ≤ gridSupAbs sfin hs X omega

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gridSupAbs_le {Omega : Type u_1} {ι : Type u_2} {sfin : Finset ι} (hs : sfin.Nonempty) {X : ι → Omega → ℝ} {omega : Omega} {b : ℝ} (hb : ∀ y ∈ sfin, |X y omega| ≤ b) : gridSupAbs sfin hs X omega ≤ b

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.measurable_gridSupAbs {Omega : Type u_1} {ι : Type u_2} [MeasurableSpace Omega] (sfin : Finset ι) (hs : sfin.Nonempty) {X : ι → Omega → ℝ} (hm : ∀ (y : ι), Measurable (X y)) : Measurable (gridSupAbs sfin hs X)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gridSupAbs_isBigOWith {Omega : Type u_1} {ι : Type u_2} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] (sfin : Finset ι) (hs : sfin.Nonempty) {X : ι → Omega → ℝ} {A sigma : ℝ} (hsigma : 0 < sigma) (hA : 0 ≤ A) (hX : ∀ y ∈ sfin, HCPolySupport.IndependentSums.IsBigO mu (HCPolySupport.IndependentSums.gammaSigma sigma) (X y) A) : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma) (gridSupAbs sfin hs X) ((3 * max 1 (Real.log ↑sfin.card)) ^ sigma⁻¹ * A)

e.maxy.bound for an arbitrary nonempty finite grid.

The amplitude is the proved l.maximums.Gamma.s amplitude of this repository, (3 max 1 (log N))^{1/sigma} A, which enlarges the source's (3 log N)^{1/sigma} A only where the source proof does not apply (N = 1).

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gridSupAbs_descendants_isBigOWith {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] {d : ℕ} (hd : 1 ≤ d) (m : ℤ) (k : ℕ) {X : HCPolySupport.TriadicCube d → Omega → ℝ} {A sigma : ℝ} (hsigma : 0 < sigma) (hA : 0 ≤ A) (hX : ∀ R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k), HCPolySupport.IndependentSums.IsBigO mu (HCPolySupport.IndependentSums.gammaSigma sigma) (X R) A) : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma) (gridSupAbs (HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) ⋯ X) (gridNetConst d sigma * (↑k + 1) ^ sigma⁻¹ * A)

The e.maxy.bound lift at the triadic grid.

A common Gamma_sigma bound at amplitude A for every one of the 3^{d(k+1)} translates z + cu_{m-1-k} of cu_m lifts to the grid maximum at amplitude gridNetConst d sigma * (k+1)^{1/sigma} * A. The (k+1)^{1/sigma} factor is exactly the source's polynomial (m - n + 1)^{1/sigma} at m - n = k + 1, and gridNetConst is the constant the source absorbs into C.

6. gridSupAbs is CoarseGraining's grid maximum

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.maxDescendantBMatrixNormAtScale_eq_gridSupAbs {d : ℕ} (m : ℤ) (k : ℕ) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) : HCPolySupport.Book.Ch02.maxDescendantBMatrixNormAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k) a = gridSupAbs (HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) ⋯ (fun (R : HCPolySupport.TriadicCube d) (b : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) => HCPolySupport.Book.Ch02.coarseBMatrixNorm R b) a

The on-grid carrier identification. CoarseGraining's per-scale grid maximum, the quantity Ch02.LambdaSqFinite is defined from, is exactly this module's gridSupAbs applied to the one-cube coarse norms |b(R; a)|.