Trilinear Hilbert transform: sep_one_atom_expansion

theorem TrilinearHT.Auto.sep_one_atom_expansion {d : ℕ} (hd : 1 ≤ d) (A : QuadraticChartData d) {H : ℝ} (hχ : ∀ (w : Fin d → ℝ), A.amplitude w ≠ 0 → ∀ (l : Fin d), |w l| ≤ H) {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ1 : ∀ (x : ℝ), |x| ≤ 1 → ψ x = 1) (hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0) (i a b : ℤ) (hab : a ≠ b) (x t : ℝ) : (∀ (ki kb : Fin d → ℤ), HasSum (fun (p : Fin (d + d + d) → ℤ) => sepCoeff A.amplitude ψ i a b ki kb p * quadraticChartAtom (sepChartA A hψ hψ0 i a b ki (tripleFst p)) (x + ↑a * t) * quadraticChartAtom (sepChartB A hψ hψ0 i a b ki kb (tripleSnd p)) (x + ↑b * t) * quadraticChartAtom (sepChartT A hψ hψ0 i a b (tripleThd p)) t) (sepFamilyValue A ψ i a b x t ki kb)) ∧ quadraticChartAtom A (x + ↑i * t) = ∑ ki ∈ slowValueBox d ⌈H + 1 + |↑(i - a)|⌉₊, ∑ kb ∈ slowValueBox d ⌈2 + |↑(b - a)|⌉₊, sepFamilyValue A ψ i a b x t ki kb

Blueprint lem:separation, lines 1402–1407 (first part): the exact separation of one atom in slot i along the other slots a, b and the time variable. The atom is a finite sum over bounded carries of absolutely convergent series of products of three chart atoms with matrices -α_a C, -α_b C, S C.

theorem TrilinearHT.Auto.tensorCutoff_norm_le_one {d : ℕ} {ψ : ℝ → ℝ} (hψ1 : ∀ (x : ℝ), |ψ x| ≤ 1) (r : ℝ) (w : Fin d → ℝ) : ‖tensorCutoff ψ r w‖ ≤ 1

theorem TrilinearHT.Auto.modulatedCutoff_norm_le_one {d : ℕ} {ψ : ℝ → ℝ} (hψ1 : ∀ (x : ℝ), |ψ x| ≤ 1) (r L : ℝ) (p : Fin d → ℤ) (w : Fin d → ℝ) : ‖modulatedCutoff ψ r L p w‖ ≤ 1

theorem TrilinearHT.Auto.modulatedChart_atom_norm_le {d : ℕ} {ψ : ℝ → ℝ} (hψ1 : ∀ (x : ℝ), |ψ x| ≤ 1) (hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0) (θ : Fin d → ℝ) (lam β : ℝ) (C : Matrix (Fin d) (Fin d) ℚ) (p : Fin d → ℤ) (hG : ContDiff ℝ (↑⊤) (modulatedCutoff ψ (3 / 4) 3 p)) (hGc : HasCompactSupport (modulatedCutoff ψ (3 / 4) 3 p)) (y : ℝ) : ‖quadraticChartAtom (mkQuadraticChart θ lam β C (modulatedCutoff ψ (3 / 4) 3 p) hG hGc) y‖ ≤ 6 ^ d

An atom whose amplitude is a modulated plateau cutoff of radius 3/4 is bounded by 6^d, uniformly in the modulation and all phase parameters.

theorem TrilinearHT.Auto.sepCoeff_summable {d : ℕ} (hd : 1 ≤ d) {χ : (Fin d → ℝ) → ℂ} (hχ : ContDiff ℝ (↑⊤) χ) {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ1 : ∀ (x : ℝ), |x| ≤ 1 → ψ x = 1) (hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0) (i a b : ℤ) (ki kb : Fin d → ℤ) : Summable fun (p : Fin (d + d + d) → ℤ) => ‖sepCoeff χ ψ i a b ki kb p‖

The separation coefficients are absolutely summable.

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

One term of the one-atom separation series.

Equations

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

theorem TrilinearHT.Auto.sepTerm_norm_le {d : ℕ} (A : QuadraticChartData d) {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ1' : ∀ (x : ℝ), |ψ x| ≤ 1) (hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0) (i a b : ℤ) (x t : ℝ) (ki kb : Fin d → ℤ) (p : Fin (d + d + d) → ℤ) : ‖sepTerm A hψ hψ0 i a b x t ki kb p‖ ≤ ‖sepCoeff A.amplitude ψ i a b ki kb p‖ * 6 ^ (3 * d)

theorem TrilinearHT.Auto.sep_pair_expansion {d e : ℕ} (hd : 1 ≤ d) (he : 1 ≤ e) (A : QuadraticChartData d) (A' : QuadraticChartData e) {H H' : ℝ} (hχ : ∀ (w : Fin d → ℝ), A.amplitude w ≠ 0 → ∀ (l : Fin d), |w l| ≤ H) (hχ' : ∀ (w : Fin e → ℝ), A'.amplitude w ≠ 0 → ∀ (l : Fin e), |w l| ≤ H') {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ1' : ∀ (x : ℝ), |ψ x| ≤ 1) (hψ1 : ∀ (x : ℝ), |x| ≤ 1 → ψ x = 1) (hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0) (i k a b : ℤ) (hab : a ≠ b) (x t : ℝ) : have Ki := slowValueBox d ⌈H + 1 + |↑(i - a)|⌉₊; have Kb := slowValueBox d ⌈2 + |↑(b - a)|⌉₊; have Ki' := slowValueBox e ⌈H' + 1 + |↑(k - a)|⌉₊; have Kb' := slowValueBox e ⌈2 + |↑(b - a)|⌉₊; HasSum (fun (q : ((↥Ki × ↥Kb) × ↥Ki' × ↥Kb') × (Fin (d + d + d) → ℤ) × (Fin (e + e + e) → ℤ)) => sepTerm A hψ hψ0 i a b x t (↑q.1.1.1) (↑q.1.1.2) q.2.1 * sepTerm A' hψ hψ0 k a b x t (↑q.1.2.1) (↑q.1.2.2) q.2.2) (quadraticChartAtom A (x + ↑i * t) * quadraticChartAtom A' (x + ↑k * t))

Blueprint lem:separation, line 1407: two atoms in distinct slots i, k are separated along the remaining slots a, b and the time variable; their product is an absolutely convergent series of products of separated factor atoms.

theorem TrilinearHT.Auto.scaleChart_bounded {d : ℕ} (A : QuadraticChartData d) {M : ℝ} (hM : 0 < M) (hA : ∀ (y : ℝ), ‖quadraticChartAtom A y‖ ≤ M) : IsBoundedQuadraticChart (scaleQuadraticChartAmplitude (↑M)⁻¹ A)

Normalizing a chart whose atom is bounded by M > 0 to a bounded atom.

noncomputable def TrilinearHT.Auto.sepPairChartA {d e : ℕ} (A : QuadraticChartData d) (A' : QuadraticChartData e) {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0) (i k a b : ℤ) (ki : Fin d → ℤ) (kj : Fin e → ℤ) (p : Fin (d + d + d) → ℤ) (p' : Fin (e + e + e) → ℤ) : QuadraticChartData (d + e)

The bounded slot-a factor of a separated pair.

Equations

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

noncomputable def TrilinearHT.Auto.sepPairChartB {d e : ℕ} (A : QuadraticChartData d) (A' : QuadraticChartData e) {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0) (i k a b : ℤ) (ki kb : Fin d → ℤ) (kj kc : Fin e → ℤ) (p : Fin (d + d + d) → ℤ) (p' : Fin (e + e + e) → ℤ) : QuadraticChartData (d + e)

The bounded slot-b factor of a separated pair.

Equations

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

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

The bounded time factor of a separated pair.

Equations

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

theorem TrilinearHT.Auto.sepChart_atom_bounds {d : ℕ} (A : QuadraticChartData d) {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ1' : ∀ (x : ℝ), |ψ x| ≤ 1) (hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0) (i a b : ℤ) (ki kb pa pb pt : Fin d → ℤ) (y : ℝ) : ‖quadraticChartAtom (sepChartA A hψ hψ0 i a b ki pa) y‖ ≤ 6 ^ d ∧ ‖quadraticChartAtom (sepChartB A hψ hψ0 i a b ki kb pb) y‖ ≤ 6 ^ d ∧ ‖quadraticChartAtom (sepChartT A hψ hψ0 i a b pt) y‖ ≤ 6 ^ d

theorem TrilinearHT.Auto.sepPairCharts_bounded {d e : ℕ} (A : QuadraticChartData d) (A' : QuadraticChartData e) {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ1' : ∀ (x : ℝ), |ψ x| ≤ 1) (hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0) (i k a b : ℤ) (ki kb : Fin d → ℤ) (kj kc : Fin e → ℤ) (p : Fin (d + d + d) → ℤ) (p' : Fin (e + e + e) → ℤ) : IsBoundedQuadraticChart (sepPairChartA A A' hψ hψ0 i k a b ki kj p p') ∧ IsBoundedQuadraticChart (sepPairChartB A A' hψ hψ0 i k a b ki kb kj kc p p') ∧ IsBoundedQuadraticChart (sepPairChartT A A' hψ hψ0 i k a b p p')

The factors of a separated pair are bounded atoms.

theorem TrilinearHT.Auto.sep_pair_expansion_normalized {d e : ℕ} (hd : 1 ≤ d) (he : 1 ≤ e) (A : QuadraticChartData d) (A' : QuadraticChartData e) {H H' : ℝ} (hχ : ∀ (w : Fin d → ℝ), A.amplitude w ≠ 0 → ∀ (l : Fin d), |w l| ≤ H) (hχ' : ∀ (w : Fin e → ℝ), A'.amplitude w ≠ 0 → ∀ (l : Fin e), |w l| ≤ H') {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ1' : ∀ (x : ℝ), |ψ x| ≤ 1) (hψ1 : ∀ (x : ℝ), |x| ≤ 1 → ψ x = 1) (hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0) (i k a b : ℤ) (hab : a ≠ b) (x t : ℝ) : have Ki := slowValueBox d ⌈H + 1 + |↑(i - a)|⌉₊; have Kb := slowValueBox d ⌈2 + |↑(b - a)|⌉₊; have Ki' := slowValueBox e ⌈H' + 1 + |↑(k - a)|⌉₊; have Kb' := slowValueBox e ⌈2 + |↑(b - a)|⌉₊; HasSum (fun (q : ((↥Ki × ↥Kb) × ↥Ki' × ↥Kb') × (Fin (d + d + d) → ℤ) × (Fin (e + e + e) → ℤ)) => sepCoeff A.amplitude ψ i a b (↑q.1.1.1) (↑q.1.1.2) q.2.1 * sepCoeff A'.amplitude ψ k a b (↑q.1.2.1) (↑q.1.2.2) q.2.2 * (↑(6 ^ d) ^ 3 * ↑(6 ^ e) ^ 3) * quadraticChartAtom (sepPairChartA A A' hψ hψ0 i k a b (↑q.1.1.1) (↑q.1.2.1) q.2.1 q.2.2) (x + ↑a * t) * quadraticChartAtom (sepPairChartB A A' hψ hψ0 i k a b (↑q.1.1.1) (↑q.1.1.2) (↑q.1.2.1) (↑q.1.2.2) q.2.1 q.2.2) (x + ↑b * t) * quadraticChartAtom (sepPairChartT A A' hψ hψ0 i k a b q.2.1 q.2.2) t) (quadraticChartAtom A (x + ↑i * t) * quadraticChartAtom A' (x + ↑k * t))

Blueprint lem:separation, eq:separation: the exact expansion φ_i(y_i) φ_k(y_k) = Σ c ψ_a(y_a) ψ_b(y_b) Q(t) with bounded factor atoms.

Quantitative bounds for the separated terms

noncomputable def TrilinearHT.Auto.tripleFstCLM (d : ℕ) : (Fin (d + d + d) → ℝ) →L[ℝ] Fin d → ℝ

The three coordinate blocks of ℝ^(d+d+d) as continuous linear maps.

Equations

• TrilinearHT.Auto.tripleFstCLM d = ContinuousLinearMap.pi fun (l : Fin d) => ContinuousLinearMap.proj (Fin.castAdd d (Fin.castAdd d l))

noncomputable def TrilinearHT.Auto.tripleSndCLM (d : ℕ) : (Fin (d + d + d) → ℝ) →L[ℝ] Fin d → ℝ

Continuous linear projection onto the middle block of three coordinate blocks.

Equations

• TrilinearHT.Auto.tripleSndCLM d = ContinuousLinearMap.pi fun (l : Fin d) => ContinuousLinearMap.proj (Fin.castAdd d (Fin.natAdd d l))

noncomputable def TrilinearHT.Auto.tripleThdCLM (d : ℕ) : (Fin (d + d + d) → ℝ) →L[ℝ] Fin d → ℝ

Continuous linear projection onto the last block of three coordinate blocks.

Equations

• TrilinearHT.Auto.tripleThdCLM d = ContinuousLinearMap.pi fun (l : Fin d) => ContinuousLinearMap.proj (Fin.natAdd (d + d) l)

theorem TrilinearHT.Auto.pi_proj_norm_le {n d : ℕ} (g : Fin d → Fin n) : ‖ContinuousLinearMap.pi fun (l : Fin d) => ContinuousLinearMap.proj (g l)‖ ≤ 1

theorem TrilinearHT.Auto.tripleFstCLM_norm_le (d : ℕ) : ‖tripleFstCLM d‖ ≤ 1

theorem TrilinearHT.Auto.tripleSndCLM_norm_le (d : ℕ) : ‖tripleSndCLM d‖ ≤ 1

theorem TrilinearHT.Auto.tripleThdCLM_norm_le (d : ℕ) : ‖tripleThdCLM d‖ ≤ 1

theorem TrilinearHT.Auto.sepPartition_geomBound {d Kρ : ℕ} (hK : 1 ≤ Kρ) (hder : ∀ (n : ℕ) (x : ℝ), |iteratedDeriv n gevreyPartition x| ≤ (↑Kρ * (↑n + 1)) ^ (Kρ * (n + 1))) (m : ℕ) (w : Fin d → ℝ) : GeomBound sepPartition w 1 (↑d * (↑Kρ * (↑m + 1)) ^ (2 * Kρ)) m

Geometric bounds for the tensor Gevrey lattice partition.

theorem TrilinearHT.Auto.quadraticChartAmplitude_geomBound {d c₀ : ℕ} {H : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) (hc : 1 ≤ c₀) (m : ℕ) (w : Fin d → ℝ) : GeomBound A.amplitude w (H ^ (2 * c₀) * (↑m + 1) ^ c₀) (H ^ (2 * c₀) * (↑m + 1) ^ c₀) m

Geometric bounds for a chart amplitude from its complexity.

theorem TrilinearHT.Auto.sep_affine_norm_le {d : ℕ} (P Q : (Fin (d + d + d) → ℝ) →L[ℝ] Fin d → ℝ) (hP : ‖P‖ ≤ 1) (hQ : ‖Q‖ ≤ 1) (s : ℝ) : ‖P + s • Q‖ ≤ 1 + |s|

theorem TrilinearHT.Auto.sepCoupledVec_geomBound {d c₀ : ℕ} {H : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) (hc : 1 ≤ c₀) {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ1' : ∀ (x : ℝ), |ψ x| ≤ 1) {Kψ : ℕ} (hKψ : 1 ≤ Kψ) (hψd : ∀ (i : ℕ) (x : ℝ), |iteratedDeriv i ψ x| ≤ (↑Kψ * (↑i + 1)) ^ (Kψ * (i + 1))) {Kρ : ℕ} (hKρ : 1 ≤ Kρ) (hρd : ∀ (n : ℕ) (x : ℝ), |iteratedDeriv n gevreyPartition x| ≤ (↑Kρ * (↑n + 1)) ^ (Kρ * (n + 1))) (i a b : ℤ) (ki kb : Fin d → ℤ) (m : ℕ) (v : Fin (d + d + d) → ℝ) : GeomBound (sepCoupledVec A.amplitude ψ i a b ki kb) v (H ^ (2 * c₀) * (↑m + 1) ^ c₀) ((1 + |↑(i - a)|) * (H ^ (2 * c₀) * (↑m + 1) ^ c₀) + (1 + (1 + |↑(b - a)|)) * (↑d * ((↑Kψ * (↑m + 1)) ^ (2 * Kψ) / (1 / 3))) + 3 * (↑d * (↑Kρ * (↑m + 1)) ^ (2 * Kρ))) m

lem:separation, line 1407: explicit geometric derivative bounds of the coupled amplitude, from the chart complexity, the plateau and the partition Gevrey bounds.

noncomputable def TrilinearHT.Auto.sepDerivBudget (d c₀ Kψ Kρ : ℕ) (H : ℝ) (i a b : ℤ) (m : ℕ) : ℝ

The derivative budget ‖Dᵐ F‖ ≤ K Rᵐ of the coupled amplitude (lem:separation).

Equations

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

theorem TrilinearHT.Auto.sepDerivBudget_nonneg {d c₀ Kψ Kρ : ℕ} {H : ℝ} (hH : 0 ≤ H) (i a b : ℤ) (m : ℕ) : 0 ≤ sepDerivBudget d c₀ Kψ Kρ H i a b m

theorem TrilinearHT.Auto.sepCoeff_shell_bounds {d c₀ : ℕ} (hd : 1 ≤ d) {H : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) (hc : 1 ≤ c₀) {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ1' : ∀ (x : ℝ), |ψ x| ≤ 1) (hψ1 : ∀ (x : ℝ), |x| ≤ 1 → ψ x = 1) (hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0) {Kψ : ℕ} (hKψ : 1 ≤ Kψ) (hψd : ∀ (i : ℕ) (x : ℝ), |iteratedDeriv i ψ x| ≤ (↑Kψ * (↑i + 1)) ^ (Kψ * (i + 1))) {Kρ : ℕ} (hKρ : 1 ≤ Kρ) (hρd : ∀ (n : ℕ) (x : ℝ), |iteratedDeriv n gevreyPartition x| ≤ (↑Kρ * (↑n + 1)) ^ (Kρ * (n + 1))) (i a b : ℤ) (ki kb : Fin d → ℤ) : have Am := fun (m : ℕ) => 4 ^ (d + d + d) * (3 ^ m * sepDerivBudget d c₀ Kψ Kρ H i a b m); (Summable fun (p : Fin (d + d + d) → ℤ) => ‖sepCoeff A.amplitude ψ i a b ki kb p‖) ∧ (∀ (q : ℕ) (T : ℝ), 1 ≤ T → (∑ p ∈ frequencyShell (d + d + d) T, ‖sepCoeff A.amplitude ψ i a b ki kb p‖) * T ^ q ≤ 7 ^ (d + d + d) * Am (q + (d + d + d) + 1) * √↑(d + d + d) ^ (q + (d + d + d) + 1)) ∧ ∑' (p : Fin (d + d + d) → ℤ), ‖sepCoeff A.amplitude ψ i a b ki kb p‖ ≤ Am 0 + 2 * (7 ^ (d + d + d) * Am (d + d + d + 1) * √↑(d + d + d) ^ (d + d + d + 1))

lem:separation, line 1407: coefficient envelope and shell masses of the separation coefficients, with the integration-by-parts order exceeding the Fourier dimension 3d by q + 1.

theorem TrilinearHT.Auto.sepDerivBudget_le_pow {d c₀ Kψ Kρ m : ℕ} {H W : ℝ} {i a b : ℤ} (hW : 3 ≤ W) (hH1 : 1 ≤ H) (hHW : H ≤ W) (hKψW : ↑Kψ ≤ W) (hKρW : ↑Kρ ≤ W) (hmW : ↑m + 1 ≤ W) (hdW : ↑d ≤ W) (hia : 1 + |↑(i - a)| ≤ W) (hba : 1 + (1 + |↑(b - a)|) ≤ W) : PowLe W (3 * c₀ + (3 * c₀ + 4 * Kψ + 4 * Kρ + 5) * m) (sepDerivBudget d c₀ Kψ Kρ H i a b m)

The coupled-amplitude derivative budget is a power of any common bound W of its parameters, with exponent linear in the order.

theorem TrilinearHT.Auto.pow_le_exp_mul_sq {W X c₁ c₂ : ℝ} {e : ℕ} (hW : 1 ≤ W) (hlog : Real.log W ≤ c₂ * X) (he : ↑e ≤ c₁ * X) : W ^ e ≤ Real.exp (c₁ * c₂ * X ^ 2)

theorem TrilinearHT.Auto.sepCoeff_budget (c₀ Kψ Kρ q S : ℕ) : ∃ (D : ℕ), 2 ≤ D ∧ ∀ {d : ℕ} {H : ℝ} {i a b : ℤ}, 1 ≤ d → Real.exp 2 ≤ H → ↑d ≤ Real.log H → |↑(i - a)| ≤ ↑S → |↑(b - a)| ≤ ↑S → have Am := fun (m : ℕ) => 4 ^ (d + d + d) * (3 ^ m * sepDerivBudget d c₀ Kψ Kρ H i a b m); 7 ^ (d + d + d) * Am (q + (d + d + d) + 1) * √↑(d + d + d) ^ (q + (d + d + d) + 1) ≤ Real.exp (↑D * (1 + Real.log H) ^ D) ∧ Am 0 + 2 * (7 ^ (d + d + d) * Am (d + d + d + 1) * √↑(d + d + d) ^ (d + d + d + 1)) ≤ Real.exp (↑D * (1 + Real.log H) ^ D)

lem:separation, line 1407: the shell masses of the separation coefficients are at most exp(D X^D) T^{-q} and their total mass at most exp(D X^D), where X = 1 + log H and D depends only on the fixed Gevrey orders, q and the slot gaps.

theorem TrilinearHT.Auto.abs_rat_le_rationalHeight (q : ℚ) : |↑q| ≤ ↑(rationalHeight q)

theorem TrilinearHT.Auto.rationalHeight_mul_le (q r : ℚ) : ↑(rationalHeight (q * r)) ≤ 2 * (↑(rationalHeight q) * ↑(rationalHeight r)) ^ 2

Heights of products of rationals.

theorem TrilinearHT.Auto.norm_iteratedFDeriv_affine_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Λ : E →L[ℝ] ℝ) (c : ℝ) (x : E) {i : ℕ} (hi : 1 ≤ i) : ‖iteratedFDeriv ℝ i (fun (y : E) => Λ y + c) x‖ ≤ ‖Λ‖ ^ i

Higher derivatives of a real affine function are bounded by powers of its linear part.

theorem TrilinearHT.Auto.GeomBound.fourierChar_affine {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Λ : E →L[ℝ] ℝ) (c : ℝ) (x : E) (m : ℕ) : GeomBound (fun (y : E) => ↑(Real.fourierChar (Λ y + c))) x 1 ((↑m + 1) * (2 * Real.pi) * ‖Λ‖) m

The Fourier character of an affine phase.

noncomputable def TrilinearHT.Auto.modulationFunctional {d : ℕ} (L : ℝ) (p : Fin d → ℤ) : (Fin d → ℝ) →L[ℝ] ℝ

The linear modulation phase w ↦ Σ_l p_l w_l / L as a continuous linear functional.

Equations

• TrilinearHT.Auto.modulationFunctional L p = ∑ l : Fin d, (↑(p l) / L) • ContinuousLinearMap.proj l

theorem TrilinearHT.Auto.modulationFunctional_apply {d : ℕ} (L : ℝ) (p : Fin d → ℤ) (w : Fin d → ℝ) : (modulationFunctional L p) w = ∑ l : Fin d, ↑(p l) * (w l / L)

theorem TrilinearHT.Auto.modulationFunctional_norm_le {d : ℕ} {L : ℝ} (hL : 0 < L) (p : Fin d → ℤ) : ‖modulationFunctional L p‖ ≤ ∑ l : Fin d, |↑(p l)| / L

theorem TrilinearHT.Auto.modulatedCutoff_geomBound {d : ℕ} {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ1' : ∀ (x : ℝ), |ψ x| ≤ 1) {Kψ : ℕ} (hK : 1 ≤ Kψ) (hder : ∀ (i : ℕ) (x : ℝ), |iteratedDeriv i ψ x| ≤ (↑Kψ * (↑i + 1)) ^ (Kψ * (i + 1))) {r : ℝ} (hr : 0 < r) (L : ℝ) (p : Fin d → ℤ) (m : ℕ) (w : Fin d → ℝ) : GeomBound (modulatedCutoff ψ r L p) w 1 (↑d * ((↑Kψ * (↑m + 1)) ^ (2 * Kψ) / r) + (↑m + 1) * (2 * Real.pi) * ‖modulationFunctional L p‖) m

Geometric derivative bounds for a modulated plateau cutoff.

theorem TrilinearHT.Auto.norm_coordinateWordDerivative_le {d m : ℕ} (χ : (Fin d → ℝ) → ℂ) (word : Fin m → Fin d) (z : Fin d → ℝ) : ‖coordinateWordDerivative m χ word z‖ ≤ ‖iteratedFDeriv ℝ m χ z‖

theorem TrilinearHT.Auto.modulatedChart_complexity {d : ℕ} {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ1' : ∀ (x : ℝ), |ψ x| ≤ 1) (hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0) {Kψ : ℕ} (hK : 1 ≤ Kψ) (hder : ∀ (i : ℕ) (x : ℝ), |iteratedDeriv i ψ x| ≤ (↑Kψ * (↑i + 1)) ^ (Kψ * (i + 1))) {r L : ℝ} (hr : 0 < r) (hL : 0 < L) (p : Fin d → ℤ) (θ : Fin d → ℝ) (lam β : ℝ) (M : Matrix (Fin d) (Fin d) ℚ) (hG : ContDiff ℝ (↑⊤) (modulatedCutoff ψ r L p)) (hGc : HasCompactSupport (modulatedCutoff ψ r L p)) {W : ℝ} (hW : Real.exp 2 ≤ W) (hdW : ↑d ≤ Real.log W) (hMW : ∀ (i j : Fin d), ↑(chartRationalHeight (M i j)) ≤ W) (hrW : 2 * r ≤ W) (hBW : ↑d * ↑Kψ ^ (2 * Kψ) / r + 2 * Real.pi * ∑ l : Fin d, |↑(p l)| / L ≤ W) : QuadraticChartComplexity (2 * Kψ) W (mkQuadraticChart θ lam β M (modulatedCutoff ψ r L p) hG hGc)

lem:separation, line 1407: complexity of a modulated-cutoff chart at Gevrey order 2Kψ. The parameter W must dominate the dimension, matrix heights, support and the first-order derivative scale.

theorem TrilinearHT.Auto.quadraticChartComplexity_order_mono {d c₀ c₁ : ℕ} {H : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) (hc : c₀ ≤ c₁) : QuadraticChartComplexity c₁ H A

theorem TrilinearHT.Auto.exists_unit_chart : ∃ (c : ℕ) (W₀ : ℝ) (E : QuadraticChartData 1), 1 ≤ c ∧ Real.exp 2 ≤ W₀ ∧ (∀ (y : ℝ), quadraticChartAtom E y = 1) ∧ ∀ (W : ℝ), W₀ ≤ W → QuadraticChartComplexity c W E

A one-dimensional chart whose atom is identically one, at a fixed Gevrey order.

theorem TrilinearHT.Auto.exists_pad_chart : ∃ (c : ℕ) (W₀ : ℝ), 1 ≤ c ∧ Real.exp 2 ≤ W₀ ∧ ∀ {d c₀ : ℕ} {H : ℝ} (A : QuadraticChartData d), QuadraticChartComplexity c₀ H A → 1 ≤ c₀ → ∃ (A' : QuadraticChartData (d + 1)), (∀ (y : ℝ), quadraticChartAtom A' y = quadraticChartAtom A y) ∧ QuadraticChartComplexity (max c₀ c) (max H W₀ ^ 6) A' ∧ (IsBoundedQuadraticChart A → IsBoundedQuadraticChart A')

Padding a chart to positive dimension without changing its atom.

noncomputable def TrilinearHT.Auto.sepFactorConst (Kψ : ℕ) : ℝ

The fixed constant in the factor-chart complexity bound of lem:separation.

Equations

• TrilinearHT.Auto.sepFactorConst Kψ = 2 * ↑Kψ ^ (2 * Kψ) + 3

theorem TrilinearHT.Auto.sepFactor_complexity {d c₀ : ℕ} {H : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ1' : ∀ (x : ℝ), |ψ x| ≤ 1) (hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0) {Kψ : ℕ} (hK : 1 ≤ Kψ) (hder : ∀ (i : ℕ) (x : ℝ), |iteratedDeriv i ψ x| ≤ (↑Kψ * (↑i + 1)) ^ (Kψ * (i + 1))) (q : ℚ) {Q : ℝ} (hQ1 : 1 ≤ Q) (hq : ↑(rationalHeight q) ≤ Q) (p : Fin d → ℤ) (θ : Fin d → ℝ) (lam β : ℝ) (hG : ContDiff ℝ (↑⊤) (modulatedCutoff ψ (3 / 4) 3 p)) (hGc : HasCompactSupport (modulatedCutoff ψ (3 / 4) 3 p)) {W : ℝ} (hW : sepFactorConst Kψ * Q ^ 2 * H ^ 2 * (1 + ∑ l : Fin d, |↑(p l)|) ≤ W) : QuadraticChartComplexity (2 * Kψ) W (mkQuadraticChart θ lam β (q • A.matrix) (modulatedCutoff ψ (3 / 4) 3 p) hG hGc)

lem:separation, line 1407: a factor chart ψ_p with matrix q C has complexity at most W at Gevrey order 2Kψ whenever W ≥ K Q² H² (1 + Σ_l |p_l|), where Q bounds the height of the fixed rational q.

noncomputable def TrilinearHT.Auto.sepQ (i a b : ℤ) : ℝ

A bound for the heights of the fixed separation rationals α_a, α_b, S.

Equations

• TrilinearHT.Auto.sepQ i a b = 1 + |↑(i - b)| + |↑(a - i)| + |↑(b - a)| + |↑((i - a) * (i - b))|

theorem TrilinearHT.Auto.one_le_sepQ (i a b : ℤ) : 1 ≤ sepQ i a b

theorem TrilinearHT.Auto.rationalHeight_int_div_le_sepQ {u v : ℤ} {Q : ℝ} (hQ : 1 + |↑u| + |↑v| ≤ Q) : ↑(rationalHeight (-(↑u / ↑v))) ≤ Q

theorem TrilinearHT.Auto.sep_heights_le (i a b : ℤ) : ↑(rationalHeight (-((↑i - ↑b) / (↑b - ↑a)))) ≤ sepQ i a b ∧ ↑(rationalHeight (-((↑a - ↑i) / (↑b - ↑a)))) ≤ sepQ i a b ∧ ↑(rationalHeight ((↑i - ↑a) * (↑i - ↑b))) ≤ sepQ i a b

theorem TrilinearHT.Auto.sum_abs_triple_le {d : ℕ} (p : Fin (d + d + d) → ℤ) : ∑ l : Fin d, |↑(tripleFst p l)| ≤ ∑ l : Fin (d + d + d), |↑(p l)| ∧ ∑ l : Fin d, |↑(tripleSnd p l)| ≤ ∑ l : Fin (d + d + d), |↑(p l)| ∧ ∑ l : Fin d, |↑(tripleThd p l)| ≤ ∑ l : Fin (d + d + d), |↑(p l)|

theorem TrilinearHT.Auto.sepCharts_complexity {d c₀ : ℕ} {H : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ1' : ∀ (x : ℝ), |ψ x| ≤ 1) (hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0) {Kψ : ℕ} (hK : 1 ≤ Kψ) (hder : ∀ (i : ℕ) (x : ℝ), |iteratedDeriv i ψ x| ≤ (↑Kψ * (↑i + 1)) ^ (Kψ * (i + 1))) (i a b : ℤ) (ki kb : Fin d → ℤ) (p : Fin (d + d + d) → ℤ) {W : ℝ} (hW : sepFactorConst Kψ * sepQ i a b ^ 2 * H ^ 2 * (1 + ∑ l : Fin (d + d + d), |↑(p l)|) ≤ W) : QuadraticChartComplexity (2 * Kψ) W (sepChartA A hψ hψ0 i a b ki (tripleFst p)) ∧ QuadraticChartComplexity (2 * Kψ) W (sepChartB A hψ hψ0 i a b ki kb (tripleSnd p)) ∧ QuadraticChartComplexity (2 * Kψ) W (sepChartT A hψ hψ0 i a b (tripleThd p))

lem:separation, line 1407: complexity of the three factor charts of one separated atom.

theorem TrilinearHT.Auto.sepPairCharts_complexity {d e c₀ c₀' : ℕ} {H : ℝ} {A : QuadraticChartData d} {A' : QuadraticChartData e} (hA : QuadraticChartComplexity c₀ H A) (hA' : QuadraticChartComplexity c₀' H A') {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ1' : ∀ (x : ℝ), |ψ x| ≤ 1) (hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0) {Kψ : ℕ} (hK : 1 ≤ Kψ) (hder : ∀ (i : ℕ) (x : ℝ), |iteratedDeriv i ψ x| ≤ (↑Kψ * (↑i + 1)) ^ (Kψ * (i + 1))) (i k a b : ℤ) (ki kb : Fin d → ℤ) (kj kc : Fin e → ℤ) (p : Fin (d + d + d) → ℤ) (p' : Fin (e + e + e) → ℤ) {W : ℝ} (hW : sepFactorConst Kψ * max (sepQ i a b) (sepQ k a b) ^ 2 * H ^ 2 * (1 + ∑ l : Fin (d + d + d), |↑(p l)| + ∑ l : Fin (e + e + e), |↑(p' l)|) ≤ W) : QuadraticChartComplexity (2 * Kψ) (W ^ 6) (sepPairChartA A A' hψ hψ0 i k a b ki kj p p') ∧ QuadraticChartComplexity (2 * Kψ) (W ^ 6) (sepPairChartB A A' hψ hψ0 i k a b ki kb kj kc p p') ∧ QuadraticChartComplexity (2 * Kψ) (W ^ 6) (sepPairChartT A A' hψ hψ0 i k a b p p')

lem:separation, line 1407: the normalized bounded factors of a separated pair have complexity at most W⁶ at the fixed Gevrey order 2Kψ, where W ≥ K Q² H² (1 + Σ|p_l| + Σ|p'_l|).

Separated forms: the kernel expansion and the Fourier supremum bound

theorem TrilinearHT.Auto.iteratedDeriv_comp_affine {φ : ℝ → ℂ} (hφ : ContDiff ℝ (↑⊤) φ) (m : ℕ) (L c t : ℝ) : iteratedDeriv m (fun (s : ℝ) => φ (L * s + c)) t = L ^ m • iteratedDeriv m φ (L * t + c)

theorem TrilinearHT.Auto.contDiff_insertNth_line {d : ℕ} (i : Fin (d + 1)) (y : Fin d → ℝ) : ContDiff ℝ ↑⊤ fun (s : ℝ) => i.insertNth s y

theorem TrilinearHT.Auto.cubePeriodization_line_le {d : ℕ} {F : (Fin (d + 1) → ℝ) → ℂ} (hF : ContDiff ℝ (↑⊤) F) {R L : ℝ} (hL : 0 < L) (hRL : 4 * R ≤ L) (hsupp : ∀ (w : Fin (d + 1) → ℝ), F w ≠ 0 → ∀ (l : Fin (d + 1)), |w l| ≤ R) (m : ℕ) {A : ℝ} (hA : ∀ (i : Fin (d + 1)) (x : Fin d → ℝ) (t : ℝ), ‖iteratedDeriv m (fun (s : ℝ) => F (i.insertNth s x)) t‖ ≤ A) (i : Fin (d + 1)) (x : Fin d → ℝ) (t : ℝ) : ‖iteratedDeriv m (fun (s : ℝ) => cubePeriodization F L (i.insertNth s x)) t‖ ≤ 4 ^ (d + 1) * (L ^ m * A)

Coordinate-line derivatives of a cube periodization.

noncomputable def TrilinearHT.Auto.kernelUnitRescale (a₀ r : ℝ) (w : ℝ × ℝ → ℂ) (u : Fin 2 → ℝ) : ℂ

The admissible kernel at unit scale, centred at the cell midpoint.

Equations

• TrilinearHT.Auto.kernelUnitRescale a₀ r w u = w (a₀ + r / 2 + r * u 0, r * u 1)

noncomputable def TrilinearHT.Auto.kernelDerivBound (κ : LocalKernelClass) (m : ℕ) : ℝ

The derivative constant of the admissible kernel class at order m.

Equations

• TrilinearHT.Auto.kernelDerivBound κ m = (κ.derivativeConstant * (↑m + 2)) ^ (κ.derivativeConstant * (↑m + 2))

theorem TrilinearHT.Auto.kernelDerivBound_nonneg (κ : LocalKernelClass) (m : ℕ) : 0 ≤ kernelDerivBound κ m

noncomputable def TrilinearHT.Auto.kernelFourierConst (κ : LocalKernelClass) : ℝ

The uniform absolute Fourier mass of admissible kernels.

Equations

• TrilinearHT.Auto.kernelFourierConst κ = 4 ^ 2 * (16 ^ 0 * TrilinearHT.Auto.kernelDerivBound κ 0) + 2 * (7 ^ 2 * (4 ^ 2 * (16 ^ 3 * TrilinearHT.Auto.kernelDerivBound κ 3)) * √↑2 ^ 3)

theorem TrilinearHT.Auto.kernelUnitRescale_support {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {u : Fin 2 → ℝ} (hu : kernelUnitRescale a₀ r w u ≠ 0) (l : Fin 2) : |u l| ≤ 4

theorem TrilinearHT.Auto.kernelUnitRescale_line_le {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) (m : ℕ) (i : Fin 2) (x : Fin 1 → ℝ) (t : ℝ) : ‖iteratedDeriv m (fun (s : ℝ) => kernelUnitRescale a₀ r w (i.insertNth s x)) t‖ ≤ kernelDerivBound κ m

theorem TrilinearHT.Auto.admissibleKernel_fourier_expansion {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) : have c := periodicFourierCoeff (cubePeriodization (kernelUnitRescale a₀ r w) 16); (Summable fun (v : Fin 2 → ℤ) => ‖c v‖) ∧ ∑' (v : Fin 2 → ℤ), ‖c v‖ ≤ kernelFourierConst κ ∧ ∀ (x t : ℝ), |x - (a₀ + r / 2)| ≤ 8 * r → |t| ≤ 8 * r → HasSum (fun (v : Fin 2 → ℤ) => c v * ↑(Real.fourierChar (↑(v 0) * ((x - (a₀ + r / 2)) / r / 16) + ↑(v 1) * (t / r / 16)))) (w (x, t))

lem:separation, line 1409: an admissible kernel has an absolutely convergent two-variable Fourier expansion near its cell, with absolute coefficient mass bounded uniformly over the kernel class. Only pure x- and t-derivatives enter.

theorem TrilinearHT.Auto.integrable_correlation_norm {A B : ℝ → ℂ} (hA : MeasureTheory.Integrable A MeasureTheory.volume) (hB : MeasureTheory.Integrable B MeasureTheory.volume) : MeasureTheory.Integrable (fun (s : ℝ) => ∫ (y : ℝ), ‖A y‖ * ‖B (y + s)‖) MeasureTheory.volume

theorem TrilinearHT.Auto.integral_progression_section {A B : ℝ → ℂ} (a b t : ℝ) : ∫ (x : ℝ), A (x + a * t) * B (x + b * t) = ∫ (y : ℝ), A y * B (y + (b - a) * t)

theorem TrilinearHT.Auto.integrable_progression_pair {A B : ℝ → ℂ} (hAm : Measurable A) (hBm : Measurable B) (hA1 : MeasureTheory.Integrable A MeasureTheory.volume) (hA2 : MeasureTheory.MemLp A 2 MeasureTheory.volume) (hB1 : MeasureTheory.Integrable B MeasureTheory.volume) (hB2 : MeasureTheory.MemLp B 2 MeasureTheory.volume) {a b : ℝ} (hab : a ≠ b) : MeasureTheory.Integrable (fun (z : ℝ × ℝ) => A (z.1 + a * z.2) * B (z.1 + b * z.2)) MeasureTheory.volume

Integrability of a pair of L¹ ∩ L² inputs along two distinct progression slots.

theorem TrilinearHT.Auto.integral_progression_pair_eq {A B K : ℝ → ℂ} (hAm : Measurable A) (hBm : Measurable B) (hA1 : MeasureTheory.Integrable A MeasureTheory.volume) (hA2 : MeasureTheory.MemLp A 2 MeasureTheory.volume) (hB1 : MeasureTheory.Integrable B MeasureTheory.volume) (hB2 : MeasureTheory.MemLp B 2 MeasureTheory.volume) (hKm : Measurable K) (hK1 : ∀ (t : ℝ), ‖K t‖ ≤ 1) {a b : ℝ} (hab : a ≠ b) : ∫ (z : ℝ × ℝ), A (z.1 + a * z.2) * B (z.1 + b * z.2) * K z.2 = ∫ (s : ℝ), ↑|b - a|⁻¹ * K (s / (b - a)) * ∫ (u : ℝ), A u * B (u + s)

Fubini and the change of variables to a correlation along two progression slots.

theorem TrilinearHT.Auto.separated_term_bound {A B : ℝ → ℂ} (hAm : Measurable A) (hBm : Measurable B) (hA1 : MeasureTheory.Integrable A MeasureTheory.volume) (hA2 : MeasureTheory.MemLp A 2 MeasureTheory.volume) (hB1 : MeasureTheory.Integrable B MeasureTheory.volume) (hB2 : MeasureTheory.MemLp B 2 MeasureTheory.volume) {a₀ r : ℝ} (hr : 0 < r) (hAs : ∀ (y : ℝ), A y ≠ 0 → y ∈ Set.Icc a₀ (a₀ + r)) (hBs : ∀ (y : ℝ), B y ≠ 0 → y ∈ Set.Icc a₀ (a₀ + r)) {a b : ℝ} (hab1 : 1 ≤ |b - a|) {Q : ℝ → ℂ} (hQm : Measurable Q) (hQ1 : ∀ (t : ℝ), ‖Q t‖ ≤ 1) {ζ : ℝ → ℝ} (hζi : MeasureTheory.Integrable ζ MeasureTheory.volume) (hζ1 : ∀ (u : ℝ), |u| ≤ 1 → ζ u = 1) {M : ℝ} (hM : ∀ (ξ : ℝ), ‖∫ (u : ℝ), Q (r * u) * ↑(ζ u) * ↑(Real.fourierChar (-(ξ * u)))‖ ≤ M) (γ : ℝ) : ‖∫ (z : ℝ × ℝ), A (z.1 + a * z.2) * B (z.1 + b * z.2) * (↑(Real.fourierChar (γ * z.2)) * Q z.2)‖ ≤ r * M * √(∫ (x : ℝ), ‖A x‖ ^ 2) * √(∫ (x : ℝ), ‖B x‖ ^ 2)

lem:separation, line 1409: one modulated separated term is bounded by r A_r times the L² norms of its two inputs supported in the cell.

theorem TrilinearHT.Auto.separated_form_le {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) (a b : Fin 4) (hab : a ≠ b) {Q : ℝ → ℂ} (hQm : Measurable Q) (hQ1 : ∀ (t : ℝ), ‖Q t‖ ≤ 1) {ζ : ℝ → ℝ} (hζi : MeasureTheory.Integrable ζ MeasureTheory.volume) (hζ1 : ∀ (u : ℝ), |u| ≤ 1 → ζ u = 1) {M : ℝ} (hM : ∀ (ξ : ℝ), ‖∫ (u : ℝ), Q (r * u) * ↑(ζ u) * ↑(Real.fourierChar (-(ξ * u)))‖ ≤ M) {Fa Fb : ℝ → ℂ} (hFam : Measurable Fa) (hFbm : Measurable Fb) (hFa2 : MeasureTheory.MemLp Fa 2 (MeasureTheory.volume.restrict (Set.Icc a₀ (a₀ + r)))) (hFb2 : MeasureTheory.MemLp Fb 2 (MeasureTheory.volume.restrict (Set.Icc a₀ (a₀ + r)))) : ‖(↑r)⁻¹ ^ 2 * ∫ (z : ℝ × ℝ), w z * Q z.2 * Fa (realProgressionCoordinate a z) * Fb (realProgressionCoordinate b z)‖ ≤ kernelFourierConst κ * M * √(r⁻¹ * ∫ (x : ℝ) in Set.Icc a₀ (a₀ + r), ‖Fa x‖ ^ 2) * √(r⁻¹ * ∫ (x : ℝ) in Set.Icc a₀ (a₀ + r), ‖Fb x‖ ^ 2)

lem:separation, line 1409: the separated single-scale form r⁻² ∫ w Q(t) F_a(y_a) F_b(y_b) in two distinct slots is bounded by C A_r times the normalized L²(I) norms, where A_r ≤ M bounds sup_ξ |∫ Q(ru) ζ(u) e(-ξu) du| and C depends only on the kernel class.

The separated phase (lem:separation, line 1411)

theorem TrilinearHT.Auto.inner_single_realMatrixOperator {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (i j : Fin n) : inner ℝ (EuclideanSpace.single i 1) ((realMatrixOperator A) (EuclideanSpace.single j 1)) = A i j

theorem TrilinearHT.Auto.isSymm_of_realMatrixOperator_starProjection {n : ℕ} {Q : Matrix (Fin n) (Fin n) ℚ} {U : Submodule ℝ (EuclideanSpace ℝ (Fin n))} [U.HasOrthogonalProjection] (h : realMatrixOperator (Q.map fun (q : ℚ) => ↑q) = U.starProjection) : Q.IsSymm

A rational matrix acting as an orthogonal projection is symmetric.

theorem TrilinearHT.Auto.inner_eq_sum_euclidean {n : ℕ} (x y : EuclideanSpace ℝ (Fin n)) : inner ℝ x y = ∑ k : Fin n, x.ofLp k * y.ofLp k

theorem TrilinearHT.Auto.one_sub_map_cast {n : ℕ} (Q : Matrix (Fin n) (Fin n) ℚ) : ((1 - Q).map fun (q : ℚ) => ↑q) = 1 - Q.map fun (q : ℚ) => ↑q

theorem TrilinearHT.Auto.isotropy_matrix_of_starProjection {n : ℕ} {Q : Matrix (Fin n) (Fin n) ℚ} {M : Matrix (Fin n) (Fin n) ℝ} {U : Submodule ℝ (EuclideanSpace ℝ (Fin n))} [U.HasOrthogonalProjection] (hP : realMatrixOperator ((1 - Q).map fun (q : ℚ) => ↑q) = U.starProjection) (hiso : ∀ x ∈ U, ∀ y ∈ U, inner ℝ y ((realMatrixOperator M) x) = 0) : (1 - Q.map fun (q : ℚ) => ↑q).transpose * M * (1 - Q.map fun (q : ℚ) => ↑q) = 0

The isotropy of the fast subspace as a matrix identity.

noncomputable def TrilinearHT.Auto.oneVariableChart {d : ℕ} (A : QuadraticChartData d) : MultivariableQuadraticChartData 1 d

A one-variable chart regarded as a chart in one real variable.

Equations

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

theorem TrilinearHT.Auto.oneVariableChart_atom {d : ℕ} (A : QuadraticChartData d) (z : Fin 1 → ℝ) : multivariableQuadraticChartAtom (oneVariableChart A) z = quadraticChartAtom A (z 0)

theorem TrilinearHT.Auto.oneVariableChart_complexity {d c₀ : ℕ} {H : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) : MultivariableQuadraticChartComplexity c₀ H (oneVariableChart A)

theorem TrilinearHT.Auto.fourier_euclidean_one (g : ℝ → ℂ) (ξ : EuclideanSpace ℝ (Fin 1)) : FourierTransform.fourier (fun (z : EuclideanSpace ℝ (Fin 1)) => g (z.ofLp 0)) ξ = ∫ (u : ℝ), ↑(Real.fourierChar (-(u * ξ.ofLp 0))) * g u

The Fourier transform on ℝ¹ of a function of the single coordinate.

theorem TrilinearHT.Auto.quadForm_entry {d : ℕ} (V : Matrix (Fin d) (Fin 1) ℝ) (M : Matrix (Fin d) (Fin d) ℝ) : (V.transpose * M * V) 0 0 = ∑ i : Fin d, ∑ j : Fin d, V i 0 * M i j * V j 0

theorem TrilinearHT.Auto.effectiveReturnQuadratic_one {d : ℕ} (C : Matrix (Fin d) (Fin d) ℝ) (Λ : Matrix (Fin 1) (Fin 1) ℝ) (V : Matrix (Fin d) (Fin 1) ℝ) (Qr : Matrix (Fin d) (Fin d) ℝ) : effectiveReturnQuadratic C Λ V ((1 - Qr) * V) (Qr * V) 0 0 = Λ 0 0 + ∑ i : Fin d, ∑ j : Fin d, V i 0 * ((1 / 2) • realSymmetricPart C + (1 - Qr).transpose * realSkewPart C * Qr) i j * V j 0

In one real variable the effective quadratic of lem:weyl is a single quadratic form.

theorem TrilinearHT.Auto.abs_rat_le_of_height {q : ℚ} {B : ℝ} (h : ↑(rationalHeight q) ≤ B) : |↑q| ≤ B

theorem TrilinearHT.Auto.separatedPhaseMatrix_height {d : ℕ} {H B : ℝ} (hH : 1 ≤ H) (hB : 1 ≤ B) (C Q : Matrix (Fin d) (Fin d) ℚ) (hC : ∀ (i j : Fin d), ↑(rationalHeight (C i j)) ≤ H) (hQ : ∀ (i j : Fin d), ↑(rationalHeight (Q i j)) ≤ B) (i j : Fin d) : ↑(rationalHeight (separatedPhaseMatrix C Q i j)) ≤ 4 * H ^ d ^ 2 * (B ^ d ^ 2) ^ 2 * (H + ↑d ^ 2 * ((1 + B) * H * B) + 1)

Height of the separated phase matrix: quasipolynomial in the heights of C and Q.

theorem TrilinearHT.Auto.separatedPhase (c₀ : ℕ) (hc : 1 ≤ c₀) (R : ℝ) (hR : 0 ≤ R) : ∃ (D : ℕ), 1 ≤ D ∧ ∃ (DJ : ℕ → ℕ), ∀ {d : ℕ} (H δ r : ℝ) (A : QuadraticChartData d), QuadraticChartComplexity c₀ H A → 0 < r → ∀ (ζ : ℝ → ℂ), Measurable ζ → (∀ (u : ℝ), ‖ζ u‖ ≤ H) → (∀ (u v : ℝ), ‖ζ v - ζ u‖ ≤ H * |v - u|) → (∀ (u : ℝ), ζ u ≠ 0 → |u| ≤ R) → 0 < δ → (∀ s < δ, ∃ (ξ : ℝ), s < ‖∫ (u : ℝ), ↑(Real.fourierChar (-(u * ξ))) * (ζ u * quadraticChartAtom A (r * u))‖) → have X := 1 + Real.log H + Real.log (max 1 δ⁻¹); ∃ (M : Matrix (Fin d) (Fin d) ℚ), (∀ (i j : Fin d), ↑(rationalHeight (M i j)) ≤ Real.exp (↑D * X ^ D)) ∧ |A.quadratic + ∑ i : Fin d, ∑ j : Fin d, A.horizontal i * ↑(M i j) * A.horizontal j| * r ^ 2 ≤ Real.exp (↑D * X ^ D) ∧ ∃ (ι : 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 : ι × (Fin (d + d) → ℤ) → ℂ), (∀ (t : ℝ), |t| ≤ R * r → HasSum (fun (p : ι × (Fin (d + d) → ℤ)) => a p * ↑(Real.fourierChar ((∑ i : Fin d, ↑(σ p i) * A.horizontal i) * t))) (↑(Real.fourierChar (-((A.quadratic + ∑ i : Fin d, ∑ j : Fin d, A.horizontal i * ↑(M i j) * A.horizontal j) * t ^ 2 + A.linear * t))) * quadraticChartAtom A t)) ∧ (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:separation, eq:separated-phase (line 1411): if the Fourier supremum A_r of a time chart is at least δ, then on the scale-r window Q(t) = e(λ_* t² + β t) Σ a_ℓ e(σ_ℓ·θ t) exactly and absolutely, with λ_* = λ + θᵀ M θ for a rational matrix M of bounded height, |λ_*| r² ≤ D, and rational frequencies σ_ℓ of height ≤ D(1+|ℓ|) and the shell bounds of lem:chartfourier; everything is quasipolynomial in H and δ⁻¹.

Uniform separated approximation of the kernel (lem:separation, line 1411)

theorem TrilinearHT.Auto.unitSquare_fourier_expansion {F : (Fin 2 → ℝ) → ℂ} (hF : ContDiff ℝ (↑⊤) F) (hsupp : ∀ (u : Fin 2 → ℝ), F u ≠ 0 → ∀ (l : Fin 2), |u l| ≤ 4) {A : ℕ → ℝ} (hA : ∀ (m : ℕ) (i : Fin 2) (x : Fin 1 → ℝ) (t : ℝ), ‖iteratedDeriv m (fun (s : ℝ) => F (i.insertNth s x)) t‖ ≤ A m) : have c := periodicFourierCoeff (cubePeriodization F 16); (Summable fun (v : Fin 2 → ℤ) => ‖c v‖) ∧ (∀ (m : ℕ), 2 < m → ∀ (v : Fin 2 → ℤ), v ≠ 0 → ‖c v‖ ≤ 4 ^ 2 * (16 ^ m * A m) * (√↑2 / (2 * Real.pi * frequencyLength v)) ^ m) ∧ (∀ (v : Fin 2 → ℤ), ‖c v‖ ≤ 4 ^ 2 * (16 ^ 0 * A 0)) ∧ ∀ (u : Fin 2 → ℝ), (∀ (l : Fin 2), |u l| ≤ 8) → HasSum (fun (v : Fin 2 → ℤ) => c v * ↑(Real.fourierChar (↑(v 0) * (u 0 / 16) + ↑(v 1) * (u 1 / 16)))) (F u)

A smooth function on ℝ² supported in [-4,4]² with coordinate-line derivative bounds has an absolutely convergent Fourier expansion on [-8,8]² with explicit coefficient decay.

noncomputable def TrilinearHT.Auto.chirpedKernelRescale (a₀ r Λ : ℝ) (w : ℝ × ℝ → ℂ) (u : Fin 2 → ℝ) : ℂ

The admissible kernel times the chirp e(Λ u₁²), at unit scale.

Equations

• TrilinearHT.Auto.chirpedKernelRescale a₀ r Λ w u = TrilinearHT.Auto.kernelUnitRescale a₀ r w u * ↑(Real.fourierChar (Λ * u 1 ^ 2))

noncomputable def TrilinearHT.Auto.kernelDerivSum (κ : LocalKernelClass) (m : ℕ) : ℝ

Cumulative derivative constant of the kernel class up to order m.

Equations

• TrilinearHT.Auto.kernelDerivSum κ m = ∑ i ∈ Finset.range (m + 1), TrilinearHT.Auto.kernelDerivBound κ i

theorem TrilinearHT.Auto.kernelDerivBound_le_sum (κ : LocalKernelClass) {i m : ℕ} (hi : i ≤ m) : kernelDerivBound κ i ≤ kernelDerivSum κ m

noncomputable def TrilinearHT.Auto.chirpLineBound (κ : LocalKernelClass) (Λ : ℝ) (m : ℕ) : ℝ

The coordinate-line derivative constant of the chirped kernel.

Equations

• TrilinearHT.Auto.chirpLineBound κ Λ m = TrilinearHT.Auto.kernelDerivSum κ m * (1 + (↑m + 1) * (2 * Real.pi) * (max (|Λ| * 25) 1 * 2)) ^ m

theorem TrilinearHT.Auto.chirpLineBound_nonneg (κ : LocalKernelClass) (Λ : ℝ) (m : ℕ) : 0 ≤ chirpLineBound κ Λ m

theorem TrilinearHT.Auto.chirpedKernelRescale_support {κ : LocalKernelClass} {a₀ r Λ : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {u : Fin 2 → ℝ} (hu : chirpedKernelRescale a₀ r Λ w u ≠ 0) (l : Fin 2) : |u l| ≤ 4

theorem TrilinearHT.Auto.chirpedKernelRescale_smooth {κ : LocalKernelClass} {a₀ r : ℝ} {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) (Λ : ℝ) : ContDiff ℝ (↑⊤) (chirpedKernelRescale a₀ r Λ w)

theorem TrilinearHT.Auto.chirpedKernelRescale_line_le {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) (Λ : ℝ) (m : ℕ) (i : Fin 2) (x : Fin 1 → ℝ) (t : ℝ) : ‖iteratedDeriv m (fun (s : ℝ) => chirpedKernelRescale a₀ r Λ w (i.insertNth s x)) t‖ ≤ chirpLineBound κ Λ m

theorem TrilinearHT.Auto.norm_tsum_sub_sum_le {β : Type u_1} {f : β → ℂ} (hf : Summable fun (x : β) => ‖f x‖) (s : Finset β) {g : β → ℝ} (hg : Summable g) (hg0 : ∀ (x : β), 0 ≤ g x) (hfg : ∀ x ∉ s, ‖f x‖ ≤ g x) : ‖∑' (x : β), f x - ∑ x ∈ s, f x‖ ≤ ∑' (x : β), g x

theorem TrilinearHT.Auto.not_mem_frequencyBox {n N : ℕ} {v : Fin n → ℤ} (hv : v ∉ frequencyBox n N) : v ≠ 0 ∧ ↑N ≤ 1 + frequencyLength v

noncomputable def TrilinearHT.Auto.chirpTailConst (κ : LocalKernelClass) (Λ : ℝ) : ℝ

The constant of the chirped kernel's Fourier tail at order three.

Equations

• TrilinearHT.Auto.chirpTailConst κ Λ = 7 ^ 2 * (4 ^ 2 * (16 ^ 3 * TrilinearHT.Auto.chirpLineBound κ Λ 3)) * √↑2 ^ 3 * 2

theorem TrilinearHT.Auto.kernel_product_approx {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) (Λ : ℝ) {n : ℕ} {ι : Type u_1} [Fintype ι] (Q : ℝ → ℂ) (γ : ι × (Fin n → ℤ) → ℝ) (a : ι × (Fin n → ℤ) → ℂ) (ha : Summable fun (p : ι × (Fin n → ℤ)) => ‖a p‖) (hQ : ∀ (t : ℝ), |t| ≤ r → HasSum (fun (p : ι × (Fin n → ℤ)) => a p * ↑(Real.fourierChar (γ p * t))) (↑(Real.fourierChar (-(Λ * (t / r) ^ 2))) * Q t)) {E : ℝ} (hshell : ∀ (T : ℝ), 1 ≤ T → (∑ f : ι, ∑ v ∈ frequencyShell n T, ‖a (f, v)‖) * T ≤ E) {sa sb : ℝ} (hab : 1 ≤ |sb - sa|) (hsa : |sa| ≤ 3) (K₁ K₂ : ℕ) (ya yb : ℝ) (hya : ya ∈ Set.Icc a₀ (a₀ + r)) (hyb : yb ∈ Set.Icc a₀ (a₀ + r)) : have cW := periodicFourierCoeff (cubePeriodization (chirpedKernelRescale a₀ r Λ w) 16); have t := (yb - ya) / (sb - sa); have x := ya - sa * t; ‖w (x, t) * Q t - ∑ p ∈ Finset.univ ×ˢ frequencyBox n (2 ^ K₁), ∑ v ∈ frequencyBox 2 (2 ^ K₂), a p * cW v * ↑(Real.fourierChar (↑(v 0) * ((x - (a₀ + r / 2)) / r / 16) + ↑(v 1) * (t / r / 16) + γ p * t))‖ ≤ localKernelSupBound κ * (2 * E / 2 ^ K₁) + (∑' (p : ι × (Fin n → ℤ)), ‖a p‖) * (chirpTailConst κ Λ / 2 ^ K₂)

lem:separation, line 1411 (core): with a time-chart expansion e(-Λ(t/r)²) Q(t) = Σ a_p e(γ_p t) on the window and the chirped kernel expansion, the kernel w(x,t) Q(t) on I × I is approximated by a finite double sum of pure linear phases in (x,t), with explicit truncation errors.

theorem TrilinearHT.Auto.chirpLineBound_le (κ : LocalKernelClass) (Λ : ℝ) (m : ℕ) : chirpLineBound κ Λ m ≤ kernelDerivSum κ m * (1300 * (↑m + 1) * (1 + |Λ|)) ^ m

noncomputable def TrilinearHT.Auto.chirpTailClassConst (κ : LocalKernelClass) : ℝ

The fixed constant of the chirped kernel tail (depends only on the kernel class).

Equations

• TrilinearHT.Auto.chirpTailClassConst κ = 2 * (7 ^ 2 * (4 ^ 2 * (16 ^ 3 * (TrilinearHT.Auto.kernelDerivSum κ 3 * (1300 * 4) ^ 3))) * 3)

noncomputable def TrilinearHT.Auto.chirpClassConst (κ : LocalKernelClass) : ℝ

The fixed constant of the chirped kernel bounds (depends only on the kernel class).

Equations

• TrilinearHT.Auto.chirpClassConst κ = TrilinearHT.Auto.chirpTailClassConst κ + 4 ^ 2 * TrilinearHT.Auto.kernelDerivSum κ 0 + 1

theorem TrilinearHT.Auto.chirpTailClassConst_nonneg (κ : LocalKernelClass) : 0 ≤ chirpTailClassConst κ

theorem TrilinearHT.Auto.chirpClassConst_pos (κ : LocalKernelClass) : 1 ≤ chirpClassConst κ

theorem TrilinearHT.Auto.sqrt_two_cube_le : √↑2 ^ 3 ≤ 3

theorem TrilinearHT.Auto.chirpTailConst_le (κ : LocalKernelClass) (Λ : ℝ) : chirpTailConst κ Λ ≤ chirpTailClassConst κ * (1 + |Λ|) ^ 3

theorem TrilinearHT.Auto.chirpedKernel_coeff_mass {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) (Λ : ℝ) : have cW := periodicFourierCoeff (cubePeriodization (chirpedKernelRescale a₀ r Λ w) 16); (Summable fun (v : Fin 2 → ℤ) => ‖cW v‖) ∧ ∑' (v : Fin 2 → ℤ), ‖cW v‖ ≤ chirpClassConst κ * (1 + |Λ|) ^ 3

Total Fourier mass of the chirped kernel.

theorem TrilinearHT.Auto.exists_two_pow_between {Y : ℝ} (hY : 1 ≤ Y) : ∃ (K : ℕ), Y ≤ 2 ^ K ∧ 2 ^ K ≤ 2 * Y

theorem TrilinearHT.Auto.trunc_error_le {s E ε : ℝ} {K : ℕ} (hε : 0 < ε) (hY : 4 * s * E / ε + 1 ≤ 2 ^ K) : s * (2 * E / 2 ^ K) ≤ ε / 2

theorem TrilinearHT.Auto.trunc_error_le' {s T T' ε : ℝ} {K : ℕ} (hs : 0 ≤ s) (hT : T ≤ T') (hε : 0 < ε) (hY : 2 * s * T' / ε + 1 ≤ 2 ^ K) : s * (T / 2 ^ K) ≤ ε / 2

theorem TrilinearHT.Auto.qp_power_bound {W X : ℝ} {k cW e : ℕ} (hW1 : 1 ≤ W) (hlogW : Real.log W ≤ ↑cW * X ^ e) (hX1 : 1 ≤ X) (hk : ↑k ≤ 11 * X) : W ^ k ≤ Real.exp (↑(11 * cW + e + 1) * X ^ (11 * cW + e + 1))

theorem TrilinearHT.Auto.approx_budget_K₁ {s0 EJ ε E1 Cκ : ℝ} {K : ℕ} (hs0 : 0 ≤ s0) (hEJ1 : 1 ≤ EJ) (hε : 0 < ε) (hε' : 1 ≤ ε⁻¹) (hE11 : 1 ≤ E1) (hC : 5 * (4 * s0 + 1) ≤ Cκ) (hK : 2 ^ K ≤ 2 * (4 * s0 * EJ / ε + 1)) : 2 * 2 ^ K + 1 ≤ Cκ * E1 * EJ * ε⁻¹

theorem TrilinearHT.Auto.approx_budget_K₂ {A Ct L ε E1 EJ Cκ : ℝ} {K : ℕ} (hA : A ≤ E1) (hCt : 0 ≤ Ct) (hL1 : 1 ≤ L) (hL : L ≤ 2 * E1) (hε : 0 < ε) (hε' : 1 ≤ ε⁻¹) (hE11 : 1 ≤ E1) (hEJ1 : 1 ≤ EJ) (hC : 5 * (16 * Ct + 1) ≤ Cκ) (hK : 2 ^ K ≤ 2 * (2 * A * (Ct * L ^ 3) / ε + 1)) : 2 * 2 ^ K + 1 ≤ (Cκ * E1 * EJ * ε⁻¹) ^ 4

theorem TrilinearHT.Auto.approx_budget_mass {Cc L E1 EJ ε Cκ : ℝ} (hCc : 0 ≤ Cc) (hL1 : 1 ≤ L) (hL : L ≤ 2 * E1) (hε' : 1 ≤ ε⁻¹) (hE11 : 1 ≤ E1) (hEJ1 : 1 ≤ EJ) (hC : 8 * Cc ≤ Cκ) (hCκ1 : 1 ≤ Cκ) : E1 * (Cc * L ^ 3) ≤ (Cκ * E1 * EJ * ε⁻¹) ^ 4

theorem TrilinearHT.Auto.phase_split_sum {α' : Type u_1} {β' : Type u_2} (S : Finset α') (V : Finset β') (f : α' → β' → ℂ) (φ c α β : α' → β' → ℝ) (ya yb : ℝ) (h : ∀ (p : α') (v : β'), φ p v = c p v + α p v * ya + β p v * yb) : ∑ p ∈ S, ∑ v ∈ V, f p v * ↑(Real.fourierChar (φ p v)) = ∑ ν : ↥S × ↥V, f ↑ν.1 ↑ν.2 * ↑(Real.fourierChar (c ↑ν.1 ↑ν.2)) * ↑(Real.fourierChar (α ↑ν.1 ↑ν.2 * ya)) * ↑(Real.fourierChar (β ↑ν.1 ↑ν.2 * yb))

theorem TrilinearHT.Auto.separatedKernelApprox (c₀ : ℕ) (hc : 1 ≤ c₀) (R : ℝ) (hR : 1 ≤ R) (κ : LocalKernelClass) : ∃ (D : ℕ), 1 ≤ D ∧ ∀ {d : ℕ} (H δ ε r a₀ : ℝ) (A : QuadraticChartData d), QuadraticChartComplexity c₀ H A → 0 < r → ∀ (w : ℝ × ℝ → ℂ), IsAdmissibleLocalKernel κ a₀ r w → ∀ (ζ : ℝ → ℂ), Measurable ζ → (∀ (u : ℝ), ‖ζ u‖ ≤ H) → (∀ (u v : ℝ), ‖ζ v - ζ u‖ ≤ H * |v - u|) → (∀ (u : ℝ), ζ u ≠ 0 → |u| ≤ R) → 0 < δ → 0 < ε → ε ≤ 1 → (∀ s < δ, ∃ (ξ : ℝ), s < ‖∫ (u : ℝ), ↑(Real.fourierChar (-(u * ξ))) * (ζ u * quadraticChartAtom A (r * u))‖) → ∀ (sa sb : ℝ), 1 ≤ |sb - sa| → |sa| ≤ 3 → have X := 1 + Real.log H + Real.log (max 1 δ⁻¹) + Real.log ε⁻¹; ∃ (ι' : Type) (x : Fintype ι') (c : ι' → ℂ) (α : ι' → ℝ) (β : ι' → ℝ), ↑(Fintype.card ι') ≤ Real.exp (↑D * X ^ D) ∧ ∑ ν : ι', ‖c ν‖ ≤ Real.exp (↑D * X ^ D) ∧ ∀ (ya yb : ℝ), ya ∈ Set.Icc a₀ (a₀ + r) → yb ∈ Set.Icc a₀ (a₀ + r) → ‖w (ya - sa * ((yb - ya) / (sb - sa)), (yb - ya) / (sb - sa)) * quadraticChartAtom A ((yb - ya) / (sb - sa)) - ∑ ν : ι', c ν * ↑(Real.fourierChar (α ν * ya)) * ↑(Real.fourierChar (β ν * yb))‖ ≤ ε

Blueprint lem:separation, line 1411: if A_r ≥ δ, the two-variable kernel w(x,t) Q(t) on I × I (with t = (y_b - y_a)/(b - a), x = y_a - a t) has a uniform ε-approximation by a finite sum Σ c_ν e(α_ν y_a) e(β_ν y_b) of products of bounded atoms (pure linear phases), with number of terms and absolute coefficient norm quasipolynomial in H, δ⁻¹, ε⁻¹.

Packaging lem:separation: coefficient tails of the separated pair

theorem TrilinearHT.Auto.pooled_shell_tail_bound_pow {ι : Type u_1} [Fintype ι] {n q : ℕ} (hq : 1 ≤ q) (a : ι × (Fin n → ℤ) → ℂ) {E : ℝ} (hshell : ∀ (T : ℝ), 1 ≤ T → (∑ f : ι, ∑ v ∈ frequencyShell n T, ‖a (f, v)‖) * T ^ q ≤ 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) ^ q

Shell bounds with decay T^{-q} give the pooled tail 2E/2^{Kq} past 2^K.

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

Tail mass past an arbitrary level T ≥ 1 from shell bounds of decay T^{-q}.

theorem TrilinearHT.Auto.product_family_tail {α : Type u_1} {β : Type u_2} (f : α → ℂ) (g : β → ℂ) (hf : Summable fun (x : α) => ‖f x‖) (hg : Summable fun (y : β) => ‖g y‖) (sf : α → ℝ) (sg : β → ℝ) (T : ℝ) (htf : Summable fun (x : α) => if T ≤ sf x then ‖f x‖ else 0) (htg : Summable fun (y : β) => if T ≤ sg y then ‖g y‖ else 0) : (Summable fun (z : α × β) => ‖f z.1 * g z.2‖) ∧ ∑' (z : α × β), ‖f z.1 * g z.2‖ = (∑' (x : α), ‖f x‖) * ∑' (y : β), ‖g y‖ ∧ (∑' (z : α × β), if T ≤ max (sf z.1) (sg z.2) then ‖f z.1 * g z.2‖ else 0) ≤ (∑' (x : α), if T ≤ sf x then ‖f x‖ else 0) * ∑' (y : β), ‖g y‖ + (∑' (x : α), ‖f x‖) * ∑' (y : β), if T ≤ sg y then ‖g y‖ else 0

Mass and tail of a product of two coefficient families.

theorem TrilinearHT.Auto.summable_prod_fintype_nonneg {ι : Type u_1} {β : Type u_2} [Fintype ι] {u : ι × β → ℝ} (hu0 : ∀ (z : ι × β), 0 ≤ u z) (hu : ∀ (i : ι), Summable fun (b : β) => u (i, b)) : Summable u ∧ ∑' (z : ι × β), u z = ∑ i : ι, ∑' (b : β), u (i, b)

theorem TrilinearHT.Auto.atom_family_budget {H E c : ℝ} {d Db : ℕ} (hH : Real.exp 2 ≤ H) (hdH : ↑d ≤ Real.log H) (hE0 : 0 ≤ E) (hE : E ≤ Real.exp (↑Db * (1 + Real.log H) ^ Db)) (hc0 : 0 ≤ c) (hc : c ≤ (95 * H) ^ d) : (2 ^ 100 + 2 ^ 101) * (c * (6 ^ d) ^ 3 * E) ≤ Real.exp (↑(114 + Db) * (1 + Real.log H) ^ (Db + 2))

theorem TrilinearHT.Auto.sepAtomFamily_bounds (c₀ : ℕ) (hc : 1 ≤ c₀) {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ1' : ∀ (x : ℝ), |ψ x| ≤ 1) (hψ1 : ∀ (x : ℝ), |x| ≤ 1 → ψ x = 1) (hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0) {Kψ : ℕ} (hKψ : 1 ≤ Kψ) (hψd : ∀ (i : ℕ) (x : ℝ), |iteratedDeriv i ψ x| ≤ (↑Kψ * (↑i + 1)) ^ (Kψ * (i + 1))) {Kρ : ℕ} (hKρ : 1 ≤ Kρ) (hρd : ∀ (n : ℕ) (x : ℝ), |iteratedDeriv n gevreyPartition x| ≤ (↑Kρ * (↑n + 1)) ^ (Kρ * (n + 1))) : ∃ (D : ℕ), 1 ≤ D ∧ ∀ {d : ℕ} (H : ℝ) (A : QuadraticChartData d), 1 ≤ d → QuadraticChartComplexity c₀ H A → ∀ (i a b : ℤ), |i| ≤ 3 → |a| ≤ 3 → |b| ≤ 3 → let Ki := slowValueBox d ⌈H + 1 + |↑(i - a)|⌉₊; let Kb := slowValueBox d ⌈2 + |↑(b - a)|⌉₊; have f := fun (q : (↥Ki × ↥Kb) × (Fin (d + d + d) → ℤ)) => sepCoeff A.amplitude ψ i a b (↑q.1.1) (↑q.1.2) q.2 * ↑(6 ^ d) ^ 3; (Summable fun (q : (↥Ki × ↥Kb) × (Fin (d + d + d) → ℤ)) => ‖f q‖) ∧ ∑' (q : (↥Ki × ↥Kb) × (Fin (d + d + d) → ℤ)), ‖f q‖ ≤ Real.exp (↑D * (1 + Real.log H) ^ D) ∧ ∀ (T : ℝ), 1 ≤ T → (Summable fun (q : (↥Ki × ↥Kb) × (Fin (d + d + d) → ℤ)) => if T ≤ 1 + frequencyLength q.2 then ‖f q‖ else 0) ∧ (∑' (q : (↥Ki × ↥Kb) × (Fin (d + d + d) → ℤ)), if T ≤ 1 + frequencyLength q.2 then ‖f q‖ else 0) ≤ Real.exp (↑D * (1 + Real.log H) ^ D) / T ^ 100

The normalized coefficient family of one separated atom: total mass and tails (lem:separation, line 1407), quasipolynomial in H.

theorem TrilinearHT.Auto.sepQ_le {i a b : ℤ} (hi : |i| ≤ 3) (ha : |a| ≤ 3) (hb : |b| ≤ 3) : sepQ i a b ≤ 55

theorem TrilinearHT.Auto.sum_abs_le_card_mul_length {n : ℕ} (p : Fin n → ℤ) : ∑ l : Fin n, |↑(p l)| ≤ ↑n * frequencyLength p

theorem TrilinearHT.Auto.slowBox_pair_card_le {d : ℕ} {H : ℝ} (hH7 : 7 ≤ H) (i a b : ℤ) (hi : |i| ≤ 3) (ha : |a| ≤ 3) (hb : |b| ≤ 3) : ↑(Fintype.card (↥(slowValueBox d ⌈H + 1 + |↑(i - a)|⌉₊) × ↥(slowValueBox d ⌈2 + |↑(b - a)|⌉₊))) ≤ (95 * H) ^ d

The slow-value boxes of one separated atom have at most (95 H)^d elements.

theorem TrilinearHT.Auto.slowBox_pair_card_exp_le {d : ℕ} {H : ℝ} (hH7 : 7 ≤ H) (hd : ↑d ≤ Real.log H) (i a b : ℤ) (hi : |i| ≤ 3) (ha : |a| ≤ 3) (hb : |b| ≤ 3) : ↑(Fintype.card (↥(slowValueBox d ⌈H + 1 + |↑(i - a)|⌉₊) × ↥(slowValueBox d ⌈2 + |↑(b - a)|⌉₊))) ≤ Real.exp (5 * (1 + Real.log H) ^ 2)

The slow-value count of one separated atom is quasi-polynomial.