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

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

Pair capture by overlapping centers (G3)

If two points of a triadic cube Q are at sup-distance at most the side length of a depth-(j+1) cell, then some overlapping center cube at depth j contains both points. This is the geometric input G3 for the fractional Sobolev versus Besov comparison.

The proof parametrizes the depth-m descendants of Q by the integer index window of radius halfRange m = (3 ^ m - 1) / 2 around 3 ^ m * Q.index, then clamps the cell of the first point one step towards the center of the window so that the resulting overlapping cube both stays inside Q and captures the second point.

def HCPolySupport.Gagliardo.halfRange : ℕ → ℤ

Radius of the integer index window of the depth-m descendants: halfRange m = (3 ^ m - 1) / 2.

Equations

• HCPolySupport.Gagliardo.halfRange 0 = 0
• HCPolySupport.Gagliardo.halfRange m.succ = 3 * HCPolySupport.Gagliardo.halfRange m + 1

theorem HCPolySupport.Gagliardo.halfRange_zero : halfRange 0 = 0

theorem HCPolySupport.Gagliardo.halfRange_succ (m : ℕ) : halfRange (m + 1) = 3 * halfRange m + 1

theorem HCPolySupport.Gagliardo.two_mul_halfRange (m : ℕ) : 2 * halfRange m = 3 ^ m - 1

theorem HCPolySupport.Gagliardo.halfRange_nonneg (m : ℕ) : 0 ≤ halfRange m

theorem HCPolySupport.Gagliardo.one_le_halfRange_succ (m : ℕ) : 1 ≤ halfRange (m + 1)

theorem HCPolySupport.Gagliardo.mem_childCubes_of_scale_eq_of_index_range {d : ℕ} {P T : TriadicCube d} (hsc : T.scale = P.scale - 1) (hidx : ∀ (i : Fin d), 0 ≤ T.index i - 3 * P.index i + 1 ∧ T.index i - 3 * P.index i + 1 < 3) : T ∈ childCubes P

Membership constructor for childCubes: a cube one scale below P whose index is within the child window of P is a child of P.

theorem HCPolySupport.Gagliardo.index_range_of_mem_descendantsAtDepth {d : ℕ} {Q : TriadicCube d} {m : ℕ} {S : TriadicCube d} : S ∈ descendantsAtDepth Q m → ∀ (i : Fin d), 3 ^ m * Q.index i - halfRange m ≤ S.index i ∧ S.index i ≤ 3 ^ m * Q.index i + halfRange m

The index of a depth-m descendant of Q lies in the window of radius halfRange m around 3 ^ m * Q.index.

theorem HCPolySupport.Gagliardo.mem_descendantsAtDepth_of_index_range {d : ℕ} {Q : TriadicCube d} {m : ℕ} {T : TriadicCube d} : T.scale = Q.scale - ↑m → (∀ (i : Fin d), 3 ^ m * Q.index i - halfRange m ≤ T.index i ∧ T.index i ≤ 3 ^ m * Q.index i + halfRange m) → T ∈ descendantsAtDepth Q m

Converse: a cube at scale Q.scale - m whose index lies in the window of radius halfRange m around 3 ^ m * Q.index is a depth-m descendant.

def HCPolySupport.Gagliardo.clampIndex (A N u : ℤ) : ℤ

Clamp u to the window [A - N, A + N].

Equations

• HCPolySupport.Gagliardo.clampIndex A N u = max (A - N) (min (A + N) u)

theorem HCPolySupport.Gagliardo.clampIndex_range_wide {A h u : ℤ} (hh : 1 ≤ h) : A - h ≤ clampIndex A (h - 1) u ∧ clampIndex A (h - 1) u ≤ A + h

The clamped index stays in the wide window of radius h.

theorem HCPolySupport.Gagliardo.clampIndex_mem_range {A h u : ℤ} (hh : 1 ≤ h) : A - (h - 1) ≤ clampIndex A (h - 1) u ∧ clampIndex A (h - 1) u ≤ A + (h - 1)

The clamped index lies in the strict window of radius h - 1.

theorem HCPolySupport.Gagliardo.clampIndex_near {A h u : ℤ} (hh : 1 ≤ h) (h1 : A - h ≤ u) (h2 : u ≤ A + h) : u - 1 ≤ clampIndex A (h - 1) u ∧ clampIndex A (h - 1) u ≤ u + 1

The clamped index moves by at most one.

theorem HCPolySupport.Gagliardo.clampIndex_cases {A h u : ℤ} (hh : 1 ≤ h) (h1 : A - h ≤ u) (h2 : u ≤ A + h) : clampIndex A (h - 1) u = u ∨ u = A - h ∧ clampIndex A (h - 1) u = u + 1 ∨ u = A + h ∧ clampIndex A (h - 1) u = u - 1

Trichotomy: clamping is the identity except at the two extremes of the wide window, where it moves one step inward.

theorem HCPolySupport.Gagliardo.overlap_cubeSet_subset_of_index_range {d : ℕ} {Q T : TriadicCube d} {m : ℕ} (hscale : T.scale = Q.scale - ↑(m + 1)) (hbound : ∀ (i : Fin d), 3 ^ (m + 1) * Q.index i - (halfRange (m + 1) - 1) ≤ T.index i ∧ T.index i ≤ 3 ^ (m + 1) * Q.index i + (halfRange (m + 1) - 1)) : ScalarOverlap.cubeSet T ⊆ cubeSet Q

Fit lemma: an overlapping cube whose center index lies in the strict window of radius halfRange (m + 1) - 1 is contained in Q.

def HCPolySupport.Gagliardo.pairCenter {d : ℕ} (Q U : TriadicCube d) (j : ℕ) : TriadicCube d

The candidate overlapping center: the depth-(j + 1) cell U of the first point, clamped one step into the strict index window of Q.

Equations

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

theorem HCPolySupport.Gagliardo.pairCenter_scale {d : ℕ} (Q U : TriadicCube d) (j : ℕ) : (pairCenter Q U j).scale = U.scale

theorem HCPolySupport.Gagliardo.pairCenter_index {d : ℕ} (Q U : TriadicCube d) (j : ℕ) (i : Fin d) : (pairCenter Q U j).index i = clampIndex (3 ^ (j + 1) * Q.index i) (halfRange (j + 1) - 1) (U.index i)

theorem HCPolySupport.Gagliardo.cubeScaleFactor_pairCenter {d : ℕ} (Q U : TriadicCube d) (j : ℕ) : cubeScaleFactor (pairCenter Q U j) = cubeScaleFactor U

theorem HCPolySupport.Gagliardo.exists_centersAtDepth_pair_mem {d : ℕ} {Q : TriadicCube d} {j : ℕ} {x y : Vec d} (hx : x ∈ cubeSet Q) (hy : y ∈ cubeSet Q) (hxy : dist x y ≤ cubeScaleFactor Q / 3 ^ (j + 1)) : ∃ S ∈ ScalarOverlap.centersAtDepth Q j, x ∈ ScalarOverlap.cubeSet S ∧ y ∈ ScalarOverlap.cubeSet S

G3 (pair capture): two points of Q at sup-distance at most the side length of a depth-(j + 1) cell are both contained in some overlapping center cube at depth j.