Section 5: Quadratic chart definitions and closure

This file was automatically generated by Claude.

Formalization of blueprint Section 5, "Quadratic chart definitions and closure" (sec:chart-definitions, lines 624-663) of blueprint/formalization_blueprint.tex.

def TrilinearHT.Auto.chartRationalHeight (q : ℚ) : ℕ

Primitive numerator/denominator height for chart matrices.

Equations

• TrilinearHT.Auto.chartRationalHeight q = max q.num.natAbs q.den

theorem TrilinearHT.Auto.chartRationalHeight_neg (q : ℚ) : chartRationalHeight (-q) = chartRationalHeight q

Quadratic chart definitions

Blueprint def:chart, lines 625-637. The horizontal frequencies and the ordinary real quadratic and linear phases are unrestricted. Complexity is charged only to dimension, rational matrix height, support and cutoff derivatives.

noncomputable def TrilinearHT.Auto.coordinateWordDerivative {d : ℕ} (m : ℕ) (χ : (Fin d → ℝ) → ℂ) (word : Fin m → Fin d) (z : Fin d → ℝ) : ℂ

A coordinate mixed derivative, indexed by its ordered coordinate word. For smooth functions this is the usual multi-index derivative of total order m.

Equations

• TrilinearHT.Auto.coordinateWordDerivative m χ word z = (iteratedFDeriv ℝ m χ z) fun (i : Fin m) => Pi.single (word i) 1

theorem TrilinearHT.Auto.coordinateWordDerivative_zero {d : ℕ} (χ : (Fin d → ℝ) → ℂ) (word : Fin 0 → Fin d) (z : Fin d → ℝ) : coordinateWordDerivative 0 χ word z = χ z

structure TrilinearHT.Auto.QuadraticChartData (d : ℕ) : Type

The data in the source quadratic chart formula. Smoothness means C-infinity, and imposes no analyticity assumption on the compact cutoff.

• horizontal : Fin d → ℝ

  Horizontal direction used to sample the chart amplitude.

• quadratic : ℝ

  Coefficient of the scalar quadratic phase.

• linear : ℝ

  Coefficient of the scalar linear phase.

• matrix : Matrix (Fin d) (Fin d) ℚ

  Rational matrix defining the chart's bilinear lattice phase.

• amplitude : (Fin d → ℝ) → ℂ

  Smooth compactly supported amplitude of the chart.

• smooth : ContDiff ℝ (↑⊤) self.amplitude
• compact : HasCompactSupport self.amplitude

noncomputable def TrilinearHT.Auto.chartMatrixPhase {d : ℕ} (C : Matrix (Fin d) (Fin d) ℚ) (z w : Fin d → ℝ) : ℝ

The bilinear phase z^T C w in a quadratic chart.

Equations

• TrilinearHT.Auto.chartMatrixPhase C z w = ∑ i : Fin d, ∑ j : Fin d, z i * ↑(C i j) * w j

noncomputable def TrilinearHT.Auto.chartHorizontalPosition {d : ℕ} (A : QuadraticChartData d) (y : ℝ) : Fin d → ℝ

Horizontal position of the chart at the real parameter y.

Equations

• TrilinearHT.Auto.chartHorizontalPosition A y i = A.horizontal i * y

noncomputable def TrilinearHT.Auto.chartLatticeRemainder {d : ℕ} (A : QuadraticChartData d) (y : ℝ) (n : Fin d → ℤ) : Fin d → ℝ

Horizontal position after subtracting the integer lattice point n.

Equations

• TrilinearHT.Auto.chartLatticeRemainder A y n i = A.horizontal i * y - ↑(n i)

noncomputable def TrilinearHT.Auto.quadraticChartLatticeSummand {d : ℕ} (A : QuadraticChartData d) (y : ℝ) (n : Fin d → ℤ) : ℂ

Amplitude and bilinear phase contributed by the lattice point n.

Equations

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

noncomputable def TrilinearHT.Auto.quadraticChartAtom {d : ℕ} (A : QuadraticChartData d) (y : ℝ) : ℂ

Blueprint def:chart, formula (atom): the actual quadratic chart function.

Equations

• TrilinearHT.Auto.quadraticChartAtom A y = ↑(Real.fourierChar (A.quadratic * y ^ 2 + A.linear * y)) * ∑' (n : Fin d → ℤ), TrilinearHT.Auto.quadraticChartLatticeSummand A y n

structure TrilinearHT.Auto.QuadraticChartComplexity {d : ℕ} (c₀ : ℕ) (H : ℝ) (A : QuadraticChartData d) : Prop

The source complexity convention at one fixed Gevrey order c₀. Coordinate words encode mixed partial derivatives and their length is total order. The real phase and horizontal parameters deliberately carry no size restrictions.

• lower : Real.exp 2 ≤ H
• dimension : ↑d ≤ Real.log H
• height (i j : Fin d) : ↑(chartRationalHeight (A.matrix i j)) ≤ H
• support (z : Fin d → ℝ) : A.amplitude z ≠ 0 → ∀ (i : Fin d), |z i| ≤ H
• derivative (m : ℕ) (word : Fin m → Fin d) (z : Fin d → ℝ) : ‖coordinateWordDerivative m A.amplitude word z‖ ≤ H ^ (c₀ * (m + 1)) * (↑m + 1) ^ (c₀ * (m + 1))

def TrilinearHT.Auto.IsBoundedQuadraticChart {d : ℕ} (A : QuadraticChartData d) : Prop

A bounded atom has pointwise supremum norm at most one.

Equations

• TrilinearHT.Auto.IsBoundedQuadraticChart A = ∀ (y : ℝ), ‖TrilinearHT.Auto.quadraticChartAtom A y‖ ≤ 1

theorem TrilinearHT.Auto.quadraticChartComplexity_parameter_pos {d c₀ : ℕ} {H : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) : 0 < H

theorem TrilinearHT.Auto.quadraticChartComplexity_amplitude_bound {d c₀ : ℕ} {H : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) (z : Fin d → ℝ) : ‖A.amplitude z‖ ≤ H ^ c₀

theorem TrilinearHT.Auto.norm_quadraticChartLatticeSummand {d : ℕ} (A : QuadraticChartData d) (y : ℝ) (n : Fin d → ℤ) : ‖quadraticChartLatticeSummand A y n‖ = ‖A.amplitude (chartLatticeRemainder A y n)‖

Quadratic chart lattice sums

noncomputable def TrilinearHT.Auto.chartLatticeBox {d : ℕ} (H : ℝ) (z : Fin d → ℝ) : Finset (Fin d → ℤ)

A finite integer box containing every lattice translate that can meet a cutoff supported in [-H,H]^d at horizontal position z.

Equations

• TrilinearHT.Auto.chartLatticeBox H z = Fintype.piFinset fun (i : Fin d) => Finset.Icc ⌊z i - H⌋ ⌊z i + H⌋

theorem TrilinearHT.Auto.mem_chartLatticeBox_of_bound {d : ℕ} {H : ℝ} {z : Fin d → ℝ} {n : Fin d → ℤ} (hn : ∀ (i : Fin d), |z i - ↑(n i)| ≤ H) : n ∈ chartLatticeBox H z

theorem TrilinearHT.Auto.chartLatticeBox_card_le {d : ℕ} {H : ℝ} (hH : 0 ≤ H) (z : Fin d → ℝ) : ↑(chartLatticeBox H z).card ≤ (2 * H + 3) ^ d

theorem TrilinearHT.Auto.quadraticChartSummand_eq_zero_off_box {d : ℕ} (A : QuadraticChartData d) {H : ℝ} (hχ : ∀ (z : Fin d → ℝ), A.amplitude z ≠ 0 → ∀ (i : Fin d), |z i| ≤ H) (y : ℝ) {n : Fin d → ℤ} (hn : n ∉ chartLatticeBox H (chartHorizontalPosition A y)) : quadraticChartLatticeSummand A y n = 0

theorem TrilinearHT.Auto.quadraticChartData_support_bound {d : ℕ} (A : QuadraticChartData d) : ∃ (H : ℝ), 0 < H ∧ ∀ (z : Fin d → ℝ), A.amplitude z ≠ 0 → ∀ (i : Fin d), |z i| ≤ H

theorem TrilinearHT.Auto.quadraticChartLatticeSummand_finite_support {d : ℕ} (A : QuadraticChartData d) (y : ℝ) : (Function.support (quadraticChartLatticeSummand A y)).Finite

Compact support makes the chart's lattice series a genuine finite sum.

theorem TrilinearHT.Auto.quadraticChartAtom_eq_sum {d c₀ : ℕ} {H : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) (y : ℝ) : quadraticChartAtom A y = ↑(Real.fourierChar (A.quadratic * y ^ 2 + A.linear * y)) * ∑ n ∈ chartLatticeBox H (chartHorizontalPosition A y), quadraticChartLatticeSummand A y n

theorem TrilinearHT.Auto.quadraticChartAtom_norm_le {d c₀ : ℕ} {H : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) (y : ℝ) : ‖quadraticChartAtom A y‖ ≤ (2 * H + 3) ^ d * H ^ c₀

Quadratic chart normalization

noncomputable def TrilinearHT.Auto.ordinaryQuadraticChart (lam β : ℝ) : QuadraticChartData 0

Ordinary quadratic phases are zero-dimensional chart atoms.

Equations

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

theorem TrilinearHT.Auto.ordinaryQuadraticChart_atom (lam β y : ℝ) : quadraticChartAtom (ordinaryQuadraticChart lam β) y = ↑(Real.fourierChar (lam * y ^ 2 + β * y))

theorem TrilinearHT.Auto.ordinaryQuadraticChart_complexity (c₀ : ℕ) {H : ℝ} (hH : Real.exp 2 ≤ H) (lam β : ℝ) : QuadraticChartComplexity c₀ H (ordinaryQuadraticChart lam β)

theorem TrilinearHT.Auto.ordinaryQuadraticChart_bounded (lam β : ℝ) : IsBoundedQuadraticChart (ordinaryQuadraticChart lam β)

noncomputable def TrilinearHT.Auto.scaleQuadraticChartAmplitude {d : ℕ} (a : ℂ) (A : QuadraticChartData d) : QuadraticChartData d

Scalar sizes are external coefficients; multiplying the cutoff by a scalar of modulus at most one does not increase complexity.

Equations

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

theorem TrilinearHT.Auto.coordinateWordDerivative_scaleChart {d : ℕ} (a : ℂ) (A : QuadraticChartData d) (m : ℕ) (word : Fin m → Fin d) (z : Fin d → ℝ) : coordinateWordDerivative m (scaleQuadraticChartAmplitude a A).amplitude word z = a * coordinateWordDerivative m A.amplitude word z

theorem TrilinearHT.Auto.scaleQuadraticChartAmplitude_atom {d : ℕ} (a : ℂ) (A : QuadraticChartData d) (y : ℝ) : quadraticChartAtom (scaleQuadraticChartAmplitude a A) y = a * quadraticChartAtom A y

theorem TrilinearHT.Auto.scaleQuadraticChartAmplitude_complexity {d c₀ : ℕ} {H : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) {a : ℂ} (ha : ‖a‖ ≤ 1) : QuadraticChartComplexity c₀ H (scaleQuadraticChartAmplitude a A)

Quadratic chart conjugation

noncomputable def TrilinearHT.Auto.conjugateQuadraticChart {d : ℕ} (A : QuadraticChartData d) : QuadraticChartData d

Blueprint lem:chart-operations: conjugate the cutoff and negate both ordinary phases and the rational matrix.

Equations

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

theorem TrilinearHT.Auto.chartMatrixPhase_neg {d : ℕ} (C : Matrix (Fin d) (Fin d) ℚ) (z w : Fin d → ℝ) : chartMatrixPhase (-C) z w = -chartMatrixPhase C z w

theorem TrilinearHT.Auto.coordinateWordDerivative_conjugateChart {d : ℕ} (A : QuadraticChartData d) (m : ℕ) (word : Fin m → Fin d) (z : Fin d → ℝ) : coordinateWordDerivative m (conjugateQuadraticChart A).amplitude word z = star (coordinateWordDerivative m A.amplitude word z)

theorem TrilinearHT.Auto.conjugateQuadraticChart_atom {d : ℕ} (A : QuadraticChartData d) (y : ℝ) : quadraticChartAtom (conjugateQuadraticChart A) y = star (quadraticChartAtom A y)

Conjugation gives exactly the pointwise complex conjugate of the atom.

theorem TrilinearHT.Auto.conjugateQuadraticChart_complexity {d c₀ : ℕ} {H : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) : QuadraticChartComplexity c₀ H (conjugateQuadraticChart A)

Blueprint lem:chart-operations: conjugation preserves the exact original dimension, height, support and fixed-order Gevrey budget.

theorem TrilinearHT.Auto.conjugateQuadraticChart_bounded {d : ℕ} {A : QuadraticChartData d} (hA : IsBoundedQuadraticChart A) : IsBoundedQuadraticChart (conjugateQuadraticChart A)

Blueprint lem:chart-operations: a bounded chart stays bounded under conjugation.

Quadratic chart dilation

noncomputable def TrilinearHT.Auto.dilateQuadraticChart {d : ℕ} (a : ℝ) (A : QuadraticChartData d) : QuadraticChartData d

Blueprint lem:chart-operations: a real dilation changes only the unrestricted horizontal, quadratic and linear frequencies.

Equations

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

theorem TrilinearHT.Auto.dilateQuadraticChart_atom {d : ℕ} (a : ℝ) (A : QuadraticChartData d) (y : ℝ) : quadraticChartAtom (dilateQuadraticChart a A) y = quadraticChartAtom A (a * y)

The dilated chart is the exact dilated atom, including dilation by zero.

theorem TrilinearHT.Auto.dilateQuadraticChart_complexity {d c₀ : ℕ} {H : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) (a : ℝ) : QuadraticChartComplexity c₀ H (dilateQuadraticChart a A)

Blueprint lem:chart-operations: dilation has no complexity cost, uniformly over every real dilation parameter.

theorem TrilinearHT.Auto.dilateQuadraticChart_bounded {d : ℕ} {A : QuadraticChartData d} (hA : IsBoundedQuadraticChart A) (a : ℝ) : IsBoundedQuadraticChart (dilateQuadraticChart a A)

Blueprint lem:chart-operations: dilation preserves pointwise boundedness.

Quadratic chart products

def TrilinearHT.Auto.chartBlockMatrix {d e : ℕ} (C : Matrix (Fin d) (Fin d) ℚ) (D : Matrix (Fin e) (Fin e) ℚ) : Matrix (Fin (d + e)) (Fin (d + e)) ℚ

Block-diagonal rational matrix on concatenated finite coordinates.

Equations

• TrilinearHT.Auto.chartBlockMatrix C D i j = Fin.addCases (fun (i : Fin d) => Fin.addCases (C i) (fun (x : Fin e) => 0) j) (fun (i : Fin e) => Fin.addCases (fun (x : Fin d) => 0) (D i) j) i

theorem TrilinearHT.Auto.chartMatrixPhase_block {d e : ℕ} (C : Matrix (Fin d) (Fin d) ℚ) (D : Matrix (Fin e) (Fin e) ℚ) (z w : Fin (d + e) → ℝ) : chartMatrixPhase (chartBlockMatrix C D) z w = (chartMatrixPhase C (fun (i : Fin d) => z (Fin.castAdd e i)) fun (i : Fin d) => w (Fin.castAdd e i)) + chartMatrixPhase D (fun (i : Fin e) => z (Fin.natAdd d i)) fun (i : Fin e) => w (Fin.natAdd d i)

noncomputable def TrilinearHT.Auto.productChartAmplitude {d e : ℕ} (A : QuadraticChartData d) (B : QuadraticChartData e) (z : Fin (d + e) → ℝ) : ℂ

Product of the two cutoffs in their disjoint coordinate blocks.

Equations

• TrilinearHT.Auto.productChartAmplitude A B z = (A.amplitude fun (i : Fin d) => z (Fin.castAdd e i)) * B.amplitude fun (i : Fin e) => z (Fin.natAdd d i)

theorem TrilinearHT.Auto.productChartAmplitude_smooth {d e : ℕ} (A : QuadraticChartData d) (B : QuadraticChartData e) : ContDiff ℝ (↑⊤) (productChartAmplitude A B)

theorem TrilinearHT.Auto.productChartAmplitude_compact {d e : ℕ} (A : QuadraticChartData d) (B : QuadraticChartData e) : HasCompactSupport (productChartAmplitude A B)

noncomputable def TrilinearHT.Auto.productQuadraticChart {d e : ℕ} (A : QuadraticChartData d) (B : QuadraticChartData e) : QuadraticChartData (d + e)

Blueprint lem:chart-operations: concatenate horizontal coordinates, add ordinary phases, and take a block-diagonal rational matrix.

Equations

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

theorem TrilinearHT.Auto.productQuadraticChart_summand {d e : ℕ} (A : QuadraticChartData d) (B : QuadraticChartData e) (y : ℝ) (n : Fin d → ℤ) (m : Fin e → ℤ) : quadraticChartLatticeSummand (productQuadraticChart A B) y (Fin.append n m) = quadraticChartLatticeSummand A y n * quadraticChartLatticeSummand B y m

theorem TrilinearHT.Auto.productQuadraticChart_atom {d e : ℕ} (A : QuadraticChartData d) (B : QuadraticChartData e) (y : ℝ) : quadraticChartAtom (productQuadraticChart A B) y = quadraticChartAtom A y * quadraticChartAtom B y

Blueprint lem:chart-operations: the block construction is exactly pointwise multiplication, with all lattice sums factored legitimately.

Quadratic chart product complexity

theorem TrilinearHT.Auto.chart_multilinear_norm_le_coordinates {d m : ℕ} (T : (Fin d → ℝ) [×m]→L[ℝ] ℂ) {M : ℝ} (hM : 0 ≤ M) (hT : ∀ (word : Fin m → Fin d), ‖T fun (i : Fin m) => Pi.single (word i) 1‖ ≤ M) : ‖T‖ ≤ ↑d ^ m * M

Coordinate bounds control the multilinear operator norm with the finite-dimensional cost d^m. This includes order and dimension zero.

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

From the source coordinate Gevrey bounds to an operator-norm bound. The fixed Gevrey order is positive; no increase in that order is needed.

noncomputable def TrilinearHT.Auto.chartCoordinateRestriction {d D : ℕ} (s : Fin d → Fin D) : (Fin D → ℝ) →L[ℝ] Fin d → ℝ

Restriction to a chosen coordinate list, allowing repeated coordinates.

Equations

• TrilinearHT.Auto.chartCoordinateRestriction s = ContinuousLinearMap.pi fun (i : Fin d) => ContinuousLinearMap.proj (s i)

theorem TrilinearHT.Auto.chartCoordinateRestriction_norm_le {d D : ℕ} (s : Fin d → Fin D) : ‖chartCoordinateRestriction s‖ ≤ 1

theorem TrilinearHT.Auto.chart_cutoff_restriction_bound {d D c₀ : ℕ} {H : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) (hc : 1 ≤ c₀) (s : Fin d → Fin D) (m : ℕ) (z : Fin D → ℝ) : ‖iteratedFDeriv ℝ m (fun (x : Fin D → ℝ) => A.amplitude fun (i : Fin d) => x (s i)) z‖ ≤ H ^ (2 * c₀ * (m + 1)) * (↑m + 1) ^ (c₀ * (m + 1))

theorem TrilinearHT.Auto.chart_product_derivative_geometric {D m : ℕ} {f g : (Fin D → ℝ) → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (z : Fin D → ℝ) {R : ℝ} (hR : 0 ≤ R) (hfi : ∀ i ≤ m, ‖iteratedFDeriv ℝ i f z‖ ≤ R ^ (i + 1)) (hgi : ∀ i ≤ m, ‖iteratedFDeriv ℝ i g z‖ ≤ R ^ (i + 1)) : ‖iteratedFDeriv ℝ m (fun (x : Fin D → ℝ) => f x * g x) z‖ ≤ 2 ^ m * R ^ (m + 2)

Leibniz's rule in operator norm, with a geometric derivative majorant.

theorem TrilinearHT.Auto.chart_cutoff_restriction_geometric {d D c₀ : ℕ} {H : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) (hc : 1 ≤ c₀) (s : Fin d → Fin D) (m i : ℕ) (hi : i ≤ m) (z : Fin D → ℝ) : ‖iteratedFDeriv ℝ i (fun (x : Fin D → ℝ) => A.amplitude fun (j : Fin d) => x (s j)) z‖ ≤ (H ^ (2 * c₀) * (↑m + 1) ^ c₀) ^ (i + 1)

theorem TrilinearHT.Auto.chart_product_geometric_budget {H : ℝ} (hH : 2 ≤ H) {c₀ : ℕ} (hc : 1 ≤ c₀) (m : ℕ) : 2 ^ m * (H ^ (2 * c₀) * (↑m + 1) ^ c₀) ^ (m + 2) ≤ (H ^ 6) ^ (c₀ * (m + 1)) * (↑m + 1) ^ (c₀ * (m + 1))

The elementary scalar estimate preserving the fixed Gevrey order in the product rule. A sixth power of the old height absorbs all extra factors.

theorem TrilinearHT.Auto.productChartAmplitude_derivative_bound {d e c₀ : ℕ} {H : ℝ} {A : QuadraticChartData d} {B : QuadraticChartData e} (hA : QuadraticChartComplexity c₀ H A) (hB : QuadraticChartComplexity c₀ H B) (hc : 1 ≤ c₀) (m : ℕ) (word : Fin m → Fin (d + e)) (z : Fin (d + e) → ℝ) : ‖coordinateWordDerivative m (productChartAmplitude A B) word z‖ ≤ (H ^ 6) ^ (c₀ * (m + 1)) * (↑m + 1) ^ (c₀ * (m + 1))

The product cutoff retains the same Gevrey order, with height budget H^6.

theorem TrilinearHT.Auto.productQuadraticChart_complexity {d e c₀ : ℕ} {H : ℝ} {A : QuadraticChartData d} {B : QuadraticChartData e} (hA : QuadraticChartComplexity c₀ H A) (hB : QuadraticChartComplexity c₀ H B) (hc : 1 ≤ c₀) : QuadraticChartComplexity c₀ (H ^ 6) (productQuadraticChart A B)

Blueprint lem:chart-operations: the product of two complexity-H charts has complexity at most H^6, uniformly in every real frequency.

Fixed finite chart products

theorem TrilinearHT.Auto.quadraticChartComplexity_mono {d c₀ : ℕ} {H K : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) (hHK : H ≤ K) : QuadraticChartComplexity c₀ K A

theorem TrilinearHT.Auto.productQuadraticChart_bounded {d e : ℕ} {A : QuadraticChartData d} {B : QuadraticChartData e} (hA : IsBoundedQuadraticChart A) (hB : IsBoundedQuadraticChart B) : IsBoundedQuadraticChart (productQuadraticChart A B)

Chart translation offset reduction

theorem TrilinearHT.Auto.chart_matrix_clear_denominators {d : ℕ} {H : ℝ} (hH : 0 ≤ H) (C : Matrix (Fin d) (Fin d) ℚ) (hC : ∀ (i j : Fin d), ↑(chartRationalHeight (C i j)) ≤ H) : ∃ (P : ℕ) (Z : Matrix (Fin d) (Fin d) ℤ), 0 < P ∧ ↑P ≤ H ^ d ^ 2 ∧ ∀ (i j : Fin d), ↑(Z i j) = ↑P * ↑(C i j)

Blueprint lem:chart-operations, line 646: clear the rational matrix with a positive common denominator bounded by H^(d^2), for real height budgets.

theorem TrilinearHT.Auto.chart_translation_offset_reduction {d : ℕ} {H : ℝ} (hH : 0 ≤ H) (C : Matrix (Fin d) (Fin d) ℚ) (hC : ∀ (i j : Fin d), ↑(chartRationalHeight (C i j)) ≤ H) (v : Fin d → ℝ) : ∃ (P : ℕ) (m : Fin d → ℤ) (a : Fin d → ℝ), 0 < P ∧ ↑P ≤ H ^ d ^ 2 ∧ (∀ (i : Fin d), v i = ↑(m i) + a i) ∧ (∀ (i : Fin d), |a i| ≤ ↑P) ∧ ∀ (i j : Fin d), ∃ (z : ℤ), ↑z = ↑(m i) * ↑(C i j)

Blueprint lem:chart-operations: every real offset is an integer multiple of the cleared denominator plus a remainder of coordinate size at most that denominator. The integer part pairs integrally with the rational matrix.

theorem TrilinearHT.Auto.chartMatrixPhase_integer_of_coefficients {d : ℕ} (C : Matrix (Fin d) (Fin d) ℚ) (m n : Fin d → ℤ) (h : ∀ (i j : Fin d), ∃ (z : ℤ), ↑z = ↑(m i) * ↑(C i j)) : ∃ (z : ℤ), ↑z = chartMatrixPhase C (fun (i : Fin d) => ↑(m i)) fun (i : Fin d) => ↑(n i)

The omitted term in the source translation expansion is an integer phase.

theorem TrilinearHT.Auto.chart_fourierChar_int (n : ℤ) : ↑(Real.fourierChar ↑n) = 1

Integer errors do not change the real Fourier character.

theorem TrilinearHT.Auto.chart_fourierChar_add_int (x : ℝ) (n : ℤ) : ↑(Real.fourierChar (x + ↑n)) = ↑(Real.fourierChar x)

Exact chart translation

theorem TrilinearHT.Auto.chartMatrixPhase_add_left {d : ℕ} (C : Matrix (Fin d) (Fin d) ℚ) (z z' w : Fin d → ℝ) : chartMatrixPhase C (z + z') w = chartMatrixPhase C z w + chartMatrixPhase C z' w

theorem TrilinearHT.Auto.chartMatrixPhase_add_right {d : ℕ} (C : Matrix (Fin d) (Fin d) ℚ) (z w w' : Fin d → ℝ) : chartMatrixPhase C z (w + w') = chartMatrixPhase C z w + chartMatrixPhase C z w'

theorem TrilinearHT.Auto.chartMatrixPhase_sub_right {d : ℕ} (C : Matrix (Fin d) (Fin d) ℚ) (z w w' : Fin d → ℝ) : chartMatrixPhase C z (w - w') = chartMatrixPhase C z w - chartMatrixPhase C z w'

theorem TrilinearHT.Auto.chartMatrixPhase_smul_left {d : ℕ} (C : Matrix (Fin d) (Fin d) ℚ) (r : ℝ) (z w : Fin d → ℝ) : chartMatrixPhase C (r • z) w = r * chartMatrixPhase C z w

theorem TrilinearHT.Auto.chartMatrixPhase_smul_right {d : ℕ} (C : Matrix (Fin d) (Fin d) ℚ) (r : ℝ) (z w : Fin d → ℝ) : chartMatrixPhase C z (r • w) = r * chartMatrixPhase C z w

theorem TrilinearHT.Auto.chartMatrixPhase_translation_identity {d : ℕ} (C : Matrix (Fin d) (Fin d) ℚ) (z a m n : Fin d → ℝ) : chartMatrixPhase C (z + m + a) (z - n + a) = chartMatrixPhase C z (z - n) + chartMatrixPhase C z a + chartMatrixPhase C m z + chartMatrixPhase C a (z - n + a) + chartMatrixPhase C m a - chartMatrixPhase C m n

The source translation expansion as an exact equality before discarding the final integral bilinear term.

theorem TrilinearHT.Auto.chart_fourierChar_smooth : ContDiff ℝ ↑⊤ fun (x : ℝ) => ↑(Real.fourierChar x)

noncomputable def TrilinearHT.Auto.translatedChartAmplitude {d : ℕ} (A : QuadraticChartData d) (a z : Fin d → ℝ) : ℂ

The translated, phase-modulated cutoff in the source proof.

Equations

• TrilinearHT.Auto.translatedChartAmplitude A a z = A.amplitude (z + a) * ↑(Real.fourierChar (TrilinearHT.Auto.chartMatrixPhase A.matrix a (z + a)))

theorem TrilinearHT.Auto.translatedChartAmplitude_smooth {d : ℕ} (A : QuadraticChartData d) (a : Fin d → ℝ) : ContDiff ℝ (↑⊤) (translatedChartAmplitude A a)

theorem TrilinearHT.Auto.translatedChartAmplitude_compact {d : ℕ} (A : QuadraticChartData d) (a : Fin d → ℝ) : HasCompactSupport (translatedChartAmplitude A a)

noncomputable def TrilinearHT.Auto.chartTranslationConstant {d : ℕ} (A : QuadraticChartData d) (t : ℝ) (m : Fin d → ℤ) (a : Fin d → ℝ) : ℝ

The ordinary constant phase created by translation is unrestricted.

Equations

• TrilinearHT.Auto.chartTranslationConstant A t m a = A.quadratic * t ^ 2 + A.linear * t + TrilinearHT.Auto.chartMatrixPhase A.matrix (fun (i : Fin d) => ↑(m i)) a

noncomputable def TrilinearHT.Auto.chartTranslationLinear {d : ℕ} (A : QuadraticChartData d) (t : ℝ) (m : Fin d → ℤ) (a : Fin d → ℝ) : ℝ

Linear phase coefficient after translating the chart by t and the lattice offset m.

Equations

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

noncomputable def TrilinearHT.Auto.shiftedQuadraticChart {d : ℕ} (A : QuadraticChartData d) (t : ℝ) (m : Fin d → ℤ) (a : Fin d → ℝ) : QuadraticChartData d

The translated chart before multiplying by its constant unit phase.

Equations

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

noncomputable def TrilinearHT.Auto.translateQuadraticChart {d : ℕ} (A : QuadraticChartData d) (t : ℝ) (m : Fin d → ℤ) (a : Fin d → ℝ) : QuadraticChartData d

Blueprint lem:chart-operations: the translated cutoff and the unrestricted ordinary phases, with the unit constant absorbed into the cutoff.

Equations

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

theorem TrilinearHT.Auto.chart_translation_phase_identity {d : ℕ} (A : QuadraticChartData d) (t y : ℝ) (m n : Fin d → ℤ) (a : Fin d → ℝ) : (A.quadratic * (y + t) ^ 2 + A.linear * (y + t) + chartMatrixPhase A.matrix ((y • A.horizontal + fun (i : Fin d) => ↑(m i)) + a) ((y • A.horizontal - fun (i : Fin d) => ↑(n i)) + a) + chartMatrixPhase A.matrix (fun (i : Fin d) => ↑(m i)) fun (i : Fin d) => ↑(n i)) = chartTranslationConstant A t m a + (A.quadratic * y ^ 2 + chartTranslationLinear A t m a * y) + chartMatrixPhase A.matrix a ((y • A.horizontal - fun (i : Fin d) => ↑(n i)) + a) + chartMatrixPhase A.matrix (y • A.horizontal) (y • A.horizontal - fun (i : Fin d) => ↑(n i))

theorem TrilinearHT.Auto.translatedChart_phased_summand {d : ℕ} (A : QuadraticChartData d) (t y : ℝ) (m n : Fin d → ℤ) (a : Fin d → ℝ) (hoff : ∀ (i : Fin d), A.horizontal i * t = ↑(m i) + a i) (hint : ∀ (i j : Fin d), ∃ (z : ℤ), ↑z = ↑(m i) * ↑(A.matrix i j)) : ↑(Real.fourierChar (chartTranslationConstant A t m a)) * (↑(Real.fourierChar (A.quadratic * y ^ 2 + chartTranslationLinear A t m a * y)) * quadraticChartLatticeSummand (shiftedQuadraticChart A t m a) y n) = ↑(Real.fourierChar (A.quadratic * (y + t) ^ 2 + A.linear * (y + t))) * quadraticChartLatticeSummand A (y + t) (n + m)

Equality of the individual translated lattice terms after multiplication by the ordinary phase factors. The only discarded phase is proved integral.

theorem TrilinearHT.Auto.translateQuadraticChart_atom {d : ℕ} (A : QuadraticChartData d) (t : ℝ) (m : Fin d → ℤ) (a : Fin d → ℝ) (hoff : ∀ (i : Fin d), A.horizontal i * t = ↑(m i) + a i) (hint : ∀ (i j : Fin d), ∃ (z : ℤ), ↑z = ↑(m i) * ↑(A.matrix i j)) (y : ℝ) : quadraticChartAtom (translateQuadraticChart A t m a) y = quadraticChartAtom A (y + t)

Blueprint lem:chart-operations: the constructed chart is exactly the translated atom. Translation size is unrestricted.

theorem TrilinearHT.Auto.translateQuadraticChart_bounded {d : ℕ} {A : QuadraticChartData d} (hA : IsBoundedQuadraticChart A) (t : ℝ) (m : Fin d → ℤ) (a : Fin d → ℝ) (hoff : ∀ (i : Fin d), A.horizontal i * t = ↑(m i) + a i) (hint : ∀ (i j : Fin d), ∃ (z : ℤ), ↑z = ↑(m i) * ↑(A.matrix i j)) : IsBoundedQuadraticChart (translateQuadraticChart A t m a)

Translation preserves the pointwise bound independently of its size.

Translated chart cutoff derivatives

theorem TrilinearHT.Auto.chart_fourierChar_iteratedDeriv (m : ℕ) (x : ℝ) : iteratedDeriv m (fun (t : ℝ) => ↑(Real.fourierChar t)) x = (2 * ↑Real.pi * Complex.I) ^ m * ↑(Real.fourierChar x)

theorem TrilinearHT.Auto.chart_fourierChar_derivative_norm (m : ℕ) (x : ℝ) : ‖iteratedFDeriv ℝ m (fun (t : ℝ) => ↑(Real.fourierChar t)) x‖ = (2 * Real.pi) ^ m

noncomputable def TrilinearHT.Auto.chartMatrixLeftLinear {d : ℕ} (C : Matrix (Fin d) (Fin d) ℚ) (a : Fin d → ℝ) : (Fin d → ℝ) →L[ℝ] ℝ

A real linear phase on the cutoff coordinates.

Equations

• TrilinearHT.Auto.chartMatrixLeftLinear C a = ∑ i : Fin d, ∑ j : Fin d, (a i * ↑(C i j)) • ContinuousLinearMap.proj j

theorem TrilinearHT.Auto.chartMatrixLeftLinear_apply {d : ℕ} (C : Matrix (Fin d) (Fin d) ℚ) (a z : Fin d → ℝ) : (chartMatrixLeftLinear C a) z = chartMatrixPhase C a z

theorem TrilinearHT.Auto.chart_linear_phase_derivative_bound {d : ℕ} (L : (Fin d → ℝ) →L[ℝ] ℝ) (a z : Fin d → ℝ) (m : ℕ) : ‖iteratedFDeriv ℝ m (fun (x : Fin d → ℝ) => ↑(Real.fourierChar (L (x + a)))) z‖ ≤ (2 * Real.pi * ‖L‖) ^ m

Every derivative of a shifted linear Fourier phase has a geometric operator-norm bound, independent of the shift.

theorem TrilinearHT.Auto.translatedChartAmplitude_derivative_bound {d c₀ : ℕ} {H T : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) (hc : 1 ≤ c₀) (hHT : H ≤ T) (a : Fin d → ℝ) (hphase : 2 * Real.pi * ‖chartMatrixLeftLinear A.matrix a‖ ≤ T) (m : ℕ) (word : Fin m → Fin d) (z : Fin d → ℝ) : ‖coordinateWordDerivative m (translatedChartAmplitude A a) word z‖ ≤ (T ^ 6) ^ (c₀ * (m + 1)) * (↑m + 1) ^ (c₀ * (m + 1))

The translated and phase-modulated cutoff obeys the same-order Gevrey bound at budget T^6, once T controls the old height and phase frequency.

Uniform chart translation complexity

theorem TrilinearHT.Auto.chartMatrixLeftLinear_norm_le {d : ℕ} {H P : ℝ} (C : Matrix (Fin d) (Fin d) ℚ) (a : Fin d → ℝ) (hH : 0 ≤ H) (hP : 0 ≤ P) (hC : ∀ (i j : Fin d), |↑(C i j)| ≤ H) (ha : ∀ (i : Fin d), |a i| ≤ P) : ‖chartMatrixLeftLinear C a‖ ≤ ↑d ^ 2 * P * H

noncomputable def TrilinearHT.Auto.chartTranslationBase (d : ℕ) (H : ℝ) : ℝ

An intermediate height controlling support and residual phase frequency.

Equations

• TrilinearHT.Auto.chartTranslationBase d H = H ^ (d ^ 2 + 6)

theorem TrilinearHT.Auto.chart_translation_base_controls {d c₀ : ℕ} {H P : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) (hP : 0 ≤ P) (hPH : P ≤ H ^ d ^ 2) (a : Fin d → ℝ) (ha : ∀ (i : Fin d), |a i| ≤ P) : H ≤ chartTranslationBase d H ∧ H + P ≤ chartTranslationBase d H ∧ 2 * Real.pi * ‖chartMatrixLeftLinear A.matrix a‖ ≤ chartTranslationBase d H

theorem TrilinearHT.Auto.translateQuadraticChart_complexity {d c₀ : ℕ} {H P : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) (hc : 1 ≤ c₀) (hP : 0 ≤ P) (hPH : P ≤ H ^ d ^ 2) (t : ℝ) (m : Fin d → ℤ) (a : Fin d → ℝ) (ha : ∀ (i : Fin d), |a i| ≤ P) : QuadraticChartComplexity c₀ (chartTranslationBase d H ^ 6) (translateQuadraticChart A t m a)

Translation complexity before replacing the dimension by its logarithmic bound.

noncomputable def TrilinearHT.Auto.chartTranslationBudget (H : ℝ) : ℝ

A uniform quasipolynomial budget for every real translation.

Equations

• TrilinearHT.Auto.chartTranslationBudget H = Real.exp (100 * TrilinearHT.Auto.logarithmicSize H ^ 3)

theorem TrilinearHT.Auto.chartTranslationBase_le_budget {d c₀ : ℕ} {H : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) : chartTranslationBase d H ^ 6 ≤ chartTranslationBudget H

theorem TrilinearHT.Auto.quadraticChart_translation_closure {d c₀ : ℕ} {H : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) (hc : 1 ≤ c₀) (t : ℝ) : ∃ (A' : QuadraticChartData d), QuadraticChartComplexity c₀ (chartTranslationBudget H) A' ∧ (IsBoundedQuadraticChart A → IsBoundedQuadraticChart A') ∧ ∀ (y : ℝ), quadraticChartAtom A' y = quadraticChartAtom A (y + t)

Blueprint lem:chart-operations: every real translation is represented by a chart with a quasipolynomial complexity bound independent of the translation. The Gevrey order is unchanged and boundedness is preserved.

Affine chart closure

theorem TrilinearHT.Auto.quadraticChart_affine_closure {d c₀ : ℕ} {H : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) (hc : 1 ≤ c₀) (s t : ℝ) : ∃ (A' : QuadraticChartData d), QuadraticChartComplexity c₀ (chartTranslationBudget H) A' ∧ (IsBoundedQuadraticChart A → IsBoundedQuadraticChart A') ∧ ∀ (y : ℝ), quadraticChartAtom A' y = quadraticChartAtom A (s * y + t)

Blueprint lem:chart-operations: any real affine substitution preserves quadratic charts with one quasipolynomial bound independent of both real parameters. This includes zero and negative dilation and preserves boundedness.

Several-variable chart formula

structure TrilinearHT.Auto.MultivariableQuadraticChartData (k d : ℕ) : Type

The several-variable source chart data, lines 656-660. The source uses one, two or three real variables; the same formula is meaningful in every finite dimension. Real horizontal and ordinary phase matrices are unrestricted.

• horizontal : Matrix (Fin d) (Fin k) ℝ

  Matrix of horizontal directions for the multivariable chart.

• quadratic : Matrix (Fin k) (Fin k) ℝ

  Symmetric matrix defining the quadratic phase in the input variables.

• symmetric : self.quadratic.IsSymm
• linear : Fin k → ℝ

  Linear phase coefficients in the input variables.

• matrix : Matrix (Fin d) (Fin d) ℚ

  Rational matrix defining the multivariable chart's lattice phase.

• amplitude : (Fin d → ℝ) → ℂ

  Smooth compactly supported amplitude of the multivariable chart.

• smooth : ContDiff ℝ (↑⊤) self.amplitude
• compact : HasCompactSupport self.amplitude

noncomputable def TrilinearHT.Auto.multivariableQuadraticChartAtom {k d : ℕ} (A : MultivariableQuadraticChartData k d) (z : Fin k → ℝ) : ℂ

The actual several-variable quadratic atom in the source display.

Equations

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

noncomputable def TrilinearHT.Auto.multivariableChartAlongLine {k d : ℕ} (A : MultivariableQuadraticChartData k d) (v : Fin k → ℝ) : QuadraticChartData d

Restricting a several-variable chart to a real line changes only the unrestricted horizontal and ordinary phase parameters.

Equations

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

def TrilinearHT.Auto.MultivariableQuadraticChartComplexity {k d : ℕ} (c₀ : ℕ) (H : ℝ) (A : MultivariableQuadraticChartData k d) : Prop

The same dimension, rational height and cutoff bounds as the one-variable definition. Evaluation on the zero line retains precisely this charged data.

Equations

• TrilinearHT.Auto.MultivariableQuadraticChartComplexity c₀ H A = TrilinearHT.Auto.QuadraticChartComplexity c₀ H (TrilinearHT.Auto.multivariableChartAlongLine A 0)

theorem TrilinearHT.Auto.multivariableChartAlongLine_complexity {k d c₀ : ℕ} {H : ℝ} {A : MultivariableQuadraticChartData k d} (hA : MultivariableQuadraticChartComplexity c₀ H A) (v : Fin k → ℝ) : QuadraticChartComplexity c₀ H (multivariableChartAlongLine A v)

theorem TrilinearHT.Auto.multivariableChartAlongLine_atom {k d : ℕ} (A : MultivariableQuadraticChartData k d) (v : Fin k → ℝ) (y : ℝ) : quadraticChartAtom (multivariableChartAlongLine A v) y = multivariableQuadraticChartAtom A (y • v)

Exact line restriction of the source several-variable formula.

Affine substitution in several-variable charts

def TrilinearHT.Auto.chartSkewPart {d : ℕ} (C : Matrix (Fin d) (Fin d) ℚ) : Matrix (Fin d) (Fin d) ℚ

Skew-symmetric part of the rational chart matrix.

Equations

• TrilinearHT.Auto.chartSkewPart C = (1 / 2) • (C - C.transpose)

Several-variable lattice finiteness