chore: uniformize theorem naming (#32726)

Following a suggestion made by @j-loreaux in the review of an earlier PR, rename several of the theorems introduced lately in `Mathlib/Analysis/Complex/ValueDistribution/*`.

Author: kebekus

Mathlib/Analysis/Complex/ValueDistribution/CharacteristicFunction.lean

@@ -74,49 +74,59 @@ lemma characteristic_sub_characteristic_eq_proximity_sub_proximity (h : Meromorp
 For `1 ≤ r`, the characteristic function for the zeros of `f * g` is less than or equal to the sum
 of the characteristic functions for the zeros of `f` and `g`, respectively.
 -/
-theorem characteristic_zero_mul_le {f₁ f₂ : ℂ → ℂ} {r : ℝ} (hr : 1 ≤ r)
+theorem characteristic_mul_zero_le {f₁ f₂ : ℂ → ℂ} {r : ℝ} (hr : 1 ≤ r)
     (h₁f₁ : MeromorphicOn f₁ Set.univ) (h₂f₁ : ∀ z, meromorphicOrderAt f₁ z ≠ ⊤)
     (h₁f₂ : MeromorphicOn f₂ Set.univ) (h₂f₂ : ∀ z, meromorphicOrderAt f₂ z ≠ ⊤) :
     characteristic (f₁ * f₂) 0 r ≤ (characteristic f₁ 0 + characteristic f₂ 0) r := by
   simp only [characteristic, Pi.add_apply]
   rw [add_add_add_comm]
-  apply add_le_add (proximity_zero_mul_le h₁f₁ h₁f₂ r)
-    (logCounting_zero_mul_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂)
+  apply add_le_add (proximity_mul_zero_le h₁f₁ h₁f₂ r)
+    (logCounting_mul_zero_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂)
+
+@[deprecated (since := "2025-12-11")] alias characteristic_zero_mul_le := characteristic_mul_zero_le
 
 /--
 Asymptotically, the characteristic function for the zeros of `f * g` is less than or equal to the
 sum of the characteristic functions for the zeros of `f` and `g`, respectively.
 -/
-theorem characteristic_zero_mul_eventually_le {f₁ f₂ : ℂ → ℂ}
+theorem characteristic_mul_zero_eventuallyLE {f₁ f₂ : ℂ → ℂ}
     (h₁f₁ : MeromorphicOn f₁ Set.univ) (h₂f₁ : ∀ z, meromorphicOrderAt f₁ z ≠ ⊤)
     (h₁f₂ : MeromorphicOn f₂ Set.univ) (h₂f₂ : ∀ z, meromorphicOrderAt f₂ z ≠ ⊤) :
     characteristic (f₁ * f₂) 0 ≤ᶠ[Filter.atTop] characteristic f₁ 0 + characteristic f₂ 0 := by
   filter_upwards [Filter.eventually_ge_atTop 1]
-  exact fun _ hr ↦ characteristic_zero_mul_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂
+  exact fun _ hr ↦ characteristic_mul_zero_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂
+
+@[deprecated (since := "2025-12-11")]
+alias characteristic_zero_mul_eventually_le := characteristic_mul_zero_eventuallyLE
 
 /--
 For `1 ≤ r`, the characteristic function for the poles of `f * g` is less than or equal to the sum
 of the characteristic functions for the poles of `f` and `g`, respectively.
 -/
-theorem characteristic_top_mul_le {f₁ f₂ : ℂ → ℂ} {r : ℝ} (hr : 1 ≤ r)
+theorem characteristic_mul_top_le {f₁ f₂ : ℂ → ℂ} {r : ℝ} (hr : 1 ≤ r)
     (h₁f₁ : MeromorphicOn f₁ Set.univ) (h₂f₁ : ∀ z, meromorphicOrderAt f₁ z ≠ ⊤)
     (h₁f₂ : MeromorphicOn f₂ Set.univ) (h₂f₂ : ∀ z, meromorphicOrderAt f₂ z ≠ ⊤) :
     characteristic (f₁ * f₂) ⊤ r ≤ (characteristic f₁ ⊤ + characteristic f₂ ⊤) r := by
   simp only [characteristic, Pi.add_apply]
   rw [add_add_add_comm]
-  apply add_le_add (proximity_top_mul_le h₁f₁ h₁f₂ r)
-    (logCounting_top_mul_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂)
+  apply add_le_add (proximity_mul_top_le h₁f₁ h₁f₂ r)
+    (logCounting_mul_top_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂)
+
+@[deprecated (since := "2025-12-11")] alias characteristic_top_mul_le := characteristic_mul_top_le
 
 /--
 Asymptotically, the characteristic function for the poles of `f * g` is less than or equal to the
 sum of the characteristic functions for the poles of `f` and `g`, respectively.
 -/
-theorem characteristic_top_mul_eventually_le {f₁ f₂ : ℂ → ℂ}
+theorem characteristic_mul_top_eventuallyLE {f₁ f₂ : ℂ → ℂ}
     (h₁f₁ : MeromorphicOn f₁ Set.univ) (h₂f₁ : ∀ z, meromorphicOrderAt f₁ z ≠ ⊤)
     (h₁f₂ : MeromorphicOn f₂ Set.univ) (h₂f₂ : ∀ z, meromorphicOrderAt f₂ z ≠ ⊤) :
     characteristic (f₁ * f₂) ⊤ ≤ᶠ[Filter.atTop] characteristic f₁ ⊤ + characteristic f₂ ⊤ := by
   filter_upwards [Filter.eventually_ge_atTop 1]
-  exact fun _ hr ↦ characteristic_top_mul_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂
+  exact fun _ hr ↦ characteristic_mul_top_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂
+
+@[deprecated (since := "2025-12-11")]
+alias characteristic_top_mul_eventually_le := characteristic_mul_top_eventuallyLE
 
 /--
 For natural numbers `n`, the characteristic function for the zeros of `f ^ n` equals `n` times the

Mathlib/Analysis/Complex/ValueDistribution/CountingFunction.lean

@@ -149,12 +149,14 @@ theorem logCounting_le {E : Type*} [NormedAddCommGroup E] [ProperSpace E]
 /--
 The logarithmic counting function respects the `≤` relation asymptotically.
 -/
-theorem logCounting_eventually_le {E : Type*} [NormedAddCommGroup E] [ProperSpace E]
+theorem logCounting_eventuallyLE {E : Type*} [NormedAddCommGroup E] [ProperSpace E]
     {f₁ f₂ : locallyFinsuppWithin (univ : Set E) ℤ} (h : f₁ ≤ f₂) :
     logCounting f₁ ≤ᶠ[Filter.atTop] logCounting f₂ := by
   filter_upwards [Filter.eventually_ge_atTop 1]
   exact fun _ hr ↦ logCounting_le h hr
 
+@[deprecated (since := "2025-12-11")] alias logCounting_eventually_le := logCounting_eventuallyLE
+
 end Function.locallyFinsuppWithin
 
 /-!
@@ -354,7 +356,7 @@ Then,
 
 But `log r` is negative for small `r`.
 -/
-theorem logCounting_zero_mul_le {f₁ f₂ : 𝕜 → 𝕜} {r : ℝ} (hr : 1 ≤ r)
+theorem logCounting_mul_zero_le {f₁ f₂ : 𝕜 → 𝕜} {r : ℝ} (hr : 1 ≤ r)
     (h₁f₁ : MeromorphicOn f₁ Set.univ) (h₂f₁ : ∀ z, meromorphicOrderAt f₁ z ≠ ⊤)
     (h₁f₂ : MeromorphicOn f₂ Set.univ) (h₂f₂ : ∀ z, meromorphicOrderAt f₂ z ≠ ⊤) :
     logCounting (f₁ * f₂) 0 r ≤ (logCounting f₁ 0 + logCounting f₂ 0) r := by
@@ -364,22 +366,27 @@ theorem logCounting_zero_mul_le {f₁ f₂ : 𝕜 → 𝕜} {r : ℝ} (hr : 1 
   apply Function.locallyFinsuppWithin.logCounting_le _ hr
   apply Function.locallyFinsuppWithin.posPart_add
 
+@[deprecated (since := "2025-12-11")] alias logCounting_zero_mul_le := logCounting_mul_zero_le
+
 /--
 Asymptotically, the logarithmic counting function for the zeros of `f * g` is less than or equal to
 the sum of the logarithmic counting functions for the zeros of `f` and `g`, respectively.
 -/
-theorem logCounting_zero_mul_eventually_le {f₁ f₂ : 𝕜 → 𝕜}
+theorem logCounting_mul_zero_eventuallyLE {f₁ f₂ : 𝕜 → 𝕜}
     (h₁f₁ : MeromorphicOn f₁ Set.univ) (h₂f₁ : ∀ z, meromorphicOrderAt f₁ z ≠ ⊤)
     (h₁f₂ : MeromorphicOn f₂ Set.univ) (h₂f₂ : ∀ z, meromorphicOrderAt f₂ z ≠ ⊤) :
     logCounting (f₁ * f₂) 0 ≤ᶠ[Filter.atTop] logCounting f₁ 0 + logCounting f₂ 0 := by
   filter_upwards [Filter.eventually_ge_atTop 1]
-  exact fun _ hr ↦ logCounting_zero_mul_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂
+  exact fun _ hr ↦ logCounting_mul_zero_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂
+
+@[deprecated (since := "2025-12-11")]
+alias logCounting_zero_mul_eventually_le := logCounting_mul_zero_eventuallyLE
 
 /--
 For `1 ≤ r`, the logarithmic counting function for the poles of `f * g` is less than or equal to the
 sum of the logarithmic counting functions for the poles of `f` and `g`, respectively.
 -/
-theorem logCounting_top_mul_le {f₁ f₂ : 𝕜 → 𝕜} {r : ℝ} (hr : 1 ≤ r)
+theorem logCounting_mul_top_le {f₁ f₂ : 𝕜 → 𝕜} {r : ℝ} (hr : 1 ≤ r)
     (h₁f₁ : MeromorphicOn f₁ Set.univ) (h₂f₁ : ∀ z, meromorphicOrderAt f₁ z ≠ ⊤)
     (h₁f₂ : MeromorphicOn f₂ Set.univ) (h₂f₂ : ∀ z, meromorphicOrderAt f₂ z ≠ ⊤) :
     logCounting (f₁ * f₂) ⊤ r ≤ (logCounting f₁ ⊤ + logCounting f₂ ⊤) r := by
@@ -389,16 +396,21 @@ theorem logCounting_top_mul_le {f₁ f₂ : 𝕜 → 𝕜} {r : ℝ} (hr : 1 ≤
   apply Function.locallyFinsuppWithin.logCounting_le _ hr
   apply Function.locallyFinsuppWithin.negPart_add
 
+@[deprecated (since := "2025-12-11")] alias logCounting_top_mul_le := logCounting_mul_top_le
+
 /--
 Asymptotically, the logarithmic counting function for the zeros of `f * g` is less than or equal to
 the sum of the logarithmic counting functions for the zeros of `f` and `g`, respectively.
 -/
-theorem logCounting_top_mul_eventually_le {f₁ f₂ : 𝕜 → 𝕜}
+theorem logCounting_mul_top_eventuallyLE {f₁ f₂ : 𝕜 → 𝕜}
     (h₁f₁ : MeromorphicOn f₁ Set.univ) (h₂f₁ : ∀ z, meromorphicOrderAt f₁ z ≠ ⊤)
     (h₁f₂ : MeromorphicOn f₂ Set.univ) (h₂f₂ : ∀ z, meromorphicOrderAt f₂ z ≠ ⊤) :
     logCounting (f₁ * f₂) ⊤ ≤ᶠ[Filter.atTop] logCounting f₁ ⊤ + logCounting f₂ ⊤ := by
   filter_upwards [Filter.eventually_ge_atTop 1]
-  exact fun _ hr ↦ logCounting_top_mul_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂
+  exact fun _ hr ↦ logCounting_mul_top_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂
+
+@[deprecated (since := "2025-12-11")]
+alias logCounting_top_mul_eventually_le := logCounting_mul_top_eventuallyLE
 
 /--
 For natural numbers `n`, the logarithmic counting function for the zeros of `f ^ n` equals `n`

Mathlib/Analysis/Complex/ValueDistribution/ProximityFunction.lean

@@ -157,7 +157,7 @@ theorem proximity_add_top_le [NormedSpace ℂ E] {f₁ f₂ : ℂ → E} (h₁f
 The proximity function `f * g` at `⊤` is less than or equal to the sum of the proximity functions of
 `f` and `g`, respectively.
 -/
-theorem proximity_top_mul_le {f₁ f₂ : ℂ → ℂ} (h₁f₁ : MeromorphicOn f₁ Set.univ)
+theorem proximity_mul_top_le {f₁ f₂ : ℂ → ℂ} (h₁f₁ : MeromorphicOn f₁ Set.univ)
     (h₁f₂ : MeromorphicOn f₂ Set.univ) :
     proximity (f₁ * f₂) ⊤ ≤ (proximity f₁ ⊤) + (proximity f₂ ⊤) := by
   calc proximity (f₁ * f₂) ⊤
@@ -179,20 +179,24 @@ theorem proximity_top_mul_le {f₁ f₂ : ℂ → ℂ} (h₁f₁ : MeromorphicOn
       · exact circleIntegrable_posLog_norm_meromorphicOn (fun x a ↦ h₁f₂ x trivial)
     _ = (proximity f₁ ⊤) + (proximity f₂ ⊤) := rfl
 
+@[deprecated (since := "2025-12-11")] alias proximity_top_mul_le := proximity_mul_top_le
+
 /--
 The proximity function `f * g` at `0` is less than or equal to the sum of the proximity functions of
 `f` and `g`, respectively.
 -/
-theorem proximity_zero_mul_le {f₁ f₂ : ℂ → ℂ} (h₁f₁ : MeromorphicOn f₁ Set.univ)
+theorem proximity_mul_zero_le {f₁ f₂ : ℂ → ℂ} (h₁f₁ : MeromorphicOn f₁ Set.univ)
     (h₁f₂ : MeromorphicOn f₂ Set.univ) :
     proximity (f₁ * f₂) 0 ≤ (proximity f₁ 0) + (proximity f₂ 0) := by
   calc proximity (f₁ * f₂) 0
     _ ≤ (proximity f₁⁻¹ ⊤) + (proximity f₂⁻¹ ⊤) := by
       rw [← proximity_inv, mul_inv]
-      apply proximity_top_mul_le (MeromorphicOn.inv_iff.mpr h₁f₁) (MeromorphicOn.inv_iff.mpr h₁f₂)
+      apply proximity_mul_top_le (MeromorphicOn.inv_iff.mpr h₁f₁) (MeromorphicOn.inv_iff.mpr h₁f₂)
     _ = (proximity f₁ 0) + (proximity f₂ 0) := by
       rw [proximity_inv, proximity_inv]
 
+@[deprecated (since := "2025-12-11")] alias proximity_zero_mul_le := proximity_mul_zero_le
+
 /--
 For natural numbers `n`, the proximity function of `f ^ n` at `⊤` equals `n` times the proximity
 function of `f` at `⊤`.