[Merged by Bors] - feat: Positivity extension for Finset.prod

Mathlib/Algebra/BigOperators/Order.lean

@@ -830,3 +830,57 @@ theorem IsAbsoluteValue.map_prod [CommSemiring R] [Nontrivial R] [LinearOrderedC
 #align is_absolute_value.map_prod IsAbsoluteValue.map_prod
 
 end AbsoluteValue
+
+namespace Mathlib.Meta.Positivity
+open Qq Lean Meta Finset
+
+/-- The `positivity` extension which proves that `∑ i in s, f i` is nonnegative if `f` is, and
+positive if each `f i` is and `s` is nonempty.
+
+Note that this does not do any complicated reasoning. In particular, it does not try to feed in the
+`i ∈ s` hypothesis to local assumptions, and the only ways it can prove `s` is nonempty is if there
+is a local `s.Nonempty` hypothesis or `s = (univ : Finset α)` and `Nonempty α` can be synthesized by
+TC inference. -/
+@[positivity Finset.sum _ _]
+def evalFinsetSum : PositivityExt where eval {u α} zα pα e := do
+  match e with
+  | ~q(@Finset.sum _ $ι $instα $s $f) =>
+    let (lhs, _, (rhs : Q($α))) ← lambdaMetaTelescope (if f.isLambda then f else q(fun x => $f x))
+     -- TODO: The following annotation is ignored. See leanprover/lean4#3126
+    let so : Option Q(Finset.Nonempty $s) ← do
+      try
+        match s with
+        | ~q(@univ _ $fi) => do
+          -- TODO(Qq): doesn't type-check without explicit `u`, even though it works outside the
+          -- `match`.
+          let _no ← synthInstanceQ (u := 0) q(Nonempty $ι)
+          return some q(Finset.univ_nonempty (α := $ι))
+        | _ => throwError "`s` is not `univ`"
+      catch _ => do
+        let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none
+        pure (some (.fvar fv))
+    match ← core zα pα rhs, so with
+    | .nonnegative pb, _ => do
+      let pα' ← synthInstanceQ q(OrderedAddCommMonoid $α)
+      assertInstancesCommute
+      let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars lhs pb
+      return .nonnegative q(@sum_nonneg $ι $α $pα' $f $s fun i _ ↦ $pr i)
+    | .positive pb, .some (fi : Q(Finset.Nonempty $s)) => do
+      let pα' ← synthInstanceQ q(OrderedCancelAddCommMonoid $α)
+      assertInstancesCommute
+      let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars lhs pb
+      return .positive q(@sum_pos $ι $α $pα' $f $s (fun i _ ↦ $pr i) $fi)
+    | _, _ => pure .none
+  | _ => throwError "not Finset.sum"
+
+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
+
+end Mathlib.Meta.Positivity

Mathlib/Analysis/Analytic/Inverse.lean

@@ -535,8 +535,6 @@ theorem radius_rightInv_pos_of_radius_pos (p : FormalMultilinearSeries 𝕜 E F)
       exact mul_nonneg (add_nonneg (norm_nonneg _) zero_le_one) apos.le
     · intro n one_le_n hn
       have In : 2 ≤ n + 1 := by linarith only [one_le_n]
-      have Snonneg : 0 ≤ S n :=
-        sum_nonneg fun x _ => mul_nonneg (pow_nonneg apos.le _) (norm_nonneg _)
       have rSn : r * S n ≤ 1 / 2 :=
         calc
           r * S n ≤ r * ((I + 1) * a) := by gcongr

Mathlib/Analysis/Calculus/ContDiff/Bounds.lean

@@ -67,8 +67,7 @@ theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_aux {Du Eu
           IH _ (hf.of_le (Nat.cast_le.2 (Nat.le_succ n))) (hg.fderivWithin hs In)
         _ ≤ ‖B‖ * ∑ i : ℕ in Finset.range (n + 1), n.choose i * ‖iteratedFDerivWithin 𝕜 i f s x‖ *
               ‖iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 g s) s x‖ :=
-          (mul_le_mul_of_nonneg_right (B.norm_precompR_le Du)
-            (Finset.sum_nonneg' fun i => by positivity))
+            mul_le_mul_of_nonneg_right (B.norm_precompR_le Du) (by positivity)
         _ = _ := by
           congr 1
           apply Finset.sum_congr rfl fun i hi => ?_
@@ -90,8 +89,7 @@ theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_aux {Du Eu
         _ ≤ ‖B‖ * ∑ i : ℕ in Finset.range (n + 1),
             n.choose i * ‖iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 f s) s x‖ *
               ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖ :=
-          (mul_le_mul_of_nonneg_right (B.norm_precompL_le Du)
-            (Finset.sum_nonneg' fun i => by positivity))
+            mul_le_mul_of_nonneg_right (B.norm_precompL_le Du) (by positivity)
         _ = _ := by
           congr 1
           apply Finset.sum_congr rfl fun i _ => ?_
@@ -222,8 +220,7 @@ theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear (B : E →L
         ‖iteratedFDerivWithin 𝕜 (n - i) gu su xu‖ :=
     Bu.norm_iteratedFDerivWithin_le_of_bilinear_aux hfu hgu hsu hxu
   simp only [Nfu, Ngu, NBu] at this
-  apply this.trans (mul_le_mul_of_nonneg_right Bu_le ?_)
-  exact Finset.sum_nonneg' fun i => by positivity
+  exact this.trans (mul_le_mul_of_nonneg_right Bu_le (by positivity))
 #align continuous_linear_map.norm_iterated_fderiv_within_le_of_bilinear ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear
 
 /-- Bounding the norm of the iterated derivative of `B (f x) (g x)` in terms of the
@@ -249,8 +246,7 @@ theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one
       ∑ i in Finset.range (n + 1), (n.choose i : ℝ) * ‖iteratedFDerivWithin 𝕜 i f s x‖ *
         ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖ := by
   apply (B.norm_iteratedFDerivWithin_le_of_bilinear hf hg hs hx hn).trans
-  apply mul_le_of_le_one_left (Finset.sum_nonneg' fun i => ?_) hB
-  positivity
+  exact mul_le_of_le_one_left (by positivity) hB
 #align continuous_linear_map.norm_iterated_fderiv_within_le_of_bilinear_of_le_one ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one
 
 /-- Bounding the norm of the iterated derivative of `B (f x) (g x)` in terms of the

Mathlib/Computability/AkraBazzi/AkraBazzi.lean

@@ -1162,7 +1162,7 @@
 /-- The main proof of the upper bound part of the Akra-Bazzi theorem. The factor
 `1 - ε n` does not change the asymptotic order, but is needed for the induction step to go
 through. -/
 lemma T_isBigO_smoothingFn_mul_asympBound :
     T =O[atTop] (fun n => (1 - ε n) * asympBound g a b n) := by
   let b' := b (min_bi b) / 2
   have hb_pos : 0 < b' := R.bi_min_div_two_pos
@@ -1243,9 +1243,6 @@
                 * ((1 + (∑ u in range (r i n), g u / u ^ ((p a b) + 1)))))) + g n with i
             · have := R.a_pos i
               positivity
-            · refine add_nonneg zero_le_one <| Finset.sum_nonneg fun j _ => ?_
-              rw [div_nonneg_iff]
-              exact Or.inl ⟨R.g_nonneg j (by positivity), by positivity⟩
             · exact bound1 n hn i
         _ = (∑ i, C * a i * ((b i) ^ (p a b) * n ^ (p a b) * (1 - ε n)
                 * ((1 + ((∑ u in range n, g u / u ^ ((p a b) + 1))
@@ -1292,7 +1289,7 @@
 /-- The main proof of the lower bound part of the Akra-Bazzi theorem. The factor
 `1 + ε n` does not change the asymptotic order, but is needed for the induction step to go
 through. -/
 lemma smoothingFn_mul_asympBound_isBigO_T :
     (fun (n : ℕ) => (1 + ε n) * asympBound g a b n) =O[atTop] T := by
   let b' := b (min_bi b) / 2
   have hb_pos : 0 < b' := R.bi_min_div_two_pos
@@ -1388,10 +1385,10 @@
                   ((1 + (∑ u in range (r i n), g u / u ^ ((p a b) + 1)))))) + g n with i
               · have := R.a_pos i
                 positivity
               · refine add_nonneg zero_le_one <| Finset.sum_nonneg fun j _ => ?_
                 rw [div_nonneg_iff]
                 exact Or.inl ⟨R.g_nonneg j (by positivity), by positivity⟩
               · exact bound2 n hn i
         _ = (∑ i, C * a i * ((b i) ^ (p a b) * n ^ (p a b) * (1 + ε n)
                   * ((1 + ((∑ u in range n, g u / u ^ ((p a b) + 1))
                   - (∑ u in Finset.Ico (r i n) n, g u / u ^ ((p a b) + 1))))))) + g n := by
@@ -1439,7 +1436,7 @@
 /-- The **Akra-Bazzi theorem**: `T ∈ O(n^p (1 + ∑_u^n g(u) / u^{p+1}))` -/
 theorem isBigO_asympBound : T =O[atTop] asympBound g a b := by
   calc T =O[atTop] (fun n => (1 - ε n) * asympBound g a b n) := by
               exact R.T_isBigO_smoothingFn_mul_asympBound
          _ =O[atTop] (fun n => 1 * asympBound g a b n) := by
               refine IsBigO.mul (isBigO_const_of_tendsto (y := 1) ?_ one_ne_zero)
                 (isBigO_refl _ _)
@@ -1458,10 +1455,10 @@
                             show Tendsto ((fun n => 1 + ε n) ∘ (Nat.cast : ℕ → ℝ)) atTop (𝓝 1)
                             exact Tendsto.comp isEquivalent_one_add_smoothingFn_one.tendsto_const
                               tendsto_nat_cast_atTop_atTop
                  _ =O[atTop] T := R.smoothingFn_mul_asympBound_isBigO_T
 
 /-- The **Akra-Bazzi theorem**: `T ∈ Θ(n^p (1 + ∑_u^n g(u) / u^{p+1}))` -/
 theorem isTheta_asympBound : T =Θ[atTop] asympBound g a b :=
   ⟨R.isBigO_asympBound, R.isBigO_symm_asympBound⟩
 
 end AkraBazziRecurrence