Update Basic.lean

Aristotle/Basic.lean

@@ -1,53 +1,45 @@
 import Mathlib
 
-open MeromorphicOn Real Set Classical Topology
+open Filter Set Topology
 
 variable
   {𝕜 : Type*} [NontriviallyNormedField 𝕜]
   {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
-  {X : Type*} {x : X} [TopologicalSpace X]
-
-theorem eventually_nhdsWithin_eventually_nhds_iff_of_isOpen {s : Set X} {a : X} {p : X → Prop}
-    (hs : IsOpen s) : (∀ᶠ y in 𝓝[s] a, ∀ᶠ x in 𝓝 y, p x) ↔ ∀ᶠ x in 𝓝[s] a, p x := by
-  nth_rw 2 [← eventually_eventually_nhdsWithin]
-  constructor
-  · intro h
-    filter_upwards [h] with _ hy
-    exact eventually_nhdsWithin_of_eventually_nhds hy
-  · intro h
-    filter_upwards [h, eventually_nhdsWithin_of_forall fun _ a ↦ a] with _ _ _
-    simp_all [IsOpen.nhdsWithin_eq]
-
-@[simp]
-theorem eventually_nhdsNE_eventually_nhds_iff [T1Space X] {a : X} {p : X → Prop} :
-    (∀ᶠ y in 𝓝[≠] a, ∀ᶠ x in 𝓝 y, p x) ↔ ∀ᶠ x in 𝓝[≠] a, p x :=
-  eventually_nhdsWithin_eventually_nhds_iff_of_isOpen isOpen_ne
-
-theorem Filter.EventuallyEq.nhdsNE_deriv {f f₁ : 𝕜 → E} {x : 𝕜} (h : f₁ =ᶠ[𝓝[≠] x] f) :
-    deriv f₁ =ᶠ[𝓝[≠] x] deriv f := by
-  rw [Filter.EventuallyEq, ← eventually_nhdsNE_eventually_nhds_iff] at *
-  filter_upwards [h] with y hy
-  apply Filter.EventuallyEq.deriv hy
+  {f : 𝕜 → E} {U : Set 𝕜}
 
 /--
-Derivatives of meromorphic functions are meromorphic.
+The singular set of a meromorphic function is countable.
 -/
-@[fun_prop]
-protected theorem MeromorphicAt.deriv [CompleteSpace E] {f : 𝕜 → E} {x : 𝕜} (h : MeromorphicAt f x) :
-    MeromorphicAt (deriv f) x := by
-  rw [MeromorphicAt.iff_eventuallyEq_zpow_smul_analyticAt] at h
-  obtain ⟨n, g, h₁g, h₂g⟩ := h
-  have : _root_.deriv (fun z ↦ (z - x) ^ n • g z)
-      =ᶠ[𝓝[≠] x] fun z ↦ (n * (z - x) ^ (n - 1)) • g z + (z - x) ^ n • _root_.deriv g z := by
-    filter_upwards [eventually_nhdsWithin_of_eventually_nhds h₁g.eventually_analyticAt,
-      eventually_nhdsWithin_of_forall fun _ a ↦ a] with z₀ h₁ h₂
-    rw [deriv_smul (DifferentiableAt.zpow (by fun_prop) (by simp_all [sub_ne_zero_of_ne h₂]))
-      (by fun_prop), add_comm, deriv_comp_sub_const (f := (· ^ n))]
-    aesop
-  rw [MeromorphicAt.meromorphicAt_congr (Filter.EventuallyEq.nhdsNE_deriv h₂g),
-    MeromorphicAt.meromorphicAt_congr this]
-  sorry
+theorem MeromorphicOn.countable_compl_analyticAt [SecondCountableTopology 𝕜] [CompleteSpace E]
+    (h : MeromorphicOn f U) :
+    ({z | AnalyticAt 𝕜 f z}ᶜ ∩ U).Countable := by
+  classical
+  have := discreteTopology_of_codiscreteWithin (eventually_codiscreteWithin_analyticAt f h)
+  apply countable_of_Lindelof_of_discrete
 
-theorem MeromorphicAt.order_deriv [CompleteSpace E] {f : 𝕜 → E} {x : 𝕜} (h : MeromorphicAt f x) (h₂ : h.order ≠ 0) :
-    h.deriv.order = h.order -1 := by
+
+variable
+  [MeasurableSpace 𝕜] [SecondCountableTopology 𝕜] [BorelSpace 𝕜]
+  [MeasurableSpace E] [CompleteSpace E] [BorelSpace E]
+
+/--
+Meromorphic functions are measurable.
+-/
+theorem meromorphic_measurable {f : 𝕜 → E} (h : MeromorphicOn f Set.univ) :
+    Measurable f := by
+  set s := {z : 𝕜 | AnalyticAt 𝕜 f z}
+  have h₁ : sᶜ.Countable  := by simpa using h.countable_compl_analyticAt
+  have h₂ : IsOpen s := isOpen_analyticAt 𝕜 f
+  have h₃ : ContinuousOn f s := fun z hz ↦ hz.continuousAt.continuousWithinAt
+  apply measurable_of_isOpen
+  intro V hV
+  rw [(by aesop : f ⁻¹' V = (f ⁻¹' V ∩ s) ∪ (f ⁻¹' V ∩ sᶜ))]
+  apply MeasurableSet.union (IsOpen.measurableSet _) (h₁.mono inter_subset_right).measurableSet
+  rw [isOpen_iff_mem_nhds] at *
+  intro x a
+  simp_all [mem_setOf_eq, mem_inter_iff, mem_preimage, inter_mem_iff, and_true, s]
+  apply h₃.continuousAt (h₂ x a.2) (hV (f x) a.1)
+
+lemma ρ₀ {r : ℝ} {hr : r ≠ 0} {f g : ℝ → ℂ} (h : MeromorphicOn f Set.univ) :
+    Measurable (fun x ↦ f x.1 + g x.2 : ℝ × ℝ → ℂ) := by
   sorry