Commit 2024-05-07 23:13 ba9d411b

View on Github →

feat: Positivity extension for Finset.prod (#9365) Followup to #9365 From LeanAPAP

Estimated changes

Modified Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean

added def Mathlib.Meta.Positivity.evalFinsetProd

Modified Mathlib/Analysis/Analytic/Composition.lean

Modified Mathlib/Analysis/Analytic/Inverse.lean

Modified Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

Modified Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean

Modified Mathlib/Data/Nat/Choose/Multinomial.lean

Modified Mathlib/Data/Nat/Factorial/BigOperators.lean

modified theorem Nat.prod_factorial_pos

Modified Mathlib/MeasureTheory/Integral/TorusIntegral.lean

Modified test/positivity.lean