Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-elim-list

Non-negative rationalssrc/rainbow/math/rational/nnrat/farkas_elim_list.clj6 definitions, 9 theorems

List-sized one-variable Fourier--Motzkin elimination over nnrat bounds. Lower bounds are folded from zero with max, while the non-empty upper family is represented by a head and a list tail. The reduced system says that the folded lower bound satisfies every upper bound. Constructively, this is equivalent to existence of a value satisfying every lower and upper bound. All definitions and proofs are native proof data and axiom-free.

Depends onmath.rational.nnrat.minmax

nnrat/ge-all :
  (x₁ : List ℚ≥0) (x₂ : ℚ≥0)
  → Prop

nnrat/le-all :
  (x₁ : ℚ≥0) (x₂ : List ℚ≥0) (x₃ : ℚ≥0)
  → Prop

nnrat/max-lb :
  (x₁ : List ℚ≥0)
  → ℚ≥0

nnrat/min-ub :
  (x₁ : ℚ≥0) (x₂ : List ℚ≥0)
  → ℚ≥0

nnrat/farkas-elim-list-reduced :
  (x₁ : List ℚ≥0) (x₂ : ℚ≥0) (x₃ : List ℚ≥0)
  → Prop

nnrat/farkas-elim-list-solvable :
  (x₁ : List ℚ≥0) (x₂ : ℚ≥0) (x₃ : List ℚ≥0)
  → Prop

nnrat/zero-at-most :
  (value : ℚ≥0)
  → 0 ≤ value

nnrat/max-lb-is-upper :
  (lowers : List ℚ≥0)
  → nnrat/ge-all lowers (nnrat/max-lb lowers)

nnrat/max-lb-least :
  (lowers : List ℚ≥0) (value : ℚ≥0) (all : nnrat/ge-all lowers value)
  → nnrat/max-lb lowers ≤ value

nnrat/le-all-antitone :
  (u0 : ℚ≥0) (urest : List ℚ≥0) (a b : ℚ≥0)
  (a-b : a ≤ b)
  (all-b : nnrat/le-all u0 urest b)
  → nnrat/le-all u0 urest a

nnrat/min-ub-is-lower :
  (u0 : ℚ≥0) (urest : List ℚ≥0)
  → nnrat/le-all u0 urest (nnrat/min-ub u0 urest)

nnrat/min-ub-greatest :
  (u0 : ℚ≥0) (urest : List ℚ≥0) (value : ℚ≥0) (all : nnrat/le-all u0 urest value)
  → value ≤ nnrat/min-ub u0 urest

nnrat/farkas-elim-list-extends :
  (lowers : List ℚ≥0) (u0 : ℚ≥0) (urest : List ℚ≥0)
  (reduced-feasible : nnrat/farkas-elim-list-reduced lowers u0 urest)
  → nnrat/farkas-elim-list-solvable lowers u0 urest

nnrat/farkas-elim-list-projects :
  (lowers : List ℚ≥0) (u0 : ℚ≥0) (urest : List ℚ≥0)
  (solution : nnrat/farkas-elim-list-solvable lowers u0 urest)
  → nnrat/farkas-elim-list-reduced lowers u0 urest

nnrat/farkas-elim-list-solvable-iff :
  (lowers : List ℚ≥0) (u0 : ℚ≥0) (urest : List ℚ≥0)
  → proposition/conjunction (reduced → solvable) (solvable → reduced)
  where reduced := nnrat/farkas-elim-list-reduced lowers u0 urest
  where solvable := nnrat/farkas-elim-list-solvable lowers u0 urest