Runge's theorem

runge_theorem — a formalization challenge from the lean-eval benchmark.

Notes

Basic Runge approximation theorem for compact subsets of ℂ. The statement uses polynomials p q : ℂ[X] and requires q to be nonvanishing on K, expressing rational functions with no poles on K. This does not include the standard pole-control refinement (one pole per connected component of ℂ \ K).

Formal statement

/-- **Runge's theorem.** If `K ⊆ ℂ` is compact and `f` is analytic on
an open neighbourhood of `K`, then for every `ε > 0`, `f` is uniformly
approximated on `K` by a rational function `p / q` with `q` non-vanishing
on `K`. -/
theorem runge (K : Set ℂ) (_hK : IsCompact K) (U : Set ℂ) (_hU : IsOpen U)
    (_hKU : K ⊆ U) (f : ℂ → ℂ) (_hf : AnalyticOnNhd ℂ f U)
    (ε : ℝ) (_hε : 0 < ε) :
    ∃ p q : ℂ[X], (∀ z ∈ K, q.eval z ≠ 0) ∧
      (∀ z ∈ K, ‖f z - p.eval z / q.eval z‖ < ε) := by
  sorry

Informal solution sketch

Show that rational functions with poles outside K are dense in the algebra of functions holomorphic on a neighbourhood of K, with respect to the uniform norm on K. Classical proofs go via Cauchy integral approximation or via Hahn–Banach / Riesz duality.

Source

C. Runge, Zur Theorie der eindeutigen analytischen Funktionen, Acta Math. 6 (1885), 229-244. Listed as §64 (additional statement 3) in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: runge
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.