Section 15.5: One distribution calculation and the final sums

This file was automatically generated by Claude.

Formalization of blueprint Section 15, "Common heights and concentration of the core terms" (sec:core), subsection 5, "One distribution calculation and the final sums" (lines 2746-2825) of blueprint/formalization_blueprint.tex.

One distribution calculation (lem:distribution, blueprint lines 2746-2769)

theorem TrilinearHT.Auto.rpow_one_sub_eq_integral {N ε : ℝ} (hN : 0 < N) (hε : 0 < ε) : N ^ (1 - ε) = ε * N * ∫ (t : ℝ) in Set.Ioi N, t ^ (-1 - ε)

N^{1-ε} = ε N ∫_{(N,∞)} t^{-1-ε} dt for N > 0.

theorem TrilinearHT.Auto.distribution_power {ι : Type u_1} (s : Finset ι) (N : ι → ℝ) {M A B c ε : ℝ} (hM : 0 < M) (hN0 : ∀ i ∈ s, 0 ≤ N i) (hNM : ∀ i ∈ s, N i ≤ M ^ 2) (hA : ∑ i ∈ s, N i ≤ A) (hApos : 0 < A) (hBpos : 0 < B) (hsparse : ∀ (δ : ℝ), 0 < δ → δ ≤ 1 → ∑ i ∈ s with N i ≤ δ * M ^ 2, N i ≤ B * δ ^ c * M ^ 2) (hc0 : 0 < c) (hc1 : c < 1) (hε : 0 < ε) (hεc : ε < c) : ∑ i ∈ s, N i ^ (1 - ε) ≤ c / (c - ε) * A ^ (1 - ε / c) * B ^ (ε / c) * M ^ (2 * ε * (1 / c - 1))

Blueprint lem:distribution: if 0 ≤ N_s ≤ M², Σ N_s ≤ A and Σ_{N_s ≤ δM²} N_s ≤ B δ^c M² for 0 < δ ≤ 1, then for 0 < ε < c < 1, Σ N_s^{1-ε} ≤ c/(c-ε) A^{1-ε/c} B^{ε/c} M^{2ε(1/c-1)}.

The final sums (blueprint lines 2771-2822)

theorem TrilinearHT.Auto.powered_count_exponents {c : ℝ} (hc : 0 < c) : c / (c - c / 4) = 4 / 3 ∧ 1 - c / 4 / c = 3 / 4 ∧ c / 4 / c = 1 / 4 ∧ 2 * (c / 4) * (1 / c - 1) = (1 - c) / 2 ∧ 3 / 4 + 3 / 4 + (1 - c) / 2 = 2 * (1 - c / 4)

Blueprint eq:fixed-power and eq:powered-count: with ε = c/4, the distribution constants are c/(c-ε) = 4/3, 1 - ε/c = 3/4, ε/c = 1/4, 2ε(1/c - 1) = (1-c)/2, and the total count exponent 3/4 + 3/4 + (1-c)/2 equals 2p with p = 1 - ε.

theorem TrilinearHT.Auto.amplitude_factor_le_one {σ₁ σ₂ σ₃ σ₄ c : ℝ} (h4 : 0 < σ₄) (h34 : σ₄ ≤ σ₃) (h23 : σ₃ ≤ σ₂) (h12 : σ₂ ≤ σ₁) (hc : 0 < c) : σ₁ ^ (-1 / 2 - c / 4) * σ₂ ^ (-1 / 2 - c / 4) * σ₃ ^ (1 - c / 4) * σ₄ ^ (3 * c / 4) ≤ 1

Blueprint line 2799: for ordered amplitudes σ₁ ≥ σ₂ ≥ σ₃ ≥ σ₄ > 0 and 0 < c, σ₁^{-1/2-c/4} σ₂^{-1/2-c/4} σ₃^{1-c/4} σ₄^{3c/4} ≤ 1.

The powered core estimate (core-estimate, blueprint lines 2771-2822)

theorem TrilinearHT.Auto.powered_count {ι : Type u_1} (s : Finset ι) (N : ι → ℝ) {M A B c : ℝ} (hM : 0 < M) (hN0 : ∀ i ∈ s, 0 ≤ N i) (hNM : ∀ i ∈ s, N i ≤ M ^ 2) (hA : ∑ i ∈ s, N i ≤ A) (hApos : 0 < A) (hBpos : 0 < B) (hsparse : ∀ (δ : ℝ), 0 < δ → δ ≤ 1 → ∑ i ∈ s with N i ≤ δ * M ^ 2, N i ≤ B * δ ^ c * M ^ 2) (hc0 : 0 < c) (hc1 : c < 1) : ∑ i ∈ s, N i ^ (1 - c / 4) ≤ 4 / 3 * A ^ (3 / 4) * B ^ (1 / 4) * M ^ ((1 - c) / 2)

Blueprint eq:powered-count (lines 2779-2782): lem:distribution with c' = c/4, A = L₀ M_i M_j and B = C ℓ L₀¹² gives Σ_s N_s^{1-c/4} ≤ (4/3) A^{3/4} B^{1/4} M^{(1-c)/2}.

theorem TrilinearHT.Auto.sum_prod_rpow_le {κ : Type u_1} {ι : Type u_2} (I : Finset ι) (Gs : Finset κ) (m : ι → κ → ℝ) (β : ι → ℝ) (hm : ∀ i ∈ I, ∀ G ∈ Gs, 0 ≤ m i G) (hβ : ∀ i ∈ I, 0 < β i) (hb : 1 ≤ ∑ i ∈ I, β i) : ∑ G ∈ Gs, ∏ i ∈ I, m i G ^ β i ≤ ∏ i ∈ I, (∑ G ∈ Gs, m i G) ^ β i

Blueprint lines 2785-2789 (Hölder over groups): for nonnegative m_i^G and positive exponents with Σ_i β_i ≥ 1, Σ_G Π_i (m_i^G)^{β_i} ≤ Π_i (Σ_G m_i^G)^{β_i}.

theorem TrilinearHT.Auto.rpow_finset_sum_le {ι : Type u_1} (s : Finset ι) (x : ι → ℝ) (hx : ∀ i ∈ s, 0 ≤ x i) {p : ℝ} (hp0 : 0 < p) (hp1 : p ≤ 1) : (∑ i ∈ s, x i) ^ p ≤ ∑ i ∈ s, x i ^ p

Subadditivity of x ↦ x^p for 0 < p ≤ 1 over finite sums of nonnegative reals.

theorem TrilinearHT.Auto.min_sum_le_rpow {ι : Type u_1} (s : Finset ι) (x : ι → ℝ) (hx : ∀ i ∈ s, 0 ≤ x i) {η p : ℝ} (hη : 0 ≤ η) (hp0 : 0 < p) (hp1 : p ≤ 1) : min η (∑ i ∈ s, x i) ≤ η ^ (1 - p) * ∑ i ∈ s, x i ^ p

Blueprint lines 2812-2816 (eq:core-final, the minimum step): for nonnegative principal quantities x_k, min(η, Σ_k x_k) ≤ η^{1-p} Σ_k x_k^p for 0 < p ≤ 1.

The powered core count over groups (blueprint lines 2783-2797)

theorem TrilinearHT.Auto.rpow_mul_neg_two {K σ a : ℝ} (hK : 0 ≤ K) (hσ : 0 < σ) : (K * σ ^ (-2)) ^ a = K ^ a * σ ^ (-2 * a)

theorem TrilinearHT.Auto.core_count_groups {κ : Type u_1} (Gs : Finset κ) (PG : κ → ℝ) (M : Fin 4 → κ → ℝ) (Mx : κ → ℝ) {σ : Fin 4 → ℝ} {L0 Bc K c : ℝ} (hc0 : 0 < c) (hc1 : c < 1) (hL0 : 0 ≤ L0) (hBc : 0 ≤ Bc) (hK : 0 ≤ K) (hσ3 : 0 < σ 3) (h23 : σ 3 ≤ σ 2) (h12 : σ 2 ≤ σ 1) (h01 : σ 1 ≤ σ 0) (hM0 : ∀ (i : Fin 4), ∀ G ∈ Gs, 0 ≤ M i G) (hMx : ∀ G ∈ Gs, 0 ≤ Mx G ∧ Mx G ≤ ∑ i : Fin 4, M i G) (hP : ∀ G ∈ Gs, PG G ≤ 4 / 3 * (L0 * M 0 G * M 1 G) ^ (3 / 4) * Bc ^ (1 / 4) * Mx G ^ ((1 - c) / 2)) (hsum : ∀ (i : Fin 4), ∑ G ∈ Gs, M i G ≤ K * σ i ^ (-2)) : (∑ G ∈ Gs, PG G) * (∏ i : Fin 4, σ i) ^ (1 - c / 4) ≤ 16 / 3 * L0 ^ (3 / 4) * Bc ^ (1 / 4) * K ^ (2 - c / 2)

Blueprint lines 2783-2797: summing eq:powered-count over groups. If each group's powered count is at most (4/3) (L₀ M₀ M₁)^{3/4} B^{1/4} (M')^{(1-c)/2} for the two largest-amplitude roles 0, 1 (σ₀ ≥ σ₁ ≥ σ₂ ≥ σ₃ > 0), with M' ≤ Σ_k M_k and path bounds Σ_G M_i^G ≤ K σ_i^{-2}, then after multiplication by (Π σ_i)^p, p = 1 - c/4, the group sum is at most (16/3) L₀^{3/4} B^{1/4} K^{2-c/2}: expand the maximizing role, apply Hölder over groups (total exponent 2p > 1) and the amplitude factor bound.

Amplitude bins (blueprint lines 2772-2778)

theorem TrilinearHT.Auto.dyadic_bins_card {lo hi : ℝ} (hlo : 0 < lo) (hlh : lo ≤ hi) (T : Finset ℤ) (hT : ∀ k ∈ T, lo ≤ 2 ^ k ∧ 2 ^ k ≤ hi) : ↑T.card ≤ Real.logb 2 (hi / lo) + 1

Blueprint line 2775 ("the remaining amplitudes lie in [D_*^{-B}, P^{C₀}]; their quadruples number at most C (1 + log D_* + log P)^4"): the dyadic exponents k with lo ≤ 2^k ≤ hi number at most log₂(hi/lo) + 1.

The minimum step and path integration (blueprint lines 2802-2816, eq:core-final)

theorem TrilinearHT.Auto.core_final_pointwise (G : RealDyadicGrid) (root : ℤ × ℤ) (S : Finset (ℤ × ℤ)) (hS : ∀ I ∈ S, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G root.1 root.2) {κ : Type u_1} (Cf : ℤ × ℤ → Finset κ) (q : ℤ × ℤ → κ → ℝ → ℝ) (hq : ∀ (I : ℤ × ℤ) (c : κ) (y : ℝ), 0 ≤ q I c y) (CI err : ℤ × ℤ → ℝ) (herr : ∀ I ∈ S, 0 ≤ err I) (hCI : ∀ I ∈ S, ∀ y ∈ dyadicGridCell G I.1 I.2, CI I ≤ ∑ c ∈ Cf I, q I c y + err I) {η p Mp : ℝ} (hη : 0 ≤ η) (hp0 : 0 < p) (hp1 : p ≤ 1) (hpath : ∀ (y : ℝ), ∑ I ∈ S with y ∈ dyadicGridCell G I.1 I.2, ∑ c ∈ Cf I, q I c y ^ p ≤ Mp) : ∑ I ∈ S, dyadicGridLength G I.1 * min η (CI I) ≤ η ^ (1 - p) * (dyadicGridLength G root.1 * Mp) + ∑ I ∈ S, dyadicGridLength G I.1 * err I

Blueprint eq:core-final (lines 2810-2816) with point-dependent principal bounds ("integrating over x* uses eq:path, including when the point-dependent principal upper bounds vary within a cell"): if for every cell I and every point y ∈ I the cell quantity is at most a sum of nonnegative principal quantities q_{I,c}(y) plus an absolute error, and at every point the powered principal quantities of the cells containing it sum to at most M_p, then Σ_I |I| min(η, C_I) ≤ η^{1-p} M_p |R| + Σ_I |I| err_I.

theorem TrilinearHT.Auto.path_count_four {κ : Type u_1} (Gs : Finset κ) (Sc : κ → Finset ℤ) (N : κ → ℤ → ℝ) (M : Fin 4 → κ → ℝ) (Mx : κ → ℝ) {σ : Fin 4 → ℝ} {L0 Bc K c : ℝ} (hc0 : 0 < c) (hc1 : c < 1) (hL0 : 0 < L0) (hBc : 0 < Bc) (hK : 0 ≤ K) (hσ3 : 0 < σ 3) (h23 : σ 3 ≤ σ 2) (h12 : σ 2 ≤ σ 1) (h01 : σ 1 ≤ σ 0) (hM0 : ∀ (i : Fin 4), ∀ G ∈ Gs, 0 ≤ M i G) (hMx : ∀ G ∈ Gs, 0 < Mx G ∧ Mx G ≤ ∑ i : Fin 4, M i G) (hN0 : ∀ G ∈ Gs, ∀ s ∈ Sc G, 0 ≤ N G s) (hNM : ∀ G ∈ Gs, ∀ s ∈ Sc G, N G s ≤ Mx G ^ 2) (htot : ∀ G ∈ Gs, ∑ s ∈ Sc G, N G s ≤ L0 * M 0 G * M 1 G) (hsparse : ∀ G ∈ Gs, ∀ (δ : ℝ), 0 < δ → δ ≤ 1 → ∑ s ∈ Sc G with N G s ≤ δ * Mx G ^ 2, N G s ≤ Bc * δ ^ c * Mx G ^ 2) (hsum : ∀ (i : Fin 4), ∑ G ∈ Gs, M i G ≤ K * σ i ^ (-2)) : (∑ G ∈ Gs, ∑ s ∈ Sc G, N G s ^ (1 - c / 4)) * (∏ i : Fin 4, σ i) ^ (1 - c / 4) ≤ 16 / 3 * L0 ^ (3 / 4) * Bc ^ (1 / 4) * K ^ (2 - c / 2)

Blueprint lines 2774-2801 (eq:fixed-power, eq:powered-count, Hölder over the groups): for each group G let the tested-tuple counts N_s^G along a path satisfy the conclusions of the tested-counts step (eq:total-count for the pair of the two largest amplitudes, N_s ≤ (M')², eq:applied-sparse with constant B), and let the label counts obey the path caps Σ_G M_i^G ≤ K σ_i^{-2} for ordered amplitudes σ₀ ≥ σ₁ ≥ σ₂ ≥ σ₃ > 0. Then with p = 1 - c/4, (Σ_G Σ_s (N_s^G)^p) (Π_i σ_i)^p ≤ (16/3) L₀^{3/4} B^{1/4} K^{2-c/2} (powered_count, core_count_groups).

noncomputable def TrilinearHT.Auto.descPerm (σ : Fin 4 → ℝ) : Equiv.Perm (Fin 4)

A permutation ordering four amplitudes decreasingly (blueprint line 2783, "temporarily order the roles so σ₁ ≥ σ₂ ≥ σ₃ ≥ σ₄").

Equations

• TrilinearHT.Auto.descPerm σ = Equiv.trans Fin.revPerm (Tuple.sort σ)

theorem TrilinearHT.Auto.descPerm_antitone (σ : Fin 4 → ℝ) {i j : Fin 4} (hij : i ≤ j) : σ ((descPerm σ) j) ≤ σ ((descPerm σ) i)

theorem TrilinearHT.Auto.path_count_four_sorted {κ : Type u_1} (Gs : Finset κ) (Sc : κ → Finset ℤ) (N : κ → ℤ → ℝ) (M : Fin 4 → κ → ℝ) (Mx : κ → ℝ) {σ : Fin 4 → ℝ} {L0 Bc K c : ℝ} (hc0 : 0 < c) (hc1 : c < 1) (hL0 : 0 < L0) (hBc : 0 < Bc) (hK : 0 ≤ K) (hσ : ∀ (i : Fin 4), 0 < σ i) (hM0 : ∀ (i : Fin 4), ∀ G ∈ Gs, 0 ≤ M i G) (hMx : ∀ G ∈ Gs, 0 < Mx G ∧ Mx G ≤ ∑ i : Fin 4, M i G) (hN0 : ∀ G ∈ Gs, ∀ s ∈ Sc G, 0 ≤ N G s) (hNM : ∀ G ∈ Gs, ∀ s ∈ Sc G, N G s ≤ Mx G ^ 2) (htot : ∀ G ∈ Gs, ∀ (i j : Fin 4), i ≠ j → ∑ s ∈ Sc G, N G s ≤ L0 * M i G * M j G) (hsparse : ∀ G ∈ Gs, ∀ (δ : ℝ), 0 < δ → δ ≤ 1 → ∑ s ∈ Sc G with N G s ≤ δ * Mx G ^ 2, N G s ≤ Bc * δ ^ c * Mx G ^ 2) (hsum : ∀ (i : Fin 4), ∑ G ∈ Gs, M i G ≤ K * σ i ^ (-2)) : (∑ G ∈ Gs, ∑ s ∈ Sc G, N G s ^ (1 - c / 4)) * (∏ i : Fin 4, σ i) ^ (1 - c / 4) ≤ 16 / 3 * L0 ^ (3 / 4) * Bc ^ (1 / 4) * K ^ (2 - c / 2)

Blueprint lines 2774-2801 with the roles ordered by amplitude: path_count_four applied after the permutation ordering the amplitudes decreasingly, using the total count of the pair of the two largest amplitudes.

theorem TrilinearHT.Auto.summable_one_add_pow_mul_geometric {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (C : ℕ) : Summable fun (n : ℕ) => r ^ n * (1 + ↑n) ^ C

A geometric series with a polynomial weight (1 + n)^C.

Negligible amplitudes on the side states (blueprint lines 2772-2774)

theorem TrilinearHT.Auto.prod_four_le_small {a : Fin 4 → ℝ} {U ε : ℝ} (h0 : ∀ (j : Fin 4), 0 ≤ a j) (hU : ∀ (j : Fin 4), a j ≤ U) (hε : 0 ≤ ε) {j₀ : Fin 4} (hj₀ : a j₀ < ε) : ∏ j : Fin 4, a j ≤ ε * U ^ 3

A product of four amplitudes in [0, U], one of them below ε, is at most ε U³.

theorem TrilinearHT.Auto.sum_bins_filter_le {ι : Type u_1} {β : Type u_2} [DecidableEq β] (T : Finset ι) (f : ι → β) (P : β → Prop) [DecidablePred P] (v : β → ℝ) {K : ℝ} (hK : 0 ≤ K) (hv : ∀ p ∈ T, P (f p) → v (f p) ≤ K) : ∑ c ∈ Finset.image f T with P c, v c * ↑{p ∈ T | f p = c}.card ≤ K * ↑T.card

A sum over the occupied bins of a predicate, weighted by the fibre counts, is at most K times the number of tuples when every such bin has value at most K.

theorem TrilinearHT.Auto.dyadic_quadruples_card {ε U : ℝ} (hε : 0 < ε) (hεU : ε ≤ U) (T : Finset (Fin 4 → ℝ)) (hT : ∀ a ∈ T, ∀ (j : Fin 4), ε ≤ a j ∧ a j ≤ U ∧ ∃ (k : ℤ), a j = 2 ^ k) : ↑T.card ≤ (Real.logb 2 (U / ε) + 1) ^ 4

Blueprint line 2774 ("the remaining amplitudes lie in [D_*^{-B}, P^{C₀}]; their quadruples number at most C (1 + log D_* + log P)^4"): dyadic amplitude quadruples with entries in [ε, U] number at most (log₂(U/ε) + 1)⁴.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.card_goodCls_le {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (I : ℤ × ℤ) (j : Fin 4) (h : ℕ) : (D.goodCls G I j h).card ≤ ((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))).card

The successful final classes at one height are final classes of alive modes, so there are at most |alive| of them (blueprint line 2772, "at most D_*^4 label tuples").

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.card_fourTested_le {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (I : ℤ × ℤ) (xs : ℝ) (anc : ℕ → (j : Fin 4) → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))) (h : ℕ) (hcard : ∀ (j : Fin 4), ↑((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))).card ≤ D.S.Dstar) : ↑(D.fourTested G I xs anc h).card ≤ D.S.Dstar ^ 4

At most D_*^4 tested four-core tuples at one cell, group and height.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.card_threeTested_le {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (I : ℤ × ℤ) (xs : ℝ) (l : Fin 4) (anc : ℕ → (j : Fin 4) → j ≠ l → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))) (X : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (Iw h : ℕ) (hcard : ∀ (j : Fin 4), ↑((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))).card ≤ D.S.Dstar) : ↑(D.threeTested G I xs l anc X Iw h).card ≤ D.S.Dstar ^ 3 * (↑Iw + 1)

At most D_*^3 (I_w + 1) tested three-core tuples and shells at one cell, group and height.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeAmp (l : Fin 4) (c : ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ)) : Fin 4 → ℝ

The amplitude tuple of a three-core bin (μ, ν, i, b_Λ, σ) with side role l: the window size b_Λ in the side role and the core sizes σ_j in the core roles.

Equations

• TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeAmp l c j = if j = l then c.2.2.2.1 else c.2.2.2.2 j

theorem TrilinearHT.Auto.entryCU_nonneg' (κ : LocalKernelClass) (J A : ℕ) : 0 ≤ entryCU κ J A

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourBinVal_small {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (hD : 2 ≤ D.S.Dstar) (J : ℕ) (G : bf.Grp) (I : ℤ × ℤ) (xs : ℝ) (anc : ℕ → (j : Fin 4) → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))) (h : ℕ) {U ε : ℝ} (hε : 0 ≤ ε) (hU : ∀ (j : Fin 4), ∀ F ∈ D.goodCls G I j h, D.clsSize G I j F ≤ U) {p : (j : Fin 4) → Finset (D.Ms j G).Md} (hp : p ∈ D.fourTested G I xs anc h) (hsmall : ∃ (j : Fin 4), (D.fourBinOf G I xs anc h p).2.2 j < ε) : fourBinVal κ' J (D.fourBinOf G I xs anc h p) ≤ 2 * fourKC κ' J * 12 ^ 4 * ε * U ^ 3

The value of a bin of a tested four-core tuple with some amplitude below ε is at most 2 C_J 12⁴ ε U³ when the class sizes are at most U (μ ≤ 1 ≤ ν, σ_j ≤ U).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeBinVal_small {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (hD : 2 ≤ D.S.Dstar) (J Aw : ℕ) (G : bf.Grp) (I : ℤ × ℤ) (xs : ℝ) (l : Fin 4) (anc : ℕ → (j : Fin 4) → j ≠ l → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))) (Iw h : ℕ) {U ε : ℝ} (hε : 0 ≤ ε) (hU : ∀ (j : Fin 4), j ≠ l → ∀ F ∈ D.goodCls G I j h, D.clsSize G I j F ≤ U) (hUs : √((dyadicGridLength A.G I.1)⁻¹ * ∫ (y : ℝ) in dyadicGridLeft A.G I.1 I.2..dyadicGridLeft A.G I.1 I.2 + dyadicGridLength A.G I.1, ‖augPhys (D.toLeaf.sv l G I) y‖ ^ 2) ≤ U) {q : ((j : Fin 4) → Finset (D.Ms j G).Md) × ℕ} (hq : q ∈ D.threeTested G I xs l anc (D.toLeaf.sv l G I) Iw h) (hsmall : ∃ (j : Fin 4), threeAmp l (D.threeBinOf G I xs l anc (D.toLeaf.sv l G I) h q) j < ε) : threeBinVal κ' J Aw l (D.threeBinOf G I xs l anc (D.toLeaf.sv l G I) h q) ≤ 8 * entryCU κ' J Aw * 2 ^ (Aw + 4) * 12 ^ 3 * ε * U ^ 3

The value of a bin of a tested three-core tuple and shell (side role l) with some amplitude of threeAmp below ε is at most 8 C_{J,A} 2^{A+4} 12³ ε U³ when the class sizes and the side size (r⁻¹ ∫_I |S|²)^{1/2} are at most U.

The powered counts on the side states (eq:powered-count)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.rpow_sum_zero_of_empty {S : Finset ℤ} {N : ℤ → ℝ} (hN : ∀ s ∈ S, N s = 0) {p : ℝ} (hp : 0 < p) : ∑ s ∈ S, N s ^ p = 0

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeRoleCount {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (h : ℕ) (xs : ℝ) (l : Fin 4) (cellOf : ℤ → ℤ × ℤ) (ancOf : (s : ℤ) → D.AncNe3 G (cellOf s) l → ℕ → (j : Fin 4) → j ≠ l → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))) (Iw : ℕ) (c : ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ)) (κ : Fin 4 → ℕ × ℕ) (S : Finset ℤ) (k : Fin 4) : ℝ

The role counts M_k^G along a three-core path in the bin c (side role l, blueprint line 2711): the number |A_k| of labels for a core role and M_l^G = Σ_s w_s for the side.

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.exists_two_core (l : Fin 4) : ∃ (a : Fin 4) (b : Fin 4), a ≠ b ∧ a ≠ l ∧ b ≠ l

The powered group sums on the side states (blueprint lines 2783-2800)

theorem TrilinearHT.Auto.fourMult_mono_dim {d d' : ℕ} (hdd : d ≤ d') {B μ ν : ℝ} (hB : 1 ≤ B) (hμ : 0 < μ) (hμν : μ ≤ ν) : fourMult d B μ ν ≤ fourMult d' B μ ν

L₀ = fourMult is monotone in the dimension.

theorem TrilinearHT.Auto.threeMult_mono_dim {d d' : ℕ} (hdd : d ≤ d') {B μ ν : ℝ} (hB : 1 ≤ B) (hμ : 0 < μ) (hμν : μ ≤ ν) : threeMult d B μ ν ≤ threeMult d' B μ ν

L₀ = threeMult is monotone in the dimension.

theorem TrilinearHT.Auto.ell_mono_dim {d d' : ℕ} (hdd : d ≤ d') {x : ℝ} (hx : 0 ≤ x) : 1 + Real.logb 2 (2 + (↑d + 1) ^ 2 * x) ≤ 1 + Real.logb 2 (2 + (↑d' + 1) ^ 2 * x)

The coefficient ℓ = 1 + log₂(2 + (d+1)² x) is monotone in the dimension (x ≥ 0).

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourUsedReps {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (h : ℕ) (xs : ℝ) (cellOf : ℤ → ℤ × ℤ) (ancOf : (s : ℤ) → D.AncNe G (cellOf s) → ℕ → (j : Fin 4) → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))) (c : ℝ × ℝ × (Fin 4 → ℝ)) (κ : Fin 4 → ℕ × ℕ) (S : Finset ℤ) (j : Fin 4) : Finset (D.Ms j G).Md

The distinct used representatives A_j^G of the role j along a four-core path (blueprint eq:top-count): the anchor modes of the role j of the tested tuples in the bin c with the types κ at the scales of the path.

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.four_labels_card_le {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (h : ℕ) (xs : ℝ) (cellOf : ℤ → ℤ × ℤ) (ancOf : (s : ℤ) → D.AncNe G (cellOf s) → ℕ → (j : Fin 4) → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))) (c : ℝ × ℝ × (Fin 4 → ℝ)) (κ : Fin 4 → ℕ × ℕ) (S : Finset ℤ) (j : Fin 4) : (S.biUnion fun (s : ℤ) => Finset.image (fun (x : Fin 4 → ℝ) => x j) (D.fourPathE G h xs cellOf ancOf c κ s)).card ≤ (D.fourUsedReps G h xs cellOf ancOf c κ S j).card

The labels of a role along a four-core path are the slopes at x* of its distinct used representatives, so M_j^G ≤ |A_j^G|.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeUsedReps {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (h : ℕ) (xs : ℝ) (l : Fin 4) (cellOf : ℤ → ℤ × ℤ) (ancOf : (s : ℤ) → D.AncNe3 G (cellOf s) l → ℕ → (j : Fin 4) → j ≠ l → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))) (Iw : ℕ) (c : ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ)) (κ : Fin 4 → ℕ × ℕ) (S : Finset ℤ) (j : Fin 4) (hj : j ≠ l) : Finset (D.Ms j G).Md

The distinct used representatives A_j^G of a core role j ≠ l along a three-core path.

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.three_labels_card_le {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (h : ℕ) (xs : ℝ) (l : Fin 4) (cellOf : ℤ → ℤ × ℤ) (ancOf : (s : ℤ) → D.AncNe3 G (cellOf s) l → ℕ → (j : Fin 4) → j ≠ l → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))) (Iw : ℕ) (c : ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ)) (κ : Fin 4 → ℕ × ℕ) (S : Finset ℤ) (j : Fin 4) (hj : j ≠ l) : (S.biUnion fun (s : ℤ) => Finset.image (fun (x : Fin 4 → ℝ) => x j) (D.threePathE G h xs l cellOf ancOf Iw c κ s)).card ≤ (D.threeUsedReps G h xs l cellOf ancOf Iw c κ S j hj).card

The labels of a core role along a three-core path are the slopes at x* of its distinct used representatives, so M_j^G ≤ |A_j^G|.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.four_group_sum_side {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) {Cj CA CT CK : ℕ} {δs W : ℝ} (hV : D.S.Valid Cj CA CT CK δs W) (hCA : 1 ≤ CA) (hCT : 4 ≤ CT) (hd2 : 2 ≤ D.S.dmax) (hD : 2 ≤ D.S.Dstar) (hB : 2 ≤ D.S.Bstar) (_hQ0 : 1 ≤ D.S.Q0) (hSP : D.SP = D.S.sideParams δs) (hdD : ↑D.S.dmax ≤ D.S.Dstar) (qG : bf.Grp → ℕ) (hqG : ∀ (G : bf.Grp), 1 ≤ qG G ∧ qG G ≤ D.S.Q0) (Gs : Finset bf.Grp) (h : ℕ) (hh : 10 ≤ h) (hhJ : h ≤ D.SP.Jst) (Cs : Finset (ℤ × ℤ)) (rep : (G : bf.Grp) → (j : Fin 4) → ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (z : bf.Grp → ChartTag) (S : bf.Grp → Finset ℤ) {cellOf : ℤ → ℤ × ℤ} {xs : ℝ} (hpath : ∀ G ∈ Gs, ∀ s ∈ S G, cellOf s ∈ Cs ∧ xs ∈ dyadicGridCell A.G (cellOf s).1 (cellOf s).2) (hcell : ∀ (s : ℤ), (cellOf s).1 = s) (ancOf : (G : bf.Grp) → (s : ℤ) → D.AncNe G (cellOf s) → ℕ → (j : Fin 4) → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))) (hG : ∀ G ∈ Gs, (∀ (j : Fin 4), 8 * (D.Ms j G).Λ ≤ D.S.Ξ) ∧ (∀ (j : Fin 4), (D.Ms j G).zc = z G) ∧ (z G).dim ≤ D.S.dmax ∧ ∃ (hrep : ∀ (j : Fin 4), (D.withQ0 (qG G)).RepOK G j h Cs (rep G j)), (D.withQ0 (qG G)).FourPathAnc G h Cs (rep G) hrep cellOf (ancOf G) (S G)) (c : ℝ × ℝ × (Fin 4 → ℝ)) (hc : 0 < c.1 ∧ c.1 ≤ 1 ∧ 1 ≤ c.2.1) (hσ : ∀ (i : Fin 4), 0 < c.2.2 i) (κ : Fin 4 → ℕ × ℕ) {K : ℝ} (hK : 0 ≤ K) (hcap : ∀ (i : Fin 4), ∑ G ∈ Gs, ↑((D.withQ0 (qG G)).fourUsedReps G h xs cellOf (ancOf G) c κ (S G) i).card ≤ K * c.2.2 i ^ (-2)) : (∑ G ∈ Gs, ∑ s ∈ S G, ↑((D.withQ0 (qG G)).fourPathE G h xs cellOf (ancOf G) c κ s).card ^ (1 - 1 / 300 / 4)) * (∏ i : Fin 4, c.2.2 i) ^ (1 - 1 / 300 / 4) ≤ 16 / 3 * fourMult D.S.dmax (D.S.Dstar ^ 5 * D.S.Eh (h - D.SP.Δ)) c.1 (2 * c.2.1) ^ (3 / 4) * (3 * 10 ^ 11 * (1 + Real.logb 2 (2 + (↑D.S.dmax + 1) ^ 2 * (4 * (2 * c.2.1) / c.1))) * fourMult D.S.dmax (D.S.Dstar ^ 5 * D.S.Eh (h - D.SP.Δ)) c.1 (2 * c.2.1) ^ 12) ^ (1 / 4) * K ^ (2 - 1 / 300 / 2)

Blueprint lines 2783-2800 for four cores on the side states: fix the path point x* (a path S, cellOf), the height h, the types κ and the bin c = (μ, ν, σ). For the groups G (each with its representatives as anchors), eq:powered-count for the pair of the two largest amplitudes, M' ≤ Σ_i M_i^G, the path caps Σ_G |A_i^G| ≤ K σ_i^{-2} of eq:top-count for the distinct used representatives, and Hölder over the groups (path_count_four_sorted) give, with p = 1 - c/4, c = 1/300, (Σ_G Σ_s (N_s^G)^p) (Π_i σ_i)^p ≤ (16/3) L₀^{3/4} (C ℓ L₀^{12})^{1/4} K^{2-c/2}, where L₀, ℓ are taken at the dimension bound d_max.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.three_total_pair {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) {Cj CA CT CK : ℕ} {δs W : ℝ} (hV : D.S.Valid Cj CA CT CK δs W) (hCA : 1 ≤ CA) (hd2 : 2 ≤ D.S.dmax) (hD : 2 ≤ D.S.Dstar) (hB : 2 ≤ D.S.Bstar) (hΔ : D.SP.Δ = 10) (G : bf.Grp) (h : ℕ) (hh : 10 ≤ h) (l : Fin 4) (Cs : Finset (ℤ × ℤ)) (rep : (j : Fin 4) → ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (hrep : ∀ (j : Fin 4), D.RepOK G j h Cs (rep j)) (hΛ : ∀ (j : Fin 4), 8 * (D.Ms j G).Λ ≤ D.S.Ξ) (z : ChartTag) (hz : ∀ (j : Fin 4), (D.Ms j G).zc = z) {S : Finset ℤ} {cellOf : ℤ → ℤ × ℤ} {xs : ℝ} (hpath : ∀ s ∈ S, cellOf s ∈ Cs ∧ xs ∈ dyadicGridCell A.G (cellOf s).1 (cellOf s).2) (hcell : ∀ (s : ℤ), (cellOf s).1 = s) {ancOf : (s : ℤ) → D.AncNe3 G (cellOf s) l → ℕ → (j : Fin 4) → j ≠ l → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))} (hanc : D.ThreePathAnc G h l Cs rep hrep cellOf ancOf S) {Iw : ℕ} (hIw : 2 ^ Iw ≤ 2 * D.U0) (c : ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ)) (hc : 0 < c.1 ∧ c.1 ≤ 1 ∧ 1 ≤ c.2.1) (κ : Fin 4 → ℕ × ℕ) : (∀ (i j : Fin 4), i ≠ j → ∑ s ∈ S, ↑(D.threePathE G h xs l cellOf ancOf Iw c κ s).card ≤ threeMult z.dim (D.S.Dstar ^ 5 * D.S.Eh (h - D.SP.Δ)) c.1 (2 * c.2.1) * D.threeRoleCount G h xs l cellOf ancOf Iw c κ S i * D.threeRoleCount G h xs l cellOf ancOf Iw c κ S j) ∧ ∀ (a b : Fin 4), a ≠ b → a ≠ l → b ≠ l → ∀ s ∈ S, ↑(D.threePathE G h xs l cellOf ancOf Iw c κ s).card ≤ D.threeRoleCount G h xs l cellOf ancOf Iw c κ S a * D.threeRoleCount G h xs l cellOf ancOf Iw c κ S b

Blueprint eq:total-count for three cores in terms of the role counts: for any two distinct roles (core or side), Σ_s N_s ≤ L₀ M_i M_j, and N_s ≤ M_a M_b for two distinct core roles.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.three_group_sum_side {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) {Cj CA CT CK : ℕ} {δs W : ℝ} (hV : D.S.Valid Cj CA CT CK δs W) (hCA : 1 ≤ CA) (hCT : 4 ≤ CT) (hd2 : 2 ≤ D.S.dmax) (hD : 2 ≤ D.S.Dstar) (hB : 2 ≤ D.S.Bstar) (_hQ0 : 1 ≤ D.S.Q0) (hSP : D.SP = D.S.sideParams δs) (hdD : ↑D.S.dmax ≤ D.S.Dstar) (qG : bf.Grp → ℕ) (hqG : ∀ (G : bf.Grp), 1 ≤ qG G ∧ qG G ≤ D.S.Q0) (Gs : Finset bf.Grp) (h : ℕ) (hh : 10 ≤ h) (hhJ : h ≤ D.SP.Jst) (l : Fin 4) (Cs : Finset (ℤ × ℤ)) (rep : (G : bf.Grp) → (j : Fin 4) → ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (z : bf.Grp → ChartTag) (S : bf.Grp → Finset ℤ) {cellOf : ℤ → ℤ × ℤ} {xs : ℝ} (hpath : ∀ G ∈ Gs, ∀ s ∈ S G, cellOf s ∈ Cs ∧ xs ∈ dyadicGridCell A.G (cellOf s).1 (cellOf s).2) (hcell : ∀ (s : ℤ), (cellOf s).1 = s) (ancOf : (G : bf.Grp) → (s : ℤ) → D.AncNe3 G (cellOf s) l → ℕ → (j : Fin 4) → j ≠ l → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))) (hG : ∀ G ∈ Gs, (∀ (j : Fin 4), 8 * (D.Ms j G).Λ ≤ D.S.Ξ) ∧ (∀ (j : Fin 4), (D.Ms j G).zc = z G) ∧ (z G).dim ≤ D.S.dmax ∧ ∃ (hrep : ∀ (j : Fin 4), (D.withQ0 (qG G)).RepOK G j h Cs (rep G j)), (D.withQ0 (qG G)).ThreePathAnc G h l Cs (rep G) hrep cellOf (ancOf G) (S G)) {Iw : ℕ} (hIw : 2 ^ Iw ≤ 2 * D.U0) (c : ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ)) (hc : 0 < c.1 ∧ c.1 ≤ 1 ∧ 1 ≤ c.2.1) (hσ : ∀ (i : Fin 4), 0 < threeAmp l c i) (κ : Fin 4 → ℕ × ℕ) {K : ℝ} (hK : 0 ≤ K) (hcap : ∀ (i : Fin 4) (hi : i ≠ l), ∑ G ∈ Gs, ↑((D.withQ0 (qG G)).threeUsedReps G h xs l cellOf (ancOf G) Iw c κ (S G) i hi).card ≤ K * threeAmp l c i ^ (-2)) (hcapl : ∑ G ∈ Gs, ∑ s ∈ S G, (D.withQ0 (qG G)).sideWeight G l cellOf c.2.2.2.1 s ≤ K * threeAmp l c l ^ (-2)) : (∑ G ∈ Gs, ∑ s ∈ S G, ↑((D.withQ0 (qG G)).threePathE G h xs l cellOf (ancOf G) Iw c κ s).card ^ (1 - 1 / 300 / 4)) * (∏ i : Fin 4, threeAmp l c i) ^ (1 - 1 / 300 / 4) ≤ 16 / 3 * threeMult D.S.dmax (D.S.Dstar ^ 5 * D.S.Eh (h - D.SP.Δ)) c.1 (2 * c.2.1) ^ (3 / 4) * (3 * 10 ^ 11 * (1 + Real.logb 2 (2 + (↑D.S.dmax + 1) ^ 2 * (2 * c.2.1 / c.1))) * threeMult D.S.dmax (D.S.Dstar ^ 5 * D.S.Eh (h - D.SP.Δ)) c.1 (2 * c.2.1) ^ 12) ^ (1 / 4) * K ^ (2 - 1 / 300 / 2)

Blueprint lines 2783-2800 for three cores with side role l on the side states: at a fixed path, height, core types and bin c = (μ, ν, i, σ_l, σ), the groups' powered counts (eq:total-count for every pair, M' ≤ Σ_k M_k^G), the path caps of eq:top-count for the core roles (Σ_G |A_j^G| ≤ K σ_j^{-2}) and the side cap Σ_G M_l^G ≤ K σ_l^{-2} (eq:side-cap, M_l^G = σ_l^{-2} Σ_s ‖S_{l,G,s}‖²_{2,I_s}), and Hölder over the groups give, with p = 1 - c/4, c = 1/300 and the amplitude tuple threeAmp = (σ_l, σ_j), (Σ_G Σ_s (N_s^G)^p) (Π σ)^p ≤ (16/3) L₀^{3/4} (C ℓ L₀^{12})^{1/4} K^{2-c/2}, with L₀, ℓ taken at the dimension bound d_max.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.band_sq_le_nodeSize {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (I : ℤ × ℤ) (j : Fin 4) (h : ℕ) {F : Finset (D.Ms j G).Md} (hF : F ∈ D.goodCls G I j h) (hpos : 0 < D.clsSize G I j F) : dyadicBand (D.clsSize G I j F) ^ 2 ≤ (D.Ms j G).nodeSize D.S ⋯ D.SP (D.c j G) h (I, D.classNode G I j h hF)

The square of the dyadic band of the component size of a successful class at an actual cell is at most the node size σ_F² of its mode node (compSizeSq, the quantity of prop:tops).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.four_usedReps_subset_tops {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (h : ℕ) (xs : ℝ) (cellOf : ℤ → ℤ × ℤ) (Cs : Finset (ℤ × ℤ)) (rep : (j : Fin 4) → ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (hrep : ∀ (j : Fin 4), D.RepOK G j h Cs (rep j)) {S : Finset ℤ} (hpath : ∀ s ∈ S, cellOf s ∈ Cs ∧ xs ∈ dyadicGridCell A.G (cellOf s).1 (cellOf s).2) {ancOf : (s : ℤ) → D.AncNe G (cellOf s) → ℕ → (j : Fin 4) → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))} (hanc : D.FourPathAnc G h Cs rep hrep cellOf ancOf S) (c : ℝ × ℝ × (Fin 4 → ℝ)) (κ : Fin 4 → ℕ × ℕ) (j : Fin 4) (Nd : Finset (ℤ × (ℤ × ℤ) × (D.Ms j G).Md)) (Rrep : ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (hR : ∀ nd ∈ Nd, Rrep nd = rep j (κ j).1 (κ j).2 nd) (hNd : ∀ s ∈ S, ∀ (F : Finset (D.Ms j G).Md) (hF : F ∈ D.goodCls G (cellOf s) j h), D.classTypeOf G (cellOf s) j h F = κ j → D.classNode G (cellOf s) j h hF ∈ Nd) (huse : ∀ s ∈ S, cellOf s ∈ A.cells ∧ fp.ActualUse G (cellOf s)) : D.fourUsedReps G h xs cellOf ancOf c κ S j ⊆ Finset.image (fun (p : (ℤ × ℤ) × ℤ × (ℤ × ℤ) × (D.Ms j G).Md) => Rrep p.2) ({p ∈ fp.useInst G D.S.K Nd | p.1 ∈ Cs ∧ xs ∈ dyadicGridCell A.G p.1.1 p.1.2 ∧ c.2.2 j ^ 2 ≤ (D.Ms j G).nodeSize D.S ⋯ D.SP (D.c j G) h p})

Blueprint eq:top-count on a four-core path (bridge to prop:tops, first_top_count_main): the distinct used representatives A_j^G of the role j along the path in the bin c are values of the representatives R.rep of first_top_count_main on use instances (I, node) with x* ∈ I and σ_j² ≤ σ_F², provided the representatives of type κ j are those of R on its nodes Nd, the class nodes of type κ j lie in Nd, and the path cells are actual-use cells.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.three_usedReps_subset_tops {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (h : ℕ) (xs : ℝ) (l : Fin 4) (cellOf : ℤ → ℤ × ℤ) (Cs : Finset (ℤ × ℤ)) (rep : (j : Fin 4) → ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (hrep : ∀ (j : Fin 4), D.RepOK G j h Cs (rep j)) {S : Finset ℤ} (hpath : ∀ s ∈ S, cellOf s ∈ Cs ∧ xs ∈ dyadicGridCell A.G (cellOf s).1 (cellOf s).2) {ancOf : (s : ℤ) → D.AncNe3 G (cellOf s) l → ℕ → (j : Fin 4) → j ≠ l → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))} (hanc : D.ThreePathAnc G h l Cs rep hrep cellOf ancOf S) (Iw : ℕ) (c : ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ)) (κ : Fin 4 → ℕ × ℕ) (j : Fin 4) (hj : j ≠ l) (Nd : Finset (ℤ × (ℤ × ℤ) × (D.Ms j G).Md)) (Rrep : ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (hR : ∀ nd ∈ Nd, Rrep nd = rep j (κ j).1 (κ j).2 nd) (hNd : ∀ s ∈ S, ∀ (F : Finset (D.Ms j G).Md) (hF : F ∈ D.goodCls G (cellOf s) j h), D.classTypeOf G (cellOf s) j h F = κ j → D.classNode G (cellOf s) j h hF ∈ Nd) (huse : ∀ s ∈ S, cellOf s ∈ A.cells ∧ fp.ActualUse G (cellOf s)) : D.threeUsedReps G h xs l cellOf ancOf Iw c κ S j hj ⊆ Finset.image (fun (p : (ℤ × ℤ) × ℤ × (ℤ × ℤ) × (D.Ms j G).Md) => Rrep p.2) ({p ∈ fp.useInst G D.S.K Nd | p.1 ∈ Cs ∧ xs ∈ dyadicGridCell A.G p.1.1 p.1.2 ∧ c.2.2.2.2 j ^ 2 ≤ (D.Ms j G).nodeSize D.S ⋯ D.SP (D.c j G) h p})

Blueprint eq:top-count on a three-core path with side role l (bridge to prop:tops): the distinct used representatives of a core role j ≠ l are values of the representatives R.rep on use instances (I, node) with x* ∈ I and σ_j² ≤ σ_F².

Band coefficients (blueprint lines 2802-2806)

theorem TrilinearHT.Auto.freq_coef_le {L ℓ Pw Pℓ Y Cc : ℝ} (hL1 : 1 ≤ L) (hL : L ≤ Pw * Y) (hℓ0 : 0 ≤ ℓ) (hℓ : ℓ ≤ Pℓ * Y) (hY : 1 ≤ Y) (hC : 0 ≤ Cc) : 16 / 3 * L ^ (3 / 4) * (Cc * ℓ * L ^ 12) ^ (1 / 4) ≤ 16 / 3 * Cc ^ (1 / 4) * Pw ^ (15 / 4) * Pℓ ^ (1 / 4) * Y ^ 4

Blueprint line 2802 ("the remaining frequency coefficient from eq:powered-count is at most P^C (1 + log(ν/μ))^C"), abstract form: if 1 ≤ L ≤ P_w Y and ℓ ≤ P_ℓ Y with Y ≥ 1, then (16/3) L^{3/4} (C ℓ L^{12})^{1/4} ≤ (16/3) C^{1/4} P_w^{15/4} P_ℓ^{1/4} Y^4.

theorem TrilinearHT.Auto.ell_le_log (d : ℕ) {y : ℝ} (hy : 2 ≤ y) : 1 + Real.logb 2 (2 + (↑d + 1) ^ 2 * y) ≤ (1 + (Real.log 2 + 2 * Real.log (↑d + 1) + 1) / Real.log 2) * (1 + Real.log y)

Blueprint lines 2802-2803: the coefficient ℓ = 1 + log₂(2 + (d+1)² y) of eq:applied-sparse is at most P_ℓ (1 + log y) for y ≥ 2, with P_ℓ = 1 + (log 2 + 2 log(d+1) + 1)/log 2.

theorem TrilinearHT.Auto.band_series2_summable {p J : ℝ} (hp : 0 < p) (hJ : 0 < J) (C : ℕ) : Summable fun (t : ℕ × ℕ) => (2 ^ (-p)) ^ t.1 * (2 ^ (-(J * p))) ^ t.2 * (1 + ↑t.1 + ↑t.2) ^ C

The two-band series Σ_{u,v ≥ 0} 2^{-pu} 2^{-Jpv} (1 + u + v)^C converges for p, Jp > 0.

theorem TrilinearHT.Auto.dyadic_band_sum_le {p J : ℝ} (hp : 0 < p) (hJ : 0 < J) (T : Finset (ℝ × ℝ)) (hT : ∀ x ∈ T, ∃ (u : ℕ) (v : ℕ), x.1 = 2 ^ (-↑u) ∧ x.2 = 2 ^ ↑v) : ∑ x ∈ T, x.1 ^ p * (x.2 ^ J)⁻¹ ^ p * (1 + Real.log (8 * x.2 / x.1)) ^ 4 ≤ ∑' (t : ℕ × ℕ), (2 ^ (-p)) ^ t.1 * (2 ^ (-(J * p))) ^ t.2 * (4 ^ 4 * (1 + ↑t.1 + ↑t.2) ^ 4)

Blueprint lines 2803-2806 ("extend the actual truncated bands to all μ = 2^{-u}, ν = 2^v; their sum is bounded by C P^C Σ 2^{-pu} 2^{-Jpv} (1+u+v)^C < ∞"): over any finite set of dyadic band pairs μ = 2^{-u} ≤ 1 ≤ ν = 2^v, the powered kernel factors μ^p ν^{-Jp} times (1 + log(8ν/μ))^4 sum to at most the convergent series Σ_{u,v} 2^{-pu} 2^{-Jpv} (4(1 + u + v))^4.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.multPoly {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) : ℝ

The polynomial factor P_w = 32 (d_max + 5)⁴ (log(288 D_*^5 H) + log 2 + 1) of the scale multiplicity at the schedule (eq:triple-test).

Equations

• D.multPoly = 32 * (↑D.S.dmax + 5) ^ 4 * (Real.log (288 * (D.S.Dstar ^ 5 * D.S.H)) + Real.log 2 + 1)

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.ellPoly {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) : ℝ

The polynomial factor P_ℓ = 1 + (log 2 + 2 log(d_max + 1) + 1)/log 2 of ℓ.

Equations

• D.ellPoly = 1 + (Real.log 2 + 2 * Real.log (↑D.S.dmax + 1) + 1) / Real.log 2

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.four_coef_sched {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) {Cj CA CT CK : ℕ} {δs W : ℝ} (hV : D.S.Valid Cj CA CT CK δs W) (hd2 : 2 ≤ D.S.dmax) (hD : 2 ≤ D.S.Dstar) (hB : 2 ≤ D.S.Bstar) (hQ : 1 ≤ D.S.Q0) (hSP : D.SP = D.S.sideParams δs) {h : ℕ} (hhJ : h ≤ D.SP.Jst) {μ ν : ℝ} (hμ : 0 < μ) (hμ1 : μ ≤ 1) (hν : 1 ≤ ν) : 16 / 3 * fourMult D.S.dmax (D.S.Dstar ^ 5 * D.S.Eh (h - D.SP.Δ)) μ (2 * ν) ^ (3 / 4) * (3 * 10 ^ 11 * (1 + Real.logb 2 (2 + (↑D.S.dmax + 1) ^ 2 * (4 * (2 * ν) / μ))) * fourMult D.S.dmax (D.S.Dstar ^ 5 * D.S.Eh (h - D.SP.Δ)) μ (2 * ν) ^ 12) ^ (1 / 4) ≤ 16 / 3 * (3 * 10 ^ 11) ^ (1 / 4) * D.multPoly ^ (15 / 4) * D.ellPoly ^ (1 / 4) * (1 + Real.log (8 * ν / μ)) ^ 4

Blueprint line 2802 for four cores on the side states: the frequency coefficient of the group sum is at most (16/3) C^{1/4} P_w^{15/4} P_ℓ^{1/4} (1 + log(8ν/μ))^4 for a genuine bin 0 < μ ≤ 1 ≤ ν (P_w, P_ℓ polynomial in d_max, log D_*, log H, i.e. ≤ P^C).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.three_coef_sched {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) {Cj CA CT CK : ℕ} {δs W : ℝ} (hV : D.S.Valid Cj CA CT CK δs W) (hd2 : 2 ≤ D.S.dmax) (hD : 2 ≤ D.S.Dstar) (hB : 2 ≤ D.S.Bstar) (hQ : 1 ≤ D.S.Q0) (hSP : D.SP = D.S.sideParams δs) {h : ℕ} (hhJ : h ≤ D.SP.Jst) {μ ν : ℝ} (hμ : 0 < μ) (hμ1 : μ ≤ 1) (hν : 1 ≤ ν) : 16 / 3 * threeMult D.S.dmax (D.S.Dstar ^ 5 * D.S.Eh (h - D.SP.Δ)) μ (2 * ν) ^ (3 / 4) * (3 * 10 ^ 11 * (1 + Real.logb 2 (2 + (↑D.S.dmax + 1) ^ 2 * (2 * ν / μ))) * threeMult D.S.dmax (D.S.Dstar ^ 5 * D.S.Eh (h - D.SP.Δ)) μ (2 * ν) ^ 12) ^ (1 / 4) ≤ 16 / 3 * (3 * 10 ^ 11) ^ (1 / 4) * D.multPoly ^ (15 / 4) * D.ellPoly ^ (1 / 4) * (1 + Real.log (2 * ν / μ)) ^ 4

Blueprint line 2802 for three cores on the side states: the frequency coefficient of the group sum is at most (16/3) C^{1/4} P_w^{15/4} P_ℓ^{1/4} (1 + log(2ν/μ))^4.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.classTypeOf_mem {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (I : ℤ × ℤ) (j : Fin 4) (h : ℕ) (F : Finset (D.Ms j G).Md) (hcard : ↑((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))).card ≤ D.S.Dstar) : D.classTypeOf G I j h F ∈ Finset.range (Nat.log 2 ⌊D.S.Dstar⌋₊ + 1) ×ˢ Finset.range (Nat.log 2 ⌊D.S.Dstar⌋₊ + 1)

Blueprint line 2806 ("types have an allowed polynomial cost"): the role type of a successful final class lies in [0, log₂ D_*]² when the role has at most D_* alive modes.

The core contribution on the side states (eq:core-final)

noncomputable def TrilinearHT.Auto.pathCell (G : RealDyadicGrid) (T : Finset (ℤ × ℤ)) (y : ℝ) (s : ℤ) : ℤ × ℤ

The path of a point y through a finite family T of dyadic cells: the cell of T at the depth s containing y (unique when it exists), and (s, 0) otherwise.

Equations

• TrilinearHT.Auto.pathCell G T y s = if h : ∃ I ∈ T, I.1 = s ∧ y ∈ TrilinearHT.Auto.dyadicGridCell G I.1 I.2 then h.choose else (s, 0)

theorem TrilinearHT.Auto.pathCell_fst (G : RealDyadicGrid) (T : Finset (ℤ × ℤ)) (y : ℝ) (s : ℤ) : (pathCell G T y s).1 = s

theorem TrilinearHT.Auto.pathCell_eq (G : RealDyadicGrid) {T : Finset (ℤ × ℤ)} {y : ℝ} {I : ℤ × ℤ} (hI : I ∈ T) (hy : y ∈ dyadicGridCell G I.1 I.2) : pathCell G T y I.1 = I

theorem TrilinearHT.Auto.path_sum_reindex {ι : Type u_1} [DecidableEq ι] (G : RealDyadicGrid) (T : Finset (ℤ × ℤ)) (gs : ℤ × ℤ → Finset ι) (y : ℝ) (f : ℤ × ℤ → ι → ℝ) : ∑ I ∈ T with y ∈ dyadicGridCell G I.1 I.2, ∑ g ∈ gs I, f I g = ∑ g ∈ {I ∈ T | y ∈ dyadicGridCell G I.1 I.2}.biUnion gs, ∑ s ∈ Finset.image Prod.fst ({I ∈ {I ∈ T | y ∈ dyadicGridCell G I.1 I.2} | g ∈ gs I}), f (pathCell G T y s) g

Reindexing the cells of a path by their depths (blueprint eq:path): for the cells of T containing y and their groups, Σ_{I ∋ y} Σ_{G ∈ g(I)} f(I, G) = Σ_G Σ_{s ∈ S_G} f(I_s, G), with S_G the depths of the cells containing y at which G is used and I_s = pathCell.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourBinVal_eq {κ' : LocalKernelClass} (J : ℕ) (c : ℝ × ℝ × (Fin 4 → ℝ)) : fourBinVal κ' J c = fourKC κ' J * 2 * 12 ^ 4 * (c.1 * (c.2.1 ^ J)⁻¹) * ∏ j : Fin 4, c.2.2 j

The four-core bin value factors as fourKC · 2 · 12⁴ · μ ν^{-J} Π_j σ_j.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.pathGroups {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (T : Finset (ℤ × ℤ)) (gs : ℤ × ℤ → Finset bf.Grp) (y : ℝ) : Finset bf.Grp

The groups used at the cells of T containing y.

Equations

• TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.pathGroups T gs y = {I ∈ T | y ∈ TrilinearHT.Auto.dyadicGridCell A.G I.1 I.2}.biUnion gs

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.pathDepths {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (T : Finset (ℤ × ℤ)) (gs : ℤ × ℤ → Finset bf.Grp) (y : ℝ) (G : bf.Grp) : Finset ℤ

The depths of the cells of T containing y at which the group G is used.

Equations

• TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.pathDepths T gs y G = Finset.image Prod.fst ({I ∈ {I ∈ T | y ∈ TrilinearHT.Auto.dyadicGridCell A.G I.1 I.2} | G ∈ gs I})

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.mem_pathDepths {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {T : Finset (ℤ × ℤ)} {gs : ℤ × ℤ → Finset bf.Grp} {y : ℝ} {G : bf.Grp} {s : ℤ} (hs : s ∈ pathDepths T gs y G) : pathCell A.G T y s ∈ T ∧ y ∈ dyadicGridCell A.G (pathCell A.G T y s).1 (pathCell A.G T y s).2 ∧ G ∈ gs (pathCell A.G T y s)

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourRetBins {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (I : ℤ × ℤ) (xs : ℝ) (anc : ℕ → (j : Fin 4) → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))) (h : ℕ) (ε : ℝ) : Finset (ℝ × ℝ × (Fin 4 → ℝ))

The retained occupied four-core bins (all amplitudes at least ε) at a cell, group and height.

Equations

• D.fourRetBins G I xs anc h ε = {c ∈ Finset.image (D.fourBinOf G I xs anc h) (D.fourTested G I xs anc h) | ∀ (j : Fin 4), ε ≤ c.2.2 j}

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourCnt {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (I : ℤ × ℤ) (xs : ℝ) (anc : ℕ → (j : Fin 4) → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))) (h : ℕ) (c : ℝ × ℝ × (Fin 4 → ℝ)) (κ : Fin 4 → ℕ × ℕ) : ℝ

The number of tested four-core tuples in the bin c with the role types κ.

Equations

• D.fourCnt G I xs anc h c κ = ↑{p ∈ D.fourTested G I xs anc h | D.fourBinOf G I xs anc h p = c ∧ ∀ (j : Fin 4), D.classTypeOf G I j h (p j) = κ j}.card

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourRetBinsA {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (I : ℤ × ℤ) (xs : ℝ) (anc : D.AncNe G I → ℕ → (j : Fin 4) → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))) (h : ℕ) (ε : ℝ) : Finset (ℝ × ℝ × (Fin 4 → ℝ))

The retained occupied four-core bins at a cell and group, with anchors depending on a proof of AncNe G I (the alive sets of the roles at the decision cell are nonempty); empty otherwise (no anchors, no alive modes, no tested tuples).

Equations

• D.fourRetBinsA G I xs anc h ε = if hA : D.AncNe G I then D.fourRetBins G I xs (anc hA) h ε else ∅

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourCntA {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (I : ℤ × ℤ) (xs : ℝ) (anc : D.AncNe G I → ℕ → (j : Fin 4) → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))) (h : ℕ) (c : ℝ × ℝ × (Fin 4 → ℝ)) (κ : Fin 4 → ℕ × ℕ) : ℝ

The number of tested four-core tuples in the bin c with the role types κ, with anchors depending on a proof of AncNe G I; zero otherwise.

Equations

• D.fourCntA G I xs anc h c κ = if hA : D.AncNe G I then D.fourCnt G I xs (anc hA) h c κ else 0

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourCntA_nonneg {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) {G : bf.Grp} {I : ℤ × ℤ} {xs : ℝ} {anc : D.AncNe G I → ℕ → (j : Fin 4) → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))} {h : ℕ} {c : ℝ × ℝ × (Fin 4 → ℝ)} {κ : Fin 4 → ℕ × ℕ} : 0 ≤ D.fourCntA G I xs anc h c κ

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourBinSumA {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (J : ℕ) (G : bf.Grp) (I : ℤ × ℤ) (xs : ℝ) (anc : D.AncNe G I → ℕ → (j : Fin 4) → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))) (h : ℕ) : ℝ

The four-core bin sum Σ_c v(c) N_c of the tested tuples at a cell, group and height (the principal quantity of eq:principal-core), with anchors depending on a proof of AncNe G I; zero otherwise.

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.four_path_bin_bound {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) {Cj CA CT CK : ℕ} {δs W : ℝ} (hV : D.S.Valid Cj CA CT CK δs W) (hCA : 1 ≤ CA) (hCT : 4 ≤ CT) (hd2 : 2 ≤ D.S.dmax) (hD : 2 ≤ D.S.Dstar) (hB : 2 ≤ D.S.Bstar) (hQ0 : 1 ≤ D.S.Q0) (hSP : D.SP = D.S.sideParams δs) (hdD : ↑D.S.dmax ≤ D.S.Dstar) (qG : bf.Grp → ℕ) (hqG : ∀ (G : bf.Grp), 1 ≤ qG G ∧ qG G ≤ D.S.Q0) (J : ℕ) (T : Finset (ℤ × ℤ)) (gs : ℤ × ℤ → Finset bf.Grp) (z : bf.Grp → ChartTag) (hGc : ∀ I ∈ T, ∀ G ∈ gs I, (∀ (j : Fin 4), 8 * (D.Ms j G).Λ ≤ D.S.Ξ) ∧ (∀ (j : Fin 4), (D.Ms j G).zc = z G) ∧ (z G).dim ≤ D.S.dmax) (h : ℕ) (hh : 10 ≤ h) (hhJ : h ≤ D.SP.Jst) (rep : (G : bf.Grp) → (j : Fin 4) → ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (hrep : ∀ I ∈ T, ∀ G ∈ gs I, ∀ (j : Fin 4), (D.withQ0 (qG G)).RepOK G j h T (rep G j)) (anc : (I : ℤ × ℤ) → (G : bf.Grp) → D.AncNe G I → ℕ → (j : Fin 4) → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))) (hanc : ∀ (I : ℤ × ℤ) (hI : I ∈ T) (G : bf.Grp) (hG : G ∈ gs I) (hA : D.AncNe G I) (j : Fin 4) (F : Finset ((D.withQ0 (qG G)).Ms j G).Md) (hF : F ∈ (D.withQ0 (qG G)).goodCls G I j h), anc I G hA h j F = (D.withQ0 (qG G)).repAnchor G I j h (rep G j) ⋯ hF) (y : ℝ) (c : ℝ × ℝ × (Fin 4 → ℝ)) (hc : 0 < c.1 ∧ c.1 ≤ 1 ∧ 1 ≤ c.2.1) (hσ : ∀ (i : Fin 4), 0 < c.2.2 i) (κ : Fin 4 → ℕ × ℕ) {K Q : ℝ} (hK : 0 ≤ K) (hQ : 0 ≤ Q) (hcap : ∀ (i : Fin 4), ∑ G ∈ pathGroups T gs y, ↑((D.withQ0 (qG G)).fourUsedReps G h y (pathCell A.G T y) (fun (s : ℤ) => anc (pathCell A.G T y s) G) c κ (pathDepths T gs y G) i).card ≤ K * c.2.2 i ^ (-2)) : ∑ G ∈ pathGroups T gs y, ∑ s ∈ pathDepths T gs y G, (Q * fourBinVal κ' J c * (D.withQ0 (qG G)).fourCntA G (pathCell A.G T y s) y (anc (pathCell A.G T y s) G) h c κ) ^ (1 - 1 / 300 / 4) ≤ (Q * (fourKC κ' J * 2 * 12 ^ 4 * (c.1 * (c.2.1 ^ J)⁻¹))) ^ (1 - 1 / 300 / 4) * (16 / 3 * (3 * 10 ^ 11) ^ (1 / 4) * D.multPoly ^ (15 / 4) * D.ellPoly ^ (1 / 4) * (1 + Real.log (8 * c.2.1 / c.1)) ^ 4 * K ^ (2 - 1 / 300 / 2))

Blueprint lines 2783-2806 at one point, height, type tuple and four-core bin c: along the path of y through the retained cells T (groups g(I), anchors the representatives), the powered principal quantities (Q · v(c) · N_{I,G})^p, v(c) the bin value, sum to at most (Q C_J 2 · 12⁴ μ ν^{-J})^p · C_c (1 + log(8ν/μ))⁴ · K^{2-c/2}, given the path caps of eq:top-count at y (four_group_sum_side, powered_bin_sum, four_coef_sched).

theorem TrilinearHT.Auto.exists_nat_of_zpow_le_one {x : ℝ} (hx : ∃ (k : ℤ), x = 2 ^ k) (h1 : x ≤ 1) : ∃ (u : ℕ), x = 2 ^ (-↑u)

theorem TrilinearHT.Auto.exists_nat_of_one_le_zpow {x : ℝ} (hx : ∃ (k : ℤ), x = 2 ^ k) (h1 : 1 ≤ x) : ∃ (v : ℕ), x = 2 ^ ↑v

theorem TrilinearHT.Auto.four_bins_sum_le {p : ℝ} (hp : 0 < p) (J : ℕ) (hJ : 1 ≤ J) {ε U : ℝ} (hε : 0 < ε) (hεU : ε ≤ U) (B : Finset (ℝ × ℝ × (Fin 4 → ℝ))) (hB : ∀ c ∈ B, (∃ (k : ℤ), c.1 = 2 ^ k) ∧ c.1 ≤ 1 ∧ (∃ (k : ℤ), c.2.1 = 2 ^ k) ∧ 1 ≤ c.2.1 ∧ ∀ (j : Fin 4), ε ≤ c.2.2 j ∧ c.2.2 j ≤ U ∧ ∃ (k : ℤ), c.2.2 j = 2 ^ k) : ∑ c ∈ B, c.1 ^ p * (c.2.1 ^ J)⁻¹ ^ p * (1 + Real.log (8 * c.2.1 / c.1)) ^ 4 ≤ (Real.logb 2 (U / ε) + 1) ^ 4 * ∑' (t : ℕ × ℕ), (2 ^ (-p)) ^ t.1 * (2 ^ (-(↑J * p))) ^ t.2 * (4 ^ 4 * (1 + ↑t.1 + ↑t.2) ^ 4)

Blueprint lines 2802-2806 (sum over the occupied bins): for a finite set of four-core bins c = (μ, ν, σ) with dyadic bands μ ≤ 1 ≤ ν and dyadic amplitudes in [ε, U], the powered kernel factors with the logarithmic coefficient sum to at most the number (log₂(U/ε) + 1)⁴ of amplitude quadruples times the convergent band series.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourTested_eq_empty {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (I : ℤ × ℤ) (xs : ℝ) (anc : ℕ → (j : Fin 4) → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))) {h : ℕ} (hh : h < D.SP.Δ) : D.fourTested G I xs anc h = ∅

Below the height Δ there are no good modes, so no tested four-core tuples.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.card_bin_eq_sum_types {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (I : ℤ × ℤ) (xs : ℝ) (anc : ℕ → (j : Fin 4) → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))) (h : ℕ) (hcard : ∀ (j : Fin 4), ↑((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))).card ≤ D.S.Dstar) (c : ℝ × ℝ × (Fin 4 → ℝ)) : ↑{p ∈ D.fourTested G I xs anc h | D.fourBinOf G I xs anc h p = c}.card = ∑ κ ∈ Fintype.piFinset fun (x : Fin 4) => Finset.range (Nat.log 2 ⌊D.S.Dstar⌋₊ + 1) ×ˢ Finset.range (Nat.log 2 ⌊D.S.Dstar⌋₊ + 1), ↑{p ∈ D.fourTested G I xs anc h | D.fourBinOf G I xs anc h p = c ∧ ∀ (j : Fin 4), D.classTypeOf G I j h (p j) = κ j}.card

The tested tuples of a bin split by their role types, all in [0, log₂ D_*]^{2·4}.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourBin_genuine {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (hD : 2 ≤ D.S.Dstar) (G : bf.Grp) (I : ℤ × ℤ) (xs : ℝ) (anc : ℕ → (j : Fin 4) → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))) (h : ℕ) {ε U : ℝ} (hU : ∀ (j : Fin 4), ∀ F ∈ D.goodCls G I j h, D.clsSize G I j F ≤ U) {c : ℝ × ℝ × (Fin 4 → ℝ)} (hc : c ∈ {c ∈ Finset.image (D.fourBinOf G I xs anc h) (D.fourTested G I xs anc h) | ∀ (j : Fin 4), ε ≤ c.2.2 j}) : ((∃ (k : ℤ), c.1 = 2 ^ k) ∧ c.1 ≤ 1 ∧ (∃ (k : ℤ), c.2.1 = 2 ^ k) ∧ 1 ≤ c.2.1 ∧ ∀ (j : Fin 4), ε ≤ c.2.2 j ∧ c.2.2 j ≤ U ∧ ∃ (k : ℤ), c.2.2 j = 2 ^ k) ∧ 0 < c.1 ∧ ∀ (i : Fin 4), 0 < c.2.2 i

A retained occupied four-core bin is genuine and dyadic: μ ≤ 1 ≤ ν dyadic bands and amplitudes in [ε, U], dyadic, when the class sizes are at most U.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourTypes {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) : Finset (Fin 4 → ℕ × ℕ)

The role-type tuples [0, log₂ D_*]^{2·4}.

Equations

• D.fourTypes = Fintype.piFinset fun (x : Fin 4) => Finset.range (Nat.log 2 ⌊D.S.Dstar⌋₊ + 1) ×ˢ Finset.range (Nat.log 2 ⌊D.S.Dstar⌋₊ + 1)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.four_principal_split {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (hD : 2 ≤ D.S.Dstar) (J : ℕ) (G : bf.Grp) (I : ℤ × ℤ) (y : ℝ) (anc : ℕ → (j : Fin 4) → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))) (H : Finset ℕ) (hcard : ∀ (j : Fin 4), ↑((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))).card ≤ D.S.Dstar) {U ε : ℝ} (hU0 : 0 ≤ U) (hε : 0 ≤ ε) (hU : ∀ h ∈ H, ∀ (j : Fin 4), ∀ F ∈ D.goodCls G I j h, D.clsSize G I j F ≤ U) : ∑ h ∈ H, (↑H.card)⁻¹ * ∑ c ∈ Finset.image (D.fourBinOf G I y anc h) (D.fourTested G I y anc h), fourBinVal κ' J c * ↑{p ∈ D.fourTested G I y anc h | D.fourBinOf G I y anc h p = c}.card ≤ ∑ h ∈ H, ∑ κ ∈ D.fourTypes, (↑H.card)⁻¹ * ∑ c ∈ D.fourRetBins G I y anc h ε, fourBinVal κ' J c * D.fourCnt G I y anc h c κ + 2 * fourKC κ' J * 12 ^ 4 * ε * U ^ 3 * D.S.Dstar ^ 4

The per-cell decomposition of eq:core-final for four cores: the principal quantity of a cell and group at a point is at most the sum, over the heights and role types, of the retained principal quantities |H|⁻¹ Σ_{retained bins} v(c) N_{c,κ}, plus the negligible-amplitude bound.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.four_principal_splitA {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (hD : 2 ≤ D.S.Dstar) (J : ℕ) (G : bf.Grp) (I : ℤ × ℤ) (y : ℝ) (anc : D.AncNe G I → ℕ → (j : Fin 4) → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))) (H : Finset ℕ) (hcard : ∀ (j : Fin 4), ↑((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))).card ≤ D.S.Dstar) {U ε : ℝ} (hU0 : 0 ≤ U) (hε : 0 ≤ ε) (hU : ∀ h ∈ H, ∀ (j : Fin 4), ∀ F ∈ D.goodCls G I j h, D.clsSize G I j F ≤ U) : ∑ h ∈ H, (↑H.card)⁻¹ * D.fourBinSumA J G I y anc h ≤ ∑ h ∈ H, ∑ κ ∈ D.fourTypes, (↑H.card)⁻¹ * ∑ c ∈ D.fourRetBinsA G I y anc h ε, fourBinVal κ' J c * D.fourCntA G I y anc h c κ + 2 * fourKC κ' J * 12 ^ 4 * ε * U ^ 3 * D.S.Dstar ^ 4

four_principal_split with anchors depending on a proof of AncNe G I: without anchors both principal quantities vanish.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourCc {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) : ℝ

The four-core frequency constant (16/3) C^{1/4} P_w^{15/4} P_ℓ^{1/4}.

Equations

• D.fourCc = 16 / 3 * (3 * 10 ^ 11) ^ (1 / 4) * D.multPoly ^ (15 / 4) * D.ellPoly ^ (1 / 4)

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.bandC (p : ℝ) (J : ℕ) : ℝ

The convergent band series Σ_{u,v} 2^{-pu} 2^{-Jpv} (4(1+u+v))⁴.

Equations

• TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.bandC p J = ∑' (t : ℕ × ℕ), (2 ^ (-p)) ^ t.1 * (2 ^ (-(↑J * p))) ^ t.2 * (4 ^ 4 * (1 + ↑t.1 + ↑t.2) ^ 4)