Reusing `finset.prod` facts for lists

Stream: general

[Yury G. Kudryashov]

Hi, is there any good way to reuse facts about finset.prod for lists? E.g., I'd like to have something like ∀ l : list α, (fin_range (length l)).prod (λ i, l.nth_le i.1 i.2) = l.prod.

[Yury G. Kudryashov]

My problem is that it's not easy to apply general facts about products/sums over finsets (e.g., AM-GM inequality) to get a similar inequality for products/sums over lists.

[Yury G. Kudryashov]

With lists it's much easier to apply it to specific numbers (e.g., to deduce AM-GM for 2, 3, 4 numbers out of the general case).

[Mario Carneiro]

I guess that theorem is possible (assuming the multiplication is commutative and associative), but the LHS looks pretty hard to work with

[Mario Carneiro]

You can always coerce a list to a finset and apply the prod operation there

[Yury G. Kudryashov]

Does coercion remove duplicates?

[Johan Commelin]

I guess it does.

[Kevin Buzzard]

You could coerce to a multiset and apply the prod operation there.

[Chris Hughes]

For every list A there's a function fin n - > A, so you can finset.sum univ over this function.

[Kevin Buzzard]

...and that's the reason why nobody bothers to build any more infrastructure for sums over lists and multisets ;-)

[Chris Hughes]

That's true for multisets. You still need lists for non commutative products.

[Yury G. Kudryashov]

@Chris Hughes I wrote one such function above. However I'd like to have a theorem like ∀ l : list α, (fin_range (length l)).prod (λ i, l.nth_le i.1 i.2) = l.prod or ∀ (l : list α) (f : α → β), (fin_range (length l)).prod (λ i, f(l.nth_le) i.1 i.2) = (l.map f).prod to be able to transfer facts from sums/prods over a finset to sums/prods of list.map.

[Yury G. Kudryashov]

Another way to deduce ∀ a b c wa wb wc : nnreal, wa + wb + wc = 1 → a^wa * b^wb * c^wc ≤ wa * a + wb * b + wc * c from ∀ {α : Type*} (s : finset α) (w z : α → ℝ≥0) (hw' : s.sum w = 1) : (s.prod (λ i, (z i) ^ (w i))) ≤ s.sum (λ i, w i * z i) is welcome. Here I assume has_pow nnreal nnreal := ⟨λ x r, nnreal.of_real (x:ℝ)^(r:ℝ)⟩.

[Yury G. Kudryashov]

With lists I can do this:

noncomputable instance nnreal.has_pow_nnreal : has_pow ℝ≥0 ℝ≥0 := ⟨λ p r, nnreal.of_real $ (p:ℝ)^(r:ℝ)⟩

theorem list.am_gm_weighted (l : list (ℝ≥0 × ℝ≥0)) (hw : (l.map prod.fst).sum = 1) :
  (l.map (λ i, (i.snd) ^ (i.fst) : ℝ≥0 × ℝ≥0 → ℝ≥0)).prod ≤
    (l.map (λ i, i.fst * i.snd : ℝ≥0 × ℝ≥0 → ℝ≥0)).sum :=
sorry

theorem am_gm3 (w₁ w₂ w₃ : ℝ≥0) (hw : w₁ + w₂ + w₃ = 1) (x₁ x₂ x₃ : ℝ≥0) :
  x₁ ^ w₁ * x₂ ^ w₂ * x₃ ^ w₃ ≤ w₁ * x₁ + w₂ * x₂ + w₃ * x₃ :=
by simpa [mul_assoc] using list.am_gm_weighted [(w₁, x₁), (w₂, x₂), (w₃, x₃)] (by simpa using hw)

However I can't quickly deduce am_gm3 from

theorem finset.am_gm_weighted {α : Type*} (s : finset α) (w z : α → ℝ≥0)
  (hw : s.sum w = 1) : s.prod (λ i, (z i) ^ (w i)) ≤ s.sum (λ i, w i * z i) :=

[Kevin Buzzard]

∀ l : list α, (fin_range (length l)).prod (λ i, l.nth_le i.1 i.2) = l.prod doesn't compile -- Lean can't find ⊢ has_one (fin (length l)). These things should surely be easy to prove by induction on l right?

[Kevin Buzzard]

failed to synthesize type class instance for
x r : ℝ≥0
⊢ has_pow ℝ ℝ

I can't get anything to work

[Kevin Buzzard]

But I see your point. A finset is not enough here because of duplicates. You need to use this finset.sum univ trick of Chris I guess.

[Mario Carneiro]

I think we need an ergonomic way to form "fin n -> A" vectors from concrete lists of values, i.e. vector.cons

[Mario Carneiro]

that would solve this problem

[Mario Carneiro]

I also can't find an instance of has_pow nnreal nnreal. Was this added at some point?

[Yury G. Kudryashov]

No, that's why I define it in my code.

[Mario Carneiro]

that's not very MWE

[Yury G. Kudryashov]

For an MWE, let's one can try to deduce

lemma list.prod_mul {α : Type*} [comm_monoid α] (l : list (α × α)) : (l.map (λ i, i.fst * i.snd : α × α → α)).prod = (l.map prod.fst).prod * (l.map prod.snd).prod := sorry

from the corresponding fact about finsets

[Yury G. Kudryashov]

Or, say, deduce ∀ a b c x y z, (a * b * c) * (x * y * z) = ((a * x) * (b * y) * (c * z)) from finset.prod_mul_distrib.

[Mario Carneiro]

actually, I was going to show how to prove your original theorem, the am_gm for 3 things from the general am_gm on finsets

[Yury G. Kudryashov]

Here is what I have for a real - finset version:

theorem finset.am_gm_weighted {α : Type*} (s : finset α) (w z : α → ℝ)
  (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : s.sum w = 1) (hz : ∀ i ∈ s, 0 ≤ z i) :
  s.prod (λ i, (z i) ^ (w i)) ≤ s.sum (λ i, w i * z i) :=
sorry

[Mario Carneiro]

This seems to work well:

import algebra.big_operators algebra.group_power data.real.nnreal data.fin

section end
open_locale nnreal

@[instance] constant nnreal.has_pow_nnreal : has_pow ℝ≥0 ℝ≥0

axiom finset.am_gm_weighted {α : Type*} (s : finset α) (w z : α → ℝ≥0)
  (hw : s.sum w = 1) : s.prod (λ i, (z i) ^ (w i)) ≤ s.sum (λ i, w i * z i)

theorem finset.prod_fin_succ {α} [comm_monoid α] {n} (f : fin (n+1) → α) :
  finset.univ.prod f = f 0 * finset.univ.prod (λ i:fin n, f i.succ) := sorry
theorem finset.sum_fin_succ {α} [add_comm_monoid α] {n} (f : fin (n+1) → α) :
  finset.univ.sum f = f 0 + finset.univ.sum (λ i:fin n, f i.succ) := sorry

theorem am_gm3 {a b c wa wb wc : nnreal} :
  wa + wb + wc = 1 → a^wa * b^wb * c^wc ≤ wa * a + wb * b + wc * c :=
begin
  have := finset.am_gm_weighted (@finset.univ (fin 3) _)
    (fin.cons wa (fin.cons wb (λ _, wc)))
    (fin.cons a (fin.cons b (λ _, c))),
  simpa [finset.prod_fin_succ, finset.sum_fin_succ, mul_assoc]
end