Scott's finite systems of linear inequalities

Definitions corresponding to §1 of Scott (1964), pp. 233–237.

def Scott1964.MeasurementStructures.LinearInequalities.Symmetric {L : Type u_1} [AddCommGroup L] (X : Set L) : Prop

A set is symmetric when it is closed under negation.

Equations

• Scott1964.MeasurementStructures.LinearInequalities.Symmetric X = ∀ ⦃x : L⦄, x ∈ X → -x ∈ X

def Scott1964.MeasurementStructures.LinearInequalities.Realizable {L : Type u_1} [AddCommGroup L] [Module ℝ L] (X N : Set L) : Prop

N is realized on X by a real linear functional.

Equations

• Scott1964.MeasurementStructures.LinearInequalities.Realizable X N = ∃ (φ : Module.Dual ℝ L), ∀ x ∈ X, x ∈ N ↔ 0 ≤ φ x

def Scott1964.MeasurementStructures.LinearInequalities.strictPositive {L : Type u_1} [AddCommGroup L] (X N : Set L) : Set L

Scott's notation x ≻ 0: positive, but its negative is not positive.

Equations

• Scott1964.MeasurementStructures.LinearInequalities.strictPositive X N = {x : L | x ∈ X ∧ x ∈ N ∧ -x ∉ N}

def Scott1964.MeasurementStructures.LinearInequalities.indifferent {L : Type u_1} [AddCommGroup L] (X N : Set L) : Set L

Vectors declared both nonnegative and nonpositive.

Equations

• Scott1964.MeasurementStructures.LinearInequalities.indifferent X N = {x : L | x ∈ X ∧ x ∈ N ∧ -x ∈ N}

def Scott1964.MeasurementStructures.LinearInequalities.SignComplete {L : Type u_1} [AddCommGroup L] (X N : Set L) : Prop

Condition (1): every vector has one of the two weak signs.

Equations

• Scott1964.MeasurementStructures.LinearInequalities.SignComplete X N = ∀ ⦃x : L⦄, x ∈ X → x ∈ N ∨ -x ∈ N

def Scott1964.MeasurementStructures.LinearInequalities.WeightedCancellation {L : Type u_1} [AddCommGroup L] [Module ℝ L] (X N : Set L) : Prop

Geometric form of Scott's condition (2).

No convex combination of strictly positive vectors belongs to the linear span of vectors carrying both weak signs. For finite symmetric systems this is equivalent to Scott's positive-coefficient cancellation condition.

Equations

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

def Scott1964.MeasurementStructures.LinearInequalities.WeightedSequenceCancellation {L : Type u_1} [AddCommGroup L] [Module ℝ L] (X N : Set L) : Prop

Scott's literal positive-weight finite-sequence condition (2). Sequences are indexed by Fin (n + 1), making nonemptiness explicit.

Equations

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

def Scott1964.MeasurementStructures.LinearInequalities.UnweightedSequenceCancellation {L : Type u_1} [AddCommGroup L] (X N : Set L) : Prop

Scott's literal unweighted finite-sequence condition (4).

Equations

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

def Scott1964.MeasurementStructures.LinearInequalities.NatWeightedSequenceCancellation {L : Type u_1} [AddCommGroup L] (X N : Set L) : Prop

Positive natural-multiplicity version, intermediate between rational weights and literal repetition.

Equations

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

def Scott1964.MeasurementStructures.LinearInequalities.IsRationalVector {S : Type u_2} (x : S → ℝ) : Prop

A vector in S → ℝ has rational coordinates.

Equations

• Scott1964.MeasurementStructures.LinearInequalities.IsRationalVector x = ∀ (s : S), ∃ (q : ℚ), x s = ↑q

def Scott1964.MeasurementStructures.LinearInequalities.IsRationalSet {S : Type u_2} (X : Set (S → ℝ)) : Prop

A set consists of rational vectors.

Equations

• Scott1964.MeasurementStructures.LinearInequalities.IsRationalSet X = ∀ ⦃x : S → ℝ⦄, x ∈ X → Scott1964.MeasurementStructures.LinearInequalities.IsRationalVector x

def Scott1964.MeasurementStructures.LinearInequalities.RelationRealizable {L : Type u_1} [AddCommGroup L] [Module ℝ L] (Y : Set L) (R : L → L → Prop) : Prop

Realizability of a relation by comparison of functional values.

Equations

• Scott1964.MeasurementStructures.LinearInequalities.RelationRealizable Y R = ∃ (φ : Module.Dual ℝ L), ∀ x ∈ Y, ∀ y ∈ Y, R x y ↔ φ y ≤ φ x

def Scott1964.MeasurementStructures.LinearInequalities.RelationComplete {L : Type u_1} (Y : Set L) (R : L → L → Prop) : Prop

Condition (5): completeness on Y.

Equations

• Scott1964.MeasurementStructures.LinearInequalities.RelationComplete Y R = ∀ ⦃x : L⦄, x ∈ Y → ∀ ⦃y : L⦄, y ∈ Y → R x y ∨ R y x

def Scott1964.MeasurementStructures.LinearInequalities.strictDifferences {L : Type u_1} [AddCommGroup L] (Y : Set L) (R : L → L → Prop) : Set L

Strictly positive differences associated to a relation.

Equations

• Scott1964.MeasurementStructures.LinearInequalities.strictDifferences Y R = {z : L | ∃ x ∈ Y, ∃ y ∈ Y, R x y ∧ ¬R y x ∧ z = x - y}

def Scott1964.MeasurementStructures.LinearInequalities.indifferentDifferences {L : Type u_1} [AddCommGroup L] (Y : Set L) (R : L → L → Prop) : Set L

Indifferent differences associated to a relation.

Equations

• Scott1964.MeasurementStructures.LinearInequalities.indifferentDifferences Y R = {z : L | ∃ x ∈ Y, ∃ y ∈ Y, R x y ∧ R y x ∧ z = x - y}

def Scott1964.MeasurementStructures.LinearInequalities.RelationCancellation {L : Type u_1} [AddCommGroup L] [Module ℝ L] (Y : Set L) (R : L → L → Prop) : Prop

Geometric form of Scott's equal-sums cancellation condition (6).

Equations

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

def Scott1964.MeasurementStructures.LinearInequalities.RelationSequenceCancellation {L : Type u_1} [AddCommGroup L] (Y : Set L) (R : L → L → Prop) : Prop

Scott's literal paired equal-sums condition (6).

Equations

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

def Scott1964.MeasurementStructures.LinearInequalities.additiveClosure {L : Type u_1} [AddCommGroup L] (Y : Set L) : Set L

The additive closure Y⁺ (including the empty sum).

Equations

• Scott1964.MeasurementStructures.LinearInequalities.additiveClosure Y = ↑(AddSubmonoid.closure Y)

structure Scott1964.MeasurementStructures.LinearInequalities.StrictlyMonotonic {L : Type u_1} [AddCommGroup L] (Z : Set L) (R : L → L → Prop) : Prop

Scott's three axioms (i)–(iii) for a strictly monotonic relation.

• complete ⦃x : L⦄ : x ∈ Z → ∀ ⦃y : L⦄, y ∈ Z → R x y ∨ R y x
• add ⦃x₀ y₀ x₁ y₁ : L⦄ : x₀ ∈ Z → y₀ ∈ Z → x₁ ∈ Z → y₁ ∈ Z → R x₀ y₀ → R x₁ y₁ → R (x₀ + x₁) (y₀ + y₁)
• cancel ⦃x₀ y₀ x₁ y₁ : L⦄ : x₀ ∈ Z → y₀ ∈ Z → x₁ ∈ Z → y₁ ∈ Z → x₀ + x₁ = y₀ + y₁ → R x₁ y₁ → R y₀ x₀

def Scott1964.MeasurementStructures.LinearInequalities.ExtendsOn {L : Type u_1} (Y Z : Set L) (R Rplus : L → L → Prop) : Prop

Rplus extends R from Y to Z.

Equations

• Scott1964.MeasurementStructures.LinearInequalities.ExtendsOn Y Z R Rplus = (Y ⊆ Z ∧ ∀ ⦃x : L⦄, x ∈ Y → ∀ ⦃y : L⦄, y ∈ Y → (Rplus x y ↔ R x y))