HomSpineDepthBandIntegral

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

The band integral: one Fubini, one symmetry, one mass bound

What this file is for

The double integral of the depth-j slice's mass over ONE triadic band. With N x = ‖g_j(x)‖ₑ^{p'} and Ω_k = straddleBand Q j k v,

  ∫∫_{Ω_k} (N x + N y)  ≤  2·(2·3^{-k}L)^d · bandStraddleWeight (d+1) j k · ∫ N.

The x-half is HomSpineDepthBandSlice's two bounds composed: the y-slice is a sup ball and is empty off the straddling layer, and the layer carries at most bandStraddleWeight of the mass. The y-half is the SAME quantity: Ω_k is symmetric and cubeMeasure Q is σ-finite, so one Tonelli swap (lintegral_lintegral_swap) identifies the two halves exactly — no second estimate is made.

1. Measurability of the two band densities

theorem Algsuperdiff.Section4.Provider.Homogenization.measurable_enorm_gridDualDepthTest {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j : ℕ) (v : HCPolySupport.TriadicCube d → HCPolySupport.Vec d) (r : ℝ) : Measurable fun (x : HCPolySupport.Vec d) => ‖HCPolySupport.euclideanNorm (gridDualDepthTest Q j v x)‖ₑ ^ r

2. The x-half

theorem Algsuperdiff.Section4.Provider.Homogenization.lintegral_lintegral_straddleBand_fst_le {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j k : ℕ) (v : HCPolySupport.TriadicCube d → HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) : ∫⁻ (x : HCPolySupport.Vec d), ∫⁻ (y : HCPolySupport.Vec d), (straddleBand Q j k v).indicator (fun (z : HCPolySupport.Vec d × HCPolySupport.Vec d) => ‖HCPolySupport.euclideanNorm (gridDualDepthTest Q j v z.1)‖ₑ ^ r) (x, y) ∂HCPolySupport.cubeMeasure Q ∂HCPolySupport.cubeMeasure Q ≤ ENNReal.ofReal ((2 * ((1 / 3) ^ k * HCPolySupport.cubeScaleFactor Q)) ^ d) * ENNReal.ofReal (bandStraddleWeight (↑d + 1) j k) * ∫⁻ (x : HCPolySupport.Vec d), ‖HCPolySupport.euclideanNorm (gridDualDepthTest Q j v x)‖ₑ ^ r ∂HCPolySupport.cubeMeasure Q

THE BAND INTEGRAL, x-HALF. The y-slice contributes the sup-ball volume and confines x to the straddling layer; the layer carries at most bandStraddleWeight of the slice's mass.

3. The y-half, by symmetry

theorem Algsuperdiff.Section4.Provider.Homogenization.lintegral_lintegral_straddleBand_snd_eq {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j k : ℕ) (v : HCPolySupport.TriadicCube d → HCPolySupport.Vec d) (r : ℝ) : ∫⁻ (x : HCPolySupport.Vec d), ∫⁻ (y : HCPolySupport.Vec d), (straddleBand Q j k v).indicator (fun (z : HCPolySupport.Vec d × HCPolySupport.Vec d) => ‖HCPolySupport.euclideanNorm (gridDualDepthTest Q j v z.2)‖ₑ ^ r) (x, y) ∂HCPolySupport.cubeMeasure Q ∂HCPolySupport.cubeMeasure Q = ∫⁻ (x : HCPolySupport.Vec d), ∫⁻ (y : HCPolySupport.Vec d), (straddleBand Q j k v).indicator (fun (z : HCPolySupport.Vec d × HCPolySupport.Vec d) => ‖HCPolySupport.euclideanNorm (gridDualDepthTest Q j v z.1)‖ₑ ^ r) (x, y) ∂HCPolySupport.cubeMeasure Q ∂HCPolySupport.cubeMeasure Q

THE SYMMETRY. One Tonelli swap identifies the y-half with the x-half: the band is symmetric and both slots carry the same finite measure.

4. The band integral

theorem Algsuperdiff.Section4.Provider.Homogenization.lintegral_lintegral_straddleBand_pair_le {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j k : ℕ) (v : HCPolySupport.TriadicCube d → HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) : ∫⁻ (x : HCPolySupport.Vec d), ∫⁻ (y : HCPolySupport.Vec d), (straddleBand Q j k v).indicator (fun (z : HCPolySupport.Vec d × HCPolySupport.Vec d) => ‖HCPolySupport.euclideanNorm (gridDualDepthTest Q j v z.1)‖ₑ ^ r) (x, y) + (straddleBand Q j k v).indicator (fun (z : HCPolySupport.Vec d × HCPolySupport.Vec d) => ‖HCPolySupport.euclideanNorm (gridDualDepthTest Q j v z.2)‖ₑ ^ r) (x, y) ∂HCPolySupport.cubeMeasure Q ∂HCPolySupport.cubeMeasure Q ≤ 2 * (ENNReal.ofReal ((2 * ((1 / 3) ^ k * HCPolySupport.cubeScaleFactor Q)) ^ d) * ENNReal.ofReal (bandStraddleWeight (↑d + 1) j k) * ∫⁻ (x : HCPolySupport.Vec d), ‖HCPolySupport.euclideanNorm (gridDualDepthTest Q j v x)‖ₑ ^ r ∂HCPolySupport.cubeMeasure Q)

THE BAND INTEGRAL. Both halves together, at the explicit band factor: the sup-ball volume of the slice times the straddling weight of the layer, twice (once per variable).