Coarse-graining support: Support.Sobolev.Fractional.ShellGeometry

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Shell geometry for the fractional Sobolev versus Besov comparison

Pure triadic-cube geometry and counting; no measure theory. This file provides the geometric inputs for both directions of the comparison:

• G1 (diameter): two points of an overlapping cube are at sup-distance less than its side length 3 * cubeScaleFactor S;
• scale bookkeeping for centers at a given depth.

The bounded-overlap count (G2) and the pair-capture lemma (G3) build on these in the companion files.

theorem HCPolySupport.Gagliardo.cubeScaleFactor_pos' {d : ℕ} (S : TriadicCube d) : 0 < cubeScaleFactor S

Positivity of the triadic scale factor (public form).

theorem HCPolySupport.Gagliardo.coord_bounds_of_mem_overlapCubeSet {d : ℕ} {S : TriadicCube d} {x : Vec d} (hx : x ∈ ScalarOverlap.cubeSet S) (i : Fin d) : (↑(S.index i) - 3 / 2) * cubeScaleFactor S ≤ x i ∧ x i < (↑(S.index i) + 3 / 2) * cubeScaleFactor S

Coordinates of a point of an overlapping cube lie in the defining window.

theorem HCPolySupport.Gagliardo.dist_le_of_mem_overlapCubeSet {d : ℕ} {S : TriadicCube d} {x y : Vec d} (hx : x ∈ ScalarOverlap.cubeSet S) (hy : y ∈ ScalarOverlap.cubeSet S) : dist x y ≤ 3 * cubeScaleFactor S

G1 (diameter bound): the overlapping cube of side 3 * cubeScaleFactor S has sup-norm diameter at most its side length.

theorem HCPolySupport.Gagliardo.scale_of_mem_centersAtDepth {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (hS : S ∈ ScalarOverlap.centersAtDepth Q j) : S.scale = Q.scale - ↑(j + 1)

The scale of a center at depth j below Q.

theorem HCPolySupport.Gagliardo.eq_of_index_eq_of_mem_centersAtDepth {d : ℕ} {Q S T : TriadicCube d} {j : ℕ} (hS : S ∈ ScalarOverlap.centersAtDepth Q j) (hT : T ∈ ScalarOverlap.centersAtDepth Q j) (hindex : S.index = T.index) : S = T

Two centers at the same depth with the same index coincide.