refactor(Analysis): golf Mathlib/Analysis/Complex/ValueDistribution/CharacteristicFunction (leanprover-community#39182)

- moves the additive lemmas next to the finite-sum version they now reuse
- shortens `characteristic_add_top_le` to a one-line `simpa` from `characteristic_sum_top_le`

Extracted from leanprover-community#37968

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Author: yuanyi-350

Mathlib/Analysis/Complex/ValueDistribution/CharacteristicFunction.lean

@@ -97,36 +97,6 @@ theorem characteristic_eventually_nonneg :
 ## Behaviour under Arithmetic Operations
 -/
 
-/--
-For `1 ≤ r`, the characteristic function of `f + g` at `⊤` is less than or equal to the sum of the
-characteristic functions of `f` and `g`, respectively, plus `log 2` (where `2` is the number of
-summands).
--/
-theorem characteristic_add_top_le {f₁ f₂ : ℂ → E} {r : ℝ} (h₁f₁ : Meromorphic f₁)
-    (h₁f₂ : Meromorphic f₂) (hr : 1 ≤ r) :
-    characteristic (f₁ + f₂) ⊤ r ≤ characteristic f₁ ⊤ r + characteristic f₂ ⊤ r + log 2 := by
-  simp only [characteristic]
-  calc proximity (f₁ + f₂) ⊤ r + logCounting (f₁ + f₂) ⊤ r
-    _ ≤ (proximity f₁ ⊤ r + proximity f₂ ⊤ r + log 2)
-      + (logCounting f₁ ⊤ r + logCounting f₂ ⊤ r) := by
-      gcongr
-      · apply proximity_add_top_le h₁f₁ h₁f₂
-      · exact logCounting_add_top_le h₁f₁ h₁f₂ hr
-    _ = proximity f₁ ⊤ r + logCounting f₁ ⊤ r + (proximity f₂ ⊤ r + logCounting f₂ ⊤ r)
-      + log 2 := by
-      ring
-
-/--
-Asymptotically, the characteristic function of `f + g` at `⊤` is less than or equal to the sum of
-the characteristic functions of `f` and `g`, respectively.
--/
-theorem characteristic_add_top_eventuallyLE {f₁ f₂ : ℂ → E} (h₁f₁ : Meromorphic f₁)
-    (h₁f₂ : Meromorphic f₂) :
-    characteristic (f₁ + f₂) ⊤
-      ≤ᶠ[Filter.atTop] characteristic f₁ ⊤ + characteristic f₂ ⊤ + fun _ ↦ log 2 := by
-  filter_upwards [Filter.eventually_ge_atTop 1] with r hr
-    using characteristic_add_top_le h₁f₁ h₁f₂ hr
-
 /--
 For `1 ≤ r`, the characteristic function of a sum `∑ a, f a` at `⊤` is less than or equal to the sum
 of the characteristic functions of `f ·`, plus `log s.card`.
@@ -156,6 +126,29 @@ theorem characteristic_sum_top_eventuallyLE {α : Type*} (s : Finset α) (f : α
   filter_upwards [Filter.eventually_ge_atTop 1]
     using fun _ hr ↦ characteristic_sum_top_le s f hf hr
 
+/--
+For `1 ≤ r`, the characteristic function of `f + g` at `⊤` is less than or equal to the sum of the
+characteristic functions of `f` and `g`, respectively, plus `log 2` (where `2` is the number of
+summands).
+-/
+theorem characteristic_add_top_le {f₁ f₂ : ℂ → E} {r : ℝ} (h₁f₁ : Meromorphic f₁)
+    (h₁f₂ : Meromorphic f₂) (hr : 1 ≤ r) :
+    characteristic (f₁ + f₂) ⊤ r ≤ characteristic f₁ ⊤ r + characteristic f₂ ⊤ r + log 2 := by
+  have h_meromorphic : ∀ a ∈ Finset.univ, Meromorphic (![f₁, f₂] a) := by
+    simpa using ⟨h₁f₁, h₁f₂⟩
+  simpa using characteristic_sum_top_le Finset.univ ![f₁, f₂] h_meromorphic hr
+
+/--
+Asymptotically, the characteristic function of `f + g` at `⊤` is less than or equal to the sum of
+the characteristic functions of `f` and `g`, respectively.
+-/
+theorem characteristic_add_top_eventuallyLE {f₁ f₂ : ℂ → E} (h₁f₁ : Meromorphic f₁)
+    (h₁f₂ : Meromorphic f₂) :
+    characteristic (f₁ + f₂) ⊤
+      ≤ᶠ[Filter.atTop] characteristic f₁ ⊤ + characteristic f₂ ⊤ + fun _ ↦ log 2 := by
+  filter_upwards [Filter.eventually_ge_atTop 1] with r hr
+    using characteristic_add_top_le h₁f₁ h₁f₂ hr
+
 /--
 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.