HomSpineDepthBandSlice

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

The straddling band, its slices and its mass

What this file is for

The two measure-theoretic ingredients of the single-depth Gagliardo reduction, one per variable.

• straddleBand Q j k v — the set of pairs (x,y) inside Q on which the depth-j slice JUMPS and whose sup distance sits in the triadic band [3^{-(k+1)}·L, 3^{-k}·L), L = cubeScaleFactor Q. It is measurable and symmetric.
• measure_straddleBandSlice_le — the y-slice: a sup ball of radius 3^{-k}·L, so of volume at most (2·3^{-k}L)^d, and EMPTY unless x lies in straddleLayerSet Q j k (all of Q at the far bands k < j; the depth-j skeleton layer of thickness 3^{j-k} at the near bands, by the separation of HomSpineDepthBandGeometry).
• lintegral_indicator_straddleLayerSet_le — the x-mass carried by that layer: at most bandStraddleWeight (d+1) j k times the total mass of the slice, since the slice is constant on cells and the layer measure is 2·d·3^{j-k} per cell (HomSpineDepthStraddleMeasure).

Together these are exactly the two factors bandKernelVolume/bandStraddleWeight that HomSpineDepthBandArith.sum_bandTerm_le sums.

1. The straddling band

def Algsuperdiff.Section4.Provider.Homogenization.straddleBand {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j k : ℕ) (v : HCPolySupport.TriadicCube d → HCPolySupport.Vec d) : Set (HCPolySupport.Vec d × HCPolySupport.Vec d)

The pairs of Q on which the depth-j slice jumps, at triadic band k.

Equations

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

theorem Algsuperdiff.Section4.Provider.Homogenization.measurableSet_straddleBand {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j k : ℕ) (v : HCPolySupport.TriadicCube d → HCPolySupport.Vec d) : MeasurableSet (straddleBand Q j k v)

theorem Algsuperdiff.Section4.Provider.Homogenization.mem_straddleBand_swap {d : ℕ} {Q : HCPolySupport.TriadicCube d} {j k : ℕ} {v : HCPolySupport.TriadicCube d → HCPolySupport.Vec d} {x y : HCPolySupport.Vec d} (h : (x, y) ∈ straddleBand Q j k v) : (y, x) ∈ straddleBand Q j k v

The band is symmetric in its two variables.

def Algsuperdiff.Section4.Provider.Homogenization.straddleLayerSet {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j k : ℕ) : Set (HCPolySupport.Vec d)

The x-set the band can meet: everything at the far bands, and the depth-j skeleton layer of thickness 3^{j-k} at the near bands.

Equations

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

2. The y-slice

theorem Algsuperdiff.Section4.Provider.Homogenization.measure_straddleBandSlice_le {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j k : ℕ) (v : HCPolySupport.TriadicCube d → HCPolySupport.Vec d) (x : HCPolySupport.Vec d) : MeasureTheory.volume {y : HCPolySupport.Vec d | (x, y) ∈ straddleBand Q j k v} ≤ ENNReal.ofReal ((2 * ((1 / 3) ^ k * HCPolySupport.cubeScaleFactor Q)) ^ d) * (straddleLayerSet Q j k).indicator (fun (x : HCPolySupport.Vec d) => 1) x

The y-slice of the band, in the shape the inner integral consumes.

3. The x-mass of the layer

theorem Algsuperdiff.Section4.Provider.Homogenization.volume_cubeBoundaryLayer_le_succ {d : ℕ} (R : HCPolySupport.TriadicCube d) {t : ℝ} (ht0 : 0 ≤ t) : MeasureTheory.volume (HCPolySupport.cubeBoundaryLayer R t) ≤ ENNReal.ofReal (2 * (↑d + 1) * t * HCPolySupport.cubeVolume R)

The straddling measure at ANY thickness t ≤ 1, at the constant D = d+1 the band arithmetic runs on: below 1/2 this is HomSpineDepthStraddleMeasure.volume_cubeBoundaryLayer_le, above it the layer is the whole cell and 2·D·t ≥ 1.

theorem Algsuperdiff.Section4.Provider.Homogenization.lintegral_enorm_gridDualDepthTest_eq {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j : ℕ) (v : HCPolySupport.TriadicCube d → HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) : ∫⁻ (x : HCPolySupport.Vec d), ‖HCPolySupport.euclideanNorm (gridDualDepthTest Q j v x)‖ₑ ^ r ∂HCPolySupport.cubeMeasure Q = ∑ R ∈ HCPolySupport.descendantsAtDepth Q j, ‖HCPolySupport.euclideanNorm (v R)‖ₑ ^ r * ENNReal.ofReal (HCPolySupport.cubeVolume R)

The total mass of a depth slice, cell by cell.

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

THE LAYER MASS. The mass the depth slice carries on the band-k straddling layer is at most bandStraddleWeight (d+1) j k times its total mass: 1 at the far bands, 2·(d+1)·3^{j-k} at the near ones.