RationalCone.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

+# 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 OAI.MatrixMultiplication.AuxiliarySeparation.rationalVectorCast line 19
Source documentation
Coordinatewise inclusion of rational vectors into real vectors.
```
def rationalVectorCast {J : Type*} (v : J → ℚ) : J → ℝ := fun j ↦ v j
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.rationalVectorCast_apply line 21

theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_rat_convex_weights_of_affineIndependent line 26

Source documentation

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

theorem exists_rat_convex_weights_of_affineIndependent
    {I J : Type*} [Fintype I] (v : I → J → ℚ) (b : J → ℚ)
    (w : I → ℝ)
    (hpos : ∀ i, 0 ≤ w i) (hsum : ∑ i, w i = 1)
    (heq : ∑ i, w i • rationalVectorCast (v i) = rationalVectorCast b)
    (hind : AffineIndependent ℝ (fun i ↦ rationalVectorCast (v i))) :
    ∃ q : I → ℚ, (∀ i, 0 ≤ q i) ∧ ∑ i, q i = 1 ∧
      ∑ i, q i • v i = b := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.rationalVectorCast

theorem OAI.MatrixMultiplication.AuxiliarySeparation.rationalVectorCast_mem_convexHull_descend line 72
Source documentation
Taking the convex hull of rational vectors in real space does not create new rational points.
```
theorem rationalVectorCast_mem_convexHull_descend
    {J : Type*} {s : Set (J → ℚ)} {b : J → ℚ}
    (h : rationalVectorCast b ∈ convexHull ℝ (rationalVectorCast '' s)) :
    b ∈ convexHull ℚ s := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.rationalVectorCast

theorem OAI.MatrixMultiplication.AuxiliarySeparation.mem_rationalCone_of_nonneg_real_solution line 91

Source documentation

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

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

theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_nonneg_rat_solution_of_real line 156

Source documentation

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

theorem exists_nonneg_rat_solution_of_real
    {I J : Type*} [Fintype I] (A : I → J → ℚ) (b : J → ℚ)
    (h : ∃ x : I → ℝ, (∀ i, 0 ≤ x i) ∧
      ∀ j, ∑ i, x i * (A i j : ℝ) = (b j : ℝ)) :
    ∃ q : I → ℚ, (∀ i, 0 ≤ q i) ∧ ∀ j, ∑ i, q i * A i j = b j := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_nat_scaled_solution_of_nonneg_real line 171

Source documentation

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

theorem exists_nat_scaled_solution_of_nonneg_real
    {I J : Type*} [Fintype I] (A : I → J → ℚ) (b : J → ℚ)
    (h : ∃ x : I → ℝ, (∀ i, 0 ≤ x i) ∧
      ∀ j, ∑ i, x i * (A i j : ℝ) = (b j : ℝ)) :
    ∃ D : ℕ, 0 < D ∧ ∃ c : I → ℕ,
      ∀ j, ∑ i, (c i : ℚ) * A i j = (D : ℚ) * b j := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_nat_scaled_int_solution_of_nonneg_real line 187

Source documentation

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

theorem exists_nat_scaled_int_solution_of_nonneg_real
    {I J : Type*} [Fintype I] (A : I → J → ℤ) (b : J → ℤ)
    (h : ∃ x : I → ℝ, (∀ i, 0 ≤ x i) ∧
      ∀ j, ∑ i, x i * (A i j : ℝ) = (b j : ℝ)) :
    ∃ D : ℕ, 0 < D ∧ ∃ c : I → ℕ,
      ∀ j, ∑ i, (c i : ℤ) * A i j = (D : ℤ) * b j := by
…