HomFinitePGauge

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

Theorem B, §4.5: the finite-p negative Besov carrier

Why a finite p

A large finite p — here p = 4d — suffices, the L^∞ statement being recovered from it by Sobolev embedding. The p ↑ ∞ application of the general coarse-graining proposition is replaced by the PRINTED finite-p proposition (stated for p ∈ [2,∞) at C(p,d)), and the L^∞ endpoint is reached by a supercritical embedding. This module supplies the finite-p carrier and the one extraction step that converts it into the exponent shift s ↦ s + d/p.

The carrier pin

The manuscript never defines ‖·‖_{W_hat^{-s,p}(□_m)}: the manuscript defines only the order -1 duals. The only negative-order fractional object defined anywhere in the manuscript is the negative Besov seminorm,

  [F]_{B^{-s}_{p,q}(□_m)}
    = ( Σ_{n ≤ m} 3^{sqn} ( avsum_{z ∈ 3^n ℤ^d ∩ □_m} |(F)_{z+□_n}|^p )^{q/p} )^{1/q}

(the printed weight 3^{sqm} is the index typo). Under the Besov--Sobolev dictionary W^{-s,p} ≃ B^{-s}_{p,p} the Step-3 object is the (p,q) = (p,p) member, which is what this module defines. Three facts about the printed grid are load-bearing and are recorded here:

• the grid of the negative Besov seminorm definition is the pure lattice 3^n ℤ^d ∩ □_m, i.e. exactly the triadic partition of □_m into the depth-(m-n) descendants — not the half-shifted family 3^{n-1} ℤ^d of the positive seminorm the Besov seminorm definition. So the carrier here is CoarseGraining's descendantsAtDepth, verbatim;
• the depth weight 3^{-sj} at depth j = m - n is exactly the display's own 3^{-ms}·3^{sn}, i.e. the gauge below is the display's left-hand quantity 3^{-ms}‖·‖. This is the normalization (negBesovInftyDepthSeminorm_eq_scaleNormalized) at finite p;
• the inner norm is the Euclidean vector norm, as in the p = ∞ pin.

Main definitions and results

• negBesovLpDepthMean — the depth-j ℓ^p mean of the grid cell averages, ( avsum_{R ∈ D_j} |(F)_R|^p )^{1/p};
• negBesovLpDepthSeminorm — its 3^{-sj} weighted form;
• sqrt_vecNormSq_cubeAverageVec_le_of_depthBound — THE EXTRACTION: one term of an ℓ^p mean over 3^{jd} cells is at most 3^{jd/p} times the mean, so the per-cell gauge holds at the shifted exponent s + d/p and at the SAME constant.

References

• ABK26, the general coarse-graining proposition; the negative Besov seminorm definition; the Besov seminorm definition.

1. Elementary rpow arithmetic

theorem Algsuperdiff.Section4.Provider.Homogenization.le_of_rpow_le_rpow {x C p : ℝ} (hx : 0 ≤ x) (hC : 0 ≤ C) (hp : 0 < p) (h : x ^ p ≤ C ^ p) : x ≤ C

From x ^ p ≤ C ^ p with nonnegative x, C and positive p, conclude x ≤ C. Stated once so no proof below re-derives it.

theorem Algsuperdiff.Section4.Provider.Homogenization.descendantsAtDepth_card_rpow {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j : ℕ) : ↑(HCPolySupport.descendantsAtDepth Q j).card = 3 ^ (↑d * ↑j)

The cardinality of the depth-j grid, as a real rpow. This is the 3^{jd} that the extraction pays.

theorem Algsuperdiff.Section4.Provider.Homogenization.descendantsAtDepth_card_pos {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j : ℕ) : 0 < ↑(HCPolySupport.descendantsAtDepth Q j).card

2. The finite-p gauge on the printed grid

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.negBesovLpDepthMean {d : ℕ} (Q : HCPolySupport.TriadicCube d) (p : ℝ) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) (j : ℕ) : ℝ

The depth-j ℓ^p mean of the grid cell averages, ( avsum_{R ∈ D_j} |(F)_R|^p )^{1/p} — the inner index of the negative Besov seminorm definition at a finite exponent p, on the pure triadic grid the manuscript prints.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.negBesovLpDepthSeminorm {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s p : ℝ) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) (j : ℕ) : ℝ

The weighted depth-j quantity of the finite-p gauge; the weight 3^{-sj} is the display's own 3^{-ms}·3^{sn} at n = m - j.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.negBesovLpDepthSeminorm Q s p F j = 3 ^ (-s * ↑j) * Algsuperdiff.Section4.Provider.Homogenization.negBesovLpDepthMean Q p F j

theorem Algsuperdiff.Section4.Provider.Homogenization.negBesovLpDepthMean_def {d : ℕ} (Q : HCPolySupport.TriadicCube d) (p : ℝ) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) (j : ℕ) : negBesovLpDepthMean Q p F j = (HCPolySupport.descendantsAverage Q j fun (R : HCPolySupport.TriadicCube d) => √(HCPolySupport.vecNormSq (HCPolySupport.cubeAverageVec R F)) ^ p) ^ (1 / p)

theorem Algsuperdiff.Section4.Provider.Homogenization.negBesovLpDepthSeminorm_def {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s p : ℝ) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) (j : ℕ) : negBesovLpDepthSeminorm Q s p F j = 3 ^ (-s * ↑j) * negBesovLpDepthMean Q p F j

3. Elementary API

theorem Algsuperdiff.Section4.Provider.Homogenization.descendantsAverage_rpow_nonneg {d : ℕ} (Q : HCPolySupport.TriadicCube d) (p : ℝ) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) (j : ℕ) : 0 ≤ HCPolySupport.descendantsAverage Q j fun (R : HCPolySupport.TriadicCube d) => √(HCPolySupport.vecNormSq (HCPolySupport.cubeAverageVec R F)) ^ p

theorem Algsuperdiff.Section4.Provider.Homogenization.negBesovLpDepthMean_nonneg {d : ℕ} (Q : HCPolySupport.TriadicCube d) (p : ℝ) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) (j : ℕ) : 0 ≤ negBesovLpDepthMean Q p F j

theorem Algsuperdiff.Section4.Provider.Homogenization.negBesovLpDepthSeminorm_nonneg {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s p : ℝ) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) (j : ℕ) : 0 ≤ negBesovLpDepthSeminorm Q s p F j

theorem Algsuperdiff.Section4.Provider.Homogenization.negBesovLpDepthMean_rpow {d : ℕ} (Q : HCPolySupport.TriadicCube d) {p : ℝ} (hp : 0 < p) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) (j : ℕ) : negBesovLpDepthMean Q p F j ^ p = HCPolySupport.descendantsAverage Q j fun (R : HCPolySupport.TriadicCube d) => √(HCPolySupport.vecNormSq (HCPolySupport.cubeAverageVec R F)) ^ p

The p-th power of the depth mean recovers the depth average.

5. THE EXTRACTION: one cell out of the ℓ^p mean

theorem Algsuperdiff.Section4.Provider.Homogenization.sqrt_vecNormSq_cubeAverageVec_le_of_depthBound {d : ℕ} {Q : HCPolySupport.TriadicCube d} {s p A : ℝ} (hp : 0 < p) {F : HCPolySupport.Vec d → HCPolySupport.Vec d} {j : ℕ} (hbd : negBesovLpDepthSeminorm Q s p F j ≤ A) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtDepth Q j) : √(HCPolySupport.vecNormSq (HCPolySupport.cubeAverageVec R F)) ≤ A * 3 ^ ((s + ↑d / p) * ↑j)

The extraction, per cell.

If the depth-j weighted ℓ^p mean is at most A, then every single cell at depth j obeys

  |(F)_R| ≤ A · 3^{j(s + d/p)}.

The 3^{jd/p} is exactly the cardinality 3^{jd} of the depth-j grid raised to 1/p; there is no other loss, so the constant is A itself. This is the "Jensen one scale up" step, in its sharp form: an ℓ^p mean controls one term at the price of the count, and that price is precisely the exponent shift s ↦ s + d/p.