feat: add simple congruence lemmata for meromorphicity and value distribution theory (#34302)

kebekus · kebekus · commit 65ada599cba6 · 2026-01-28T06:03:45.000Z
Add simple congruence lemmas for meromorphicity and the main functions of Value Distribution Theory. Remove unnecessary assumption from `divisor_congr_codiscreteWithin`. Minor golfing.
diff --git a/Mathlib/Analysis/Complex/ValueDistribution/CharacteristicFunction.lean b/Mathlib/Analysis/Complex/ValueDistribution/CharacteristicFunction.lean
@@ -33,13 +33,13 @@ Approximation*][MR3156076] for a detailed discussion.
 
 @[expose] public section
 
-open Metric Real Set
+open Filter Metric Real Set
 
 namespace ValueDistribution
 
 variable
   {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
-  {f : ℂ → E} {a : WithTop E}
+  {f g : ℂ → E} {a : WithTop E}
 
 variable (f a) in
 /--
@@ -56,6 +56,14 @@ noncomputable def characteristic : ℝ → ℝ := proximity f a + logCounting f
 ## Elementary Properties
 -/
 
+/--
+If two functions differ only on a discrete set, then their characteristic functions agree, except
+perhaps at radius 0.
+-/
+theorem characteristic_congr_codiscrete {r : ℝ} (hfg : f =ᶠ[codiscrete ℂ] g) (hr : r ≠ 0) :
+    characteristic f a r = characteristic g a r := by
+  simp [characteristic, proximity_congr_codiscrete hfg hr, logCounting_congr_codiscrete hfg]
+
 /--
 The difference between the characteristic functions for the poles of `f` and `f - const` simplifies
 to the difference between the proximity functions.
@@ -68,20 +76,20 @@ lemma characteristic_sub_characteristic_eq_proximity_sub_proximity (h : Meromorp
 /--
 The characteristic function is even.
 -/
-theorem characteristic_even {a : WithTop E} :
+theorem characteristic_even :
     (characteristic f a).Even := proximity_even.add logCounting_even
 
 /--
 For `1 ≤ r`, the characteristic function is non-negative.
 -/
-theorem characteristic_nonneg {r : ℝ} {a : WithTop E} (hr : 1 ≤ r) :
+theorem characteristic_nonneg {r : ℝ} (hr : 1 ≤ r) :
     0 ≤ characteristic f a r :=
   add_nonneg (proximity_nonneg r) (logCounting_nonneg hr)
 
 /--
 The characteristic function is asymptotically non-negative.
 -/
-theorem characteristic_eventually_nonneg {f : ℂ → ℂ} {a : WithTop ℂ} :
+theorem characteristic_eventually_nonneg :
     0 ≤ᶠ[Filter.atTop] characteristic f a := by
   filter_upwards [Filter.eventually_ge_atTop 1] using fun _ hr ↦ by simp [characteristic_nonneg hr]
 
diff --git a/Mathlib/Analysis/Complex/ValueDistribution/LogCounting/Basic.lean b/Mathlib/Analysis/Complex/ValueDistribution/LogCounting/Basic.lean
@@ -40,7 +40,7 @@ Approximation*][MR3156076] for a detailed discussion.
 
 @[expose] public section
 
-open Function MeromorphicOn Metric Real Set
+open Filter Function MeromorphicOn Metric Real Set
 
 /-!
 ## Supporting Notation
@@ -337,6 +337,22 @@ theorem logCounting_eventually_nonneg {f : 𝕜 → E} {e : WithTop E} :
 ## Elementary Properties of the Logarithmic Counting Function
 -/
 
+/--
+If two functions differ only on a discrete set, then their logarithmic counting
+functions agree.
+-/
+theorem logCounting_congr_codiscrete [NormedSpace ℂ E] {f g : ℂ → E} (hfg : f =ᶠ[codiscrete ℂ] g) :
+    logCounting f = logCounting g := by
+  ext a : 1
+  by_cases h : a = ⊤
+  · simp only [logCounting, h, ↓reduceDIte]
+    congr 2
+    exact divisor_congr_codiscreteWithin hfg isOpen_univ
+  · simp only [logCounting, h, ↓reduceDIte]
+    congr 2
+    apply divisor_congr_codiscreteWithin _ isOpen_univ
+    filter_upwards [hfg] using by simp
+
 /--
 Relation between the logarithmic counting functions of `f` and of `f⁻¹`.
 -/
diff --git a/Mathlib/Analysis/Complex/ValueDistribution/Proximity/Basic.lean b/Mathlib/Analysis/Complex/ValueDistribution/Proximity/Basic.lean
@@ -28,7 +28,7 @@ Approximation*][MR3156076] for a detailed discussion.
 
 @[expose] public section
 
-open Metric Real Set
+open Filter Metric Real Set
 
 namespace ValueDistribution
 
@@ -81,6 +81,28 @@ lemma proximity_top : proximity f ⊤ = circleAverage (log⁺ ‖f ·‖) 0 := b
 ## Elementary Properties of the Proximity Function
 -/
 
+/--
+If two functions differ only on a discrete set, then their proximity functions
+agree, except perhaps at radius 0.
+-/
+lemma proximity_congr_codiscreteWithin {f g : ℂ → E} {a : WithTop E} {r : ℝ}
+    (hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g) (hr : r ≠ 0) :
+    proximity f a r = proximity g a r := by
+  by_cases h : a = ⊤
+  all_goals
+    simp only [proximity, h, ↓reduceDIte]
+    apply circleAverage_congr_codiscreteWithin _ hr
+    filter_upwards [hfg] using by aesop
+
+/--
+If two functions differ only on a discrete set, then their proximity functions
+agree, except perhaps at radius 0.
+-/
+lemma proximity_congr_codiscrete {f g : ℂ → E} {a : WithTop E} {r : ℝ}
+    (hfg : f =ᶠ[codiscrete ℂ] g) (hr : r ≠ 0) :
+    proximity f a r = proximity g a r :=
+  proximity_congr_codiscreteWithin (hfg.filter_mono (codiscreteWithin.mono (by tauto))) hr
+
 /--
 For finite values `a₀`, the proximity function `proximity f a₀` equals the proximity function for
 the value zero of the shifted function `f - a₀`.
@@ -126,6 +148,10 @@ theorem proximity_nonneg {a : WithTop E} :
   · intro r
     simpa [proximity, h] using circleAverage_nonneg_of_nonneg (fun x _ ↦ posLog_nonneg)
 
+@[simp] lemma proximity_const {c : E} {r : ℝ} :
+    proximity (fun _ ↦ c) ⊤ r = log⁺ ‖c‖ := by
+  simp [proximity, circleAverage_const]
+
 /-!
 ## Behaviour under Arithmetic Operations
 -/
diff --git a/Mathlib/Analysis/Meromorphic/Basic.lean b/Mathlib/Analysis/Meromorphic/Basic.lean
@@ -466,6 +466,15 @@ theorem congr_codiscreteWithin (hf : MeromorphicOn f U) (h₁ : f =ᶠ[codiscret
   simp only [Set.mem_compl_iff, Set.mem_diff, Set.mem_setOf_eq, not_and] at h₂a
   tauto
 
+/--
+If two functions differ only on a discrete set of an open, then one is meromorphic iff so is the
+other.
+-/
+theorem _root_.meromorphicOn_congr_codiscreteWithin {f g : 𝕜 → E} (h₁ : f =ᶠ[codiscreteWithin U] g)
+    (h₂ : IsOpen U) :
+    MeromorphicOn f U ↔ MeromorphicOn g U :=
+  ⟨(·.congr_codiscreteWithin h₁ h₂), (·.congr_codiscreteWithin h₁.symm h₂)⟩
+
 lemma id {U : Set 𝕜} : MeromorphicOn id U := fun x _ ↦ .id x
 
 lemma const (e : E) {U : Set 𝕜} : MeromorphicOn (fun _ ↦ e) U :=
@@ -651,6 +660,21 @@ protected lemma deriv [CompleteSpace E] (hf : Meromorphic f) : Meromorphic (deri
 lemma iterated_deriv [CompleteSpace E] {n : ℕ} (hf : Meromorphic f) :
     Meromorphic (deriv^[n] f) := fun x ↦ (hf x).iterated_deriv
 
+/--
+If `f` is meromorphic, if `g` agrees with `f` on a codiscrete set, then `g` is also meromorphic.
+-/
+theorem congr_codiscrete (hf : Meromorphic f) (h₁ : f =ᶠ[codiscrete 𝕜] g) :
+    Meromorphic g := by
+  rw [← meromorphicOn_univ] at *
+  exact hf.congr_codiscreteWithin (eventuallyEq_of_mem h₁ fun ⦃x⦄ a ↦ a) isOpen_univ
+
+/--
+If two functions differ only on a discrete set, then one is meromorphic iff so is the other.
+-/
+theorem _root_.meromorphic_congr_codiscrete (h₁ : f =ᶠ[codiscrete 𝕜] g) :
+    Meromorphic f ↔ Meromorphic g :=
+  ⟨(·.congr_codiscrete h₁), (·.congr_codiscrete h₁.symm)⟩
+
 /--
 The singular set of a meromorphic function is countable.
 -/
diff --git a/Mathlib/Analysis/Meromorphic/Divisor.lean b/Mathlib/Analysis/Meromorphic/Divisor.lean
@@ -76,41 +76,41 @@ If `f₁` is meromorphic on `U`, if `f₂` agrees with `f₁` on a codiscrete su
 `U`, then `f₁` and `f₂` induce the same divisors on `U`.
 -/
 theorem divisor_congr_codiscreteWithin_of_eqOn_compl {f₁ f₂ : 𝕜 → E} (hf₁ : MeromorphicOn f₁ U)
-    (h₁ : f₁ =ᶠ[Filter.codiscreteWithin U] f₂) (h₂ : Set.EqOn f₁ f₂ Uᶜ) :
+    (h₁ : f₁ =ᶠ[codiscreteWithin U] f₂) (h₂ : Set.EqOn f₁ f₂ Uᶜ) :
     divisor f₁ U = divisor f₂ U := by
   ext x
   by_cases hx : x ∈ U
   · simp only [hf₁, hx, divisor_apply, hf₁.congr_codiscreteWithin_of_eqOn_compl h₁ h₂]
     congr 1
     apply meromorphicOrderAt_congr
-    simp_rw [EventuallyEq, Filter.Eventually, mem_codiscreteWithin,
-      disjoint_principal_right] at h₁
+    simp_rw [EventuallyEq, Filter.Eventually, mem_codiscreteWithin, disjoint_principal_right] at h₁
     filter_upwards [h₁ x hx] with a ha
     simp at ha
     tauto
   · simp [hx]
 
 /--
-If `f₁` is meromorphic on an open set `U`, if `f₂` agrees with `f₁` on a codiscrete subset of `U`,
-then `f₁` and `f₂` induce the same divisors on `U`.
+If two functions differ only on a discrete set of an open, then they induce the same divisors.
 -/
-theorem divisor_congr_codiscreteWithin {f₁ f₂ : 𝕜 → E} (hf₁ : MeromorphicOn f₁ U)
-    (h₁ : f₁ =ᶠ[Filter.codiscreteWithin U] f₂) (h₂ : IsOpen U) :
+theorem divisor_congr_codiscreteWithin {f₁ f₂ : 𝕜 → E} (h₁ : f₁ =ᶠ[codiscreteWithin U] f₂)
+    (h₂ : IsOpen U) :
     divisor f₁ U = divisor f₂ U := by
-  ext x
-  by_cases hx : x ∈ U
-  · simp only [hf₁, hx, divisor_apply, hf₁.congr_codiscreteWithin h₁ h₂]
-    congr 1
-    apply meromorphicOrderAt_congr
-    simp_rw [EventuallyEq, Filter.Eventually, mem_codiscreteWithin,
-      disjoint_principal_right] at h₁
-    have : U ∈ 𝓝[≠] x := by
-      apply mem_nhdsWithin.mpr
-      use U, h₂, hx, Set.inter_subset_left
-    filter_upwards [this, h₁ x hx] with a h₁a h₂a
-    simp only [Set.mem_compl_iff, Set.mem_diff, Set.mem_setOf_eq, not_and] at h₂a
-    tauto
-  · simp [hx]
+  by_cases hf₁ : MeromorphicOn f₁ U
+  · ext x
+    by_cases hx : x ∈ U
+    · simp only [hf₁, hx, divisor_apply, hf₁.congr_codiscreteWithin h₁ h₂]
+      congr 1
+      apply meromorphicOrderAt_congr
+      simp_rw [EventuallyEq, Filter.Eventually, mem_codiscreteWithin,
+        disjoint_principal_right] at h₁
+      have : U ∈ 𝓝[≠] x := by
+        apply mem_nhdsWithin.mpr
+        use U, h₂, hx, Set.inter_subset_left
+      filter_upwards [this, h₁ x hx] with a h₁a h₂a
+      simp only [Set.mem_compl_iff, Set.mem_diff, Set.mem_setOf_eq, not_and] at h₂a
+      tauto
+    · simp [hx]
+  · simp [divisor, hf₁, (meromorphicOn_congr_codiscreteWithin h₁ h₂).not.1 hf₁]
 
 /-!
 ## Divisors of Analytic Functions
