analytic continuation?

Stream: Is there code for X?

[Alex Kontorovich]

Do we have analytic continuation? Something like:

import Mathlib

theorem AnalyticContinuation {f g : ℂ → ℂ} {s t : Set ℂ} (f_on_s : AnalyticOn ℂ f s)
    (g_on_t : AnalyticOn ℂ g t) (f_eq_g_on_cap : Set.EqOn f g (s ∩ t))
    (s_open : IsOpen s) (t_open : IsOpen t) (cap_nonempty : Set.Nonempty (s ∩ t)) :
    ∃! h : ℂ → ℂ, AnalyticOn ℂ h (s ∪ t) ∧ Set.EqOn h f s ∧ Set.EqOn h g t := by
  sorry

[Alex Kontorovich]

Or even this:

import Mathlib

theorem AnalyticContinuation' {f g : ℂ → ℂ} {s t u : Set ℂ} (f_on_s : AnalyticOn ℂ f s)
    (g_on_t : AnalyticOn ℂ g t) (u_sub : u ⊆ s ∩ t) (u_open : IsOpen u)
    (u_nonempty : Set.Nonempty u) (f_eq_g_on_u : Set.EqOn f g u) :
    Set.EqOn f g (s ∩ t) := by
  sorry

[Matt Diamond]

this is a completely naive guess, but is docs#AnalyticOn.eqOn_of_preconnected_of_eventuallyEq related at all?

[Alex Kontorovich]

I think that should work, thanks!!