AnnulusSeparation

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

The annulus-separation count of ABK26's per-scale atoms

ABK26 asserts three times that a family of per-scale atoms is 2-dependent, with no argument. This module supplies the count, over this repository's carriers and at this repository's separation predicate SeparatedBy (Euclidean vecNorm), in the form the varying-level independence producer iIndepFun_of_local_cutoffSample consumes.

The geometry

The G_0 atom Y_n reads the field on the annulus Box_n \ Box_{n-1} through the truncation a_{n-2}, so its truncation level is Lidx n = n - 2. Two indices n' < n share only the shells i <= n' - 2, whose range of dependence is sqrt d * 3 ^ (n' - 2) = sqrt d * 3 ^ (min (Lidx n) (Lidx n')) -- exactly the threshold at which iIndep_lowerShellLocalSigma_of_varyingLevel and its observable consequence are stated. The G_2 atom X_j reads cubes z + Box_n at the field a_{n-2} with n <= j - 1, i.e. at truncation level `<= j

• 3; the same count runs at that offset. Both offsets are covered here by the free integer parameter cofseparatedBy_annulusRegion_of_gap`.

The count

dist(annulus n, annulus n') >= 1/2 * 3^(n-1) - 1/2 * 3^(n')     (coordinate gap)
1/2 * 3^(n-1) - 1/2 * 3^(n') >= sqrt d * 3^(n'-c)
                                        <== 3 + 2*3^(1-c)*sqrt d <= 3^(n-n')

so the atoms are r-dependent for every r >= 1 with 3 + 2*3^(1-c)*sqrt d <= 3 ^ r, i.e. for r(d) = max {2, ceil (log_3 (3 + 2*3^(1-c)*sqrt d))}.

The metric: Euclidean versus sup, and the honest constants

This repository's SeparatedBy is stated at the Euclidean Homogenization.Book.Ch02.vecNorm, because that is the spelling of Frozen.Assumptions.ShellLawJ1.range_dependence. The constants do not change. The lower bound used here is the single-coordinate bound |x i - y i| <= vecNorm (x - y), which is the sup-metric gap; and the gap is attained in the Euclidean metric as well (take x, y on a common coordinate axis), so no Euclidean improvement of 3 + 2*3^(1-c)*sqrt d is available from the annuli's geometry. The count is therefore identical to the sup-metric one, and it is sharp for this argument.

The dimension caveat

At the offset c = 2 of the G_0 lane, r = 2 requires 3 + (2/3) sqrt d <= 9, i.e. sqrt d <= 9, i.e. d <= 81. Beyond that dimension the count is not r = 2 but r(d) above, which separatedBy_annulusRegion_of_gap delivers at every r. This dimension caveat comes entirely from the sqrt d in the shells' range of dependence, which the manuscript's per-scale display drops.

Main definitions

• annulusRegion d n -- the closed sup-norm annulus {x : 1/2*3^(n-1) <= |x|_inf <= 1/2*3^n}, the region read by the per-scale atom at index n.

Main results

• separatedBy_of_coordinate_gap -- the workhorse: a coordinate gap between two regions is a SeparatedBy bound.
• separatedBy_annulusRegion_of_gap -- the r(d) count at a free truncation offset c.
• mem_annulusRegion_of_le_triadicLatticePoint -- the no-enlargement fact: a cube z + Box_j centred at a triadic lattice point z of the open annulus, with j <= n - 1, is still contained in annulusRegion d n. This is what makes the count above consumable with no fattening of the annuli.

Coordinate bounds for the Euclidean norm

theorem Algsuperdiff.Section4.Probability.vecNorm_sub_comm {d : ℕ} (x y : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.vecNorm (x - y) = HCPolySupport.Book.Ch02.vecNorm (y - x)

The Euclidean norm of a difference is symmetric.

theorem Algsuperdiff.Section4.Probability.SeparatedBy.symm {d : ℕ} {r : ℝ} {U V : Set (HCPolySupport.Vec d)} (h : SeparatedBy r U V) : SeparatedBy r V U

Separation is symmetric.

theorem Algsuperdiff.Section4.Probability.separatedBy_of_coordinate_gap {d : ℕ} {a b : ℝ} {U V : Set (HCPolySupport.Vec d)} (hU : ∀ x ∈ U, ∃ (i : Fin d), a ≤ |x i|) (hV : ∀ y ∈ V, ∀ (i : Fin d), |y i| ≤ b) : SeparatedBy (a - b) U V

Separation from a coordinate gap. If every point of U has some coordinate of size at least a, and every point of V has all coordinates of size at most b, then U and V are (a - b)-separated. The bound used is the sup-metric gap, which the Euclidean norm dominates.

The annulus

def Algsuperdiff.Section4.Probability.annulusRegion (d : ℕ) (n : ℤ) : Set (HCPolySupport.Vec d)

The annulus closure(Box_n) \ Box_{n-1} in the sup norm of Vec d: the region the per-scale atom at index n reads. It is written in coordinates, matching the coordinate definition of the triadic cubes.

Equations

• Algsuperdiff.Section4.Probability.annulusRegion d n = {x : HCPolySupport.Vec d | (∃ (i : Fin d), 1 / 2 * 3 ^ (n - 1) ≤ |x i|) ∧ ∀ (i : Fin d), |x i| ≤ 1 / 2 * 3 ^ n}

theorem Algsuperdiff.Section4.Probability.measurableSet_annulusRegion (d : ℕ) (n : ℤ) : MeasurableSet (annulusRegion d n)

The r(d) arithmetic

theorem Algsuperdiff.Section4.Probability.sqrt_mul_zpow_le_annulus_gap {d : ℕ} {c n n' : ℤ} (hgap : 3 + 2 * 3 ^ (1 - c) * √↑d ≤ 3 ^ (n - n')) : √↑d * 3 ^ (n' - c) ≤ 1 / 2 * 3 ^ (n - 1) - 1 / 2 * 3 ^ n'

The arithmetic core of the count. Under the gap condition 3 + 2*3^(1-c)*sqrt d <= 3^(n-n'), the annuli's coordinate gap 1/2*3^(n-1) - 1/2*3^(n') dominates the range of dependence sqrt d * 3^(n'-c) of the coarsest shared shell.

The separation of the annuli

theorem Algsuperdiff.Section4.Probability.separatedBy_annulusRegion_of_lt {d : ℕ} {c n n' : ℤ} (hlt : n' < n) (hgap : 3 + 2 * 3 ^ (1 - c) * √↑d ≤ 3 ^ (n - n')) : SeparatedBy (√↑d * 3 ^ min (n - c) (n' - c)) (annulusRegion d n) (annulusRegion d n')

The count, ordered form. For n' < n satisfying the gap condition, the annuli are separated at the shared-shell threshold sqrt d * 3 ^ (min (n - c) (n' - c)) -- exactly the threshold consumed by iIndepFun_of_local_cutoffSample at Lidx m = m - c.

theorem Algsuperdiff.Section4.Probability.separatedBy_annulusRegion_of_gap {d : ℕ} {c : ℤ} {r : ℕ} (hr1 : 1 ≤ r) (hr : 3 + 2 * 3 ^ (1 - c) * √↑d ≤ 3 ^ r) {n n' : ℤ} (hgap : ↑r ≤ |n - n'|) : SeparatedBy (√↑d * 3 ^ min (n - c) (n' - c)) (annulusRegion d n) (annulusRegion d n')

The r(d) count. If r >= 1 and 3 + 2*3^(1-c)*sqrt d <= 3^r, then annuli whose indices differ by at least r are separated at the shared-shell threshold sqrt d * 3 ^ (min (n - c) (n' - c)). This is the honest form of "the per-scale atoms are r-dependent", and it is exactly the hsep hypothesis of iIndepFun_of_local_cutoffSample at Lidx m = m - c.

The events' triadic geometry

theorem Algsuperdiff.Section4.Probability.mem_annulusRegion_of_le_triadicLatticePoint {d : ℕ} {j n : ℤ} (hj : j ≤ n - 1) {v : Fin d → ℤ} (hv : Support.triadicLatticePoint j v ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d n) \ HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 1))) {x : HCPolySupport.Vec d} (hx : ∀ (i : Fin d), |x i - Support.triadicLatticePoint j v i| ≤ 1 / 2 * 3 ^ j) : x ∈ annulusRegion d n

No enlargement of the annulus (the decisive geometric input). Let z be a triadic lattice point of spacing 3^j lying in the open annulus Box_n \ Box_{n-1}, with j <= n - 1. Then every point of the closed cube z + Box_j is still in annulusRegion d n: the read cubes of the per-scale atom tile the annulus and do not stick out of it.

This is the fact that lets separatedBy_annulusRegion_of_gap be applied to the regions the G_0 and G_2 atoms actually read, with no fattening (and hence no degradation of the d-range).