Section 15.2: Torus norms and Fourier tests #
This file was automatically generated by Claude.
Formalization of blueprint Section 15, "Common heights and concentration of the core terms"
(sec:core), subsection 2, "Torus norms and Fourier tests" (lines 2482-2583) of
blueprint/formalization_blueprint.tex.
Torus norms and Fourier tests (blueprint lines 2482-2585) #
Torus norms and Fourier tests (blueprint lines 2482-2585) #
Blueprint eq:Haar-four (lines 2497-2502): on a rational connected subtorus 𝓗, for a
multiplier bounded by W,
∫_{𝓗²} K(u,v) Π_j |h_j(u + (j - l') v)| ≤ W Π_j ‖h_j‖_{L²(𝓗)}; this is eq:absolute with all
four exponents equal to two. The zero-dimensional torus is included.
Blueprint lines 2568-2572: for a fixed assignment of the failures, Hölder with m₀ ≥ 1
factors and the deterministic bound give
E Π_j a'_j ≤ C^{m₀} ((2δ)^n)^{1/m₀} Π_j σ_j from a'_j ≤ C σ_j and
E (a'_j)² ≤ C (2δ)^{n_j} σ_j² with Σ_j n_j = n (here ρ = 2δ, C ≥ 1).
Many four-step paths (lem:sparse-count, blueprint lines 2608-2609) #
The codegree of two first-part vertices in a bipartite edge set.
Instances For
The first-part neighborhood of a second-part vertex.
Instances For
Four-step paths a - y₁ - x - y₂ - a' in a bipartite edge set.
Equations
Instances For
Edge count through neighborhoods.
Pairs of a neighborhood with a property, summed over the second part, count codegrees.
Torus norms (frequency-tests, eq:torus-size, blueprint lines 2482-2495) #
Blueprint lines 2487-2490 (cell averages against Haar norms): for a trigonometric sum
g(t) = Σ_k c_k e^{i φ_k t} on the normalized cell [0,1] whose frequency differences are tiny
(|φ_k - φ_{k'}| ≤ ε) on the related pairs and huge (|φ_k - φ_{k'}| ≥ 2/ε) otherwise, the cell
average of |g|² differs from the coset sum Σ_{k ~ k'} c_k cBar_{k'} (its Haar norm on the
annihilator torus) by at most ε (Σ_k |c_k|)².
Blueprint lines 2487-2490 (Haar side of eq:torus-size): on the annihilator torus of a
rational space, ∫ |Σ_k c_k χ_k|² = Σ_{k - k' ∈ K_B} c_k cBar_{k'}.
The reference data of a tested four-core tuple at scale R: box shifts n, m with
q' = Σ x_r + 36 n·ζ, t' = Σ r x_r + 36 m·ζ, |q'|, |t'| ≤ ν R and
|t' - j q'| ≥ μ R for every line j (blueprint eq:four-tests).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The side window of a tested tuple (blueprint line 2564, b_Λ): the integer frequencies k
with |k - r(Q + 36 n·ζ)| ≤ 2Λ for some box shift |n| ≤ B, where Q = Σ x_r. The window
energies sideWinE pair the side with e(+k y / r), so the index k here is -k in the
blueprint's |k + r(Q + n·ξ)| ≤ 2Λ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Torus sizes (blueprint lines 2483-2495, eq:torus-size) #
Blueprint eq:torus-size (lines 2489-2495): if the squared Haar norm is at most the cell
average X plus ε (Σ_D s_D)² (cell_average_close, haar_norm_sq_eq), the cell average is at
most 2 Σ_D ‖A_D‖² (almost orthogonality of minimal CURRENT components), at most D_* components
are selected and ε ≤ D_*^{-100}, then
a' ≤ √2 (Σ_D (‖A_D‖ + D_*^{-30} s_D)²)^{1/2}.
Fourier decay of the normalized kernel (blueprint lines 2526-2534) #
Uniform Fourier decay of a smooth function vanishing outside [-R, R]:
(1 + |q|^J) ‖𝓕 f q‖ ≤ 2 R (A₀ + (2π)^{-J} A_J) when |f| ≤ A₀ and |f^{(J)}| ≤ A_J.
The bounds of a normalized kernel at unit scale: smooth, vanishing outside [-R, R]², with
line derivatives in each variable bounded by A m.
Instances For
The phase-weighted kernel on ℝ × ℝ (in the order (s, x)) is integrable.
The sheared slices u ↦ w(u - j s, s) and their phase-weighted product integrability.
Blueprint lines 2529-2533 (zeros on the lines t = j q and smoothness near them): if the
marginals ∫ w(u - j s, s) ds vanish, then near the line,
(1 + |q|^J) |WFourier(q, j q + δ)| ≤ 2R · 2πR|δ| · 2(R + |j|R) (A₀ + (2π)^{-J} A_J).
Blueprint lines 2526-2534 (|WFourier_s(r q', r t')| ≤ C_J μ ν^{-J}): if the marginals along
the
lines t = j q, j ∈ L (|j| ≤ J_b), vanish, then with μ = min(1, min_j |t - j q|) and
ν = max(1, |q|, |t|), |WFourier(q, t)| ν^J ≤ C μ for an explicit C depending only on R, J_b
and the derivative bounds.
Blueprint lines 2522-2534: the unit-scale admissible kernel W_s has the bounds of a
normalized kernel, uniformly over the kernel class.
Blueprint line 2529 ("the four marginals give zeros of WFourier_s(q,t) on the four lines
t = j q"): the unit-scale kernel has vanishing marginals along the four lines.
Blueprint lines 2526-2534 for the admissible kernels: |WFourier_s(q, t)| ν^J ≤ C_J μ with
μ = min(1, min_{0 ≤ j ≤ 3} |t - j q|), ν = max(1, |q|, |t|), uniformly over the class.
Four-core tests: coset reduction (blueprint lines 2506-2529) #
Characters are integrable on the annihilator torus (a probability space).
Blueprint line 2524 ("their frequencies differ by a tiny quantity, so replace the Fourier values
by the reference value"): the kernel transform is Lipschitz,
|WFourier(q, t) - WFourier(q₁, t₁)| ≤ (2R)² A₀ · 2πR (|q - q₁| + |t - t₁|).
Blueprint line 2526 (the retained coset coefficient is bounded by C Π_j a'_j by
eq:Haar-four): for a bounded continuous multiplier R, continuous g_j on 𝓗 and a unimodular
continuous weight χ,
|∫∫_{𝓗²} R(u, v) Π_j g_j(u + (j - l) v) χ(u, v)| ≤ W Π_j ‖g_j‖_{L²(𝓗)}.
Blueprint lines 2522-2523 ("its characters sample WFourier_s at r(Q + n·ξ, T + m·ξ)"): the
normalized local form of an integrable kernel against a linear phase e(A x + B t + C) is a value
of the Fourier transform of the unit-scale kernel,
r⁻² ∫ w(z) e(A z₁ + B z₂ + C) = e(C + A (a₀ + r/2)) WFourier(-r A, -r B).
Three-core tests (blueprint lines 2536-2565) #
Blueprint lines 2540-2542 and 2553-2556 (the anchor function and the pairing entries): with
anchor l and |l| ≤ J_b, a kernel transform bounded by C μ ν^{-(J + A)} (decay_lines, with
the line t = l q among the zero lines) has, at (κ, β + l κ),
|WFourier(κ, β + lκ)| ≤ C (J_b + 2)^{J + A} min(1, |β|) max(1, |β|)^{-J} max(1, |κ|)^{-A}.
The L² norm of a continuous function on the annihilator torus.
Blueprint lines 2545-2547 (‖D_m‖₂ ≤ C Π_{j ≠ l} a'_j by duality and eq:Haar-four): for the
slice D_m(u) = ∫ D(u, v) e(-m·v) dv of D(u, v) = R(u, v) Π_{j ≠ l} g_j(u + (j - l) v),
‖D_m‖_{L²(𝓗)} ≤ W Π_{j ≠ l} ‖g_j‖_{L²(𝓗)}.
Side windows (blueprint lines 2549-2562, eq:side-windows) #
One shell of eq:side-windows (lines 2553-2556: "in a shell of radius Λ, each row and
column has O(Λ) entries, since both the integers and the reference frequencies are separated"):
Σ_{|k + f_n| ≤ R} |a_n| |b_k| ≤ (2R + 2) ‖a‖₂ ‖b‖_{ℓ²(W_R)}, W_R the window of k within R of
some -f_n.
The dyadic majorant of (1 + x)^{-(A+2)}:
(1 + x)^{-(A+2)} ≤ 2^{A+2} Σ_{i ≤ I} 2^{-i(A+2)} 1[x ≤ 2^i] + 2^{-I(A+2)} for x ≥ 0.
Blueprint eq:side-windows (lines 2553-2562): for a pairing matrix with entries
|M_{n,k}| ≤ C (1 + |k + f_n|)^{-(A+2)} against 1-separated reference frequencies f_n,
`|Σ_{n,k} a_n b_k M_{n,k}| ≤ C 2^{A+4} Σ_{Λ = 2^i ≤ 2^I} Λ^{-(A+1)} ‖a‖₂ b_Λ
- C 2^{-I(A+2)} Σ|a_n| Σ|b_k|
, withb_Λtheℓ²norm ofbon the windowW_Λ`.
Failure assignments and the principal core (blueprint lines 2566-2585) #
Continuous functions on the annihilator torus are integrable.
Blueprint lines 2547-2549 ("collect horizontal Fourier coefficients by cosets and choose one
reference n per coset; Parseval bounds their ℓ² norm"): for references n in distinct cosets
of K_B ∩ ℤ^d, the Haar coefficients ⟨f, χ_n⟩ of a continuous function on the annihilator torus
satisfy Bessel's inequality Σ_n |⟨f, χ_n⟩|² ≤ ‖f‖²_{L²(𝓗)}.
The dual slice D_m(u) = ∫ D(u, v) e(-m·v) dv of
D(u, v) = R(u, v) Π_{j ≠ l} g_j(u + (j - l) v) (blueprint lines 2543-2546).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint eq:side-windows (lines 2543-2562) for a three-core test with anchor l and
reference m: the horizontal coset coefficients a_n = ⟨D_m, χ_n⟩ at references n in distinct
cosets have ℓ² norm at most W Π_{j ≠ l} a'_j (torus_bessel, dual_slice_bound); against a
pairing matrix with entries |M_{n,k}| ≤ C (1 + |k + f_n|)^{-(A+2)} and 1-separated reference
frequencies f_n, the pairing is at most
C 2^{A+4} Σ_{Λ = 2^i ≤ 2^I} Λ^{-(A+1)} (W Π_{j ≠ l} a'_j) b_Λ + C 2^{-I(A+2)} Σ|a_n| Σ|b_k|.
Blueprint lines 2568-2572 ("apply the probability bound separately to each minimal-component
summand ... dropping extra success requirements only enlarges its probability"): over the words
w ∈ H^n of failed heights, the components K of role j failing at every height assigned to
j carry total weight at most ρ^{n_j} |H|^n Σ_K σ_K when each component is bad at a proportion
at most ρ of H.
The uniform average over the words w ∈ H^n as a measure on Fin n → ℕ.
Equations
- TrilinearHT.Auto.wordAvg H n = ∑ w ∈ Fintype.piFinset fun (x : Fin n) => H, (↑H.card ^ n)⁻¹ • MeasureTheory.Measure.dirac w
Instances For
Blueprint lines 2568-2572 averaged over the words of failed heights: if the role sizes
a'_j(w) satisfy a'_j ≤ C σ_j on the words and their averaged squares are at most
C ρ^{n_j} σ_j², then the averaged product is at most C^{m₀} (ρ^{Σ n_j})^{1/m₀} Π_j σ_j
(Hölder with m₀ factors, core_moment_bound).
An admissible local kernel is integrable (it is continuous with compact support).
The anchor function W_B(y) = ∫ w(y - l t, t) e(B t) dt of a kernel (blueprint lines
2540-2542).
Equations
Instances For
Blueprint lines 2519-2523 with the numerical errors of eq:core-numerical: if on the kernel
support the product of the inputs is within ε of a finite phase sum
Σ_p C_p e(A_p (z₁ - x₀) + B_p z₂), the local form is within 2 ‖w‖_∞ ε of
Σ_p C_p e(A_p (a₀ + r/2 - x₀)) WFourier(-r A_p, -r B_p).
The character expansion of D(u, v) = R(u, v) Π_j g_j(u + (j - l) v) for trigonometric
polynomials R = Σ_q r_q χ_{q₁}(u) χ_{q₂}(v) and g_j = Σ_k a_{j,k} χ_{n_{j,k}} on the torus
(blueprint lines 2519-2523): the sum over (q, k) of r_q Π_j a_{j,k_j} times the characters
χ_{q₁ + Σ_j n_{j,k_j}}(u) χ_{q₂ + Σ_j (j - l) n_{j,k_j}}(v).
coset_sum_eq_haar for a trigonometric polynomial indexed by an arbitrary finite set with a
frequency map.
four_core_test for a trigonometric expansion indexed by an arbitrary finite set with a
frequency map fr (no merging of equal frequencies needed).
Blueprint lines 2519-2523 (four cores, anchor l' = 0): if on the kernel support the product
of the inputs is within ε of e(Σ_j γ_j (y_j - x₀)) D(ξ(x - x₀), ξ t) for the torus
trigonometric polynomial D(u, v) = R(u, v) Π_j g_j(u + j v), then the local form is within
2 ‖w‖_∞ ε of Σ_x C_x e(A_x (a₀ + r/2 - x₀)) WFourier(-r A_x, -r B_x) over the expansion of D
(four_product_expand), with A_x = Σ_j γ_j + P₁(x)·ξ and B_x = Σ_j j γ_j + P₂(x)·ξ.
Blueprint lines 2519-2531 (the four-core test on a cell): under the hypotheses of
four_core_physical, if the kernel samples K_x = e(A_x (a₀ + r/2 - x₀)) WFourier(-r A_x, -r B_x) are
within ε of a reference value K₀ on the reference coset p₀ + K_B² of the expansion
frequencies and at most τ off it, and the torus multiplier is bounded by W on 𝓗², then
|Λ| ≤ 2 ‖w‖_∞ ε_ph + |K₀| W Π_j ‖g_j‖_{L²(𝓗)} + max(ε, τ) Σ_x |C_x|.
Blueprint lines 2489-2493 ("the physical norm is bounded by the augmented one"): the cell integral of the squared physical combination is at most the squared norm of the augmented combination.
The cell integral of the squared physical combination of waves is at most the squared norm of the combination of cell modes.
Blueprint eq:torus-size (lines 2482-2495) for one role on the cell: with anchor shift
s₀ = a₀ - x* (|s₀| ≤ r), if the frequency differences 2π r (n_k - n_{k'})·ξ of the
trigonometric polynomial g = Σ_k c_k χ_{n_k} are at most ε on the relation n_k - n_{k'} ∈ K_B
and at least 2/ε off it (eq:gap), its normalized cell average
∫₀¹ |g(ξ(s₀ + r t))|² dt is at most X ≤ 2 Σ_D ‖A_D‖², at most D_* components are selected
with coefficient sums covering Σ_k |c_k|, and 2ε ≤ D_*^{-100}, then
‖g‖_{L²(𝓗)} ≤ √2 (Σ_D (‖A_D‖ + D_*^{-30} s_D)²)^{1/2}.
The sheared kernel w(y - l t, t) vanishes unless y lies in the cell and |t| ≤ r, and then
all progression points y + (j - l) t lie in the cell.
Blueprint lines 2549-2556 ("expand S' in normalized Fourier coefficients ... the matrix of
pairings"): for a continuous function G with G(a) = G(a + r) and summable Fourier coefficients
on [a, a + r) and an integrable S there, the pairing ∫ S G is the convergent sum over
k ∈ ℤ of GFourier(k) ∫ S(y) e(k y / r) dy.
The anchor function as an integral over [-r, r].
Blueprint lines 2540-2556 (the pairing entries): the Fourier coefficient of
G(y) = e(α (y - x₀)) W_β(y) on the cell [a₀, a₀ + r) at k is
r e(-α x₀ + A (a₀ + r/2)) WFourier(-r A, -r (l A + β)) with A = α - k/r.
The kernel decay constant at order two of admissible_kernel_decay'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Order-two decay of the unit kernel transform: |WFourier(q, t)| ≤ C₂ max(1, |q|)^{-2}.
Blueprint lines 2549-2556 for one tuple term: the anchor pairing
r⁻² ∫ S(y) e(α (y - x₀)) W_β(y) dy of a function integrable on the cell is the convergent sum over
k ∈ ℤ of r⁻¹ e(...) WFourier(-r(α - k/r), -r(l(α - k/r) + β)) s_k, s_k = ∫_I S(y) e(k y/r) dy.
The decay constant of order J of admissible_kernel_decay.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Decay of order J: |WFourier(q, t)| max(1, |q|, |t|)^J ≤ C_J.
Blueprint lines 2523-2526 ("other cosets have rapidly decreasing Fourier tails") summed over
the cell frequencies: if |b| ≥ 4 and J ≥ 2, then
Σ_k |WFourier(k - c, l (k - c) - b)| ≤ 12 C_J (4/|b|)^{J-2}.
Blueprint lines 2523-2526 ("their frequencies differ by a tiny quantity, so replace the
Fourier values by the reference value") summed over the cell frequencies: with the Lipschitz
constant L_W of the unit kernel transform and δ = 4|c - c'| + |b - b'|,
Σ_k |WFourier(k - c, l(k - c) - b) - WFourier(k - c', l(k - c') - b')| ≤ 24 √(L_W δ C₄).
Σ_k |WFourier(k - c, l(k - c) - b)| ≤ 12 C₂.
Blueprint lines 2543-2549 ("only the reference m coset contributes ... collect horizontal
Fourier coefficients by cosets"): if R(u, v) Π_{j ≠ l} g_j(u + (j - l) v) has the character
expansion Σ_x C_x χ_{n_x}(u) χ_{m_x}(v) on 𝓗², the Haar coefficient of the dual slice D_{m₀}
at n is the coset sum Σ_{n_x ∈ n + K_B, m_x ∈ m₀ + K_B} C_x.
The normalized anchor pairing r⁻² ∫ S(y) e(α (y - x₀)) W_β(y) dy.
Equations
- TrilinearHT.Auto.anchorP r w l S x₀ α β = (↑r)⁻¹ ^ 2 * ∫ (y : ℝ), S y * (↑(Real.fourierChar (α * (y - x₀))) * TrilinearHT.Auto.anchorFn w l β y)
Instances For
The pairing of one tuple term against a reference: the anchor pairings differ by at most
r⁻¹ ‖S‖_{L¹(I)} Σ_k |K(k) - K'(k)|.
The norm of one anchor pairing: at most r⁻¹ ‖S‖_{L¹(I)} Σ_k |K(k)|.
Near vertical cosets: the kernel samples at (α, β) and the reference (α', β') differ in
total by at most 24 √(L_W δ C₄) + 12 π r|α - α'| C₂ (with x₀ in the cell).
The entry constant of the three-core pairing matrix:
C_{J+A+2} 5^{J+A+2} 2^{A+2} min(1, |b|) max(1, |b|)^{-J}.
Equations
Instances For
Blueprint lines 2553-2556 (|M_{n,k}| ≤ C_{J,A} μ ν^{-J} (1 + |k + r(Q + n·ξ)|)^{-A}): the
kernel samples of the anchor pairing at (α, β) satisfy
|K(k)| ≤ entryC (1 + |k - r α|)^{-(A+2)} with μ, ν built from r β.
The windows of the reference frequencies: the integers within 2^I of some r α_n.
Equations
Instances For
Blueprint eq:side-windows (lines 2543-2562) for the reference terms of a three-core test:
with Haar coefficients a_n = ⟨D_{m₀}, χ_n⟩ at 1-separated reference frequencies r α_n,
|Σ_n a_n P(α_n, β₀)| is at most the window bound of three_core_windows over the windows of
the references plus the tail 12 C_ent 2^{-IA} ‖S‖_{L¹(I)} Σ_n |a_n|.
Blueprint lines 2523-2549 for the three-core tuple terms: collecting the tuple terms by the
vertical reference coset m₀ + K_B and horizontal reference cosets, the sum
Σ_x C_x P(α_x, β_x) equals Σ_{n ∈ N} a_n P(α_n, β₀) plus the near differences and the far
terms, where a_n is the Haar coefficient of the dual slice D_{m₀} at n.
The near-coset reduction error per unit coefficient (anchorK_near with both frequency
differences at most ε₁).
Equations
- One or more equations did not get rendered due to their size.
Instances For
form_anchor_phase_approx for an anchored form r⁻² ∫ w(z) F(z) S(z₁ + l z₂) dz with a
general core factor F (e.g. the core product times the side gauge).
Blueprint lines 2537-2545 (three cores, anchor l): the four-slot torus expansion re-anchored
at u = U + l V. On the physical side,
e(Σ_j γ_j (y_j - x₀)) R(U, V) Π_j g_j(U + j V) = Σ_x C_x e(A_x (y_l - x₀) + (B_x - l A_x) t);
on the torus, R(u - l v, v) g_l(u) Π_{j ≠ l} g_j(u + (j - l) v) has the character expansion
with frequencies (P₁(x), P₂(x) - l P₁(x)).
The torus side of reanchor_physical.
Indicators of the half-open cell may be dropped in the local form of the cell.
The kernel sample of the four-core test at real frequencies (A, B).
Equations
- TrilinearHT.Auto.fourK a₀ r w x₀ A B = ↑(Real.fourierChar (A * (a₀ + r / 2 - x₀))) * TrilinearHT.Auto.kernelFT (TrilinearHT.Auto.unitKernel a₀ r w) (-(r * A)) (-(r * B))
Instances For
Blueprint lines 2523-2526 (reference value on the coset): if r|A - A'|, r|B - B'| ≤ ε₁ and
x₀ lies in the cell, the four-core kernel samples differ by at most
(π C₀ + 2 L_W) ε₁ with C₀ = kerC 0 and L_W the Lipschitz constant of the unit kernel.
Blueprint lines 2523-2526 (other cosets have rapidly decreasing Fourier tails): if
r|A| ≥ H or r|B| ≥ H with H ≥ 1, the sample is at most C_J H^{-J}.
Blueprint lines 2523-2526 (the reference coset of a tested four-core tuple): if the expansion
frequencies on the reference coset are within ε₁/r of the reference (A₀, B₀) and off it at
distance at least H/r in one coordinate, with a moderate reference r|A₀|, r|B₀| ≤ U and
H - U ≥ 1, then the kernel samples satisfy the coset hypotheses of the four-core test with
ε = (π C₀ + 2 L_W) ε₁ and τ = C_J (H - U)^{-J}.
The horizontal torus frequency of a term of the four-core expansion
(multiplier frequency L v₁ plus the four role frequencies Q₀ L v_j + n_{j,k}).
Equations
- TrilinearHT.Auto.expP1 L QL n x = (↑L • fun (a : Fin d) => x.1 (Fin.castAdd d a)) + ∑ j : Fin 4, (↑QL • (x.2 j).1 + n j (x.2 j).2)
Instances For
Blueprint lines 2482-2486 ("for every character difference needed below, r n·ξ is tiny if
n ∈ K_B and huge otherwise"): for the tiny span K_B of the pure frequency vector ϑ of a
nonexceptional primary (gap eq:gap at height H), an integer vector of height at most H in
K_B ∩ ℤ^d is tiny, and one outside is huge.
Blueprint lines 2566-2582 (the core terms over failure histories): if, for every trial count,
assignment, failed word and final height, the masked tuple sum is at most a principal quantity
Ψ plus the per-tuple numerical errors e, and the averages of Ψ over the words and final
heights obey the moment bound C (ρ^n)^{1/m₀} Z (word_moment_bound), then with
m₀ ρ^{1/m₀} < 1 the full
tuple sum is at most C Z / (1 - m₀ ρ^{1/m₀}) + Σ_r e_r (each pure tuple has first-success
weight one, first_success_masked; the assignments are summed as in
assignments_total).
word_moment_bound for nonnegative real role sizes.
Blueprint lines 2568-2575 (Hölder with m₀ factors over the words, then the final heights):
if the principal quantity of a word and final height is Σ_p c_p Π_j a'_{j,p}(w) with role sizes
a'_{j,p} ≤ 2 σ_{j,p} and word averages of a'_{j,p}² at most 2 ρ^{n_j} σ_{j,p}², then its
average over the words and final heights is at most 2^{m₀} (ρ^n)^{1/m₀} Z, with
Z = Σ_h |H|⁻¹ Σ_p c_p Π_j σ_{j,p}.
Summing over the class tuples of the members of each class tuple recovers the full sum.
The local form integrand of measurable inputs bounded on the cell is integrable.
The height of a vector padded by zeros in front.
Blueprint lines 2482-2484 ("a successful component contains a nonexceptional primary; apply
its gap eq:gap to pure ϑ shifts"): the gap of a frequency vector Θ = (θ_v, ϑ) at height H
restricts to pure ϑ shifts of height at most H.
Entries of the four-core expansion frequencies are bounded by the box and shift sizes.
The anchored side function e(-c_l p_ρ(y)) f_l(y) of the three-core reduction.
Equations
- TrilinearHT.Auto.sideSd z ρ l g y = ↑(Real.fourierChar (-(↑(TrilinearHT.Auto.slotCoeff l) * TrilinearHT.Auto.centerPhase z ρ y))) * g y
Instances For
The truncated torus input Σ_{(v, k) ∈ B × F_j} cc_v c_k χ_{QL v + n_k} of a role.
Equations
- TrilinearHT.Auto.coreG QL Bx F c n cc j u = ∑ p ∈ TrilinearHT.Auto.frequencyBox d Bx ×ˢ F j, cc j p.1 * c j p.2 * TrilinearHT.Auto.torusCharacter (↑QL • p.1 + n j p.2) u
Instances For
The truncated torus multiplier Σ_q cm_q χ_{L q'}(u) χ_{L q''}(v).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The re-anchored multiplier R(u - l v, v) g_l(u) on the annihilator of K ∩ ℤ^d.
Equations
- TrilinearHT.Auto.coreRA V L QL Bx F c n cc cm l uv = TrilinearHT.Auto.coreR L Bx cm (↑uv.1 - ↑↑l • ↑uv.2) ↑uv.2 * TrilinearHT.Auto.coreG QL Bx F c n cc l ↑uv.1
Instances For
Jensen for the square root on a probability space: E √X ≤ √(E X).
Bessel's inequality for the cell Fourier coefficients of a square-integrable side function:
Σ_{k ∈ s} |∫_I S(y) e(k y / r) dy|² ≤ r ∫_I |S|² (blueprint lines 2556-2560, the side windows
b_Λ).
The branch phase is jointly measurable in the offset and the point.
The anchored side function is jointly measurable in the offset and the point.
Blueprint lines 2556-2560 (the side window energies b_Λ² before the offset average): for a
measurable side function, square integrable on the cell, the window energy
X(ρ) = Σ_{k ∈ K} |∫_I S'_ρ(y) e(k y / r) dy|² of the anchored side is integrable in the fresh
offset and at most r ∫_I |f_l|² for every offset.
The truncated torus input of a role factors as (truncated cutoff) × (input polynomial).
Blueprint lines 2487-2495 (eq:torus-size for the truncated inputs): if the truncated cutoff
of role j is at most M on the torus, the L²(𝓗) norm of the truncated torus input is at most
M times that of the input polynomial Σ_k c_k χ_{n_k}.
offset_average_sqrt with several square-root terms and an almost-everywhere bound: if
F ≤ 2 E Φ and Φ ≤ a + Σ_i b_i √X_i almost everywhere, then F ≤ 2 (a + Σ_i b_i √(E X_i)).
Blueprint line 2482 ("a successful component contains a nonexceptional primary"): a good
mode's CURRENT component carries a primary label that is good (goodP h).
Blueprint lines 2482-2486 (frequency tests): the gap eq:gap of a nonexceptional primary
Θ = (θ_v, ϑ) at height H (thresholds T⁻¹/r_v and T/r_t), applied to pure ϑ shifts,
makes r n·ξ (with ξ = ϑ/L, r_t ≤ r ≤ r_v) tiny (≤ T⁻¹/L) for integer n of height at
most H in the tiny span K_B and huge (≥ T/L) otherwise.
Blueprint lines 2512-2534 (eq:four-tests, the kernel factor of the four-core test): at the
reference frequencies (q', t') the kernel sample satisfies |WFourier_s(r q', r t')| ν^J ≤ C_J μ with
μ = min(1, min_{0 ≤ j ≤ 3} r|t' - j q'|) and ν = max(1, r|q'|, r|t'|) (the four marginals
give zeros on the lines t = j q).
The core index data of a three-core tuple with side role l, the side carried as one trivial
term (none, the convention of three_core_principal).
Equations
- TrilinearHT.Auto.sideOptF l F j = if j = l then {none} else Finset.map Function.Embedding.some (F j)
Instances For
The four-core test quantity μ = min(1, min_{0 ≤ j ≤ 3} r |t' - j q'|) of eq:four-tests.
Equations
- TrilinearHT.Auto.fourMu r A B = min 1 ((Finset.image (fun (j : Fin 4) => ↑↑j) Finset.univ).inf' TrilinearHT.Auto.fourMu._proof_1 fun (j : ℝ) => r * |B - j * A|)
Instances For
Blueprint lines 2566-2569 (discarded four-core tuples): if the inner minimum is below U₀⁻¹
(μ ≤ U₀⁻¹) or no reference lies in max(|q'|, |t'|) ≤ U₀ R_s (ν ≥ U₀), the kernel sample at
the reference is at most C_J U₀⁻¹ (fourK_mu_nu with J ≥ 1).
A fixed choice of an element of a finite set (the default if empty).
Equations
- TrilinearHT.Auto.finPick S = if h : S.Nonempty then Exists.choose h else default
Instances For
The reference of the coset of v modulo K among the frequencies P: a fixed member of P
in the same coset (blueprint line 2547, "choose one reference n from the box per coset").
Equations
- TrilinearHT.Auto.cosetRep K P v = TrilinearHT.Auto.finPick ({u ∈ P | v - u ∈ K})
Instances For
The value of one slot of a pattern at one index: the component subtotal in a core slot, the
pattern piece otherwise (compSlot at a single slot).
Equations
Instances For
Blueprint lines 2463-2582 for one pattern on a leaf cell and group (core slots expanded into
their components, sides and errors fixed): the pattern form is at most
C Z / (1 - 4 ρ^{1/4}) + Σ_r e_r if for every failure history (n, a, w, h) the forms of the
masked slot sums grouped by the final-height classes cls h are at most principal quantities
Ψ_p plus the errors of their member tuples, and the history averages of Σ_p Ψ_p obey the
moment bound (first_success_bound, multilinear_regroup).
Distinct minimal components of a block on a pre-cell are disjoint.
The class of a minimal component is the CURRENT component of any of its modes.
Blueprint lines 2576-2582 and 2775-2776 ("after fixing ... the dyadic amplitude and frequency bins ... a uniform per-bin estimate suffices"): if every term is at most the value of its bin, the sum is at most the sum over the occupied bins of the bin value times the number of terms in the bin.
The frequency dichotomy on the side states (blueprint lines 2483-2487) #
The tiny-span smallness eq:mode-parameters at the chosen schedule: the spanning constant of
the tiny span of a chart of dimension at most d_max times the tiny threshold T⁻¹/r_{v_b} is
below the large threshold T/r_{t_b} (Valid.tinySpan_small).
Blueprint lines 2483-2487 on a leaf cell I of the side states: a mode good at a height h
for the block components on the pre-cell lies in a CURRENT component carrying a nonexceptional
key p ("a successful component contains a nonexceptional primary"); its gap eq:gap, applied to
pure ϑ shifts, makes |I| n·ξ (ξ = ϑ / L) tiny (≤ T⁻¹/L) for every integer n of height at
most H in the rational tiny-frequency space K_B and huge (≥ T/L) otherwise.
Sixteen times the frequency box is below H (blueprint lines 2483-2487: "apply its gap to
pure ϑ shifts in all the boxes under consideration"; differences of the four-core expansion
frequencies): 16 D_*^5 E_h < H for h ≤ J_*.
Blueprint lines 2483-2487 for every character difference needed below: at the chosen schedule
(S.Valid, side parameters S.sideParams δ_*), on a leaf cell I and for a mode good at a final
upper height h with predecessor height h - Δ, every integer frequency n with
|n|_∞ ≤ 16 B'_{h-Δ} = 16 D_*^5 E_{h-Δ} (all the boxes under consideration) has |I| n·ξ
tiny if n ∈ K_B and huge otherwise
(ξ = ϑ / L_{h-Δ}, K_B the rational tiny-frequency space of a nonexceptional key of the
successful component). The torus 𝓗 = (K_B ∩ ℤ^d)^⊥ is connected with exact character integrals
(rationalAnnihilator).