Trilinear Hilbert transform: triple_count_bound

theorem TrilinearHT.Auto.triple_count_bound {d : ℕ} {ι : Type u_1} (ζ : Fin d → ℤ) (N H : ℕ) (ε : Fin 3 → ℕ) (α β : Fin 3 → ℤ) (hαβ : ∀ (j : Fin 3), α j * β j = 6) (hα3 : ∀ (j : Fin 3), |α j| ≤ 3) (B B₀ P : Fin 3 → Finset ℤ) (hB₀ : ∀ (j : Fin 3), B₀ j ⊆ B j) (hB₀ne : ∀ (j : Fin 3), (B₀ j).Nonempty) (hcov : ∀ (j : Fin 3), ∀ a ∈ B j, ∀ b ∈ B j, ∃ p ∈ P j, a - b - p ∈ shiftBox ζ N (ε j) 2) (hdouble : ∀ (j : Fin 3), (shiftBox ζ N (ε j) (H + 2)).card ≤ 2 * (shiftBox ζ N (ε j) H).card) {Q S μ ν Rs Bw : ℝ} (hRs : 0 ≤ Rs) (hν : 0 ≤ ν) (hBw : 0 ≤ Bw) (hanch : ∀ (j : Fin 3), ∀ a ∈ B₀ j, ∀ a' ∈ B₀ j, ∀ (k : Fin d → ℤ), (∀ (i : Fin d), |↑(k i)| ≤ Q) → |↑(a - a' - shiftDot k ζ)| ≤ S → a = a') (V : Finset ι) (tv : ι → Fin 3 → ℤ) (htv : ∀ v ∈ V, ∀ (j : Fin 3), tv v j ∈ B j) (Rv : ι → ℝ) (F : Finset (Fin 3 → ℤ)) (hF : ∀ f ∈ F, ∀ (j : Fin 3), f j ∈ B j) (Rf : (Fin 3 → ℤ) → ℝ) (nv : ι → Fin d → ℤ) (nf : (Fin 3 → ℤ) → Fin d → ℤ) (hnv : ∀ v ∈ V, ∀ (i : Fin d), |↑(nv v i)| ≤ Bw) (hnf : ∀ f ∈ F, ∀ (i : Fin d), |↑(nf f i)| ≤ Bw) (hannv : ∀ v ∈ V, μ * Rv v ≤ |↑(tripleResidual ζ α (tv v) (nv v))| ∧ |↑(tripleResidual ζ α (tv v) (nv v))| ≤ ν * Rv v) (hannf : ∀ f ∈ F, |↑(tripleResidual ζ α f (nf f))| ≤ ν * Rf f) (hRv : ∀ v ∈ V, Rv v ≤ Rs) (hRf : ∀ f ∈ F, Rf f ≤ Rs) (hsepF : ∀ f ∈ F, ∀ f' ∈ F, ∀ (j : Fin 3) (k : Fin d → ℤ), (∀ (i : Fin d), |↑(k i)| ≤ Q) → |↑(f j - f' j - shiftDot k ζ)| ≤ 4 * (↑H * ↑(ε j)) → f j = f' j) (hdist : ∀ v ∈ V, ∀ v' ∈ V, v ≠ v' → Rv v' < Rv v ∨ Rv v < Rv v') (hsmallv : ∀ v ∈ V, ∀ v' ∈ V, Rv v' < Rv v → ν * Rv v' ≤ μ * Rv v / 1000) (hsmallf : ∀ v ∈ V, ∀ f ∈ F, ν * Rf f ≤ μ * Rv v / 1000) (hsmallε : ∀ v ∈ V, ∀ (j : Fin 3), 36 * (↑H * ↑(ε j)) ≤ μ * Rv v / 1000) (hgap : ∀ v ∈ V, ∀ (m : Fin d → ℤ), (∀ (i : Fin d), |↑(m i)| ≤ Q) → ¬(μ * Rv v / 50 ≤ |↑(shiftDot m ζ)| ∧ |↑(shiftDot m ζ)| ≤ 50 * ν * Rv v)) (hQ : 144 * Bw + 216 * (↑H * ↑N) ≤ Q) (hS : 12 * (↑H * (↑(ε 0) + ↑(ε 1) + ↑(ε 2))) + 4 * ν * Rs ≤ S) (hμR : ∀ v ∈ V, 0 ≤ μ * Rv v) : ↑(V.card * F.card) ≤ (2 * ↑(P 0).card / ↑(B₀ 0).card) ^ 2 * ↑(B₀ 0).card * ((2 * ↑(P 1).card / ↑(B₀ 1).card) ^ 2 * ↑(B₀ 1).card) * (2 * ↑(P 2).card / ↑(B₀ 2).card) ^ 3

Blueprint lines 2678-2694 (slab cover and separation of translated triples): with growth data for three roles, the indexed outputs t_v + f of the selected middle-range triples t_v and the last-range triples f ∈ F lie in distinct cover boxes, so q |F| ≤ (2|P₀|/|B₀₀|)² |B₀₀| (2|P₁|/|B₀₁|)² |B₀₁| (2|P₂|/|B₀₂|)³.

The integer form of the sparse-count data (blueprint lines 2587-2604)

def TrilinearHT.Auto.roleCoeff (r l : Fin 4) : ℤ

The progression coefficient α_r = r - l' of role r for the excluded role l'.

Equations

• TrilinearHT.Auto.roleCoeff r l = ↑↑r - ↑↑l

theorem TrilinearHT.Auto.roleCoeff_table (r l : Fin 4) : r ≠ l → |roleCoeff r l| ≤ 3 ∧ roleCoeff r l * (6 / roleCoeff r l) = 6

theorem TrilinearHT.Auto.roleCoeff_spec {r l : Fin 4} (h : r ≠ l) : |roleCoeff r l| ≤ 3 ∧ ∃ (β : ℤ), roleCoeff r l * β = 6

structure TrilinearHT.Auto.SparseCountData : Type

Blueprint lem:sparse-count, data after the reduction to a common grid: integer labels divisible by six, integer reserved frequencies ζ, scales R_s = R₀ 2^s, and the five hypotheses (pair determination with multiplicity L, side incidence, separation, annular witnesses, and the pure-shift gap with the relaxed constants).

• d : ℕ

  Dimension of the integer relation used in sparse counting.

• ζ : Fin self.d → ℤ

  Integer coefficients of the sparse-counting relation.

• core : Finset (Fin 4)

  Set of three or four core slots participating in sparse counting.

• core_card : self.core.card = 3 ∨ self.core.card = 4
• S : Finset ℤ

  Finite set of integer scales used in the counting estimate.

• R₀ : ℝ

  Positive base length defining the physical scale at integer depth s.

• R₀_pos : 0 < self.R₀
• E : ℤ → Finset (Fin 4 → ℤ)

  Finite family of integer slot tuples at each scale.

• A : Fin 4 → Finset ℤ

  Allowed coordinate values in each slot.

• M : ℝ

  Uniform bound for the allowed coordinate counts and total incidence weight.

• one_le_M : 1 ≤ self.M
• card_A (i : Fin 4) : i ∈ self.core → ↑(self.A i).card ≤ self.M
• mem_A (s : ℤ) : s ∈ self.S → ∀ x ∈ self.E s, ∀ i ∈ self.core, x i ∈ self.A i
• six_dvd (s : ℤ) : s ∈ self.S → ∀ x ∈ self.E s, ∀ i ∈ self.core, 6 ∣ x i
• L : ℕ

  Upper bound for the number of scales sharing the same slot tuple.

• one_le_L : 1 ≤ self.L
• pair (i : Fin 4) : i ∈ self.core → ∀ j ∈ self.core, i ≠ j → ∀ s ∈ self.S, ∀ s' ∈ self.S, ∀ x ∈ self.E s, ∀ x' ∈ self.E s', x i = x' i → x j = x' j → x = x'
• mult (x : Fin 4 → ℤ) : {s ∈ self.S | x ∈ self.E s}.card ≤ self.L
• w : ℤ → ℝ

  Nonnegative scale weights controlling triple-core coordinate incidences.

• w_nonneg (s : ℤ) : 0 ≤ self.w s
• w_sum : ∑ s ∈ self.S, self.w s ≤ self.M
• w_inc : self.core.card = 3 → ∀ s ∈ self.S, ∀ i ∈ self.core, ∀ (a : ℤ), ↑{x ∈ self.E s | x i = a}.card ≤ self.w s
• μ : ℝ

  Positive lower frequency scale in the sparse-counting separation assumptions.

• ν : ℝ

  Upper frequency scale dominating the lower scale.

• Sg : ℝ

  Separation parameter entering the sparse-counting hypotheses.

• Q : ℝ

  Arithmetic parameter of the sparse-counting frequency relations.

• B : ℝ

  Positive complexity bound used in the sparse-counting estimates.

• μ_pos : 0 < self.μ
• μ_le_ν : self.μ ≤ self.ν
• one_le_B : 1 ≤ self.B
• one_le_μR (s : ℤ) : s ∈ self.S → 1 ≤ self.μ * (self.R₀ * 2 ^ s)
• sep (i : Fin 4) : i ∈ self.core → ∀ s ∈ self.S, ∀ s' ∈ self.S, ∀ x ∈ self.E s, ∀ x' ∈ self.E s', x i ≠ x' i → ∀ (n : Fin self.d → ℤ), (∀ (r : Fin self.d), |↑(n r)| ≤ self.Q) → self.Sg * max (self.R₀ * 2 ^ s) (self.R₀ * 2 ^ s') < |↑(x i - x' i + shiftDot n self.ζ)|
• ann (T : Finset (Fin 4)) : T ⊆ self.core → T.card = 3 → ∀ l ∉ T, ∀ s ∈ self.S, ∀ x ∈ self.E s, ∃ (n : Fin self.d → ℤ), (∀ (r : Fin self.d), |↑(n r)| ≤ self.B) ∧ self.μ * (self.R₀ * 2 ^ s) ≤ |↑(∑ r ∈ T, roleCoeff r l * x r + 36 * shiftDot n self.ζ)| ∧ |↑(∑ r ∈ T, roleCoeff r l * x r + 36 * shiftDot n self.ζ)| ≤ self.ν * (self.R₀ * 2 ^ s)
• gap (s : ℤ) : s ∈ self.S → (self.E s).Nonempty → ∀ (n : Fin self.d → ℤ), (∀ (r : Fin self.d), |↑(n r)| ≤ self.Q) → ¬(self.μ * (self.R₀ * 2 ^ s) / 50 ≤ |↑(shiftDot n self.ζ)| ∧ |↑(shiftDot n self.ζ)| ≤ 50 * self.ν * (self.R₀ * 2 ^ s))

noncomputable def TrilinearHT.Auto.SparseCountData.R (D : SparseCountData) (s : ℤ) : ℝ

The scale R_s = R₀ 2^s.

Equations

• D.R s = D.R₀ * 2 ^ s

theorem TrilinearHT.Auto.SparseCountData.R_pos (D : SparseCountData) (s : ℤ) : 0 < D.R s

theorem TrilinearHT.Auto.SparseCountData.R_strictMono (D : SparseCountData) : StrictMono D.R

theorem TrilinearHT.Auto.SparseCountData.R_add (D : SparseCountData) (s : ℤ) (g : ℕ) : D.R (s + ↑g) = 2 ^ g * D.R s

theorem TrilinearHT.Auto.SparseCountData.exists_two_other (D : SparseCountData) {i : Fin 4} (hi : i ∈ D.core) : ∃ j ∈ D.core, ∃ k ∈ D.core, i ≠ j ∧ i ≠ k ∧ j ≠ k

Three distinct core roles exist besides any given core role.

theorem TrilinearHT.Auto.SparseCountData.total_mass_le (D : SparseCountData) (S' : Finset ℤ) (hS' : S' ⊆ D.S) : ∑ s ∈ S', ↑(D.E s).card ≤ ↑D.L * D.M ^ 2

The total mass is at most L M² (pair determination and multiplicity).

Blocks and difference covers (lem:sparse-count, blueprint lines 2611-2626)

theorem TrilinearHT.Auto.SparseCountData.pair_fiber_le (D : SparseCountData) (O : Finset (ℤ × (Fin 4 → ℤ))) (hO : ∀ o ∈ O, o.1 ∈ D.S ∧ o.2 ∈ D.E o.1) {i j : Fin 4} (hi : i ∈ D.core) (hj : j ∈ D.core) (hij : i ≠ j) (e : ℤ × ℤ) : {o ∈ O | (o.2 i, o.2 j) = e}.card ≤ D.L

Occurrences with a common pair of labels in two distinct core roles have at most L elements (pair determination and multiplicity).

theorem TrilinearHT.Auto.SparseCountData.card_pow_four_le {n : ℕ} {M : ℝ} (h : ↑n ≤ M) : ↑(n * (n * (n * n))) ≤ M ^ 4

theorem TrilinearHT.Auto.SparseCountData.cover_count_arith {P κ : ℕ} {M η : ℝ} (hη : 0 < η) (hM : 0 < M) (h : ↑P * ↑κ ≤ M ^ 4) (hκ : η ^ 5 * M ^ 3 / 160000 ≤ ↑κ) : ↑P ≤ 160000 / η ^ 5 * M

theorem TrilinearHT.Auto.SparseCountData.abs_alt_four_le (a b c d : ℝ) : |a - b + c - d| ≤ |a| + |b| + |c| + |d|

theorem TrilinearHT.Auto.SparseCountData.sum_three {i j k : Fin 4} (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) (f : Fin 4 → ℤ) : ∑ r ∈ {i, j, k}, f r = f i + f j + f k

theorem TrilinearHT.Auto.SparseCountData.extract_cover_subset (D : SparseCountData) (O : Finset (ℤ × (Fin 4 → ℤ))) (hO : ∀ o ∈ O, o.1 ∈ D.S ∧ o.2 ∈ D.E o.1) {i j k l : Fin 4} (hi : i ∈ D.core) (hj : j ∈ D.core) (hk : k ∈ D.core) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) (hl : l ∉ {i, j, k}) {Rp : ℝ} (hRp : ∀ o ∈ O, D.R o.1 ≤ Rp) (N ε : ℕ) (hN : 24 * D.B ≤ ↑N) (hε : 4 * D.ν * Rp ≤ ↑ε) {η : ℝ} (hη : 0 < η) (Unc : Finset ℤ) (hUnc : Unc ⊆ D.A i) (hbig : η * ↑D.L * D.M ^ 2 < ↑{o ∈ O | o.2 i ∈ Unc}.card) : ∃ B₀ ⊆ Unc, B₀.Nonempty ∧ η * D.M / 3 ≤ ↑B₀.card ∧ ∃ (P : Finset ℤ), ↑P.card ≤ 160000 / η ^ 5 * D.M ∧ ∀ a ∈ B₀, ∀ b ∈ B₀, ∃ p ∈ P, a - b - p ∈ shiftBox D.ζ N ε 2

Blueprint lines 2618-2626 (one extraction step): if the occurrences with an uncovered i-label have mass greater than η L M², the four-step paths of the (i, j) projection, coloured by the k-label, give a subset B₀ of the uncovered labels with |B₀| ≥ η M / 3 whose difference set is covered by at most 160000 η^{-5} M translates of U(2).

theorem TrilinearHT.Auto.SparseCountData.cover_family (D : SparseCountData) (O : Finset (ℤ × (Fin 4 → ℤ))) (hO : ∀ o ∈ O, o.1 ∈ D.S ∧ o.2 ∈ D.E o.1) {i j k l : Fin 4} (hi : i ∈ D.core) (hj : j ∈ D.core) (hk : k ∈ D.core) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) (hl : l ∉ {i, j, k}) {Rp : ℝ} (hRp : ∀ o ∈ O, D.R o.1 ≤ Rp) (N ε : ℕ) (hN : 24 * D.B ≤ ↑N) (hε : 4 * D.ν * Rp ≤ ↑ε) {η : ℝ} (hη : 0 < η) : ∃ (𝓑 : Finset (Finset ℤ)), (∀ B ∈ 𝓑, B ⊆ D.A i) ∧ (∀ B ∈ 𝓑, ∀ B' ∈ 𝓑, B ≠ B' → Disjoint B B') ∧ (∀ B ∈ 𝓑, η * D.M / 3 ≤ ↑B.card) ∧ (∀ B ∈ 𝓑, ∃ (P : Finset ℤ), ↑P.card ≤ 160000 / η ^ 5 * D.M ∧ ∀ a ∈ B, ∀ b ∈ B, ∃ p ∈ P, a - b - p ∈ shiftBox D.ζ N ε 2) ∧ ↑{o ∈ O | ∀ B ∈ 𝓑, o.2 i ∉ B}.card ≤ η * ↑D.L * D.M ^ 2

Blueprint lines 2618-2626 (iterated extraction): the incident i-labels of a family of occurrences are covered, apart from occurrences of mass at most η L M², by pairwise disjoint subsets B ⊆ A_i, each with |B| ≥ η M / 3 and with a difference cover by at most 160000 η^{-5} M translates of U(2) (eq:two-cover-counts); there are at most 3/η of them.

theorem TrilinearHT.Auto.SparseCountData.cover_family_card (D : SparseCountData) {𝓑 : Finset (Finset ℤ)} {i : Fin 4} (hi : i ∈ D.core) (h1 : ∀ B ∈ 𝓑, B ⊆ D.A i) (h2 : ∀ B ∈ 𝓑, ∀ B' ∈ 𝓑, B ≠ B' → Disjoint B B') {η : ℝ} (hη : 0 < η) (h3 : ∀ B ∈ 𝓑, η * D.M / 3 ≤ ↑B.card) : ↑𝓑.card ≤ 3 / η

Disjoint cover subsets of A_i, each of size at least η M / 3, number at most 3/η.

Three mass ranges and separated middle scales (blueprint lines 2642-2646)

def TrilinearHT.Auto.upperMass {α : Type u_1} (C : Finset (ℤ × α)) (c : ℤ) : ℕ

The mass of scales at least c.

Equations

• TrilinearHT.Auto.upperMass C c = {o ∈ C | c ≤ o.1}.card

theorem TrilinearHT.Auto.upperMass_split {α : Type u_1} (C : Finset (ℤ × α)) (c : ℤ) : upperMass C c = {o ∈ C | o.1 = c}.card + {o ∈ C | c + 1 ≤ o.1}.card

theorem TrilinearHT.Auto.upperMass_above_max {α : Type u_1} (C : Finset (ℤ × α)) {θ : ℝ} (hθ : 0 < θ) (c : ℤ) (hc : ∀ s ∈ Finset.image Prod.fst C, c < s → ↑(upperMass C s) < θ) : ↑{o ∈ C | c + 1 ≤ o.1}.card < θ

Above the largest scale with upper mass at least θ, the upper mass is below θ.

theorem TrilinearHT.Auto.mass_ranges {α : Type u_1} (C : Finset (ℤ × α)) {m₀ : ℝ} (hm : ∀ (s : ℤ), ↑{o ∈ C | o.1 = s}.card ≤ m₀) (hC : 12 * m₀ ≤ ↑C.card) (hCpos : 0 < C.card) : ∃ (c₁ : ℤ), ∃ c₂ < c₁, ↑C.card / 3 ≤ ↑{o ∈ C | c₁ ≤ o.1}.card ∧ ↑C.card / 4 ≤ ↑{o ∈ C | c₂ ≤ o.1 ∧ o.1 < c₁}.card ∧ ↑C.card / 4 ≤ ↑{o ∈ C | o.1 < c₂}.card

Blueprint lines 2642-2643 (three mass ranges): if every scale carries mass at most m₀ and the total mass is at least 12 m₀, there are cuts c₂ < c₁ such that the first range (scales ≥ c₁) has at least a third of the mass and the middle (c₂ ≤ s < c₁) and last (s < c₂) ranges at least a quarter each.

theorem TrilinearHT.Auto.residue_selection (Wm : Finset ℤ) (sF : ℤ) (hWm : ∀ s ∈ Wm, sF < s) {g : ℕ} (hg : 1 ≤ g) : ∃ V ⊆ Wm, (∀ v ∈ V, sF + ↑g ≤ v) ∧ (∀ v ∈ V, ∀ v' ∈ V, v' < v → v' + ↑g ≤ v) ∧ ↑Wm.card ≤ ↑g * ↑V.card + ↑g

Blueprint lines 2645-2646 (separated middle scales): among scales above s_F, those at least g above s_F lying in one residue class modulo g are pairwise at least g apart, and there are at least (|W| - g)/g of them.

theorem TrilinearHT.Auto.SparseCountData.label_fiber_le (D : SparseCountData) (O : Finset (ℤ × (Fin 4 → ℤ))) (hO : ∀ o ∈ O, o.1 ∈ D.S ∧ o.2 ∈ D.E o.1) {r : Fin 4} (hr : r ∈ D.core) (a : ℤ) : ↑{o ∈ O | o.2 r = a}.card ≤ ↑D.L * D.M

A fixed label in one core role has at most L M occurrences.

theorem TrilinearHT.Auto.SparseCountData.proj_fiber_le (D : SparseCountData) (O : Finset (ℤ × (Fin 4 → ℤ))) (hO : ∀ o ∈ O, o.1 ∈ D.S ∧ o.2 ∈ D.E o.1) (e : Fin 3 → Fin 4) (he : Function.Injective e) (heC : ∀ (j : Fin 3), e j ∈ D.core) (f : Fin 3 → ℤ) : {o ∈ O | (fun (j : Fin 3) => o.2 (e j)) = f}.card ≤ D.L

Occurrences with a common projection to three distinct core roles number at most L.

theorem TrilinearHT.Auto.combination_arith {ρ M L K₁ δ g V F P₀ P₁ P₂ b₀ b₁ b₂ : ℝ} (hρ : 0 < ρ) (hM : 0 < M) (hL : 1 ≤ L) (hδ : 0 < δ) (hg : 1 ≤ g) (hK : 0 ≤ K₁) (hb₀ : ρ * M / (3 * L) ≤ b₀) (hb₁ : ρ * M / (3 * L) ≤ b₁) (hb₂ : ρ * M / (3 * L) ≤ b₂) (hP₀ : 0 ≤ P₀) (hP₁ : 0 ≤ P₁) (hP₂ : 0 ≤ P₂) (hP₀K : P₀ ≤ K₁ * M) (hP₁K : P₁ ≤ K₁ * M) (hP₂K : P₂ ≤ K₁ * M) (hV : ρ / (8 * g * δ) ≤ V) (hF : ρ * M ^ 2 / (4 * L) ≤ F) (hcount : V * F ≤ (2 * P₀ / b₀) ^ 2 * b₀ * ((2 * P₁ / b₁) ^ 2 * b₁) * (2 * P₂ / b₂) ^ 3) (hρL : ρ ≤ L) : ρ ^ 10 ≤ 10 ^ 6 * δ * g * K₁ ^ 7 * L ^ 9

Blueprint lines 2696-2698 (the mass bound of one combination): from the slab count |V||F| ≤ (2K₁M/b₀)² b₀ (2K₁M/b₁)² b₁ (2K₁M/b₂)³ with anchor sizes b_j ≥ ρM/(3L), |F| ≥ ρM²/(4L), |V| ≥ ρ/(8gδ) and ρ ≤ L, one gets ρ¹⁰ ≤ 10⁶ δ g K₁⁷ L⁹.

theorem TrilinearHT.Auto.SparseCountData.card_le_mul_card_image_real {β : Type u_1} {γ : Type u_2} [DecidableEq γ] (s : Finset β) (f : β → γ) (c : ℝ) (h : ∀ a ∈ Finset.image f s, ↑{x ∈ s | f x = a}.card ≤ c) : ↑s.card ≤ c * ↑(Finset.image f s).card

theorem TrilinearHT.Auto.SparseCountData.ann_triple (D : SparseCountData) (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) {s : ℤ} (hs : s ∈ D.S) {x : Fin 4 → ℤ} (hx : x ∈ D.E s) : ∃ (n : Fin D.d → ℤ), (∀ (r : Fin D.d), |↑(n r)| ≤ D.B) ∧ D.μ * D.R s ≤ |↑(tripleResidual D.ζ (fun (j : Fin 3) => roleCoeff (e j) l) (fun (j : Fin 3) => x (e j)) n)| ∧ |↑(tripleResidual D.ζ (fun (j : Fin 3) => roleCoeff (e j) l) (fun (j : Fin 3) => x (e j)) n)| ≤ D.ν * D.R s

The annular witnesses of ann for a triple enumerated by an injection e.