feat: formulate identity principle for meromorphic functions on topologically perfect subsets (#37371)

Add a simple, but useful, reformulation of the identity principle for meromorphic functions on topologically perfect subsets. To facilitate application, establish (closures of) open subsets in perfect topological spaces are preperfect sets.

Author: kebekus

Mathlib/Analysis/Meromorphic/Divisor.lean

@@ -6,6 +6,7 @@ Authors: Stefan Kebekus
 module
 
 public import Mathlib.Algebra.Order.WithTop.Untop0
+public import Mathlib.Analysis.Meromorphic.IsolatedZeros
 public import Mathlib.Analysis.Meromorphic.Order
 public import Mathlib.Topology.LocallyFinsupp
 
@@ -93,6 +94,24 @@ theorem divisor_congr_codiscreteWithin_of_eqOn_compl {f₁ f₂ : 𝕜 → E} (h
     tauto
   · simp [hx]
 
+/-
+If two meromorphic functions agree outside a set codiscrete within a perfect set, then they define
+the same divisors there.
+-/
+theorem divisor_of_eventuallyEq_codiscreteWithin_preperfect {f₁ f₂ : 𝕜 → E}
+    (hf₁ : MeromorphicOn f₁ U) (hf₂ : MeromorphicOn f₂ U) (hU : Preperfect U)
+    (h : f₁ =ᶠ[codiscreteWithin U] f₂) :
+    divisor f₁ U = divisor f₂ U := by
+  ext z
+  by_cases hz : z ∉ U
+  · simp_all
+  rw [not_not] at hz
+  rw [divisor_apply hf₁ hz, divisor_apply hf₂ hz]
+  congr 1
+  apply meromorphicOrderAt_congr
+  apply (hf₁ z hz).eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin_preperfect
+    (hf₂ z hz) hz hU h
+
 /--
 If two functions differ only on a discrete set of an open, then they induce the same divisors.
 -/

Mathlib/Analysis/Meromorphic/IsolatedZeros.lean

@@ -94,4 +94,29 @@ theorem eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin (hf : MeromorphicAt
   rw [eventuallyEq_iff_sub] at *
   apply (hf.sub hg).eventuallyEq_zero_nhdsNE_of_eventuallyEq_zero_codiscreteWithin h₁x h₂x h
 
+/-
+Variant of `MeromorphicAt.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin`, as a statement
+about meromorphic functions that agree outside a set codiscrete within a perfect set.
+-/
+theorem eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin_preperfect (hf : MeromorphicAt f x)
+    (hg : MeromorphicAt g x) (hx : x ∈ U) (hU : Preperfect U) (h : f =ᶠ[codiscreteWithin U] g) :
+    f =ᶠ[𝓝[≠] x] g :=
+  hf.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin hg hx (hU x hx) h
+
+/-
+Variant of `MeromorphicAt.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin`, as a statement
+about meromorphic functions agreeing in a neighborhood of a preperfect set.
+-/
+theorem eventually_nhdsSet_eventuallyEq_codiscreteWithin (hf : MeromorphicOn f U)
+    (hg : MeromorphicOn g U) (hU : Preperfect U) (h : f =ᶠ[codiscreteWithin U] g) :
+    ∀ᶠ x in 𝓝ˢ U, f =ᶠ[𝓝[≠] x] g := by
+  rw [eventually_nhdsSet_iff_exists]
+  use {x | f =ᶠ[𝓝[≠] x] g}
+  simp only [Set.mem_setOf_eq, imp_self, implies_true, and_true]
+  constructor
+  · apply isOpen_setOf_eventually_nhdsWithin
+  · intro x hx
+    rw [Set.mem_setOf]
+    exact eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin (hf x hx) (hg x hx) hx (hU x hx) h
+
 end MeromorphicAt

Mathlib/Topology/Perfect.lean

@@ -125,6 +125,20 @@ theorem Preperfect.perfect_closure (hC : Preperfect C) : Perfect (closure C) :=
   rw [closure_eq_cluster_pts] at hx
   exact hx
 
+/-
+Open subsects in perfect spaces are preperfect.
+-/
+theorem IsOpen.preperfect [PerfectSpace α] {U : Set α} (hU : IsOpen U) :
+    Preperfect U := by
+  simpa using PerfectSpace.univ_preperfect.open_inter hU
+
+/-
+Closures of open subsects in perfect spaces are preperfect, hence perfect.
+-/
+theorem IsOpen.perfect_closure [PerfectSpace α] {U : Set α} (hU : IsOpen U) :
+    Perfect (closure U) :=
+  hU.preperfect.perfect_closure
+
 /-- In a T1 space, being preperfect is equivalent to having perfect closure. -/
 theorem preperfect_iff_perfect_closure [T1Space α] : Preperfect C ↔ Perfect (closure C) := by
   constructor <;> intro h