Osgood's theorem in finite products

Joint continuity and separate holomorphy imply joint analyticity on an open subset of a finite complex coordinate space. The stronger Hartogs theorem without continuity is not proved here. The polydisc Cauchy formula and its series construction live in the imported modules and remain available through this file.

theorem CarlsonFunctions.SeveralComplexVariables.analyticOnNhd_pi_of_analyticOnNhd_update {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {ι : Type u_2} [Fintype ι] {U : Set (ι → ℂ)} {f : (ι → ℂ) → E} (hU : IsOpen U) (hfc : ContinuousOn f U) (hf : ∀ z ∈ U, ∀ (i : ι), AnalyticAt ℂ (fun (w : ℂ) => f (Function.update z i w)) (z i)) : AnalyticOnNhd ℂ f U

Osgood's theorem, finite-product form. A jointly continuous function on an open subset of a finite product of copies of ℂ is jointly analytic when all of its one-coordinate restrictions are analytic.

This is weaker than Hartogs' theorem, which drops the continuity hypothesis. Continuity is present in every current application in this library.