Ring of holomorphic functions is an integral domain

Stream: Is there code for X?

[Seewoo Lee]

Let $\mathcal{O}(\mathbb{C})$ be the ring of holomorphic functions on $\mathbb{C}$. Then it is an integral domain - do we have this in mathlib?

I think a standard proof is to invoke the identity theorem of complex analysis, but I cannot find this in mathlib. Here's more precise version that I may want:

• The functions might only defined on $\mathfrak{H}$, the complex upper half plane (in fact, I'm interested in modular forms)
• I want to prove that $f g = 0$ implies $g = 0$, where we know that $f$ is not identically zero. Unfortunately, $f$ has zeros at (infinitely many) points, and we know the points exactly, although formalizing that won't be simple. (In fact, both $f, g$ are modular forms and $f = E_{4}$ is the weight 4 Eisenstein series, which has zeros at the $\mathrm{SL}_{2}(\mathbb{Z})$-orbits of $e^{2\pi i / 3}$. We know that $$E_{4}$ does not vanish on the imaginary axis, but we still need a version of identity theorem to prove $g = 0$ identically)

[Johan Commelin]

I think this lemma, and/or the ones below it will be useful for this: https://github.com/leanprover-community/mathlib4/blob/e3ce54eedb2ab716b7f62aecc31b0308cb7719b8/Mathlib/Analysis/Analytic/IsolatedZeros.lean#L249-L257

[David Loeffler]

Here's something which works:

import Mathlib

open Filter Topology in
lemma AnalyticOnNhd.eq_zero_or_eq_zero {U : Set ℂ} {f g : ℂ → ℂ}
    (hf : AnalyticOnNhd ℂ f U) (hg : AnalyticOnNhd ℂ g U)
    (hfg : ∀ z ∈ U, f z * g z = 0) (hU : IsPreconnected U) :
    (∀ z ∈ U, f z = 0) ∨ (∀ z ∈ U, g z = 0) := by
  -- We want to apply `IsPreconnected.preperfect_of_nontrivial` which requires `U` to have at least
  -- two elements. So we need to dispose of two silly special cases first.
  by_cases hU' : U = ∅
  · simp [hU']
  obtain ⟨z, hz⟩ : ∃ z, z ∈ U := Set.nonempty_iff_ne_empty.mpr hU'
  by_cases hU'' : U = {z}
  · simpa [hU''] using hfg z hz
  rw [← Ne, ← Set.nontrivial_iff_ne_singleton hz] at hU''
  -- Now connectedness implies that `z` is an accumulation point of `U`, so at least one of
  -- `f` and `g` must vanish frequently in a neighbourhood of `z`.
  have : ∃ᶠ w in 𝓝[≠] z, w ∈ U :=
    frequently_mem_iff_neBot.mpr <| hU.preperfect_of_nontrivial hU'' z hz
  have : ∃ᶠ w in 𝓝[≠] z, f w = 0 ∨ g w = 0 :=
    this.mp <| by filter_upwards with w hw using mul_eq_zero.mp (hfg w hw)
  cases frequently_or_distrib.mp this with
  | inl h => exact Or.inl <| hf.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hz h
  | inr h => exact Or.inr <| hg.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hz h

[Seewoo Lee]

Thank you!!

[David Loeffler]

Incidentally, I'm intrigued by what you say about your intended application of this to modular forms. How exactly are you getting the non-vanishing of E4 away from the orbit of $\exp(2 \pi i / 3)$? The "conventional" proof of this – the one you see in Serre's book for example – relies on counting poles and zeros via a contour integral, and that argument is a pain to formalise. My impression is that this has been the primary blockage to developing modular forms in Mathlib for a very long time now.

[Seewoo Lee]

My original question is more like "do we even have identity theorem?" and the answer seems yes, thanks to both of you. But for the actual purpose, I think proving that those are the only zeros of $E_4$ is not easy as you mentioned (almost as hard as proving valence formula). Fortunately, I found an alternative approach (non-formal proof) for something I wanted to prove that avoids all the hard parts with cost of another efforts, which should be easier than the things you mentioned (nothing about zeros of $E_4$). It would be interesting if there are other proofs on zeros of $E_4$ that avoids the contour integral though..

[Seewoo Lee]

Also cc @Chris Birkbeck

[Chris Birkbeck]

Maybe we should put a bounty out for formalising contour integrals.

[Chris Birkbeck]

But yes, I don't know of another proof of this for E4. If we can avoid it for the time being that would be great.

[David Loeffler]

David Loeffler said:

Here's something which works: [...]

Now PR'ed as #20996.