Rational vectors

Elementary closure facts used in Scott's reduction from relations to inequalities on the rational difference set Y - Y.

theorem Scott1964.MeasurementStructures.LinearInequalities.isRationalVector_zero {S : Type u_1} : IsRationalVector 0

theorem Scott1964.MeasurementStructures.LinearInequalities.IsRationalVector.neg {S : Type u_1} {x : S → ℝ} (hx : IsRationalVector x) : IsRationalVector (-x)

theorem Scott1964.MeasurementStructures.LinearInequalities.IsRationalVector.sub {S : Type u_1} {x y : S → ℝ} (hx : IsRationalVector x) (hy : IsRationalVector y) : IsRationalVector (x - y)

theorem Scott1964.MeasurementStructures.LinearInequalities.rational_difference_set {S : Type u_1} {Y : Set (S → ℝ)} (hY : IsRationalSet Y) : IsRationalSet {z : S → ℝ | ∃ x ∈ Y, ∃ y ∈ Y, z = x - y}

theorem Scott1964.MeasurementStructures.LinearInequalities.exists_pos_rational_relation {S : Type u_1} {I : Type u_2} [Fintype I] [Finite S] (x : I → S → ℝ) (hx : ∀ (i : I), IsRationalVector (x i)) (c : I → ℝ) (hc : ∀ (i : I), 0 < c i) (hsum : ∑ i : I, c i • x i = 0) : ∃ (q : I → ℚ), (∀ (i : I), 0 < q i) ∧ ∑ i : I, ↑(q i) • x i = 0

A strictly positive real relation between finitely many rational vectors can be replaced by a strictly positive rational relation.

This is the scalar-extension step in Scott's proof of Theorem 1.2. Exactness of tensoring the rational kernel with ℝ writes the given real relation as a finite real linear combination of rational kernel vectors. Density of a finite product of copies of ℚ then preserves all strict coordinate inequalities.

theorem Scott1964.MeasurementStructures.LinearInequalities.UnweightedSequenceCancellation.natWeighted {L : Type u_2} [AddCommGroup L] {X N : Set L} (h : UnweightedSequenceCancellation X N) : NatWeightedSequenceCancellation X N

Clearing to positive natural coefficients can be discharged by literal repetition of each vector.

theorem Scott1964.MeasurementStructures.LinearInequalities.UnweightedSequenceCancellation.rationalWeighted {S : Type u_2} [Finite S] {X N : Set (S → ℝ)} (h : UnweightedSequenceCancellation X N) (hX : IsRationalSet X) : WeightedSequenceCancellation X N

On rational coordinate vectors, Scott's unit-weight cancellation condition implies his arbitrary positive-real-weight condition.