Trilinear Hilbert transform: combination_bound

theorem TrilinearHT.Auto.SparseCountData.combination_bound (D : SparseCountData) (C : Finset (ℤ × (Fin 4 → ℤ))) (hC : ∀ o ∈ C, o.1 ∈ D.S ∧ o.2 ∈ D.E o.1) {δ : ℝ} (hδ : 0 < δ) (hδm : ∀ (s : ℤ), ↑{o ∈ C | o.1 = s}.card ≤ δ * D.M ^ 2) (e : Fin 3 → Fin 4) (he : Function.Injective e) (heC : ∀ (j : Fin 3), e j ∈ D.core) {l : Fin 4} (hl : ∀ (j : Fin 3), e j ≠ l) (B P : Fin 3 → Finset ℤ) (ε : Fin 3 → ℕ) (N₀ : ℕ) (Rp : Fin 3 → ℝ) (hBC : ∀ o ∈ C, ∀ (j : Fin 3), o.2 (e j) ∈ B j) (hcov : ∀ (j : Fin 3), ∀ a ∈ B j, ∀ b ∈ B j, ∃ p ∈ P j, a - b - p ∈ shiftBox D.ζ N₀ (ε j) 2) {K₁ : ℝ} (hK : 0 ≤ K₁) (hP : ∀ (j : Fin 3), ↑(P j).card ≤ K₁ * D.M) (hε : ∀ (j : Fin 3), ↑(ε j) ≤ 17 * D.ν * Rp j) (hRp : ∀ (j : Fin 3), ∀ o ∈ C, Rp j < D.R o.1) (hN₀ : ↑N₀ ≤ 33 * D.B) {g : ℕ} (hg : 1 ≤ g) (hgΓ : 612000000 * (↑D.d + 1) ^ 2 * D.ν ≤ 2 ^ g * D.μ) (hQ : 7200000 * (↑D.d + 1) ^ 2 * D.B ≤ D.Q) (hSg : 700000 * (↑D.d + 1) ^ 2 * D.ν ≤ D.Sg) (hbig : 12 * ↑g * δ * D.M ^ 2 < ↑C.card) (hCL : ↑C.card ≤ ↑D.L * D.M ^ 2) : (↑C.card / D.M ^ 2) ^ 10 ≤ 10 ^ 6 * δ * ↑g * K₁ ^ 7 * ↑D.L ^ 9

Blueprint lines 2640-2698 (one combination): occurrences of one block whose three future roles lie in fixed future cover subsets B_j (with difference covers of size at most K₁ M relative to the future block widths) have normalized mass ρ = |C|/M² with ρ ≤ 12 g δ or ρ¹⁰ ≤ 10⁶ δ g K₁⁷ L⁹, where 2^g exceeds the margin Γ.

Counting blocks (lem:sparse-count, blueprint lines 2613-2616)

noncomputable def TrilinearHT.Auto.blockIndex {α : Type u_1} (C : Finset (ℤ × α)) (θ : ℝ) (s : ℤ) : ℕ

The counting block of scale s: ⌊G(s)/θ⌋ for the mass G(s) of scales ≥ s.

Equations

• TrilinearHT.Auto.blockIndex C θ s = ⌊↑(TrilinearHT.Auto.upperMass C s) / θ⌋₊

theorem TrilinearHT.Auto.upperMass_anti {α : Type u_1} (C : Finset (ℤ × α)) {s s' : ℤ} (h : s ≤ s') : upperMass C s' ≤ upperMass C s

theorem TrilinearHT.Auto.blockIndex_anti {α : Type u_1} (C : Finset (ℤ × α)) {θ : ℝ} (hθ : 0 < θ) {s s' : ℤ} (h : s ≤ s') : blockIndex C θ s' ≤ blockIndex C θ s

Larger scales lie in earlier (or equal) blocks.

theorem TrilinearHT.Auto.lt_of_blockIndex_lt {α : Type u_1} (C : Finset (ℤ × α)) {θ : ℝ} (hθ : 0 < θ) {s s' : ℤ} (h : blockIndex C θ s < blockIndex C θ s') : s' < s

A later block consists of strictly smaller scales.

theorem TrilinearHT.Auto.blockIndex_lt {α : Type u_1} (C : Finset (ℤ × α)) {θ : ℝ} (hθ : 0 < θ) (s : ℤ) : blockIndex C θ s < ⌊↑C.card / θ⌋₊ + 1

theorem TrilinearHT.Auto.block_mass_le {α : Type u_1} (C : Finset (ℤ × α)) {θ m₀ : ℝ} (hθ : 0 < θ) (hm : ∀ (s : ℤ), ↑{o ∈ C | o.1 = s}.card ≤ m₀) (b : ℕ) : ↑{o ∈ C | blockIndex C θ o.1 = b}.card ≤ θ + m₀

Blueprint lines 2614-2615: each counting block has mass at most θ + m₀, where m₀ bounds the mass of a single scale.

theorem TrilinearHT.Auto.nonfuture_pair_sum {ι : Type u_1} (J : Finset ι) (m m' mass : ι → ℝ) (hm : ∀ b ∈ J, 0 ≤ m b) (hm' : ∀ b ∈ J, 0 ≤ m' b) (hmass0 : ∀ b ∈ J, 0 ≤ mass b) {c L M : ℝ} (hc : 0 ≤ c) (hL : 0 ≤ L) (hmc : ∀ b ∈ J, mass b ≤ c) (hmL : ∀ b ∈ J, mass b ≤ L * m b * m' b) (hsum : ∑ b ∈ J, m b ≤ M) (hsum' : ∑ b ∈ J, m' b ≤ M) : ∑ b ∈ J, mass b ≤ √(c * L) * M

Blueprint lines 2628-2633 (nonfuture pairs): if the block masses satisfy mass_b ≤ min(c, L m_b m'_b) and Σ_b m_b, Σ_b m'_b ≤ M, then Σ_b mass_b ≤ √(c L) M.

theorem TrilinearHT.Auto.sum_card_disjoint_le {ι : Type u_1} (J : Finset ι) (X : ι → Finset ℤ) (A : Finset ℤ) (hX : ∀ b ∈ J, X b ⊆ A) (hdis : ∀ b ∈ J, ∀ b' ∈ J, b ≠ b' → Disjoint (X b) (X b')) {M : ℝ} (hA : ↑A.card ≤ M) : ∑ b ∈ J, ↑(X b).card ≤ M

Disjoint subsets of a set of size at most M have total size at most M.

theorem TrilinearHT.Auto.SparseCountData.uncovered_mass_le (D : SparseCountData) (Occ : Finset (ℤ × (Fin 4 → ℤ))) (β : ℤ → ℕ) (J₀ : ℕ) (hβ : ∀ o ∈ Occ, β o.1 < J₀) (𝓑 : ℕ → Fin 4 → Finset (Finset ℤ)) {c : ℝ} (hc : ∀ b < J₀, ∀ i ∈ D.core, ↑{o ∈ {o ∈ Occ | β o.1 = b} | ∀ B ∈ 𝓑 b i, o.2 i ∉ B}.card ≤ c) : ↑{o ∈ Occ | ∃ i ∈ D.core, ∀ B ∈ 𝓑 (β o.1) i, o.2 i ∉ B}.card ≤ ↑J₀ * ↑D.core.card * c

Blueprint line 2627 (uncovered occurrences): occurrences missing an own-block covered label in some core role have mass at most J₀ · |core| · c if each block and role contributes ≤ c.

theorem TrilinearHT.Auto.SparseCountData.pair_nonfuture_mass_le (D : SparseCountData) (Occ : Finset (ℤ × (Fin 4 → ℤ))) (hOcc : ∀ o ∈ Occ, o.1 ∈ D.S ∧ o.2 ∈ D.E o.1) (β : ℤ → ℕ) (J₀ : ℕ) (hβ : ∀ o ∈ Occ, β o.1 < J₀) (NF : ℕ → Fin 4 → Finset ℤ) {i j : Fin 4} (hi : i ∈ D.core) (hj : j ∈ D.core) (hij : i ≠ j) (hNFA : ∀ (b : ℕ), ∀ r ∈ D.core, NF b r ⊆ D.A r) (hNFdis : ∀ r ∈ D.core, ∀ b ∈ Finset.range J₀, ∀ b' ∈ Finset.range J₀, b ≠ b' → Disjoint (NF b r) (NF b' r)) {c : ℝ} (hc : 0 ≤ c) (hblock : ∀ (b : ℕ), ↑{o ∈ Occ | β o.1 = b}.card ≤ c) : ↑{o ∈ Occ | o.2 i ∈ NF (β o.1) i ∧ o.2 j ∈ NF (β o.1) j}.card ≤ √(c * ↑D.L) * D.M

Blueprint lines 2628-2633 (two nonfuture core roles): occurrences whose labels in two distinct core roles are nonfuture labels of their block have mass at most √(c L) M, when each block has mass at most c.

theorem TrilinearHT.Auto.SparseCountData.side_nonfuture_mass_le (D : SparseCountData) (h3 : D.core.card = 3) (Occ : Finset (ℤ × (Fin 4 → ℤ))) (hOcc : ∀ o ∈ Occ, o.1 ∈ D.S ∧ o.2 ∈ D.E o.1) (β : ℤ → ℕ) (J₀ : ℕ) (hβ : ∀ o ∈ Occ, β o.1 < J₀) (NF : ℕ → Fin 4 → Finset ℤ) {i : Fin 4} (hi : i ∈ D.core) (hNFA : ∀ (b : ℕ), NF b i ⊆ D.A i) (hNFdis : ∀ b ∈ Finset.range J₀, ∀ b' ∈ Finset.range J₀, b ≠ b' → Disjoint (NF b i) (NF b' i)) {c : ℝ} (hc : 0 ≤ c) (hblock : ∀ (b : ℕ), ↑{o ∈ Occ | β o.1 = b}.card ≤ c) : ↑{o ∈ Occ | o.2 i ∈ NF (β o.1) i}.card ≤ √(c * 1) * D.M

Blueprint lines 2628-2633 (a nonfuture core role and the side role, three cores): the side incidence w_s gives mass_b ≤ m_b Σ_{s ∈ b} w_s, so these occurrences have mass at most √c M when each block has mass at most c.

noncomputable def TrilinearHT.Auto.SparseCountData.lightOcc (D : SparseCountData) (δ : ℝ) : Finset (ℤ × (Fin 4 → ℤ))

The occurrences at scales of mass at most δ M².

Equations

• D.lightOcc δ = {s ∈ D.S | ↑(D.E s).card ≤ δ * D.M ^ 2}.biUnion fun (s : ℤ) => Finset.image (fun (x : Fin 4 → ℤ) => (s, x)) (D.E s)

theorem TrilinearHT.Auto.SparseCountData.mem_lightOcc (D : SparseCountData) {δ : ℝ} {o : ℤ × (Fin 4 → ℤ)} (ho : o ∈ D.lightOcc δ) : o.1 ∈ D.S ∧ o.2 ∈ D.E o.1 ∧ ↑(D.E o.1).card ≤ δ * D.M ^ 2

theorem TrilinearHT.Auto.SparseCountData.card_lightOcc (D : SparseCountData) (δ : ℝ) : ↑(D.lightOcc δ).card = ∑ s ∈ D.S with ↑(D.E s).card ≤ δ * D.M ^ 2, ↑(D.E s).card

theorem TrilinearHT.Auto.SparseCountData.lightOcc_scale_mass (D : SparseCountData) {δ : ℝ} (hδ : 0 ≤ δ) (s : ℤ) : ↑{o ∈ D.lightOcc δ | o.1 = s}.card ≤ δ * D.M ^ 2

theorem TrilinearHT.Auto.SparseCountData.block_covers (D : SparseCountData) (Occ : Finset (ℤ × (Fin 4 → ℤ))) (hOcc : ∀ o ∈ Occ, o.1 ∈ D.S ∧ o.2 ∈ D.E o.1) (β : ℤ → ℕ) (hβlt : ∀ o ∈ Occ, ∀ o' ∈ Occ, β o.1 < β o'.1 → o'.1 < o.1) (N₀ : ℕ) (hN₀ : 24 * D.B ≤ ↑N₀) {η : ℝ} (hη : 0 < η) : ∃ (Rp : ℕ → ℝ) (ε : ℕ → ℕ) (𝓑 : ℕ → Fin 4 → Finset (Finset ℤ)) (Pc : ℕ → Fin 4 → Finset ℤ → Finset ℤ), (∀ (b : ℕ), ∀ o ∈ Occ, β o.1 < b → Rp b < D.R o.1) ∧ (∀ (b : ℕ), ↑(ε b) ≤ 17 * D.ν * Rp b) ∧ (∀ (b : ℕ), ∀ i ∈ D.core, ∀ B ∈ 𝓑 b i, B ⊆ D.A i) ∧ (∀ (b : ℕ), ∀ i ∈ D.core, ∀ B ∈ 𝓑 b i, ∀ B' ∈ 𝓑 b i, B ≠ B' → Disjoint B B') ∧ (∀ (b : ℕ), ∀ i ∈ D.core, ↑(𝓑 b i).card ≤ 3 / η) ∧ (∀ (b : ℕ), ∀ i ∈ D.core, ∀ B ∈ 𝓑 b i, ↑(Pc b i B).card ≤ 160000 / η ^ 5 * D.M ∧ ∀ a ∈ B, ∀ a' ∈ B, ∃ p ∈ Pc b i B, a - a' - p ∈ shiftBox D.ζ N₀ (ε b) 2) ∧ ∀ (b : ℕ), ∀ i ∈ D.core, ↑{o ∈ {o ∈ Occ | β o.1 = b} | ∀ B ∈ 𝓑 b i, o.2 i ∉ B}.card ≤ η * ↑D.L * D.M ^ 2

Blueprint lines 2613-2626 (difference covers in every block and role): for occurrences split into blocks β with later blocks at strictly smaller scales, there are block widths ε_b with ε_b ≤ 17 ν R_b^+, where R_b^+ is below every scale of an earlier block, and in each block and core role a cover family as in cover_family.

noncomputable def TrilinearHT.Auto.SparseCountData.enumRoles (T : Finset (Fin 4)) : Fin 3 → Fin 4

An enumeration of a three-element set of roles.

Equations

• TrilinearHT.Auto.SparseCountData.enumRoles T = if h : T.card = 3 then fun (j : Fin 3) => (T.orderEmbOfFin h) j else fun (x : Fin 3) => 0

theorem TrilinearHT.Auto.SparseCountData.enumRoles_spec {T : Finset (Fin 4)} (h : T.card = 3) : Function.Injective (enumRoles T) ∧ ∀ (j : Fin 3), enumRoles T j ∈ T

theorem TrilinearHT.Auto.SparseCountData.combinations_mass_le (D : SparseCountData) (Occ : Finset (ℤ × (Fin 4 → ℤ))) (hOcc : ∀ o ∈ Occ, o.1 ∈ D.S ∧ o.2 ∈ D.E o.1) {δ : ℝ} (hδ : 0 < δ) (hδm : ∀ (s : ℤ), ↑{o ∈ Occ | o.1 = s}.card ≤ δ * D.M ^ 2) (hOccL : ↑Occ.card ≤ ↑D.L * D.M ^ 2) (β : ℤ → ℕ) (J₀ : ℕ) (hβ : ∀ o ∈ Occ, β o.1 < J₀) (N₀ : ℕ) (hN₀ : ↑N₀ ≤ 33 * D.B) {η : ℝ} (hη : 0 < η) (Rp : ℕ → ℝ) (ε : ℕ → ℕ) (𝓑 : ℕ → Fin 4 → Finset (Finset ℤ)) (Pc : ℕ → Fin 4 → Finset ℤ → Finset ℤ) (hRp : ∀ (b : ℕ), ∀ o ∈ Occ, β o.1 < b → Rp b < D.R o.1) (hε : ∀ (b : ℕ), ↑(ε b) ≤ 17 * D.ν * Rp b) (h𝓑card : ∀ (b : ℕ), ∀ i ∈ D.core, ↑(𝓑 b i).card ≤ 3 / η) (hPc : ∀ (b : ℕ), ∀ i ∈ D.core, ∀ B ∈ 𝓑 b i, ↑(Pc b i B).card ≤ 160000 / η ^ 5 * D.M ∧ ∀ a ∈ B, ∀ a' ∈ B, ∃ p ∈ Pc b i B, a - a' - p ∈ shiftBox D.ζ N₀ (ε b) 2) {g : ℕ} (hg : 1 ≤ g) (hgΓ : 612000000 * (↑D.d + 1) ^ 2 * D.ν ≤ 2 ^ g * D.μ) (hQ : 7200000 * (↑D.d + 1) ^ 2 * D.B ≤ D.Q) (hSg : 700000 * (↑D.d + 1) ^ 2 * D.ν ≤ D.Sg) {Y : ℝ} (hY1 : 12 * ↑g * δ * D.M ^ 2 ≤ Y) (hY2 : ∀ (x : ℝ), 0 ≤ x → (x / D.M ^ 2) ^ 10 ≤ 10 ^ 6 * δ * ↑g * (160000 / η ^ 5) ^ 7 * ↑D.L ^ 9 → x ≤ Y) : ↑{o ∈ Occ | 3 ≤ {i ∈ D.core | ∃ b' ∈ Finset.range J₀, β o.1 < b' ∧ ∃ B ∈ 𝓑 b' i, o.2 i ∈ B}.card}.card ≤ ↑J₀ * 4 * (12 * ↑J₀ / η) ^ 3 * Y

Blueprint lines 2634-2638 (combinations): occurrences all of whose core labels are covered in their own block and which have at least three future roles are grouped by their block, a triple of future roles and future cover subsets for them; there are at most J₀ · 4 · (12 J₀/η)³ combinations, and each has mass at most Y by combination_bound.

theorem TrilinearHT.Auto.SparseCountData.nonfuture_mass_le (D : SparseCountData) (Occ : Finset (ℤ × (Fin 4 → ℤ))) (hOcc : ∀ o ∈ Occ, o.1 ∈ D.S ∧ o.2 ∈ D.E o.1) (β : ℤ → ℕ) (J₀ : ℕ) (hβ : ∀ o ∈ Occ, β o.1 < J₀) (𝓑 : ℕ → Fin 4 → Finset (Finset ℤ)) (hA : ∀ (b : ℕ), ∀ i ∈ D.core, ∀ B ∈ 𝓑 b i, B ⊆ D.A i) {c : ℝ} (hc : 0 ≤ c) (hblock : ∀ (b : ℕ), ↑{o ∈ Occ | β o.1 = b}.card ≤ c) : ↑{o ∈ Occ | (∀ i ∈ D.core, ∃ B ∈ 𝓑 (β o.1) i, o.2 i ∈ B) ∧ {i ∈ D.core | ∃ b' ∈ Finset.range J₀, β o.1 < b' ∧ ∃ B ∈ 𝓑 b' i, o.2 i ∈ B}.card < 3}.card ≤ 16 * (√(c * ↑D.L) * D.M)

Blueprint lines 2628-2633 (all nonfuture terms): occurrences with every core label covered in its block but fewer than three future core roles have mass at most 16 √(c L) M.

theorem TrilinearHT.Auto.sparse_final_arith {X J₀ L ℓ τ M U₁ U₂ U₃ : ℝ} (hτ0 : 0 < τ) (hL : 1 ≤ L) (hℓ : 1 ≤ ℓ) (hM : 0 < M) (hJ0 : 0 ≤ J₀) (hJ : J₀ ≤ 3 * L * τ⁻¹ ^ 2) (hX : X ≤ U₁ + U₂ + U₃) (h1 : U₁ ≤ J₀ * 4 * (τ ^ 3 / L * L * M ^ 2)) (h2 : U₂ ≤ 16 * (√(2 * (τ ^ 2 * M ^ 2) * L) * M)) (h3 : U₃ ≤ J₀ * 4 * (12 * J₀ / (τ ^ 3 / L)) ^ 3 * (10 ^ 5 * ℓ * (τ ^ 3 / L)⁻¹ ^ 4 * L * τ ^ 30 * M ^ 2)) : X ≤ 10 ^ 11 * ℓ * L ^ 12 * τ * M ^ 2

Blueprint lines 2700-2705 (final count): the uncovered, nonfuture and combination masses sum to at most 10¹¹ ℓ L¹² τ M² (via eq:count-balance).

theorem TrilinearHT.Auto.exists_scale_margin {d : ℕ} {μ ν : ℝ} (hμ : 0 < μ) (hμν : μ ≤ ν) : ∃ (g : ℕ), 1 ≤ g ∧ 612000000 * (↑d + 1) ^ 2 * ν ≤ 2 ^ g * μ ∧ ↑g ≤ 32 * (1 + Real.logb 2 (2 + (↑d + 1) ^ 2 * ν / μ))

The logarithmic scale margin: there is g ≤ 32 ℓ with 2^g μ ≥ 612000000 (d+1)² ν, where ℓ = 1 + log₂(2 + (d+1)² ν/μ).

theorem TrilinearHT.Auto.sparse_Y1_arith {M δ τ g ℓ η L : ℝ} (hM : 0 < M) (hτ0 : 0 < τ) (hτ1 : τ ≤ 1) (hδ : δ = τ ^ 300) (hg : g ≤ 32 * ℓ) (hℓ : 1 ≤ ℓ) (hη : 0 < η) (hη1 : η ≤ 1) (hL : 1 ≤ L) : 12 * g * δ * M ^ 2 ≤ 10 ^ 5 * ℓ * η⁻¹ ^ 4 * L * τ ^ 30 * M ^ 2

theorem TrilinearHT.Auto.sparse_Y2_arith {x M δ τ g ℓ η L : ℝ} (hM : 0 < M) (hx : 0 ≤ x) (hτ0 : 0 < τ) (hδ : δ = τ ^ 300) (hg : g ≤ 32 * ℓ) (hℓ : 1 ≤ ℓ) (hη : 0 < η) (hη1 : η ≤ 1) (hL : 1 ≤ L) (h : (x / M ^ 2) ^ 10 ≤ 10 ^ 6 * δ * g * (160000 / η ^ 5) ^ 7 * L ^ 9) : x ≤ 10 ^ 5 * ℓ * η⁻¹ ^ 4 * L * τ ^ 30 * M ^ 2

theorem TrilinearHT.Auto.SparseCountData.sparse_mass_bound (D : SparseCountData) (hQ : 7200000 * (↑D.d + 1) ^ 2 * D.B ≤ D.Q) (hSg : 700000 * (↑D.d + 1) ^ 2 * D.ν ≤ D.Sg) {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ ≤ 1) : ∑ s ∈ D.S with ↑(D.E s).card ≤ δ * D.M ^ 2, ↑(D.E s).card ≤ 10 ^ 11 * (1 + Real.logb 2 (2 + (↑D.d + 1) ^ 2 * D.ν / D.μ)) * ↑D.L ^ 12 * δ ^ (1 / 300) * D.M ^ 2

Blueprint lem:sparse-count, eq:sparse-count for the grid data: with the reserves Q ≥ 7.2·10⁶ (d+1)² B and Σ ≥ 7·10⁵ (d+1)² ν, for 0 < δ ≤ 1, Σ_{s : N_s ≤ δ M²} N_s ≤ 10¹¹ ℓ L¹² δ^{1/300} M² with ℓ = 1 + log₂(2 + (d+1)² ν/μ).

Reduction to a common grid (lem:sparse-count, blueprint lines 2606-2607)

noncomputable def TrilinearHT.Auto.gridLabel (h x : ℝ) : ℤ

Rounding of a label to the grid 6hℤ, in grid units.

Equations

• TrilinearHT.Auto.gridLabel h x = 6 * round (x / (6 * h))

theorem TrilinearHT.Auto.gridLabel_err {h : ℝ} (hh : 0 < h) (x : ℝ) : |h * ↑(gridLabel h x) - x| ≤ 3 * h

theorem TrilinearHT.Auto.six_dvd_gridLabel (h x : ℝ) : 6 ∣ gridLabel h x

theorem TrilinearHT.Auto.round_err {h : ℝ} (hh : 0 < h) (x : ℝ) : |h * ↑(round (x / h)) - x| ≤ h / 2

theorem TrilinearHT.Auto.gridLabel_close {h : ℝ} (hh : 0 < h) {x y : ℝ} (hxy : gridLabel h x = gridLabel h y) : |x - y| ≤ 6 * h

Equal grid labels force close labels: |x - y| ≤ 6h.

theorem TrilinearHT.Auto.shift_round_err {d : ℕ} {h Q : ℝ} (hh : 0 < h) (ζ : Fin d → ℝ) (n : Fin d → ℤ) (hn : ∀ (k : Fin d), |↑(n k)| ≤ Q) : |h * ↑(shiftDot n fun (k : Fin d) => round (ζ k / h)) - ∑ k : Fin d, ↑(n k) * ζ k| ≤ ↑d * Q * h / 2

The pure-shift error of rounded frequencies: |h n·ζ' - n·ζ| ≤ d Q h / 2.

theorem TrilinearHT.Auto.logb_scale_bound {y : ℝ} (hy : 0 ≤ y) : 1 + Real.logb 2 (2 + 4 * y) ≤ 3 * (1 + Real.logb 2 (2 + y)) ∧ 0 ≤ 1 + Real.logb 2 (2 + 4 * y)

theorem TrilinearHT.Auto.sparse_count_final_arith {X δ L μ ν M : ℝ} {d : ℕ} (hδ0 : 0 < δ) (hL : 1 ≤ L) (hμ : 0 < μ) (hν : 0 ≤ ν) (h : X ≤ 10 ^ 11 * (1 + Real.logb 2 (2 + (↑d + 1) ^ 2 * (2 * ν) / (μ / 2))) * ↑⌊L⌋₊ ^ 12 * δ ^ (1 / 300) * M ^ 2) : X ≤ 3 * 10 ^ 11 * (1 + Real.logb 2 (2 + (↑d + 1) ^ 2 * ν / μ)) * L ^ 12 * δ ^ (1 / 300) * M ^ 2