Trilinear Hilbert transform: leaf_bound #
Blueprint prop:localize at one active cell and one leaf (lines 1848-1853) on the main columns:
given an expansion of the upper guard input in pure bounded charts of vertices of its cumulative
mask, the form of the leaf inputs is the sum over the current groups of the forms of their ball
outputs, up to the old-source (τ_o), matching (τ_m), separation (τ₂) and residual (τ_r)
errors; the first ball outputs expand with coefficient sums at most colBudget √N_t S.
Blueprint prop:localize at one active cell and one leaf (lines 1848-1853), with the expansion
of the upper guard (line 1850: "expand only this outer primal"): a cumulative main filter
(coefficient sum at most colBudget √N_u S over its N_u main labels, blueprint line 1835) or
the basic slot, whose input is a combination of its available original columns (coefficient sum
at most colBudget √(2 colBudget) S).
The error of one leaf of leaf_main with at most D current groups.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cell form of an attempt on the main columns (zero off the active cells).
Equations
Instances For
On an active cell the cell form is the local form of the physical parts (blueprint line 1841:
H_I(Z_0, Z_1, Z_2, Z_3)).
Blueprint prop:localize (lines 1838-1856) for an attempt on the main columns, summed over a
set of active cells without failed vertices: the weighted cell minima of the forms of the slot
inputs are at most the weighted minima, over the leaves of the guarded color search, of the sums
over the current groups of the forms of their ball outputs
Z_{l,G,s} = L_{l,G,s} B_{l,s} z_l, plus the weighted leaf errors (the cell minimum distributes
over the leaves by eq:min-subadd).
The localized sum of an attempt on the main columns (blueprint prop:localize, line 1854) #
The arithmetic of the leaf error (blueprint line 1854): with the coefficient sum of the upper
guard at most 2 C a S, the thresholds τ₃ / (D a), τ₃ / (D b), τ₃ / (D c) of
eq:catalog-test for path counts a² ≤ b² ≤ c², the pair threshold τ₂ = τ₃ / (D² c²) and
C ≤ D, each expansion cost is canceled and the leaf error is at most 9 (D + 1) τ₃ S⁴.
The leaf error with the thresholds of eq:catalog-test at the path counts n and the pair
threshold τ₂ = τ₃ / (D² n_{L+1}) is at most 9 (D + 1) τ₃ S⁴ (blueprint line 1854).
Blueprint prop:localize (lines 1838-1856) for an attempt on the main columns. For slot inputs
z_l that are augmented vectors supported on the active cells without template coordinates, the
catalog closure (lem:closure) at the thresholds τ₃ / (D √n_{r-1}) of eq:catalog-test gives slot
catalogs of same-tag templates passing all named tests, and then, on every set of active cells of
path multiplicity at most M_p without failed vertices whose colors are at most L and whose basic
guard slot input is a combination of its original columns, with local input sizes at most S:
the weighted cell minima of the forms of the slot inputs are at most the sum over the leaves of
the guarded color search of the weighted minima of the current-group sums
Σ_G H_I(Z_{0,G,s}, …, Z_{3,G,s}), Z_{l,G,s} = L_{l,G,s} B_{l,s} z_l (one positive smeared ball
filter after a shared product of cumulative filters or complements), plus
Σ|I| · #leaves · 9 (D + 1) τ₃ S⁴. The pair threshold is τ₂ = τ₃ / (D² n_{L+1}), chosen after
the main count (line 1854), and H_ed is large for it (lem:graph). The catalogs also satisfy
the closure counts of lem:closure (ranks at most L + 5, at most n_r main labels of rank at most
r at cells in at most M_p active cells, length at most #cells · T), which give the main
budget of line 1859.
Basic-slot histories on the main columns (blueprint line 1859) #
Generic compression and locality lemmas (moved from Sec13_3) #
A projection onto vectors fixed by a self-adjoint restriction ignores the restriction.
The span of column functions vanishing off J is fixed by the restriction to J ⊆ s.
Compression of the outer main ball projection (blueprint lines 2068-2070) #
The one-factor compression constant of columnSpatialCompression.
Instances For
Blueprint lines 2068-2070 (lem:compression with one factor): rows Q_k local to decision
cells u_k and Bessel with constant c remain Bessel after inserting the inherited projection at
their decision cells, with constant c · C₁².
The row-space triangle inequality for averages (blueprint line 2069, "restore its average"): a row bound for each averaged operator persists for the average.
Averaged cumulative layers as averages of complement products (lines 2072-2074) #
Blueprint lines 2072-2074 ("expand complements ... retain averages as averages"): a layer product of pad averages is the uniform average over pad tuples of complement products.
Compression of averaged cumulative histories (blueprint lines 2072-2075) #
The complement-compression constant of columnSpatialCompression_complements for n
factors.
Equations
Instances For
Rows bounded for each member of a uniform average over a finite set remain bounded for the average.
Blueprint lines 2072-2075 (lem:compression with complements and averages): rows local to
their decision cells and Bessel with constant B remain Bessel after inserting the averaged
cumulative layers at their decision cells, at the complement-compression cost.
On a cell of the depth-h partition, the depth projection is the cell projection, on both
sides.
Blueprint lines 1879-1890 (compression for global histories): rows that split orthogonally
over the cells of their depth partition and are Bessel with constant B remain Bessel after
inserting the global averaged histories of their depths, at the complement-compression cost.
Relabeling of column spaces (blueprint line 1859: histories acting on F_l) #
The pointwise relabeling of augmented vectors along an injection of labels: the physical
coordinate is kept and the private coordinate of v is moved to f v.
Equations
- TrilinearHT.Auto.relabelCLM f = ∑ o : Option V, ContinuousLinearMap.smulRight (EuclideanSpace.proj o) (EuclideanSpace.single (Option.map f o) 1)
Instances For
The relabeling of column inputs along an injection of labels.
Equations
Instances For
The relabeling as a linear isometry.
Equations
- TrilinearHT.Auto.colRelabelLI hf = { toLinearMap := ↑(TrilinearHT.Auto.colRelabel f), norm_map' := ⋯ }
Instances For
An isometric embedding transports orthogonal projections onto finite-dimensional subspaces:
the projection onto the image of K of the image of x is the image of the projection of x.
Relabeling a private column value moves its private coordinate.
Relabeling a weighted column gives the weighted column of the image label.
A cell column of a column tree is a weighted column.
The image of a cell range of a column tree under a relabeling is the span of the relabeled weighted columns.
The main column tree of an attempt (blueprint lines 1805, 1859) #
The relevant main labels of a catalog: the original basic columns available on some active cell and the templates of the catalog.
Equations
Instances For
Equations
- bf.instFintypeRLab Mc s = Fintype.ofFinite (bf.RLab Mc s)
The underlying main label of a relevant label.
Instances For
The birth cells of the relevant main labels: the family birth cell of an original column, clamped to the attempt root, and the birth cell of a template.
Equations
Instances For
An original label available at a cell of the setup is available at its family birth cell.
An available original label's cell lies in its main birth cell.
The number of templates of a catalog whose birth cell contains the point y.
Equations
Instances For
A main budget of a catalog of an attempt: the templates are born at active cells, and the
budget B dominates eight column budgets plus the template path counts (blueprint line 1835:
the common main catalog budget).
- B : ℝ
Upper bound for the original column budget plus the template count along a path.
Instances For
At most eight column budgets of original columns have a main birth cell containing a point.
The main column tree of a catalog of an attempt (blueprint lines 1805, 1859): the relevant main
labels with their main scalars and private weights, born at their (clamped) family birth cells
and template birth cells, on the complete tree of the attempt, with a budget B that dominates
eight column budgets plus the template path counts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The active ancestors of a cell: the active cells containing it.
Equations
- TrilinearHT.Auto.ActiveSetup.BasicFamilies.activeAnc c = {a ∈ A.cells | TrilinearHT.Auto.dyadicGridCell A.G c.1 c.2 ⊆ TrilinearHT.Auto.dyadicGridCell A.G a.1 a.2}
Instances For
The deepest active ancestor of a cell, if any (blueprint line 1859: between actual uses the inherited projections are retained).
Equations
Instances For
The main labels of the slot l at an active cell a, of rank at most r, in the vertex
mask M: the available original columns whose vertex lies in M and the templates born above
a of rank at most r with tag in M (blueprint lines 1805-1806).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inherited masks of the main column tree for the slot l, rank r and depth-monotone
vertex masks M: at a cell, the main labels of its deepest active ancestor, none above the attempt
(blueprint line 1859: retained inherited projections, zero before the attempt).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The main depth family of the slot l for the rank r and the depth-monotone vertex masks
M (blueprint line 1859): the nested depth projections of the main column tree with the
inherited masks, on the complete tree of the attempt.
Equations
Instances For
At an active cell the relabeled cell projection of the main depth family is the main projection (blueprint lines 1805, 1859): the global main projections restrict to the cell-local ones.
Relabelings, restrictions and adjoints #
A relabeling commutes with the restriction to a set.
The adjoint of a relabeling also commutes with the restriction to a set.
Along an injection the adjoint of the relabeling is a left inverse.
On the range of an injective relabeling, relabeling after the adjoint is the identity.
Layer products intertwine along a map intertwining their factors.
On a cell of the depth partition, the global averaged history is the layer product of the averaged cell projections of the cell (blueprint lines 1859, 1879: histories evaluated at their decision cells).
The main column tree as a depth family on the complete tree of the attempt (its masks are
replaced by withMask).
Instances For
At an active cell, the cell restriction of the relabeled global depth projection of the main tree with the inherited masks is the main projection of the cell applied to the restricted relabeled input (blueprint lines 1805, 1859).
The inherited cumulative masks of the main tree of the slot l (blueprint lines 1807, 1859):
the split m, the pad index p.
Equations
Instances For
The inherited ball masks of the main tree of the slot l for the group G at the ball level
j and the pad index p (blueprint lines 1807, 1859).
Equations
Instances For
The global shared cumulative history B'_{l,s} with layers ls at the depth h, on the
relevant main labels: a layer product of averaged global main depth projections or their
complements (blueprint lines 1859, 1871).
Equations
Instances For
The global positive smeared ball filter L_{l,G} at the ball level j and the depth h
(blueprint lines 1807, 1859).
Equations
Instances For
At an active cell the global cumulative history restricts to the cell-local history of the search leaves (blueprint line 1859).
At an active cell the global ball filter restricts to the cell-local ball filter (blueprint line 1859).
The restriction to a set keeps the absence of template coordinates.
A relabeling keeps the physical coordinate.
The restriction to a set restricts the physical coordinate.
The embedding of the column space of the basic family (l, j) into the main column space:
its columns are the original basic columns of the slot l (blueprint lines 1676, 1805).
Equations
Instances For
The global basic input of the slot l at the depth h: the fixed signed sum
P_{l,0,h} F_{l,0} - P_{l,1,h} F_{l,1} of the depth projections of the two basic families acting on
their inputs, in the main column space (blueprint prop:base line 1611, line 1859).
Equations
Instances For
The basic input of the slot l on the cell I: the global basic input at the depth of I
restricted to I.
Equations
- bf.basicIn Mc l I = (TrilinearHT.Auto.columnL2Restriction (TrilinearHT.Auto.dyadicGridCell A.G I.1 I.2) ⋯) (bf.gBasic Mc l I.1)
Instances For
At an active cell the basic depth projection restricts to the basic cell projection.
The basic input on an active cell is the fixed signed sum of the basic cell projections of the family inputs.
A basic cell column embeds as the main column of its original label.
An original column of the slot l available at an active cell is the relabeling of a column
of the main tree.
The basic input on an active cell has only relevant main coordinates.
Blueprint line 1859: on an active cell the shared history of a basic B slot is the cell
restriction of the global shared history at the depth of the cell acting on the global basic input
(the fixed signed sum of the basic depth projections of the family inputs F_l), relabeled from
the relevant main labels.
Blueprint line 1859, the leaf outputs of a basic B slot: on an active cell the ball output
Z_{l,G,s} = L_{l,G,s} B_{l,s} B_l is the cell restriction of the global ball filter applied to the
global shared history of the global basic input.
Blueprint line 1859 (the compression loss): rows on the main column space that are Bessel with
constant B and local to active decision cells u_i remain Bessel after inserting, at the depth
of each decision cell, the global shared history of the slot l and the basic depth projection of
the family (l, j) acting on an input Z of the family (e.g. F_{l,j} or 1_R F_{l,j}), at the
cost of the complement compression of the main tree for |ls| factors and the one-factor
compression of the basic tree.
The basic input of a cell has no template coordinates (blueprint line 1805: original labels have rank zero).
The basic input of a cell vanishes off the cell.
On an active cell the basic input is a combination of the original columns of the slot available there (blueprint lines 1611, 1859: the basic guard slot input of prop:localize).
The physical coordinate of the basic input of an active cell is the basic argument B_l on the
cell (blueprint prop:base line 1611).
The zero convention and the retained inherited projections (blueprint line 1859) #
Above the attempt (no active cell contains the cell) the inherited masks of the main tree are empty (blueprint line 1859: before an attempt the outputs are zero).
Between actual uses the inherited projections are retained (blueprint line 1859): at a cell of
the tree whose deepest active ancestor is a, the masks of the main tree are those of a.
Above the attempt the main cell projections vanish.
Blueprint line 1859 (zero convention): on a cell of the depth partition lying above the attempt (contained in no active cell) the global ball outputs vanish.
The compression loss G₀ (blueprint lines 1670, 1859) #
The complement compression for n = O(log k) factors in a column tree with
log (2 budget) ≤ k^c is a small overhead G₀ = exp(C_q (1 + log 2k)^2) (eq:small-overhead).
The one-factor compression constant is at most the complement compression constant for one factor.
Blueprint line 1859, "the compression loss is G₀": the loss of basic_compression for
histories of length n ≤ c (log k + 1) in a main tree and a basic tree with log (2 budget) ≤ k^c
is at most G₀ = exp(C_q (1 + log 2k)^2) with C_q = 4096 (c+1) (1024 (c+1) + c + 7).
The template path count of a catalog is at most the number of main labels at the deepest template birth cell containing the point (blueprint line 1835: the main catalog budget is a path count).
A main budget from catalog counts: if the main labels of rank at most r number at most N at
every active cell, then 8 colBudget + N is a main budget (blueprint lines 1828, 1835).
Equations
Instances For
Certified variation on the main columns (blueprint lem:variation, lines 1861-1879) #
Generic variation lemmas (moved from Sec13_1, Sec13_3 and Sec13_4) #
A depth projection commutes with the restriction to a cell of a coarser depth partition.
A column function (of any label type) vanishing off the root of a depth family splits orthogonally over its depth partition.
A column function vanishing off the root splits orthogonally over a depth partition.
The interval rows of one nested depth family are Bessel (orthogonal increments) and split orthogonally over the partition at their left depth.
One layer of the jump: the change of a single averaged layer between the endpoints, applied to the left history of the preceding layers, is compressed.
Blueprint lines 1886-1888 ("telescope B_t' - B_r', discard left contractions, and use the
changed middle factors as orthogonal rows on [r,t]; compression inserts their right factors"):
the jumps of the global averaged histories over disjoint depth intervals.
The active cells are closed under ancestors below the root.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Rows whose outputs vanish off the root of a depth family and which commute with the
restrictions to its depth-h cells split orthogonally over that partition (the hypothesis of
basic_insert).
Outputs of a restriction vanish off its set.
Depth intervals of naturals shifted by a common offset stay disjoint.
The jumps of a basic depth family over disjoint intervals measured from a deeper root are Bessel.
Certified variation with general histories (blueprint lines 1879-1905, 2149) #
certifiedVariation with the histories B' replaced by arbitrary vectors: the left histories
Br i enter only through the compression estimate for the ball rows, and the right histories
Bt i only through the jump bound Σ_i ‖Bt i - Br i‖² ≤ J. Then
Σ_{G,i} ‖E (L_{t} Bt - L_{r} Br)‖² ≤ 2 C_w (G₀ ‖F‖² + J). This is the form used for the
attempt (blueprint line 2149), whose histories are products of global nested projections.
certifiedVariation_gen for pad averages of ball projections (blueprint line 1883, "couple
individual pad choices across times; Jensen").
Whole endpoint ranges on the main columns (blueprint lines 1777-1789, 1875) #
Group outputs over finer labels V that push forward along lab : V → W, with at most one
label of each fiber present at the point, have the norm of the pushed-forward group output when
the scalars agree at the present labels and the weights agree.
Two occurrences of an original label whose admission cells meet have the same vertex: admission cells of distinct vertices of one label are disjoint.
The vertex-labelled main labels: vertices (original column occurrences) and templates.
Instances For
The main label of a vertex-labelled main label.
Instances For
The vertex-labelled main label of a main label at a cell.
Instances For
The scalars of the vertex-labelled main labels: the chart atom of an available vertex (zero otherwise) and the template atom.
Equations
Instances For
The private weights of the vertex-labelled main labels.
Equations
Instances For
The tag of a vertex-labelled main label (a default beyond the catalog).
Equations
Instances For
A vertex-labelled main label occurs at a cell: an available original column of the slot with that vertex, or a template of the catalog.
Equations
Instances For
The scalar of an occurring vertex-labelled main label is a pure source chart of its tag in the slot, on the whole line (blueprint line 1798: pure main columns).
A downstream actual-use certificate of the group G of color k inside the cell I: an
active cell u ⊆ I with a successful present vertex of color k and group G (blueprint lines
1863, 1876).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint lem:masks, separation clause, for endpoints: tags in the ball masks of distinct
groups of one color on nested certified endpoint cells J ⊆ I are at distance greater than one at
the finer endpoint.
An endpoint occurrence of a vertex-labelled main label for the group G of color k on the
cell I: the cell is active, the label occurs there with its tag in a pad mask of G at a pad at
most H_max, and I carries a downstream use certificate of G (blueprint lem:whole-ranges:
"usable endpoint cells whose masks contain their tags").
Equations
Instances For
Overlapping occurrences of two labels in distinct groups of one color are separated at the finer of the two depths.
The last separating depth of two vertex-labelled main labels among the occurrence depths.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint lem:whole-ranges (lines 1777-1789) for one slot l and color k of the attempt on
the main columns: group outputs built from occurring vertex-labelled main columns (original column
occurrences and templates) with coefficients constant on whole certified endpoint cells, whose
masks contain the tags, are almost orthogonal, ‖Σ_G Z_G‖² ≤ (1 + τ N W₀²) Σ_G ‖Z_G‖² with the
inverse private weights at most W₀² = colBudget², when the edge height dominates the graph
threshold at τ and at most N group-label pairs are present at each point.
A group output with pushed-forward coefficients is the sum of the coefficients times the columns of the image labels.
Finite sums of main columns on cells are, as functions, sums of indicator coefficients times the private column values.