HomSpineDepthBandGeometry #

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

Band geometry for the single-depth Gagliardo reduction #

What this file is for #

HomSpineDepthGagliardoBand names the Gagliardo band input GridDepthGagliardoBandInput; HomSpineDepthStraddleMeasure supplies the separation and the straddling measure. The reduction of the Gagliardo double integral of the depth-j slice to the band sums needs four more elementary facts, all proved here:

dist_le_euclideanDist — the ambient sup metric is below the Euclidean one, so the Gagliardo kernel (which uses euclideanDist at a NEGATIVE exponent) is bounded above by the sup-metric kernel, and the sup-metric balls of Real.volume_pi_closedBall become available (volume_closedBall_eq, and its open-ball corollary volume_setOf_dist_lt_le);
exists_triadic_band — every distance strictly inside (0, side) lies in exactly one triadic band [3^{-(k+1)}·side, 3^{-k}·side), k: ℕ;
dist_lt_cubeScaleFactor — the sup diameter of a triadic cube is its side, so band k = 0 is the coarsest one that occurs;
mem_biUnion_cubeBoundaryLayer_of_gridDualDepthTest_ne — the SEPARATION in the form the near bands consume: if the depth-j slice jumps between x and a point within t·(cell side) of it, then x is in the depth-j skeleton layer of thickness t, whose measure HomSpineDepthStraddleMeasure bounds.

The measurability facts the Tonelli step of the reduction needs (measurable_gridDualDepthTest, measurable_cubeEuclideanWspKernel) are proved here too, since they are pure ambient facts.

1. The two metrics, and sup-metric balls #

source

theorem Algsuperdiff.Section4.Provider.Homogenization.dist_le_euclideanDist {d : ℕ} (x y : HCPolySupport.Vec d) :

dist x y ≤ HCPolySupport.euclideanDist x y

The ambient (sup) distance of Vec d is below the Euclidean distance. The Gagliardo kernel carries a NEGATIVE power of euclideanDist, so this is the inequality that lets the estimate run on sup-metric balls.

source

theorem Algsuperdiff.Section4.Provider.Homogenization.euclideanDist_rpow_neg_le {d : ℕ} (x y : HCPolySupport.Vec d) {e : ℝ} (he : 0 < e) :

HCPolySupport.euclideanDist x y ^ (-e) ≤ dist x y ^ (-e)

The Gagliardo kernel, bounded above by the sup-metric kernel. (Both sides vanish on the diagonal: Real.rpow sends 0 to 0 at a negative exponent.)

source

theorem Algsuperdiff.Section4.Provider.Homogenization.volume_closedBall_eq {d : ℕ} (x : HCPolySupport.Vec d) {ρ : ℝ} (hρ : 0 ≤ ρ) :

MeasureTheory.volume (Metric.closedBall x ρ) = ENNReal.ofReal ((2 * ρ) ^ d)

The sup-metric closed ball has volume (2ρ)^d.

source

theorem Algsuperdiff.Section4.Provider.Homogenization.volume_setOf_dist_lt_le {d : ℕ} (x : HCPolySupport.Vec d) {ρ : ℝ} (hρ : 0 ≤ ρ) :

MeasureTheory.volume {y : HCPolySupport.Vec d | dist x y < ρ} ≤ ENNReal.ofReal ((2 * ρ) ^ d)

The set of points within sup-distance ρ of x has volume at most (2ρ)^d.

2. The triadic bands #

source

theorem Algsuperdiff.Section4.Provider.Homogenization.exists_triadic_band {u : ℝ} (hu0 : 0 < u) (hu1 : u < 1) :

∃ (k : ℕ), (1 / 3) ^ (k + 1) ≤ u ∧ u < (1 / 3) ^ k

THE TRIADIC BAND DECOMPOSITION. Every u ∈ (0,1) lies in exactly one band [3^{-(k+1)}, 3^{-k}) with k: ℕ.

source

theorem Algsuperdiff.Section4.Provider.Homogenization.dist_lt_cubeScaleFactor {d : ℕ} {Q : HCPolySupport.TriadicCube d} {x y : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.cubeSet Q) (hy : y ∈ HCPolySupport.cubeSet Q) :

dist x y < HCPolySupport.cubeScaleFactor Q

The sup diameter of a triadic cube is its side: no band coarser than k = 0 occurs inside a cube.

3. The separation, in skeleton-layer form #

source

theorem Algsuperdiff.Section4.Provider.Homogenization.mem_biUnion_cubeBoundaryLayer_of_gridDualDepthTest_ne {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j : ℕ) (v : HCPolySupport.TriadicCube d → HCPolySupport.Vec d) {t : ℝ} (ht : 0 ≤ t) {x y : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.cubeSet Q) (hne : gridDualDepthTest Q j v y ≠ gridDualDepthTest Q j v x) (hlt : dist x y < t * (HCPolySupport.cubeScaleFactor Q / 3 ^ j)) :

x ∈ ⋃ R ∈ HCPolySupport.descendantsAtDepth Q j, HCPolySupport.cubeBoundaryLayer R t

THE SEPARATION FOR THE NEAR BANDS. If the depth-j slice takes different values at x and at a point within t·(cell side) of x, then x lies in the depth-j skeleton layer of normalized thickness t, whose normalized measure is at most 2·d·t.