Trilinear Hilbert transform: mainAttemptLift #
Blueprint line 1932 (eq:modes and the lift R_(l,G)) on the main columns of a role: the
augmented modes ψ_m = ζ^ρ e(c_l p_ρ) e(λ_m (y - a)² + γ_m (y - a)) of the first-match
expansions of all primaries Φ at their first-match cells, with private indices distinct across
primaries and branches, and the pointwise linear map with physical coordinate
(ζ^ρ)² F_phys + Σ_Φ F_Φ / √ε_Φ q_Φ (q_Φ = Σ_m a_(Φ,m) (ψ_m)_phys - (ζ^ρ)² φ_Φ on the first-match
branches of Φ, zero before the match) and mode coordinates √ε_m a_(Φ,m) F_Φ / √ε_Φ. The
primary weights are the private weights ε_Φ of the main columns; the mode weights are chosen
locally, ε_m = ε_Φ / (Σ_m' |a_(Φ,m')|² + 1), so that the private map has squared norm at most one
and 1 / ε_m ≤ colBudget² (exp(D X^D)² + 1) (log (1/ε_m) ≤ P^C). The physical correction
satisfies Σ_Φ |q_Φ|² / ε_Φ ≤ δ_c² N colBudget² pointwise, N bounding the main labels at the
cells (δ_c D_m^C); with δ_c² N colBudget² ≤ 1 this is the absolute norm bound of the lift.
The mode budget D_* (blueprint line 1934) #
The clearing integer Q₀ (blueprint lines 1893 and 1934) #
The clearing integer of a rational matrix: the product of the denominators of its entries
(blueprint line 1893: "an integer Q₀ in the main budget clearing C_z").
Equations
- TrilinearHT.Auto.clearInt C = ∏ a : Fin d, ∏ b : Fin d, (C a b).den
Instances For
Groups and main uses along a path (blueprint lines 1728-1730 and 1934) #
The change counter does not decrease from an ancestor to a cell, and when it is unchanged the color data are unchanged.
The groups of the present central vertices along a chain of cells number at most
N_v (potMax + 1): each of the at most N_v vertices of the chain changes its color data fewer
than potMax times (blueprint lines 1728-1730; line 1934: "actual main uses along a path across
groups").
The groups of the attempt with a present central vertex at an active cell containing a point
number at most D (potMax + 1), D the vertex bound (blueprint line 1934: "actual main uses
along a path across groups").
The uniform first-match size and the budget D_* (blueprint line 1934) #
For a nonnegative top score, a ball level j ≤ 4 and a pad p ≤ P, the ball radius is at
most b₁ d₀ + b₁ + bbase 4 + P.
The edge height increases with the radius.
The uniform first-match size of the attempt: the size X of mainFirstMatch_finite at the
largest ball radius b₁ d₀ + b₁ + bbase 4 + P of the four ball levels (blueprint line 1934: the
bounds are uniform in the groups and the branch offsets).
Equations
Instances For
The first-match size of a role is at least one.
The first-match size of a role with a nonnegative top score at a level j ≤ 4 is at most the
uniform size.
The mode budget D_* of the attempt (blueprint line 1934), for the first-match degree D,
the dimension bound d_B, the source complexity H, the precision δ_c, a bound N for the main
labels at one cell, and the parameter k. With B = exp(D X_max^D) and the count
M₁ = B (4 max(1, 4B/δ_c) + 1)^(4 d_B) of the modes of one primary at one branch, it is the sum of
e^k; the modes and main uses of all groups along a path, D (potMax + 1) (N + 1) M₁; the
rational heights of eq:mode-differences; the inverse private weights colBudget² (B² + 1); the
bound H_ed^(d_B²) of the clearing integer Q₀; and the absolute coefficient sums
(√N + 1) colBudget B of the lifted main outputs on normalized cells. It does not depend on the
branch offsets.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint line 1934: the budget D_* dominates e^k, the first-match bound B, the modes of
all groups along a path (D (potMax + 1) groups, at most N matched primaries, at most the
bound of mainAttemptLift modes for each), the main uses along a path (D (potMax + 1) N), the
rational heights, the inverse private weights, the coefficient sums, and the modes of one role at
a point and of one primary at one branch, for a role with a nonnegative top score at a level
j ≤ 4, uniformly in the branch offsets.
The logarithm of the budget D_* in terms of E bounding d_B, log H_ed, log colBudget,
log N and log (1/δ_c): log D_* ≤ 4 (d_B + 1) (L_B + E + 6) + E³ + k + L_p + 2E + 7, where
L_B = D X_max^D and L_p = log (potMax + 1) (blueprint line 1934).
The number of color degrees is at most 5001 k^c when colBudget ≤ exp(k^c).
The logarithm of potMax + 1 for the vertex bound: at most 2 d₀ (2 d₀ + 1) + d₀ + 2E + 9.
The uniform first-match size is at most w^(113c+116), w = 5002 k P, under the standing
bounds of log_modeStar_poly.
log (potMax + 1) ≤ w^(2c+3), w = 5002 k P, when colBudget ≤ exp(k^c).
Blueprint line 1934: log D_* ≤ P^C. For fixed degrees c (of the standing bounds) and D
(of the first-match expansion) there is a degree C such that, whenever L + 6, the dimension
bound d_B, log H_ed, log H, log (1/δ_c), log N and log colBudget are at most k^c
and H_max + 1 ≤ (k P)^c, the budget D_* of the attempt satisfies log D_* ≤ C (k P)^C
(line 1673: "all later bounds polynomial in P, k will be written P^C").
The top score of the group of a present central vertex is nonnegative (blueprint line 1934: the ball radii of the actual groups are at most the uniform radius).
The Fourier expansion of the squared gauge (ζ^ρ)² (blueprint lines 1944 and 2056) #
The periodic branch profile t ↦ b(fract t).
Equations
Instances For
Near any point the periodic profile is a sum of two translates of the profile.
Blueprint line 2056: the squared gauge is, uniformly in w and in the offset, the sum of its
Fourier modes in the box |v|_∞ ≤ 2^(K+1) up to 2B/2^K, with coefficients bounded by one and
B = 7^d A √d^(d+1) for the derivative constant A of order d + 1.
gaugeSq_truncate in every dimension (in dimension zero the gauge is one).
The gauge multiplier on the true supports (blueprint line 1944) #
Blueprint lines 1942-1944 ("slightly enlarge the cutoffs inside each branch region, making them
one on the required supports, and extend by zero at its cuts"): the enlarged cutoff of parameter
δ/2 is one wherever the true cutoff of parameter δ is nonzero (the true cutoff vanishes within
δ of each cut, branchProfile_eq_zero_near_cut) and zero at the cuts. Hence the four true
cutoffs times the four gauge phases e(c_j p_{ρ_j}(y_j)) equal exactly the four true cutoffs times
the smooth periodic multiplier gaugeMult (δ/2) at the torus point.
The full absolute Fourier norm of a smooth 1-periodic function on ℝ^d with supremum bound
B and derivative bound A of order d + 1 (blueprint line 1944: "its Gevrey and absolute
Fourier bounds"): it is the sum of its absolutely convergent Fourier series, and
Σ_v |cHat_v| ≤ 5^d B + 2 · 7^d A √d^(d+1).
The derivative constant of order 2d + 1 of the multiplier (gaugeMult_deriv_le), with
Q₀ and the entry bound C_m as real parameters.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The full Fourier norm bound of the multiplier.
Equations
- TrilinearHT.Auto.gaugeMultNorm d Q0 Cm δ = 5 ^ (d + d) + 2 * TrilinearHT.Auto.gaugeMultTail d Q0 Cm δ
Instances For
The full Fourier norm bound of the squared gauge (ζ^ρ)².
Equations
- TrilinearHT.Auto.gaugeSqNorm d δ = 5 ^ d + 2 * TrilinearHT.Auto.gaugeTail d δ
Instances For
Truncation of a smooth 1-periodic function with its Fourier coefficients: the coefficients
cHat_v are bounded by the supremum bound B, every finite absolute coefficient sum is at most the
full norm bound 5^d B + 2 · 7^d A √d^(d+1), and the Fourier sum over the box
|v|_∞ ≤ 2^(K+1) approximates the function uniformly within 2 · 7^d A √d^(d+1) / 2^K.
Uniformity of the Fourier constants in the center tag (blueprint line 1944) #
The derivative constant of the multiplier increases with the dimension, Q₀ and C_m.
Blueprint lines 1944 and 2055 ("expand (ζ^ρ)² on the ϑ torus with coefficient sum at most
D_* and tail D_*^{-300}"): the squared gauge is approximated uniformly within 2 B_ζ/2^K by its
Fourier sum over the box |v|_∞ ≤ 2^(K+1), and every finite absolute sum of the coefficients is at
most the full Fourier norm gaugeSqNorm.
Size of the Fourier constants (blueprint line 1944: log B_* ≤ P^C) #
The full Fourier norm bound of the multipliers is at most exp(T_G + 2) with
T_G = 12E + (2E + 1)(E³ + κ + 514E + 523) + 2E(2E + 1), κ = log bumpConst, when d_B,
log H_ed and log (1/δ) are at most E.
The full Fourier norm bound of the squared gauge is at most exp(T_S + 2) with
T_S = 2E + (E + 1)(κ + 258E + 515) + E(E + 1), κ = log bumpConst, when d_B and
log (1/δ) are at most E.
The enlarged budget D_* and the common cutoff B_* (blueprint line 1944) #
The height bound of the key differences of the modes of every group (the bound B_σ of
exists_mainModeSystem), max(1, B (1 + 4 (2 d_B + 1) max(1, 4B/δ_c))) at the largest curvature
bound B = exp(D X_max^D).
Equations
Instances For
The heights of the rescaled differences of mode differences (blueprint line 1934: D_* covers
the rational heights of eq:mode-differences and Q₀): 2 (Q₀ (3 B_σ²)²)² + 1 with
Q₀ ≤ H_ed^(d_B²) + 1.
Equations
Instances For
The key heights and the clearing bound are at most modeStar + 1.
Blueprint line 1944 ("enlarge D_* to cover these full Fourier norms, including (ζ^ρ)²"):
the budget modeStar of line 1934 plus the full Fourier norm bounds of the gauge multipliers
(enlarged cutoff δ/2, centers of dimension at most d_B, Q₀ ≤ H_ed^(d_B²), entries at most
H_ed) and of the squared gauge (ζ^ρ)² (cutoff δ).
Equations
Instances For
The enlarged budget dominates e^k, the budget of line 1934 and the two full Fourier norm
bounds.
The uniform truncation constant of the multipliers and of (ζ^ρ)².
Equations
- fp.tailStar dB δ = TrilinearHT.Auto.gaugeMultTail dB (fp.Hed ^ (dB * dB)) fp.Hed (δ / 2) + TrilinearHT.Auto.gaugeTail dB δ
Instances For
The cutoff exponent K_* (blueprint line 1944): the least K with
2^K ≥ 2 (T_* + 1) D_*^300, T_* the uniform truncation constant.
Equations
Instances For
Truncation tails below D_*^(-300): every truncation constant T ≤ T_* gives
2 T / 2^(K_*) ≤ D_*^(-300).
log B_* ≤ 301 log D_* + 3 for B_* = 2^(K_* + 1).
The polynomial size of the Fourier exponents T_G + T_S ≤ (5κ + 4682) E⁴ for E ≥ 1.
Blueprint line 1944: the enlarged budget and the common cutoff satisfy log D_* ≤ P^C and
log B_* ≤ P^C. For fixed degrees c (of the standing bounds) and D (of the first-match
expansion) there is a degree C such that, under the standing bounds of log_modeStar_poly and
0 < δ, δ⁻¹ ≤ exp(k^c), 0 < δ_c, both log D_* and log B_*, B_* = 2^(K_*+1), are at most
C (k P)^C.
Freezing and retention (blueprint line 1967) #
A finite combination of private columns at one point, as a main augmented value.
The labels of the inherited ball masks of a role at a cell whose deepest active ancestor is
a are primaries of the role at a (blueprint lines 1859, 1888 and 1967: between actual uses the
inherited projections are retained).
Blueprint lines 1859 and 1967: on a cell U of a depth partition of the main tree, the
relabeled global ball output of a role vanishes if U has no active ancestor (zero before the
attempt); otherwise it is a combination, with constant coefficients on U, of the main columns
on U of the primaries of the role at the deepest active ancestor a of U (the retained
inherited projections).
The same representation for the basic coarse output Z_{l,G,u} (blueprint lines 1859, 1967).
The restriction of a column vector to a set agrees almost everywhere with the indicator.
An actual use of the group G at a cell (blueprint line 1753: "a group has an actual use
only at a current central assignment"): the cell is active and carries a present central vertex
with successful color data whose group is G.
Equations
Instances For
Blueprint line 1967 (retention rule): the v_b-cells retained for the group G in the block
[b, b + K): the cells of the attempt tree of depth v_b = b - 2K containing a cell with an
actual use of G at a depth of the block.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint line 1967 ("freeze Z_{l,G,u_b}, setting it to zero before the attempt"): the frozen
basic coarse output of the role at the depth u; zero at depths before the attempt root.
Instances For
The frozen output on a cell of the depth partition: zero, or a constant-coefficient combination of the main columns of the primaries at the deepest active ancestor.
Blueprint line 1967 ("a mode available at u_b has first match no later than u_b"): a
first-match cell of a primary at an active cell a that meets a subcell U of a contains U.
Blueprint line 1967 ("the preceding uniform budget applies to these particular endpoint
evaluations, and their coefficients are constant on their u_b-cells"): for a lift with the
exports of mainAttemptLift (on the family of all active cells), on every cell U of the depth
partition at u the lifted frozen output is a combination of augmented modes with coefficients
β_m = c_(Φ(m)) a_m constant on U, supported on the modes alive on U ("a mode available at
u_b has first match no later than u_b"), and Σ_m |β_m| ≤ B √N colBudget ‖Z‖_U / √|U|, where
c are the coefficients of the frozen output on U, B bounds the per-primary coefficient sums
and N the main labels at the active cells.
Blueprint line 1967 ("write ZTilde_(l,G,b) = R_(l,G) Z_(l,G,u_b) on the retained
branches"): the
frozen lifted output of the block b: the lift of the output frozen at u_b = b - 4K, restricted
to the union of the retained v_b-cells.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint line 1967: on a retained v_b-cell J inside a cell U of the depth partition at
u_b = b - 4K, the frozen lifted output ZTilde_(l,G,b) = R_(l,G) Z_(l,G,u_b) is a combination of
augmented modes with coefficients constant on U and supported on the modes alive on U, of
absolute sum at most the budget D_* times the normalized norm of the frozen output on U ("the
preceding uniform budget applies to these particular endpoint evaluations, and their coefficients
are constant on their u_b-cells"). The
lift is any lift with the exports of mainAttemptLift on the family of all active cells, for a
role with a nonnegative top score at a level j ≤ 4.
The main-column mode systems (blueprint lines 1971-1975) #
The lift with its primary labels transported along an equivalence (the mode data, weights and coefficients are unchanged).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The exports of mainAttemptLift (blueprint lines 1932-1940) for one role l, group G with
top score g, ball level j and catalog s, on the family of all active cells: the lift L with
the main private weights, its synthesis of main outputs into augmented modes with physical parts
ψ, the per-primary coefficient sums at most exp(D X^D), first-match cells cellOf and
coefficients constant on them.
- syn (y : ℝ) (β : bf.Lab ⊕ Fin fp.Mc → ℂ) : (∀ (Φ : bf.Lab ⊕ Fin fp.Mc), β Φ ≠ 0 → ∃ I ∈ fp.firstCells A.cells l s G j d Φ, y ∈ dyadicGridCell A.G I.1 I.2) → (L.at_ y) (augmentedMain (fun (Φ : bf.Lab ⊕ Fin fp.Mc) => mainScalar fp.Mc (bf.origCols l) s Φ y) L.εP β) = ∑ m : Md, (β (L.own m) * L.a m y) • augmentedMode (fun (m : Md) => ψ m y) L.εM m
- ind (m : Md) (y : ℝ) : L.a m y = (dyadicGridCell A.G (cellOf m).1 (cellOf m).2).indicator (fun (x : ℝ) => L.a m (dyadicGridLeft A.G (cellOf m).1 (cellOf m).2)) y
Instances For
Blueprint lines 1971-1975 (the frozen-mode data interface) for the lift of mainAttemptLift:
the modes of one role and group of the attempt, with their first-match cells, curvatures, rational
frequency differences and private indices, form a mode system (ModeSystem, primary labels
relabeled by Fin n) whose waves are the physical modes of the lift R_{l,G} and whose private
weights are those of R_{l,G}; the lift has the exports of mainAttemptLift on the family of all
active cells, the corrections of size δ_c and the gauge (ζ^ρ)². The mode system has the tag
z of the group, curvature bound B = exp(D X^D), dimensions at most d_B, inverse private
weights at most colBudget² (B² + 1), and at most
N B (4 max(1, 4B/δ_c) + 1)^(4 d_B) modes through each point and alive at each cell.