Eulerian form of #2513: perturbed generalized Eulerian rows interlace

RealRooted/Challenges/Combinatorial/OrbitPerturbation.lean

@@ -48,9 +48,19 @@ label = "A three-term θ-recurrence family has interlacing rows"
 headline = true
 
 [[theorems]]
-name = "RealRooted.splits_C_mul_add_C_mul_one_add_X_pow_of_recurrence"
+name = "RealRooted.strictInterl_C_mul_add_C_mul_one_add_X_pow_of_recurrence"
 module = "RealRooted.EulerOperator.OrbitPerturbationCayley"
-label = "Eulerian form: perturbed Eulerian-type rows are real-rooted"
+label = "Eulerian form: perturbed Eulerian-type rows interlace strictly"
+
+[[theorems]]
+name = "RealRooted.strictInterl_C_mul_generalizedEulerian_add"
+module = "RealRooted.EulerOperator.OrbitPerturbationCayley"
+label = "Perturbed generalized Eulerian polynomials interlace strictly"
+
+[[theorems]]
+name = "RealRooted.strictInterl_cayleyTransform_succ_of_roots_mem_Icc"
+module = "RealRooted.PolynomialValueEulerNumerator.Interlacing"
+label = "The Cayley transform preserves degree-raising interlacing on [-1, 0]"
 -->
 
 <!-- realrooted-catalog-content -->
@@ -89,9 +99,12 @@ and is of independent research interest.
 **Eulerian form.**  The Cayley transform
 $T_nf=(1-x)^nf\bigl(x/(1-x)\bigr)$ maps $Q_n$ to $c\,E_n+(1-c)(1+x)^n$,
 where $c=r$, $E_0=1$ and
-$E_{n+1}=\bigl(1+(1+sn)x\bigr)E_n+s\,x(1-x)E_n'$.  For $s=1$ the $E_n$ are
-the Eulerian polynomials.  So for $s\ge1$ and $c\ge1/2$ every row
-$c\,E_n+(1-c)(1+x)^n$ is real-rooted.
+$E_{n+1}=\bigl(1+(1+sn)x\bigr)E_n+s\,x(1-x)E_n'$.  These are the
+generalized Eulerian polynomials; for $s=1$ the $E_n$ are the Eulerian
+polynomials.  So for $s\ge1$ and $c\ge1/2$ the rows
+$A_n=c\,E_n+(1-c)(1+x)^n$ are real-rooted and $A_n$ strictly interlaces
+$A_{n+1}$, because the Cayley transform preserves interlacing of polynomials
+with roots in $[-1,0]$.
 
 **Applications.**  The parameters $s=1$ with $c=1/2$, $2$, $3$, $7$ and
 $s=2$ with $c=1/2$ give the OEIS triangles A141689, A141690, A141696, A141697

RealRooted/EulerOperator/OrbitPerturbationCayley.lean

@@ -2,7 +2,9 @@ module
 
 public import RealRooted.EulerOperator.OrbitPerturbationFamily
 public import RealRooted.Mathlib.Algebra.Polynomial.CayleyTransform.Basic
+public import RealRooted.GeneralizedEulerian
 import RealRooted.Mathlib.Algebra.Polynomial.CayleyTransform.Algebra
+import RealRooted.PolynomialValueEulerNumerator.Interlacing
 import Mathlib.Tactic.ComputeDegree
 import Mathlib.Tactic.Ring
 
@@ -81,30 +83,62 @@ theorem cayleyTransform_orbitPerturbationRow (α c : ℝ) (n : ℕ) :
   rw [orbitPerturbationRow_eq, cayleyTransform_add, cayleyTransform_C_mul, cayleyTransform_C_mul,
     hY, cayleyEulerOrbit]
 
+/-- A sequence with the seed and recurrence of the transformed orbit is the transformed orbit. -/
+private theorem eq_cayleyEulerOrbit_of_recurrence {s : ℝ} (hs : 0 < s) {E : ℕ → ℝ[X]}
+    (h0 : E 0 = 1)
+    (hrec : ∀ n : ℕ, E (n + 1) =
+      (1 + C (1 + s * n) * X) * E n + C s * X * (1 - X) * (E n).derivative) (n : ℕ) :
+    E n = cayleyEulerOrbit (s / 2) n := by
+  induction n with
+  | zero => rw [h0, cayleyEulerOrbit_zero]
+  | succ m ih =>
+      rw [hrec m, cayleyEulerOrbit_succ (by linarith), ih, show 2 * (s / 2) = s by ring]
+
 /-- **Eulerian form of RealRooted #2513, Theorem 1.**  Let `s ≥ 1` and `c ≥ 1 / 2`, and let
-`E 0 = 1` and `E (n + 1) = (1 + (1 + s n) X) E n + s X (1 - X) E n'`.  Then
-`c E n + (1 - c) (1 + X) ^ n` is real-rooted for every `n`. -/
+`E 0 = 1` and `E (n + 1) = (1 + (1 + s n) X) E n + s X (1 - X) E n'`.  Then the rows
+`A n = c E n + (1 - c) (1 + X) ^ n` are real-rooted, with roots `≤ 0`, and `A n` strictly
+interlaces `A (n + 1)`. -/
+theorem strictInterl_C_mul_add_C_mul_one_add_X_pow_of_recurrence {s c : ℝ} (hs : 1 ≤ s)
+    (hc : 1 / 2 ≤ c) {E : ℕ → ℝ[X]} (h0 : E 0 = 1)
+    (hrec : ∀ n : ℕ, E (n + 1) =
+      (1 + C (1 + s * n) * X) * E n + C s * X * (1 - X) * (E n).derivative) (n : ℕ) :
+    StrictInterl (C c * E n + C (1 - c) * (1 + X) ^ n)
+      (C c * E (n + 1) + C (1 - c) * (1 + X) ^ (n + 1)) := by
+  have hE := eq_cayleyEulerOrbit_of_recurrence (by linarith) h0 hrec
+  rw [hE n, hE (n + 1), ← cayleyTransform_orbitPerturbationRow,
+    ← cayleyTransform_orbitPerturbationRow]
+  obtain ⟨hdeg, hroot, -, hint⟩ := orbitPerturbationRow_package (α := s / 2) (by linarith) hc n
+  obtain ⟨hdeg1, hroot1, -⟩ := orbitPerturbationRow_package (α := s / 2) (by linarith) hc (n + 1)
+  exact strictInterl_cayleyTransform_succ_of_roots_mem_Icc hdeg hdeg1 hint
+    (fun r hr ↦ ⟨(hroot.2.2 r hr).1.le, (hroot.2.2 r hr).2.le⟩)
+    (fun r hr ↦ ⟨(hroot1.2.2 r hr).1.le, (hroot1.2.2 r hr).2.le⟩)
+
+/-- Real-rootedness in the Eulerian form of RealRooted #2513, Theorem 1: for `s ≥ 1` and
+`c ≥ 1 / 2`, every row `c E n + (1 - c) (1 + X) ^ n` splits. -/
 theorem splits_C_mul_add_C_mul_one_add_X_pow_of_recurrence {s c : ℝ} (hs : 1 ≤ s)
     (hc : 1 / 2 ≤ c) {E : ℕ → ℝ[X]} (h0 : E 0 = 1)
     (hrec : ∀ n : ℕ, E (n + 1) =
       (1 + C (1 + s * n) * X) * E n + C s * X * (1 - X) * (E n).derivative) (n : ℕ) :
-    (C c * E n + C (1 - c) * (1 + X) ^ n).Splits := by
-  have hα : 0 < s / 2 := by linarith
-  have hE : ∀ m, E m = cayleyEulerOrbit (s / 2) m := by
-    intro m
-    induction m with
-    | zero => rw [h0, cayleyEulerOrbit_zero]
-    | succ m ih =>
-        rw [hrec m, cayleyEulerOrbit_succ hα, ih,
-          show 2 * (s / 2) = s by ring]
-  rw [hE n, ← cayleyTransform_orbitPerturbationRow]
-  have hroot := (orbitPerturbationRow_package (α := s / 2) (by linarith) hc n).1
-  refine hroot.splits.cayleyTransform ?_
-  rw [orbitPerturbationRow_eq]
-  refine natDegree_add_le_of_degree_le ((natDegree_C_mul_le _ _).trans
-    (natDegree_centeredEulerOrbit_comp_le hα n)) ((natDegree_C_mul_le _ _).trans ?_)
-  refine natDegree_pow_le.trans ?_
-  have h1 : (C 2 * X + C 1 : ℝ[X]).natDegree ≤ 1 := by compute_degree
-  nlinarith
+    (C c * E n + C (1 - c) * (1 + X) ^ n).Splits :=
+  (strictInterl_C_mul_add_C_mul_one_add_X_pow_of_recurrence hs hc h0 hrec n).1.2
+
+
+/-- The transformed orbit is the generalized Eulerian polynomial with parameter `2 α`. -/
+theorem cayleyEulerOrbit_eq_generalizedEulerian {α : ℝ} (hα : 0 < α) (n : ℕ) :
+    cayleyEulerOrbit α n = generalizedEulerian (2 * α) n := by
+  induction n with
+  | zero => rw [cayleyEulerOrbit_zero]; rfl
+  | succ n ih =>
+      rw [cayleyEulerOrbit_succ hα, ih, generalizedEulerian_succ, add_comm (1 : ℝ),
+        mul_assoc]
+
+/-- Perturbed generalized Eulerian polynomials: for `s ≥ 1` and `c ≥ 1 / 2`, the rows
+`c A_n^{(s)} + (1 - c) (1 + X) ^ n` interlace strictly (RealRooted #2513, Theorem 1). -/
+theorem strictInterl_C_mul_generalizedEulerian_add {s c : ℝ} (hs : 1 ≤ s) (hc : 1 / 2 ≤ c)
+    (n : ℕ) :
+    StrictInterl (C c * generalizedEulerian s n + C (1 - c) * (1 + X) ^ n)
+      (C c * generalizedEulerian s (n + 1) + C (1 - c) * (1 + X) ^ (n + 1)) :=
+  strictInterl_C_mul_add_C_mul_one_add_X_pow_of_recurrence hs hc rfl
+    (fun n ↦ by rw [generalizedEulerian_succ, add_comm (s * n)]) n
 
 end RealRooted

RealRooted/EulerOperator/OrbitPerturbationFamily.lean

@@ -4,6 +4,7 @@ public import RealRooted.EulerOperator.OrbitPerturbation
 import RealRooted.EulerOperator.OrbitPerturbationInterlacing
 import RealRooted.Linear
 import RealRooted.MaWang.Weak.DerivativeSign
+import Mathlib.Tactic.ComputeDegree
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.LinearCombination
 import Mathlib.Tactic.Positivity
@@ -95,11 +96,12 @@ theorem orbitPerturbationRow_one (α r : ℝ) : orbitPerturbationRow α r 1 = C
   simp [orbitPerturbationRow, centeredEulerStep]
   ring
 
-/-- For `α ≥ 1 / 2` and `r ≥ 1 / 2`, the perturbed rows have simple roots in `(-1, 0)` and
-consecutive rows interlace strictly. -/
+/-- For `α ≥ 1 / 2` and `r ≥ 1 / 2`, the perturbed rows have degree `n` and simple roots in
+`(-1, 0)`, and consecutive rows interlace strictly. -/
 theorem orbitPerturbationRow_package {α r : ℝ} (hαhalf : 1 / 2 ≤ α) (hrhalf : 1 / 2 ≤ r)
     (n : ℕ) :
-    IsRealRootedIn (Ioo (-1 : ℝ) 0) (orbitPerturbationRow α r n) ∧
+    (orbitPerturbationRow α r n).natDegree = n ∧
+      IsRealRootedIn (Ioo (-1 : ℝ) 0) (orbitPerturbationRow α r n) ∧
       HasSimpleRoots (orbitPerturbationRow α r n) ∧
       StrictInterl (orbitPerturbationRow α r n) (orbitPerturbationRow α r (n + 1)) := by
   have hrpos : 0 < r := by linarith
@@ -117,7 +119,8 @@ theorem orbitPerturbationRow_package {α r : ℝ} (hαhalf : 1 / 2 ≤ α) (hrha
     norm_num
   rcases Nat.eq_zero_or_pos n with rfl | hn
   · rw [orbitPerturbationRow_zero α r]
-    refine ⟨IsRealRootedIn.one, hasSimpleRoots_of_natDegree_le_one one_ne_zero (by simp), ?_⟩
+    refine ⟨natDegree_one, IsRealRootedIn.one,
+      hasSimpleRoots_of_natDegree_le_one one_ne_zero (by simp), ?_⟩
     rw [zero_add, orbitPerturbationRow_one α r]
     exact StrictInterl.of_natDegree_eq_zero_left one_ne_zero (by simp)
       (by
@@ -131,9 +134,12 @@ theorem orbitPerturbationRow_package {α r : ℝ} (hαhalf : 1 / 2 ≤ α) (hrha
   have hb1 : (1 - r) / r ≤ 1 := by
     rw [div_le_iff₀ hrpos]
     linarith
-  obtain ⟨-, -, hroot, hsimple, hint⟩ := centeredEulerOrbit_add_monomial hαhalf hb hb1 hn
+  obtain ⟨hdeg, -, hroot, hsimple, hint⟩ := centeredEulerOrbit_add_monomial hαhalf hb hb1 hn
   rw [orbitPerturbationRow_eq_C_mul hrpos.ne', orbitPerturbationRow_eq_C_mul hrpos.ne']
-  refine ⟨?_, ?_, ?_⟩
+  refine ⟨?_, ?_, ?_, ?_⟩
+  · rw [natDegree_C_mul hrpos.ne', natDegree_comp, hdeg]
+    have : (C 2 * X + C 1 : ℝ[X]).natDegree = 1 := by compute_degree!
+    rw [this, mul_one]
   · refine IsRealRootedIn.C_mul hrpos.ne' ?_
     rw [← hloc]
     exact hroot.comp_C_mul_X_add_C 1 two_ne_zero
@@ -188,6 +194,6 @@ theorem strictInterl_of_orbitPerturbation_recurrence {s κ : ℝ} (hs : 1 ≤ s)
         change ((m : ℝ[X]) + 1) * Q (m + 3) = ((m : ℝ[X]) + 1) * orbitPerturbationRow α r (m + 3)
         rw [hrec m, orbitPerturbationRow_recurrence, ih.2.1, ih.2.2, hs2]
   rw [(hQ n).1, (hQ (n + 1)).1]
-  exact orbitPerturbationRow_package hαhalf hrhalf n
+  exact (orbitPerturbationRow_package hαhalf hrhalf n).2
 
 end RealRooted

RealRooted/PolynomialValueEulerNumerator/Interlacing.lean

@@ -385,6 +385,62 @@ theorem strictInterl_cayleyTransform_of_roots_mem_Icc
       (hss_len.trans hrs_len.symm) halt
       (fun r hr => (hss_box r hr).1) (fun r hr => (hrs_box r hr).1)
 
+/-- Degree-raising form of `strictInterl_cayleyTransform_of_roots_mem_Icc`: if `p ≪ q` with
+`deg p = n`, `deg q = n + 1` and all roots in `[-1, 0]`, then the Cayley transforms of degrees
+`n` and `n + 1` interlace.  We adjoin the root `-1` to `p`, which does not change its degree-`(n+1)`
+transform. -/
+theorem strictInterl_cayleyTransform_succ_of_roots_mem_Icc
+    {p q : ℝ[X]} {n : ℕ}
+    (hpdeg : p.natDegree = n) (hqdeg : q.natDegree = n + 1)
+    (h : StrictInterl p q)
+    (hp_roots : ∀ r ∈ p.roots, (-1 : ℝ) ≤ r ∧ r ≤ 0)
+    (hq_roots : ∀ r ∈ q.roots, (-1 : ℝ) ≤ r ∧ r ≤ 0) :
+    StrictInterl (Polynomial.cayleyTransform n p)
+      (Polynomial.cayleyTransform (n + 1) q) := by
+  have hX : (X + 1 : ℝ[X]) = X - C (-1) := by simp
+  rcases h with ⟨hp_rr, hq_rr, ss, rs, hss, hrs, hss_eq, hrs_eq, hshape⟩
+  have hp0 : p ≠ 0 := hp_rr.1
+  have hprod_ne : (X + 1) * p ≠ 0 := by
+    rw [hX]
+    exact mul_ne_zero (X_sub_C_ne_zero _) hp0
+  have hroots : ((X + 1) * p).roots = (-1 : ℝ) ::ₘ p.roots := by
+    rw [hX, roots_mul (hX ▸ hprod_ne), roots_X_sub_C, Multiset.singleton_add]
+  have hdeg' : ((X + 1) * p).natDegree = n + 1 := by
+    rw [hX, natDegree_mul (X_sub_C_ne_zero _) hp0, natDegree_X_sub_C, hpdeg, add_comm]
+  have hsplit : ((X + 1) * p).Splits := by
+    rw [hX]
+    exact (Splits.X_sub_C _).mul hp_rr.2
+  have hss_len : ss.length = n := by
+    rw [← Multiset.coe_card, hss_eq, Polynomial.splits_iff_card_roots.mp hp_rr.2, hpdeg]
+  have hrs_len : rs.length = n + 1 := by
+    rw [← Multiset.coe_card, hrs_eq, Polynomial.splits_iff_card_roots.mp hq_rr.2, hqdeg]
+  have hint : ListInterlaces ss rs := by
+    rcases hshape with hdiff | hsame
+    · exact hdiff.2
+    · lia
+  have hss_box : ∀ r ∈ ss, (-1 : ℝ) ≤ r ∧ r ≤ 0 := fun r hr ↦
+    hp_roots r (by simpa [hss_eq] using Multiset.mem_coe.mpr hr)
+  have hrs_box : ∀ r ∈ rs, (-1 : ℝ) ≤ r ∧ r ≤ 0 := fun r hr ↦
+    hq_roots r (by simpa [hrs_eq] using Multiset.mem_coe.mpr hr)
+  have hpq : StrictInterl ((X + 1) * p) q := by
+    obtain ⟨r, rs', rfl⟩ : ∃ r rs', rs = r :: rs' :=
+      List.exists_cons_of_length_pos (by lia)
+    refine ⟨⟨hprod_ne, hsplit⟩, hq_rr, -1 :: ss, r :: rs', ?_, hrs, ?_, hrs_eq,
+      Or.inr ⟨by simp [hss_len, hrs_len], (hrs_box r (by simp)).1, hint⟩⟩
+    · exact List.pairwise_cons.mpr ⟨fun s hs ↦ (hss_box s hs).1, hss⟩
+    · rw [hroots, ← hss_eq, Multiset.cons_coe]
+  have hmain := strictInterl_cayleyTransform_of_roots_mem_Icc hdeg' hqdeg hpq (by
+    intro r hr
+    rw [hroots, Multiset.mem_cons] at hr
+    rcases hr with rfl | hr
+    · norm_num
+    · exact hp_roots r hr) hq_roots
+  rwa [show Polynomial.cayleyTransform (n + 1) ((X + 1) * p) =
+      Polynomial.cayleyTransform n p by
+    rw [add_mul, one_mul, cayleyTransform_add, cayleyTransform_succ_X_mul hpdeg.le,
+      cayleyTransform_succ hpdeg.le]
+    ring] at hmain
+
 /-- A monic split interval-rooted input has its `E`-image rooted in the same
 closed interval. -/
 lemma brandenE_roots_mem_Icc_of_monic {p : ℝ[X]}