Section 12.4: Binary localization and variation

This file was automatically generated by Claude.

Formalization of blueprint Section 12, "Curvature localization" (sec:localization), subsection 4, "Binary localization and variation" (lines 1837-1883) of blueprint/formalization_blueprint.tex.

Localization at one search leaf

def TrilinearHT.Auto.leafGroupOutput {V : Type u_1} [AddCommGroup V] [Module ℂ V] {γ : Type u_2} (L : γ → Fin 4 → V →ₗ[ℂ] V) (x : Fin 4 → V) (G : γ) : Fin 4 → V

The group output Z_{l,G} = L_{l,G} x_l in all four slots.

Equations

• TrilinearHT.Auto.leafGroupOutput L x G l = (L G l) (x l)

def TrilinearHT.Auto.leafResiduals {V : Type u_1} [AddCommGroup V] [Module ℂ V] {γ : Type u_2} (L : γ → Fin 4 → V →ₗ[ℂ] V) (x : Fin 4 → V) (u t p q : Fin 4) (G : γ) : Fin 3 → Fin 4 → V

The three residual insertions after fixing the group source L_{t,G} x_t in slot t: successively filter the slots u, p, q.

Equations

• One or more equations did not get rendered due to their size.
• TrilinearHT.Auto.leafResiduals L x u t p q G 0 = Function.update (Function.update x t ((L G t) (x t))) u (x u - (L G u) (x u))
• TrilinearHT.Auto.leafResiduals L x u t p q G 1 = Function.update (Function.update (Function.update x t ((L G t) (x t))) u ((L G u) (x u))) p (x p - (L G p) (x p))

theorem TrilinearHT.Auto.update_comm_apply {V : Type u_1} {u t : Fin 4} (h : u ≠ t) (x : Fin 4 → V) (a b : V) : Function.update (Function.update x u a) t b = Function.update (Function.update x t b) u a

theorem TrilinearHT.Auto.leaf_telescope {V : Type u_1} [AddCommGroup V] [Module ℂ V] (Λ : MultilinearMap ℂ (fun (x : Fin 4) => V) ℂ) {γ : Type u_2} (L : γ → Fin 4 → V →ₗ[ℂ] V) (x : Fin 4 → V) {u t p q : Fin 4} (hut : u ≠ t) (hup : u ≠ p) (huq : u ≠ q) (htp : t ≠ p) (htq : t ≠ q) (hpq : p ≠ q) (G : γ) : Λ (Function.update x t ((L G t) (x t))) = Λ (leafGroupOutput L x G) + ∑ i : Fin 3, Λ (leafResiduals L x u t p q G i)

The filter telescoping in the slots u, p, q with the group source fixed in slot t.

theorem TrilinearHT.Auto.leaf_identity {V : Type u_1} [AddCommGroup V] [Module ℂ V] (Λ : MultilinearMap ℂ (fun (x : Fin 4) => V) ℂ) {ι : Type u_2} {γ : Type u_3} (L : γ → Fin 4 → V →ₗ[ℂ] V) (x : Fin 4 → V) {u t p q : Fin 4} (hut : u ≠ t) (hup : u ≠ p) (huq : u ≠ q) (htp : t ≠ p) (htq : t ≠ q) (hpq : p ≠ q) (S : Finset ι) (a : ι → ℂ) (φ : ι → V) (hx : x u = ∑ v ∈ S, a v • φ v) (Gs : Finset γ) : Λ x = ∑ G ∈ Gs, Λ (leafGroupOutput L x G) + ∑ v ∈ S, a v * Λ (Function.update (Function.update x u (φ v)) t (x t - ∑ G ∈ Gs, (L G t) (x t))) + ∑ G ∈ Gs, ∑ i : Fin 3, Λ (leafResiduals L x u t p q G i)

Blueprint prop:localize, lines 1847-1850: the exact expansion at one leaf. The outer primal of slot u is expanded into sources; the sum of the first ball projections of the current groups is inserted in slot t; the remaining slots are filtered successively.

theorem TrilinearHT.Auto.leaf_localization {V : Type u_1} [AddCommGroup V] [Module ℂ V] (Λ : MultilinearMap ℂ (fun (x : Fin 4) => V) ℂ) {ι : Type u_2} {γ : Type u_3} (L : γ → Fin 4 → V →ₗ[ℂ] V) (x : Fin 4 → V) {u t p q : Fin 4} (hut : u ≠ t) (hup : u ≠ p) (huq : u ≠ q) (htp : t ≠ p) (htq : t ≠ q) (hpq : p ≠ q) (S : Finset ι) (a : ι → ℂ) (φ : ι → V) (hx : x u = ∑ v ∈ S, a v • φ v) (Gs : Finset γ) (grp : ι → Option γ) {εo εm εs εr : ℝ} (hold : ∀ v ∈ S, grp v = none → ‖Λ (Function.update (Function.update x u (φ v)) t (x t))‖ ≤ εo ∧ ∀ G ∈ Gs, ‖Λ (Function.update (Function.update x u (φ v)) t ((L G t) (x t)))‖ ≤ εo) (hcur : ∀ v ∈ S, ∀ (G₀ : γ), grp v = some G₀ → G₀ ∈ Gs ∧ ‖Λ (Function.update (Function.update x u (φ v)) t (x t - (L G₀ t) (x t)))‖ ≤ εm ∧ ∀ G ∈ Gs, G ≠ G₀ → ‖Λ (Function.update (Function.update x u (φ v)) t ((L G t) (x t)))‖ ≤ εs) (hres : ∀ G ∈ Gs, ∀ (i : Fin 3), ‖Λ (leafResiduals L x u t p q G i)‖ ≤ εr) (hεo : 0 ≤ εo) (hεm : 0 ≤ εm) (hεs : 0 ≤ εs) : ‖Λ x - ∑ G ∈ Gs, Λ (leafGroupOutput L x G)‖ ≤ (∑ v ∈ S, ‖a v‖) * ((↑Gs.card + 1) * εo + εm + ↑Gs.card * εs) + ↑Gs.card * (3 * εr)

Blueprint prop:localize, lines 1847-1852: the error at one leaf. Old sources are killed by the lower guard (εo); a current source of group G₀ has the matching difference controlled by the catalog test (εm) and pair separation from the other groups (εs); the residual insertions against the fixed group source are tested (εr).

The current-group decomposition (prop:localize)

theorem TrilinearHT.Auto.min_finset_subadd {σ : Type u_1} (s : Finset σ) {η : ℝ} (hη : 0 ≤ η) (f : σ → ℝ) (hf : ∀ j ∈ s, 0 ≤ f j) : min η (∑ j ∈ s, f j) ≤ ∑ j ∈ s, min η (f j)

eq:min-subadd for finite sums of nonnegative numbers.

theorem TrilinearHT.Auto.cell_min_leaves {ιc : Type u_1} {σ : Type u_2} (cells : Finset ιc) (wt : ιc → ℝ) (hwt : ∀ (I : ιc), 0 ≤ wt I) {η : ℝ} (hη : 0 ≤ η) (Hval : ιc → ℂ) (leaves : Finset σ) (Hleaf : ιc → σ → ℂ) (hsplit : ∀ I ∈ cells, Hval I = ∑ s ∈ leaves, Hleaf I s) (Mn : ιc → σ → ℂ) (ε : ιc → σ → ℝ) (hleaf : ∀ I ∈ cells, ∀ s ∈ leaves, ‖Hleaf I s - Mn I s‖ ≤ ε I s) : ∑ I ∈ cells, wt I * min η ‖Hval I‖ ≤ ∑ s ∈ leaves, ∑ I ∈ cells, wt I * min η ‖Mn I s‖ + ∑ I ∈ cells, wt I * ∑ s ∈ leaves, ε I s

The cell minima distribute over the leaves (blueprint line 1858, via eq:min-subadd).

Certified variation (lem:variation)

theorem TrilinearHT.Auto.synthesis_le_of_bessel' {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] {κ : Type u_3} (s : Finset κ) (R : κ → H →L[ℂ] F) {c : ℝ} (hc : 0 ≤ c) (hB : ∀ (h : H), ∑ k ∈ s, ‖(R k) h‖ ^ 2 ≤ c * ‖h‖ ^ 2) (x : κ → F) : ‖∑ k ∈ s, (ContinuousLinearMap.adjoint (R k)) (x k)‖ ^ 2 ≤ c * ∑ k ∈ s, ‖x k‖ ^ 2

Synthesis bound dual to a Bessel row family into a second Hilbert space.

theorem TrilinearHT.Auto.synthesis_le_of_bessel {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {κ : Type u_2} (s : Finset κ) (R : κ → H →L[ℂ] H) {c : ℝ} (hc : 0 ≤ c) (hB : ∀ (h : H), ∑ k ∈ s, ‖(R k) h‖ ^ 2 ≤ c * ‖h‖ ^ 2) (x : κ → H) : ‖∑ k ∈ s, (ContinuousLinearMap.adjoint (R k)) (x k)‖ ^ 2 ≤ c * ∑ k ∈ s, ‖x k‖ ^ 2

Synthesis bound dual to a Bessel row family.

theorem TrilinearHT.Auto.joint_bessel_of_wholeRanges {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {γ : Type u_2} {κ : Type u_3} [Fintype γ] [DecidableEq γ] (s : Finset κ) (grp : κ → γ) (R : κ → H →L[ℂ] H) (hgrp : ∀ (G : γ) (h : H), ∑ k ∈ s with grp k = G, ‖(R k) h‖ ^ 2 ≤ ‖h‖ ^ 2) {C : ℝ} (hC : 0 ≤ C) (hwr : ∀ (x : κ → H), ‖∑ k ∈ s, (ContinuousLinearMap.adjoint (R k)) (x k)‖ ^ 2 ≤ C * ∑ G : γ, ‖∑ k ∈ s with grp k = G, (ContinuousLinearMap.adjoint (R k)) (x k)‖ ^ 2) (h : H) : ∑ k ∈ s, ‖(R k) h‖ ^ 2 ≤ C * ‖h‖ ^ 2

Blueprint lem:variation, line 1867: rows that are Bessel within each group and whose adjoint outputs over the groups satisfy the almost-orthogonality eq:whole-ranges (‖Σ_G Z_G‖² ≤ C Σ_G ‖Z_G‖²) are jointly Bessel with constant C.

theorem TrilinearHT.Auto.sum_filter_fst {γ : Type u_2} {ι : Type u_3} [Fintype γ] [Fintype ι] [DecidableEq γ] (f : γ × ι → ℝ) (G : γ) : ∑ k : γ × ι with k.1 = G, f k = ∑ i : ι, f (G, i)

theorem TrilinearHT.Auto.ColorSetup.cumMask_mono {V : Type u_1} [DecidableEq V] {K : ColorSetup V} {T : AdmTree V} {Nv m m' h h' : ℕ} (hm : m ≤ m') (hh : h ≤ h') (I : T.Cell) : K.cumMask T Nv m h I ⊆ K.cumMask T Nv m' h' I

theorem TrilinearHT.Auto.ColorSetup.cumMask_succ {V : Type u_1} [DecidableEq V] {K : ColorSetup V} {T : AdmTree V} {Nv m h : ℕ} {I : T.Cell} {b : V} (hb : b ∈ K.cumMask T Nv (m + 1) h I) : b ∈ K.cumMask T Nv m h I ∨ ∃ w ∈ T.X I, K.color T Nv I w = m + 1 ∧ K.dist.d (T.depth I) w b ≤ ↑h

A vertex of the cumulative mask at m + 1 is old (in the mask at m) or within the pad of a vertex of color exactly m + 1 (blueprint line 1850).

def TrilinearHT.Auto.thirdSlot (up : Fin 4) (low : Option (Fin 4)) : Fin 4

The third slot: the least slot that is not a current guard.

Equations

• TrilinearHT.Auto.thirdSlot up low = if 0 ≠ up ∧ low ≠ some 0 then 0 else if 1 ≠ up ∧ low ≠ some 1 then 1 else if 2 ≠ up ∧ low ≠ some 2 then 2 else 3

structure TrilinearHT.Auto.SearchLeaf : Type

A leaf of the search: its color, its guards and the layers of each slot.

• k : ℕ

  Current lower color bound of the binary-search leaf.

• hi : ℕ

  Current upper color bound of the binary-search leaf.

• up : Fin 4

  Distinguished upper-guard slot of the search leaf.

• low : Option (Fin 4)

  Optional lower-guard slot of the search leaf.

• layers : Fin 4 → List (ℕ × Bool)

  Rank and branch choices accumulated by the filters in each slot.

def TrilinearHT.Auto.searchLeaves : ℕ → ℕ → ℕ → Fin 4 → Option (Fin 4) → (Fin 4 → List (ℕ × Bool)) → List SearchLeaf

The guarded binary search over the colors [ℓ, h] (blueprint lines 1848-1849): split at m = ⌊(ℓ+h)/2⌋ with the cumulative filter of the third slot; the positive branch makes it the upper guard with [ℓ, m], the residual branch the lower guard with [m+1, h].

Equations

• One or more equations did not get rendered due to their size.
• TrilinearHT.Auto.searchLeaves 0 x✝⁴ x✝³ x✝² x✝¹ x✝ = [{ k := x✝⁴, hi := x✝³, up := x✝², low := x✝¹, layers := x✝ }]

theorem TrilinearHT.Auto.searchLeaves_form {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (Λ : MultilinearMap ℂ (fun (x : Fin 4) => H) ℂ) (Cum : Fin 4 → ℕ → H →L[ℂ] H) (z : Fin 4 → H) (fuel ℓ h : ℕ) (up : Fin 4) (low : Option (Fin 4)) (ls : Fin 4 → List (ℕ × Bool)) : (Λ fun (l : Fin 4) => (layerOp (Cum l) (ls l)) (z l)) = (List.map (fun (L : SearchLeaf) => Λ fun (l : Fin 4) => (layerOp (Cum l) (L.layers l)) (z l)) (searchLeaves fuel ℓ h up low ls)).sum

Blueprint prop:localize, lines 1841-1843: the search is an exact expansion over its leaves.

def TrilinearHT.Auto.SearchInv (up₀ : Fin 4) (ℓ₀ h₀ ℓ h : ℕ) (up : Fin 4) (low : Option (Fin 4)) (ls : Fin 4 → List (ℕ × Bool)) : Prop

The guard invariant (blueprint line 1848): the upper guard ends with the positive filter at the upper end of the interval (or is the initial basic slot with no filter at the top color), the lower guard ends with the residual filter just below the lower end (or there is none at the bottom color), and the guards differ.

Equations

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

Expansion of averaged catalog filters (blueprint lines 1850, 1835)

Contractions

theorem TrilinearHT.Auto.norm_opAvg_apply_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {P : ℕ} (Q : Fin P → H →L[ℂ] H) (hQ : ∀ (p : Fin P) (x : H), ‖(Q p) x‖ ≤ ‖x‖) (x : H) : ‖(opAvg Q) x‖ ≤ ‖x‖

theorem TrilinearHT.Auto.norm_id_sub_opAvg_apply_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {P : ℕ} (hP : 0 < P) (Q : Fin P → H →L[ℂ] H) (hQ : ∀ (p : Fin P) (x : H), ‖x - (Q p) x‖ ≤ ‖x‖) (x : H) : ‖(ContinuousLinearMap.id ℂ H - opAvg Q) x‖ ≤ ‖x‖

theorem TrilinearHT.Auto.norm_layerOp_apply_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (Cum : ℕ → H →L[ℂ] H) (h1 : ∀ (m : ℕ) (x : H), ‖(Cum m) x‖ ≤ ‖x‖) (h2 : ∀ (m : ℕ) (x : H), ‖(ContinuousLinearMap.id ℂ H - Cum m) x‖ ≤ ‖x‖) (ls : List (ℕ × Bool)) (x : H) : ‖(layerOp Cum ls) x‖ ≤ ‖x‖

A layered product of contractions whose complements are contractions is a contraction.

def TrilinearHT.Auto.dfltLeaf : SearchLeaf

A default search leaf.

Equations

• TrilinearHT.Auto.dfltLeaf = { k := 0, hi := 0, up := 0, low := none, layers := fun (x : Fin 4) => [] }

def TrilinearHT.Auto.searchList (fuel Lc : ℕ) (up₀ : Fin 4) : List SearchLeaf

The leaves of the guarded search over the colors [1, Lc] from the basic guard up₀.

Equations

• TrilinearHT.Auto.searchList fuel Lc up₀ = TrilinearHT.Auto.searchLeaves fuel 1 Lc up₀ none fun (x : Fin 4) => []

def TrilinearHT.Auto.leafAt (fuel Lc : ℕ) (up₀ : Fin 4) (s : ℕ) : SearchLeaf

The s-th leaf.

Equations

• TrilinearHT.Auto.leafAt fuel Lc up₀ s = (TrilinearHT.Auto.searchList fuel Lc up₀).getD s TrilinearHT.Auto.dfltLeaf

theorem TrilinearHT.Auto.list_sum_map_eq_sum_range {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (f : α → M) (d : α) (l : List α) : (List.map f l).sum = ∑ s ∈ Finset.range l.length, f (l.getD s d)

theorem TrilinearHT.Auto.search_cell_min {ιc : Type u_1} (cells : Finset ιc) (wt : ιc → ℝ) (hwt : ∀ (I : ιc), 0 ≤ wt I) {η : ℝ} (hη : 0 ≤ η) {V : ιc → Type u_2} [(I : ιc) → NormedAddCommGroup (V I)] [(I : ιc) → InnerProductSpace ℂ (V I)] (Λ : (I : ιc) → MultilinearMap ℂ (fun (x : Fin 4) => V I) ℂ) (Cum : (I : ιc) → Fin 4 → ℕ → V I →L[ℂ] V I) (z : (I : ιc) → Fin 4 → V I) (fuel Lc : ℕ) (up₀ : Fin 4) (Main : ιc → ℕ → ℂ) (err : ιc → ℕ → ℝ) (hleaf : ∀ I ∈ cells, ∀ s ∈ Finset.range (searchList fuel Lc up₀).length, ‖((Λ I) fun (l : Fin 4) => (layerOp (Cum I l) ((leafAt fuel Lc up₀ s).layers l)) (z I l)) - Main I s‖ ≤ err I s) : ∑ I ∈ cells, wt I * min η ‖(Λ I) (z I)‖ ≤ ∑ s ∈ Finset.range (searchList fuel Lc up₀).length, ∑ I ∈ cells, wt I * min η ‖Main I s‖ + ∑ I ∈ cells, wt I * ∑ s ∈ Finset.range (searchList fuel Lc up₀).length, err I s

Blueprint prop:localize (lines 1838-1856), summed over cells: with the guarded color search (the same leaves on every cell), the weighted cell minima are at most the weighted minima of the leaf main terms plus the weighted leaf errors.

theorem TrilinearHT.Auto.memLp_cell_indicator {G : RealDyadicGrid} {I : ℤ × ℤ} {f : ℝ → ℂ} (hf : MeasureTheory.MemLp f 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))) : MeasureTheory.MemLp ((dyadicGridCell G I.1 I.2).indicator f) 2 MeasureTheory.volume

theorem TrilinearHT.Auto.cellLp_ae {G : RealDyadicGrid} {I : ℤ × ℤ} {f : ℝ → ℂ} (hf : MeasureTheory.MemLp f 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))) : ↑↑(cellLp G I f) =ᵐ[MeasureTheory.volume] (dyadicGridCell G I.1 I.2).indicator f

Mask facts of an attempt (blueprint lem:masks, lines 1760-1762)

Roles at a leaf

def TrilinearHT.Auto.otherTwo (u t : Fin 4) : Fin 4 × Fin 4

The two slots other than u and t, in increasing order.

Equations

• TrilinearHT.Auto.otherTwo u t = if 0 ≠ u ∧ 0 ≠ t then (0, if 1 ≠ u ∧ 1 ≠ t then 1 else if 2 ≠ u ∧ 2 ≠ t then 2 else 3) else if 1 ≠ u ∧ 1 ≠ t then (1, if 2 ≠ u ∧ 2 ≠ t then 2 else 3) else (2, 3)

def TrilinearHT.Auto.SearchLeaf.role (L : SearchLeaf) (l : Fin 4) : ℕ

The role level of a slot at a leaf: the third slot t carries the first ball level, the upper guard the second, the two remaining slots the third and fourth (blueprint line 1853).

Equations

• L.role l = if l = TrilinearHT.Auto.thirdSlot L.up L.low then 1 else if l = L.up then 2 else if l = (TrilinearHT.Auto.otherTwo L.up (TrilinearHT.Auto.thirdSlot L.up L.low)).1 then 3 else 4

theorem TrilinearHT.Auto.ActiveSetup.Dg_sep {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (H τ : ℝ) : Real.exp 2 ≤ H → 0 < τ → τ ≤ 1 → ∀ (v w : ChartTag) {a i k b : Fin 4}, a ≠ i → a ≠ k → a ≠ b → i ≠ k → i ≠ b → k ≠ b → 1 ≤ v.dim → 1 ≤ w.dim → ∀ (B : QuadraticChartData v.dim) (B' : QuadraticChartData w.dim), QuadraticChartComplexity (A.csrc + 1) H B → QuadraticChartComplexity (A.csrc + 1) H B' → IsBoundedQuadraticChart B → IsBoundedQuadraticChart B' → B.horizontal = v.θ → B.matrix = ↑(slotCoeff i) • v.C → B.quadratic = ↑(slotCoeff i) * v.lam → B'.horizontal = w.θ → B'.matrix = ↑(slotCoeff k) • w.C → B'.quadratic = ↑(slotCoeff k) * w.lam → ∀ {a₀ r : ℝ}, 0 < r → ∀ {wI : ℝ × ℝ → ℂ}, IsAdmissibleLocalKernel κ a₀ r wI → ¬tagEdge (Real.exp (↑A.Dg * (1 + Real.log H + Real.log τ⁻¹) ^ A.Dg)) r v w → PairSmall a₀ r wI i k (quadraticChartAtom B) (quadraticChartAtom B') τ

The distinct-slot separation of the declaration graph at the common source order.

One leaf of an attempt at one cell (blueprint prop:localize, lines 1848-1856)

theorem TrilinearHT.Auto.fin4_fourth (u t g : Fin 4) : u ≠ t → g ≠ u → g ≠ t → ∃ (b : Fin 4), b ≠ u ∧ b ≠ t ∧ g ≠ b

theorem TrilinearHT.Auto.columnL2Restriction_eq_self {V : Type u_1} [Fintype V] (s : Set ℝ) (hs : MeasurableSet s) (v : ↥(ColumnL2 V)) (hv : ∀ᵐ (y : ℝ), y ∉ s → ↑↑v y = 0) : (columnL2Restriction s hs) v = v

Restriction fixes vectors that vanish off the restriction set.

theorem TrilinearHT.Auto.columnL2Restriction_comp_of_subset {V : Type u_1} [Fintype V] {s t : Set ℝ} (hs : MeasurableSet s) (ht : MeasurableSet t) (hst : s ⊆ t) : columnL2Restriction s hs ∘SL columnL2Restriction t ht = columnL2Restriction s hs

Block structure of depth projections and compression of global histories

theorem TrilinearHT.Auto.columnL2Restriction_adjoint {V : Type u_1} [Fintype V] (s : Set ℝ) (hs : MeasurableSet s) : ContinuousLinearMap.adjoint (columnL2Restriction s hs) = columnL2Restriction s hs

theorem TrilinearHT.Auto.cellColumnProjection_adjoint {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) : ContinuousLinearMap.adjoint (cellColumnProjection D A hc) = cellColumnProjection D A hc

theorem TrilinearHT.Auto.cellColumnProjection_restrict {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) : columnL2Restriction (dyadicGridCell D.grid c.1 c.2) ⋯ ∘SL cellColumnProjection D A hc = cellColumnProjection D A hc ∧ cellColumnProjection D A hc ∘SL columnL2Restriction (dyadicGridCell D.grid c.1 c.2) ⋯ = cellColumnProjection D A hc

Cell projections are local to their cell on both sides.

theorem TrilinearHT.Auto.columnL2Restriction_comp_disjoint {V : Type u_1} [Fintype V] {s t : Set ℝ} (hs : MeasurableSet s) (ht : MeasurableSet t) (hst : Disjoint s t) : columnL2Restriction s hs ∘SL columnL2Restriction t ht = 0

theorem TrilinearHT.Auto.columnL2Restriction_comp_of_subset' {V : Type u_1} [Fintype V] {s t : Set ℝ} (hs : MeasurableSet s) (ht : MeasurableSet t) (hst : s ⊆ t) : columnL2Restriction t ht ∘SL columnL2Restriction s hs = columnL2Restriction s hs

theorem TrilinearHT.Auto.norm_sub_starProjection_le {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (P : E →L[ℂ] E) (hP : IsStarProjection P) (x : E) : ‖x - P x‖ ≤ ‖x‖

Fixed stacks for the attempt histories (eq:stack-energy, blueprint lines 2394-2423)

theorem TrilinearHT.Auto.globHist_norm_le {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) {P : ℕ} (hP : 0 < P) (Am : ℕ → Fin P → InheritedColumnMask Ψ.D) (ls : List (ℕ × Bool)) (h : ℤ) (z : ↥(ColumnL2 V)) : ‖(globHist Ψ Am ls h) z‖ ≤ ‖z‖

theorem TrilinearHT.Auto.cellColumnProjection_commute_restrict {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) {s : Set ℝ} (hs : MeasurableSet s) (h : dyadicGridCell D.grid c.1 c.2 ⊆ s ∨ Disjoint (dyadicGridCell D.grid c.1 c.2) s) : columnL2Restriction s hs ∘SL cellColumnProjection D A hc = cellColumnProjection D A hc ∘SL columnL2Restriction s hs

A cell projection commutes with the restriction to a cell containing it or disjoint from it.

theorem TrilinearHT.Auto.ColumnDepthFamily.proj_commute_restrict {V : Type u_1} [Fintype V] (Φ : ColumnDepthFamily V) (h : ℤ) {Q : ℤ × ℤ} (hQ : Q.1 ≤ Φ.depth h) : columnL2Restriction (dyadicGridCell Φ.D.grid Q.1 Q.2) ⋯ ∘SL Φ.proj h = Φ.proj h ∘SL columnL2Restriction (dyadicGridCell Φ.D.grid Q.1 Q.2) ⋯

The depth projections of a column family commute with the restriction to any dyadic cell of depth at most the partition depth (blueprint lines 1879-1890: histories are local).

The objects of one search leaf (blueprint lines 2838, 1959-1962)

Leaf outputs of basic slots as global outputs (blueprint lines 1611, 2159-2162)

Cell values of the transfer steps as restrictions of global values (lines 2386-2391)

theorem TrilinearHT.Auto.searchLeaves_layers_length_le (fuel ℓ h : ℕ) (up : Fin 4) (low : Option (Fin 4)) (ls : Fin 4 → List (ℕ × Bool)) (L : SearchLeaf) : L ∈ searchLeaves fuel ℓ h up low ls → ∀ (l : Fin 4), (L.layers l).length ≤ (ls l).length + fuel

Each search step appends at most one layer to one slot: the layer lists of the leaves of a search with fuel f are at most f longer than the initial ones.

theorem TrilinearHT.Auto.leafAt_layers_length_le (fuel Lc : ℕ) (up₀ : Fin 4) (s : ℕ) (l : Fin 4) : ((leafAt fuel Lc up₀ s).layers l).length ≤ fuel

Blueprint lines 1841-1849 with the fuel ⌈log₂ L⌉ + 1 of the attempt: the leaf layer lists have length at most the fuel, logarithmic in the number of colors.

Current-group decomposition on the main columns (blueprint prop:localize, lines 1838-1856)

theorem TrilinearHT.Auto.localProgressionForm_congr_support {r : ℝ} {k : ℝ × ℝ → ℂ} {f f' : Fin 4 → ℝ → ℂ} (h : ∀ (z : ℝ × ℝ), k z ≠ 0 → ∀ (j : Fin 4), f j (realProgressionCoordinate j z) = f' j (realProgressionCoordinate j z)) : localProgressionForm r k f = localProgressionForm r k f'

A local form only sees its inputs on the progression coordinates of the kernel support.

theorem TrilinearHT.Auto.cellForm_apply {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {V : Type u_1} [Fintype V] (x : Fin 4 → ↥(ColumnL2 V)) : (cellForm hr hw V) x = localProgressionForm r w fun (l : Fin 4) => augPhys (x l)

theorem TrilinearHT.Auto.localProgressionForm_smul (r : ℝ) (w : ℝ × ℝ → ℂ) (f : Fin 4 → ℝ → ℂ) (c : Fin 4 → ℂ) : (localProgressionForm r w fun (j : Fin 4) => c j • f j) = (∏ j : Fin 4, c j) * localProgressionForm r w f

The local form is multilinear: scaling the inputs scales the form by the product.

Applying a passing test (blueprint eq:catalog-test with spectators)

theorem TrilinearHT.Auto.localProgressionForm_congr_cell {κ : LocalKernelClass} {G : RealDyadicGrid} {I : ℤ × ℤ} {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) w) {f g : Fin 4 → ℝ → ℂ} (h : ∀ (j : Fin 4), ∀ᵐ (y : ℝ), y ∈ dyadicGridCell G I.1 I.2 → f j y = g j y) : localProgressionForm (dyadicGridLength G I.1) w f = localProgressionForm (dyadicGridLength G I.1) w g

An admissible local form only sees its inputs on the cell.

theorem TrilinearHT.Auto.fin4_cover_of_distinct (u t a b l : Fin 4) : u ≠ t → u ≠ a → u ≠ b → t ≠ a → t ≠ b → a ≠ b → l = u ∨ l = t ∨ l = a ∨ l = b

theorem TrilinearHT.Auto.thirdSlot_ne (up : Fin 4) (low : Option (Fin 4)) : thirdSlot up low ≠ up ∧ low ≠ some (thirdSlot up low)

theorem TrilinearHT.Auto.searchLeaves_inv {up₀ : Fin 4} {ℓ₀ h₀ : ℕ} (fuel ℓ h : ℕ) (up : Fin 4) (low : Option (Fin 4)) (ls : Fin 4 → List (ℕ × Bool)) : SearchInv up₀ ℓ₀ h₀ ℓ h up low ls → ∀ L ∈ searchLeaves fuel ℓ h up low ls, SearchInv up₀ ℓ₀ h₀ L.k L.hi L.up L.low L.layers

Spectator sizes and pair separation at a leaf

theorem TrilinearHT.Auto.augPhys_normalized_le {V : Type u_1} [Fintype V] (G : RealDyadicGrid) (I : ℤ × ℤ) (x : ↥(ColumnL2 V)) : MeasureTheory.eLpNorm (augPhys x) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1)) ≤ ENNReal.ofReal (‖x‖ / √(dyadicGridLength G I.1))

The normalized size of the physical part of an augmented vector on a cell is at most ‖x‖ / √|I|.

theorem TrilinearHT.Auto.cellForm_pair_le {G : RealDyadicGrid} {I : ℤ × ℤ} {κ : LocalKernelClass} {wI : ℝ × ℝ → ℂ} (hwI : IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) wI) {V : Type u_1} [Fintype V] {u t a b : Fin 4} (hut : u ≠ t) (hua : u ≠ a) (hub : u ≠ b) (hta : t ≠ a) (htb : t ≠ b) (hab : a ≠ b) {ι : Type u_2} (F : Finset ι) (c : ι → ℂ) (col : ι → ↥(ColumnL2 V)) (Y : ι → ℝ → ℂ) (hcol : ∀ m ∈ F, ∀ᵐ (y : ℝ), y ∈ dyadicGridCell G I.1 I.2 → augPhys (col m) y = Y m y) (Xs : ℝ → ℂ) {τ₂ : ℝ} (hsep : ∀ m ∈ F, PairSmall (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) wI u t Xs (Y m) τ₂) (X : Fin 4 → ↥(ColumnL2 V)) (hXu : ∀ᵐ (y : ℝ), y ∈ dyadicGridCell G I.1 I.2 → augPhys (X u) y = Xs y) (hXt : X t = ∑ m ∈ F, c m • col m) {Sa Sb : ℝ} (hSa : 0 < Sa) (hSb : 0 < Sb) (hXa : MeasureTheory.eLpNorm (augPhys (X a)) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1)) ≤ ENNReal.ofReal Sa) (hXb : MeasureTheory.eLpNorm (augPhys (X b)) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1)) ≤ ENNReal.ofReal Sb) : ‖(cellForm ⋯ hwI V) X‖ ≤ τ₂ * Sa * Sb * ∑ m ∈ F, ‖c m‖

Pair separation at a leaf (blueprint line 1852): a pure source in slot u against a combination of pure columns in slot t, each pair separated in the sense of PairSmall, with two spectators of normalized sizes S_a, S_b.

theorem TrilinearHT.Auto.otherTwo_spec (u t : Fin 4) (h : u ≠ t) : (otherTwo u t).1 ≠ u ∧ (otherTwo u t).1 ≠ t ∧ (otherTwo u t).2 ≠ u ∧ (otherTwo u t).2 ≠ t ∧ (otherTwo u t).1 ≠ (otherTwo u t).2

theorem TrilinearHT.Auto.SearchLeaf.role_t (L : SearchLeaf) : L.role (thirdSlot L.up L.low) = 1

theorem TrilinearHT.Auto.SearchLeaf.role_ge (L : SearchLeaf) {l : Fin 4} (hl : l ≠ thirdSlot L.up L.low) : 2 ≤ L.role l

theorem TrilinearHT.Auto.SearchLeaf.role_le (L : SearchLeaf) (l : Fin 4) : L.role l ≤ 4

theorem TrilinearHT.Auto.searchLeaves_layers_length (fuel ℓ h : ℕ) (up : Fin 4) (low : Option (Fin 4)) (ls : Fin 4 → List (ℕ × Bool)) (L : SearchLeaf) : L ∈ searchLeaves fuel ℓ h up low ls → ∀ (l : Fin 4), (L.layers l).length ≤ (ls l).length + fuel

Each split adds one layer to one slot, so the layers grow by at most the search depth.

theorem TrilinearHT.Auto.leafAt_mem {fuel Lc : ℕ} {up₀ : Fin 4} {s : ℕ} (hs : s < (searchList fuel Lc up₀).length) : leafAt fuel Lc up₀ s ∈ searchList fuel Lc up₀

theorem TrilinearHT.Auto.searchLeaves_range (fuel ℓ h : ℕ) (up : Fin 4) (low : Option (Fin 4)) (ls : Fin 4 → List (ℕ × Bool)) : ℓ ≤ h → h - ℓ < 2 ^ fuel → ∀ L ∈ searchLeaves fuel ℓ h up low ls, L.k = L.hi ∧ ℓ ≤ L.k ∧ L.hi ≤ h

With enough fuel every leaf of the search has a single color k = hi in the initial range.

theorem TrilinearHT.Auto.searchList_inv (fuel Lc : ℕ) (up₀ : Fin 4) (L : SearchLeaf) : L ∈ searchList fuel Lc up₀ → SearchInv up₀ 1 Lc L.k L.hi L.up L.low L.layers

theorem TrilinearHT.Auto.leafAt_facts {fuel Lc : ℕ} {up₀ : Fin 4} (hL1 : 1 ≤ Lc) (hfuel : Lc - 1 < 2 ^ fuel) {s : ℕ} (hs : s < (searchList fuel Lc up₀).length) : (leafAt fuel Lc up₀ s).k = (leafAt fuel Lc up₀ s).hi ∧ 1 ≤ (leafAt fuel Lc up₀ s).k ∧ (leafAt fuel Lc up₀ s).k ≤ Lc ∧ SearchInv up₀ 1 Lc (leafAt fuel Lc up₀ s).k (leafAt fuel Lc up₀ s).hi (leafAt fuel Lc up₀ s).up (leafAt fuel Lc up₀ s).low (leafAt fuel Lc up₀ s).layers

The leaves of a complete search over [1, Lc]: a single color k ∈ [1, Lc] and the search invariant.

theorem TrilinearHT.Auto.searchLeaves_length_le (fuel ℓ h : ℕ) (up : Fin 4) (low : Option (Fin 4)) (ls : Fin 4 → List (ℕ × Bool)) : (searchLeaves fuel ℓ h up low ls).length ≤ 2 ^ fuel

The guarded binary search has at most 2^fuel leaves.

Applying a passing residual (blueprint eq:catalog-test with spectators)

theorem TrilinearHT.Auto.ResidOK.mono {W : Type u_1} [Fintype W] {Tg : Type u_2} {G : RealDyadicGrid} {I : ℤ × ℤ} {c₀ : ℕ} {H : ℝ} {tagOf : Tg → ChartTag} {wI : ℝ × ℝ → ℂ} {t : Fin 4} {M M' : Tg → Prop} {R : ↥(ColumnL2 W)} {β β' : ℝ} (h : ResidOK G I c₀ H tagOf wI t M R β) (hM : ∀ (x : Tg), M' x → M x) (hβ : β ≤ β') : ResidOK G I c₀ H tagOf wI t M' R β'

A passing residual passes for smaller masks and larger levels.

theorem TrilinearHT.Auto.ResidOK.form_le {W : Type u_1} [Fintype W] {κ : LocalKernelClass} {Tg : Type u_2} {G : RealDyadicGrid} {I : ℤ × ℤ} {c₀ : ℕ} {H : ℝ} {tagOf : Tg → ChartTag} {wI : ℝ × ℝ → ℂ} (hwI : IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) wI) {t : Fin 4} {M : Tg → Prop} {R : ↥(ColumnL2 W)} {β : ℝ} (h : ResidOK G I c₀ H tagOf wI t M R β) {x : Tg} (hx : M x) {u a b : Fin 4} (hut : u ≠ t) (hua : u ≠ a) (hub : u ≠ b) (hta : t ≠ a) (htb : t ≠ b) (hab : a ≠ b) (A : QuadraticChartData (tagOf x).dim) (hA : QuadraticChartComplexity c₀ H A) (hAθ : A.horizontal = (tagOf x).θ) (hAM : A.matrix = ↑(slotCoeff u) • (tagOf x).C) (hAq : A.quadratic = ↑(slotCoeff u) * (tagOf x).lam) (X : Fin 4 → ↥(ColumnL2 W)) (hXu : ∀ᵐ (y : ℝ), y ∈ dyadicGridCell G I.1 I.2 → augPhys (X u) y = quadraticChartAtom A y) (hXt : X t = R) {Sa Sb : ℝ} (hSa : 0 < Sa) (hSb : 0 < Sb) (hXa : MeasureTheory.eLpNorm (augPhys (X a)) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1)) ≤ ENNReal.ofReal Sa) (hXb : MeasureTheory.eLpNorm (augPhys (X b)) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1)) ≤ ENNReal.ofReal Sb) : ‖(cellForm ⋯ hwI W) X‖ ≤ β * Sa * Sb

A residual passing at level β bounds the cell form with a pure source of a tag in the mask in another slot u, the residual in its slot t, and two spectators of normalized sizes S_a, S_b by β S_a S_b.

theorem TrilinearHT.Auto.ResidOK.combo_le {W : Type u_1} [Fintype W] {κ : LocalKernelClass} {Tg : Type u_2} {G : RealDyadicGrid} {I : ℤ × ℤ} {c₀ : ℕ} {H : ℝ} {tagOf : Tg → ChartTag} {wI : ℝ × ℝ → ℂ} (hwI : IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) wI) {t : Fin 4} {M : Tg → Prop} {R : ↥(ColumnL2 W)} {β : ℝ} (h : ResidOK G I c₀ H tagOf wI t M R β) {u a b : Fin 4} (hut : u ≠ t) (hua : u ≠ a) (hub : u ≠ b) (hta : t ≠ a) (htb : t ≠ b) (hab : a ≠ b) {κs : Type u_3} (F : Finset κs) (c : κs → ℂ) (src : κs → ↥(ColumnL2 W)) (tag : κs → Tg) (htag : ∀ m ∈ F, M (tag m)) (hsrc : ∀ m ∈ F, ∃ (A : QuadraticChartData (tagOf (tag m)).dim), QuadraticChartComplexity c₀ H A ∧ A.horizontal = (tagOf (tag m)).θ ∧ A.matrix = ↑(slotCoeff u) • (tagOf (tag m)).C ∧ A.quadratic = ↑(slotCoeff u) * (tagOf (tag m)).lam ∧ ∀ᵐ (y : ℝ), y ∈ dyadicGridCell G I.1 I.2 → augPhys (src m) y = quadraticChartAtom A y) (X : Fin 4 → ↥(ColumnL2 W)) (hXu : X u = ∑ m ∈ F, c m • src m) (hXt : X t = R) {Sa Sb : ℝ} (hSa : 0 < Sa) (hSb : 0 < Sb) (hXa : MeasureTheory.eLpNorm (augPhys (X a)) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1)) ≤ ENNReal.ofReal Sa) (hXb : MeasureTheory.eLpNorm (augPhys (X b)) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1)) ≤ ENNReal.ofReal Sb) : ‖(cellForm ⋯ hwI W) X‖ ≤ (∑ m ∈ F, ‖c m‖) * (β * Sa * Sb)

A combination of pure sources (tags in the mask) in slot u against a residual passing at level β in slot t, with two spectators: the cell form is at most (Σ |c_m|) β S_a S_b (blueprint lines 1850-1855).

Sources and separation on the original basic columns

Blueprint lines 1676, 1798 and 1850-1852.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.occAvail_of_mem {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) {c : bf.admT.Cell} {x : bf.Vtx} (hx : x ∈ bf.admT.X c) : bf.occAvail (↑x.2) x.1

A present vertex is available at its admission cell.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.vtxAt_fst {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (I : ℤ × ℤ) (x : bf.Lab) : (bf.vtxAt I x).1 = x

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.vtxAt_spec {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) {I : ℤ × ℤ} {x : bf.Lab} (h : bf.occAvail I x) : bf.occAvail (↑(bf.vtxAt I x).2) x ∧ dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G (↑(bf.vtxAt I x).2).1 (↑(bf.vtxAt I x).2).2

The vertex of an original column available at a cell of the setup is available at its admission cell, which contains the cell.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.vchart_tag {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (x : bf.Vtx) : (bf.vchart x).snd.horizontal = (bf.vtag x).θ ∧ (bf.vchart x).snd.matrix = ↑(slotCoeff x.1.fst) • (bf.vtag x).C ∧ (bf.vchart x).snd.quadratic = ↑(slotCoeff x.1.fst) * (bf.vtag x).lam

The tag data of a vertex chart: its horizontal part, matrix and quadratic coefficient are those of its normalized tag with the slot multiplier (blueprint line 1677).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.origCol_source {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (l : Fin 4) {I : ℤ × ℤ} {x : bf.Lab} (hx : (bf.origCols l).avail I x) : QuadraticChartComplexity A.csrc A.Hsrc (bf.vchart (bf.vtxAt I x)).snd ∧ IsBoundedQuadraticChart (bf.vchart (bf.vtxAt I x)).snd ∧ (bf.vchart (bf.vtxAt I x)).snd.horizontal = (bf.vtag (bf.vtxAt I x)).θ ∧ (bf.vchart (bf.vtxAt I x)).snd.matrix = ↑(slotCoeff l) • (bf.vtag (bf.vtxAt I x)).C ∧ (bf.vchart (bf.vtxAt I x)).snd.quadratic = ↑(slotCoeff l) * (bf.vtag (bf.vtxAt I x)).lam ∧ ∀ y ∈ dyadicGridCell A.G I.1 I.2, (bf.origCols l).scalar x y = quadraticChartAtom (bf.vchart (bf.vtxAt I x)).snd y

An available original column of the slot l is, on the cell, the bounded pure chart of its vertex, of the common source complexity, with the tag data of its slot (blueprint line 1676).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.templateCol_source {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) {x : bf.Vtx} (hx : bf.occAvail (↑x.2) x.1) (t : Fin 4) {R : Fin (bf.vtag x).dim → ℕ} (hR : R ∈ residueBox (bf.vtag x).dim 9) (γ : ℝ) (I : ℤ × ℤ) (r : ℕ) : ∃ (A' : QuadraticChartData (bf.vtag x).dim), QuadraticChartComplexity A.csrc A.Hsrc A' ∧ A'.horizontal = (bf.vtag x).θ ∧ A'.matrix = ↑(slotCoeff t) • (bf.vtag x).C ∧ A'.quadratic = ↑(slotCoeff t) * (bf.vtag x).lam ∧ (templateCol (bf.vtag x) t R γ I r x).atom = quadraticChartAtom A'

The templates of the tag of an available vertex in any slot are pure sources of that tag in that slot, of the common source complexity.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.depth_admAt {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) {I : ℤ × ℤ} (hI : I ∈ A.cells) : bf.admT.depth (bf.admAt I) = I.1

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.mem_mask_of_near {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (Hed : ℝ) (Hmax : ℕ) (ωp ωh : Fin A.fcd0 → bf.Vtx → Fin (A.fcd0 + 1)) {I : bf.admT.Cell} {w b : bf.Vtx} (hw : w ∈ bf.admT.X I) (hs : (bf.colorSetup Hed Hmax ωp ωh).Success ((bf.colorSetup Hed Hmax ωp ωh).colorData (bf.admT.st I) w)) (hb : b ∈ bf.admT.X I) {h : ℕ} (hd : (bf.tagDist Hed).d (bf.admT.depth I) b w ≤ ↑h) (hh : h ≤ Hmax) : b ∈ (bf.colorSetup Hed Hmax ωp ωh).mask bf.admT A.famVtxBound ((bf.colorSetup Hed Hmax ωp ωh).grp bf.admT A.famVtxBound I w) h I

A present vertex within pad h ≤ H_max of a successful current center lies in the ball mask of its group (blueprint lem:masks, first assertion).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.mask_sep {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (Hed : ℝ) (Hmax : ℕ) (ωp ωh : Fin A.fcd0 → bf.Vtx → Fin (A.fcd0 + 1)) {I : bf.admT.Cell} {w₁ w₂ : bf.Vtx} (hw₁ : w₁ ∈ bf.admT.X I) (hw₂ : w₂ ∈ bf.admT.X I) (hs₁ : (bf.colorSetup Hed Hmax ωp ωh).Success ((bf.colorSetup Hed Hmax ωp ωh).colorData (bf.admT.st I) w₁)) (hs₂ : (bf.colorSetup Hed Hmax ωp ωh).Success ((bf.colorSetup Hed Hmax ωp ωh).colorData (bf.admT.st I) w₂)) (hcol : (bf.colorSetup Hed Hmax ωp ωh).color bf.admT A.famVtxBound I w₁ = (bf.colorSetup Hed Hmax ωp ωh).color bf.admT A.famVtxBound I w₂) (hne : (bf.colorSetup Hed Hmax ωp ωh).grp bf.admT A.famVtxBound I w₁ ≠ (bf.colorSetup Hed Hmax ωp ωh).grp bf.admT A.famVtxBound I w₂) {h h' : ℕ} (hh : h ≤ Hmax) (hh' : h' ≤ Hmax) {b b' : bf.Vtx} (hb : b ∈ (bf.colorSetup Hed Hmax ωp ωh).mask bf.admT A.famVtxBound ((bf.colorSetup Hed Hmax ωp ωh).grp bf.admT A.famVtxBound I w₁) h I) (hb' : b' ∈ (bf.colorSetup Hed Hmax ωp ωh).mask bf.admT A.famVtxBound ((bf.colorSetup Hed Hmax ωp ωh).grp bf.admT A.famVtxBound I w₂) h' I) : ¬(bf.tagDist Hed).d (bf.admT.depth I) b b' ≤ 1

Distinct current groups of one color have separated masks at the current cell (blueprint lem:masks, last assertion).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.not_tagEdge_of_dist {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (Hed : ℝ) {s : ℤ} {b b' : bf.Vtx} (h : ¬(bf.tagDist Hed).d s b b' ≤ 1) : ¬tagEdge Hed (dyadicGridLength A.G s) (bf.vtag b) (bf.vtag b')

Vertices at graph distance greater than one carry tags not joined by an edge.

Leaf histories as named tests (blueprint lines 1807-1815, 1845)

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.layerEntries {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) (ls : List (ℕ × Bool)) (hls : ∀ e ∈ ls, e.1 ≤ fp.Lc) (c : Fin ls.length → Fin fp.P) (i : Fin ls.length) : Fin (fp.Lc + 6) × fp.MaskName I × Bool

The history entries of a list of cumulative layers at the pad choice c (blueprint lines 1807, 1845): the layer i at the split m_i is the rank-(L - m_i + 1) main projection with the cumulative mask at the pad 10 P (L - m_i + 1) + c_i + 1, with its complement flag.

Equations

• fp.layerEntries I ls hls c i = (⟨fp.crank ls[i].1, ⋯⟩, Sum.inl (⟨ls[i].1, ⋯⟩, ⟨fp.cbase ls[i].1 + ↑(c i) + 1, ⋯⟩), ls[i].2)

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.layerName {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) (r : Fin (fp.Lc + 5)) (Mt : fp.MaskName I) (ls : List (ℕ × Bool)) (hls : ∀ e ∈ ls, e.1 ≤ fp.Lc) (hlen : ls.length ≤ fp.mH) (c : Fin ls.length → Fin fp.P) : fp.TestName I Unit

The name of the test with target rank r + 1, target mask name Mt, and the history of the cumulative layers ls at the pad choice c.

Equations

• fp.layerName I r Mt ls hls hlen c = (r, Mt, ⟨⟨ls.length, ⋯⟩, fp.layerEntries I ls hls c⟩, ())

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.layerName_hist {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (cat : List (CatCol bf.Vtx)) (I : ℤ × ℤ) (z : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (r : Fin (fp.Lc + 5)) (Mt : fp.MaskName I) (ls : List (ℕ × Bool)) (hls : ∀ e ∈ ls, e.1 ≤ fp.Lc) (hlen : ls.length ≤ fp.mH) (c : Fin ls.length → Fin fp.P) : MainTest.hist A.G fp.Mc (bf.origCols l) I (fp.testOf l I (fun (x : Unit) => z) (fp.layerName I r Mt ls hls hlen c)) fp.mH cat = (operatorComplementProduct (fun (i : ℕ) => mainProj A.G fp.Mc (bf.origCols l) cat I (fp.crank (ls.getD i (0, false)).1) (fp.cmask I (ls.getD i (0, false)).1 (↑(choiceExt ⋯ c i) + 1))) (fun (i : ℕ) => (ls.getD i (0, false)).2) ls.length) z

The history of a layer test is the complement product of the single-choice layers.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.layer_residOK {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) {κ' : LocalKernelClass} {cS : ℕ} {HS : ℝ} {tagOf : bf.Vtx → ChartTag} {wI : ℝ × ℝ → ℂ} {I : ℤ × ℤ} (hwI : IsAdmissibleLocalKernel κ' (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1) wI) (l : Fin 4) (cat : List (CatCol bf.Vtx)) (z : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (ls : List (ℕ × Bool)) (hls : ∀ e ∈ ls, e.1 ≤ fp.Lc) (hlen : ls.length ≤ fp.mH) (r : Fin (fp.Lc + 5)) (Mt : Fin fp.P → fp.MaskName I) {τ : ℝ} (hpass : ∀ (pc : Fin fp.P × (Fin ls.length → Fin fp.P)), (fp.testOf l I (fun (x : Unit) => z) (fp.layerName I r (Mt pc.1) ls hls hlen pc.2)).Pass A.G (bf.origCols l) I cS HS tagOf wI τ fp.mH cat) : ResidOK A.G I cS HS tagOf wI l (fun (x : bf.Vtx) => ∀ (p : Fin fp.P), fp.maskOf I (Mt p) x) ((layerOp (fun (m : ℕ) => fp.cumFilt l cat I m) ls) z - (opAvg fun (p : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols l) cat I (↑r + 1) (fp.maskOf I (Mt p))) ((layerOp (fun (m : ℕ) => fp.cumFilt l cat I m) ls) z)) (τ * cellNorm A.G I z)

Blueprint lines 1810-1813 at a leaf: if the layer tests of all pad choices pass, the residual of the averaged target filter on the averaged layered history of a slot input passes, against every source whose tag lies in all the target pad masks.

The error at one leaf from passing residuals (blueprint lines 1850-1853)

theorem TrilinearHT.Auto.augPhys_size_le {W : Type u_1} [Fintype W] (G : RealDyadicGrid) (I : ℤ × ℤ) {y x : ↥(ColumnL2 W)} (hy : ‖y‖ ≤ ‖x‖) {S : ℝ} (hS : ‖x‖ / √(dyadicGridLength G I.1) ≤ S) : MeasureTheory.eLpNorm (augPhys y) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1)) ≤ ENNReal.ofReal S

Spectator sizes from norms: a vector of norm at most ‖x‖ with ‖x‖ / √|I| ≤ S has normalized physical size at most S.

theorem TrilinearHT.Auto.leaf_error_resid {W : Type u_1} [Fintype W] {κ : LocalKernelClass} {Tg : Type u_2} {G : RealDyadicGrid} {I : ℤ × ℤ} {c₀ : ℕ} {H : ℝ} {tagOf : Tg → ChartTag} {wI : ℝ × ℝ → ℂ} (hwI : IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) wI) (x : Fin 4 → ↥(ColumnL2 W)) {γ : Type u_3} (L : γ → Fin 4 → ↥(ColumnL2 W) →L[ℂ] ↥(ColumnL2 W)) (hL : ∀ (g : γ) (l : Fin 4) (y : ↥(ColumnL2 W)), ‖(L g l) y‖ ≤ ‖y‖) {u t p q : Fin 4} (hut : u ≠ t) (hup : u ≠ p) (huq : u ≠ q) (htp : t ≠ p) (htq : t ≠ q) (hpq : p ≠ q) {Sz : ℝ} (hSz0 : 0 < Sz) (hSz : ∀ (l : Fin 4), ‖x l‖ / √(dyadicGridLength G I.1) ≤ Sz) {ι : Type u_4} (S : Finset ι) (a : ι → ℂ) (φ : ι → ↥(ColumnL2 W)) (tag : ι → Tg) (Ax : (v : ι) → QuadraticChartData (tagOf (tag v)).dim) (hx : x u = ∑ v ∈ S, a v • φ v) (hAx : ∀ v ∈ S, QuadraticChartComplexity c₀ H (Ax v) ∧ (Ax v).horizontal = (tagOf (tag v)).θ ∧ (Ax v).matrix = ↑(slotCoeff u) • (tagOf (tag v)).C ∧ (Ax v).quadratic = ↑(slotCoeff u) * (tagOf (tag v)).lam ∧ ∀ᵐ (y : ℝ), y ∈ dyadicGridCell G I.1 I.2 → augPhys (φ v) y = quadraticChartAtom (Ax v) y) (Gs : Finset γ) (grp : ι → Option γ) {κs : Type u_5} (F : γ → Finset κs) (c : γ → κs → ℂ) (col : κs → ↥(ColumnL2 W)) (Y : κs → ℝ → ℂ) (ctag : κs → Tg) {βo βm βr τ₂ Ct : ℝ} (hβo : 0 ≤ βo) (hβm : 0 ≤ βm) (hβr : 0 ≤ βr) (hτ₂ : 0 ≤ τ₂) (hCt0 : 0 ≤ Ct) (hold : ∀ v ∈ S, grp v = none → ∃ (gl : Fin 4) (b' : Fin 4), gl ≠ u ∧ gl ≠ t ∧ b' ≠ u ∧ b' ≠ t ∧ gl ≠ b' ∧ ∃ (M : Tg → Prop), M (tag v) ∧ ResidOK G I c₀ H tagOf wI gl M (x gl) βo) (hcur : ∀ v ∈ S, ∀ (g₀ : γ), grp v = some g₀ → g₀ ∈ Gs ∧ ∃ (M : Tg → Prop), M (tag v) ∧ ResidOK G I c₀ H tagOf wI t M (x t - (L g₀ t) (x t)) βm) (hexp : ∀ g ∈ Gs, (L g t) (x t) = ∑ m ∈ F g, c g m • col m ∧ ∑ m ∈ F g, ‖c g m‖ ≤ Ct) (hcol : ∀ g ∈ Gs, ∀ m ∈ F g, ∀ᵐ (y : ℝ), y ∈ dyadicGridCell G I.1 I.2 → augPhys (col m) y = Y m y) (hsep : ∀ v ∈ S, ∀ (g₀ : γ), grp v = some g₀ → ∀ g ∈ Gs, g ≠ g₀ → ∀ m ∈ F g, PairSmall (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) wI u t (quadraticChartAtom (Ax v)) (Y m) τ₂) (hres : ∀ g ∈ Gs, ∀ (l : Fin 4), l ≠ t → ∃ (M : Tg → Prop), (∀ m ∈ F g, M (ctag m)) ∧ ResidOK G I c₀ H tagOf wI l M (x l - (L g l) (x l)) βr) (hsrcT : ∀ g ∈ Gs, ∀ m ∈ F g, ∃ (A' : QuadraticChartData (tagOf (ctag m)).dim), QuadraticChartComplexity c₀ H A' ∧ A'.horizontal = (tagOf (ctag m)).θ ∧ A'.matrix = ↑(slotCoeff t) • (tagOf (ctag m)).C ∧ A'.quadratic = ↑(slotCoeff t) * (tagOf (ctag m)).lam ∧ ∀ᵐ (y : ℝ), y ∈ dyadicGridCell G I.1 I.2 → augPhys (col m) y = quadraticChartAtom A' y) : ‖(cellForm ⋯ hwI W) x - ∑ g ∈ Gs, (cellForm ⋯ hwI W) fun (l : Fin 4) => (L g l) (x l)‖ ≤ (∑ v ∈ S, ‖a v‖) * ((↑Gs.card + 1) * (βo * Sz * Sz) + βm * Sz * Sz + ↑Gs.card * (τ₂ * Sz * Sz * Ct)) + ↑Gs.card * (3 * (Ct * (βr * Sz * Sz)))

Blueprint prop:localize at one cell and leaf (lines 1848-1853), from passing residuals: the form of the leaf inputs is the sum over the current groups of the forms of their filter outputs, up to the error of leaf_localization. The upper guard in slot u is expanded in pure sources; an old source is killed by a residual of a lower guard (level βo); a current source of the group G₀ meets the first ball residual of its group in slot t (level βm) and is separated (τ₂) from the columns of the first ball outputs of the other groups; the residual insertions in the other slots are tested against those columns (level βr); the first ball outputs expand with coefficient sums at most Ct.

Masked expansions of main filter outputs (blueprint lines 1835, 1850)

noncomputable def TrilinearHT.Auto.labelTag {V : Type} [Fintype V] {Tg : Type u_1} {Mc : ℕ} (O : OrigCols V Tg) (s : List (CatCol Tg)) (I : ℤ × ℤ) (d : Tg) : V ⊕ Fin Mc → Tg

The tag of a main label at a cell: the vertex of an original column, the tag of a template (a default tag beyond the catalog).

Equations

• TrilinearHT.Auto.labelTag O s I d = Sum.elim (fun (v : V) => O.tag I v) fun (n : Fin Mc) => if h : ↑n < s.length then s[↑n].tag else d

noncomputable def TrilinearHT.Auto.mainLabelsM {V : Type} [Fintype V] {Tg : Type u_1} (G : RealDyadicGrid) (Mc : ℕ) (O : OrigCols V Tg) (s : List (CatCol Tg)) (I : ℤ × ℤ) (r : ℕ) (M : Tg → Prop) (d : Tg) : Finset (V ⊕ Fin Mc)

The main labels of rank at most r at the cell whose tag lies in the mask M.

Equations

• TrilinearHT.Auto.mainLabelsM G Mc O s I r M d = {v ∈ TrilinearHT.Auto.mainLabels G Mc O s I r | M (TrilinearHT.Auto.labelTag O s I d v)}

theorem TrilinearHT.Auto.mem_mainLabels {V : Type} [Fintype V] {Tg : Type u_1} {G : RealDyadicGrid} {Mc : ℕ} {O : OrigCols V Tg} {s : List (CatCol Tg)} {I : ℤ × ℤ} {r : ℕ} {v : V ⊕ Fin Mc} : v ∈ mainLabels G Mc O s I r ↔ Sum.elim (fun (v : V) => O.avail I v) (fun (n : Fin Mc) => ∃ (hn : ↑n < s.length), dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G s[↑n].birth.1 s[↑n].birth.2 ∧ s[↑n].rank ≤ r) v

theorem TrilinearHT.Auto.mem_mainLabelsM {V : Type} [Fintype V] {Tg : Type u_1} {G : RealDyadicGrid} {Mc : ℕ} {O : OrigCols V Tg} {s : List (CatCol Tg)} {I : ℤ × ℤ} {r : ℕ} {M : Tg → Prop} {d : Tg} {v : V ⊕ Fin Mc} : v ∈ mainLabelsM G Mc O s I r M d ↔ v ∈ mainLabels G Mc O s I r ∧ M (labelTag O s I d v)

theorem TrilinearHT.Auto.mainLabelsM_subset {V : Type} [Fintype V] {Tg : Type u_1} {G : RealDyadicGrid} {Mc : ℕ} {O : OrigCols V Tg} (s : List (CatCol Tg)) (I : ℤ × ℤ) (r : ℕ) (M : Tg → Prop) (d : Tg) : mainLabelsM G Mc O s I r M d ⊆ mainLabels G Mc O s I r

theorem TrilinearHT.Auto.mainLabelsM_mono {V : Type} [Fintype V] {Tg : Type u_1} {G : RealDyadicGrid} {Mc : ℕ} {O : OrigCols V Tg} (s : List (CatCol Tg)) (I : ℤ × ℤ) (r : ℕ) {M M' : Tg → Prop} (hM : ∀ (x : Tg), M x → M' x) (d : Tg) : mainLabelsM G Mc O s I r M d ⊆ mainLabelsM G Mc O s I r M' d

theorem TrilinearHT.Auto.mainRange_exists_coeffM {V : Type} [Fintype V] {Tg : Type u_1} {G : RealDyadicGrid} {Mc : ℕ} {O : OrigCols V Tg} {s : List (CatCol Tg)} {I : ℤ × ℤ} {r : ℕ} {M : Tg → Prop} (d : Tg) {x : ↥(ColumnL2 (V ⊕ Fin Mc))} (hx : x ∈ mainRange G Mc O s I r M) : ∃ (c : V ⊕ Fin Mc → ℂ), x = ∑ v ∈ mainLabelsM G Mc O s I r M d, c v • mainCol G Mc O s I v

Every vector of a main range is a combination of the columns of the main labels of the mask.

@[reducible, inline]

abbrev TrilinearHT.Auto.ActiveSetup.BasicFamilies.Grp {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) : Type

The groups of the attempt: a color with its complete color data.

Equations

• bf.Grp = (ℕ × Option (Fin A.fcd0 × bf.Vtx × ℤ) × ℕ × (ℕ × ℕ) × Option (Fin A.fcd0 × bf.Vtx × ℤ))

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.avg_expansion {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (l : Fin 4) {Mc : ℕ} (s : List (CatCol bf.Vtx)) (I : ℤ × ℤ) (r : ℕ) {P : ℕ} (hP : 0 < P) (M : Fin P → bf.Vtx → Prop) (Mtop : bf.Vtx → Prop) (hM : ∀ (p : Fin P) (x : bf.Vtx), M p x → Mtop x) (d : bf.Vtx) (z : ↥(ColumnL2 (bf.Lab ⊕ Fin Mc))) : ∃ (c : bf.Lab ⊕ Fin Mc → ℂ), (opAvg fun (p : Fin P) => mainProj A.G Mc (bf.origCols l) s I r (M p)) z = ∑ v ∈ mainLabelsM A.G Mc (bf.origCols l) s I r Mtop d, c v • mainCol A.G Mc (bf.origCols l) s I v ∧ ∑ v ∈ mainLabelsM A.G Mc (bf.origCols l) s I r Mtop d, ‖c v‖ ≤ A.colBudget * √↑(mainLabelsM A.G Mc (bf.origCols l) s I r Mtop d).card * ‖z‖ / √(dyadicGridLength A.G I.1)

Blueprint line 1835 for an averaged main filter: the average over the pads of rank-r main projections with masks M p inside Mtop, applied to an input of the slot l, is a combination of the columns of the main labels of the mask Mtop whose coefficients have absolute sum at most colBudget √N ‖z‖ / √|I|, N the number of these labels.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.mainLabel_source {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (l : Fin 4) {Mc : ℕ} (s : List (CatCol bf.Vtx)) (hT : ∀ e ∈ s, ∃ R ∈ residueBox (bf.vtag e.tag).dim 9, ∃ (γ : ℝ), e = templateCol (bf.vtag e.tag) l R γ e.birth e.rank e.tag) (htag : ∀ e ∈ s, bf.occAvail (↑e.tag.2) e.tag.1) (I : ℤ × ℤ) (r : ℕ) (M : bf.Vtx → Prop) (d : bf.Vtx) {v : bf.Lab ⊕ Fin Mc} (hv : v ∈ mainLabelsM A.G Mc (bf.origCols l) s I r M d) : M (labelTag (bf.origCols l) s I d v) ∧ ∃ (A' : QuadraticChartData (bf.vtag (labelTag (bf.origCols l) s I d v)).dim), QuadraticChartComplexity A.csrc A.Hsrc A' ∧ IsBoundedQuadraticChart A' ∧ A'.horizontal = (bf.vtag (labelTag (bf.origCols l) s I d v)).θ ∧ A'.matrix = ↑(slotCoeff l) • (bf.vtag (labelTag (bf.origCols l) s I d v)).C ∧ A'.quadratic = ↑(slotCoeff l) * (bf.vtag (labelTag (bf.origCols l) s I d v)).lam ∧ ∀ᵐ (y : ℝ), y ∈ dyadicGridCell A.G I.1 I.2 → augPhys (mainCol A.G Mc (bf.origCols l) s I v) y = quadraticChartAtom A' y

A main label of the mask at a cell is a pure source of its tag in the slot: an available original column is the chart of its vertex, a template of the catalog is the chart of its template (blueprint lines 1676, 1798).

The leaves of an attempt on the main columns (blueprint prop:localize, lines 1848-1853)

theorem TrilinearHT.Auto.cellNorm_le {W : Type u_1} [Fintype W] (G : RealDyadicGrid) (I : ℤ × ℤ) (x : ↥(ColumnL2 W)) : cellNorm G I x ≤ ‖x‖ / √(dyadicGridLength G I.1)

The normalized norm on a cell is at most the norm over √|I|.

theorem TrilinearHT.Auto.searchLeaves_layers_le (B fuel ℓ h : ℕ) (up : Fin 4) (low : Option (Fin 4)) (ls : Fin 4 → List (ℕ × Bool)) : h ≤ B → (∀ (l : Fin 4), ∀ e ∈ ls l, e.1 ≤ B) → ∀ L ∈ searchLeaves fuel ℓ h up low ls, ∀ (l : Fin 4), ∀ e ∈ L.layers l, e.1 ≤ B

The layers of the guarded search only split at colors at most the initial upper end.

theorem TrilinearHT.Auto.leafAt_layers_le {fuel Lc : ℕ} {up₀ : Fin 4} (s : ℕ) (l : Fin 4) (e : ℕ × Bool) : e ∈ (leafAt fuel Lc up₀ s).layers l → e.1 ≤ Lc

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.cbase_succ_le {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) {k : ℕ} (hk : 1 ≤ k) (hkL : k ≤ fp.Lc) : fp.cbase k + fp.P ≤ fp.cbase (k - 1)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.cbase_le_bbase {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (k j : ℕ) : fp.cbase k + fp.P ≤ fp.bbase j

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.bbase_one_le {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) {j : ℕ} (hj : 2 ≤ j) : fp.bbase 1 + fp.P ≤ fp.bbase j

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.groupsAt {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) (k : ℕ) : Finset bf.Grp

The current groups of the cell I at the color k: the groups of the present vertices of color k (blueprint line 1850).

Equations

• fp.groupsAt I k = Finset.image (fp.K.grp bf.admT A.famVtxBound (bf.admAt I)) ({w ∈ bf.admT.X (bf.admAt I) | fp.K.color bf.admT A.famVtxBound (bf.admAt I) w = k})

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.mem_groupsAt {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) {I : ℤ × ℤ} {k : ℕ} {G : bf.Grp} (h : G ∈ fp.groupsAt I k) : ∃ w ∈ bf.admT.X (bf.admAt I), fp.K.color bf.admT A.famVtxBound (bf.admAt I) w = k ∧ fp.K.grp bf.admT A.famVtxBound (bf.admAt I) w = G

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.card_groupsAt_le {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) (k : ℕ) : (fp.groupsAt I k).card ≤ A.famVtxBound

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.classify {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) (hsucc : ∀ w ∈ bf.admT.X (bf.admAt I), fp.K.Success (fp.K.colorData (bf.admT.st (bf.admAt I)) w)) {k hpad : ℕ} (hk : 1 ≤ k) (hkL : k ≤ fp.Lc) (hpadle : hpad ≤ fp.cbase k + fp.P + 1) {x : bf.Vtx} (hx : x ∈ fp.K.cumMask bf.admT A.famVtxBound k hpad (bf.admAt I)) : (∀ (p' : ℕ), fp.cmask I (k - 1) (p' + 1) x) ∨ ∃ G ∈ fp.groupsAt I k, ∀ (p' : ℕ), fp.bmask I G 1 (p' + 1) x

Blueprint line 1850: a vertex of the upper cumulative mask at color k (at a pad at most the upper pad) is old (in every lower guard mask at k - 1) or lies, at every pad, in the first ball mask of a current group of color k.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.sep_pair {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) {I : ℤ × ℤ} (hI : I ∈ A.cells) (hsucc : ∀ w ∈ bf.admT.X (bf.admAt I), fp.K.Success (fp.K.colorData (bf.admT.st (bf.admAt I)) w)) {k : ℕ} {G₀ G : bf.Grp} (hG₀ : G₀ ∈ fp.groupsAt I k) (hG : G ∈ fp.groupsAt I k) (hne : G ≠ G₀) {τ₂ : ℝ} (hτ₂ : 0 < τ₂) (hτ₂1 : τ₂ ≤ 1) (hHed : Real.exp (↑A.Dg * (1 + Real.log A.Hsrc + Real.log τ₂⁻¹) ^ A.Dg) ≤ fp.Hed) {u t : Fin 4} (hut : u ≠ t) {x : bf.Vtx} {p₀ : ℕ} (hp₀ : p₀ ≤ fp.P) (hx : fp.bmask I G₀ 1 p₀ x) (Ax : QuadraticChartData (bf.vtag x).dim) (hAx : QuadraticChartComplexity A.csrc A.Hsrc Ax) (hAb : IsBoundedQuadraticChart Ax) (hθ : Ax.horizontal = (bf.vtag x).θ) (hM : Ax.matrix = ↑(slotCoeff u) • (bf.vtag x).C) (hq : Ax.quadratic = ↑(slotCoeff u) * (bf.vtag x).lam) {y : bf.Vtx} {p : ℕ} (hp : p ≤ fp.P) (hy : fp.bmask I G 1 p y) (Ay : QuadraticChartData (bf.vtag y).dim) (hAy : QuadraticChartComplexity A.csrc A.Hsrc Ay) (hAyb : IsBoundedQuadraticChart Ay) (hθ' : Ay.horizontal = (bf.vtag y).θ) (hM' : Ay.matrix = ↑(slotCoeff t) • (bf.vtag y).C) (hq' : Ay.quadratic = ↑(slotCoeff t) * (bf.vtag y).lam) {wI : ℝ × ℝ → ℂ} (hwI : IsAdmissibleLocalKernel κ (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1) wI) : PairSmall (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1) wI u t (quadraticChartAtom Ax) (quadraticChartAtom Ay) τ₂

Blueprint lines 1851-1852: a pure chart of a vertex of the first ball mask of one current group in slot u is pair-separated (PairSmall with τ₂) from every pure chart, in slot t, of a vertex of a first ball mask of a different current group of the same color.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.layer_residOK' {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) {κ' : LocalKernelClass} {cS : ℕ} {HS : ℝ} {tagOf : bf.Vtx → ChartTag} {wI : ℝ × ℝ → ℂ} {I : ℤ × ℤ} (hwI : IsAdmissibleLocalKernel κ' (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1) wI) (l : Fin 4) (cat : List (CatCol bf.Vtx)) (z : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (ls : List (ℕ × Bool)) (hls : ∀ e ∈ ls, e.1 ≤ fp.Lc) (hlen : ls.length ≤ fp.mH) (r : Fin (fp.Lc + 5)) {rk : ℕ} (hrk : ↑r + 1 = rk) (Mt : Fin fp.P → fp.MaskName I) (Mk : Fin fp.P → bf.Vtx → Prop) (hMk : ∀ (p : Fin fp.P), fp.maskOf I (Mt p) = Mk p) {τ : ℝ} (hpass : ∀ (pc : Fin fp.P × (Fin ls.length → Fin fp.P)), (fp.testOf l I (fun (x : Unit) => z) (fp.layerName I r (Mt pc.1) ls hls hlen pc.2)).Pass A.G (bf.origCols l) I cS HS tagOf wI τ fp.mH cat) : ResidOK A.G I cS HS tagOf wI l (fun (x : bf.Vtx) => ∀ (p : Fin fp.P), Mk p x) ((layerOp (fun (m : ℕ) => fp.cumFilt l cat I m) ls) z - (opAvg fun (p : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols l) cat I rk (Mk p)) ((layerOp (fun (m : ℕ) => fp.cumFilt l cat I m) ls) z)) (τ * cellNorm A.G I z)

layer_residOK with the target rank and masks given by equations.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.inputL {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (I : ℤ × ℤ) (x : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (ls : Fin 4 → List (ℕ × Bool)) (l : Fin 4) : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))

The layered input of the slot l at a leaf with layers ls on the cell I.

Equations

• fp.inputL cat I x ls l = (TrilinearHT.Auto.layerOp (fun (m : ℕ) => fp.cumFilt l (cat l) I m) (ls l)) (x l)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.norm_cumFilt_apply_le {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (I : ℤ × ℤ) (m : ℕ) (y : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : ‖(fp.cumFilt l s I m) y‖ ≤ ‖y‖ ∧ ‖(ContinuousLinearMap.id ℂ ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)) - fp.cumFilt l s I m) y‖ ≤ ‖y‖

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.norm_ballFilt_apply_le {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (I : ℤ × ℤ) (G : bf.Grp) (j : ℕ) (y : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : ‖(fp.ballFilt l s I G j) y‖ ≤ ‖y‖

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.norm_inputL_le {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (I : ℤ × ℤ) (x : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (ls : Fin 4 → List (ℕ × Bool)) (l : Fin 4) : ‖fp.inputL cat I x ls l‖ ≤ ‖x l‖

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.level_le {τ' τr cN Sz : ℝ} (h1 : τ' ≤ τr) (h2 : 0 ≤ cN) (h3 : cN ≤ Sz) (h4 : 0 ≤ τr) : τ' * cN ≤ τr * Sz