Reference · Signed rationals

rainbow.math.rational.signed.dyadic-jensen

Signed rationalssrc/rainbow/math/rational/signed/dyadic_jensen.clj0 definitions, 2 theorems

Dyadic (four-point) Jensen for signed-rational convex functions -- n-point Jensen for the power-of-two case, reachable WITHOUT the reciprocal wall that blocks general n-point Jensen (which needs weight renormalization by 1/(1-w0)). Uses only halving (w=1/2), so it iterates two-point convexity through nested midpoints. nnrat/half-add-self-equivalent-one : 1/2 + 1/2 ~ 1 signed/dyadic-jensen-four : convex-on f -> f(mid(mid x0 x1)(mid x2 x3)) <= mid(mid (f x0)(f x1))(mid (f x2)(f x3)) where mid a b = (1/2)a + (1/2)b. f is abstract, so the type stays cheap to check (f stuck at the combination). Proof: apply convex-on at (1/2,1/2) to each midpoint (bounding f of a midpoint by the midpoint of f's), then combine by midpoint monotonicity and transitivity. Wall-free; does not touch the LP checker.

Depends onmath.rational.signed.convex-functionmath.rational.signed.multiply-monotonemath.rational.signed.order-monotonemath.rational.signed.order-transitivitymath.rational.signed.multiply-ordermath.rational.nnrat.farkas-elim-list

nnrat/half-add-self-equivalent-one :
  → nnrat/half + nnrat/half = 1

signed/dyadic-jensen-four :
  (f : ℚ → ℚ) (cf : signed/convex-on f) (x0 x1 x2 x3 : ℚ)
  → f (signed/from-nnrat nnrat/half · (signed/from-nnrat nnrat/half · x0 + signed/from-nnrat nnrat/half · x1) + signed/from-nnrat nnrat/half · (signed/from-nnrat nnrat/half · x2 + signed/from-nnrat nnrat/half · x3)) ≤ signed/from-nnrat nnrat/half · (signed/from-nnrat nnrat/half · f x0 + signed/from-nnrat nnrat/half · f x1) + signed/from-nnrat nnrat/half · (signed/from-nnrat nnrat/half · f x2 + signed/from-nnrat nnrat/half · f x3)