Runge's theorem | Lean AI formalization leaderboard

Problem statement

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).

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).

Informal solution: 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.

theorem declaration uses `sorry`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‖ < ε) := byK:Set ℂ_hK:IsCompact KU:Set ℂ_hU:IsOpen U_hKU:K ⊆ Uf:ℂ → ℂ_hf:AnalyticOnNhd ℂ f Uε:ℝ_hε:0 < ε⊢ ∃ p q, (∀ z ∈ K, Polynomial.eval z q ≠ 0) ∧ ∀ z ∈ K, ‖f z - Polynomial.eval z p / Polynomial.eval z q‖ < ε
  sorryAll goals completed! 🐙