From 7bbf97915c5a5836d9ce620b762abe736f884156 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Fri, 12 Dec 2025 10:49:54 +0100 Subject: [PATCH] Delete 884838fd-52e4-4608-80c9-73a896264eae-output.lean --- ...fd-52e4-4608-80c9-73a896264eae-output.lean | 92 ------------------- 1 file changed, 92 deletions(-) delete mode 100644 884838fd-52e4-4608-80c9-73a896264eae-output.lean diff --git a/884838fd-52e4-4608-80c9-73a896264eae-output.lean b/884838fd-52e4-4608-80c9-73a896264eae-output.lean deleted file mode 100644 index bd95070..0000000 --- a/884838fd-52e4-4608-80c9-73a896264eae-output.lean +++ /dev/null @@ -1,92 +0,0 @@ -/- -This file was edited by Aristotle. - -Lean version: leanprover/lean4:v4.24.0 -Mathlib version: f897ebcf72cd16f89ab4577d0c826cd14afaafc7 - -The following was proved by Aristotle: - -- lemma meromorphic_measurable {f : ℂ → ℂ} (h : MeromorphicOn f ⊤) : - Measurable f --/ - -import Mathlib - - -open MeromorphicOn Real Set Classical Topology - -noncomputable section AristotleLemmas - -#check MeromorphicAt - -#check MeromorphicAt.eventually_analyticAt -#check AnalyticAt.continuousAt -#check Set.Countable.measurableSet -#check Measurable.piecewise - -lemma measurable_of_continuousOn_open_of_countable_closed {f : ℂ → ℂ} {U : Set ℂ} - (hU : IsOpen U) (h_count : Uᶜ.Countable) (h_cont : ContinuousOn f U) : Measurable f := by - -- Assume the contrary, that $f$ is not measurable. - by_contra h_not_measurable; - -- Since $f$ is not measurable, there exists an open set $V$ such that $f^{-1}(V)$ is not measurable. - obtain ⟨V, hV_open, hV_not_meas⟩ : ∃ V : Set ℂ, IsOpen V ∧ ¬ MeasurableSet (f ⁻¹' V) := by - -- By definition of measurability, if $f$ is not measurable, then there exists an open set $V$ such that $f^{-1}(V)$ is not measurable. - have h_not_measurable_def : ¬(∀ V : Set ℂ, IsOpen V → MeasurableSet (f ⁻¹' V)) := by - exact fun h => h_not_measurable <| measurable_of_isOpen h; - aesop; - -- Since $f$ is continuous on $U$, the preimage of any open set under $f|_U$ is open in $U$, hence measurable. - have h_preimage_U_meas : MeasurableSet (f ⁻¹' V ∩ U) := by - -- The preimage of an open set under a continuous function is open. - have h_preimage_open : IsOpen (f ⁻¹' V ∩ U) := by - rw [ isOpen_iff_mem_nhds ] at * ; aesop; - exact h_cont.continuousAt ( hU x right ) |> fun h => h.tendsto.eventually ( hV_open _ left ); - exact h_preimage_open.measurableSet; - -- Since $U^c$ is countable, the preimage $f^{-1}(V)$ can be written as the union of $f^{-1}(V) \cap U$ and $f^{-1}(V) \cap U^c$. - have h_preimage_union : f ⁻¹' V = (f ⁻¹' V ∩ U) ∪ (f ⁻¹' V ∩ Uᶜ) := by - rw [ ← Set.inter_union_distrib_left, Set.union_compl_self, Set.inter_univ ]; - -- Since $U^c$ is countable, the preimage $f^{-1}(V) \cap U^c$ is also countable. - have h_preimage_Uc_countable : Set.Countable (f ⁻¹' V ∩ Uᶜ) := by - exact h_count.mono fun x hx => hx.2; - exact hV_not_meas <| h_preimage_union.symm ▸ MeasurableSet.union h_preimage_U_meas ( h_preimage_Uc_countable.measurableSet ) - -end AristotleLemmas - -lemma meromorphic_measurable {f : ℂ → ℂ} (h : MeromorphicOn f ⊤) : - Measurable f := by - -- The set of singularities of a meromorphic function is countable. - have h_countable : Set.Countable {z : ℂ | ¬AnalyticAt ℂ f z} := by - -- Let $S$ be the set of points where $f$ is not analytic. For each $z \in S$, there exists a neighborhood around $z$ where $f$ is analytic except at $z$. - set S := {z : ℂ | ¬AnalyticAt ℂ f z} - have h_discrete : ∀ z ∈ S, ∃ ε > 0, ∀ w ∈ Metric.ball z ε, w ≠ z → AnalyticAt ℂ f w := by - -- Since $f$ is meromorphic on the entire complex plane, for any $z \in S$, there exists an $\epsilon > 0$ such that $f$ is analytic on the punctured disk around $z$ (excluding $z$ itself). - have h_meromorphic : ∀ z ∈ S, ∃ ε > 0, ∀ w ∈ Metric.ball z ε, w ≠ z → AnalyticAt ℂ f w := by - intro z hz - have h_meromorphic_at_z : MeromorphicAt f z := by - exact? - -- By definition of MeromorphicAt, there exists a neighborhood around z where f is analytic except at z itself. - have h_neighborhood : ∀ᶠ w in 𝓝[≠] z, AnalyticAt ℂ f w := by - exact?; - rw [ eventually_nhdsWithin_iff ] at h_neighborhood; - rw [ Metric.eventually_nhds_iff ] at h_neighborhood; aesop; - assumption; - -- Since $S$ is discrete, it is countable. - have h_countable : DiscreteTopology S := by - -- To show that S is discrete, we use the fact that for each z in S, there exists an ε > 0 such that the ball around z with radius ε contains no other points of S except z itself. - have h_discrete : ∀ z ∈ S, ∃ ε > 0, Metric.ball z ε ∩ S = {z} := by - exact fun z hz => by obtain ⟨ ε, ε_pos, hε ⟩ := h_discrete z hz; exact ⟨ ε, ε_pos, Set.eq_singleton_iff_unique_mem.mpr ⟨ ⟨ Metric.mem_ball_self ε_pos, hz ⟩, fun w hw => Classical.not_not.1 fun hw' => hw.2 <| hε w hw.1 hw' ⟩ ⟩ ; - refine' singletons_open_iff_discrete.mp _; - intro z; specialize h_discrete z z.2; aesop; - rw [ Set.eq_singleton_iff_unique_mem ] at right ; aesop; - exact ⟨ Metric.ball val w, Metric.isOpen_ball, by ext ⟨ x, hx ⟩ ; specialize right x; aesop ⟩; - exact Set.countable_coe_iff.mp ( by exact? ); - -- Since $U$ is open and $f$ is continuous on $U$, and the complement of $U$ is countable, we can apply the lemma to conclude that $f$ is measurable. - have h_measurable : Measurable f := by - have hU : IsOpen {z : ℂ | AnalyticAt ℂ f z} := by - exact? - have h_cont : ContinuousOn f {z : ℂ | AnalyticAt ℂ f z} := by - exact fun x hx => hx.continuousAt.continuousWithinAt - have h_count : {z : ℂ | ¬AnalyticAt ℂ f z}.Countable := by - -- Apply the fact that the set of points where f is not analytic is countable. - exact h_countable - exact measurable_of_continuousOn_open_of_countable_closed hU h_count h_cont; - exact h_measurable \ No newline at end of file