DescendantLattice

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

The descendant enumeration and the lattice enumeration are the same list

ABK26, Section 4.1 writes every per-scale maximum as a maximum over the lattice translates

max_{z in 3^n Z^d cap cu_m}  ( . )(z + cu_n) ,

while the proved (infinity,2) identity of d.mathcal.E runs its maximum over descendantsAtScale (cu_m) n, the triadic descendants of cu_m at scale n. This module proves that the two enumerate the same cubes, in both directions, and transfers maxima across the correspondence.

The arithmetic content

A triadic cube is a scale together with an integer index, and its point set is the translate of the origin cube of that scale by 3^scale * index. The descendants of cu_m at depth t are exactly the cubes of scale m - t whose index v satisfies the balanced-ternary box condition

2 |v_i| < 3^t     for every coordinate `i`,

which is proved here by induction on t from childCubes (each step multiplies the index by 3 and adds a balanced digit in {-1,0,1}; the reverse step divides by 3, where oddness of 3^t supplies the strict inequality). The lattice side 3^n Z^d cap cu_m -- i.e. Support.latticeCubeSet d n m -- unfolds to |3^n v_i| < 3^m / 2, the same condition with t = m - n. Hence the identification, with no geometric hypothesis beyond n <= m.

What is proved

• mem_descendantsAtDepth_iff -- the index-box characterization of descendants.
• mem_latticeCubeSet_iff -- the same box, read off the Section 4 lattice set.
• mem_descendantsAtScale_originCube_iff, latticeCube_mem_descendantsAtScale, eq_latticeCube_of_mem_descendantsAtScale -- the correspondence, both ways.
• latticeCubeFinset, descendantsAtScale_originCube_eq_image -- the index bijection of the descendant enumeration.
• maxDescendantNormalizedBlockResponse_le_of_lattice_bounds and eightEss_blockResponse_le_of_lattice_bounds -- the two targets joined: the scale-n descendant maximum of the normalized block response is bounded by the manuscript's two lattice maxima of the scalar J, at the field and at its transpose, with constant 1.

Integer bookkeeping

The index-box characterization of the descendants

theorem Algsuperdiff.Section4.Provider.Annular.mem_descendantsAtDepth_iff {d : ℕ} (Q R : HCPolySupport.TriadicCube d) (t : ℕ) : R ∈ HCPolySupport.descendantsAtDepth Q t ↔ R.scale = Q.scale - ↑t ∧ ∀ (i : Fin d), 2 * |R.index i - 3 ^ t * Q.index i| < 3 ^ t

The descendants of a triadic cube, in index coordinates. The depth-t descendants of Q are exactly the scale-(Q.scale - t) cubes whose index lies in the balanced box of radius 3^t / 2 around 3^t Q.index.

The lattice enumeration

def Algsuperdiff.Section4.Provider.Annular.latticeCube {d : ℕ} (n : ℤ) (v : Fin d → ℤ) : HCPolySupport.TriadicCube d

The scale-n triadic cube based at the lattice point 3^n v.

Equations

• Algsuperdiff.Section4.Provider.Annular.latticeCube n v = { scale := n, index := v }

@[simp]

theorem Algsuperdiff.Section4.Provider.Annular.latticeCube_scale {d : ℕ} (n : ℤ) (v : Fin d → ℤ) : (latticeCube n v).scale = n

@[simp]

theorem Algsuperdiff.Section4.Provider.Annular.latticeCube_index {d : ℕ} (n : ℤ) (v : Fin d → ℤ) : (latticeCube n v).index = v

theorem Algsuperdiff.Section4.Provider.Annular.latticeCube_index_self {d : ℕ} (R : HCPolySupport.TriadicCube d) : latticeCube R.scale R.index = R

theorem Algsuperdiff.Section4.Provider.Annular.mem_latticeCubeSet_iff {d : ℕ} {n m : ℤ} (hnm : n ≤ m) (v : Fin d → ℤ) : v ∈ Support.latticeCubeSet d n m ↔ ∀ (i : Fin d), 2 * |v i| < 3 ^ (m - n).toNat

3^n Z^d cap cu_m, in index coordinates. A scale-n lattice point lies in the open cube cu_m exactly when its index lies in the balanced box of radius 3^{m-n} / 2.

The correspondence

theorem Algsuperdiff.Section4.Provider.Annular.mem_descendantsAtScale_originCube_iff {d : ℕ} {n m : ℤ} (hnm : n ≤ m) (R : HCPolySupport.TriadicCube d) : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) n ↔ R.scale = n ∧ R.index ∈ Support.latticeCubeSet d n m

The descendants of cu_m at scale n are the lattice cubes of 3^n Z^d cap cu_m.

theorem Algsuperdiff.Section4.Provider.Annular.latticeCube_mem_descendantsAtScale {d : ℕ} {n m : ℤ} (hnm : n ≤ m) {v : Fin d → ℤ} (hv : v ∈ Support.latticeCubeSet d n m) : latticeCube n v ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) n

theorem Algsuperdiff.Section4.Provider.Annular.scale_eq_of_mem_descendantsAtScale_originCube {d : ℕ} {n m : ℤ} (hnm : n ≤ m) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) n) : R.scale = n

theorem Algsuperdiff.Section4.Provider.Annular.index_mem_latticeCubeSet_of_mem_descendantsAtScale {d : ℕ} {n m : ℤ} (hnm : n ≤ m) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) n) : R.index ∈ Support.latticeCubeSet d n m

theorem Algsuperdiff.Section4.Provider.Annular.eq_latticeCube_of_mem_descendantsAtScale {d : ℕ} {n m : ℤ} (hnm : n ≤ m) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) n) : R = latticeCube n R.index

Every descendant is the lattice cube at its own base point.

The index bijection and the transfer of maxima

def Algsuperdiff.Section4.Provider.Annular.latticeCubeFinset (d : ℕ) (n m : ℤ) : Finset (Fin d → ℤ)

The finite index set of 3^n Z^d cap cu_m.

Equations

• Algsuperdiff.Section4.Provider.Annular.latticeCubeFinset d n m = Finset.image HCPolySupport.TriadicCube.index (HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) n)

theorem Algsuperdiff.Section4.Provider.Annular.mem_latticeCubeFinset_iff {d : ℕ} {n m : ℤ} (hnm : n ≤ m) (v : Fin d → ℤ) : v ∈ latticeCubeFinset d n m ↔ v ∈ Support.latticeCubeSet d n m

theorem Algsuperdiff.Section4.Provider.Annular.descendantsAtScale_originCube_eq_image {d : ℕ} {n m : ℤ} (hnm : n ≤ m) : HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) n = Finset.image (latticeCube n) (latticeCubeFinset d n m)

The index bijection: the descendant family is the image of the lattice index set under v |-> 3^n v + cu_n.

theorem Algsuperdiff.Section4.Provider.Annular.latticeCube_injective {d : ℕ} (n : ℤ) : Function.Injective (latticeCube n)

theorem Algsuperdiff.Section4.Provider.Annular.latticeCubeFinset_card {d : ℕ} {n m : ℤ} (hnm : n ≤ m) : (latticeCubeFinset d n m).card = (3 ^ d) ^ (m - n).toNat

The lattice count #(3^n Z^d cap cu_m) = 3^{d(m-n)}, obtained from the descendant count through the index bijection.

The two targets joined

theorem Algsuperdiff.Section4.Provider.Annular.maxDescendantNormalizedBlockResponse_le_of_lattice_bounds {d : ℕ} [NeZero d] (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {n m : ℤ} (hnm : n ≤ m) (sigma : Section3.Observable.PositiveScalar) {Jf Jt : ℝ} (hfld : ∀ v ∈ Support.latticeCubeSet d n m, ∀ (e : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e = 1 → HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain (latticeCube n v)) (F.coeffOn (latticeCube n v)) (Section3.Observable.inverseSqrtLoad sigma e) (Section3.Observable.sqrtLoad sigma e) ≤ Jf) (htrn : ∀ v ∈ Support.latticeCubeSet d n m, ∀ (e : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e = 1 → HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain (latticeCube n v)) (F.coeffOn (latticeCube n v)).transpose (Section3.Observable.inverseSqrtLoad sigma e) (Section3.Observable.sqrtLoad sigma e) ≤ Jt) : HCPolySupport.Book.Ch02.maxDescendantNormalizedBlockResponseAtScale (HCPolySupport.originCube d m) n F (Section3.Observable.isotropicComparatorMatrix sigma) ≤ Jf + Jt

The e.bfJ.general conversion, at the manuscript's lattice enumeration (with the transpose remark).

The scale-n descendant maximum of the normalized block response -- the inner quantity of the (infinity,2) error at scale n -- is bounded by the sum of the two lattice maxima of the scalar response, one for the field and one for its transpose, over z in 3^n Z^d cap cu_m and unit loads.

theorem Algsuperdiff.Section4.Provider.Annular.eightEss_blockResponse_le_of_lattice_bounds {d : ℕ} [NeZero d] (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (sigma : Section3.Observable.PositiveScalar) {Jfld Jtrn : ℕ → ℝ} (hfld : ∀ (l : ℕ), ∀ v ∈ Support.latticeCubeSet d (m - ↑l) m, ∀ (e : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e = 1 → HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain (latticeCube (m - ↑l) v)) (F.coeffOn (latticeCube (m - ↑l) v)) (Section3.Observable.inverseSqrtLoad sigma e) (Section3.Observable.sqrtLoad sigma e) ≤ Jfld l) (htrn : ∀ (l : ℕ), ∀ v ∈ Support.latticeCubeSet d (m - ↑l) m, ∀ (e : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e = 1 → HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain (latticeCube (m - ↑l) v)) (F.coeffOn (latticeCube (m - ↑l) v)).transpose (Section3.Observable.inverseSqrtLoad sigma e) (Section3.Observable.sqrtLoad sigma e) ≤ Jtrn l) (l : ℕ) : HCPolySupport.Book.Ch02.maxDescendantNormalizedBlockResponseAtScale (HCPolySupport.originCube d m) (m - ↑l) F (Section3.Observable.isotropicComparatorMatrix sigma) ≤ 1 * (Jfld l + Jtrn l)

The same statement in the scale-sum indexing n = m - l of the (infinity,2) opening: this is exactly the hbfJ slot of the eight-ess display, at the constant 1.