Rational approximation within rational affine constraints

A generalized inverse over the rationals gives an affine projection onto any consistent rational system. Its real extension allows approximation by rational solutions while retaining open inequalities.

theorem EGZ.BalancedCombination.exists_matrix_generalized_inverse {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] (A : Matrix I J ℚ) : ∃ (B : Matrix J I ℚ), A * B * A = A

Every rational matrix admits a generalized inverse, including rectangular and rank-deficient matrices.

theorem EGZ.BalancedCombination.exists_rational_solution_mem_open {I : Type u_1} {J : Type u_2} [Finite I] [Fintype J] (A : Matrix I J ℚ) (b : I → ℚ) (x : J → ℝ) (hx : (A.map ⇑(Rat.castHom ℝ)).mulVec x = fun (i : I) => ↑(b i)) (U : Set (J → ℝ)) (hU : IsOpen U) (hxU : x ∈ U) : ∃ (y : J → ℚ), A.mulVec y = b ∧ (fun (j : J) => ↑(y j)) ∈ U

Rational solutions of a rational linear system are dense in its real solution set. In particular, any open inequalities valid at a real solution remain valid at some rational solution.