+# Rational nonnegative certificates

Finite rational linear systems with a nonnegative real solution have a nonnegative rational solution. Affinely independent convex representations allow a rational-linear projection to preserve the coefficients exactly.

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.rationalVectorCast {J : Type u_1} (v : J → ℚ) : J → ℝ

Coordinatewise inclusion of rational vectors into real vectors.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.rationalVectorCast v j = ↑(v j)

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.rationalVectorCast_apply {J : Type u_1} (v : J → ℚ) (j : J) : rationalVectorCast v j = ↑(v j)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exists_rat_convex_weights_of_affineIndependent {I : Type u_1} {J : Type u_2} [Fintype I] (v : I → J → ℚ) (b : J → ℚ) (w : I → ℝ) (hpos : ∀ (i : I), 0 ≤ w i) (hsum : ∑ i : I, w i = 1) (heq : ∑ i : I, w i • rationalVectorCast (v i) = rationalVectorCast b) (hind : AffineIndependent ℝ fun (i : I) => rationalVectorCast (v i)) : ∃ (q : I → ℚ), (∀ (i : I), 0 ≤ q i) ∧ ∑ i : I, q i = 1 ∧ ∑ i : I, q i • v i = b

In an affinely independent rational family, the coefficients of a real convex representation of a rational point are rational.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.rationalVectorCast_mem_convexHull_descend {J : Type u_1} {s : Set (J → ℚ)} {b : J → ℚ} (h : rationalVectorCast b ∈ (convexHull ℝ) (rationalVectorCast '' s)) : b ∈ (convexHull ℚ) s

Taking the convex hull of rational vectors in real space does not create new rational points.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.mem_rationalCone_of_nonneg_real_solution {I : Type u_1} {J : Type u_2} [Fintype I] (A : I → J → ℚ) (b : J → ℚ) (x : I → ℝ) (hxpos : ∀ (i : I), 0 ≤ x i) (hxeq : ∀ (j : J), ∑ i : I, x i * ↑(A i j) = ↑(b j)) : b ∈ PointedCone.hull ℚ (Set.range A)

A rational point in the real cone generated by a finite rational family already lies in the rational cone generated by that family.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exists_nonneg_rat_solution_of_real {I : Type u_1} {J : Type u_2} [Fintype I] (A : I → J → ℚ) (b : J → ℚ) (h : ∃ (x : I → ℝ), (∀ (i : I), 0 ≤ x i) ∧ ∀ (j : J), ∑ i : I, x i * ↑(A i j) = ↑(b j)) : ∃ (q : I → ℚ), (∀ (i : I), 0 ≤ q i) ∧ ∀ (j : J), ∑ i : I, q i * A i j = b j

Nonnegative solvability of a finite rational linear system descends from real coefficients to rational coefficients. The equation index type may be infinite.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exists_nat_scaled_solution_of_nonneg_real {I : Type u_1} {J : Type u_2} [Fintype I] (A : I → J → ℚ) (b : J → ℚ) (h : ∃ (x : I → ℝ), (∀ (i : I), 0 ≤ x i) ∧ ∀ (j : J), ∑ i : I, x i * ↑(A i j) = ↑(b j)) : ∃ (D : ℕ), 0 < D ∧ ∃ (c : I → ℕ), ∀ (j : J), ∑ i : I, ↑(c i) * A i j = ↑D * b j

Clearing denominators turns a nonnegative real solution of a rational system into a positive integer multiple with natural coefficients.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exists_nat_scaled_int_solution_of_nonneg_real {I : Type u_1} {J : Type u_2} [Fintype I] (A : I → J → ℤ) (b : J → ℤ) (h : ∃ (x : I → ℝ), (∀ (i : I), 0 ≤ x i) ∧ ∀ (j : J), ∑ i : I, x i * ↑(A i j) = ↑(b j)) : ∃ (D : ℕ), 0 < D ∧ ∃ (c : I → ℕ), ∀ (j : J), ∑ i : I, ↑(c i) * A i j = ↑D * b j

Integer form of finite cone certificate extraction. This is the form used when the selected additive relations have integral coefficients.