Inverse-power sums over multisets of naturals

Multiset.invPowSum α m sums n⁻ᵅ over m. t.Dominates s says some submultiset of t matches s element-for-element with each matched entry of t at most its partner in s; that alone forces s.invPowSum α ≤ t.invPowSum α simultaneously for every exponent 0 ≤ α. t.StrictDominates s adds ¬ s.Dominates t, which makes the inequality strict for every 0 < α.

Domination is equivalent to a Hall-type counting condition — s has no more entries below any threshold than t has — so it is first-order stochastic dominance of the counting distributions, decided with card s * (card s + card t) comparisons. Certificates therefore close by decide +kernel for multisets of a few hundred entries.

At a natural exponent k with every entry dividing a common denominator D, the sum clears to the ℕ-valued divPowSum D k, so pinned-exponent comparisons also close by decide.

Main results

• Multiset.Dominates.invPowSum_le, Multiset.StrictDominates.invPowSum_lt
• Multiset.dominates_iff_forall, Multiset.dominates_iff_forall_mem
• Multiset.invPowSum_prodMul
• Multiset.invPowSum_mul_pow_eq_divPowSum

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

t.Dominates s: some submultiset of t matches s element-for-element, 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

t.StrictDominates s: t dominates s but not conversely. By dominates_iff_forall this is strict first-order stochastic dominance of the counting distributions; it holds 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

Greedy matching: pair the least entry of s with any entry of t below it, which the counting condition supplies and which leaves the condition intact for what remains.

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✝ = Multiset.decidableStrictDominates._aux_1 x✝¹ x✝

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 ℕ-valued common-denominator form of invPowSum at a natural exponent: Σ (D/n)ᵏ over m. When every entry divides D, invPowSum k m is divPowSum D k m / Dᵏ exactly, so pinned-exponent comparisons clear to ℕ inequalities closed by decide.

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)

Clearing the common denominator: at a natural exponent, invPowSum times Dᵏ is the ℕ-valued 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

Evaluation form on reals, for symbolic or pinned exponents.

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

Real form of the common-denominator identity.

Certificates