Reference · Non-negative rationals

rainbow.math.rational.nnrat.fubini

Non-negative rationalssrc/rainbow/math/rational/nnrat/fubini.clj0 definitions, 1 theorems

Fubini / double-sum swap for finite nnrat sums, up to nnrat equivalence (~): nnrat/map-sum-swap : sum_{i in is} sum_{j in js} F i j ~ sum_{j in js} sum_{i in is} F i j i.e. map-sum A (\i. map-sum B (F i) js) is ~ map-sum B (\j. map-sum A (\i. F i j) is) js. The keystone that turns the weighted-sum monotone legs into an actual LP weak-duality bound c.x <= b.y (via (Aᵀy).x = y.(Ax)), and the reusable interchange behind expectation-of-sum, covariance, and any rectangular double accumulation. Proof: List.rec induction on the outer list `is`. nil : LHS = 0; RHS = sum_j (empty inner sum) = sum_j 0 ~ 0 (map-sum-zero). cons : LHS = (sum_j F h j) + (inner IH); RHS's outer mapping splits by the inner cons recurrence into (F h j) + rest, and map-sum-add pushes that out to (sum_j F h j) + (sum_j rest); the IH identifies (inner IH) with (sum_j rest); add-respects-equivalence recombines. Polymorphic in both index types. Native and axiom-free; chains nnrat-map-sum-additive on d63.

Depends onmath.rational.nnrat.map-sum-additive

nnrat/map-sum-swap.{u} :
  (A B : Type u) (F : A → B → ℚ≥0) (is : List A) (js : List B)
  → nnrat/map-sum A (fun i => nnrat/map-sum B (F i) js) is = nnrat/map-sum B (fun j => nnrat/map-sum A (fun i => F i j) is) js