Quantitative rational linear algebra

This file was automatically generated by Codex.

This module proves uniform height and Euclidean operator-norm estimates for rational matrices, nonsingular inverses, pivot right inverses on their ranges, and orthogonal projections and their complements. It also counts matrices of bounded height and selects bounded-height bases without a spanning-list cost. The proof clears denominators and uses determinant and adjugate formulas. All statements and supporting definitions use only Mathlib and this module.

Source: blueprint/formalization_blueprint.tex, lem:rational-linear, lines 416–420. Verified library references are Mathlib.Data.Rat.Lemmas (reduced numerator and denominator), Mathlib.LinearAlgebra.Matrix.Adjugate (Cramer's rule), Mathlib.LinearAlgebra.Matrix.Rank (row and column rank), and Mathlib.Analysis.InnerProductSpace.Projection.Basic (orthogonal projection). The rational height convention agrees with Rat.mulHeight₁_eq_max in Mathlib.NumberTheory.Height.NumberField. The bounded-height frequency development uses the same independent denominator and determinant machinery (lem:height, lines 603–619).

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

Blueprint lem:rational-linear: height is the maximum of the absolute reduced numerator and the positive reduced denominator.

Equations

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

def TrilinearHT.Auto.boundedRationalEnumeration (B : ℕ) : Finset ℚ

A finite enumeration containing every rational of height at most B.

Equations

• TrilinearHT.Auto.boundedRationalEnumeration B = Finset.image (fun (p : ℤ × ℕ) => ↑p.1 / ↑p.2) (Finset.Icc (-↑B) ↑B ×ˢ Finset.Icc 1 B)

theorem TrilinearHT.Auto.mem_boundedRationalEnumeration {q : ℚ} {B : ℕ} (hq : rationalHeight q ≤ B) : q ∈ boundedRationalEnumeration B

theorem TrilinearHT.Auto.boundedRationalEnumeration_card (B : ℕ) (hB : 1 ≤ B) : (boundedRationalEnumeration B).card ≤ 3 * B ^ 2

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

def TrilinearHT.Auto.rationalCommonDenominator {ι : Type u_1} [Fintype ι] (a : ι → ℚ) : ℕ

A common denominator for a finite rational tuple, with exactly one factor for each entry as in lem:rational-linear, line 420.

Equations

• TrilinearHT.Auto.rationalCommonDenominator a = ∏ i : ι, (a i).den

theorem TrilinearHT.Auto.rationalCommonDenominator_pos {ι : Type u_1} [Fintype ι] (a : ι → ℚ) : 0 < rationalCommonDenominator a

theorem TrilinearHT.Auto.rationalCommonDenominator_le {ι : Type u_1} [Fintype ι] (a : ι → ℚ) {B : ℕ} (ha : ∀ (i : ι), rationalHeight (a i) ≤ B) : rationalCommonDenominator a ≤ B ^ Fintype.card ι

theorem TrilinearHT.Auto.rational_clear_denominators {ι : Type u_1} [Fintype ι] (a : ι → ℚ) {B : ℕ} (ha : ∀ (i : ι), rationalHeight (a i) ≤ B) : ∃ (z : ι → ℤ), ∀ (i : ι), ↑(z i) = ↑(rationalCommonDenominator a) * a i ∧ (z i).natAbs ≤ B * rationalCommonDenominator a

Clearing all denominators gives integer coordinates of size at most B D, where D is their positive common denominator.

theorem TrilinearHT.Auto.integerMatrix_det_bound {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) {K : ℕ} (hA : ∀ (i j : Fin n), (A i j).natAbs ≤ K) : A.det.natAbs ≤ n.factorial * K ^ n

Determinant expansion bound for an integer matrix. This also controls every square minor by applying the same theorem to its submatrix.

theorem TrilinearHT.Auto.rationalHeight_div_int_le (a b : ℤ) (hb : b ≠ 0) : rationalHeight (↑a / ↑b) ≤ max a.natAbs b.natAbs

theorem TrilinearHT.Auto.rationalMatrix_clear_denominators {n B : ℕ} (A : Matrix (Fin n) (Fin n) ℚ) (hA : ∀ (i j : Fin n), rationalHeight (A i j) ≤ B) : ∃ (D : ℕ) (Z : Matrix (Fin n) (Fin n) ℤ), 0 < D ∧ D ≤ B ^ n ^ 2 ∧ (∀ (i j : Fin n), ↑(Z i j) = ↑D * A i j) ∧ (∀ (i j : Fin n), (Z i j).natAbs ≤ B ^ (n ^ 2 + 1)) ∧ Z.det.natAbs ≤ n.factorial * B ^ (n * (n ^ 2 + 1))

Blueprint lem:rational-linear, line 420: the product of all matrix denominators is at most B^(n²), and the cleared integer entries are at most B^(n²+1). The determinant bound is the one from the source expansion.

theorem TrilinearHT.Auto.integerMatrix_adjugate_bound {n K : ℕ} (hK : 1 ≤ K) (Z : Matrix (Fin n) (Fin n) ℤ) (hZ : ∀ (i j : Fin n), (Z i j).natAbs ≤ K) (i j : Fin n) : (Z.adjugate i j).natAbs ≤ n.factorial * K ^ n

theorem TrilinearHT.Auto.rationalMatrix_inverse_entry {n : ℕ} (A : Matrix (Fin n) (Fin n) ℚ) (hA : A.det ≠ 0) {D : ℕ} (hD : 0 < D) (Z : Matrix (Fin n) (Fin n) ℤ) (hZ : ∀ (i j : Fin n), ↑(Z i j) = ↑D * A i j) : Z.det ≠ 0 ∧ ∀ (i j : Fin n), A⁻¹ i j = ↑(↑D * Z.adjugate i j) / ↑Z.det

The adjugate formula after clearing denominators, keeping the original matrix inverse and an integer numerator and denominator.

theorem TrilinearHT.Auto.rationalMatrix_inverse_height_raw {n B : ℕ} (hB : 1 ≤ B) (A : Matrix (Fin n) (Fin n) ℚ) (hA : ∀ (i j : Fin n), rationalHeight (A i j) ≤ B) (hdet : A.det ≠ 0) (i j : Fin n) : rationalHeight (A⁻¹ i j) ≤ n.factorial * B ^ (n ^ 2 + n * (n ^ 2 + 1))

The explicit Cramer bound underlying lem:rational-linear: inverse entry heights are bounded by a factorial times a polynomial power of B.

theorem TrilinearHT.Auto.euclidean_norm_le_sum_coordinates {n : ℕ} (x : EuclideanSpace ℝ (Fin n)) : ‖x‖ ≤ ∑ i : Fin n, ‖x.ofLp i‖

theorem TrilinearHT.Auto.realMatrix_operatorNorm_le {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) {K : ℝ} (hK : 0 ≤ K) (hA : ∀ (i j : Fin n), |A i j| ≤ K) : ‖Matrix.toEuclideanCLM A‖ ≤ ↑n ^ 2 * K

An entrywise bound controls the Euclidean operator norm. The harmless quadratic dimension factor is absorbed in the source exponential bound.

theorem TrilinearHT.Auto.rational_inverse_budget (n B : ℕ) (hB : 1 ≤ B) : (n + 1) ^ 2 * (n.factorial * B ^ (n ^ 2 + n * (n ^ 2 + 1))) ≤ (2 * B) ^ (2 * (n + 1) ^ 4)

theorem TrilinearHT.Auto.rationalMatrix_inverse_bounds {n d : ℕ} (hnd : n ≤ d) {B : ℝ} (hB : 2 ≤ B) (A : Matrix (Fin n) (Fin n) ℚ) (hA : ∀ (i j : Fin n), ↑(rationalHeight (A i j)) ≤ B) (hdet : A.det ≠ 0) : (∀ (i j : Fin n), ↑(rationalHeight (A⁻¹ i j)) ≤ Real.exp (2 * (↑d + 1) ^ 4 * Real.log (2 * B))) ∧ ‖Matrix.toEuclideanCLM (A⁻¹.map fun (q : ℚ) => ↑q)‖ ≤ Real.exp (2 * (↑d + 1) ^ 4 * Real.log (2 * B))

Blueprint lem:rational-linear, lines 418–420: nonsingular rational inverses have entry heights and Euclidean operator norm at most exp (2 (d+1)^4 log (2B)), uniformly for dimensions at most d.

theorem TrilinearHT.Auto.rational_spanning_subfamily {m n : ℕ} (v : Fin m → Fin n → ℚ) : ∃ (r : ℕ) (_ : r ≤ n) (e : Fin r ↪ Fin m), (LinearIndependent ℚ fun (i : Fin r) => v (e i)) ∧ Submodule.span ℚ (Set.range fun (i : Fin r) => v (e i)) = Submodule.span ℚ (Set.range v)

Select a basis from a finite rational spanning list. Its size is bounded by the ambient dimension, independently of the length of the list.

theorem TrilinearHT.Auto.rational_pivot_minor {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) : ∃ (r : ℕ) (_ : r ≤ m) (_ : r ≤ n) (rows : Fin r ↪ Fin m) (cols : Fin r ↪ Fin n), (A.submatrix ⇑rows ⇑cols).det ≠ 0 ∧ Submodule.span ℚ (Set.range fun (j : Fin r) => A.col (cols j)) = Submodule.span ℚ (Set.range A.col)

A full-rank square minor obtained by selecting independent columns and then independent rows. Its columns span the complete matrix range.

noncomputable def TrilinearHT.Auto.rationalMatrixZeroExtend {r s m n : ℕ} (rows : Fin r ↪ Fin m) (cols : Fin s ↪ Fin n) (M : Matrix (Fin r) (Fin s) ℚ) : Matrix (Fin m) (Fin n) ℚ

Place a small matrix in specified rows and columns, with zero entries outside them. This is the pivot solution with all other coordinates zero.

Equations

• TrilinearHT.Auto.rationalMatrixZeroExtend rows cols M = Function.extend (⇑rows) (fun (i : Fin r) => Function.extend (⇑cols) (M i) 0) 0

theorem TrilinearHT.Auto.rationalMatrixZeroExtend_apply {r s m n : ℕ} (rows : Fin r ↪ Fin m) (cols : Fin s ↪ Fin n) (M : Matrix (Fin r) (Fin s) ℚ) (i : Fin r) (j : Fin s) : rationalMatrixZeroExtend rows cols M (rows i) (cols j) = M i j

theorem TrilinearHT.Auto.rationalMatrixZeroExtend_entry {r s m n : ℕ} (rows : Fin r ↪ Fin m) (cols : Fin s ↪ Fin n) (M : Matrix (Fin r) (Fin s) ℚ) (i : Fin m) (j : Fin n) : rationalMatrixZeroExtend rows cols M i j = 0 ∨ ∃ (k : Fin r) (l : Fin s), rationalMatrixZeroExtend rows cols M i j = M k l

theorem TrilinearHT.Auto.rational_mulVec_extend {r m n : ℕ} (cols : Fin r ↪ Fin n) (A : Matrix (Fin m) (Fin n) ℚ) (v : Fin r → ℚ) : A.mulVec (Function.extend (⇑cols) v 0) = (A.submatrix id ⇑cols).mulVec v

theorem TrilinearHT.Auto.rationalMatrixZeroExtend_mulVec {r s m n : ℕ} (rows : Fin r ↪ Fin m) (cols : Fin s ↪ Fin n) (M : Matrix (Fin r) (Fin s) ℚ) (v : Fin n → ℚ) : (rationalMatrixZeroExtend rows cols M).mulVec v = Function.extend (⇑rows) (M.mulVec (v ∘ ⇑cols)) 0

theorem TrilinearHT.Auto.rational_pivot_rightInverse {m n r : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) (rows : Fin r ↪ Fin m) (cols : Fin r ↪ Fin n) (hdet : (A.submatrix ⇑rows ⇑cols).det ≠ 0) (hspan : Submodule.span ℚ (Set.range fun (j : Fin r) => A.col (cols j)) = Submodule.span ℚ (Set.range A.col)) (y : Fin m → ℚ) : y ∈ A.mulVecLin.range → A.mulVec ((rationalMatrixZeroExtend cols rows (A.submatrix ⇑rows ⇑cols)⁻¹).mulVec y) = y

Solving the pivot subsystem and setting nonpivot coordinates to zero gives a right inverse on the full range, as in lem:rational-linear.

noncomputable def TrilinearHT.Auto.realMatrixOperator {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)

The real Euclidean operator attached to a possibly rectangular matrix.

Equations

• TrilinearHT.Auto.realMatrixOperator A = LinearMap.toContinuousLinearMap (Matrix.toEuclideanLin A)

theorem TrilinearHT.Auto.realMatrixOperator_norm_le {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) {K : ℝ} (hK : 0 ≤ K) (hA : ∀ (i : Fin m) (j : Fin n), |A i j| ≤ K) : ‖realMatrixOperator A‖ ≤ ↑m * ↑n * K

theorem TrilinearHT.Auto.dimension_sq_le_rational_budget (d : ℕ) {B : ℝ} (hB : 2 ≤ B) : ↑d ^ 2 ≤ Real.exp (2 * (↑d + 1) ^ 4 * Real.log (2 * B))

theorem TrilinearHT.Auto.rationalMatrix_rightInverse_bounds {m n d : ℕ} (hm : m ≤ d) (hn : n ≤ d) {B : ℝ} (hB : 2 ≤ B) (A : Matrix (Fin m) (Fin n) ℚ) (hA : ∀ (i : Fin m) (j : Fin n), ↑(rationalHeight (A i j)) ≤ B) : ∃ (U : Matrix (Fin n) (Fin m) ℚ), (∀ y ∈ A.mulVecLin.range, A.mulVec (U.mulVec y) = y) ∧ (∀ (i : Fin n) (j : Fin m), ↑(rationalHeight (U i j)) ≤ Real.exp (4 * (↑d + 1) ^ 4 * Real.log (2 * B))) ∧ ‖realMatrixOperator (U.map fun (q : ℚ) => ↑q)‖ ≤ Real.exp (4 * (↑d + 1) ^ 4 * Real.log (2 * B))

Blueprint lem:rational-linear: every rational matrix has a rational right inverse on its range, with uniformly bounded height and Euclidean operator norm. The construction uses a pivot minor and zero coordinates.

theorem TrilinearHT.Auto.height_le_rational_budget (d : ℕ) {B : ℝ} (hB : 2 ≤ B) : B ≤ Real.exp (2 * (↑d + 1) ^ 4 * Real.log (2 * B))

theorem TrilinearHT.Auto.rational_gram_det_ne_zero {r n : ℕ} (S : Matrix (Fin r) (Fin n) ℚ) (hS : LinearIndependent ℚ S.row) : (S * S.transpose).det ≠ 0

theorem TrilinearHT.Auto.realMatrixOperator_apply {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (x : EuclideanSpace ℝ (Fin n)) : ((realMatrixOperator A) x).ofLp = A.mulVec x.ofLp

theorem TrilinearHT.Auto.realMatrixOperator_mul_apply {l m n : ℕ} (A : Matrix (Fin l) (Fin m) ℝ) (B : Matrix (Fin m) (Fin n) ℝ) (x : EuclideanSpace ℝ (Fin n)) : (realMatrixOperator (A * B)) x = (realMatrixOperator A) ((realMatrixOperator B) x)

theorem TrilinearHT.Auto.realMatrixOperator_transpose_inner {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (x : EuclideanSpace ℝ (Fin n)) (y : EuclideanSpace ℝ (Fin m)) : inner ℝ ((realMatrixOperator A) x) y = inner ℝ x ((realMatrixOperator A.transpose) y)

theorem TrilinearHT.Auto.real_gram_projection {r n : ℕ} (S : Matrix (Fin r) (Fin n) ℝ) (hS : (S * S.transpose).det ≠ 0) : realMatrixOperator (S.transpose * (S * S.transpose)⁻¹ * S) = (↑(realMatrixOperator S.transpose)).range.starProjection

The Gram inverse formula is the actual orthogonal projection onto the row space, not merely an idempotent with the same rational dimension.

noncomputable def TrilinearHT.Auto.rationalRowProjection {r n : ℕ} (S : Matrix (Fin r) (Fin n) ℚ) : Matrix (Fin n) (Fin n) ℚ

The rational matrix in the Gram formula for the orthogonal row-space projection of lem:rational-linear.

Equations

• TrilinearHT.Auto.rationalRowProjection S = S.transpose * (S * S.transpose)⁻¹ * S

theorem TrilinearHT.Auto.rationalMatrix_cast_inv {n : ℕ} (A : Matrix (Fin n) (Fin n) ℚ) (hA : A.det ≠ 0) : (A⁻¹.map fun (q : ℚ) => ↑q) = (A.map fun (q : ℚ) => ↑q)⁻¹

theorem TrilinearHT.Auto.rationalRowProjection_eq_starProjection {r n : ℕ} (S : Matrix (Fin r) (Fin n) ℚ) (hS : LinearIndependent ℚ S.row) : realMatrixOperator ((rationalRowProjection S).map fun (q : ℚ) => ↑q) = (↑(realMatrixOperator (S.transpose.map fun (q : ℚ) => ↑q))).range.starProjection

The rational Gram formula agrees, after real scalar extension, with Mathlib's orthogonal projection onto the real row space.

theorem TrilinearHT.Auto.rationalRowProjection_smul {r n : ℕ} (S : Matrix (Fin r) (Fin n) ℚ) (hS : (S * S.transpose).det ≠ 0) {c : ℚ} (hc : c ≠ 0) : rationalRowProjection (c • S) = rationalRowProjection S

theorem TrilinearHT.Auto.integerMatrix_mul_bound {m n p K L : ℕ} (A : Matrix (Fin m) (Fin n) ℤ) (B : Matrix (Fin n) (Fin p) ℤ) (hA : ∀ (i : Fin m) (j : Fin n), (A i j).natAbs ≤ K) (hB : ∀ (i : Fin n) (j : Fin p), (B i j).natAbs ≤ L) (i : Fin m) (j : Fin p) : ((A * B) i j).natAbs ≤ n * K * L

theorem TrilinearHT.Auto.integerRowProjection_fraction {r n : ℕ} (Z : Matrix (Fin r) (Fin n) ℤ) (i j : Fin n) : rationalRowProjection (Z.map fun (z : ℤ) => ↑z) i j = ↑((Z.transpose * (Z * Z.transpose).adjugate * Z) i j) / ↑(Z * Z.transpose).det

A single integer numerator and denominator represent every entry of the projection associated with an integer matrix.

theorem TrilinearHT.Auto.integerRowProjection_height {r n K : ℕ} (hK : 1 ≤ K) (Z : Matrix (Fin r) (Fin n) ℤ) (hZ : ∀ (i : Fin r) (j : Fin n), (Z i j).natAbs ≤ K) (hdet : (Z * Z.transpose).det ≠ 0) (i j : Fin n) : rationalHeight (rationalRowProjection (Z.map fun (z : ℤ) => ↑z) i j) ≤ (r + 1) ^ 2 * K ^ 2 * (r.factorial * ((n + 1) * K ^ 2) ^ r)

The common integer denominator and numerator of the Gram projection have a bound that does not multiply unrelated rational entry heights.

theorem TrilinearHT.Auto.rationalRectangularMatrix_clear_denominators {r n B : ℕ} (S : Matrix (Fin r) (Fin n) ℚ) (hS : ∀ (i : Fin r) (j : Fin n), rationalHeight (S i j) ≤ B) : ∃ (D : ℕ) (Z : Matrix (Fin r) (Fin n) ℤ), 0 < D ∧ D ≤ B ^ (r * n) ∧ (Z.map fun (z : ℤ) => ↑z) = ↑D • S ∧ ∀ (i : Fin r) (j : Fin n), (Z i j).natAbs ≤ B ^ (r * n + 1)

theorem TrilinearHT.Auto.rationalRowProjection_height_raw {r n B : ℕ} (hB : 1 ≤ B) (S : Matrix (Fin r) (Fin n) ℚ) (hS : ∀ (i : Fin r) (j : Fin n), rationalHeight (S i j) ≤ B) (hlin : LinearIndependent ℚ S.row) (i j : Fin n) : rationalHeight (rationalRowProjection S i j) ≤ (r + 1) ^ 2 * (B ^ (r * n + 1)) ^ 2 * (r.factorial * ((n + 1) * (B ^ (r * n + 1)) ^ 2) ^ r)

The shared-denominator height estimate for a rational Gram projection, before converting its explicit polynomial powers to the source budget.

theorem TrilinearHT.Auto.rational_projection_budget {r n d B : ℕ} (hr : r ≤ d) (hn : n ≤ d) (hB : 1 ≤ B) : (r + 1) ^ 2 * (B ^ (r * n + 1)) ^ 2 * (r.factorial * ((n + 1) * (B ^ (r * n + 1)) ^ 2) ^ r) ≤ (2 * B) ^ (4 * (d + 1) ^ 4)

theorem TrilinearHT.Auto.rationalRowProjection_bounds {r n d : ℕ} (hr : r ≤ d) (hn : n ≤ d) {B : ℝ} (hB : 2 ≤ B) (S : Matrix (Fin r) (Fin n) ℚ) (hS : ∀ (i : Fin r) (j : Fin n), ↑(rationalHeight (S i j)) ≤ B) (hlin : LinearIndependent ℚ S.row) : (∀ (i j : Fin n), ↑(rationalHeight (rationalRowProjection S i j)) ≤ Real.exp (4 * (↑d + 1) ^ 4 * Real.log (2 * B))) ∧ ‖realMatrixOperator ((rationalRowProjection S).map fun (q : ℚ) => ↑q)‖ ≤ 1

Blueprint lem:rational-linear: the rational row-space projection has the stated exponential height bound and Euclidean operator norm at most one.

noncomputable def TrilinearHT.Auto.rationalRealRowSpace {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) : Submodule ℝ (EuclideanSpace ℝ (Fin n))

Real row space of a rational matrix, in Euclidean coordinates.

Equations

• TrilinearHT.Auto.rationalRealRowSpace A = (↑(TrilinearHT.Auto.realMatrixOperator (A.transpose.map fun (q : ℚ) => ↑q))).range

theorem TrilinearHT.Auto.rational_rowSpan_factor {m r n : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) (S : Matrix (Fin r) (Fin n) ℚ) (hspan : Submodule.span ℚ (Set.range A.row) ≤ Submodule.span ℚ (Set.range S.row)) : ∃ (F : Matrix (Fin m) (Fin r) ℚ), A = F * S

theorem TrilinearHT.Auto.rationalRealRowSpace_mono {m r n : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) (S : Matrix (Fin r) (Fin n) ℚ) (hspan : Submodule.span ℚ (Set.range A.row) ≤ Submodule.span ℚ (Set.range S.row)) : rationalRealRowSpace A ≤ rationalRealRowSpace S

theorem TrilinearHT.Auto.rationalRealRowSpace_eq {m r n : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) (S : Matrix (Fin r) (Fin n) ℚ) (hspan : Submodule.span ℚ (Set.range A.row) = Submodule.span ℚ (Set.range S.row)) : rationalRealRowSpace A = rationalRealRowSpace S

theorem TrilinearHT.Auto.rationalHeight_one_sub (q : ℚ) : rationalHeight (1 - q) ≤ 2 * rationalHeight q

theorem TrilinearHT.Auto.rationalHeight_neg (q : ℚ) : rationalHeight (-q) = rationalHeight q

theorem TrilinearHT.Auto.rationalMatrix_complement_height {n : ℕ} (P : Matrix (Fin n) (Fin n) ℚ) (i j : Fin n) : rationalHeight ((1 - P) i j) ≤ 2 * rationalHeight (P i j)

theorem TrilinearHT.Auto.realMatrixOperator_sub {m n : ℕ} (A B : Matrix (Fin m) (Fin n) ℝ) : realMatrixOperator (A - B) = realMatrixOperator A - realMatrixOperator B

theorem TrilinearHT.Auto.realMatrixOperator_one (n : ℕ) : realMatrixOperator 1 = ContinuousLinearMap.id ℝ (EuclideanSpace ℝ (Fin n))

theorem TrilinearHT.Auto.rationalMatrix_projection_bounds {m n d : ℕ} (hn : n ≤ d) {B : ℝ} (hB : 2 ≤ B) (A : Matrix (Fin m) (Fin n) ℚ) (hA : ∀ (i : Fin m) (j : Fin n), ↑(rationalHeight (A i j)) ≤ B) : ∃ (P : Matrix (Fin n) (Fin n) ℚ), realMatrixOperator (P.map fun (q : ℚ) => ↑q) = (rationalRealRowSpace A).starProjection ∧ realMatrixOperator ((1 - P).map fun (q : ℚ) => ↑q) = (rationalRealRowSpace A)ᗮ.starProjection ∧ (∀ (i j : Fin n), ↑(rationalHeight (P i j)) ≤ Real.exp (8 * (↑d + 1) ^ 4 * Real.log (2 * B))) ∧ (∀ (i j : Fin n), ↑(rationalHeight ((1 - P) i j)) ≤ Real.exp (8 * (↑d + 1) ^ 4 * Real.log (2 * B))) ∧ ‖realMatrixOperator (P.map fun (q : ℚ) => ↑q)‖ ≤ 1 ∧ ‖realMatrixOperator ((1 - P).map fun (q : ℚ) => ↑q)‖ ≤ 1

Blueprint lem:rational-linear, lines 418–420: arbitrary rational equations determine rational orthogonal projections onto their real row space and its orthogonal complement. Both have height at most exp (8 (d+1)^4 log (2B)) and operator norm at most one.

theorem TrilinearHT.Auto.rational_clear_denominators_sharp {ι : Type u_1} [Fintype ι] (a : ι → ℚ) {B : ℕ} (ha : ∀ (i : ι), rationalHeight (a i) ≤ B) : ∃ (z : ι → ℤ), ∀ (i : ι), ↑(z i) = ↑(rationalCommonDenominator a) * a i ∧ (z i).natAbs ≤ B ^ Fintype.card ι

Blueprint lem:height, proof line 617: clearing one vector's denominators gives integer entries bounded by B^d, where d is the number of coordinates. The coordinate's own denominator is canceled before estimating the product of the remaining denominators.

theorem TrilinearHT.Auto.integerMatrix_cramer_bound {n K : ℕ} (Z : Matrix (Fin n) (Fin n) ℤ) (b : Fin n → ℤ) (hZ : ∀ (i j : Fin n), (Z i j).natAbs ≤ K) (hb : ∀ (i : Fin n), (b i).natAbs ≤ K) (j : Fin n) : (Z.cramer b j).natAbs ≤ n.factorial * K ^ n

Replacement determinants give the sharp Cramer numerator bound needed in the circuit argument of lem:height, proof line 617.

theorem TrilinearHT.Auto.integerMatrix_cramer_cast {n : ℕ} (Z : Matrix (Fin n) (Fin n) ℤ) (b : Fin n → ℤ) (i : Fin n) : ↑(Z.cramer b i) = ((Int.castRingHom ℚ).mapMatrix Z).cramer (fun (j : Fin n) => ↑(b j)) i

theorem TrilinearHT.Auto.rational_pivot_minor_of_dependent {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) (hdep : ¬LinearIndependent ℚ A.col) : ∃ (r : ℕ) (_ : r ≤ m) (_ : r < n) (rows : Fin r ↪ Fin m) (cols : Fin r ↪ Fin n), (A.submatrix ⇑rows ⇑cols).det ≠ 0 ∧ Submodule.span ℚ (Set.range fun (j : Fin r) => A.col (cols j)) = Submodule.span ℚ (Set.range A.col)

A dependent column family has a proper nonsingular pivot minor, so at least one column remains available for the Cramer dependence.

theorem TrilinearHT.Auto.rational_pivot_cramer {m n r : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) (rows : Fin r ↪ Fin m) (cols : Fin r ↪ Fin n) (hdet : (A.submatrix ⇑rows ⇑cols).det ≠ 0) (hspan : Submodule.span ℚ (Set.range fun (j : Fin r) => A.col (cols j)) = Submodule.span ℚ (Set.range A.col)) (j : Fin n) : (A.submatrix id ⇑cols).mulVec ((A.submatrix ⇑rows ⇑cols).cramer (A.col j ∘ ⇑rows)) = (A.submatrix ⇑rows ⇑cols).det • A.col j

Cramer numerators for a pivot minor reproduce any column after embedding back into the full row space.

theorem TrilinearHT.Auto.integerMatrix_small_kernel {m n K : ℕ} (A : Matrix (Fin m) (Fin n) ℤ) (hK : 1 ≤ K) (hA : ∀ (i : Fin m) (j : Fin n), (A i j).natAbs ≤ K) (hdep : ¬LinearIndependent ℚ (A.map fun (z : ℤ) => ↑z).col) : ∃ (c : Fin n → ℤ), c ≠ 0 ∧ A.mulVec c = 0 ∧ ∀ (i : Fin n), (c i).natAbs ≤ m.factorial * K ^ m

An integer matrix with dependent columns has a nonzero integral kernel vector with the determinant bound, independent of the number of columns.

theorem TrilinearHT.Auto.rational_small_dependence {d n B : ℕ} (v : Fin n → Fin d → ℚ) (hB : 1 ≤ B) (hv : ∀ (i : Fin n) (j : Fin d), rationalHeight (v i j) ≤ B) (hdep : ¬LinearIndependent ℚ v) : ∃ (c : Fin n → ℤ), c ≠ 0 ∧ ∑ i : Fin n, ↑(c i) • v i = 0 ∧ ∀ (i : Fin n), (c i).natAbs ≤ d.factorial * B ^ (d ^ 2 + d)

Every dependent bounded-height rational family has an integral relation with the sharp coefficient budget from lem:height.

theorem TrilinearHT.Auto.separated_integer_sum_ne_zero {n H : ℕ} {R : ℝ} (hR : ↑n * ↑H < R) (x : Fin n → ℝ) (hx : ∀ (i : Fin n), x i ≠ 0) (hsep : ∀ (i j : Fin n), i < j → R * |x i| ≤ |x j|) (c : Fin n → ℤ) (hc : c ≠ 0) (hbound : ∀ (i : Fin n), (c i).natAbs ≤ H) : ∑ i : Fin n, ↑(c i) * x i ≠ 0

The largest nonzero term prevents cancellation in an integral linear combination of sufficiently separated real magnitudes.

noncomputable def TrilinearHT.Auto.rationalHeightRatio (d B : ℕ) : ℝ

The geometric separation ratio in the height-bin argument.

Equations

• TrilinearHT.Auto.rationalHeightRatio d B = 4 * ↑d * ↑(d.factorial * B ^ (d ^ 2 + d))

theorem TrilinearHT.Auto.rational_separated_independent_of_card {d n B : ℕ} (hd : 0 < d) (hn : n ≤ d + 1) (hB : 1 ≤ B) (v : Fin n → Fin d → ℚ) (hv : ∀ (i : Fin n) (j : Fin d), rationalHeight (v i j) ≤ B) (L : (Fin d → ℚ) →ₗ[ℚ] ℝ) (hx : ∀ (i : Fin n), L (v i) ≠ 0) (hsep : ∀ (i j : Fin n), i < j → rationalHeightRatio d B * |L (v i)| ≤ |L (v j)|) : LinearIndependent ℚ v

theorem TrilinearHT.Auto.rational_separated_independent_of_pos {d n B : ℕ} (hd : 0 < d) (hB : 1 ≤ B) (v : Fin n → Fin d → ℚ) (hv : ∀ (i : Fin n) (j : Fin d), rationalHeight (v i j) ≤ B) (L : (Fin d → ℚ) →ₗ[ℚ] ℝ) (hx : ∀ (i : Fin n), L (v i) ≠ 0) (hsep : ∀ (i j : Fin n), i < j → rationalHeightRatio d B * |L (v i)| ≤ |L (v j)|) : LinearIndependent ℚ v

Blueprint lem:height, proof line 617: bounded-height rational vectors with geometrically separated nonzero evaluations are independent.

theorem TrilinearHT.Auto.rational_separated_independent {d n B : ℕ} (hB : 1 ≤ B) (v : Fin n → Fin d → ℚ) (hv : ∀ (i : Fin n) (j : Fin d), rationalHeight (v i j) ≤ B) (L : (Fin d → ℚ) →ₗ[ℚ] ℝ) (hx : ∀ (i : Fin n), L (v i) ≠ 0) (hsep : ∀ (i j : Fin n), i < j → rationalHeightRatio d B * |L (v i)| ≤ |L (v j)|) : LinearIndependent ℚ v

The same independence statement includes the empty, zero-dimensional case.

noncomputable def TrilinearHT.Auto.rationalEvaluation {d : ℕ} (ξ : Fin d → ℝ) : (Fin d → ℚ) →ₗ[ℚ] ℝ

Evaluation of rational vectors against a real frequency.

Equations

• TrilinearHT.Auto.rationalEvaluation ξ = { toFun := fun (v : Fin d → ℚ) => ∑ j : Fin d, ↑(v j) * ξ j, map_add' := ⋯, map_smul' := ⋯ }

theorem TrilinearHT.Auto.finite_positive_geometric_cover (s : Finset ℝ) {R : ℝ} (hR : 1 ≤ R) (hs : ∀ x ∈ s, 0 < x) : ∃ t ⊆ s, (∀ x ∈ s, ∃ a ∈ t, a ≤ x ∧ x ≤ R * a) ∧ ∀ a ∈ t, ∀ b ∈ t, a < b → R * a < b

Greedily covering a finite positive set by multiplicative intervals produces centers that are separated by more than the interval ratio.

theorem TrilinearHT.Auto.rational_geometric_cover {d B : ℕ} (hB : 1 ≤ B) (L : (Fin d → ℚ) →ₗ[ℚ] ℝ) (s : Finset ℝ) (hs : ∀ x ∈ s, 0 < x) (hrepr : ∀ x ∈ s, ∃ (v : Fin d → ℚ), (∀ (j : Fin d), rationalHeight (v j) ≤ B) ∧ |L v| = x) {R : ℝ} (hR : 1 ≤ R) (hlarge : rationalHeightRatio d B ≤ R) : ∃ t ⊆ s, t.card ≤ d ∧ ∀ x ∈ s, ∃ a ∈ t, a ≤ x ∧ x ≤ R * a

A finite positive set of bounded-height evaluations is covered by at most d multiplicative intervals.

noncomputable def TrilinearHT.Auto.boundedRationalVectors (d B : ℕ) : Finset (Fin d → ℚ)

A finite enumeration of precisely the rational vectors of bounded height.

Equations

• TrilinearHT.Auto.boundedRationalVectors d B = {v ∈ Fintype.piFinset fun (x : Fin d) => TrilinearHT.Auto.boundedRationalEnumeration B | ∀ (j : Fin d), TrilinearHT.Auto.rationalHeight (v j) ≤ B}

theorem TrilinearHT.Auto.mem_boundedRationalVectors {d B : ℕ} {v : Fin d → ℚ} : v ∈ boundedRationalVectors d B ↔ ∀ (j : Fin d), rationalHeight (v j) ≤ B

noncomputable def TrilinearHT.Auto.boundedRationalMagnitudes {d : ℕ} (B : ℕ) (L : (Fin d → ℚ) →ₗ[ℚ] ℝ) : Finset ℝ

The nonzero evaluation magnitudes of all bounded-height vectors.

Equations

• TrilinearHT.Auto.boundedRationalMagnitudes B L = (Finset.image (fun (v : Fin d → ℚ) => |L v|) (TrilinearHT.Auto.boundedRationalVectors d B)).erase 0

theorem TrilinearHT.Auto.mem_boundedRationalMagnitudes {d B : ℕ} {L : (Fin d → ℚ) →ₗ[ℚ] ℝ} {x : ℝ} : x ∈ boundedRationalMagnitudes B L ↔ 0 < x ∧ ∃ (v : Fin d → ℚ), (∀ (j : Fin d), rationalHeight (v j) ≤ B) ∧ |L v| = x

theorem TrilinearHT.Auto.rationalHeightRatio_log_bound (d : ℕ) {B : ℕ} (hB : 2 ≤ B) : Real.log (max 1 (rationalHeightRatio d B)) ≤ 8 * (↑d + 1) ^ 3 * Real.log (2 * ↑B)

theorem TrilinearHT.Auto.rational_logarithmic_cover_nat {d B : ℕ} (hB : 2 ≤ B) (L : (Fin d → ℚ) →ₗ[ℚ] ℝ) : ∃ (t : Finset ℝ), t.card ≤ d ∧ ∀ (v : Fin d → ℚ), (∀ (j : Fin d), rationalHeight (v j) ≤ B) → L v ≠ 0 → ∃ a ∈ t, Real.log |L v| ∈ Set.Icc a (a + 8 * (↑d + 1) ^ 3 * Real.log (2 * ↑B))

Blueprint lem:height, lines 603 and 617: the logarithms of all nonzero bounded-height evaluations lie in at most d intervals, each of length 8 (d+1)^3 log(2B).

theorem TrilinearHT.Auto.rational_logarithmic_cover {d : ℕ} {B : ℝ} (hB : 2 ≤ B) (L : (Fin d → ℚ) →ₗ[ℚ] ℝ) : ∃ (t : Finset ℝ), t.card ≤ d ∧ ∀ (v : Fin d → ℚ), (∀ (j : Fin d), ↑(rationalHeight (v j)) ≤ B) → L v ≠ 0 → ∃ a ∈ t, Real.log |L v| ∈ Set.Icc a (a + 8 * (↑d + 1) ^ 3 * Real.log (2 * B))

Real-valued height budgets are handled by their natural floor, without enlarging either the dimension or the logarithmic width.

theorem TrilinearHT.Auto.rational_frequency_logarithmic_cover {d : ℕ} {B : ℝ} (hB : 2 ≤ B) (ξ : Fin d → ℝ) : ∃ (t : Finset ℝ), t.card ≤ d ∧ ∀ (v : Fin d → ℚ), (∀ (j : Fin d), ↑(rationalHeight (v j)) ≤ B) → ∑ j : Fin d, ↑(v j) * ξ j ≠ 0 → ∃ a ∈ t, Real.log |∑ j : Fin d, ↑(v j) * ξ j| ∈ Set.Icc a (a + 8 * (↑d + 1) ^ 3 * Real.log (2 * B))

The logarithmic cover for the source's dot-product frequencies.

theorem TrilinearHT.Auto.integer_floor_interval_card_le {a b : ℝ} (hab : a ≤ b) : ↑(Finset.Icc ⌊a⌋ ⌊b⌋).card ≤ b - a + 2

Rounding the endpoints of a real interval costs fewer than two additional integer positions.

noncomputable def TrilinearHT.Auto.logarithmicMagnitudeBins (s : Finset ℝ) (δ : ℝ) : Finset ℤ

Bins of fixed logarithmic width occupied by a finite magnitude set.

Equations

• TrilinearHT.Auto.logarithmicMagnitudeBins s δ = Finset.image (fun (x : ℝ) => ⌊Real.log x / δ⌋) s

theorem TrilinearHT.Auto.logarithmicMagnitudeBins_card_le (s t : Finset ℝ) {δ W : ℝ} (hδ : 0 < δ) (hW : 0 ≤ W) (hcover : ∀ x ∈ s, ∃ a ∈ t, Real.log x ∈ Set.Icc a (a + W)) : ↑(logarithmicMagnitudeBins s δ).card ≤ ↑t.card * (W / δ + 2)

theorem TrilinearHT.Auto.dyadicMagnitudeBin_spec {x : ℝ} (hx : 0 < x) : 2 ^ ⌊Real.log x / Real.log 2⌋ ≤ x ∧ x < 2 ^ (⌊Real.log x / Real.log 2⌋ + 1)

The logarithmic bin index agrees with the usual half-open dyadic magnitude interval.

theorem TrilinearHT.Auto.height_log_one_le {B : ℝ} (hB : 2 ≤ B) : 1 ≤ Real.log (2 * B)

theorem TrilinearHT.Auto.rational_magnitude_bins_card_le {d : ℕ} {B : ℝ} (hB : 2 ≤ B) (L : (Fin d → ℚ) →ₗ[ℚ] ℝ) (s : Finset ℝ) (hs : ∀ x ∈ s, 0 < x) (hrepr : ∀ x ∈ s, ∃ (v : Fin d → ℚ), (∀ (j : Fin d), ↑(rationalHeight (v j)) ≤ B) ∧ |L v| = x) : ↑(logarithmicMagnitudeBins s (Real.log 2)).card ≤ 32 * (↑d + 1) ^ 4 * Real.log (2 * B)

Any finite set of bounded-height evaluation magnitudes occupies at most the source's polynomial-logarithmic number of dyadic bins.

noncomputable def TrilinearHT.Auto.rationalMagnitudeBins {d : ℕ} (B : ℝ) (L : (Fin d → ℚ) →ₗ[ℚ] ℝ) : Finset ℤ

The exact finite set of dyadic bins occupied by nonzero rational evaluations with real height budget B.

Equations

• TrilinearHT.Auto.rationalMagnitudeBins B L = TrilinearHT.Auto.logarithmicMagnitudeBins (TrilinearHT.Auto.boundedRationalMagnitudes ⌊B⌋₊ L) (Real.log 2)

theorem TrilinearHT.Auto.rationalMagnitudeBins_card_le {d : ℕ} {B : ℝ} (hB : 2 ≤ B) (L : (Fin d → ℚ) →ₗ[ℚ] ℝ) : ↑(rationalMagnitudeBins B L).card ≤ 32 * (↑d + 1) ^ 4 * Real.log (2 * B)

Blueprint lem:height, line 603: all bounded-height frequencies occupy at most 32 (d+1)^4 log(2B) dyadic magnitude bins.

theorem TrilinearHT.Auto.finite_logarithmic_scale_count (s t : Finset ℝ) {δ W A B : ℝ} (hδ : 0 < δ) (hW : 0 ≤ W) (hAB : A ≤ B) (v : ℝ) (hcover : ∀ x ∈ s, ∃ a ∈ t, Real.log x ∈ Set.Icc a (a + W)) : ∃ (N : Finset ℤ), (∀ (n : ℤ), n ∈ N ↔ ∃ x ∈ s, A ≤ Real.log x + v - δ * ↑n ∧ Real.log x + v - δ * ↑n ≤ B) ∧ ↑N.card ≤ ↑t.card * ((W + B - A) / δ + 2)

Translating logarithmic intervals along an integer grid gives a finite set of crossing scales with a uniform count.

theorem TrilinearHT.Auto.rational_logarithmic_scale_count {d : ℕ} {B : ℝ} (hB : 2 ≤ B) (L : (Fin d → ℚ) →ₗ[ℚ] ℝ) {δ : ℝ} (hδ : Real.log 2 ≤ δ) (v p q : ℝ) (hpq : p ≤ q) : ∃ (N : Finset ℤ), (∀ (n : ℤ), n ∈ N ↔ ∃ (a : Fin d → ℚ), (∀ (j : Fin d), ↑(rationalHeight (a j)) ≤ B) ∧ L a ≠ 0 ∧ p ≤ Real.log |L a| + v - δ * ↑n ∧ Real.log |L a| + v - δ * ↑n ≤ q) ∧ ↑N.card ≤ 32 * (↑d + 1) ^ 4 * (Real.log (2 * B) + q - p)

Uniform translated-scale count for bounded-height evaluations in logarithmic coordinates; the grid spacing may be any value at least log 2.

theorem TrilinearHT.Auto.rational_dyadic_scale_count {d u : ℕ} {B α β : ℝ} (hB : 2 ≤ B) (hu : 1 ≤ u) (hα : 0 < α) (hαβ : α ≤ β) (L : (Fin d → ℚ) →ₗ[ℚ] ℝ) (c : ℝ) : ∃ (N : Finset ℤ), (∀ (n : ℤ), n ∈ N ↔ ∃ (a : Fin d → ℚ), (∀ (j : Fin d), ↑(rationalHeight (a j)) ≤ B) ∧ α ≤ c * (2 ^ (-n)) ^ u * |L a| ∧ c * (2 ^ (-n)) ^ u * |L a| ≤ β) ∧ ↑N.card ≤ 32 * (↑d + 1) ^ 4 * (Real.log (2 * B) + Real.log (2 * β / α))

The translated dyadic scale count, uniform in the scale multiplier and valid for every positive integral dilation exponent.

theorem TrilinearHT.Auto.rational_frequency_scale_count {d u : ℕ} {B α β : ℝ} (hB : 2 ≤ B) (hu : 1 ≤ u) (hα : 0 < α) (hαβ : α ≤ β) (ξ : Fin d → ℝ) (r₀ : ℝ) : ∃ (N : Finset ℤ), (∀ (n : ℤ), n ∈ N ↔ ∃ (a : Fin d → ℚ), (∀ (j : Fin d), ↑(rationalHeight (a j)) ≤ B) ∧ α ≤ (r₀ * 2 ^ (-n)) ^ u * |∑ j : Fin d, ↑(a j) * ξ j| ∧ (r₀ * 2 ^ (-n)) ^ u * |∑ j : Fin d, ↑(a j) * ξ j| ≤ β) ∧ ↑N.card ≤ 32 * (↑d + 1) ^ 4 * (Real.log (2 * B) + Real.log (2 * β / α))

Blueprint lem:height, lines 603-607: the source scale formula r_n = r_0 2^(-n), for every positive integer exponent (in particular 1 and 2).

noncomputable def TrilinearHT.Auto.upperTruncatedMagnitude (ε x : ℝ) : ℝ

Keep a nonnegative magnitude only when it is below the specified threshold.

Equations

• TrilinearHT.Auto.upperTruncatedMagnitude ε x = if x ≤ ε then x else 0

theorem TrilinearHT.Auto.upperTruncatedMagnitude_nonneg (ε : ℝ) {x : ℝ} (hx : 0 ≤ x) : 0 ≤ upperTruncatedMagnitude ε x

theorem TrilinearHT.Auto.integer_geometric_truncated_sum_le (q : ℤ → ℝ) {ε : ℝ} (hε : 0 ≤ ε) (hdecay : ∀ (m n : ℤ), m ≤ n → q n ≤ q m * (1 / 2) ^ (n - m).toNat) (F : Finset ℤ) : ∑ n ∈ F, upperTruncatedMagnitude ε (q n) ≤ 2 * ε

A geometrically decreasing integer sequence contributes at most twice the cutoff threshold to every finite truncated sum.

noncomputable def TrilinearHT.Auto.dyadicMagnitudeProfile (c : ℝ) (u : ℕ) (n : ℤ) : ℝ

A dyadically decaying magnitude profile, indexed by every integer scale.

Equations

• TrilinearHT.Auto.dyadicMagnitudeProfile c u n = c * (2 ^ (-n)) ^ u

theorem TrilinearHT.Auto.dyadicMagnitudeProfile_nonneg {c : ℝ} (hc : 0 ≤ c) (u : ℕ) (n : ℤ) : 0 ≤ dyadicMagnitudeProfile c u n

theorem TrilinearHT.Auto.dyadicMagnitudeProfile_decay {c : ℝ} (hc : 0 ≤ c) {u : ℕ} (hu : 1 ≤ u) (m n : ℤ) (hmn : m ≤ n) : dyadicMagnitudeProfile c u n ≤ dyadicMagnitudeProfile c u m * (1 / 2) ^ (n - m).toNat

theorem TrilinearHT.Auto.dyadicMagnitudeProfile_truncated_sum_le {c ε : ℝ} (hc : 0 ≤ c) (hε : 0 ≤ ε) {u : ℕ} (hu : 1 ≤ u) (F : Finset ℤ) : ∑ n ∈ F, upperTruncatedMagnitude ε (dyadicMagnitudeProfile c u n) ≤ 2 * ε

noncomputable def TrilinearHT.Auto.finiteTinyMaximum (s : Finset ℝ) (w ε : ℝ) : ℝ

Maximum of the positive scaled magnitudes below ε, with the source convention that an empty maximum is zero.

Equations

• TrilinearHT.Auto.finiteTinyMaximum s w ε = (insert 0 ({y ∈ Finset.image (fun (x : ℝ) => w * x) s | 0 < y ∧ y ≤ ε})).max' ⋯

theorem TrilinearHT.Auto.finiteTinyMaximum_nonneg (s : Finset ℝ) (w ε : ℝ) : 0 ≤ finiteTinyMaximum s w ε

theorem TrilinearHT.Auto.finiteTinyMaximum_le (s : Finset ℝ) (w ε : ℝ) {M : ℝ} (hM : 0 ≤ M) (hs : ∀ x ∈ s, 0 < w * x → w * x ≤ ε → w * x ≤ M) : finiteTinyMaximum s w ε ≤ M

theorem TrilinearHT.Auto.finiteTinyMaximum_eq_zero_of_nonpos (s : Finset ℝ) (ε : ℝ) (hs : ∀ x ∈ s, 0 ≤ x) {w : ℝ} (hw : w ≤ 0) : finiteTinyMaximum s w ε = 0

theorem TrilinearHT.Auto.finiteTinyMaximum_le_bins (s : Finset ℝ) (hs : ∀ x ∈ s, 0 < x) {w : ℝ} (hw : 0 ≤ w) (ε : ℝ) : finiteTinyMaximum s w ε ≤ ∑ j ∈ logarithmicMagnitudeBins s (Real.log 2), 2 * upperTruncatedMagnitude ε (w * 2 ^ j)

In one occupied dyadic bin the small maximum is at most twice its lower endpoint, provided that endpoint is below the cutoff.

theorem TrilinearHT.Auto.finiteTinyMaximum_dyadic_sum_le (s : Finset ℝ) (hs : ∀ x ∈ s, 0 < x) (c : ℝ) {u : ℕ} (hu : 1 ≤ u) {ε : ℝ} (hε : 0 ≤ ε) (F : Finset ℤ) : ∑ n ∈ F, finiteTinyMaximum s (dyadicMagnitudeProfile c u n) ε ≤ 4 * ↑(logarithmicMagnitudeBins s (Real.log 2)).card * ε

theorem TrilinearHT.Auto.finiteTinyMaximum_dyadic_tsum_le (s : Finset ℝ) (hs : ∀ x ∈ s, 0 < x) (c : ℝ) {u : ℕ} (hu : 1 ≤ u) {ε : ℝ} (hε : 0 ≤ ε) : (Summable fun (n : ℤ) => finiteTinyMaximum s (dyadicMagnitudeProfile c u n) ε) ∧ ∑' (n : ℤ), finiteTinyMaximum s (dyadicMagnitudeProfile c u n) ε ≤ 4 * ↑(logarithmicMagnitudeBins s (Real.log 2)).card * ε

The tiny maxima are summable over all integer scales, with four times the cutoff threshold per occupied dyadic magnitude bin.

theorem TrilinearHT.Auto.le_finiteTinyMaximum {s : Finset ℝ} {w ε x : ℝ} (hx : x ∈ s) (hpos : 0 < w * x) (hsmall : w * x ≤ ε) : w * x ≤ finiteTinyMaximum s w ε

noncomputable def TrilinearHT.Auto.rationalTinyMaximum {d : ℕ} (B : ℝ) (L : (Fin d → ℚ) →ₗ[ℚ] ℝ) (c : ℝ) (u : ℕ) (ε : ℝ) (n : ℤ) : ℝ

The exact tiny maximum over all bounded-height rational evaluations.

Equations

• TrilinearHT.Auto.rationalTinyMaximum B L c u ε n = TrilinearHT.Auto.finiteTinyMaximum (TrilinearHT.Auto.boundedRationalMagnitudes ⌊B⌋₊ L) (TrilinearHT.Auto.dyadicMagnitudeProfile c u n) ε

theorem TrilinearHT.Auto.rationalTinyMaximum_tsum_le {d u : ℕ} {B ε : ℝ} (hB : 2 ≤ B) (hu : 1 ≤ u) (hε : 0 ≤ ε) (L : (Fin d → ℚ) →ₗ[ℚ] ℝ) (c : ℝ) : Summable (rationalTinyMaximum B L c u ε) ∧ ∑' (n : ℤ), rationalTinyMaximum B L c u ε n ≤ 128 * (↑d + 1) ^ 4 * Real.log (2 * B) * ε

Blueprint lem:height, tiny-sum formula, lines 608-614 and 617: the exact tiny maxima are summable and bounded by the occupied-bin count.

theorem TrilinearHT.Auto.rational_frequency_tiny_sum {d u : ℕ} {B ε : ℝ} (hB : 2 ≤ B) (hu : 1 ≤ u) (hε : 0 ≤ ε) (ξ : Fin d → ℝ) (r₀ : ℝ) : (Summable fun (n : ℤ) => finiteTinyMaximum (boundedRationalMagnitudes ⌊B⌋₊ (rationalEvaluation ξ)) ((r₀ * 2 ^ (-n)) ^ u) ε) ∧ ∑' (n : ℤ), finiteTinyMaximum (boundedRationalMagnitudes ⌊B⌋₊ (rationalEvaluation ξ)) ((r₀ * 2 ^ (-n)) ^ u) ε ≤ 128 * (↑d + 1) ^ 4 * Real.log (2 * B) * ε

The source tiny-sum estimate with r_n = r_0 2^(-n) and dot-product frequencies, including the empty-maximum convention and actual summability.

noncomputable def TrilinearHT.Auto.quadraticReturnFrequency {d k : ℕ} (C : Matrix (Fin d) (Fin d) ℝ) (V : Matrix (Fin d) (Fin k) ℝ) (Λ : Matrix (Fin k) (Fin k) ℝ) (h : Fin k → ℝ) (m : Fin d → ℝ) : Fin k → ℝ

Return frequency determined by the quadratic matrix, return directions and lattice offset.

Equations

• TrilinearHT.Auto.quadraticReturnFrequency C V Λ h m = (2 • Λ + V.transpose * C * V).mulVec h - (V.transpose * (C - C.transpose)).mulVec m

theorem TrilinearHT.Auto.realMatrixOperator_range {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) : (↑(realMatrixOperator A)).range = Submodule.span ℝ (Set.range fun (j : Fin n) => WithLp.toLp 2 (A.col j))

theorem TrilinearHT.Auto.rationalRealRowSpace_eq_span {m n : ℕ} (S : Matrix (Fin m) (Fin n) ℚ) : rationalRealRowSpace S = Submodule.span ℝ (Set.range fun (i : Fin m) => WithLp.toLp 2 fun (j : Fin n) => ↑(S i j))

theorem TrilinearHT.Auto.rationalHeight_intCast_bound (z : ℤ) {B : ℝ} (hB : 1 ≤ B) (hz : |↑z| ≤ B) : ↑(rationalHeight ↑z) ≤ B

theorem TrilinearHT.Auto.integer_span_projection_bounds {m n : ℕ} (Z : Matrix (Fin m) (Fin n) ℤ) {B : ℝ} (hB : 2 ≤ B) (hZ : ∀ (i : Fin m) (j : Fin n), |↑(Z i j)| ≤ B) : let U := Submodule.span ℝ (Set.range fun (i : Fin m) => WithLp.toLp 2 fun (j : Fin n) => ↑(Z i j)); ∃ (P : Matrix (Fin n) (Fin n) ℚ), realMatrixOperator (P.map fun (q : ℚ) => ↑q) = U.starProjection ∧ realMatrixOperator ((1 - P).map fun (q : ℚ) => ↑q) = Uᗮ.starProjection ∧ (∀ (i j : Fin n), ↑(rationalHeight (P i j)) ≤ Real.exp (8 * (↑n + 1) ^ 4 * Real.log (2 * B))) ∧ (∀ (i j : Fin n), ↑(rationalHeight ((1 - P) i j)) ≤ Real.exp (8 * (↑n + 1) ^ 4 * Real.log (2 * B))) ∧ ‖realMatrixOperator (P.map fun (q : ℚ) => ↑q)‖ ≤ 1 ∧ ‖realMatrixOperator ((1 - P).map fun (q : ℚ) => ↑q)‖ ≤ 1

A subspace generated by bounded integer vectors has rational orthogonal projections with a uniform height bound, independent of the list length.

theorem TrilinearHT.Auto.rational_rows_independent_of_real {r n : ℕ} (S : Matrix (Fin r) (Fin n) ℚ) (hS : LinearIndependent ℝ fun (i : Fin r) => WithLp.toLp 2 fun (j : Fin n) => ↑(S i j)) : LinearIndependent ℚ S.row

theorem TrilinearHT.Auto.realMatrixOperator_mul_norm_le {l m n : ℕ} (A : Matrix (Fin l) (Fin m) ℝ) (B : Matrix (Fin m) (Fin n) ℝ) : ‖realMatrixOperator (A * B)‖ ≤ ‖realMatrixOperator A‖ * ‖realMatrixOperator B‖

theorem TrilinearHT.Auto.real_matrix_mul_entry_bound {l m n : ℕ} (A : Matrix (Fin l) (Fin m) ℝ) (B : Matrix (Fin m) (Fin n) ℝ) {R S : ℝ} (hR : 0 ≤ R) (hA : ∀ (i : Fin l) (j : Fin m), |A i j| ≤ R) (hB : ∀ (i : Fin m) (j : Fin n), |B i j| ≤ S) (i : Fin l) (j : Fin n) : |(A * B) i j| ≤ ↑m * R * S

theorem TrilinearHT.Auto.rationalRowProjection_mul_norm_le {r n k : ℕ} (S : Matrix (Fin r) (Fin n) ℚ) (V : Matrix (Fin n) (Fin k) ℝ) (hlin : LinearIndependent ℚ S.row) {B G W : ℝ} (hB : 0 ≤ B) (hG : 2 ≤ G) (hW : 0 ≤ W) (hS : ∀ (i : Fin r) (j : Fin n), |↑(S i j)| ≤ B) (hGram : ∀ (i j : Fin r), ↑(rationalHeight ((S * S.transpose) i j)) ≤ G) (hSV : ∀ (i : Fin r) (j : Fin k), |((S.map fun (q : ℚ) => ↑q) * V) i j| ≤ W) : ‖realMatrixOperator (((rationalRowProjection S).map fun (q : ℚ) => ↑q) * V)‖ ≤ ↑n * ↑r * B * (↑r * ↑r * Real.exp (2 * (↑r + 1) ^ 4 * Real.log (2 * G)) * (↑r * ↑k * W))

theorem TrilinearHT.Auto.integer_gram_height_bound {r n : ℕ} (Z : Matrix (Fin r) (Fin n) ℤ) {B : ℝ} (hB : 0 ≤ B) (hZ : ∀ (i : Fin r) (j : Fin n), |↑(Z i j)| ≤ B) (i j : Fin r) : ↑(rationalHeight (((Z.map fun (z : ℤ) => ↑z) * (Z.map fun (z : ℤ) => ↑z).transpose) i j)) ≤ max 2 (↑n * B ^ 2)

theorem TrilinearHT.Auto.integerRowProjection_mul_norm_le {r n k : ℕ} (Z : Matrix (Fin r) (Fin n) ℤ) (V : Matrix (Fin n) (Fin k) ℝ) (hlin : LinearIndependent ℝ fun (i : Fin r) => WithLp.toLp 2 fun (j : Fin n) => ↑(Z i j)) {B W : ℝ} (hB : 0 ≤ B) (hW : 0 ≤ W) (hZ : ∀ (i : Fin r) (j : Fin n), |↑(Z i j)| ≤ B) (hZV : ∀ (i : Fin r) (j : Fin k), |((Z.map fun (z : ℤ) => ↑z) * V) i j| ≤ W) : ‖realMatrixOperator (((rationalRowProjection (Z.map fun (z : ℤ) => ↑z)).map fun (q : ℚ) => ↑q) * V)‖ ≤ ↑n * ↑r * B * (↑r * ↑r * Real.exp (2 * (↑r + 1) ^ 4 * Real.log (2 * max 2 (↑n * B ^ 2))) * (↑r * ↑k * W))

theorem TrilinearHT.Auto.integer_span_projection_velocity_bounds {r n k : ℕ} (Z : Matrix (Fin r) (Fin n) ℤ) (V : Matrix (Fin n) (Fin k) ℝ) (hlin : LinearIndependent ℝ fun (i : Fin r) => WithLp.toLp 2 fun (j : Fin n) => ↑(Z i j)) {B W : ℝ} (hB : 2 ≤ B) (hW : 0 ≤ W) (hZ : ∀ (i : Fin r) (j : Fin n), |↑(Z i j)| ≤ B) (hZV : ∀ (i : Fin r) (j : Fin k), |((Z.map fun (z : ℤ) => ↑z) * V) i j| ≤ W) : let U := Submodule.span ℝ (Set.range fun (i : Fin r) => WithLp.toLp 2 fun (j : Fin n) => ↑(Z i j)); ∃ (P : Matrix (Fin n) (Fin n) ℚ), realMatrixOperator (P.map fun (q : ℚ) => ↑q) = U.starProjection ∧ realMatrixOperator ((1 - P).map fun (q : ℚ) => ↑q) = Uᗮ.starProjection ∧ (∀ (i j : Fin n), ↑(rationalHeight (P i j)) ≤ Real.exp (8 * (↑n + 1) ^ 4 * Real.log (2 * B))) ∧ (∀ (i j : Fin n), ↑(rationalHeight ((1 - P) i j)) ≤ Real.exp (8 * (↑n + 1) ^ 4 * Real.log (2 * B))) ∧ ‖realMatrixOperator (P.map fun (q : ℚ) => ↑q)‖ ≤ 1 ∧ ‖realMatrixOperator ((1 - P).map fun (q : ℚ) => ↑q)‖ ≤ 1 ∧ ‖realMatrixOperator ((P.map fun (q : ℚ) => ↑q) * V)‖ ≤ ↑n * ↑r * B * (↑r * ↑r * Real.exp (2 * (↑r + 1) ^ 4 * Real.log (2 * max 2 (↑n * B ^ 2))) * (↑r * ↑k * W))

The same rational orthogonal projection has controlled height and controlled composition with a matrix whose products with its integer rows are bounded. No bound on the input matrix itself is assumed.

theorem TrilinearHT.Auto.real_matrix_mul_entry_eq_row_inner {r n k : ℕ} (S : Matrix (Fin r) (Fin n) ℝ) (V : Matrix (Fin n) (Fin k) ℝ) (i : Fin r) (j : Fin k) : (S * V) i j = inner ℝ (WithLp.toLp 2 (S.row i)) ((realMatrixOperator V) ((EuclideanSpace.basisFun (Fin k) ℝ) j))

noncomputable def TrilinearHT.Auto.realSymmetricPart {d : ℕ} (C : Matrix (Fin d) (Fin d) ℝ) : Matrix (Fin d) (Fin d) ℝ

Symmetric part of a real matrix.

Equations

• TrilinearHT.Auto.realSymmetricPart C = (1 / 2) • (C + C.transpose)

noncomputable def TrilinearHT.Auto.realSkewPart {d : ℕ} (C : Matrix (Fin d) (Fin d) ℝ) : Matrix (Fin d) (Fin d) ℝ

Skew-symmetric part of a real matrix.

Equations

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

noncomputable def TrilinearHT.Auto.effectiveReturnQuadratic {d k : ℕ} (C : Matrix (Fin d) (Fin d) ℝ) (Λ : Matrix (Fin k) (Fin k) ℝ) (V F S : Matrix (Fin d) (Fin k) ℝ) : Matrix (Fin k) (Fin k) ℝ

Quadratic matrix remaining after the return-coordinate change.

Equations

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

theorem TrilinearHT.Auto.effectiveReturnQuadratic_identity {d k : ℕ} (C : Matrix (Fin d) (Fin d) ℝ) (Λ : Matrix (Fin k) (Fin k) ℝ) (V F S : Matrix (Fin d) (Fin k) ℝ) (hV : V = F + S) (hiso : F.transpose * (C - C.transpose) * F = 0) : 2 • Λ + V.transpose * C * V - V.transpose * (C - C.transpose) * F = 2 • effectiveReturnQuadratic C Λ V F S + (1 / 2) • (S.transpose * (C - C.transpose) * S)

The exact quadratic identity in blueprint lem:return-splitting.

theorem TrilinearHT.Auto.realMatrixOperator_basis_apply {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (j : Fin n) : (realMatrixOperator A) ((EuclideanSpace.basisFun (Fin n) ℝ) j) = WithLp.toLp 2 (A.col j)

theorem TrilinearHT.Auto.realMatrix_abs_entry_le_norm {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (i : Fin m) (j : Fin n) : |A i j| ≤ ‖realMatrixOperator A‖

theorem TrilinearHT.Auto.realMatrix_transpose_norm_le {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) : ‖realMatrixOperator A.transpose‖ ≤ ↑n * ↑m * ‖realMatrixOperator A‖

theorem TrilinearHT.Auto.realMatrix_norm_le_from_scaled_columns {k : ℕ} (A : Matrix (Fin k) (Fin k) ℝ) {s R : ℝ} (hs : 0 < s) (hR : 0 ≤ R) (hcol : ∀ (j : Fin k), ∃ (t : ℝ), s ≤ t ∧ ‖(realMatrixOperator A) (t • (EuclideanSpace.basisFun (Fin k) ℝ) j)‖ ≤ R) : ‖realMatrixOperator A‖ ≤ ↑k * ↑k * (R / s)

theorem TrilinearHT.Auto.effectiveReturnQuadratic_frequency {d k : ℕ} (C : Matrix (Fin d) (Fin d) ℝ) (Λ : Matrix (Fin k) (Fin k) ℝ) (V F S : Matrix (Fin d) (Fin k) ℝ) (hV : V = F + S) (hiso : F.transpose * (C - C.transpose) * F = 0) (h : Fin k → ℝ) (m : Fin d → ℝ) (hdelta : (F.transpose * (C - C.transpose)).mulVec (m - F.mulVec h) = 0) : quadraticReturnFrequency C V Λ h m = 2 • (effectiveReturnQuadratic C Λ V F S).mulVec h + (1 / 2) • (S.transpose * (C - C.transpose) * S).mulVec h - (S.transpose * (C - C.transpose)).mulVec (m - F.mulVec h)

theorem TrilinearHT.Auto.isotropic_subspace_transpose_kills {d k : ℕ} (A : Matrix (Fin d) (Fin d) ℝ) (F : Matrix (Fin d) (Fin k) ℝ) (U : Submodule ℝ (EuclideanSpace ℝ (Fin d))) (hF : ∀ (x : EuclideanSpace ℝ (Fin k)), (realMatrixOperator F) x ∈ U) (hiso : ∀ x ∈ U, ∀ y ∈ U, inner ℝ y ((realMatrixOperator A) x) = 0) {z : EuclideanSpace ℝ (Fin d)} (hz : z ∈ U) : (realMatrixOperator (F.transpose * A)) z = 0

theorem TrilinearHT.Auto.isotropic_subspace_matrix_zero {d k : ℕ} (A : Matrix (Fin d) (Fin d) ℝ) (F : Matrix (Fin d) (Fin k) ℝ) (U : Submodule ℝ (EuclideanSpace ℝ (Fin d))) (hF : ∀ (x : EuclideanSpace ℝ (Fin k)), (realMatrixOperator F) x ∈ U) (hiso : ∀ x ∈ U, ∀ y ∈ U, inner ℝ y ((realMatrixOperator A) x) = 0) : F.transpose * A * F = 0

theorem TrilinearHT.Auto.effectiveReturnQuadratic_frequency_euclidean {d k : ℕ} (C : Matrix (Fin d) (Fin d) ℝ) (Λ : Matrix (Fin k) (Fin k) ℝ) (V F S : Matrix (Fin d) (Fin k) ℝ) (hV : V = F + S) (hiso : F.transpose * (C - C.transpose) * F = 0) (h : Fin k → ℝ) (m : Fin d → ℝ) (hdelta : (F.transpose * (C - C.transpose)).mulVec (m - F.mulVec h) = 0) : WithLp.toLp 2 (quadraticReturnFrequency C V Λ h m) = 2 • (realMatrixOperator (effectiveReturnQuadratic C Λ V F S)) (WithLp.toLp 2 h) + (1 / 2) • (realMatrixOperator S.transpose) ((realMatrixOperator (C - C.transpose)) ((realMatrixOperator S) (WithLp.toLp 2 h))) - (realMatrixOperator S.transpose) ((realMatrixOperator (C - C.transpose)) (WithLp.toLp 2 (m - F.mulVec h)))

theorem TrilinearHT.Auto.effectiveReturnQuadratic_apply_bound {d k : ℕ} (C : Matrix (Fin d) (Fin d) ℝ) (Λ : Matrix (Fin k) (Fin k) ℝ) (V F S : Matrix (Fin d) (Fin k) ℝ) (hV : V = F + S) (hiso : F.transpose * (C - C.transpose) * F = 0) (h : Fin k → ℝ) (m : Fin d → ℝ) (hdelta : (F.transpose * (C - C.transpose)).mulVec (m - F.mulVec h) = 0) {a B N M : ℝ} (hS : ‖realMatrixOperator S‖ ≤ B) (hA : ‖realMatrixOperator (C - C.transpose)‖ ≤ N) (hh : ‖WithLp.toLp 2 h‖ ≤ a) (hd : ‖WithLp.toLp 2 (m - F.mulVec h)‖ ≤ a) (hΩ : ‖WithLp.toLp 2 (quadraticReturnFrequency C V Λ h m)‖ ≤ M) : ‖(realMatrixOperator (effectiveReturnQuadratic C Λ V F S)) (WithLp.toLp 2 h)‖ ≤ M + ↑k * ↑d * B * (N * (B * a)) + ↑k * ↑d * B * (N * a)

theorem TrilinearHT.Auto.effectiveReturnQuadratic_norm_of_coordinate_returns {d k : ℕ} (C : Matrix (Fin d) (Fin d) ℝ) (Λ : Matrix (Fin k) (Fin k) ℝ) (V F S : Matrix (Fin d) (Fin k) ℝ) (hV : V = F + S) (U : Submodule ℝ (EuclideanSpace ℝ (Fin d))) (hproj : ∀ (x : EuclideanSpace ℝ (Fin k)), (realMatrixOperator F) x = U.starProjection ((realMatrixOperator V) x)) (hiso : ∀ x ∈ U, ∀ y ∈ U, inner ℝ y ((realMatrixOperator (C - C.transpose)) x) = 0) {a B N M s : ℝ} (ha : 0 ≤ a) (hM : 0 ≤ M) (hs : 0 < s) (hS : ‖realMatrixOperator S‖ ≤ B) (hA : ‖realMatrixOperator (C - C.transpose)‖ ≤ N) (hreturn : ∀ (j : Fin k), ∃ (t : ℝ) (m : EuclideanSpace ℝ (Fin d)), s ≤ t ∧ m ∈ U ∧ ‖t • (EuclideanSpace.basisFun (Fin k) ℝ) j‖ + ‖(realMatrixOperator V) (t • (EuclideanSpace.basisFun (Fin k) ℝ) j) - m‖ ≤ a ∧ ‖WithLp.toLp 2 (quadraticReturnFrequency C V Λ (t • (EuclideanSpace.basisFun (Fin k) ℝ) j).ofLp m.ofLp)‖ ≤ M) : ‖realMatrixOperator (effectiveReturnQuadratic C Λ V F S)‖ ≤ ↑k * ↑k * ((M + ↑k * ↑d * B * (N * (B * a)) + ↑k * ↑d * B * (N * a)) / s)

The effective quadratic form is bounded from coordinate returns in an isotropic subspace, using only the slow velocity and the return errors.