refactor(NumberTheory/LSeries): move evaluation argument s to last in LSeries_congr (#29060)

Align with Mathlib convention of having evaluation variables last, improving readability, partial application, and consistency with derivative/continuity lemmas. Previously, `s` was first, which was slightly off-pattern and less ergonomic in pipelines.

Co-authored-by: Roman Kvasnytskyi <rkvasnytskyi@playtika.com>

Author: Periecle

Mathlib/NumberTheory/LSeries/Basic.lean

@@ -160,8 +160,8 @@ noncomputable
 def LSeries (f : ℕ → ℂ) (s : ℂ) : ℂ :=
   ∑' n, term f s n
 
--- TODO: change argument order in `LSeries_congr` to have `s` last.
-lemma LSeries_congr {f g : ℕ → ℂ} (s : ℂ) (h : ∀ {n}, n ≠ 0 → f n = g n) :
+/-- Congruence for `LSeries` with the evaluation variable `s`. -/
+lemma LSeries_congr {f g : ℕ → ℂ} (h : ∀ {n}, n ≠ 0 → f n = g n) (s : ℂ) :
     LSeries f s = LSeries g s :=
   tsum_congr <| term_congr h s
 
@@ -226,7 +226,7 @@ lemma LSeriesHasSum_iff {f : ℕ → ℂ} {s a : ℂ} :
 
 lemma LSeriesHasSum_congr {f g : ℕ → ℂ} (s a : ℂ) (h : ∀ {n}, n ≠ 0 → f n = g n) :
     LSeriesHasSum f s a ↔ LSeriesHasSum g s a := by
-  simp [LSeriesHasSum_iff, LSeriesSummable_congr s h, LSeries_congr s h]
+  simp [LSeriesHasSum_iff, LSeriesSummable_congr s h, LSeries_congr h s]
 
 lemma LSeriesSummable.of_re_le_re {f : ℕ → ℂ} {s s' : ℂ} (h : s.re ≤ s'.re)
     (hf : LSeriesSummable f s) : LSeriesSummable f s' := by

Mathlib/NumberTheory/LSeries/Dirichlet.lean

@@ -250,7 +250,7 @@ namespace ArithmeticFunction
 to the constant sequence `1`. -/
 lemma LSeries_zeta_eq : L ↗ζ = L 1 := by
   ext s
-  exact (LSeries_congr s const_one_eq_zeta).symm
+  exact (LSeries_congr const_one_eq_zeta s).symm
 
 /-- The `LSeries` associated to the arithmetic function `ζ` converges at `s` if and only if
 `re s > 1`. -/
@@ -376,7 +376,7 @@ lemma LSeries_twist_vonMangoldt_eq {N : ℕ} (χ : DirichletCharacter ℂ N) {s
   have hΛ : LSeriesSummable (↗χ * ↗Λ) s := LSeriesSummable_twist_vonMangoldt χ hs
   rw [eq_div_iff <| LSeries_ne_zero_of_one_lt_re χ hs, ← LSeries_convolution' hΛ hχ,
     convolution_twist_vonMangoldt, LSeries_deriv hs', neg_neg]
-  exact LSeries_congr s fun _ ↦ by simp [mul_comm, logMul]
+  exact LSeries_congr (fun _ ↦ by simp [mul_comm, logMul]) s
 
 end DirichletCharacter
 
@@ -386,7 +386,7 @@ open DirichletCharacter in
 /-- The L-series of the von Mangoldt function `Λ` equals the negative logarithmic derivative
 of the L-series of the constant sequence `1` on its domain of convergence `re s > 1`. -/
 lemma LSeries_vonMangoldt_eq {s : ℂ} (hs : 1 < s.re) : L ↗Λ s = - deriv (L 1) s / L 1 s := by
-  refine (LSeries_congr s fun {n} _ ↦ ?_).trans <|
+  refine (LSeries_congr (fun {n} _ ↦ ?_) s).trans <|
     LSeries_modOne_eq ▸ LSeries_twist_vonMangoldt_eq χ₁ hs
   simp [Subsingleton.eq_one (n : ZMod 1)]
 

Mathlib/NumberTheory/LSeries/Injectivity.lean

@@ -124,7 +124,7 @@ lemma LSeries.tendsto_atTop {f : ℕ → ℂ} (ha : abscissaOfAbsConv f < ⊤) :
   have hF₀ : F 0 = 0 := rfl
   have hF {n : ℕ} (hn : n ≠ 0) : F n = f n := if_neg hn
   have ha' : abscissaOfAbsConv F < ⊤ := (abscissaOfAbsConv_congr hF).symm ▸ ha
-  simp_rw [← LSeries_congr _ hF]
+  simp_rw [← LSeries_congr hF]
   convert LSeries.tendsto_cpow_mul_atTop (n := 0) (fun _ hm ↦ Nat.le_zero.mp hm ▸ hF₀) ha' using 1
   simp
 
@@ -149,7 +149,7 @@ lemma LSeries_eventually_eq_zero_iff' {f : ℕ → ℂ} :
       have hF {n : ℕ} (hn : n ≠ 0) : F n = f n := if_neg hn
       suffices ∀ n, F n = 0 from fun n hn ↦ (hF hn).symm.trans (this n)
       have ha : ¬ abscissaOfAbsConv F = ⊤ := abscissaOfAbsConv_congr hF ▸ h
-      have h' (x : ℝ) : LSeries F x = LSeries f x := LSeries_congr x hF
+      have h' (x : ℝ) : LSeries F x = LSeries f x := LSeries_congr hF x
       have H' (n : ℕ) : (fun x : ℝ ↦ n ^ (x : ℂ) * LSeries F x) =ᶠ[atTop] fun _ ↦ 0 := by
         simp only [h']
         rw [eventuallyEq_iff_exists_mem] at H ⊢
@@ -167,7 +167,7 @@ lemma LSeries_eventually_eq_zero_iff' {f : ℕ → ℂ} :
       | succ n =>
           simpa using LSeries.tendsto_cpow_mul_atTop (fun m hm ↦ ih m <| lt_succ_of_le hm) <|
             Ne.lt_top ha
-    · simp [LSeries_congr x fun {n} ↦ H n, show (fun _ : ℕ ↦ (0 : ℂ)) = 0 from rfl]
+    · simp [LSeries_congr (fun {n} ↦ H n) x, show (fun _ : ℕ ↦ (0 : ℂ)) = 0 from rfl]
 
 open Nat in
 /-- Assuming `f 0 = 0`, the `LSeries` of `f` is zero if and only if either `f = 0` or the
@@ -228,7 +228,7 @@ if `f n = g n` whenever `n ≠ 0`. -/
 lemma LSeries_eq_iff_of_abscissaOfAbsConv_lt_top {f g : ℕ → ℂ} (hf : abscissaOfAbsConv f < ⊤)
     (hg : abscissaOfAbsConv g < ⊤) :
     LSeries f = LSeries g ↔ ∀ n ≠ 0, f n = g n := by
-  refine ⟨fun H n hn ↦ ?_, fun H ↦ funext (LSeries_congr · fun {n} ↦ H n)⟩
+  refine ⟨fun H n hn ↦ ?_, fun H ↦ funext (LSeries_congr fun {n} ↦ H n)⟩
   refine eq_of_LSeries_eventually_eq hf hg ?_ hn
   exact Filter.Eventually.of_forall fun x ↦ congr_fun H x
 

Mathlib/NumberTheory/LSeries/Nonvanishing.lean

@@ -150,7 +150,7 @@ private lemma F_eq_LSeries (B : BadChar N) {s : ℂ} (hs : 1 < s.re) :
     simp only [ne_eq, hs', not_false_eq_true, Function.update_of_ne, B.χ.LFunction_eq_LSeries hs]
     congr 1
     · simp_rw [← LSeries_zeta_eq_riemannZeta hs, ← natCoe_apply]
-    · exact LSeries_congr s B.χ.apply_eq_toArithmeticFunction_apply
+    · exact LSeries_congr B.χ.apply_eq_toArithmeticFunction_apply s
   -- summability side goals from `LSeries_convolution'`
   · exact LSeriesSummable_zeta_iff.mpr hs
   · exact (LSeriesSummable_congr _ fun h ↦ (B.χ.apply_eq_toArithmeticFunction_apply h).symm).mpr <|

Mathlib/NumberTheory/LSeries/PrimesInAP.lean

@@ -287,7 +287,7 @@ lemma LSeries_residueClass_eq (ha : IsUnit a) {s : ℂ} (hs : 1 < s.re) :
   rw [eq_inv_mul_iff_mul_eq₀ <| mod_cast (Nat.totient_pos.mpr q.pos_of_neZero).ne']
   simp_rw [← LSeries_smul,
     ← LSeries_sum <| fun χ _ ↦ (LSeriesSummable_twist_vonMangoldt χ hs).smul _]
-  refine LSeries_congr s fun {n} _ ↦ ?_
+  refine LSeries_congr (fun {n} _ ↦ ?_) s
   simp only [Pi.smul_apply, residueClass_apply ha, smul_eq_mul, ← mul_assoc,
     mul_inv_cancel_of_invertible, one_mul, Finset.sum_apply, Pi.mul_apply]
 

Mathlib/NumberTheory/LSeries/SumCoeff.lean

@@ -137,7 +137,7 @@ theorem LSeries_eq_mul_integral (f : ℕ → ℂ) {r : ℝ} (hr : 0 ≤ r) {s :
     (by filter_upwards [eventually_ne_atTop 0] with n h using if_neg h)] at hS
   have (n : _) : ∑ k ∈ Icc 1 n, (if k = 0 then 0 else f k) = ∑ k ∈ Icc 1 n, f k :=
     Finset.sum_congr rfl fun k hk ↦ by rw [if_neg (zero_lt_one.trans_le (mem_Icc.mp hk).1).ne']
-  rw [← LSeries_congr _ (fun _ ↦ if_neg _), LSeries_eq_mul_integral_aux (if_pos rfl) hr hs hS] <;>
+  rw [← LSeries_congr fun _ ↦ if_neg _, LSeries_eq_mul_integral_aux (if_pos rfl) hr hs hS] <;>
   simp_all
 
 /-- A version of `LSeries_eq_mul_integral` where we use the stronger condition that the partial sums