HomSpineDepthBandArith

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

The band sum of the single-depth Gagliardo reduction, in closed form

What this file is for

Pure scalar arithmetic, over abstract reals, away from every measure: the exact size of the triadic band sum the Gagliardo reduction of a depth-j slice produces. Banding the double integral at |x-y| ∈ [3^{-(k+1)}·L, 3^{-k}·L) (L the side of the ambient cube, k: ℕ by exists_triadic_band), band k carries

• the KERNEL factor (3^{-(k+1)}L)^{-(a+d)} (a = s·p' the order weight),
• the sup-BALL factor (2·3^{-k}L)^d, and
• the STRADDLING weight bandStraddleWeight: 1 at the far bands k < j (every pair straddles) and 2·D·3^{j-k} at the near bands k ≥ j (HomSpineDepthStraddleMeasure.volume_cubeBoundaryLayer_le at thickness 3^{j-k}).

sum_bandTerm_le sums the three over ALL bands and matches exactly HomSpineDepthGagliardoBand.gridDepthBandFactor a j = near + Σ_{i<j} 3^{-i·a}, at the explicit dimensional prefactor 2^{d+2}·D·3^d and the cell-side weight (L/3^j)^{-a}. The two halves are the band facts used verbatim: sum_near_band_le for k ≥ j and the truncated geometric sum for k < j. The one-band kernel gain 3^a ≤ 2 is HomLiftScaleArith.three_rpow_le_two.

1. Elementary rpow facts on the admissible band

theorem Algsuperdiff.Section4.Provider.Homogenization.inv_three_pow_eq (k : ℕ) : (1 / 3) ^ k = 3 ^ (-↑k)

The triadic weight as a real power.

2. The band term

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.bandStraddleWeight (D : ℝ) (j k : ℕ) : ℝ

The straddling weight of band k at depth j: at the far bands every pair straddles the depth-j skeleton (weight 1); at the near bands only the boundary layer of thickness 3^{j-k} does, and its measure is 2·d·3^{j-k} times the cell measure — read here at D = d+1.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.bandStraddleWeight D j k = if k < j then 1 else 2 * D * (1 / 3) ^ (k - j)

theorem Algsuperdiff.Section4.Provider.Homogenization.bandStraddleWeight_nonneg {D : ℝ} (hD : 0 ≤ D) (j k : ℕ) : 0 ≤ bandStraddleWeight D j k

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.bandKernelVolume (a L : ℝ) (dd k : ℕ) : ℝ

The kernel-times-ball factor of band k: (3^{-(k+1)}L)^{-(a+d)}·(2·3^{-k}L)^d.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.bandKernelVolume a L dd k = ((1 / 3) ^ (k + 1) * L) ^ (-(a + ↑dd)) * (2 * ((1 / 3) ^ k * L)) ^ dd

theorem Algsuperdiff.Section4.Provider.Homogenization.bandKernelVolume_eq {a L : ℝ} (hL : 0 < L) (dd k : ℕ) : bandKernelVolume a L dd k = 2 ^ dd * 3 ^ (a + ↑dd) * (3 ^ (a * ↑k) * L ^ (-a))

The band factor in closed form. The d powers of the ball radius cancel d of the d+a powers of the kernel, leaving one gain 3^a per band and the running weight 3^{a·k}·L^{-a}.

theorem Algsuperdiff.Section4.Provider.Homogenization.bandKernelVolume_nonneg {a L : ℝ} (hL : 0 ≤ L) (dd k : ℕ) : 0 ≤ bandKernelVolume a L dd k

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.bandTerm (a L D : ℝ) (dd j k : ℕ) : ℝ

The full band term: kernel × ball × straddling weight.

Equations

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

3. The two halves of the band sum

theorem Algsuperdiff.Section4.Provider.Homogenization.sum_far_three_rpow_le {a : ℝ} (ha0 : 0 < a) (j : ℕ) : ∑ k ∈ Finset.range j, 3 ^ (a * ↑k) ≤ 3 ^ (a * ↑j) * ∑ i ∈ Finset.range j, 3 ^ (-a * ↑i)

The FAR half k < j: the running weights 3^{a·k} are the truncated geometric sum of HomSpineDepthGagliardoBand, read backwards from the cell scale.

theorem Algsuperdiff.Section4.Provider.Homogenization.sum_near_bandStraddleWeight_le {a : ℝ} (ha : a ≤ 1 / 2) {D : ℝ} (hD : 0 ≤ D) (j n : ℕ) : ∑ k ∈ Finset.Ico j n, 3 ^ (a * ↑k) * bandStraddleWeight D j k ≤ 2 * D * 3 ^ (a * ↑j) * nearBandGeometricConstant

The NEAR half k ≥ j: geometric at ratio 3^{-(1-a)} ≤ 3^{-1/2}, so the sum_near_band_le applies verbatim.

4. The band sum

theorem Algsuperdiff.Section4.Provider.Homogenization.sum_three_rpow_mul_bandStraddleWeight_le {a : ℝ} (ha0 : 0 < a) (ha : a ≤ 1 / 2) {D : ℝ} (hD : 1 ≤ D) (j n : ℕ) : ∑ k ∈ Finset.range n, 3 ^ (a * ↑k) * bandStraddleWeight D j k ≤ 2 * D * 3 ^ (a * ↑j) * gridDepthBandFactor a j

The weighted running sum, both halves together.

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

THE BAND SUM, CLOSED. Every partial sum of the band terms is below the depth-j band factor at the explicit dimensional prefactor 2^{d+2}·D·3^d and the cell-side weight (L/3^j)^{-a}.

This is the whole arithmetic of the single-depth Gagliardo reduction: the far bands give Σ_{i<j} 3^{-i·a}, the near bands give nearBandGeometricConstant, and the one-band kernel gain 3^a is absorbed by a ≤ 1/2.