Reference · Non-negative rationals

rainbow.math.rational.nnrat.convex-multi-point

Non-negative rationalssrc/rainbow/math/rational/nnrat/convex_multi_point.clj0 definitions, 2 theorems

Finite nonnegative-weighted combinations preserve global value bounds: sum_i (w i * m) <= sum_i (w i * v i) when forall i, m <= v i sum_i (w i * v i) <= sum_i (w i * Mx) when forall i, v i <= Mx These are the N-point convexity / averaging brackets without a normalization assumption on the weights. Each proof first uses nnrat/multiply-monotone to lift the global bound through the nonnegative weight at one index, then uses nnrat/map-sum-monotone to lift those pointwise bounds through the finite sum. Polymorphic in the index type. Native and axiom-free; chains nnrat-list-sum and nnrat-multiply-monotone on D63.

Depends onmath.rational.nnrat.list-summath.rational.nnrat.multiply-monotone

nnrat/weighted-combo-at-least.{u} :
  (A : Type u) (w v : A → ℚ≥0) (m : ℚ≥0)
  (hm : ∀ (i : A), m ≤ v i)
  (idx : List A)
  → nnrat/map-sum A (fun i => w i · m) idx ≤ nnrat/map-sum A (fun i => w i · v i) idx

nnrat/weighted-combo-at-most.{u} :
  (A : Type u) (w v : A → ℚ≥0) (Mx : ℚ≥0)
  (hMx : ∀ (i : A), v i ≤ Mx)
  (idx : List A)
  → nnrat/map-sum A (fun i => w i · v i) idx ≤ nnrat/map-sum A (fun i => w i · Mx) idx