feat(analysis/complex/open_mapping): the open mapping thm for holomorphic functions

[vbeffara]

---

• [x] depends on: #16723

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#16723~~ By Dependent Issues (🤖). Happy coding!

[vbeffara]

I hadn't thought about generalizations (I should have known by now ;->) but definitely some are possible. For E \to \C, most would go through as soon as [proper_space E] with the same proof. For more general, I'm guessing that looking at lines through a point and applying the one-dimensional version would either find a line along which the function is not locally constant and then we get a ball in the image, or not in which case the function is locally zero along every line which implies (hopefully) that its series is zero. I'm not completely sure that it works, I will give it a try!

[vbeffara]

This is going to work for the generalization:

example {E : Type*} [normed_add_comm_group E] [normed_space ℂ E] {z₀ : E} {g : E → ℂ}
  (hg : analytic_at ℂ g z₀) : (∀ᶠ z in 𝓝 z₀, g z = g z₀) ∨ (𝓝 (g z₀) ≤ map g (𝓝 z₀)) :=
begin
  let ray : E → ℂ → ℂ := λ z t, g (z₀ + t • z),
  obtain ⟨r, hr, hgr⟩ : ∃ r > 0, analytic_on ℂ g (ball z₀ r), sorry,
  have h1 : ∀ z ∈ sphere (0 : E) 1, analytic_on ℂ (ray z) (ball 0 r), sorry,
  by_cases (∀ z ∈ sphere (0 : E) 1, ∀ᶠ t in 𝓝 0, ray z t = ray z 0),
  { left, -- If g is eventually constant along every direction, then it is eventually constant
    have h2 : ∀ z ∈ sphere (0 : E) 1, ∀ t ∈ ball (0 : ℂ) r, ray z t = g z₀, sorry,
    refine eventually_of_mem (ball_mem_nhds z₀ hr) (λ z hz, _),
    by_cases h' : z = z₀,
    { rw h' },
    { let w : E := ∥z - z₀∥⁻¹ • (z - z₀),
      have h3 : w ∈ sphere (0 : E) 1, sorry,
      have h4 : ∥z - z₀∥ < r, sorry,
      have h5 : ↑∥z - z₀∥ ∈ ball (0 : ℂ) r, sorry,
      have h6 : ∥z - z₀∥ ≠ 0, sorry,
      specialize h2 w h3 (∥z - z₀∥) h5,
      simp only [ray, w] at h2,
      norm_cast at h2,
      simpa only [smul_smul, mul_inv_cancel h6, one_smul, add_sub_cancel'_right] using h2 } },
  { right, -- Otherwise, it is open along at least one direction and that implies the result
    push_neg at h,
    obtain ⟨z, hz, hrz⟩ := h,
    specialize h1 z hz 0 (mem_ball_self hr),
    have h7 := h1.eventually_constant_or_nhds_le_map_nhds.resolve_left hrz,
    have h8 : ray z 0 = g z₀, sorry, rw [h8] at h7,
    refine h7.trans _,
    have h9 : ray z = g ∘ (λ t, z₀ + t • z) := rfl, rw [h9, ← map_compose],
    apply map_mono,
    have h10 : continuous (λ (t : ℂ), z₀ + t • z),
      from continuous_const.add (continuous_id'.smul continuous_const),
    simpa using h10.tendsto 0 }
end

Needs a lot of refining and de-sorrying though.

[vbeffara]

OK, so I extended both analytic_at.eventually_constant_or_nhds_le_map_nhds and analytic_on.is_constant_or_is_open to the E → ℂ case, and I believe I addressed all the other comments.

[sgouezel]

That's really cool! For each lemma whose proof is longer than 10 lines, could you please add a docstring explaning the content of the result, and a comment at the beginning of the proof sketching the proof briefly? (Well, this rule is maybe too mechanical, maybe a better rule is: add a docstring whenever the statement is either hard to parse or important, and add a proof comment whenever the proof is not completely trivial). bors d+

[bors[bot]]

:v: vbeffara can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[vbeffara]

Docstrings added. bors r+

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests