Inverse-power sums over multisets of naturals

Multiset.invPowSum α m is the sum of n⁻ᵅ over a multiset m of naturals. A multiset t dominates s when some submultiset of t matches s entry for entry, each matched entry of t being at most its partner in s. Then s.invPowSum α ≤ t.invPowSum α at every exponent 0 ≤ α, and strictly so at every 0 < α when s does not dominate t in turn.

Dominance is equivalent to a counting condition of Hall type, that s has no more entries below any threshold than t has, so it is first-order stochastic dominance of the counting distributions, and it is decidable. At a natural exponent k, when every entry divides a common denominator D, the sum times Dᵏ is the natural number divPowSum D k m.

Main definitions

• Multiset.invPowSum α m: the sum of n⁻ᵅ over m.
• Multiset.Dominates, Multiset.StrictDominates: dominance and its strict part.
• Multiset.prodMul s t: the multiset of pairwise products.
• Multiset.divPowSum D k m: the sum of (D / n)ᵏ over m.

Main results

• Multiset.Dominates.invPowSum_le, Multiset.StrictDominates.invPowSum_lt: dominance orders the inverse-power sums at every exponent.
• Multiset.dominates_iff_forall: dominance is the counting condition.
• Multiset.invPowSum_prodMul: the sum over pairwise products is the product of the sums.
• Multiset.invPowSum_mul_pow_eq_divPowSum: clearing the common denominator.

Inverse-power sums

noncomputable def Multiset.invPowSum (α : ℝ) (m : Multiset ℕ) : ENNReal

The sum of n⁻ᵅ over m. Entries equal to 0 contribute ⊤.

Equations

• Multiset.invPowSum α m = (Multiset.map (fun (n : ℕ) => (↑n)⁻¹ ^ α) m).sum

@[simp]

theorem Multiset.invPowSum_zero (α : ℝ) : invPowSum α 0 = 0

@[simp]

theorem Multiset.invPowSum_cons (α : ℝ) (n : ℕ) (m : Multiset ℕ) : invPowSum α (n ::ₘ m) = (↑n)⁻¹ ^ α + invPowSum α m

@[simp]

theorem Multiset.invPowSum_singleton (α : ℝ) (n : ℕ) : invPowSum α {n} = (↑n)⁻¹ ^ α

@[simp]

theorem Multiset.invPowSum_add (α : ℝ) (m₁ m₂ : Multiset ℕ) : invPowSum α (m₁ + m₂) = invPowSum α m₁ + invPowSum α m₂

theorem Multiset.invPowSum_mono {α : ℝ} {s t : Multiset ℕ} (h : s ≤ t) : invPowSum α s ≤ invPowSum α t

theorem Multiset.invPowSum_pos {α : ℝ} {m : Multiset ℕ} (hα : 0 ≤ α) (hm : m ≠ 0) : 0 < invPowSum α m

theorem Multiset.invPowSum_ne_top {α : ℝ} {s : Multiset ℕ} (hα : 0 ≤ α) (hs : 0 ∉ s) : invPowSum α s ≠ ⊤

Domination

def Multiset.Dominates (t s : Multiset ℕ) : Prop

A multiset t dominates s when some submultiset of t matches s entry for entry, each matched entry of t being at most its partner in s.

Equations

• t.Dominates s = ∃ t' ≤ t, Multiset.Rel (fun (x1 x2 : ℕ) => x1 ≤ x2) t' s

def Multiset.StrictDominates (t s : Multiset ℕ) : Prop

A multiset t strictly dominates s when it dominates s and s does not dominate it. It does so as soon as t has a spare entry over the matching, or some matched entry strictly below its partner.

Equations

• t.StrictDominates s = (t.Dominates s ∧ ¬s.Dominates t)

theorem Multiset.StrictDominates.dominates {s t : Multiset ℕ} (h : t.StrictDominates s) : t.Dominates s

theorem Multiset.StrictDominates.ne_zero {s t : Multiset ℕ} (h : t.StrictDominates s) : t ≠ 0

theorem Multiset.invPowSum_le_invPowSum_of_rel {α : ℝ} {s t : Multiset ℕ} (hα : 0 ≤ α) (h : Rel (fun (x1 x2 : ℕ) => x1 ≤ x2) t s) : invPowSum α s ≤ invPowSum α t

theorem Multiset.Dominates.invPowSum_le {α : ℝ} {s t : Multiset ℕ} (h : t.Dominates s) (hα : 0 ≤ α) : invPowSum α s ≤ invPowSum α t

The Hall criterion

theorem Multiset.card_filter_le_card_filter_of_rel {s t : Multiset ℕ} (h : Rel (fun (x1 x2 : ℕ) => x1 ≤ x2) t s) (k : ℕ) : (filter (fun (x : ℕ) => x ≤ k) s).card ≤ (filter (fun (x : ℕ) => x ≤ k) t).card

theorem Multiset.Dominates.card_filter_le {s t : Multiset ℕ} (h : t.Dominates s) (k : ℕ) : (filter (fun (x : ℕ) => x ≤ k) s).card ≤ (filter (fun (x : ℕ) => x ≤ k) t).card

theorem Multiset.dominates_of_forall_mem {s t : Multiset ℕ} (h : ∀ k ∈ s, (filter (fun (x : ℕ) => x ≤ k) s).card ≤ (filter (fun (x : ℕ) => x ≤ k) t).card) : t.Dominates s

theorem Multiset.dominates_iff_forall_mem {s t : Multiset ℕ} : t.Dominates s ↔ ∀ k ∈ s, (filter (fun (x : ℕ) => x ≤ k) s).card ≤ (filter (fun (x : ℕ) => x ≤ k) t).card

theorem Multiset.dominates_iff_forall {s t : Multiset ℕ} : t.Dominates s ↔ ∀ (k : ℕ), (filter (fun (x : ℕ) => x ≤ k) s).card ≤ (filter (fun (x : ℕ) => x ≤ k) t).card

@[instance_reducible]

instance Multiset.decidableDominates : DecidableRel Dominates

Equations

• x✝¹.decidableDominates x✝ = decidable_of_iff (∀ k ∈ x✝, (Multiset.filter (fun (x : ℕ) => x ≤ k) x✝).card ≤ (Multiset.filter (fun (x : ℕ) => x ≤ k) x✝¹).card) ⋯

@[instance_reducible]

instance Multiset.decidableStrictDominates : DecidableRel StrictDominates

Equations

• x✝¹.decidableStrictDominates x✝ = { decide := decide (x✝¹.Dominates x✝) && decide ¬x✝.Dominates x✝¹, reflects_decide := ⋯ }

theorem Multiset.dominates_refl (s : Multiset ℕ) : s.Dominates s

Strict domination is strict on inverse-power sums

theorem Multiset.StrictDominates.invPowSum_lt {α : ℝ} {s t : Multiset ℕ} (h : t.StrictDominates s) (hα : 0 < α) (hs : 0 ∉ s) : invPowSum α s < invPowSum α t

Pairwise products

def Multiset.prodMul (s t : Multiset ℕ) : Multiset ℕ

The multiset of pairwise products of s and t.

Equations

• s.prodMul t = Multiset.map (fun (p : ℕ × ℕ) => p.1 * p.2) (s ×ˢ t)

@[simp]

theorem Multiset.zero_prodMul (t : Multiset ℕ) : prodMul 0 t = 0

@[simp]

theorem Multiset.cons_prodMul (n : ℕ) (s t : Multiset ℕ) : (n ::ₘ s).prodMul t = map (fun (x : ℕ) => n * x) t + s.prodMul t

@[simp]

theorem Multiset.card_prodMul (s t : Multiset ℕ) : (s.prodMul t).card = s.card * t.card

theorem Multiset.prodMul_eq_zero_iff {s t : Multiset ℕ} : s.prodMul t = 0 ↔ s = 0 ∨ t = 0

theorem Multiset.invPowSum_map_mul {α : ℝ} (hα : 0 ≤ α) (n : ℕ) (t : Multiset ℕ) : invPowSum α (map (fun (x : ℕ) => n * x) t) = (↑n)⁻¹ ^ α * invPowSum α t

theorem Multiset.invPowSum_prodMul {α : ℝ} (hα : 0 ≤ α) (s t : Multiset ℕ) : invPowSum α (s.prodMul t) = invPowSum α s * invPowSum α t

theorem Multiset.zero_notMem_prodMul {s t : Multiset ℕ} (hs : 0 ∉ s) (ht : 0 ∉ t) : 0 ∉ s.prodMul t

Common-denominator power sums

def Multiset.divPowSum (D k : ℕ) (m : Multiset ℕ) : ℕ

The sum of (D / n)ᵏ over m. When every entry divides D it is invPowSum k m with the common denominator Dᵏ cleared.

Equations

• Multiset.divPowSum D k m = (Multiset.map (fun (n : ℕ) => (D / n) ^ k) m).sum

@[simp]

theorem Multiset.divPowSum_zero (D k : ℕ) : divPowSum D k 0 = 0

theorem Multiset.ne_zero_of_divPowSum_ne_zero {m : Multiset ℕ} {D k : ℕ} (h : divPowSum D k m ≠ 0) : m ≠ 0

theorem Multiset.divPowSum_pos {m : Multiset ℕ} {D k : ℕ} (hD : D ≠ 0) (h : ∀ n ∈ m, n ∣ D) (hm : m ≠ 0) : 0 < divPowSum D k m

theorem Multiset.invPowSum_mul_pow_eq_divPowSum {D : ℕ} (hD : D ≠ 0) (k : ℕ) {m : Multiset ℕ} (h : ∀ n ∈ m, n ∣ D) : invPowSum (↑k) m * ↑D ^ k = ↑(divPowSum D k m)

At a natural exponent, invPowSum times the common denominator Dᵏ is divPowSum.

theorem Multiset.invPowSum_replicate (α : ℝ) (m n : ℕ) : invPowSum α (replicate m n) = ↑m * (↑n)⁻¹ ^ α

theorem Multiset.invPowSum_toReal {α : ℝ} {m : Multiset ℕ} (hα : 0 ≤ α) (hm : 0 ∉ m) : (invPowSum α m).toReal = (map (fun (n : ℕ) => (↑n)⁻¹ ^ α) m).sum

theorem Multiset.invPowSum_toReal_eq {D : ℕ} (hD : D ≠ 0) (k : ℕ) {m : Multiset ℕ} (h : ∀ n ∈ m, n ∣ D) : (invPowSum (↑k) m).toReal = ↑(divPowSum D k m) / ↑D ^ k