Roots of meromorphic function on a connected set

Stream: maths

[Daniel Weber]

I want this result:

import Mathlib

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]

example (f : 𝕜 → E) (U : Set 𝕜) (hf : MeromorphicOn f U) (hu : IsConnected U) :
    IsTotallyDisconnected (U ∩ (f ⁻¹' {0})) ∨ IsTotallyDisconnected (U \ (f ⁻¹' {0})) := by
  sorry

which I can't find in Mathlib. Is docs#IsTotallyDisconnected the correct thing to use here? Are there assumptions I'm missing?

[David Loeffler]

We almost certainly don't have this. There is very little API for meromorphic functions at present (we have a definition but not much more). Would the version for holomorphic functions be enough for you, or do you really need meromorphic?

[Daniel Weber]

I want to define the field of meromorphic functions (up to equality AE) on a connected set, so I think I need this to show that division works

[Daniel Weber]

I managed to get

import Mathlib

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]

open MeasureTheory Filter

@[simp]
lemma not_and_and_not_self {a b : Prop} : ¬(a ∧ b ∧ ¬ a) := by
  simp only [not_and, not_not]
  exact fun a _ ↦ a

example (f : 𝕜 → E) (U : Set 𝕜) (hf : MeromorphicOn f U) (hu : IsConnected U) :
    IsTotallyDisconnected (U ∩ (f ⁻¹' {0})) ∨ IsTotallyDisconnected (U \ (f ⁻¹' {0})) := by
  by_contra! nh
  suffices ∃ x ∈ U, AccPt x (𝓟 (U ∩ (f ⁻¹' {0}))) ∧ AccPt x (𝓟 (U \ (f ⁻¹' {0}))) by
    obtain ⟨x, hxu, h1, h2⟩ := this
    obtain ⟨n, hn⟩ := hf x hxu
    rw [accPt_iff_nhds] at h1 h2
    rcases AnalyticAt.eventually_eq_zero_or_eventually_ne_zero hn with h | h
    · rw [eventually_iff] at h
      obtain ⟨y, hy1, hy2⟩ := h2 _ h
      simp_all [sub_eq_zero]
    · rw [eventually_iff, mem_nhdsWithin_iff_exists_mem_nhds_inter] at h
      obtain ⟨h, hn⟩ := h
      obtain ⟨y, hy1, hy2⟩ := h1 _ hn.1
      simp_all only [ne_eq, smul_eq_zero, pow_eq_zero_iff', not_or, not_and, Decidable.not_not,
        Set.mem_diff, Set.mem_inter_iff, Set.mem_preimage, Set.mem_singleton_iff]
      have : y ∈ h ∩ {x}ᶜ := by simp [*]
      apply hn.2 at this
      simp_all
  sorry

but I'm not sure how to do the topology for the last part (or if it's even true--it feels correct, but I don't know topology well).

[Daniel Weber]

I just realized that docs#IsTotallyDisconnected isn't what I want, how do I state that a set is discrete?

[Kevin Buzzard]

Right, {1/n : n in N+} union {0} is totally disconnected but not discrete.

[Yakov Pechersky]

Does docs#IsTotallySeparated work for you?

[Daniel Weber]

What I actually need is that it has measure zero, I'm not sure exactly what implies that

[Kevin Buzzard]

I should think that a cantor set can have positive measure and be totally separated?

[Daniel Weber]

Currently I'm trying to prove

import Mathlib

variable {𝕜 : Type*}  [TopologicalSpace 𝕜]

open Filter

example (U : Set 𝕜) (hs : IsPreconnected U) (a b : Set 𝕜) (h : a ∪ b = U)
    (ha : ∃ x ∈ U, AccPt x (𝓟 a)) (hb : ∃ x ∈ U, AccPt x (𝓟 b)) :
    ∃ x ∈ U, AccPt x (𝓟 a) ∧ AccPt x (𝓟 b) := by sorry

but I'm not sure if it's even true. Using docs#isPreconnected_closed_iff on the closures of a and b I can show that there's a docs#ClusterPt common to a and b, but that's not enough

EDIT: It also required T1Space 𝕜, but I managed to prove this

[David Loeffler]

Somehow, AE-equality feels like the wrong notion here; I think it should be enough to work with equality away from a discrete closed subset (i.e. eventual equality for the filter docs#Filter.codiscrete). This has the advantage that if f and g are eventually equal along this filter, then f is meromorphic iff g is (which isn't true for ae-equality, or equality away from a totally-disconnected set).

[Daniel Weber]

hmm. This also lets me not talk about measures at all, right?

[Daniel Weber]

Do you think it makes more sense to first define a ring for all functions and have the field of meromorphic functions as a subtype of that, or should this field just be defined directly?

[Kevin Buzzard]

I thought that the decision was that a meromorphic function isn't a function (it's an equivalence class) but maybe I'm behind the times

[Daniel Weber]

Yeah, I'm taking a quotient

[Kevin Buzzard]

Oh I see -- you're proposing taking the quotient to make the "ring for all functions" and then making a subtype of that.

[Daniel Weber]

Yes, compared to directly taking a quotient on the subtype of meromorphic functions

[Vincent Beffara]

How about defining the field of fractions of the ring of holomorphic functions?

[Daniel Weber]

The benefit being that there's no need for a quotient? Showing that the ring of analytic functions form a domain would require a similar theorem, but I have already proved most prerequisites for it, so that's fine. It might be difficult to show it agrees with docs#MeromorphicOn, though

[Daniel Weber]

What even are the conditions on the domain and range for this to be true?

[Daniel Weber]

Could someone please move this to #maths , by the way?

[Vincent Beffara]

Daniel Weber said:

What even are the conditions on the domain and range for this to be true?

Every meromorphic functions on a open set U of the complex plane (with values in \C \cup \{\infty\}) is a quotient of two holomorphic functions on U, see e.g. Theorem 15.12 in Rudin. (It is nontrivial and uses Weierstrass factorization, which AFAIK is not in Mathlib but would be worth adding.)

[Kevin Buzzard]

This statement is more subtle than it might seem at first glance because when both f and g vanish at z, f/g still has a well-defined value at z, it just depends on more than f and g at z.

[Daniel Weber]

Vincent Beffara said:

Daniel Weber said:

What even are the conditions on the domain and range for this to be true?

Every meromorphic functions on a open set U of the complex plane (with values in \C \cup \{\infty\}) is a quotient of two holomorphic functions on U, see e.g. Theorem 15.12 in Rudin. (It is nontrivial and uses Weierstrass factorization, which AFAIK is not in Mathlib but would be worth adding.)

I know this, but is this also true for analytic functions on an open subset of $\mathbb{R}$? A general normed field? I think this should be stated as generally as possible.

[Daniel Weber]

Kevin Buzzard said:

This statement is more subtle than it might seem at first glance because when both f and g vanish at z, f/g still has a well-defined value at z, it just depends on more than f and g at z.

In Mathlib's definition of docs#MeromorphicOn simply f/g is a meromorphic function, see docs#MeromorphicOn.div nvm, I think I misunderstood what you're saying. The statement would be that for any meromorphic h there are analytic f, g such that f/g is eventually equal to h on docs#Filter.codiscrete, I think

[Kevin Buzzard]

I guess what I'm saying is just covered by the assertion that in every equivalence class there is a unique holomorphic representative taking values in C union infinity.

[Vincent Beffara]

Daniel Weber said:

Vincent Beffara said:

Daniel Weber said:

What even are the conditions on the domain and range for this to be true?

Every meromorphic functions on a open set U of the complex plane (with values in \C \cup \{\infty\}) is a quotient of two holomorphic functions on U, see e.g. Theorem 15.12 in Rudin. (It is nontrivial and uses Weierstrass factorization, which AFAIK is not in Mathlib but would be worth adding.)

I know this, but is this also true for analytic functions on an open subset of $\mathbb{R}$? A general normed field? I think this should be stated as generally as possible.

At least for an open subset of R it should extend painlessly (theorem 15.11 in Rudin asserts that given an open set U in the complex plane and a locally finite set of A with prescribed orders on it, there is a holomorphic function on U having exactly these as zeroes; if instead U is an open set of R, take V to be U union (C - R) and apply that theorem in V, I don't see anything going wrong).

The general Weierstrass product construction might work on any complete field?

[Kevin Buzzard]

There's a Weierstrass factorization theorem in nonarchimedean analysis; a random google gives this for example. IIRC Bosch-Guentzer-Remmert has a version which doesn't assume alg closed (there is also a Weierstrass preparation theorem etc).

[Daniel Weber]

I've thought about this a bit more, and I think that for the result I want to prove (e^x^2 doesn't have an elementary antiderivative) it makes more sense to define it using quotient types and later an IsFractionRing instance could be proved for it

[Daniel Weber]

Currently I'm doing this. Is there a nicer way to construct the Field instance?

import Mathlib.Analysis.Analytic.Meromorphic

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] (U : Set 𝕜)

open Filter Topology

structure PreMF where
  toFun : 𝕜 → 𝕜
  meromorphicOn : MeromorphicOn toFun U

instance PreMF.setoid : Setoid (PreMF U) where
  r := fun f g ↦ f.toFun ∘ Subtype.val =ᶠ[codiscrete U] g.toFun ∘ Subtype.val
  iseqv := {
    trans := EventuallyEq.trans
    refl := fun _ ↦ EventuallyEq.rfl
    symm := EventuallyEq.symm
  }

def MF := Quotient (PreMF.setoid U)

variable [Fact (IsPreconnected U)]

instance : Field (MF U) where
  zero := ⟦⟨0, MeromorphicOn.const 0⟩⟧
  one := ⟦⟨1, MeromorphicOn.const 1⟩⟧
  add := Quotient.lift₂ (fun x y ↦ ⟦⟨x.1 + y.1, x.2.add y.2⟩⟧) (fun _ _ _ _ h₁ h₂ ↦
    Quotient.sound <| Filter.EventuallyEq.add h₁ h₂)
  neg := Quotient.lift (fun x ↦ ⟦⟨-x.1, x.2.neg⟩⟧) (fun _ _ h ↦
    Quotient.sound <| Filter.EventuallyEq.neg h)
  mul := Quotient.lift₂ (fun x y ↦ ⟦⟨x.1 * y.1, x.2.mul y.2⟩⟧) (fun _ _ _ _ h₁ h₂ ↦
    Quotient.sound <| Filter.EventuallyEq.mul h₁ h₂)
  inv := Quotient.lift (fun x ↦ ⟦⟨x.1⁻¹, x.2.inv⟩⟧) (fun _ _ h ↦
    Quotient.sound <| Filter.EventuallyEq.inv h)
  add_assoc a b c := by
    induction' a using Quotient.ind with a
    induction' b using Quotient.ind with b
    induction' c using Quotient.ind with c
    change ⟦⟨a.1 + b.1 + c.1, _⟩⟧ = (⟦⟨a.1 + (b.1 + c.1), _⟩⟧ : MF U)
    congr 2
    apply add_assoc
  add_comm a b := by
    induction' a using Quotient.ind with a
    induction' b using Quotient.ind with b
    change ⟦⟨a.1 + b.1, _⟩⟧ = (⟦⟨b.1 + a.1, _⟩⟧ : MF U)
    congr 2
    apply add_comm
  zero_add a := by
    induction' a using Quotient.ind with a
    change ⟦⟨0 + a.1, _⟩⟧ = ⟦a⟧
    congr
    apply zero_add
  add_zero a := by
    induction' a using Quotient.ind with a
    change ⟦⟨a.1 + 0, _⟩⟧ = ⟦a⟧
    congr
    apply add_zero
  left_distrib a b c := by
    induction' a using Quotient.ind with a
    induction' b using Quotient.ind with b
    induction' c using Quotient.ind with c
    change ⟦⟨a.1 * (b.1 + c.1), _⟩⟧ = (⟦⟨a.1 * b.1 + a.1 * c.1, _⟩⟧ : MF U)
    congr
    apply left_distrib

[Daniel Weber]

Perhaps I don't need to actually work with meromorphic functions, as I can move to a region where the function is analytic. Do I need to assume that the space is locally connected to be able to do that?

[Vincent Beffara]

I would tend to start like this from analytic functions, likely something similar can be done in your case:

import Mathlib

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
variable (U : Set 𝕜) [Fact (IsOpen U)] [Fact (IsConnected U)]

def An : Subring (𝕜 → 𝕜) where
  carrier := { f : 𝕜 → 𝕜 | AnalyticOn 𝕜 f U }
  zero_mem' := analyticOn_const (v := 0)
  one_mem' := analyticOn_const (v := 1)
  mul_mem' := AnalyticOn.mul
  add_mem' := AnalyticOn.add
  neg_mem' := AnalyticOn.neg

def Zer : Ideal (An U) where
  carrier := { f | ∀ x ∈ U, f.1 x = 0 }
  zero_mem' _ _ := rfl
  add_mem' hf hg x hx := by simp [hf x hx, hg x hx]
  smul_mem' f g hg x hx := by simp [hg x hx]

instance : (Zer U).IsPrime where
  ne_top' := by
    rename_i inst ; obtain ⟨x, hx⟩ := inst.out.nonempty
    rw [Ideal.ne_top_iff_one]
    intro h1
    simpa using h1 x hx
  mem_or_mem' {f g} hfg := sorry -- this is from isolated zeros

abbrev Mero := FractionRing (An U ⧸ Zer U)

#synth Field (Mero U)

[Daniel Weber]

Oh, a quotient by an ideal is much nicer than constructing a relation and proving everything about a quotient of it

[Antoine Chambert-Loir]

Kevin Buzzard said:

)

Analytic functions of nonarchimedean analysis are not mathlib's analytic functions. For mathlib, a locally constant function on a (complete) nonarchimedean field $K$ is analytic, but not for Bosch-Güntzer-Remmert unless it is constant.

[Antoine Chambert-Loir]

In the nonarchimedean setting, all “connected”-like hypothesis will be almost never applicable.

[Daniel Weber]

Vincent Beffara said:

I would tend to start like this from analytic functions, likely something similar can be done in your case:

import Mathlib

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
variable (U : Set 𝕜) [Fact (IsOpen U)] [Fact (IsConnected U)]

def An : Subring (𝕜 → 𝕜) where
  carrier := { f : 𝕜 → 𝕜 | AnalyticOn 𝕜 f U }
  zero_mem' := analyticOn_const (v := 0)
  one_mem' := analyticOn_const (v := 1)
  mul_mem' := AnalyticOn.mul
  add_mem' := AnalyticOn.add
  neg_mem' := AnalyticOn.neg

def Zer : Ideal (An U) where
  carrier := { f | ∀ x ∈ U, f.1 x = 0 }
  zero_mem' _ _ := rfl
  add_mem' hf hg x hx := by simp [hf x hx, hg x hx]
  smul_mem' f g hg x hx := by simp [hg x hx]

instance : (Zer U).IsPrime where
  ne_top' := by
    rename_i inst ; obtain ⟨x, hx⟩ := inst.out.nonempty
    rw [Ideal.ne_top_iff_one]
    intro h1
    simpa using h1 x hx
  mem_or_mem' {f g} hfg := sorry -- this is from isolated zeros

abbrev Mero := FractionRing (An U ⧸ Zer U)

#synth Field (Mero U)

May I PR this to Mathlib?

[Vincent Beffara]

Sure, just with better naming :wink: although it might be better to first show the equivalence with the definition that is already there (I don’t remember if you have that proof already)

[Daniel Weber]

Definition of what? Meromorphic functions?

[Vincent Beffara]

Yes, docs#MeromorphicOn

[Daniel Weber]

That's a fairly complex proof, and since I don't need it for my project (proving that $$\erf$$ isn't elementary) I think I'm going to leave it as a TODO