feat: Positivity extension for Finset.prod (#9365)

Followup to #9365

From LeanAPAP



Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Alex J Best <[email protected]>

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

@@ -206,3 +206,61 @@ lemma IsAbsoluteValue.map_prod [CommSemiring R] [Nontrivial R] [LinearOrderedCom
 #align is_absolute_value.map_prod IsAbsoluteValue.map_prod
 
 end AbsoluteValue
+
+namespace Mathlib.Meta.Positivity
+open Qq Lean Meta Finset
+
+private alias ⟨_, prod_ne_zero⟩ := prod_ne_zero_iff
+
+/-- The `positivity` extension which proves that `∏ i in s, f i` is nonnegative if `f` is, and
+positive if each `f i` is.
+
+TODO: The following example does not work
+```
+example (s : Finset ℕ) (f : ℕ → ℤ) (hf : ∀ n, 0 ≤ f n) : 0 ≤ s.prod f := by positivity
+```
+because `compareHyp` can't look for assumptions behind binders.
+-/
+@[positivity Finset.prod _ _]
+def evalFinsetProd : PositivityExt where eval {u α} zα pα e := do
+  match e with
+  | ~q(@Finset.prod $ι _ $instα $s $f) =>
+    let i : Q($ι) ← mkFreshExprMVarQ q($ι) .syntheticOpaque
+    have body : Q($α) := Expr.betaRev f #[i]
+    let rbody ← core zα pα body
+    let _instαmon ← synthInstanceQ q(CommMonoidWithZero $α)
+
+    -- Try to show that the product is positive
+    let p_pos : Option Q(0 < $e) := ← do
+      let .positive pbody := rbody | pure none -- Fail if the body is not provably positive
+      -- TODO(quote4#38): We must name the following, else `assertInstancesCommute` loops.
+      let .some _instαzeroone ← trySynthInstanceQ q(ZeroLEOneClass $α) | pure none
+      let .some _instαposmul ← trySynthInstanceQ q(PosMulStrictMono $α) | pure none
+      let .some _instαnontriv ← trySynthInstanceQ q(Nontrivial $α) | pure none
+      assertInstancesCommute
+      let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars #[i] pbody (binderInfoForMVars := .default)
+      return some q(prod_pos fun i _ ↦ $pr i)
+    if let some p_pos := p_pos then return .positive p_pos
+
+    -- Try to show that the product is nonnegative
+    let p_nonneg : Option Q(0 ≤ $e) := ← do
+      let .some pbody := rbody.toNonneg
+        | return none -- Fail if the body is not provably nonnegative
+      let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars #[i] pbody (binderInfoForMVars := .default)
+      -- TODO(quote4#38): We must name the following, else `assertInstancesCommute` loops.
+      let .some _instαzeroone ← trySynthInstanceQ q(ZeroLEOneClass $α) | pure none
+      let .some _instαposmul ← trySynthInstanceQ q(PosMulMono $α) | pure none
+      assertInstancesCommute
+      return some q(prod_nonneg fun i _ ↦ $pr i)
+    if let some p_nonneg := p_nonneg then return .nonnegative p_nonneg
+
+    -- Fall back to showing that the product is nonzero
+    let pbody ← rbody.toNonzero
+    let pr : Q(∀ i, $f i ≠ 0) ← mkLambdaFVars #[i] pbody (binderInfoForMVars := .default)
+    -- TODO(quote4#38): We must name the following, else `assertInstancesCommute` loops.
+    let _instαnontriv ← synthInstanceQ q(Nontrivial $α)
+    let _instαnozerodiv ← synthInstanceQ q(NoZeroDivisors $α)
+    assertInstancesCommute
+    return .nonzero q(prod_ne_zero fun i _ ↦ $pr i)
+
+end Mathlib.Meta.Positivity

Mathlib/Analysis/Analytic/Composition.lean

@@ -331,9 +331,7 @@ the norms of the relevant bits of `q` and `p`. -/
 theorem compAlongComposition_norm {n : ℕ} (q : FormalMultilinearSeries 𝕜 F G)
     (p : FormalMultilinearSeries 𝕜 E F) (c : Composition n) :
     ‖q.compAlongComposition p c‖ ≤ ‖q c.length‖ * ∏ i, ‖p (c.blocksFun i)‖ :=
-  ContinuousMultilinearMap.opNorm_le_bound _
-    (mul_nonneg (norm_nonneg _) (Finset.prod_nonneg fun _i _hi => norm_nonneg _))
-    (compAlongComposition_bound _ _ _)
+  ContinuousMultilinearMap.opNorm_le_bound _ (by positivity) (compAlongComposition_bound _ _ _)
 #align formal_multilinear_series.comp_along_composition_norm FormalMultilinearSeries.compAlongComposition_norm
 
 theorem compAlongComposition_nnnorm {n : ℕ} (q : FormalMultilinearSeries 𝕜 F G)

Mathlib/Analysis/Analytic/Inverse.lean

@@ -476,8 +476,7 @@ theorem radius_rightInv_pos_of_radius_pos_aux2 {n : ℕ} (hn : 2 ≤ n + 1)
       gcongr
       apply (compAlongComposition_norm _ _ _).trans
       gcongr
-      · exact prod_nonneg fun j _ => norm_nonneg _
-      · apply hp
+      apply hp
     _ =
         I * a +
           I * C *

Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean

@@ -217,24 +217,18 @@ operation. -/
 theorem isBoundedLinearMap_prod_multilinear {E : ι → Type*} [∀ i, NormedAddCommGroup (E i)]
     [∀ i, NormedSpace 𝕜 (E i)] :
     IsBoundedLinearMap 𝕜 fun p : ContinuousMultilinearMap 𝕜 E F × ContinuousMultilinearMap 𝕜 E G =>
-      p.1.prod p.2 :=
-  { map_add := fun p₁ p₂ => by
-      ext1 m
-      rfl
-    map_smul := fun c p => by
-      ext1 m
-      rfl
-    bound :=
-      ⟨1, zero_lt_one, fun p => by
-        rw [one_mul]
-        apply ContinuousMultilinearMap.opNorm_le_bound _ (norm_nonneg _) _
-        intro m
-        rw [ContinuousMultilinearMap.prod_apply, norm_prod_le_iff]
-        constructor
-        · exact (p.1.le_opNorm m).trans (mul_le_mul_of_nonneg_right (norm_fst_le p)
-            (Finset.prod_nonneg fun i _ => norm_nonneg _))
-        · exact (p.2.le_opNorm m).trans (mul_le_mul_of_nonneg_right (norm_snd_le p)
-            (Finset.prod_nonneg fun i _ => norm_nonneg _))⟩ }
+      p.1.prod p.2 where
+  map_add p₁ p₂ := by ext : 1; rfl
+  map_smul c p := by ext : 1; rfl
+  bound := by
+    refine ⟨1, zero_lt_one, fun p ↦ ?_⟩
+    rw [one_mul]
+    apply ContinuousMultilinearMap.opNorm_le_bound _ (norm_nonneg _) _
+    intro m
+    rw [ContinuousMultilinearMap.prod_apply, norm_prod_le_iff]
+    constructor
+    · exact (p.1.le_opNorm m).trans (mul_le_mul_of_nonneg_right (norm_fst_le p) <| by positivity)
+    · exact (p.2.le_opNorm m).trans (mul_le_mul_of_nonneg_right (norm_snd_le p) <| by positivity)
 #align is_bounded_linear_map_prod_multilinear isBoundedLinearMap_prod_multilinear
 
 /-- Given a fixed continuous linear map `g`, associating to a continuous multilinear map `f` the

Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

@@ -241,10 +241,8 @@ continuous. -/
 theorem continuous_of_bound (C : ℝ) (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) : Continuous f := by
   let D := max C 1
   have D_pos : 0 ≤ D := le_trans zero_le_one (le_max_right _ _)
-  replace H : ∀ m, ‖f m‖ ≤ D * ∏ i, ‖m i‖ := by
-    intro m
-    apply le_trans (H m) (mul_le_mul_of_nonneg_right (le_max_left _ _) _)
-    exact prod_nonneg fun (i : ι) _ => norm_nonneg (m i)
+  replace H (m) : ‖f m‖ ≤ D * ∏ i, ‖m i‖ :=
+    (H m).trans (mul_le_mul_of_nonneg_right (le_max_left _ _) <| by positivity)
   refine' continuous_iff_continuousAt.2 fun m => _
   refine'
     continuousAt_of_locally_lipschitz zero_lt_one
@@ -362,7 +360,7 @@ variable {f m}
 theorem le_mul_prod_of_le_opNorm_of_le {C : ℝ} {b : ι → ℝ} (hC : ‖f‖ ≤ C) (hm : ∀ i, ‖m i‖ ≤ b i) :
     ‖f m‖ ≤ C * ∏ i, b i :=
   (f.le_opNorm m).trans <| mul_le_mul hC (prod_le_prod (fun _ _ ↦ norm_nonneg _) fun _ _ ↦ hm _)
-    (prod_nonneg fun _ _ ↦ norm_nonneg _) ((opNorm_nonneg _).trans hC)
+    (by positivity) ((opNorm_nonneg _).trans hC)
 
 @[deprecated] alias le_mul_prod_of_le_op_norm_of_le := le_mul_prod_of_le_opNorm_of_le -- 2024-02-02
 
@@ -400,8 +398,7 @@ theorem le_of_opNorm_le {C : ℝ} (h : ‖f‖ ≤ C) : ‖f m‖ ≤ C * ∏ i,
 variable (f)
 
 theorem ratio_le_opNorm : (‖f m‖ / ∏ i, ‖m i‖) ≤ ‖f‖ :=
-  div_le_of_nonneg_of_le_mul (prod_nonneg fun _ _ => norm_nonneg _) (opNorm_nonneg _)
-    (f.le_opNorm m)
+  div_le_of_nonneg_of_le_mul (by positivity) (opNorm_nonneg _) (f.le_opNorm m)
 #align continuous_multilinear_map.ratio_le_op_norm ContinuousMultilinearMap.ratio_le_opNorm
 
 @[deprecated] alias ratio_le_op_norm := ratio_le_opNorm -- deprecated on 2024-02-02
@@ -768,9 +765,8 @@ theorem MultilinearMap.mkContinuous_norm_le (f : MultilinearMap 𝕜 E G) {C : 
 nonnegative. -/
 theorem MultilinearMap.mkContinuous_norm_le' (f : MultilinearMap 𝕜 E G) {C : ℝ}
     (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) : ‖f.mkContinuous C H‖ ≤ max C 0 :=
-  ContinuousMultilinearMap.opNorm_le_bound _ (le_max_right _ _) fun m =>
-    (H m).trans <|
-      mul_le_mul_of_nonneg_right (le_max_left _ _) (prod_nonneg fun _ _ => norm_nonneg _)
+  ContinuousMultilinearMap.opNorm_le_bound _ (le_max_right _ _) fun m ↦ (H m).trans <|
+    mul_le_mul_of_nonneg_right (le_max_left _ _) <| by positivity
 #align multilinear_map.mk_continuous_norm_le' MultilinearMap.mkContinuous_norm_le'
 
 namespace ContinuousMultilinearMap
@@ -1029,8 +1025,7 @@ def flipMultilinear (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G') :
           LinearMap.mkContinuous_apply, Pi.smul_apply, AddHom.coe_mk] }
     ‖f‖ fun m => by
       dsimp only [MultilinearMap.coe_mk]
-      refine LinearMap.mkContinuous_norm_le _
-        (mul_nonneg (norm_nonneg f) (prod_nonneg fun i _ => norm_nonneg (m i))) _
+      exact LinearMap.mkContinuous_norm_le _ (by positivity) _
 #align continuous_linear_map.flip_multilinear ContinuousLinearMap.flipMultilinear
 #align continuous_linear_map.flip_multilinear_apply_apply ContinuousLinearMap.flipMultilinear_apply_apply
 
@@ -1103,7 +1098,7 @@ def mkContinuousMultilinear (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G
       simp only [coe_mk]
       refine ((f m).mkContinuous_norm_le' _).trans_eq ?_
       rw [max_mul_of_nonneg, zero_mul]
-      exact prod_nonneg fun _ _ => norm_nonneg _
+      positivity
 #align multilinear_map.mk_continuous_multilinear MultilinearMap.mkContinuousMultilinear
 
 @[simp]
@@ -1134,7 +1129,7 @@ set_option linter.uppercaseLean3 false
 
 theorem norm_compContinuousLinearMap_le (g : ContinuousMultilinearMap 𝕜 E₁ G)
     (f : ∀ i, E i →L[𝕜] E₁ i) : ‖g.compContinuousLinearMap f‖ ≤ ‖g‖ * ∏ i, ‖f i‖ :=
-  opNorm_le_bound _ (mul_nonneg (norm_nonneg _) <| prod_nonneg fun i _ => norm_nonneg _) fun m =>
+  opNorm_le_bound _ (by positivity) fun m =>
     calc
       ‖g fun i => f i (m i)‖ ≤ ‖g‖ * ∏ i, ‖f i (m i)‖ := g.le_opNorm _
       _ ≤ ‖g‖ * ∏ i, ‖f i‖ * ‖m i‖ :=
@@ -1194,7 +1189,7 @@ theorem compContinuousLinearMapL_apply (g : ContinuousMultilinearMap 𝕜 E₁ G
 variable (G) in
 theorem norm_compContinuousLinearMapL_le (f : ∀ i, E i →L[𝕜] E₁ i) :
     ‖compContinuousLinearMapL (G := G) f‖ ≤ ∏ i, ‖f i‖ :=
-  LinearMap.mkContinuous_norm_le _ (prod_nonneg fun _ _ => norm_nonneg _) _
+  LinearMap.mkContinuous_norm_le _ (by positivity) _
 #align continuous_multilinear_map.norm_comp_continuous_linear_mapL_le ContinuousMultilinearMap.norm_compContinuousLinearMapL_le
 
 /-- `ContinuousMultilinearMap.compContinuousLinearMap` as a bundled continuous linear map.
@@ -1369,8 +1364,6 @@ addition of `Finset.prod` where needed). The duplication could be avoided by ded
 case from the multilinear case via a currying isomorphism. However, this would mess up imports,
 and it is more satisfactory to have the simplest case as a standalone proof. -/
 instance completeSpace [CompleteSpace G] : CompleteSpace (ContinuousMultilinearMap 𝕜 E G) := by
-  have nonneg : ∀ v : ∀ i, E i, 0 ≤ ∏ i, ‖v i‖ := fun v =>
-    Finset.prod_nonneg fun i _ => norm_nonneg _
   -- We show that every Cauchy sequence converges.
   refine' Metric.complete_of_cauchySeq_tendsto fun f hf => _
   -- We now expand out the definition of a Cauchy sequence,
@@ -1379,12 +1372,13 @@ instance completeSpace [CompleteSpace G] : CompleteSpace (ContinuousMultilinearM
   have cau : ∀ v, CauchySeq fun n => f n v := by
     intro v
     apply cauchySeq_iff_le_tendsto_0.2 ⟨fun n => b n * ∏ i, ‖v i‖, _, _, _⟩
-    · intro
-      exact mul_nonneg (b0 _) (nonneg v)
+    · intro n
+      have := b0 n
+      positivity
     · intro n m N hn hm
       rw [dist_eq_norm]
       apply le_trans ((f n - f m).le_opNorm v) _
-      exact mul_le_mul_of_nonneg_right (b_bound n m N hn hm) (nonneg v)
+      exact mul_le_mul_of_nonneg_right (b_bound n m N hn hm) <| by positivity
     · simpa using b_lim.mul tendsto_const_nhds
   -- We assemble the limits points of those Cauchy sequences
   -- (which exist as `G` is complete)
@@ -1409,7 +1403,7 @@ instance completeSpace [CompleteSpace G] : CompleteSpace (ContinuousMultilinearM
     have A : ∀ n, ‖f n v‖ ≤ (b 0 + ‖f 0‖) * ∏ i, ‖v i‖ := by
       intro n
       apply le_trans ((f n).le_opNorm _) _
-      apply mul_le_mul_of_nonneg_right _ (nonneg v)
+      apply mul_le_mul_of_nonneg_right _ <| by positivity
       calc
         ‖f n‖ = ‖f n - f 0 + f 0‖ := by
           congr 1
@@ -1429,7 +1423,7 @@ instance completeSpace [CompleteSpace G] : CompleteSpace (ContinuousMultilinearM
     have A : ∀ᶠ m in atTop, ‖(f n - f m) v‖ ≤ b n * ∏ i, ‖v i‖ := by
       refine' eventually_atTop.2 ⟨n, fun m hm => _⟩
       apply le_trans ((f n - f m).le_opNorm _) _
-      exact mul_le_mul_of_nonneg_right (b_bound n m n le_rfl hm) (nonneg v)
+      exact mul_le_mul_of_nonneg_right (b_bound n m n le_rfl hm) <| by positivity
     have B : Tendsto (fun m => ‖(f n - f m) v‖) atTop (𝓝 ‖(f n - Fcont) v‖) :=
       Tendsto.norm (tendsto_const_nhds.sub (hF v))
     exact le_of_tendsto B A

Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean

@@ -63,8 +63,7 @@ theorem ContinuousLinearMap.norm_map_tail_le
     ‖f (m 0) (tail m)‖ ≤ ‖f‖ * ∏ i, ‖m i‖ :=
   calc
     ‖f (m 0) (tail m)‖ ≤ ‖f (m 0)‖ * ∏ i, ‖(tail m) i‖ := (f (m 0)).le_opNorm _
-    _ ≤ ‖f‖ * ‖m 0‖ * ∏ i, ‖(tail m) i‖ :=
-      (mul_le_mul_of_nonneg_right (f.le_opNorm _) (prod_nonneg fun _ _ => norm_nonneg _))
+    _ ≤ ‖f‖ * ‖m 0‖ * ∏ i, ‖tail m i‖ := mul_le_mul_of_nonneg_right (f.le_opNorm _) <| by positivity
     _ = ‖f‖ * (‖m 0‖ * ∏ i, ‖(tail m) i‖) := by ring
     _ = ‖f‖ * ∏ i, ‖m i‖ := by
       rw [prod_univ_succ]
@@ -269,8 +268,7 @@ def ContinuousMultilinearMap.curryRight (f : ContinuousMultilinearMap 𝕜 Ei G)
         simp }
   f'.mkContinuous ‖f‖ fun m => by
     simp only [f', MultilinearMap.coe_mk]
-    exact LinearMap.mkContinuous_norm_le _
-      (mul_nonneg (norm_nonneg _) (prod_nonneg fun _ _ => norm_nonneg _)) _
+    exact LinearMap.mkContinuous_norm_le _ (by positivity) _
 #align continuous_multilinear_map.curry_right ContinuousMultilinearMap.curryRight
 
 @[simp]

Mathlib/Data/Nat/Choose/Multinomial.lean

@@ -65,7 +65,7 @@ lemma multinomial_cons (ha : a ∉ s) (f : α → ℕ) :
     multinomial, mul_assoc, mul_left_comm _ (f a)!,
     Nat.div_mul_cancel (prod_factorial_dvd_factorial_sum _ _), ← mul_assoc, Nat.choose_symm_add,
     Nat.add_choose_mul_factorial_mul_factorial, Finset.sum_cons]
-  exact prod_pos fun i _ ↦ by positivity
+  positivity
 
 lemma multinomial_insert [DecidableEq α] (ha : a ∉ s) (f : α → ℕ) :
     multinomial (insert a s) f = (f a + ∑ i in s, f i).choose (f a) * multinomial s f := by

Mathlib/Data/Nat/Factorial/BigOperators.lean

@@ -28,8 +28,7 @@ lemma monotone_factorial : Monotone factorial := fun _ _ => factorial_le
 
 variable {α : Type*} (s : Finset α) (f : α → ℕ)
 
-theorem prod_factorial_pos : 0 < ∏ i in s, (f i)! :=
-  Finset.prod_pos fun i _ => factorial_pos (f i)
+theorem prod_factorial_pos : 0 < ∏ i in s, (f i)! := by positivity
 #align nat.prod_factorial_pos Nat.prod_factorial_pos
 
 theorem prod_factorial_dvd_factorial_sum : (∏ i in s, (f i)!) ∣ (∑ i in s, f i)! := by

Mathlib/MeasureTheory/Integral/TorusIntegral.lean

@@ -199,8 +199,7 @@ theorem norm_torusIntegral_le_of_norm_le_const {C : ℝ} (hf : ∀ θ, ‖f (tor
           ‖(∏ i : Fin n, R i * exp (θ i * I) * I : ℂ) • f (torusMap c R θ)‖ =
               (∏ i : Fin n, |R i|) * ‖f (torusMap c R θ)‖ :=
             by simp [norm_smul]
-          _ ≤ (∏ i : Fin n, |R i|) * C :=
-            mul_le_mul_of_nonneg_left (hf _) (Finset.prod_nonneg fun _ _ => abs_nonneg _)
+          _ ≤ (∏ i : Fin n, |R i|) * C := mul_le_mul_of_nonneg_left (hf _) <| by positivity
     _ = ((2 * π) ^ (n : ℕ) * ∏ i, |R i|) * C := by
       simp only [Pi.zero_def, Real.volume_Icc_pi_toReal fun _ => Real.two_pi_pos.le, sub_zero,
         Fin.prod_const, mul_assoc, mul_comm ((2 * π) ^ (n : ℕ))]

test/positivity.lean

@@ -382,6 +382,27 @@ example (s : Finset ℕ) (f : ℕ → ℕ) (a : ℕ) : 0 ≤ s.sum (f a) := by p
 set_option linter.unusedVariables false in
 example (f : ℕ → ℕ) (hf : 0 ≤ f 0) : 0 ≤ ∑ n in Finset.range 10, f n := by positivity
 
+example (n : ℕ) : ∏ j in range n, (-1) ≠ 0 := by positivity
+example (n : ℕ) (a : ℕ → ℤ) : 0 ≤ ∏ j in range n, a j^2 := by positivity
+example (a : ULift.{2} ℕ → ℤ) (s : Finset (ULift.{2} ℕ)) : 0 ≤ ∏ j in s, a j^2 := by positivity
+example (n : ℕ) (a : ℕ → ℤ) : 0 ≤ ∏ j : Fin 8, ∏ i in range n, (a j^2 + i ^ 2) := by positivity
+example (n : ℕ) (a : ℕ → ℤ) : 0 < ∏ j : Fin (n + 1), (a j^2 + 1) := by positivity
+example (a : ℕ → ℤ) : 0 < ∏ j in ({1} : Finset ℕ), (a j^2 + 1) := by
+  have : Finset.Nonempty {1} := singleton_nonempty 1
+  positivity
+example (s : Finset ℕ) : 0 ≤ ∏ j in s, j := by positivity
+example (s : Finset ℕ) : 0 ≤ s.sum id := by positivity
+example (s : Finset ℕ) (f : ℕ → ℕ) (a : ℕ) : 0 ≤ s.sum (f a) := by positivity
+
+-- Make sure that the extension doesn't produce an invalid term by accidentally unifying `?n` with
+-- `0` because of the `hf` assumption
+set_option linter.unusedVariables false in
+example (f : ℕ → ℕ) (hf : 0 ≤ f 0) : 0 ≤ ∏ n in Finset.range 10, f n := by positivity
+
+-- Make sure that `positivity` isn't too greedy by trying to prove that a product is positive
+-- because its body is even if multiplication isn't strictly monotone
+example [OrderedCommSemiring α] {a : α} (ha : 0 < a) : 0 ≤ ∏ _i in {(0 : α)}, a := by positivity
+
 /- ## Other extensions -/
 
 example [Zero β] [PartialOrder β] [FunLike F α β] [NonnegHomClass F α β]