HomSpineDepthBandReduction

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

THE GAGLIARDO REDUCTION of a single depth slice

What this file is for

The Gagliardo double integral of the depth-j slice g_j, reduced to the band sums. Three moves, in order.

• enorm_cubeEuclideanWspKernel_rpow_le_tsum — POINTWISE. On a pair inside Q the kernel either vanishes (g_j does not jump) or the pair sits in EXACTLY ONE triadic band (exists_triadic_band), where the kernel is at most the band's lower endpoint to the power -(a+d) (euclideanDist ≥ dist, HomSpineDepthBandGeometry) and the increment is at most 2^{p'} times the two endpoint masses.
• lintegral_lintegral_enorm_cubeEuclideanWspKernel_rpow_le — the two integrals: one lintegral_prod to split the Gagliardo product measure, one lintegral_tsum per variable to exchange the band sum with the integrals, and HomSpineDepthBandIntegral's band integral in each term.
• cubeEuclideanWspESeminorm_gridDualDepthTest_rpow_le — the result:

  [g_j]_{W^{s,p'}(Q)}^{p'} ≤ 2^{p'}·2^{d+3}·(d+1)·3^d ·
      (cell side)^{-s·p'} · (near + Σ_{i<j} 3^{-i·s·p'}) · ⨍_Q ‖g_j‖^{p'},

with gridDepthBandFactor on the nose — the band shape HomSpineDepthGagliardoBand.GridDepthGagliardoBandInput demands.

1. Two elementary ℝ≥0∞ facts

theorem Algsuperdiff.Section4.Provider.Homogenization.ennreal_add_rpow_le (u v : ENNReal) {r : ℝ} (hr : 0 ≤ r) : (u + v) ^ r ≤ 2 ^ r * (u ^ r + v ^ r)

The crude p-th power splitting, at the constant 2^p (no convexity).

theorem Algsuperdiff.Section4.Provider.Homogenization.euclideanNorm_sub_le {d : ℕ} (u w : HCPolySupport.Vec d) : HCPolySupport.euclideanNorm (u - w) ≤ HCPolySupport.euclideanNorm u + HCPolySupport.euclideanNorm w

The Euclidean magnitude is subadditive on differences.

2. The band integrand

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.bandIntegrand {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ↑HCPolySupport.FractionalOrder) (q : HCPolySupport.FiniteLpExponent) (j : ℕ) (v : HCPolySupport.TriadicCube d → HCPolySupport.Vec d) (k : ℕ) : HCPolySupport.Vec d × HCPolySupport.Vec d → ENNReal

The integrand of one triadic band: the band's kernel ceiling (3^{-(k+1)}L)^{-(a+d)} times 2^{p'} times the two endpoint masses of the depth slice, supported on the straddling band.

Equations

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

theorem Algsuperdiff.Section4.Provider.Homogenization.measurable_bandIntegrand {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ↑HCPolySupport.FractionalOrder) (q : HCPolySupport.FiniteLpExponent) (j : ℕ) (v : HCPolySupport.TriadicCube d → HCPolySupport.Vec d) (k : ℕ) : Measurable (bandIntegrand Q s q j v k)

3. The pointwise band bound

theorem Algsuperdiff.Section4.Provider.Homogenization.enorm_cubeEuclideanWspKernel_rpow_le_tsum {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ↑HCPolySupport.FractionalOrder) (q : HCPolySupport.FiniteLpExponent) (j : ℕ) (v : HCPolySupport.TriadicCube d → HCPolySupport.Vec d) {x y : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.cubeSet Q) (hy : y ∈ HCPolySupport.cubeSet Q) : ‖HCPolySupport.cubeEuclideanWspKernel s q (gridDualDepthTest Q j v) (x, y)‖ₑ ^ q.exponent.toReal ≤ ∑' (k : ℕ), bandIntegrand Q s q j v k (x, y)

THE POINTWISE BAND BOUND. Every pair of Q is either a non-jump of the depth slice (kernel zero) or sits in exactly one triadic band.

4. The band integral, at the band term

theorem Algsuperdiff.Section4.Provider.Homogenization.lintegral_lintegral_bandIntegrand_le {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ↑HCPolySupport.FractionalOrder) (q : HCPolySupport.FiniteLpExponent) (j : ℕ) (v : HCPolySupport.TriadicCube d → HCPolySupport.Vec d) (k : ℕ) : ∫⁻ (x : HCPolySupport.Vec d), ∫⁻ (y : HCPolySupport.Vec d), bandIntegrand Q s q j v k (x, y) ∂HCPolySupport.cubeMeasure Q ∂HCPolySupport.cubeMeasure Q ≤ ENNReal.ofReal (bandTerm (↑s * q.exponent.toReal) (HCPolySupport.cubeScaleFactor Q) (↑d + 1) d j k) * (2 ^ q.exponent.toReal * 2) * ∫⁻ (x : HCPolySupport.Vec d), ‖HCPolySupport.euclideanNorm (gridDualDepthTest Q j v x)‖ₑ ^ q.exponent.toReal ∂HCPolySupport.cubeMeasure Q

5. The double integral

theorem Algsuperdiff.Section4.Provider.Homogenization.tsum_ofReal_bandTerm_le {a L : ℝ} (ha0 : 0 < a) (ha : a ≤ 1 / 2) (hL : 0 < L) {D : ℝ} (hD : 1 ≤ D) (dd j : ℕ) : ∑' (k : ℕ), ENNReal.ofReal (bandTerm a L D dd j k) ≤ ENNReal.ofReal (2 ^ (dd + 2) * D * 3 ^ dd * (L / 3 ^ j) ^ (-a) * gridDepthBandFactor a j)

The band sum of HomSpineDepthBandArith, read as an ℝ≥0∞ series.

theorem Algsuperdiff.Section4.Provider.Homogenization.lintegral_lintegral_enorm_cubeEuclideanWspKernel_rpow_le {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ↑HCPolySupport.FractionalOrder) (q : HCPolySupport.FiniteLpExponent) (j : ℕ) (v : HCPolySupport.TriadicCube d → HCPolySupport.Vec d) (hband : ↑s * q.exponent.toReal ≤ 1 / 2) : ∫⁻ (x : HCPolySupport.Vec d), ∫⁻ (y : HCPolySupport.Vec d), ‖HCPolySupport.cubeEuclideanWspKernel s q (gridDualDepthTest Q j v) (x, y)‖ₑ ^ q.exponent.toReal ∂HCPolySupport.cubeMeasure Q ∂HCPolySupport.cubeMeasure Q ≤ ENNReal.ofReal (2 ^ (d + 2) * (↑d + 1) * 3 ^ d * (HCPolySupport.cubeScaleFactor Q / 3 ^ j) ^ (-(↑s * q.exponent.toReal)) * gridDepthBandFactor (↑s * q.exponent.toReal) j) * (2 ^ q.exponent.toReal * 2) * ∫⁻ (x : HCPolySupport.Vec d), ‖HCPolySupport.euclideanNorm (gridDualDepthTest Q j v x)‖ₑ ^ q.exponent.toReal ∂HCPolySupport.cubeMeasure Q

THE DOUBLE INTEGRAL. Pointwise band bound, one lintegral_tsum per variable, the band integral in each term, and the closed band sum.

6. The Gagliardo seminorm of the depth slice

theorem Algsuperdiff.Section4.Provider.Homogenization.cubeEuclideanWspESeminorm_gridDualDepthTest_rpow_le {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ↑HCPolySupport.FractionalOrder) (q : HCPolySupport.FiniteLpExponent) (j : ℕ) (v : HCPolySupport.TriadicCube d → HCPolySupport.Vec d) (hband : ↑s * q.exponent.toReal ≤ 1 / 2) : HCPolySupport.cubeEuclideanWspESeminorm Q s q (gridDualDepthTest Q j v) ^ q.exponent.toReal ≤ ENNReal.ofReal (2 ^ (d + 2) * (↑d + 1) * 3 ^ d * (HCPolySupport.cubeScaleFactor Q / 3 ^ j) ^ (-(↑s * q.exponent.toReal)) * gridDepthBandFactor (↑s * q.exponent.toReal) j) * (2 ^ q.exponent.toReal * 2) * ∫⁻ (x : HCPolySupport.Vec d), ‖HCPolySupport.euclideanNorm (gridDualDepthTest Q j v x)‖ₑ ^ q.exponent.toReal ∂HCPolySupport.normalizedCubeMeasure Q

THE GAGLIARDO REDUCTION. The single-depth Gagliardo seminorm, reduced to the band factor gridDepthBandFactor at the explicit dimensional constant 2^{p'}·2^{d+3}·(d+1)·3^d and the cell-side weight.