Analytic uniqueness from positive real parameters

This file records uniqueness principles for holomorphic functions whose values are known only on the positive real locus. They are useful for transporting certain identities proved using real probability measures to their complex analytic continuations.

theorem AnalyticOnNhd.eqOn_of_eventuallyEq_ofRealCarlson {U : Set ℂ} {F G : ℂ → ℂ} {x₀ : ℝ} (hF : AnalyticOnNhd ℂ F U) (hG : AnalyticOnNhd ℂ G U) (hU : IsPreconnected U) (hx₀ : ↑x₀ ∈ U) (hEq : ∀ᶠ (x : ℝ) in nhds x₀, F ↑x = G ↑x) : Set.EqOn F G U

Local one-variable uniqueness from agreement on a real germ. This is the form useful when the functions are only analytic on a connected continuation domain rather than entire.

theorem analyticOnNhd_eq_of_eqOn_posRealCarlson {F G : ℂ → ℂ} (hF : AnalyticOnNhd ℂ F Set.univ) (hG : AnalyticOnNhd ℂ G Set.univ) (hEq : ∀ (x : ℝ), 0 < x → F ↑x = G ↑x) : F = G

Two entire functions of one complex variable which agree at every positive real number agree everywhere.

theorem analyticOnNhd_eq_of_eqOn_posReal_piCarlson {ι : Type u_1} [Fintype ι] {F G : (ι → ℂ) → ℂ} (hF : AnalyticOnNhd ℂ F Set.univ) (hG : AnalyticOnNhd ℂ G Set.univ) (hEq : ∀ (b : ι → ℝ), (∀ (i : ι), 0 < b i) → (F fun (i : ι) => ↑(b i)) = G fun (i : ι) => ↑(b i)) : F = G

Two entire functions of finitely many complex variables which agree on all vectors of strictly positive real parameters agree everywhere. No complex-open agreement hypothesis is needed.