prod_le_pow_card

Stream: mathlib4

[Winston Yin (尹維晨)]

I have found prod_le_pow_card (for List, Multiset, Finset) quite difficult to use.

import Mathlib

example {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {n : ℕ} (x : Fin n → E) {C : ℝ} (hC : 0 ≤ C) :
    ∏ i : Fin n, ‖x i‖ ≤ C ^ (Finset.univ : Finset (Fin n)).card := by
  apply Finset.prod_le_pow_card -- error
  sorry

We can't apply Finset.prod_le_pow_card here unless we first construct C and ‖x i‖ as ℝ≥0. I'm unfamiliar with the typeclasses in Mathlib.Algebra.Order.BigOperators.Group.Finset, so I'm hesitant to make a PR, but here's a suggestion for a useful lemma:

lemma Finset.prod_le_pow_card' {ι : Type*} {R : Type*} [CommMonoidWithZero R]
    [PartialOrder R] [ZeroLEOneClass R] [PosMulMono R] {f : ι → R} {s : Finset ι} {n : R}
    (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ n) :
    s.prod f ≤ n ^ s.card :=
  (Finset.prod_le_prod h0 h1).trans_eq (Finset.prod_const n)

This can be applied in the example above. I have not seen the existing Finset.prod_le_pow_card used in too many places yet.

I faced similar problems when using mul_lt_one and all its friends, so either I'm missing something simple, or this is indeed not user friendly.

[Kevin Buzzard]

docs#Finset.prod_le_pow_card

[Kevin Buzzard]

I guess conversely your result doesn't imply Finset.prod_le_pow_card because you demand a 0 in your monoid so it won't apply to e.g. PNat. I don't see any harm in having both.

Hmm, on looking through mathlib though, there might indeed be an argument for replacing the current versions with your version. As you point out these results are rarely used; in fact they seem to be used twice (other than when proving one version from another); the first is in Analysis/Normed/Unbundled/SpectralNorm.lean and it's here:

      have : (map f t).prod ≤ f y ^ (p.natDegree - m) := by
        set g : L → NNReal := fun x ↦ ⟨f x, apply_nonneg f x⟩
        have h_card : p.natDegree - m = card (t.map g) := by rw [card_map, ht_card, ← hps]
        have hx_le : ∀ x : NNReal, x ∈ map g t → x ≤ g y := by
          intro r hr
          obtain ⟨_, hzt, hzr⟩ := mem_map.mp hr
          exact hzr ▸ hy_max _ (hts _ hzt)
        have : (map g t).prod ≤ g y ^ (p.natDegree - m) := h_card ▸ prod_le_pow_card _ _ hx_le
        simpa [g, ← NNReal.coe_le_coe, NNReal.coe_pow, NNReal.coe_mk, NNReal.coe_multiset_prod,
          map_map, Function.comp_apply, NNReal.coe_mk] using this

which as far as I can see, says "we want Finset.prod_le_pow_card' but it doesn't exist, so we explicitly rewrite everything into NNReal, apply Finset.prod_le_pow_card and then deduce what we want". Can you golf this proof with Finset.prod_le_pow_card'?

The second is in Topology/Algebra/Polynomial.lean and again it looks like we're going through some song and dance to reduce to a situation where the current lemma applies. It's here

  lift B to ℝ≥0 using hB
  rw [← coe_nnnorm, ← NNReal.coe_pow, NNReal.coe_le_coe, ← nnnormHom_apply, ← MonoidHom.coe_coe,
    MonoidHom.map_multiset_prod]
  refine (prod_le_pow_card _ B fun x hx => ?_).trans_eq (by rw [card_map, hs.2])

and again the question is about reals and is painfully coerced into nonnegative reals (this is essentially the end of the proof).

So my instinct is that if you change all three of the mathlib definitions to your proposed ones and then find that you're able to golf these two proofs, then this is a great argument for replacing our current lemma with your proposal. If people say "but there are possible applications to PNat which we don't have any of but which we're losing" then you could rename the old lemma as a primed lemma. I'm not entirely sure how the deprecation would work there though.

[Winston Yin (尹維晨)]

Thank you! Pulling on this loose thread is unravelling a lot of convenient lemmas of this nature that are missing. I'll just add my Finset.prod_le_pow_card' for now and carefully find these missing lemmas after the current project.

[Kevin Buzzard]

If you add it in a PR then see if you can golf the proofs, esp the one in SpectralNorm.lean because it might literally be a case of "I can replace 10 lines by 1 line" which would be a nice justification for the PR.

[Eric Wieser]

Perhaps it should be _of_nonneg instead of '

[Winston Yin (尹維晨)]

I've created #34120. It seems that the existing naming scheme is to add a subscript 0 to the lemmas assuming CommMonoidWithZero.