Reciprocal natural weights in the extended nonnegative reals

For finitely many coordinates, the weight of d with reciprocal natural weights r is the real sum of ratios ∑ i, d i / r i whenever d ≤ r. The bound permits zero weights: their exponents must also be zero, so they contribute zero to both sums. This identifies extended nonnegative weights with ordinary real ratios without requiring every weight to be positive.

On a product κ × ι of blocks indexed by κ, the weight giving the coordinate (h, i₀ h) of each block the reciprocal natural weight (d h)⁻¹ and every other coordinate the weight 0 is the sum ∑ h, n (h, i₀ h) / d h.

theorem Finsupp.weight_inv_natCast_eq_ofReal_sum_div {σ : Type u_1} [Fintype σ] {r : σ → ℕ} {d : σ →₀ ℕ} (hdr : ∀ (i : σ), d i ≤ r i) : (weight fun (j : σ) => (↑(r j))⁻¹) d = ENNReal.ofReal (∑ i : σ, ↑(d i) / ↑(r i))

If d ≤ r, the reciprocal natural weight of d in ℝ≥0∞ is the real sum ∑ᵢ dᵢ / rᵢ. Zero weights are allowed, since their corresponding exponents are zero.

theorem Finsupp.weight_ite_inv_natCast_eq_sum_div {κ : Type u_2} {ι : Type u_3} [Fintype κ] [Finite ι] [DecidableEq ι] (i₀ : κ → ι) (d : κ → ℕ) (n : κ × ι →₀ ℕ) : (weight fun (p : κ × ι) => if p.2 = i₀ p.1 then (↑(d p.1))⁻¹ else 0) n = ∑ h : κ, ↑(n (h, i₀ h)) / ↑(d h)

On blocks κ × ι, the weight that is (d h)⁻¹ at the coordinate (h, i₀ h) of each block and 0 elsewhere is the sum ∑ h, n (h, i₀ h) / d h in ℝ≥0∞.