Reference · Non-negative rationals

rainbow.math.rational.nnrat.finite-min-positive

Non-negative rationalssrc/rainbow/math/rational/nnrat/finite_min_positive.clj0 definitions, 4 theorems

Positive lower bounds from finite exact-rational minima. The existing non-empty minimum fold takes an explicit initial value and a list of remaining values. If every input is strictly positive, its result is strictly positive. Combined with the fold's existing lower-bound law, this produces an exact positive value below every input—the quantitative finite-minimum ingredient for Markov minorization and mixing bounds. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.nnrat.farkas-elim-listmath.rational.nnrat.positive

nnrat/min-ub-positive :
  (initial : ℚ≥0) (rest : List ℚ≥0) (initial-positive : nnrat/positive initial)
  (rest-positive : ∀ (value : ℚ≥0), ∀ (member : list/membership ℚ≥0 rest value), nnrat/positive value)
  → nnrat/positive (nnrat/min-ub initial rest)

nnrat/min-ub-positive-lower-bound :
  (initial : ℚ≥0) (rest : List ℚ≥0) (initial-positive : nnrat/positive initial)
  (rest-positive : ∀ (value : ℚ≥0), ∀ (member : list/membership ℚ≥0 rest value), nnrat/positive value)
  → proposition/conjunction (nnrat/positive (nnrat/min-ub initial rest)) (all)
  where all := nnrat/le-all initial rest (nnrat/min-ub initial rest)

nnrat/le-all-member :
  (initial : ℚ≥0) (rest : List ℚ≥0) (low : ℚ≥0) (bounds : nnrat/le-all initial rest low)
  (value : ℚ≥0) (member : list/membership ℚ≥0 (data/cons ℚ≥0 initial rest) value)
  → low ≤ value

nnrat/min-ub-below-member :
  (initial : ℚ≥0) (rest : List ℚ≥0) (value : ℚ≥0)
  (member : list/membership ℚ≥0 (data/cons ℚ≥0 initial rest) value)
  → nnrat/min-ub initial rest ≤ value