Commit 2021-03-06 21:16 df1e6f92

refactor(data/{finset,multiset}): move inductions proofs on sum/prod from finset to multiset, add more induction lemmas (#6561) The starting point is finset.le_sum_of_subadditive, which is extended in several ways:

• It is written in multiplicative form, and a [to_additive] attribute generates the additive version,
• It is proven for multiset, which is then used for the proof of the finset case.
• For multiset, some lemmas are written for foldr/foldl (and prod is a foldr).
• Versions of these lemmas specialized to nonempty sets are provided. These don't need the initial hypothesis f 1 = 1/f 0 = 0.
• The new ..._on_pred lemmas like finset.le_sum_of_subadditive_on_pred apply to functions that are only sub-additive for arguments that verify some property. I included an application of this with snorm_sum_le, which uses that the Lp seminorm is subadditive on a.e.-measurable functions. Those on_pred lemmas could be avoided by constructing the submonoid given by the predicate, then using the standard subadditive result, but I find convenient to be able to use them directly.