Trigger CI for leanprover-community/batteries#1007

Mathlib.lean

@@ -710,6 +710,7 @@ import Mathlib.Algebra.Order.Ring.Unbundled.Rat
 import Mathlib.Algebra.Order.Ring.WithTop
 import Mathlib.Algebra.Order.Star.Basic
 import Mathlib.Algebra.Order.Star.Conjneg
+import Mathlib.Algebra.Order.Star.Prod
 import Mathlib.Algebra.Order.Sub.Basic
 import Mathlib.Algebra.Order.Sub.Defs
 import Mathlib.Algebra.Order.Sub.Prod
@@ -3582,6 +3583,7 @@ import Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
 import Mathlib.NumberTheory.LSeries.HurwitzZetaValues
 import Mathlib.NumberTheory.LSeries.Linearity
 import Mathlib.NumberTheory.LSeries.MellinEqDirichlet
+import Mathlib.NumberTheory.LSeries.Positivity
 import Mathlib.NumberTheory.LSeries.RiemannZeta
 import Mathlib.NumberTheory.LSeries.ZMod
 import Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean

@@ -73,6 +73,18 @@ theorem smul_finprod' {ι : Sort*} [Finite ι] {f : ι → β} (r : α) :
   simp only [finprod_eq_prod_plift_of_mulSupport_subset (s := Finset.univ) (by simp),
     finprod_eq_prod_of_fintype, Finset.smul_prod']
 
+variable {G : Type*} [Group G] [MulDistribMulAction G β]
+
+theorem Finset.smul_prod_perm [Fintype G] (b : β) (g : G) :
+    (g • ∏ h : G, h • b) = ∏ h : G, h • b := by
+  simp only [smul_prod', smul_smul]
+  exact Finset.prod_bijective (g * ·) (Group.mulLeft_bijective g) (by simp) (fun _ _ ↦ rfl)
+
+theorem smul_finprod_perm [Finite G] (b : β) (g : G) :
+    (g • ∏ᶠ h : G, h • b) = ∏ᶠ h : G, h • b := by
+  cases nonempty_fintype G
+  simp only [finprod_eq_prod_of_fintype, Finset.smul_prod_perm]
+
 end
 
 namespace List

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -1401,6 +1401,15 @@ theorem prod_le_iff {H : Subgroup G} {K : Subgroup N} {J : Subgroup (G × N)} :
 theorem prod_eq_bot_iff {H : Subgroup G} {K : Subgroup N} : H.prod K = ⊥ ↔ H = ⊥ ∧ K = ⊥ := by
   simpa only [← Subgroup.toSubmonoid_eq] using Submonoid.prod_eq_bot_iff
 
+@[to_additive closure_prod]
+theorem closure_prod {s : Set G} {t : Set N} (hs : 1 ∈ s) (ht : 1 ∈ t) :
+    closure (s ×ˢ t) = (closure s).prod (closure t) :=
+  le_antisymm
+    (closure_le _ |>.2 <| Set.prod_subset_prod_iff.2 <| .inl ⟨subset_closure, subset_closure⟩)
+    (prod_le_iff.2 ⟨
+      map_le_iff_le_comap.2 <| closure_le _ |>.2 fun _x hx => subset_closure ⟨hx, ht⟩,
+      map_le_iff_le_comap.2 <| closure_le _ |>.2 fun _y hy => subset_closure ⟨hs, hy⟩⟩)
+
 /-- Product of subgroups is isomorphic to their product as groups. -/
 @[to_additive prodEquiv
       "Product of additive subgroups is isomorphic to their product

Mathlib/Algebra/Group/Submonoid/Operations.lean

@@ -715,6 +715,15 @@ theorem prod_le_iff {s : Submonoid M} {t : Submonoid N} {u : Submonoid (M × N)}
       simpa using h2
     simpa using Submonoid.mul_mem _ h1' h2'
 
+@[to_additive closure_prod]
+theorem closure_prod {s : Set M} {t : Set N} (hs : 1 ∈ s) (ht : 1 ∈ t) :
+    closure (s ×ˢ t) = (closure s).prod (closure t) :=
+  le_antisymm
+    (closure_le.2 <| Set.prod_subset_prod_iff.2 <| .inl ⟨subset_closure, subset_closure⟩)
+    (prod_le_iff.2 ⟨
+      map_le_of_le_comap _ <| closure_le.2 fun _x hx => subset_closure ⟨hx, ht⟩,
+      map_le_of_le_comap _ <| closure_le.2 fun _y hy => subset_closure ⟨hs, hy⟩⟩)
+
 end Submonoid
 
 namespace MonoidHom

Mathlib/Algebra/Order/Star/Prod.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2024 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import Mathlib.Algebra.Order.Star.Basic
+import Mathlib.Algebra.Star.Prod
+import Mathlib.Algebra.Ring.Prod
+
+/-!
+# Products of star-ordered rings
+-/
+
+variable {α β : Type*}
+
+open AddSubmonoid in
+instance Prod.instStarOrderedRing
+    [NonUnitalSemiring α] [NonUnitalSemiring β] [PartialOrder α] [PartialOrder β]
+    [StarRing α] [StarRing β] [StarOrderedRing α] [StarOrderedRing β] :
+    StarOrderedRing (α × β) where
+  le_iff := Prod.forall.2 fun xa xy => Prod.forall.2 fun ya yb => by
+    have :
+        closure (Set.range fun s : α × β ↦ star s * s) =
+          (closure <| Set.range fun s : α ↦ star s * s).prod
+          (closure <| Set.range fun s : β ↦ star s * s) := by
+      rw [← closure_prod (Set.mem_range.2 ⟨0, by simp⟩) (Set.mem_range.2 ⟨0, by simp⟩),
+        Set.prod_range_range_eq]
+      simp_rw [Prod.mul_def, Prod.star_def]
+    simp only [mk_le_mk, Prod.exists, mk_add_mk, mk.injEq, StarOrderedRing.le_iff, this,
+      AddSubmonoid.mem_prod, exists_and_exists_comm, and_and_and_comm]

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean

@@ -83,10 +83,7 @@ lemma isClosedEmbedding_cfcₙAux : IsClosedEmbedding (cfcₙAux hp₁ a ha) :=
   refine ((cfcHom_isClosedEmbedding (hp₁.mpr ha)).comp ?_).comp
     ContinuousMapZero.isClosedEmbedding_toContinuousMap
   let e : C(σₙ 𝕜 a, 𝕜) ≃ₜ C(σ 𝕜 (a : A⁺¹), 𝕜) :=
-    { (Homeomorph.compStarAlgEquiv' 𝕜 𝕜 <| .setCongr <|
-        (quasispectrum_eq_spectrum_inr' 𝕜 𝕜 a).symm) with
-      continuous_toFun := ContinuousMap.continuous_comp_left _
-      continuous_invFun := ContinuousMap.continuous_comp_left _ }
+    (Homeomorph.setCongr (quasispectrum_eq_spectrum_inr' 𝕜 𝕜 a)).arrowCongr (.refl _)
   exact e.isClosedEmbedding
 
 @[deprecated (since := "2024-10-20")]

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean

@@ -178,7 +178,7 @@ theorem cfcₙHom_comp [UniqueNonUnitalContinuousFunctionalCalculus R A] (f : C(
   suffices cfcₙHom (cfcₙHom_predicate ha f) = φ from DFunLike.congr_fun this.symm g
   refine cfcₙHom_eq_of_continuous_of_map_id (cfcₙHom_predicate ha f) φ ?_ ?_
   · refine (cfcₙHom_isClosedEmbedding ha).continuous.comp <| continuous_induced_rng.mpr ?_
-    exact f'.toContinuousMap.continuous_comp_left.comp continuous_induced_dom
+    exact f'.toContinuousMap.continuous_precomp.comp continuous_induced_dom
   · simp only [φ, ψ, NonUnitalStarAlgHom.comp_apply, NonUnitalStarAlgHom.coe_mk',
       NonUnitalAlgHom.coe_mk]
     congr

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean

@@ -56,7 +56,7 @@ namespace ContinuousMap
 noncomputable def toNNReal (f : C(X, ℝ)) : C(X, ℝ≥0) := .realToNNReal |>.comp f
 
 @[fun_prop]
-lemma continuous_toNNReal : Continuous (toNNReal (X := X)) := continuous_comp _
+lemma continuous_toNNReal : Continuous (toNNReal (X := X)) := continuous_postcomp _
 
 @[simp]
 lemma toNNReal_apply (f : C(X, ℝ)) (x : X) : f.toNNReal x = (f x).toNNReal := rfl
@@ -187,7 +187,7 @@ instance NNReal.instUniqueContinuousFunctionalCalculus [UniqueContinuousFunction
         Continuous ξ' ∧ ξ' (.restrict s' <| .id ℝ) = ξ (.restrict s <| .id ℝ≥0)) := by
       intro ξ'
       refine ⟨ξ.continuous_realContinuousMapOfNNReal hξ |>.comp <|
-        ContinuousMap.continuous_comp_left _, ?_⟩
+        ContinuousMap.continuous_precomp _, ?_⟩
       exact ξ.realContinuousMapOfNNReal_apply_comp_toReal (.restrict s <| .id ℝ≥0)
     obtain ⟨hφ', hφ_id⟩ := this φ hφ
     obtain ⟨hψ', hψ_id⟩ := this ψ hψ
@@ -249,7 +249,7 @@ lemma toNNReal_apply (f : C(X, ℝ)₀) (x : X) : f.toNNReal x = Real.toNNReal (
 lemma continuous_toNNReal : Continuous (toNNReal (X := X)) := by
   rw [continuous_induced_rng]
   convert_to Continuous (ContinuousMap.toNNReal ∘ ((↑) : C(X, ℝ)₀ → C(X, ℝ))) using 1
-  exact ContinuousMap.continuous_comp _ |>.comp continuous_induced_dom
+  exact ContinuousMap.continuous_postcomp _ |>.comp continuous_induced_dom
 
 lemma toContinuousMapHom_toNNReal (f : C(X, ℝ)₀) :
     (toContinuousMapHom (X := X) (R := ℝ) f).toNNReal =
@@ -401,7 +401,7 @@ instance NNReal.instUniqueNonUnitalContinuousFunctionalCalculus
       intro ξ'
       refine ⟨ξ.continuous_realContinuousMapZeroOfNNReal hξ |>.comp <| ?_, ?_⟩
       · rw [continuous_induced_rng]
-        exact ContinuousMap.continuous_comp_left _ |>.comp continuous_induced_dom
+        exact ContinuousMap.continuous_precomp _ |>.comp continuous_induced_dom
       · exact ξ.realContinuousMapZeroOfNNReal_apply_comp_toReal (.id h0)
     obtain ⟨hφ', hφ_id⟩ := this φ hφ
     obtain ⟨hψ', hψ_id⟩ := this ψ hψ

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean

@@ -271,7 +271,7 @@ theorem cfcHom_comp [UniqueContinuousFunctionalCalculus R A] (f : C(spectrum R a
     (cfcHom ha).comp <| ContinuousMap.compStarAlgHom' R R f'
   suffices cfcHom (cfcHom_predicate ha f) = φ from DFunLike.congr_fun this.symm g
   refine cfcHom_eq_of_continuous_of_map_id (cfcHom_predicate ha f) φ ?_ ?_
-  · exact (cfcHom_isClosedEmbedding ha).continuous.comp f'.continuous_comp_left
+  · exact (cfcHom_isClosedEmbedding ha).continuous.comp f'.continuous_precomp
   · simp only [φ, StarAlgHom.comp_apply, ContinuousMap.compStarAlgHom'_apply]
     congr
     ext x

Mathlib/Analysis/RCLike/Basic.lean

@@ -872,6 +872,20 @@ instance {A : Type*} [NonUnitalRing A] [StarRing A] [PartialOrder A] [StarOrdere
 
 scoped[ComplexOrder] attribute [instance] StarModule.instOrderedSMul
 
+theorem ofReal_mul_pos_iff (x : ℝ) (z : K) :
+    0 < x * z ↔ (x < 0 ∧ z < 0) ∨ (0 < x ∧ 0 < z) := by
+  simp only [pos_iff (K := K), neg_iff (K := K), re_ofReal_mul, im_ofReal_mul]
+  obtain hx | hx | hx := lt_trichotomy x 0
+  · simp only [mul_pos_iff, not_lt_of_gt hx, false_and, hx, true_and, false_or, mul_eq_zero, hx.ne,
+      or_false]
+  · simp only [hx, zero_mul, lt_self_iff_false, false_and, false_or]
+  · simp only [mul_pos_iff, hx, true_and, not_lt_of_gt hx, false_and, or_false, mul_eq_zero,
+      hx.ne', false_or]
+
+theorem ofReal_mul_neg_iff (x : ℝ) (z : K) :
+    x * z < 0 ↔ (x < 0 ∧ 0 < z) ∨ (0 < x ∧ z < 0) := by
+  simpa only [mul_neg, neg_pos, neg_neg_iff_pos] using ofReal_mul_pos_iff x (-z)
+
 end Order
 
 section CleanupLemmas

Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

@@ -997,6 +997,13 @@ lemma abs_cpow_inv_two_im (x : ℂ) : |(x ^ (2⁻¹ : ℂ)).im| = sqrt ((abs x -
     ← Real.sqrt_eq_rpow, _root_.abs_mul, _root_.abs_of_nonneg (sqrt_nonneg _), abs_sin_half,
     ← sqrt_mul (abs.nonneg _), ← mul_div_assoc, mul_sub, mul_one, abs_mul_cos_arg]
 
+open scoped ComplexOrder in
+lemma inv_natCast_cpow_ofReal_pos {n : ℕ} (hn : n ≠ 0) (x : ℝ) :
+    0 < ((n : ℂ) ^ (x : ℂ))⁻¹ := by
+  refine RCLike.inv_pos_of_pos ?_
+  rw [show (n : ℂ) ^ (x : ℂ) = (n : ℝ) ^ (x : ℂ) from rfl, ← ofReal_cpow n.cast_nonneg']
+  positivity
+
 end Complex
 
 section Tactics

Mathlib/Data/Complex/Order.lean

@@ -63,6 +63,12 @@ theorem nonneg_iff {z : ℂ} : 0 ≤ z ↔ 0 ≤ z.re ∧ 0 = z.im :=
 theorem pos_iff {z : ℂ} : 0 < z ↔ 0 < z.re ∧ 0 = z.im :=
   lt_def
 
+theorem nonpos_iff {z : ℂ} : z ≤ 0 ↔ z.re ≤ 0 ∧ z.im = 0 :=
+  le_def
+
+theorem neg_iff {z : ℂ} : z < 0 ↔ z.re < 0 ∧ z.im = 0 :=
+  lt_def
+
 @[simp, norm_cast]
 theorem real_le_real {x y : ℝ} : (x : ℂ) ≤ (y : ℂ) ↔ x ≤ y := by simp [le_def, ofReal]
 

Mathlib/Logic/Basic.lean

@@ -485,6 +485,10 @@ theorem imp_forall_iff {α : Type*} {p : Prop} {q : α → Prop} : (p → ∀ x,
 theorem exists_swap {p : α → β → Prop} : (∃ x y, p x y) ↔ ∃ y x, p x y :=
   ⟨fun ⟨x, y, h⟩ ↦ ⟨y, x, h⟩, fun ⟨y, x, h⟩ ↦ ⟨x, y, h⟩⟩
 
+theorem exists_and_exists_comm {P : α → Prop} {Q : β → Prop} :
+    (∃ a, P a) ∧ (∃ b, Q b) ↔ ∃ a b, P a ∧ Q b :=
+  ⟨fun ⟨⟨a, ha⟩, ⟨b, hb⟩⟩ ↦ ⟨a, b, ⟨ha, hb⟩⟩, fun ⟨a, b, ⟨ha, hb⟩⟩ ↦ ⟨⟨a, ha⟩, ⟨b, hb⟩⟩⟩
+
 export Classical (not_forall)
 
 theorem not_forall_not : (¬∀ x, ¬p x) ↔ ∃ x, p x := Decidable.not_forall_not

Mathlib/NumberTheory/LSeries/Basic.lean

@@ -111,6 +111,20 @@ lemma norm_term_le_of_re_le_re (f : ℕ → ℂ) {s s' : ℂ} (h : s.re ≤ s'.r
   next => rfl
   next hn => gcongr; exact Nat.one_le_cast.mpr <| Nat.one_le_iff_ne_zero.mpr hn
 
+section positivity
+
+open scoped ComplexOrder
+
+lemma term_nonneg {a : ℕ → ℂ} {n : ℕ} (h : 0 ≤ a n) (x : ℝ) : 0 ≤ term a x n := by
+  rw [term_def]
+  split_ifs with hn
+  exacts [le_rfl, mul_nonneg h (inv_natCast_cpow_ofReal_pos hn x).le]
+
+lemma term_pos {a : ℕ → ℂ} {n : ℕ} (hn : n ≠ 0) (h : 0 < a n) (x : ℝ) : 0 < term a x n := by
+  simpa only [term_of_ne_zero hn] using mul_pos h <| inv_natCast_cpow_ofReal_pos hn x
+
+end positivity
+
 end LSeries
 
 /-!

Mathlib/NumberTheory/LSeries/Positivity.lean

@@ -0,0 +1,109 @@
+/-
+Copyright (c) 2024 Michael Stoll. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Birkbeck, David Loeffler, Michael Stoll
+-/
+import Mathlib.Analysis.Complex.TaylorSeries
+import Mathlib.Analysis.Complex.Positivity
+import Mathlib.NumberTheory.ArithmeticFunction
+import Mathlib.NumberTheory.LSeries.Deriv
+
+/-!
+# Positivity of values of L-series
+
+The main results of this file are as follows.
+
+* If `a : ℕ → ℂ` takes nonnegative real values and `a 1 > 0`, then `L a x > 0`
+  when `x : ℝ` is in the open half-plane of absolute convergence; see
+  `LSeries.positive` and `ArithmeticFunction.LSeries_positive`.
+
+* If in addition the L_series of `a` agrees on some open right half-plane where it
+  converges with an entire function `f`, then `f` is positive on the real axis;
+  see `LSeries.positive_of_eq_differentiable` and
+  `ArithmeticFunction.LSeries_positive_of_eq_differentiable`.
+-/
+
+open scoped ComplexOrder
+
+open Complex
+
+namespace LSeries
+
+/-- If all values of a `ℂ`-valued arithmetic function are nonnegative reals and `x` is a
+real number in the domain of absolute convergence, then the `n`th iterated derivative
+of the associated L-series is nonnegative real when `n` is even and nonpositive real
+when `n` is odd. -/
+lemma iteratedDeriv_alternating {a : ℕ → ℂ} (hn : 0 ≤ a) {x : ℝ}
+    (h : LSeries.abscissaOfAbsConv a < x) (n : ℕ) :
+    0 ≤ (-1) ^ n * iteratedDeriv n (LSeries a) x := by
+  rw [LSeries_iteratedDeriv _ h, LSeries, ← mul_assoc, ← pow_add, Even.neg_one_pow ⟨n, rfl⟩,
+    one_mul]
+  refine tsum_nonneg fun k ↦ ?_
+  rw [LSeries.term_def]
+  split
+  · exact le_rfl
+  · refine mul_nonneg ?_ <| (inv_natCast_cpow_ofReal_pos (by assumption) x).le
+    induction n with
+    | zero => simpa only [Function.iterate_zero, id_eq] using hn k
+    | succ n IH =>
+        rw [Function.iterate_succ_apply']
+        refine mul_nonneg ?_ IH
+        simp only [← natCast_log, zero_le_real, Real.log_natCast_nonneg]
+
+/-- If all values of `a : ℕ → ℂ` are nonnegative reals and `a 1` is positive,
+then `L a x` is positive real for all real `x` larger than `abscissaOfAbsConv a`. -/
+lemma positive {a : ℕ → ℂ} (ha₀ : 0 ≤ a) (ha₁ : 0 < a 1) {x : ℝ} (hx : abscissaOfAbsConv a < x) :
+    0 < LSeries a x := by
+  rw [LSeries]
+  refine tsum_pos ?_ (fun n ↦ term_nonneg (ha₀ n) x) 1 <| term_pos one_ne_zero ha₁ x
+  exact LSeriesSummable_of_abscissaOfAbsConv_lt_re <| by simpa only [ofReal_re] using hx
+
+/-- If all values of `a : ℕ → ℂ` are nonnegative reals and `a 1`
+is positive, and the L-series of `a` agrees with an entire function `f` on some open
+right half-plane where it converges, then `f` is real and positive on `ℝ`. -/
+lemma positive_of_differentiable_of_eqOn {a : ℕ → ℂ} (ha₀ : 0 ≤ a) (ha₁ : 0 < a 1) {f : ℂ → ℂ}
+    (hf : Differentiable ℂ f) {x : ℝ} (hx : abscissaOfAbsConv a ≤ x)
+    (hf' : {s | x < s.re}.EqOn f (LSeries a)) (y : ℝ) :
+    0 < f y := by
+  have hxy : x < max x y + 1 := (le_max_left x y).trans_lt (lt_add_one _)
+  have hxy' : abscissaOfAbsConv a < max x y + 1 := hx.trans_lt <| mod_cast hxy
+  have hys : (max x y + 1 : ℂ) ∈ {s | x < s.re} := by
+    simp only [Set.mem_setOf_eq, add_re, ofReal_re, one_re, hxy]
+  have hfx : 0 < f (max x y + 1) := by
+    simpa only [hf' hys, ofReal_add, ofReal_one] using positive ha₀ ha₁ hxy'
+  refine (hfx.trans_le <| hf.apply_le_of_iteratedDeriv_alternating (fun n _ ↦ ?_) ?_)
+  · have hs : IsOpen {s : ℂ | x < s.re} := continuous_re.isOpen_preimage _ isOpen_Ioi
+    simpa only [hf'.iteratedDeriv_of_isOpen hs n hys, ofReal_add, ofReal_one] using
+      iteratedDeriv_alternating ha₀ hxy' n
+  · exact_mod_cast (le_max_right x y).trans (lt_add_one _).le
+
+end LSeries
+
+namespace ArithmeticFunction
+
+/-- If all values of a `ℂ`-valued arithmetic function are nonnegative reals and `x` is a
+real number in the domain of absolute convergence, then the `n`th iterated derivative
+of the associated L-series is nonnegative real when `n` is even and nonpositive real
+when `n` is odd. -/
+lemma iteratedDeriv_LSeries_alternating (a : ArithmeticFunction ℂ) (hn : ∀ n, 0 ≤ a n) {x : ℝ}
+    (h : LSeries.abscissaOfAbsConv a < x) (n : ℕ) :
+    0 ≤ (-1) ^ n * iteratedDeriv n (LSeries (a ·)) x :=
+  LSeries.iteratedDeriv_alternating hn h n
+
+/-- If all values of a `ℂ`-valued arithmetic function `a` are nonnegative reals and `a 1` is
+positive, then `L a x` is positive real for all real `x` larger than `abscissaOfAbsConv a`. -/
+lemma LSeries_positive {a : ℕ → ℂ} (ha₀ : 0 ≤ a) (ha₁ : 0 < a 1) {x : ℝ}
+    (hx : LSeries.abscissaOfAbsConv a < x) :
+    0 < LSeries a x :=
+  LSeries.positive ha₀ ha₁ hx
+
+/-- If all values of a `ℂ`-valued arithmetic function `a` are nonnegative reals and `a 1`
+is positive, and the L-series of `a` agrees with an entire function `f` on some open
+right half-plane where it converges, then `f` is real and positive on `ℝ`. -/
+lemma LSeries_positive_of_differentiable_of_eqOn {a : ArithmeticFunction ℂ} (ha₀ : 0 ≤ (a ·))
+    (ha₁ : 0 < a 1) {f : ℂ → ℂ} (hf : Differentiable ℂ f) {x : ℝ}
+    (hx : LSeries.abscissaOfAbsConv a ≤ x) (hf' : {s | x < s.re}.EqOn f (LSeries a)) (y : ℝ) :
+    0 < f y :=
+  LSeries.positive_of_differentiable_of_eqOn ha₀ ha₁ hf hx hf' y
+
+end ArithmeticFunction

Mathlib/NumberTheory/LSeries/RiemannZeta.lean

@@ -202,6 +202,25 @@ theorem zeta_nat_eq_tsum_of_gt_one {k : ℕ} (hk : 1 < k) :
 lemma riemannZeta_residue_one : Tendsto (fun s ↦ (s - 1) * riemannZeta s) (𝓝[≠] 1) (𝓝 1) := by
   exact hurwitzZetaEven_residue_one 0
 
+/-- The residue of `ζ(s)` at `s = 1` is equal to 1, expressed using `tsum`. -/
+theorem tendsto_sub_mul_tsum_nat_cpow :
+    Tendsto (fun s : ℂ ↦ (s - 1) * ∑' (n : ℕ), 1 / (n : ℂ) ^ s) (𝓝[{s | 1 < re s}] 1) (𝓝 1) := by
+  refine (tendsto_nhdsWithin_mono_left ?_ riemannZeta_residue_one).congr' ?_
+  · simp only [subset_compl_singleton_iff, mem_setOf_eq, one_re, not_lt, le_refl]
+  · filter_upwards [eventually_mem_nhdsWithin] with s hs using
+      congr_arg _ <| zeta_eq_tsum_one_div_nat_cpow hs
+
+/-- The residue of `ζ(s)` at `s = 1` is equal to 1 expressed using `tsum` and for a
+real variable. -/
+theorem tendsto_sub_mul_tsum_nat_rpow :
+    Tendsto (fun s : ℝ ↦ (s - 1) * ∑' (n : ℕ), 1 / (n : ℝ) ^ s) (𝓝[>] 1) (𝓝 1) := by
+  rw [← tendsto_ofReal_iff, ofReal_one]
+  have : Tendsto (fun s : ℝ ↦ (s : ℂ)) (𝓝[>] 1) (𝓝[{s | 1 < re s}] 1) :=
+    continuous_ofReal.continuousWithinAt.tendsto_nhdsWithin (fun _ _ ↦ by aesop)
+  apply (tendsto_sub_mul_tsum_nat_cpow.comp this).congr fun s ↦ ?_
+  simp only [one_div, Function.comp_apply, ofReal_mul, ofReal_sub, ofReal_one, ofReal_tsum,
+    ofReal_inv, ofReal_cpow (Nat.cast_nonneg _), ofReal_natCast]
+
 /- naming scheme was changed from `riemannCompletedZeta` to `completedRiemannZeta`; add
 aliases for the old names -/
 section aliases