Add generalized-Laguerre sequence interlacing

RealRooted.lean

@@ -179,6 +179,7 @@ import RealRooted.DerivativeRecurrence
 import RealRooted.DerivativeRecurrence.Linear
 import RealRooted.DerivativeRecurrence.QuadraticDegree
 import RealRooted.DerivativeRecurrence.GeneralizedLaguerre
+import RealRooted.DerivativeRecurrence.GeneralizedLaguerreInterlacing
 import RealRooted.DerivativeRecurrence.QuadraticInterlacing
 import RealRooted.DerivativeRecurrence.QuadraticSeed
 import RealRooted.DerivativeRecurrence.QuadraticShift
@@ -684,6 +685,7 @@ import RealRooted.Tactic.Examples.Finish
 import RealRooted.Tactic.Examples.FiniteSymbol
 import RealRooted.Tactic.Examples.FiniteSymbolPF
 import RealRooted.Tactic.Examples.GammaRealRoots
+import RealRooted.Tactic.Examples.GeneralizedLaguerre
 import RealRooted.Tactic.Examples.Hadamard
 import RealRooted.Tactic.Examples.HermiteBiehler
 import RealRooted.Tactic.Examples.HermitePoulain
@@ -742,6 +744,7 @@ import RealRooted.Tactic.Finish
 import RealRooted.Tactic.FiniteSymbol
 import RealRooted.Tactic.FiniteSymbolPF
 import RealRooted.Tactic.GammaRealRoots
+import RealRooted.Tactic.GeneralizedLaguerre
 import RealRooted.Tactic.Hadamard
 import RealRooted.Tactic.HermiteBiehler
 import RealRooted.Tactic.HermitePoulain

RealRooted/DerivativeRecurrence.lean

@@ -1,6 +1,7 @@
 import RealRooted.DerivativeRecurrence.Linear
 import RealRooted.DerivativeRecurrence.QuadraticDegree
 import RealRooted.DerivativeRecurrence.GeneralizedLaguerre
+import RealRooted.DerivativeRecurrence.GeneralizedLaguerreInterlacing
 import RealRooted.DerivativeRecurrence.QuadraticInterlacing
 import RealRooted.DerivativeRecurrence.QuadraticSeed
 import RealRooted.DerivativeRecurrence.QuadraticShift

RealRooted/DerivativeRecurrence/GeneralizedLaguerreInterlacing.lean

@@ -0,0 +1,86 @@
+import RealRooted.DerivativeRecurrence.GeneralizedLaguerre
+import RealRooted.DerivativeRecurrence.QuadraticInterlacing
+
+/-!
+# Interlacing for generalized-Laguerre differential recurrences
+
+This module applies the algebraic generalized-Laguerre reduction to the
+bilinear derivative-recurrence interlacing API.
+-/
+
+open Polynomial
+
+noncomputable section
+
+namespace RealRooted
+
+/-- The generalized-Laguerre reduction in the bilinear recurrence form used by
+the degree and interlacing API. -/
+theorem generalized_laguerre_second_derivative_bilinear
+    {P : ℕ → ℝ[X]} {m c : ℝ} (hzero : P 0 = 1)
+    (hrec : ∀ n, P (n + 1) =
+      (C c + X) * P n +
+        (C (m * c) + C (2 * m) * X) * (P n).derivative +
+          C (m ^ 2) * X * (P n).derivative.derivative) :
+    ∀ n, P (n + 1) =
+      (C m * X + C (-(0 : ℝ)) * X ^ 2) * (P n).derivative +
+        (C (c + m * (n : ℝ)) + C (1 + 0 * (n : ℝ)) * X) * P n := by
+  intro n
+  rw [generalized_laguerre_second_derivative_reduced hzero hrec n]
+  simp
+  ring
+
+/-- Every row of a generalized-Laguerre second-derivative sequence has degree
+equal to its index. -/
+theorem natDegree_of_generalized_laguerre_second_derivative
+    {P : ℕ → ℝ[X]} {m c : ℝ} (hzero : P 0 = 1)
+    (hrec : ∀ n, P (n + 1) =
+      (C c + X) * P n +
+        (C (m * c) + C (2 * m) * X) * (P n).derivative +
+          C (m ^ 2) * X * (P n).derivative.derivative) :
+    ∀ n, (P n).natDegree = n := by
+  exact natDegree_of_quadratic_derivative_bilinear P m 0 c m 1 0 hzero
+    (generalized_laguerre_second_derivative_bilinear hzero hrec) (by norm_num) (by norm_num)
+
+/-- Consecutive rows of a generalized-Laguerre second-derivative sequence are
+in proper position when both parameters are nonnegative. -/
+theorem prec_of_generalized_laguerre_second_derivative
+    {P : ℕ → ℝ[X]} {m c : ℝ} (hzero : P 0 = 1)
+    (hrec : ∀ n, P (n + 1) =
+      (C c + X) * P n +
+        (C (m * c) + C (2 * m) * X) * (P n).derivative +
+          C (m ^ 2) * X * (P n).derivative.derivative)
+    (hm : 0 ≤ m) (hc : 0 ≤ c) :
+    ∀ n, Prec (P n) (P (n + 1)) := by
+  exact prec_of_quadratic_derivative_bilinear P m 0 c m 1 0 hzero
+    (generalized_laguerre_second_derivative_bilinear hzero hrec)
+    hm (by norm_num) hc hm (by norm_num) (by norm_num)
+
+/-- Consecutive rows of a generalized-Laguerre second-derivative sequence
+interlace when both parameters are nonnegative. -/
+theorem interlaces_of_generalized_laguerre_second_derivative
+    {P : ℕ → ℝ[X]} {m c : ℝ} (hzero : P 0 = 1)
+    (hrec : ∀ n, P (n + 1) =
+      (C c + X) * P n +
+        (C (m * c) + C (2 * m) * X) * (P n).derivative +
+          C (m ^ 2) * X * (P n).derivative.derivative)
+    (hm : 0 ≤ m) (hc : 0 ≤ c) :
+    ∀ n, Interlaces (P n) (P (n + 1)) := by
+  intro n
+  exact (prec_of_generalized_laguerre_second_derivative hzero hrec hm hc n).toInterlaces (by
+    rw [natDegree_of_generalized_laguerre_second_derivative hzero hrec,
+      natDegree_of_generalized_laguerre_second_derivative hzero hrec])
+
+/-- Every row of a generalized-Laguerre second-derivative sequence is nonzero
+and real-rooted when both parameters are nonnegative. -/
+theorem isRealRooted_of_generalized_laguerre_second_derivative_sequence
+    {P : ℕ → ℝ[X]} {m c : ℝ} (hzero : P 0 = 1)
+    (hrec : ∀ n, P (n + 1) =
+      (C c + X) * P n +
+        (C (m * c) + C (2 * m) * X) * (P n).derivative +
+          C (m ^ 2) * X * (P n).derivative.derivative)
+    (hm : 0 ≤ m) (hc : 0 ≤ c) :
+    ∀ n, P n ≠ 0 ∧ (P n).Splits := fun n =>
+  (prec_of_generalized_laguerre_second_derivative hzero hrec hm hc n).1
+
+end RealRooted

RealRooted/DerivativeRecurrence/QuadraticInterlacing.lean

@@ -192,6 +192,203 @@ theorem prec_of_quadratic_derivative_linear
         (prec_of_quadratic_derivative_linear P a b c s t h0 hrec
           ha hb hc hs hbt (n + 1)).2.1.2
 
+lemma quadratic_derivative_bilinear_coeff_zero_succ
+    (P : ℕ → ℝ[X]) (a b c u s t : ℝ)
+    (hrec : ∀ n, P (n + 1) =
+      (C a * X + C (-b) * X ^ 2) * (P n).derivative +
+        (C (c + u * (n : ℝ)) + C (s + t * (n : ℝ)) * X) * P n)
+    (n : ℕ) :
+    Polynomial.coeff (P (n + 1)) 0 =
+      (c + u * (n : ℝ)) * Polynomial.coeff (P n) 0 := by
+  simp_all
+
+lemma hasNonnegCoeffs_of_quadratic_derivative_bilinear
+    (P : ℕ → ℝ[X]) (a b c u s t : ℝ)
+    (h0 : P 0 = 1)
+    (hrec : ∀ n, P (n + 1) =
+      (C a * X + C (-b) * X ^ 2) * (P n).derivative +
+        (C (c + u * (n : ℝ)) + C (s + t * (n : ℝ)) * X) * P n)
+    (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hu : 0 ≤ u)
+    (hs : 0 < s) (hbt : b ≤ t) :
+    ∀ n : ℕ, HasNonnegCoeffs (P n)
+  | 0 => by
+      intro k
+      rw [h0]
+      rcases k with _ | k <;> simp [coeff_one]
+  | n + 1 => by
+      rintro (_ | k)
+      · rw [quadratic_derivative_bilinear_coeff_zero_succ P a b c u s t hrec]
+        exact mul_nonneg (add_nonneg hc (mul_nonneg hu (Nat.cast_nonneg n)))
+          (hasNonnegCoeffs_of_quadratic_derivative_bilinear P a b c u s t h0 hrec
+            ha hb hc hu hs hbt n 0)
+      · rw [quadratic_derivative_bilinear_coeff_succ P a b c u s t hrec]
+        refine add_nonneg
+          (mul_nonneg (by
+            nlinarith [ha, hc, hu, Nat.cast_nonneg (α := ℝ) k, Nat.cast_nonneg (α := ℝ) n])
+            (hasNonnegCoeffs_of_quadratic_derivative_bilinear P a b c u s t h0 hrec
+              ha hb hc hu hs hbt n (k + 1))) ?_
+        rcases quadratic_derivative_bilinear_top_and_above P a b c u s t h0 hrec hs hbt n with
+          ⟨_, habove⟩
+        by_cases hkn : k ≤ n
+        · exact mul_nonneg (by
+            have hn : 0 ≤ (n : ℝ) := by simp
+            have hkn' : (k : ℝ) ≤ (n : ℝ) := by exact_mod_cast hkn
+            nlinarith [hs, hb, hbt, hn, hkn'])
+            (hasNonnegCoeffs_of_quadratic_derivative_bilinear P a b c u s t h0 hrec
+              ha hb hc hu hs hbt n k)
+        · simp_all
+
+lemma hasPosLeadingCoeff_of_quadratic_derivative_bilinear
+    (P : ℕ → ℝ[X]) (a b c u s t : ℝ)
+    (h0 : P 0 = 1)
+    (hrec : ∀ n, P (n + 1) =
+      (C a * X + C (-b) * X ^ 2) * (P n).derivative +
+        (C (c + u * (n : ℝ)) + C (s + t * (n : ℝ)) * X) * P n)
+    (hs : 0 < s) (hbt : b ≤ t) (n : ℕ) :
+    HasPosLeadingCoeff (P n) := by
+  rw [HasPosLeadingCoeff, leadingCoeff,
+    natDegree_of_quadratic_derivative_bilinear P a b c u s t h0 hrec hs hbt]
+  exact (quadratic_derivative_bilinear_top_and_above
+    P a b c u s t h0 hrec hs hbt n).1
+
+lemma prec_step_of_quadratic_derivative_bilinear
+    (P : ℕ → ℝ[X]) (a b c u s t : ℝ)
+    (h0 : P 0 = 1)
+    (hrec : ∀ n, P (n + 1) =
+      (C a * X + C (-b) * X ^ 2) * (P n).derivative +
+        (C (c + u * (n : ℝ)) + C (s + t * (n : ℝ)) * X) * P n)
+    (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hu : 0 ≤ u)
+    (hs : 0 < s) (hbt : b ≤ t)
+    (n : ℕ) (hn : 2 ≤ n) (hsp : (P n).Splits) :
+    Prec (P n) (P (n + 1)) := by
+  have hne : P n ≠ 0 :=
+    ne_zero_of_quadratic_derivative_bilinear P a b c u s t h0 hrec hs hbt n
+  have hroots_nonpos : ∀ r, (P n).IsRoot r → r ≤ 0 := fun r hr =>
+    roots_nonpos_of_hasNonnegCoeffs
+      (hasNonnegCoeffs_of_quadratic_derivative_bilinear P a b c u s t h0 hrec
+        ha hb hc hu hs hbt n) r ((mem_roots hne).mpr hr)
+  have hInter : Interlaces (P n).derivative (P n) :=
+    derivative_interlaces hsp (by
+      rw [natDegree_of_quadratic_derivative_bilinear P a b c u s t h0 hrec hs hbt]
+      exact hn)
+  have hg_pos : HasPosLeadingCoeff (P n).derivative :=
+    (hasPosLeadingCoeff_of_quadratic_derivative_bilinear
+      P a b c u s t h0 hrec hs hbt n).derivative (by
+        rw [natDegree_of_quadratic_derivative_bilinear P a b c u s t h0 hrec hs hbt]
+        lia)
+  have hF_eq :
+      (C (c + u * (n : ℝ)) + C (s + t * (n : ℝ)) * X) * P n +
+        (C a * X + C (-b) * X ^ 2) * (P n).derivative = P (n + 1) := by
+    grind
+  have hF_pos :
+      HasPosLeadingCoeff
+        ((C (c + u * (n : ℝ)) + C (s + t * (n : ℝ)) * X) * P n +
+          (C a * X + C (-b) * X ^ 2) * (P n).derivative) := by
+    rw [hF_eq]
+    exact hasPosLeadingCoeff_of_quadratic_derivative_bilinear
+      P a b c u s t h0 hrec hs hbt (n + 1)
+  have hdeg_lo :
+      (P n).natDegree ≤
+        ((C (c + u * (n : ℝ)) + C (s + t * (n : ℝ)) * X) * P n +
+          (C a * X + C (-b) * X ^ 2) * (P n).derivative).natDegree := by
+    rw [hF_eq, natDegree_of_quadratic_derivative_bilinear
+      P a b c u s t h0 hrec hs hbt,
+      natDegree_of_quadratic_derivative_bilinear P a b c u s t h0 hrec hs hbt]
+    lia
+  have hdeg_hi :
+      ((C (c + u * (n : ℝ)) + C (s + t * (n : ℝ)) * X) * P n +
+        (C a * X + C (-b) * X ^ 2) * (P n).derivative).natDegree ≤
+          (P n).natDegree + 1 := by
+    rw [hF_eq, natDegree_of_quadratic_derivative_bilinear
+      P a b c u s t h0 hrec hs hbt,
+      natDegree_of_quadratic_derivative_bilinear P a b c u s t h0 hrec hs hbt]
+  have hb_nonpos : ∀ r, (P n).IsRoot r →
+      (C a * X + C (-b) * X ^ 2 : ℝ[X]).eval r ≤ 0 := by
+    intro r hr
+    exact quadratic_derivative_linear_v_nonpos_of_nonpos ha hb (hroots_nonpos r hr)
+  have := prec_of_interlaces_evalCoeff_nonpos
+    (f := P n) (g := (P n).derivative)
+    (a := C (c + u * (n : ℝ)) + C (s + t * (n : ℝ)) * X)
+    (b := C a * X + C (-b) * X ^ 2)
+    hInter hg_pos hF_pos hdeg_lo hdeg_hi hb_nonpos
+  rw [hF_eq] at this
+  exact this
+
+theorem prec_of_quadratic_derivative_bilinear
+    (P : ℕ → ℝ[X]) (a b c u s t : ℝ)
+    (h0 : P 0 = 1)
+    (hrec : ∀ n, P (n + 1) =
+      (C a * X + C (-b) * X ^ 2) * (P n).derivative +
+        (C (c + u * (n : ℝ)) + C (s + t * (n : ℝ)) * X) * P n)
+    (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hu : 0 ≤ u)
+    (hs : 0 < s) (hbt : b ≤ t) :
+    ∀ n : ℕ, Prec (P n) (P (n + 1))
+  | 0 => by
+      have : Interlaces (P 0) (P 1) := by
+        rw [h0]
+        exact interlaces_one_linear (p := P 1)
+          (by rw [natDegree_of_quadratic_derivative_bilinear
+            P a b c u s t h0 hrec hs hbt])
+      exact this.toPrec
+  | 1 => by
+      have hp1 : P 1 = C c + C s * X := by simp_all
+      have hder : (P 1).derivative = C s := by simp_all
+      have hInter : Interlaces (P 1).derivative (P 1) := by
+        rw [hder]
+        exact interlaces_C_linear (c := s) hs.ne' (p := P 1)
+          (by rw [natDegree_of_quadratic_derivative_bilinear
+            P a b c u s t h0 hrec hs hbt])
+      have hg_pos : HasPosLeadingCoeff (P 1).derivative := by
+        rw [hder]
+        simpa [HasPosLeadingCoeff, leadingCoeff] using hs
+      have hF_eq :
+          (C (c + u * ((1 : ℕ) : ℝ)) + C (s + t * ((1 : ℕ) : ℝ)) * X) * P 1 +
+            (C a * X + C (-b) * X ^ 2) * (P 1).derivative = P 2 := by
+        grind
+      have hF_pos :
+          HasPosLeadingCoeff
+            ((C (c + u * ((1 : ℕ) : ℝ)) + C (s + t * ((1 : ℕ) : ℝ)) * X) * P 1 +
+              (C a * X + C (-b) * X ^ 2) * (P 1).derivative) := by
+        rw [hF_eq]
+        exact hasPosLeadingCoeff_of_quadratic_derivative_bilinear
+          P a b c u s t h0 hrec hs hbt 2
+      have hdeg_lo :
+          (P 1).natDegree ≤
+            ((C (c + u * ((1 : ℕ) : ℝ)) + C (s + t * ((1 : ℕ) : ℝ)) * X) * P 1 +
+              (C a * X + C (-b) * X ^ 2) * (P 1).derivative).natDegree := by
+        rw [hF_eq, natDegree_of_quadratic_derivative_bilinear
+          P a b c u s t h0 hrec hs hbt,
+          natDegree_of_quadratic_derivative_bilinear P a b c u s t h0 hrec hs hbt]
+        lia
+      have hdeg_hi :
+          ((C (c + u * ((1 : ℕ) : ℝ)) + C (s + t * ((1 : ℕ) : ℝ)) * X) * P 1 +
+            (C a * X + C (-b) * X ^ 2) * (P 1).derivative).natDegree ≤
+              (P 1).natDegree + 1 := by
+        rw [hF_eq, natDegree_of_quadratic_derivative_bilinear
+          P a b c u s t h0 hrec hs hbt,
+          natDegree_of_quadratic_derivative_bilinear P a b c u s t h0 hrec hs hbt]
+      have hne : P 1 ≠ 0 :=
+        ne_zero_of_quadratic_derivative_bilinear P a b c u s t h0 hrec hs hbt 1
+      have hb_nonpos : ∀ r, (P 1).IsRoot r →
+          (C a * X + C (-b) * X ^ 2 : ℝ[X]).eval r ≤ 0 := by
+        intro r hr
+        have hr_nonpos := roots_nonpos_of_hasNonnegCoeffs
+          (hasNonnegCoeffs_of_quadratic_derivative_bilinear P a b c u s t h0 hrec
+            ha hb hc hu hs hbt 1) r ((mem_roots hne).mpr hr)
+        exact quadratic_derivative_linear_v_nonpos_of_nonpos ha hb hr_nonpos
+      have := prec_of_interlaces_evalCoeff_nonpos
+        (f := P 1) (g := (P 1).derivative)
+        (a := C (c + u * ((1 : ℕ) : ℝ)) + C (s + t * ((1 : ℕ) : ℝ)) * X)
+        (b := C a * X + C (-b) * X ^ 2)
+        hInter hg_pos hF_pos hdeg_lo hdeg_hi hb_nonpos
+      rw [hF_eq] at this
+      exact this
+  | n + 2 =>
+      prec_step_of_quadratic_derivative_bilinear P a b c u s t h0 hrec
+        ha hb hc hu hs hbt (n + 2) (by lia)
+        (prec_of_quadratic_derivative_bilinear P a b c u s t h0 hrec
+          ha hb hc hu hs hbt (n + 1)).2.1.2
+
 lemma hasNonnegCoeffs_of_quadratic_derivative_linear_offset
     (P : ℕ → ℝ[X]) (a b c s t : ℝ) (d : ℕ)
     (hbase_nonneg : HasNonnegCoeffs (P 0))

RealRooted/Tactic.lean

@@ -27,6 +27,7 @@ import RealRooted.Tactic.SecondDerivative
 import RealRooted.Tactic.Favard
 import RealRooted.Tactic.LiuWang
 import RealRooted.Tactic.GammaRealRoots
+import RealRooted.Tactic.GeneralizedLaguerre
 import RealRooted.Tactic.MagnitudeDominated
 import RealRooted.Tactic.PreservingOperatorSequence
 import RealRooted.Tactic.Product

RealRooted/Tactic/Examples.lean

@@ -22,6 +22,7 @@ import RealRooted.Tactic.Examples.Wagner
 import RealRooted.Tactic.Examples.WagnerX
 import RealRooted.Tactic.Examples.Favard
 import RealRooted.Tactic.Examples.GammaRealRoots
+import RealRooted.Tactic.Examples.GeneralizedLaguerre
 import RealRooted.Tactic.Examples.MaWang
 import RealRooted.Tactic.Examples.EndpointDerivative
 import RealRooted.Tactic.Examples.MagnitudeDominated

RealRooted/Tactic/Examples/GeneralizedLaguerre.lean

@@ -0,0 +1,48 @@
+import RealRooted.Tactic.GeneralizedLaguerre
+
+/-!
+# Generalized-Laguerre second-derivative tactic examples
+
+Regression tests for three parameter pairs used by OEIS proof clients.
+-/
+
+open Polynomial
+
+namespace RealRooted
+namespace Tactic
+
+example {P : ℕ → ℝ[X]} (hzero : P 0 = 1)
+    (hrec : ∀ n, P (n + 1) =
+      (C 2 + X) * P n + (C 2 + C 2 * X) * (P n).derivative +
+        C 1 * X * (P n).derivative.derivative) :
+    ∀ n, Interlaces (P n) (P (n + 1)) := by
+  rr_generalized_laguerre_second_derivative_sequence using
+    scale := (1 : ℝ),
+    parameter := (2 : ℝ),
+    base := hzero,
+    recurrence := hrec
+
+example {P : ℕ → ℝ[X]} (hzero : P 0 = 1)
+    (hrec : ∀ n, P (n + 1) =
+      (C 2 + X) * P n + (C 4 + C 4 * X) * (P n).derivative +
+        C 4 * X * (P n).derivative.derivative) :
+    ∀ n, Prec (P n) (P (n + 1)) := by
+  rr_generalized_laguerre_second_derivative_sequence using
+    scale := (2 : ℝ),
+    parameter := (2 : ℝ),
+    base := hzero,
+    recurrence := hrec
+
+example {P : ℕ → ℝ[X]} (hzero : P 0 = 1)
+    (hrec : ∀ n, P (n + 1) =
+      (C 6 + X) * P n + (C 24 + C 8 * X) * (P n).derivative +
+        C 16 * X * (P n).derivative.derivative) :
+    ∀ n, P n ≠ 0 ∧ (P n).Splits := by
+  rr_generalized_laguerre_second_derivative_sequence using
+    scale := (4 : ℝ),
+    parameter := (6 : ℝ),
+    base := hzero,
+    recurrence := hrec
+
+end Tactic
+end RealRooted