Trilinear Hilbert transform: sparse_count_explicit

theorem TrilinearHT.Auto.sparse_count_explicit (d : ℕ) (ζ : Fin d → ℝ) (core : Finset (Fin 4)) : core.card = 3 ∨ core.card = 4 → ∀ (A : Fin 4 → Finset ℝ) (M L : ℝ), 1 ≤ M → 1 ≤ L → (∀ i ∈ core, ↑(A i).card ≤ M) → ∀ (B Sg Q μ ν R₀ : ℝ), 1 ≤ B → 0 < μ → μ ≤ 1 → 1 ≤ ν → 0 < R₀ → ∀ (S : Finset ℤ) (E : ℤ → Finset (Fin 4 → ℝ)), (∀ s ∈ S, ∀ x ∈ E s, (∀ i ∈ core, x i ∈ A i) ∧ ∀ i ∉ core, x i = 0) → (∀ i ∈ core, ∀ j ∈ core, i ≠ j → ∀ s ∈ S, ∀ s' ∈ S, ∀ x ∈ E s, ∀ x' ∈ E s', x i = x' i → x j = x' j → x = x') → (∀ (x : Fin 4 → ℝ), ↑{s ∈ S | x ∈ E s}.card ≤ L) → (core.card = 3 → ∃ (w : ℤ → ℝ), (∀ (s : ℤ), 0 ≤ w s) ∧ ∑ s ∈ S, w s ≤ M ∧ ∀ s ∈ S, ∀ i ∈ core, ∀ (a : ℝ), ↑{x ∈ E s | x i = a}.card ≤ w s) → (∀ i ∈ core, ∀ s ∈ S, ∀ s' ∈ S, ∀ x ∈ E s, ∀ x' ∈ E s', x i ≠ x' i → ∀ (n : Fin d → ℤ), (∀ (k : Fin d), |↑(n k)| ≤ Q) → Sg * max (R₀ * 2 ^ s) (R₀ * 2 ^ s') < |x i - x' i + ∑ k : Fin d, ↑(n k) * ζ k|) → (∀ T ⊆ core, T.card = 3 → ∀ l ∉ T, ∀ s ∈ S, ∀ x ∈ E s, ∃ (n : Fin d → ℤ), (∀ (k : Fin d), |↑(n k)| ≤ B) ∧ μ * (R₀ * 2 ^ s) ≤ |∑ i ∈ T, ↑(roleCoeff i l) * x i + 36 * ∑ k : Fin d, ↑(n k) * ζ k| ∧ |∑ i ∈ T, ↑(roleCoeff i l) * x i + 36 * ∑ k : Fin d, ↑(n k) * ζ k| ≤ ν * (R₀ * 2 ^ s)) → (∀ s ∈ S, (E s).Nonempty → ∀ (n : Fin d → ℤ), (∀ (k : Fin d), |↑(n k)| ≤ Q) → |∑ k : Fin d, ↑(n k) * ζ k| ∉ Set.Icc (μ * (R₀ * 2 ^ s) / 1000) (1000 * ν * (R₀ * 2 ^ s))) → 7200000 * (↑d + 1) ^ 2 * B ≤ Q → 7200000 * (↑d + 1) ^ 2 * ν ≤ Sg → ∀ (δ : ℝ), 0 < δ → δ ≤ 1 → ∑ s ∈ S with ↑(E s).card ≤ δ * M ^ 2, ↑(E s).card ≤ 3 * 10 ^ 11 * (1 + Real.logb 2 (2 + (↑d + 1) ^ 2 * ν / μ)) * L ^ 12 * δ ^ (1 / 300) * M ^ 2

Blueprint lem:sparse-count (lines 2587-2705), eq:sparse-count, with the explicit absolute constants C = 3 · 10^{11}, C_res = 7200000: for real labels A_i (|A_i| ≤ M, M, L ≥ 1), frequencies ζ ∈ ℝ^d, B ≥ 1, 0 < μ ≤ 1 ≤ ν, scales R_s = R₀ 2^s and tuple sets E_s satisfying (1) pair determination with at most L scale occurrences, (2) side incidence, (3) separation, (4) annular witnesses for every triple, and (5) the pure-shift gap, the reserves Q ≥ C_res (d+1)² B, Σ ≥ C_res (d+1)² ν imply, for 0 < δ ≤ 1, Σ_{s : N_s ≤ δ M²} N_s ≤ C ℓ L¹² δ^{1/300} M² with ℓ = 1 + log₂(2 + (d+1)² ν/μ). Tuples are functions on the four roles vanishing off the core roles; a role coefficient is α_i = i - l'.

def TrilinearHT.Auto.ThreeRef {d : ℕ} (ζ : Fin d → ℝ) (l : Fin 4) (B μ ν R : ℝ) (x : Fin 4 → ℝ) : Prop

The reference data of a tested three-core tuple (side role l) at scale R: a box shift m with μ R ≤ |T_l + 36 m·ζ| ≤ ν R, T_l = Σ_{i ≠ l} (i - l) x_i (blueprint lines 2552-2553, the nonzero T_l test).

Equations

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