Documentation

TauCeti.Analysis.Complex.PowerSeries.Approximation

Approximating holomorphic functions on a disc by entire functions #

A holomorphic function on an open disc ball c s in ℂ, with values in a complex Banach space, is the uniform limit on every smaller closed disc closedBall c r, r < s, of the partial sums of its Taylor series at c. These partial sums are polynomial in z - c, hence entire. So the function is uniformly approximated on closedBall c r by entire functions.

This is the disc case of Runge's approximation theorem. It is the correction step in the solution of the inhomogeneous Cauchy–Riemann equation on a disc by exhaustion, where local solutions on an increasing sequence of discs are made to converge by subtracting entire approximations of their holomorphic differences.

References #

theorem DifferentiableOn.exists_differentiable_norm_sub_lt {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℂ W] [CompleteSpace W] {h : ℂ → W} {c : ℂ} {r s ε : ℝ} (hh : DifferentiableOn ℂ h (Metric.ball c s)) (hrs : r < s) (hε : 0 < ε) :
∃ (P : ℂ → W), Differentiable ℂ P ∧ ∀ z ∈ Metric.closedBall c r, ‖h z - P z‖ < ε

A holomorphic function on an open disc ball c s is approximated uniformly on every smaller closed disc closedBall c r, r < s, by entire functions.