From 1f6fcd938af2bff932a11160b0458b4bea56f6e9 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Mon, 8 Dec 2025 07:17:08 +0100 Subject: [PATCH] Create 884838fd-52e4-4608-80c9-73a896264eae-output.lean --- ...fd-52e4-4608-80c9-73a896264eae-output.lean | 92 +++++++++++++++++++ 1 file changed, 92 insertions(+) create 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 new file mode 100644 index 0000000..bd95070 --- /dev/null +++ b/884838fd-52e4-4608-80c9-73a896264eae-output.lean @@ -0,0 +1,92 @@ +/- +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