Trilinear Hilbert transform: sep_one_atom_lattice

theorem TrilinearHT.Auto.sep_one_atom_lattice {d : ℕ} (χ : (Fin d → ℝ) → ℂ) {H : ℝ} (hχ : ∀ (w : Fin d → ℝ), χ w ≠ 0 → ∀ (l : Fin d), |w l| ≤ H) {ψ : ℝ → ℝ} (hψ1 : ∀ (x : ℝ), |x| ≤ 1 → ψ x = 1) (hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0) (C : Matrix (Fin d) (Fin d) ℚ) (θ : Fin d → ℝ) (i a b : ℤ) (x t : ℝ) : have u := fun (j : ℤ) (l : Fin d) => θ l * (x + ↑j * t); have ut := fun (l : Fin d) => θ l * t; have Ki := ⌈H + 1 + |↑(i - a)|⌉₊; have Kb := ⌈2 + |↑(b - a)|⌉₊; ∑' (n : Fin d → ℤ), χ (u i - fun (l : Fin d) => ↑(n l)) * ↑(Real.fourierChar (chartMatrixPhase C (u i) (u i - fun (l : Fin d) => ↑(n l)))) = ∑ ki ∈ slowValueBox d Ki, ∑ kb ∈ slowValueBox d Kb, ∑' (D : (Fin d → ℤ) × (Fin d → ℤ) × (Fin d → ℤ)), sepCoupledAmplitude χ ψ i a b ki kb (u a - fun (l : Fin d) => ↑(D.1 l)) (u b - fun (l : Fin d) => ↑(D.2.1 l)) (ut - fun (l : Fin d) => ↑(D.2.2 l)) * ↑(Real.fourierChar (chartMatrixPhase C (u i) (u i - fun (l : Fin d) => ↑(D.1 l + (i - a) * D.2.2 l + ki l))))

Blueprint lem:separation, lines 1402–1404: the exact lattice identity for one atom. After inserting lattice partitions for the slots a, b and for t, the original index is recovered from its carry k_i, and the equality cutoff fixes the carry k_b; only bounded carries occur.

Fourier expansion of compactly supported smooth functions

A smooth function supported in the cube [-R,R]ⁿ is periodized with period L ≥ 4R and rescaled to unit period. Inside a cutoff equal to one on the cube it is the sum of its absolutely convergent Fourier series. Used in lem:separation, line 1407.

noncomputable def TrilinearHT.Auto.cubePeriodization {n : ℕ} (F : (Fin n → ℝ) → ℂ) (L : ℝ) (x : Fin n → ℝ) : ℂ

The unit-rescaled L-periodization x ↦ Σⱼ F(L(x + j)).

Equations

• TrilinearHT.Auto.cubePeriodization F L x = ∑' (j : Fin n → ℤ), F (L • (x + fun (l : Fin n) => ↑(j l)))

theorem TrilinearHT.Auto.cubePeriodization_periodic {n : ℕ} (F : (Fin n → ℝ) → ℂ) (L : ℝ) (x : Fin n → ℝ) (k : Fin n → ℤ) : cubePeriodization F L (x + fun (l : Fin n) => ↑(k l)) = cubePeriodization F L x

theorem TrilinearHT.Auto.cubePeriodization_local {n : ℕ} (F : (Fin n → ℝ) → ℂ) {R L : ℝ} (hL : 0 < L) (hRL : 4 * R ≤ L) (hsupp : ∀ (w : Fin n → ℝ), F w ≠ 0 → ∀ (l : Fin n), |w l| ≤ R) (x₀ y : Fin n → ℝ) (hy : dist y x₀ < 1 / 4) : cubePeriodization F L y = ∑ j ∈ chartLatticeBox (1 / 2) (-x₀), F (L • (y + fun (l : Fin n) => ↑(j l)))

Locally the periodization is a finite sum.

theorem TrilinearHT.Auto.cubePeriodization_eventuallyEq {n : ℕ} (F : (Fin n → ℝ) → ℂ) {R L : ℝ} (hL : 0 < L) (hRL : 4 * R ≤ L) (hsupp : ∀ (w : Fin n → ℝ), F w ≠ 0 → ∀ (l : Fin n), |w l| ≤ R) (x₀ : Fin n → ℝ) : cubePeriodization F L =ᶠ[nhds x₀] fun (y : Fin n → ℝ) => ∑ j ∈ chartLatticeBox (1 / 2) (-x₀), F (L • (y + fun (l : Fin n) => ↑(j l)))

theorem TrilinearHT.Auto.cubePeriodization_smooth {n : ℕ} {F : (Fin n → ℝ) → ℂ} (hF : ContDiff ℝ (↑⊤) F) {R L : ℝ} (hL : 0 < L) (hRL : 4 * R ≤ L) (hsupp : ∀ (w : Fin n → ℝ), F w ≠ 0 → ∀ (l : Fin n), |w l| ≤ R) : ContDiff ℝ (↑⊤) (cubePeriodization F L)

theorem TrilinearHT.Auto.cubePeriodization_iteratedFDeriv_le {n : ℕ} {F : (Fin n → ℝ) → ℂ} (hF : ContDiff ℝ (↑⊤) F) {R L : ℝ} (hL : 0 < L) (hRL : 4 * R ≤ L) (hsupp : ∀ (w : Fin n → ℝ), F w ≠ 0 → ∀ (l : Fin n), |w l| ≤ R) (m : ℕ) {A : ℝ} (hA : ∀ (w : Fin n → ℝ), ‖iteratedFDeriv ℝ m F w‖ ≤ A) (x₀ : Fin n → ℝ) : ‖iteratedFDeriv ℝ m (cubePeriodization F L) x₀‖ ≤ 4 ^ n * (L ^ m * A)

theorem TrilinearHT.Auto.cubePeriodization_eq {n : ℕ} (F : (Fin n → ℝ) → ℂ) {R L : ℝ} (hR : 0 < R) (hL : 0 < L) (hRL : 4 * R ≤ L) (hsupp : ∀ (w : Fin n → ℝ), F w ≠ 0 → ∀ (l : Fin n), |w l| ≤ R) (w : Fin n → ℝ) (hw : ∀ (l : Fin n), |w l| ≤ 2 * R) : (cubePeriodization F L fun (l : Fin n) => w l / L) = F w

theorem TrilinearHT.Auto.compact_cutoff_fourier_expansion {n m : ℕ} (hn : 1 ≤ n) (hm : n < m) {F : (Fin n → ℝ) → ℂ} (hF : ContDiff ℝ (↑⊤) F) {R L : ℝ} (hR : 0 < R) (hL : 0 < L) (hRL : 4 * R ≤ L) (hsupp : ∀ (w : Fin n → ℝ), F w ≠ 0 → ∀ (l : Fin n), |w l| ≤ R) {Φ : (Fin n → ℝ) → ℂ} (hΦ1 : ∀ (w : Fin n → ℝ), (∀ (l : Fin n), |w l| ≤ R) → Φ w = 1) (hΦ0 : ∀ (w : Fin n → ℝ), Φ w ≠ 0 → ∀ (l : Fin n), |w l| ≤ 2 * R) {A₀ A : ℝ} (hA₀ : ∀ (w : Fin n → ℝ), ‖F w‖ ≤ A₀) (hA : ∀ (w : Fin n → ℝ), ‖iteratedFDeriv ℝ m F w‖ ≤ A) : (∀ (w : Fin n → ℝ), HasSum (fun (p : Fin n → ℤ) => periodicFourierCoeff (cubePeriodization F L) p * (Φ w * ↑(Real.fourierChar (∑ l : Fin n, ↑(p l) * (w l / L))))) (F w)) ∧ (Summable fun (p : Fin n → ℤ) => ‖periodicFourierCoeff (cubePeriodization F L) p‖) ∧ (∀ (p : Fin n → ℤ), p ≠ 0 → ‖periodicFourierCoeff (cubePeriodization F L) p‖ ≤ 4 ^ n * (L ^ m * A) * (√↑n / (2 * Real.pi * frequencyLength p)) ^ m) ∧ ∀ (p : Fin n → ℤ), ‖periodicFourierCoeff (cubePeriodization F L) p‖ ≤ 4 ^ n * A₀

Blueprint lem:separation, line 1407: a smooth function supported in [-R,R]ⁿ equals Σ_p c_p Φ(w) e(p·w/L) inside any cutoff Φ that is one on [-R,R]ⁿ and vanishes outside [-2R,2R]ⁿ, for L ≥ 4R. The coefficients are those of the unit-rescaled periodization, with derivative-controlled decay.

noncomputable def TrilinearHT.Auto.modulatedCutoff {d : ℕ} (ψ : ℝ → ℝ) (r L : ℝ) (p : Fin d → ℤ) (w : Fin d → ℝ) : ℂ

A modulated plateau cutoff w ↦ Φ(w) e(p·w/L), the factor amplitudes of the product-cutoff expansion in lem:separation, line 1407.

Equations

• TrilinearHT.Auto.modulatedCutoff ψ r L p w = TrilinearHT.Auto.tensorCutoff ψ r w * ↑(Real.fourierChar (∑ l : Fin d, ↑(p l) * (w l / L)))

theorem TrilinearHT.Auto.modulatedCutoff_smooth {d : ℕ} {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (r L : ℝ) (p : Fin d → ℤ) : ContDiff ℝ (↑⊤) (modulatedCutoff ψ r L p)

theorem TrilinearHT.Auto.tensorCutoff_hasCompactSupport {d : ℕ} {ψ : ℝ → ℝ} (hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0) {r : ℝ} (hr : 0 < r) : HasCompactSupport (tensorCutoff ψ r)

theorem TrilinearHT.Auto.modulatedCutoff_hasCompactSupport {d : ℕ} {ψ : ℝ → ℝ} (hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0) {r : ℝ} (hr : 0 < r) (L : ℝ) (p : Fin d → ℤ) : HasCompactSupport (modulatedCutoff ψ r L p)

noncomputable def TrilinearHT.Auto.mkQuadraticChart {d : ℕ} (θ : Fin d → ℝ) (lam β : ℝ) (C : Matrix (Fin d) (Fin d) ℚ) (G : (Fin d → ℝ) → ℂ) (hG : ContDiff ℝ (↑⊤) G) (hGc : HasCompactSupport G) : QuadraticChartData d

A one-variable chart with given horizontal vector, phases, rational matrix and smooth compact amplitude.

Equations

• TrilinearHT.Auto.mkQuadraticChart θ lam β C G hG hGc = { horizontal := θ, quadratic := lam, linear := β, matrix := C, amplitude := G, smooth := hG, compact := hGc }

theorem TrilinearHT.Auto.mkQuadraticChart_atom {d : ℕ} (θ : Fin d → ℝ) (lam β : ℝ) (C : Matrix (Fin d) (Fin d) ℚ) (G : (Fin d → ℝ) → ℂ) (hG : ContDiff ℝ (↑⊤) G) (hGc : HasCompactSupport G) (y : ℝ) : quadraticChartAtom (mkQuadraticChart θ lam β C G hG hGc) y = ↑(Real.fourierChar (lam * y ^ 2 + β * y)) * ∑' (n : Fin d → ℤ), G ((fun (l : Fin d) => θ l * y) - fun (l : Fin d) => ↑(n l)) * ↑(Real.fourierChar (chartMatrixPhase C (fun (l : Fin d) => θ l * y) ((fun (l : Fin d) => θ l * y) - fun (l : Fin d) => ↑(n l))))

theorem TrilinearHT.Auto.chartMatrixPhase_scale_matrix {d : ℕ} (C : Matrix (Fin d) (Fin d) ℚ) (q : ℚ) (u w : Fin d → ℝ) : chartMatrixPhase (q • C) u w = ↑q * chartMatrixPhase C u w

theorem TrilinearHT.Auto.chartMatrixPhase_line {d : ℕ} (C : Matrix (Fin d) (Fin d) ℚ) (θ : Fin d → ℝ) (y : ℝ) (v : Fin d → ℝ) : chartMatrixPhase C (fun (l : Fin d) => θ l * y) ((fun (l : Fin d) => θ l * y) - v) = y ^ 2 * chartMatrixPhase C θ θ - y * chartMatrixPhase C θ v

theorem TrilinearHT.Auto.chartMatrixPhase_int_comb {d : ℕ} (C : Matrix (Fin d) (Fin d) ℚ) (θ : Fin d → ℝ) (c₁ c₂ c₃ : ℤ) (v₁ v₂ v₃ : Fin d → ℤ) : (chartMatrixPhase C θ fun (l : Fin d) => ↑(c₁ * v₁ l + c₂ * v₂ l + c₃ * v₃ l)) = ((↑c₁ * chartMatrixPhase C θ fun (l : Fin d) => ↑(v₁ l)) + ↑c₂ * chartMatrixPhase C θ fun (l : Fin d) => ↑(v₂ l)) + ↑c₃ * chartMatrixPhase C θ fun (l : Fin d) => ↑(v₃ l)

theorem TrilinearHT.Auto.separation_phase_split {d : ℕ} (C : Matrix (Fin d) (Fin d) ℚ) (θ : Fin d → ℝ) (lam β : ℝ) (i a b : ℤ) (hab : a ≠ b) (x t : ℝ) (da db dd ki kb : Fin d → ℤ) (hdb : db = fun (l : Fin d) => da l + (b - a) * dd l + kb l) : have αa := (↑i - ↑b) / (↑b - ↑a); have αb := (↑a - ↑i) / (↑b - ↑a); have S := (↑i - ↑a) * (↑i - ↑b); have u := fun (j : ℤ) (l : Fin d) => θ l * (x + ↑j * t); have ut := fun (l : Fin d) => θ l * t; have n := fun (l : Fin d) => da l + (i - a) * dd l + ki l; have Bk := chartMatrixPhase C θ fun (l : Fin d) => ↑(ki l); have Bkb := chartMatrixPhase C θ fun (l : Fin d) => ↑(kb l); lam * (x + ↑i * t) ^ 2 + β * (x + ↑i * t) + chartMatrixPhase C (u i) (u i - fun (l : Fin d) => ↑(n l)) = -↑αa * lam * (x + ↑a * t) ^ 2 + (-↑αa * β + ↑αa * Bk) * (x + ↑a * t) + chartMatrixPhase (-αa • C) (u a) (u a - fun (l : Fin d) => ↑(da l)) + (-↑αb * lam * (x + ↑b * t) ^ 2 + (-↑αb * β + ↑αb * Bk - ↑αb * Bkb) * (x + ↑b * t) + chartMatrixPhase (-αb • C) (u b) (u b - fun (l : Fin d) => ↑(db l))) + (↑S * lam * t ^ 2 + 0 * t + chartMatrixPhase (S • C) ut (ut - fun (l : Fin d) => ↑(dd l)))

Blueprint lem:separation, line 1405: on the constraint d_b = d_a + (b-a)d + k_b, the full phase of the original atom splits exactly into the phases of the three factor charts: matrices -α_a C, -α_b C, S C, quadratic coefficients -α_a λ, -α_b λ, S λ, and linear phases carrying the integer carries.

def TrilinearHT.Auto.tripleVec {d : ℕ} {α : Type u_1} (u v w : Fin d → α) : Fin (d + d + d) → α

Three blocks of coordinates as one vector of length d + d + d.

Equations

• TrilinearHT.Auto.tripleVec u v w = Fin.append (Fin.append u v) w

def TrilinearHT.Auto.tripleFst {d : ℕ} {α : Type u_1} (z : Fin (d + d + d) → α) : Fin d → α

First coordinate block of a vector divided into three equal blocks.

Equations

• TrilinearHT.Auto.tripleFst z l = z (Fin.castAdd d (Fin.castAdd d l))

def TrilinearHT.Auto.tripleSnd {d : ℕ} {α : Type u_1} (z : Fin (d + d + d) → α) : Fin d → α

Middle coordinate block of a vector divided into three equal blocks.

Equations

• TrilinearHT.Auto.tripleSnd z l = z (Fin.castAdd d (Fin.natAdd d l))

def TrilinearHT.Auto.tripleThd {d : ℕ} {α : Type u_1} (z : Fin (d + d + d) → α) : Fin d → α

Last coordinate block of a vector divided into three equal blocks.

Equations

• TrilinearHT.Auto.tripleThd z l = z (Fin.natAdd (d + d) l)

@[simp]

theorem TrilinearHT.Auto.tripleFst_tripleVec {d : ℕ} {α : Type u_1} (u v w : Fin d → α) : tripleFst (tripleVec u v w) = u

@[simp]

theorem TrilinearHT.Auto.tripleSnd_tripleVec {d : ℕ} {α : Type u_1} (u v w : Fin d → α) : tripleSnd (tripleVec u v w) = v

@[simp]

theorem TrilinearHT.Auto.tripleThd_tripleVec {d : ℕ} {α : Type u_1} (u v w : Fin d → α) : tripleThd (tripleVec u v w) = w

theorem TrilinearHT.Auto.sum_tripleVec {d : ℕ} {M : Type u_1} [AddCommMonoid M] (f : Fin (d + d + d) → M) : ∑ l : Fin (d + d + d), f l = ∑ l : Fin d, f (Fin.castAdd d (Fin.castAdd d l)) + ∑ l : Fin d, f (Fin.castAdd d (Fin.natAdd d l)) + ∑ l : Fin d, f (Fin.natAdd (d + d) l)

theorem TrilinearHT.Auto.prod_tripleVec {d : ℕ} {M : Type u_1} [CommMonoid M] (f : Fin (d + d + d) → M) : ∏ l : Fin (d + d + d), f l = ((∏ l : Fin d, f (Fin.castAdd d (Fin.castAdd d l))) * ∏ l : Fin d, f (Fin.castAdd d (Fin.natAdd d l))) * ∏ l : Fin d, f (Fin.natAdd (d + d) l)

theorem TrilinearHT.Auto.modulated_tripleVec {d : ℕ} (ψ : ℝ → ℝ) (r L : ℝ) (p : Fin (d + d + d) → ℤ) (u v w : Fin d → ℝ) : tensorCutoff ψ r (tripleVec u v w) * ↑(Real.fourierChar (∑ l : Fin (d + d + d), ↑(p l) * (tripleVec u v w l / L))) = modulatedCutoff ψ r L (tripleFst p) u * modulatedCutoff ψ r L (tripleSnd p) v * modulatedCutoff ψ r L (tripleThd p) w

A product cutoff with a character factors over the three blocks.

theorem TrilinearHT.Auto.exists_iteratedFDeriv_bound {n : ℕ} {F : (Fin n → ℝ) → ℂ} (hF : ContDiff ℝ (↑⊤) F) (hc : HasCompactSupport F) (m : ℕ) : ∃ (A : ℝ), ∀ (w : Fin n → ℝ), ‖iteratedFDeriv ℝ m F w‖ ≤ A

Compactly supported smooth functions have bounded derivatives of each order.

noncomputable def TrilinearHT.Auto.sepCoupledVec {d : ℕ} (χ : (Fin d → ℝ) → ℂ) (ψ : ℝ → ℝ) (i a b : ℤ) (ki kb : Fin d → ℤ) (v : Fin (d + d + d) → ℝ) : ℂ

The coupled amplitude of lem:separation as a function on ℝ^(d+d+d).

Equations

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

theorem TrilinearHT.Auto.sepPartition_smooth {d : ℕ} : ContDiff ℝ (↑⊤) sepPartition

theorem TrilinearHT.Auto.tripleFst_contDiff {d : ℕ} : ContDiff ℝ (↑⊤) tripleFst

theorem TrilinearHT.Auto.tripleSnd_contDiff {d : ℕ} : ContDiff ℝ (↑⊤) tripleSnd

theorem TrilinearHT.Auto.tripleThd_contDiff {d : ℕ} : ContDiff ℝ (↑⊤) tripleThd

theorem TrilinearHT.Auto.sepCoupledVec_smooth {d : ℕ} {χ : (Fin d → ℝ) → ℂ} (hχ : ContDiff ℝ (↑⊤) χ) {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (i a b : ℤ) (ki kb : Fin d → ℤ) : ContDiff ℝ (↑⊤) (sepCoupledVec χ ψ i a b ki kb)

theorem TrilinearHT.Auto.sepCoupledVec_support {d : ℕ} {χ : (Fin d → ℝ) → ℂ} {ψ : ℝ → ℝ} {i a b : ℤ} {ki kb : Fin d → ℤ} {v : Fin (d + d + d) → ℝ} (hv : sepCoupledVec χ ψ i a b ki kb v ≠ 0) (l : Fin (d + d + d)) : |v l| ≤ 3 / 4

noncomputable def TrilinearHT.Auto.sepCoeff {d : ℕ} (χ : (Fin d → ℝ) → ℂ) (ψ : ℝ → ℝ) (i a b : ℤ) (ki kb : Fin d → ℤ) (p : Fin (d + d + d) → ℤ) : ℂ

The Fourier coefficients of the coupled amplitude (unit-rescaled, period 3).

Equations

• TrilinearHT.Auto.sepCoeff χ ψ i a b ki kb p = TrilinearHT.Auto.periodicFourierCoeff (TrilinearHT.Auto.cubePeriodization (TrilinearHT.Auto.sepCoupledVec χ ψ i a b ki kb) 3) p

noncomputable def TrilinearHT.Auto.sepChartA {d : ℕ} (A : QuadraticChartData d) {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0) (i a b : ℤ) (ki pa : Fin d → ℤ) : QuadraticChartData d

The slot-a factor chart of lem:separation (matrix -α_a C).

Equations

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

noncomputable def TrilinearHT.Auto.sepChartB {d : ℕ} (A : QuadraticChartData d) {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0) (i a b : ℤ) (ki kb pb : Fin d → ℤ) : QuadraticChartData d

The slot-b factor chart of lem:separation (matrix -α_b C).

Equations

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

noncomputable def TrilinearHT.Auto.sepChartT {d : ℕ} (A : QuadraticChartData d) {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0) (i a b : ℤ) (pt : Fin d → ℤ) : QuadraticChartData d

The time factor chart of lem:separation (matrix S C, S = (i-a)(i-b)).

Equations

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

theorem TrilinearHT.Auto.triple_sum_factor {α : Type u_1} {β : Type u_2} {γ : Type u_3} (c : ℂ) (s₁ : Finset α) (s₂ : Finset β) (s₃ : Finset γ) (f : α → ℂ) (g : β → ℂ) (h : γ → ℂ) : ((c * ∑ x ∈ s₁, f x) * ∑ y ∈ s₂, g y) * ∑ z ∈ s₃, h z = ∑ x ∈ s₁, ∑ y ∈ s₂, ∑ z ∈ s₃, c * (f x * g y * h z)

noncomputable def TrilinearHT.Auto.sepFamilyValue {d : ℕ} (A : QuadraticChartData d) (ψ : ℝ → ℝ) (i a b : ℤ) (x t : ℝ) (ki kb : Fin d → ℤ) : ℂ

The contribution of one carry pair (k_i, k_b) to the separated atom.

Equations

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