Finite weight vectors in ℝ≥0∞

A weight vector on a Finset s is a function f : X → ℝ≥0∞ with ∑ x ∈ s, f x = 1; the weights of a probability measure on its finite carrier are the motivating example. This file records the arithmetic of comparing two weight vectors, and of rounding one onto a grid.

Two weight vectors split against each other: the mass min (f x) (g x) matched at x and the excess f x - g x above g add up to f x. When g is dominated by f away from one designated atom x₀ -- so that g arises from f by transferring weight onto x₀ -- the designated atom can only gain, and it gains exactly the total excess. Only equality of the two finite total masses is used there, not normalization to one.

Rounding to a common denominator M cannot be done pointwise, since the weights have to keep summing to one. TauCeti.exists_nat_weights_of_sum_eq_one rounds every weight but the one at x₀ down to a multiple of 1 / M and lets x₀ absorb the slack; the rounded weights are then dominated away from x₀ and lose less than 1 / M each.

Main results

• Finset.sum_min_add_sum_tsub -- the matched mass and the excess mass add up to the total;
• ENNReal.toReal_sub_add_toReal_sub -- the excesses in both directions add up to the distance;
• TauCeti.le_of_sum_eq_of_forall_ne_le -- an atom dominating everywhere else can only gain;
• TauCeti.add_sum_tsub_eq_of_forall_ne_le -- it gains exactly the total excess;
• TauCeti.exists_nat_weights_of_sum_eq_one -- rounding a weight vector to a common denominator.

theorem Finset.sum_min_add_sum_tsub {X : Type u_1} (s : Finset X) (f g : X → ENNReal) : ∑ x ∈ s, min (f x) (g x) + ∑ x ∈ s, (f x - g x) = ∑ x ∈ s, f x

The mass of f matched by g and the mass of f above g add up to f.

theorem ENNReal.toReal_sub_add_toReal_sub {a b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : (a - b).toReal + (b - a).toReal = |a.toReal - b.toReal|

The excess of a over b and the excess of b over a add up to their distance: for finite a and b, (a - b) + (b - a) = |a - b|, read in ℝ.

theorem TauCeti.le_of_sum_eq_of_forall_ne_le {X : Type u_1} {s : Finset X} {f g : X → ENNReal} {x₀ : X} (hx₀ : x₀ ∈ s) (hfg : ∑ x ∈ s, f x = ∑ x ∈ s, g x) (hne : ∑ x ∈ s, f x ≠ ⊤) (hdom : ∀ x ∈ s, x ≠ x₀ → g x ≤ f x) : f x₀ ≤ g x₀

Away from x₀ the smaller of two weight vectors of equal finite total mass is g, so the designated atom x₀ can only gain weight.

theorem TauCeti.add_sum_tsub_eq_of_forall_ne_le {X : Type u_1} {s : Finset X} {f g : X → ENNReal} {x₀ : X} (hx₀ : x₀ ∈ s) (hfg : ∑ x ∈ s, f x = ∑ x ∈ s, g x) (hne : ∑ x ∈ s, f x ≠ ⊤) (hdom : ∀ x ∈ s, x ≠ x₀ → g x ≤ f x) : f x₀ + ∑ x ∈ s, (f x - g x) = g x₀

The designated atom x₀ absorbs exactly the total weight transferred onto it.

theorem TauCeti.exists_nat_weights_of_sum_eq_one {X : Type u_1} {s : Finset X} {f : X → ENNReal} {x₀ : X} (hx₀ : x₀ ∈ s) (hf : ∑ x ∈ s, f x = 1) {M : ℕ} (hM : 0 < M) : ∃ (m : X → ℕ), ∑ x ∈ s, m x = M ∧ (∀ x ∈ s, x ≠ x₀ → ↑(m x) ≤ ↑M * f x) ∧ ∀ x ∈ s, x ≠ x₀ → ↑M * f x ≤ ↑(m x) + 1

Rounding a weight vector to a common denominator. A weight vector of total mass one is turned into one whose entries are the multiples m x / M of 1 / M, by rounding every weight but the one at a designated atom x₀ down and letting x₀ absorb the slack. Away from x₀ the rounded weight is below the original one and within 1 / M of it; at x₀ nothing is claimed, since that is where all the slack goes.

The conclusion is stated multiplicatively, as m x ≤ M * f x and M * f x ≤ m x + 1, so that it holds with no inequality between M and the size of the weights.