feat(polynomial): close bounded real-root limits

Author: PerAlexandersson

RealRooted.lean

@@ -587,6 +587,7 @@ import RealRooted.Mathlib.Algebra.Polynomial.Splits.Complex
 import RealRooted.Mathlib.Algebra.Polynomial.Splits.Derivative
 import RealRooted.Mathlib.Analysis.Complex.OpenMapping
 import RealRooted.Mathlib.Analysis.Complex.Polynomial.ClosedRoots
+import RealRooted.Mathlib.Analysis.Complex.Polynomial.ClosedRoots.Real
 import RealRooted.Mathlib.Analysis.Normed.Field.Approximation
 import RealRooted.Mathlib.Analysis.Polynomial.Asymptotics
 import RealRooted.Mathlib.Analysis.Polynomial.MahlerMeasure

RealRooted/Mathlib/Analysis/Complex/Polynomial/ClosedRoots.lean

@@ -1,6 +1,10 @@
-import Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
-import Mathlib.Algebra.Polynomial.Splits
-import Mathlib.Analysis.Complex.Polynomial.Basic
+module
+
+public import Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
+public import Mathlib.Algebra.Polynomial.Splits
+public import Mathlib.Analysis.Complex.Polynomial.Basic
+
+public section
 
 /-!
 # Closed conditions on roots of polynomial limits

RealRooted/Mathlib/Analysis/Complex/Polynomial/ClosedRoots/Real.lean

@@ -0,0 +1,46 @@
+module
+
+public import RealRooted.Mathlib.Algebra.Polynomial.Splits.Complex
+public import RealRooted.Mathlib.Analysis.Complex.Polynomial.ClosedRoots
+
+public section
+
+noncomputable section
+
+open Filter Topology
+
+namespace Polynomial
+
+/-- Pointwise limits of real splitting polynomials with uniformly bounded
+degree are zero or split. -/
+theorem eq_zero_or_splits_of_tendsto_eval_of_natDegree_le
+    {p : ℕ → ℝ[X]} {p₀ : ℝ[X]} {N : ℕ}
+    (hdeg : ∀ n, (p n).natDegree ≤ N)
+    (hsplit : ∀ n, p n = 0 ∨ (p n).Splits)
+    (heval : ∀ z : ℂ, Tendsto
+      (fun n => ((p n).map Complex.ofRealHom).eval z) atTop
+        (𝓝 ((p₀.map Complex.ofRealHom).eval z))) :
+    p₀ = 0 ∨ p₀.Splits := by
+  by_cases hp₀ : p₀ = 0
+  · exact Or.inl hp₀
+  right
+  apply splits_of_all_roots_real
+  intro z hz
+  have hzroots : z ∈ (p₀.map Complex.ofRealHom).roots :=
+    (mem_roots (Polynomial.map_ne_zero hp₀)).mpr hz
+  have hreal : z ∈ {z : ℂ | z.im = 0} :=
+    roots_mem_of_tendsto_eval_of_natDegree_le
+      (isClosed_eq Complex.continuous_im continuous_const)
+      (fun n => by
+        simpa only [natDegree_map_eq_of_injective Complex.ofRealHom.injective] using hdeg n)
+      (fun n r hr => by
+        rcases hsplit n with hpzero | hpsplits
+        · rw [hpzero] at hr
+          simp at hr
+        · rw [hpsplits.roots_map Complex.ofRealHom, Multiset.mem_map] at hr
+          obtain ⟨s, -, rfl⟩ := hr
+          simp)
+      heval z hzroots
+  exact hreal
+
+end Polynomial

RealRooted/Production.lean

@@ -587,6 +587,7 @@ import RealRooted.Mathlib.Algebra.Polynomial.Splits.Complex
 import RealRooted.Mathlib.Algebra.Polynomial.Splits.Derivative
 import RealRooted.Mathlib.Analysis.Complex.OpenMapping
 import RealRooted.Mathlib.Analysis.Complex.Polynomial.ClosedRoots
+import RealRooted.Mathlib.Analysis.Complex.Polynomial.ClosedRoots.Real
 import RealRooted.Mathlib.Analysis.Normed.Field.Approximation
 import RealRooted.Mathlib.Analysis.Polynomial.Asymptotics
 import RealRooted.Mathlib.RingTheory.PowerSeries.CatalanQuadratic

scripts/import_architecture.json

@@ -10,10 +10,10 @@
   },
   "budgets": {
     "RealRooted": {
-      "max_modules": 1177
+      "max_modules": 1178
     },
     "RealRooted.Production": {
-      "max_modules": 1056
+      "max_modules": 1057
     },
     "RealRooted.Tactic.Examples": {
       "max_modules": 633
@@ -402,6 +402,9 @@
     "RealRooted.Mathlib.Algebra.Polynomial.Splits.Complex": {
       "max_modules": 1
     },
+    "RealRooted.Mathlib.Analysis.Complex.Polynomial.ClosedRoots.Real": {
+      "max_modules": 3
+    },
     "RealRooted.HermiteBiehler.Basic": {
       "max_modules": 13
     },