Analyticity of uniform limits on complex polydiscs, using the Cauchy integral formula and convergence of weighted integrals over compact sets.

theorem KamProject.Arnold1963.analyticAt_cauchyIntegral {n : ℕ} {f : ComplexSpace n → ℂ} {c w : ComplexSpace n} {r : RealSpace n} (hr : ∀ (i : Fin n), 0 ≤ r i) (hf : ContinuousOn f (Set.univ.pi fun (i : Fin n) => Metric.closedBall (c i) (r i))) (hw : ∀ (i : Fin n), w i ∈ Metric.ball (c i) (r i)) : AnalyticAt ℂ (fun (a : ComplexSpace n) => ∯ (z : Fin n → ℂ) in T(c, r), cauchyKernel a z * f z) w

theorem KamProject.Arnold1963.tendsto_weightedIntegral_of_uniform_compact {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {K : Set X} (hK : IsCompact K) (hKm : MeasurableSet K) {F : ℕ → X → ℂ} {f a : X → ℂ} (hF : ∀ (s : ℕ), ContinuousOn (F s) K) (ha : ContinuousOn a K) (hu : TendstoUniformlyOn F f Filter.atTop K) : Filter.Tendsto (fun (s : ℕ) => ∫ (x : X) in K, a x * F s x ∂μ) Filter.atTop (nhds (∫ (x : X) in K, a x * f x ∂μ))

theorem KamProject.Arnold1963.analyticAt_uniform_limit_polydisc {n : ℕ} {F : ℕ → ComplexSpace n → ℂ} {f : ComplexSpace n → ℂ} {c : ComplexSpace n} {R : ℝ} (hR : 0 < R) (hF : ∀ (s : ℕ), AnalyticOnNhd ℂ (F s) (Metric.closedBall c R)) (hu : TendstoUniformlyOn F f Filter.atTop (Metric.closedBall c R)) : AnalyticAt ℂ f c

theorem KamProject.Arnold1963.analyticOnNhd_uniform_limit {n : ℕ} {U : Set (ComplexSpace n)} (hU : IsOpen U) {F : ℕ → ComplexSpace n → ℂ} {f : ComplexSpace n → ℂ} (hF : ∀ (s : ℕ), AnalyticOnNhd ℂ (F s) U) (hu : TendstoUniformlyOn F f Filter.atTop U) : AnalyticOnNhd ℂ f U