From ba9d411b0518c2de8057c3488cbfbf68ce5e5439 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Tue, 7 May 2024 23:13:53 +0000 Subject: [PATCH] feat: Positivity extension for `Finset.prod` (#9365) Followup to #9365 From LeanAPAP Co-authored-by: Eric Wieser Co-authored-by: Alex J Best --- .../Order/BigOperators/Ring/Finset.lean | 58 +++++++++++++++++++ Mathlib/Analysis/Analytic/Composition.lean | 4 +- Mathlib/Analysis/Analytic/Inverse.lean | 3 +- .../NormedSpace/BoundedLinearMaps.lean | 30 ++++------ .../NormedSpace/Multilinear/Basic.lean | 38 +++++------- .../NormedSpace/Multilinear/Curry.lean | 6 +- Mathlib/Data/Nat/Choose/Multinomial.lean | 2 +- Mathlib/Data/Nat/Factorial/BigOperators.lean | 3 +- .../MeasureTheory/Integral/TorusIntegral.lean | 3 +- test/positivity.lean | 21 +++++++ 10 files changed, 114 insertions(+), 54 deletions(-) diff --git a/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean b/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean index 1c8f13e1aa0a1..5ba5ee09a25db 100644 --- a/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean +++ b/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 diff --git a/Mathlib/Analysis/Analytic/Composition.lean b/Mathlib/Analysis/Analytic/Composition.lean index 2d23fb07258b2..5da081023ea5f 100644 --- a/Mathlib/Analysis/Analytic/Composition.lean +++ b/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) diff --git a/Mathlib/Analysis/Analytic/Inverse.lean b/Mathlib/Analysis/Analytic/Inverse.lean index b51b9dac274f1..f0d914db19b87 100644 --- a/Mathlib/Analysis/Analytic/Inverse.lean +++ b/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 * diff --git a/Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean b/Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean index 455de6a2ef748..c2be04a15b2ba 100644 --- a/Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean +++ b/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 diff --git a/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean b/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean index 74b5d188840b4..0dc7f02aed35f 100644 --- a/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean +++ b/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 diff --git a/Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean b/Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean index e085b0f9e8c0b..b5896ae869221 100644 --- a/Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean +++ b/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] diff --git a/Mathlib/Data/Nat/Choose/Multinomial.lean b/Mathlib/Data/Nat/Choose/Multinomial.lean index a9e0378d8566d..27a01d251fb26 100644 --- a/Mathlib/Data/Nat/Choose/Multinomial.lean +++ b/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 diff --git a/Mathlib/Data/Nat/Factorial/BigOperators.lean b/Mathlib/Data/Nat/Factorial/BigOperators.lean index 74c65728722a5..3d7cf6af12894 100644 --- a/Mathlib/Data/Nat/Factorial/BigOperators.lean +++ b/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 diff --git a/Mathlib/MeasureTheory/Integral/TorusIntegral.lean b/Mathlib/MeasureTheory/Integral/TorusIntegral.lean index b56d0f5fe3046..d3e3ce6ef54e3 100644 --- a/Mathlib/MeasureTheory/Integral/TorusIntegral.lean +++ b/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 : ℕ))] diff --git a/test/positivity.lean b/test/positivity.lean index 3150b776d1a80..5e58a2e5776d3 100644 --- a/test/positivity.lean +++ b/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 α β]