Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Fractional.OverlapCount

Coarse-graining support: Support.Sobolev.Fractional.OverlapCount #

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

Bounded-overlap count (G2) for the depth-j overlapping center family #

A point x can lie in at most 3 ^ d of the overlapping cubes ScalarOverlap.cubeSet S as S ranges over ScalarOverlap.centersAtDepth Q j.

The proof is purely arithmetic: all centers at depth j share the same scale, hence the same side factor c = 3 ^ (Q.scale - (j + 1)). Membership of x in the overlapping cube of S pins each coordinate S.index i into the integer window (x i / c - 3/2, x i / c + 3/2], which contains at most 3 integers. Since a center is determined by its index vector, at most 3 ^ d centers can capture x.

source
theorem HCPolySupport.Gagliardo.card_Icc_window_le_three (t : ℝ) :
(Finset.Icc (⌊t - 3 / 2⌋ + 1) ⌊t + 3 / 2⌋).card ≤ 3

The half-open real window (t - 3/2, t + 3/2] contains at most three integers: they all lie in Finset.Icc (⌊t - 3/2⌋ + 1) ⌊t + 3/2⌋, and this interval has at most three elements.

source
theorem HCPolySupport.Gagliardo.index_mem_Icc_of_mem_overlapCubeSet {d : ℕ} {S : TriadicCube d} {x : Vec d} (hx : x ∈ ScalarOverlap.cubeSet S) (i : Fin d) :
S.index i ∈ Finset.Icc (⌊x i / cubeScaleFactor S - 3 / 2⌋ + 1) ⌊x i / cubeScaleFactor S + 3 / 2⌋

If x lies in the overlapping cube of S, then each coordinate of the index of S lies in the integer window determined by x i / cubeScaleFactor S.

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

All cubes of the depth-j center family share the side factor 3 ^ (Q.scale - (j + 1)).

source
theorem HCPolySupport.Gagliardo.card_centersAtDepth_filter_mem_le {d : ℕ} (Q : TriadicCube d) (j : ℕ) (x : Vec d) :
{S ∈ ScalarOverlap.centersAtDepth Q j | x ∈ ScalarOverlap.cubeSet S}.card ≤ 3 ^ d

G2 (bounded overlap): a point lies in at most 3^d overlapping cubes of the depth-j center family.