Trilinear Hilbert transform: splitFourierExpansion

theorem TrilinearHT.Auto.exp_le_ceil_power_budget {x a b : ℝ} (p : ℕ) (hx : 1 ≤ x) (hab : a ≤ b) : Real.exp (a * x ^ p) ≤ Real.exp (↑(⌈b⌉₊ + p) * x ^ (⌈b⌉₊ + p))

A fixed polynomial exponential is bounded by a larger integer budget.

theorem TrilinearHT.Auto.power_le_exp_budget {H x : ℝ} (c p : ℕ) (hH : 0 < H) (hx : 1 ≤ x) (hp : 1 ≤ p) (hlog : Real.log H ≤ x) : H ^ c ≤ Real.exp (↑c * x ^ p)

A logarithmic bound controls every fixed power by an exponential budget.

theorem TrilinearHT.Auto.splitFourierExpansion (c₀ : ℕ) (hc : 1 ≤ c₀) (k : ℕ) (R : ℝ) (hR : 0 ≤ R) : ∃ (D : ℕ), 1 ≤ D ∧ ∃ (DJ : ℕ → ℕ), ∀ {d : ℕ} (H B : ℝ), Real.exp 2 ≤ H → ↑d ≤ Real.log H → 2 ≤ B → ∀ (C Q : Matrix (Fin d) (Fin d) ℚ), (∀ (i j : Fin d), ↑(rationalHeight (C i j)) ≤ H) → Q.IsSymm → (∀ (i j : Fin d), ↑(rationalHeight (Q i j)) ≤ B) → (1 - Q.map fun (q : ℚ) => ↑q).transpose * ((C.map fun (q : ℚ) => ↑q) - (C.map fun (q : ℚ) => ↑q).transpose) * (1 - Q.map fun (q : ℚ) => ↑q) = 0 → have X := 1 + Real.log H + Real.log B; ∃ (ι : Type) (x : Fintype ι) (σ : ι × (Fin (d + d) → ℤ) → Fin d → ℚ), ↑(Fintype.card ι) ≤ Real.exp (↑D * X ^ D) ∧ (∀ (p : ι × (Fin (d + d) → ℤ)) (i : Fin d), ↑(rationalHeight (σ p i)) ≤ Real.exp (↑D * X ^ D) * (1 + frequencyLength p.2)) ∧ ∀ (A : MultivariableQuadraticChartData k d), A.matrix = C → MultivariableQuadraticChartComplexity c₀ H A → ‖realMatrixOperator ((Q.map fun (q : ℚ) => ↑q) * A.horizontal)‖ ≤ B → ∃ (a : ι × (Fin (d + d) → ℤ) → ℂ), (∀ (z : Fin k → ℝ), (∀ (i : Fin k), |z i| ≤ R) → HasSum (fun (p : ι × (Fin (d + d) → ℤ)) => a p * ↑(Real.fourierChar ((fun (i : Fin d) => ↑(σ p i)) ⬝ᵥ A.horizontal.mulVec z))) (↑(Real.fourierChar (-(z ⬝ᵥ (effectiveReturnQuadratic (C.map fun (q : ℚ) => ↑q) A.quadratic A.horizontal ((1 - Q.map fun (q : ℚ) => ↑q) * A.horizontal) ((Q.map fun (q : ℚ) => ↑q) * A.horizontal)).mulVec z + A.linear ⬝ᵥ z))) * multivariableQuadraticChartAtom A z)) ∧ (Summable fun (p : ι × (Fin (d + d) → ℤ)) => ‖a p‖) ∧ ∑' (p : ι × (Fin (d + d) → ℤ)), ‖a p‖ ≤ Real.exp (↑D * X ^ D) ∧ ∀ (J : ℕ), (∀ (p : ι × (Fin (d + d) → ℤ)), ‖a p‖ * (1 + frequencyLength p.2) ^ (J * (d + 1) ^ 2) ≤ Real.exp (↑(DJ J) * X ^ DJ J)) ∧ ∀ (T : ℝ), 1 ≤ T → (∑ f : ι, ∑ v ∈ frequencyShell (d + d) T, ‖a (f, v)‖) * T ^ (J * (d + 1) ^ 2) ≤ Real.exp (↑(DJ J) * X ^ DJ J)

Blueprint lem:chartfourier (Fourier expansion with uniform envelopes), lines 1338–1377. Let Q be a chart of complexity H (fixed Gevrey order c₀) with matrix C, and let a rational symmetric splitting matrix Q_s of height at most B have fast part P_f = 1 - Q_s isotropic for C - Cᵀ and bounded slow velocity ‖P_s V‖ ≤ B. Then on the fixed box [-R,R]^k Q(z) = e(zᵀΛ_* z + bᵀz) Σ_ℓ a_ℓ e(σ_ℓᵀ V z) exactly and absolutely, with Λ_* the effective quadratic form of eq:effective. The families ι are at most exp(D X^D) in number, each indexed by 2d integers; the rational frequencies σ (chosen before the amplitude and the slow velocity) have height at most exp(D X^D)(1+|ℓ|); Σ|a_ℓ| ≤ exp(D X^D); and for every J the pooled envelope satisfies |a_ℓ|(1+|ℓ|)^{J(d+1)²} ≤ exp(D_J X^{D_J}), while the absolute mass in each dyadic shell T ≤ 1+|ℓ| < 2T is at most exp(D_J X^{D_J}) T^{-J(d+1)²}. Here X = 1 + log H + log B, so all bounds are quasipolynomial in H, B.

theorem TrilinearHT.Auto.pooled_shell_tail_bound {ι : Type u_1} [Fintype ι] {n : ℕ} (a : ι × (Fin n → ℤ) → ℂ) {E : ℝ} (hshell : ∀ (T : ℝ), 1 ≤ T → (∑ f : ι, ∑ v ∈ frequencyShell n T, ‖a (f, v)‖) * T ≤ E) (K : ℕ) : (Summable fun (p : ι × (Fin n → ℤ)) => ‖if p.2 ≠ 0 ∧ 2 ^ K ≤ 1 + frequencyLength p.2 then a p else 0‖) ∧ ∑' (p : ι × (Fin n → ℤ)), ‖if p.2 ≠ 0 ∧ 2 ^ K ≤ 1 + frequencyLength p.2 then a p else 0‖ ≤ 2 * E / 2 ^ K

Blueprint lem:chartfourier, line 1347: shell bounds with one power of decay give a pooled tail bound, so a uniform tail ε requires truncation only at frequency 2^K ≥ 2E/ε.

Progression separation (lem:separation)

noncomputable def TrilinearHT.Auto.sepPartition {d : ℕ} (w : Fin d → ℝ) : ℂ

The tensor Gevrey lattice partition used for the slot lifts.

Equations

• TrilinearHT.Auto.sepPartition w = TrilinearHT.Auto.chartCoordinateProduct TrilinearHT.Auto.gevreyPartition w

theorem TrilinearHT.Auto.sepPartition_tsum {d : ℕ} (z : Fin d → ℝ) : ∑' (k : Fin d → ℤ), sepPartition (z - fun (l : Fin d) => ↑(k l)) = 1

theorem TrilinearHT.Auto.sepPartition_ne_zero {d : ℕ} {w : Fin d → ℝ} (hw : sepPartition w ≠ 0) (l : Fin d) : |w l| ≤ 3 / 4

noncomputable def TrilinearHT.Auto.sepCoupledAmplitude {d : ℕ} (χ : (Fin d → ℝ) → ℂ) (ψ : ℝ → ℝ) (i a b : ℤ) (ki kb : Fin d → ℤ) (wa wb w : Fin d → ℝ) : ℂ

The coupled amplitude of lem:separation, lines 1403–1407: the original cutoff at w_a + (i-a)w - k_i, the equality cutoff imposing d_b = d_a + (b-a)d + k_b, and the three lattice partitions.

Equations

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

theorem TrilinearHT.Auto.tensorCutoff_int {d : ℕ} {ψ : ℝ → ℝ} (hψ1 : ∀ (x : ℝ), |x| ≤ 1 → ψ x = 1) (hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0) (v : Fin d → ℤ) : (tensorCutoff ψ (1 / 3) fun (l : Fin d) => ↑(v l)) = if v = 0 then 1 else 0