Trilinear Hilbert transform: progressionSeparation

theorem TrilinearHT.Auto.progressionSeparation (c₀ : ℕ) (hc : 1 ≤ c₀) : ∃ (c₁ : ℕ) (D : ℕ), 1 ≤ c₁ ∧ 1 ≤ D ∧ ∀ {d e : ℕ} (H : ℝ) (A : QuadraticChartData d) (A' : QuadraticChartData e), 1 ≤ d → 1 ≤ e → QuadraticChartComplexity c₀ H A → QuadraticChartComplexity c₀ H A' → ∀ (i k a b : ℤ), a ≠ b → |i| ≤ 3 → |k| ≤ 3 → |a| ≤ 3 → |b| ≤ 3 → have X := 1 + Real.log H; ∃ (τ : Type) (_ : Countable τ) (cf : τ → ℂ) (φa : τ → QuadraticChartData (d + e)) (φb : τ → QuadraticChartData (d + e)) (φt : τ → QuadraticChartData (d + e)) (size : τ → ℝ), (∀ (x t : ℝ), HasSum (fun (q : τ) => cf q * quadraticChartAtom (φa q) (x + ↑a * t) * quadraticChartAtom (φb q) (x + ↑b * t) * quadraticChartAtom (φt q) t) (quadraticChartAtom A (x + ↑i * t) * quadraticChartAtom A' (x + ↑k * t))) ∧ (∀ (q : τ), IsBoundedQuadraticChart (φa q) ∧ IsBoundedQuadraticChart (φb q) ∧ IsBoundedQuadraticChart (φt q)) ∧ (∀ (q : τ), 1 ≤ size q) ∧ (Summable fun (q : τ) => ‖cf q‖) ∧ ∑' (q : τ), ‖cf q‖ ≤ Real.exp (↑D * X ^ D) ∧ (∀ (T : ℝ), 1 ≤ T → (∑' (q : τ), if T ≤ size q then ‖cf q‖ else 0) ≤ Real.exp (↑D * X ^ D) / T ^ 100) ∧ (∀ (q : τ), QuadraticChartComplexity c₁ ((Real.exp (↑D * X ^ D) * size q) ^ 6) (φa q) ∧ QuadraticChartComplexity c₁ ((Real.exp (↑D * X ^ D) * size q) ^ 6) (φb q) ∧ QuadraticChartComplexity c₁ ((Real.exp (↑D * X ^ D) * size q) ^ 6) (φt q)) ∧ (∀ (T : ℝ), 1 ≤ T → ∃ (Qs : Finset τ), (∀ (q : τ), size q ≤ T → q ∈ Qs) ∧ ↑Qs.card ≤ Real.exp (10 * X ^ 2) * (3 * T) ^ (3 * (d + e))) ∧ ∀ (q : τ), (φt q).horizontal = Fin.append A.horizontal A'.horizontal ∧ (φt q).matrix = chartBlockMatrix (((↑i - ↑a) * (↑i - ↑b)) • A.matrix) (((↑k - ↑a) * (↑k - ↑b)) • A'.matrix) ∧ (φt q).quadratic = ↑((↑i - ↑a) * (↑i - ↑b)) * A.quadratic + ↑((↑k - ↑a) * (↑k - ↑b)) * A'.quadratic

Blueprint lem:separation (Declaration separation, line 1413, THT.Chart.progressionSeparation): two atoms in distinct slots i, k have an exact absolutely convergent expansion φ_i(y_i) φ_k(y_k) = Σ c ψ_a(y_a) ψ_b(y_b) Q(t) with bounded factor atoms; the coefficients have total mass and shell tails D T^{-100}, and the factors of a term in shell T have complexity at most (DT)^6 at a fixed Gevrey order, with D quasipolynomial in H. The single-scale form bound, the separated phase and the uniform kernel approximation are separated_form_le, separatedPhase and separatedKernelApprox.