Trilinear Hilbert transform: three_core_tuple_bound #
Blueprint eq:core-numerical (lines 2562-2567) for a three-core tuple on a leaf cell of the
side states, side role l and side column X (enlarged gauge cutoff δ/2, truncation tails at
most D_*^{-300}, full Fourier norms at most D_*, J ≥ 3, windows up to 2^{I_w} ≥ U₀/2): the
cell form is at most the principal window quantity threePrin if the tuple passes the three-core
test, and 0 if it is discarded, plus the absolute error
C_{J,A} D_*^{-100} Π_{j ≠ l} Σ_{F_j} |α| σ
with the local side size σ = (r⁻¹ ∫_I |S_phys|²)^{1/2} as extra factor. Discarded tuples:
|β| < U₀⁻¹ gives C_{J,A} μ ν^{-J} ≤ C_{J,A} U₀⁻¹ (entryC_le_min), and no reference gives all
anchored frequencies far (three_core_noref_side).
Moments of the core torus sizes over the failure histories (blueprint lines 2569-2577) #
role_moments with an arbitrary constant c: if for every word w ∈ H^n the role size is at
most c (Σ_K b_K)^{1/2} over the K ∈ T failing at all heights assigned to the role, and every
K ∈ T is bad at a proportion at most ρ of H, then A(w) ≤ c (Σ_T b)^{1/2} and the word
average of A² is at most c² ρ^{n_j} Σ_T b.
The minimal PRE component of a core mode is a core component.
The modes of a core component are core.
A minimal component lies in the minimal CURRENT component of any of its modes.
A minimal component inside a minimal CURRENT component has that component as its class at
height 0.
Blueprint lines 2569-2572 ("apply the probability bound separately to each minimal-component
summand in eq:torus-size"): when the selected modes F are the core modes of entire minimal
CURRENT components inside F_h(x), each satisfying P, the sum of eq:torus-size is at most the
sum of the summands of eq:component-size over the minimal CURRENT components satisfying P.
The components of a core slot at a cell are the core components of its pre-cell.
The final class F_h(m) of a mode of the role j (blueprint line 2467), as a set of
modes.
Equations
- D.finCls G I j h m = Finset.map { toFun := Subtype.val, inj' := ⋯ } (((D.Ms j G).blockComps D.S ⋯ (A.blkStart D.S.K I.1) (D.preAt I)).F h m)
Instances For
The masked components of a core role j with final class F (blueprint lines 2466-2467 and
2569): the core components of the cell in the role mask of the assignment asg of the failed
trials, the failed word w and the final height h, whose final class at h is F.
Equations
Instances For
The selected modes of a core role with final class F (blueprint line 2569): the alive modes
of its masked components.
Equations
Instances For
The goodness at a height t of a minimal CURRENT component U of a core role: every core
component of the cell inside U is good at t.
Instances For
The summand of eq:component-size of a minimal CURRENT component U of the role j:
(‖A_U‖_{2,I} + D_*^{-30} Σ_{m core in U} |α_m|)².
Equations
- One or more equations did not get rendered due to their size.
Instances For
The torus form eq:core-torus-form of selected modes F of the role j at the torus height
h' and the point x*, with shifts n and anchor mode a: shifts at most D_* E_{h'} and
error at most D_*^{-150} times the absolute coefficient sum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint lines 2466-2467 and 2569 for the masked selection: the selected modes of a core role
with the final class F_h(m) lie in F_h(m), and they are the core modes of entire minimal
CURRENT components (the masks select whole units, roleMask_iff_of_same_unit).
Blueprint line 2466 for minimal CURRENT components: on the upper heights a minimal CURRENT
component of a core role is bad at a proportion at most 2δ_* (its core components share their
good predicates, compGood_iff_of_same_class_le, coreComp_bad_card).
Blueprint lines 2569-2572 on a leaf cell of the side states: for a final upper height h, the
final class F_h(m) of a good mode m of a core role j, an assignment asg of the n failed
trials and torus forms of the selected modes for all words w ∈ H^n (shifts ns w, anchor a),
the torus sizes a'_j(w) of eq:torus-size satisfy a'_j(w) ≤ 6 σ_F and
E_w a'_j(w)² ≤ 36 (2δ_*)^{n_j} σ_F², with n_j the number of trials assigned to j and
σ_F² = compSizeSq (eq:component-size): each minimal-component summand of eq:torus-size
requires its unit to fail at the n_j heights assigned to j, which has probability at most
(2δ_*)^{n_j} (the other success requirements are dropped).
The principal core contributions (blueprint eq:principal-core, lines 2577-2582) #
The minimal CURRENT components inside a final class F of the role j (the summation units of
eq:component-size).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The component size σ_F of a final class F of the role j (blueprint
eq:component-size).
Equations
- D.clsSize G I j F = √(∑ U ∈ D.clsUnits G I j F, D.unitSizeSq G I j U)
Instances For
The component size of the final class F_h(m) is σ_F = compSizeSq^{1/2}.
A choice of the shifts of the torus form eq:core-torus-form of the selected modes of a core
role (any shifts with the torus form, when they exist).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The torus size a'_j of the selected modes of a core role with the chosen shifts.
Equations
Instances For
Blueprint lines 2467-2471 for the masked selection with a given anchor: when every selected
mode lies in the PRE predecessor E_{h-Δ}(a) of the anchor, the selected modes have the torus
form eq:core-torus-form at h - Δ (cell_torus_form).
The subtotals of pairwise disjoint components add up to the subtotal of their union.
The selected modes are the union of the masked components.
The masked components of a core slot with final class F, as entries of the component
index set: summing any function over them is summing over maskComps.
The masked components of a core slot are pairwise disjoint.
Blueprint lines 2466-2467 (grouping at the final classes): the masked subtotals of a core slot
with final class F add up to the subtotal of the selected modes.
Blueprint lines 2565-2566 for a group of masked tuples: the absolute coefficient sum of the selected modes of a core slot is the sum over the masked components of their coefficient sums.
The final classes at h of the core components of a role good at h.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A final class of a good core component is the final class of a mode good at h.
Anchors of the final classes (blueprint line 2467, "they lie in the unique good predecessor of
each F_j; let a_j be its representative"): at every upper height h and in every role, every
mode of a core component good at h lies in the PRE predecessor E_{h-Δ} of the anchor of its
final class (for instance the hereditary representatives, selected_in_pred_of_rep).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The selected modes of a final class lie in the PRE predecessor of its anchor.
role_size_moments for a final class F = F_h(m), in terms of σ_F = clsSize F.
The principal coefficient of a four-core tuple with representatives a: |WFourier_s(r q', r t')|
when it passes the four-core test, 0 when it is discarded (blueprint lines 2519-2530).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The tuple errors of a group of masked tuples with final classes p: the sum over the group of
Π_l Σ_{m ∈ r_l} |α_m| is the product of the coefficient sums of the selected modes.
Blueprint lines 2463-2582 for the four-core pattern on a leaf cell of the side states
(eq:principal-core before binning, with eq:core-numerical): with anchors of the final classes
(AnchorOK), the form of the four core slots is at most 2⁴ Z / (1 - 4 (2δ_*)^{1/4}) plus the
absolute tuple errors C_J D_*^{-100} Π_l Σ_{m ∈ r_l} |α_m|, where
Z = Σ_{h ∈ H} |H|⁻¹ Σ_p c_p Π_j 6 σ_{p_j} sums over the final heights and the tuples p of final
classes of good core components the principal coefficients c_p = |WFourier_s(r q', r t')| of the
passing tuples (0 for discarded ones) times the class sizes (exact common-height selection
pattern_first_success, first success pattern_leaf_bound, grouping masked_group_sum, tuple
bounds four_core_tuple_bound, moments role_size_moments_cls and principal_word_average).
The value C_J 2μ ν^{-J} Π_j 6 (2 σ_j) of a four-core dyadic bin (μ, ν, σ) (blueprint
eq:principal-core, Λ = 1).
Equations
Instances For
The dyadic bin (μ, ν, (σ_j)_j) of a four-core tuple with representatives a and sizes σ
(the bands of eq:four-tests and the dyadic bands of the sizes).
Equations
- D.fourBin G I xs h' a σv = (D.fourMuBand G I xs h' a, D.fourNuBand G I xs h' a, fun (j : Fin 4) => TrilinearHT.Auto.dyadicBand (σv j))
Instances For
The tested four-core tuples of a family: those passing the four-core test with all sizes positive.
Equations
- D.fourTestedOf G I xs h' T a σv = {p ∈ T | D.fourPasses G I xs h' (a p) ∧ ∀ (j : Fin 4), 0 < σv p j}
Instances For
Blueprint eq:principal-core (lines 2577-2582) for four cores (Λ = 1), at one final height:
the principal quantity Σ_p c_p Π_j 6 σ_{p,j} (c_p = |WFourier_s(r q', r t')| for passing
tuples, 0
for discarded ones) is at most the sum over the occupied dyadic bins (μ, ν, σ) of the bin values
C_J 2μ ν^{-J} Π_j 6 (2σ_j) times the number N of tuples in the bin that pass the four-core
test and have all σ_j > 0 (zero factors contribute nothing; four_core_kernel_sample,
fourBands_spec, sum_by_bins).
The tested four-core tuples at a final height h: tuples of final classes of good core
components passing the four-core test with their anchors and with all class sizes positive.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The dyadic bin of a four-core tuple of final classes at the final height h.
Equations
Instances For
Blueprint eq:principal-core (lines 2577-2582) for the four-core pattern on a leaf cell of
the side states (Λ = 1): the form of the four core slots is at most
2⁴/(1 - 4(2δ_*)^{1/4}) Σ_{h ∈ H} |H|⁻¹ Σ_{bins} C_J 2μ ν^{-J} Π_j 6(2σ_j) N_{h,bin}, plus the
absolute tuple errors of eq:core-numerical. Here N_{h,bin} is the number of tested tuples of
final classes at the final height h in the bin. These tuples pass the four-core test and have
nonzero class sizes, and they are counted once each: distinct classes have distinct anchors,
anchor_injective. The bin consists of the dyadic bands of μ, ν and of the component sizes
σ_j of eq:component-size.
A product with the factor 1 at one index is the product over the other indices.
The principal window coefficient of a three-core tuple with side role l (blueprint
eq:side-windows): 2 Σ_{Λ = 2^i ≤ 2^{I_w}} r⁻¹ C_{J,A} μ ν^{-J} 2^{A+4} Λ^{-(A+1)} b_Λ r with the
offset-averaged window energies of the side X, so that threePrin = threeC Π_{j ≠ l} a'_j.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The principal coefficient of a three-core tuple: threeC if it passes the three-core test,
0 if it is discarded.
Equations
Instances For
In a non-core slot occurring in a group of masked tuples, the group consists of the single dummy entry.
Blueprint lines 2549-2560 for a group of masked tuples of a three-core pattern: the side slot of the grouped form is the side itself.
The tuple errors of a group of masked tuples of a three-core pattern (side slot l): the sum
over the group of Π_k Σ_{m ∈ r_k} |α_m| (the side slot contributing 1) is the product over the
core slots of the coefficient sums of the selected modes.
Anchors of the final classes in one role j (the property AnchorOK for this role): every
mode of a core component good at an upper height h lies in E_{h-Δ} of the anchor of its
class.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The selected modes of a final class lie in the PRE predecessor of its anchor (one role).
The slopes γ_j^* = ω_{a_j}(x_*) of the anchors of a three-core tuple p of final classes at
the height h (side role l, whose entry is 0).