Add sign-regular matrix predicate API

RealRooted.lean

@@ -21,8 +21,11 @@ import RealRooted.AllCombo
 import RealRooted.Apolarity
 import RealRooted.Basic
 import RealRooted.Bezoutian
-import RealRooted.BoundarySpecializationRight
+import RealRooted.BorceaBranden.Applications.BidiagonalSymbol
+import RealRooted.BorceaBranden.Applications.HomogenizeStable
+import RealRooted.BorceaBranden.Applications.UnivariateSymbol
 import RealRooted.BorceaBranden.BoundarySpecialization
+import RealRooted.BorceaBranden.FiniteSymbolBasis
 import RealRooted.BorceaBranden.FiniteSymbolCoefficient
 import RealRooted.BorceaBranden.FiniteSymbolContraction
 import RealRooted.BorceaBranden.FiniteSymbolDegree
@@ -32,10 +35,7 @@ import RealRooted.BorceaBranden.FiniteSymbolProduct
 import RealRooted.BorceaBranden.FiniteSymbolReciprocal
 import RealRooted.BorceaBranden.FiniteSymbolReconstruction
 import RealRooted.BorceaBranden.FiniteSymbolReconstructionCore
-import RealRooted.BorceaBranden.FiniteSymbolBasis
-import RealRooted.BorceaBranden.Applications.BidiagonalSymbol
-import RealRooted.BorceaBranden.Applications.HomogenizeStable
-import RealRooted.BorceaBranden.Applications.UnivariateSymbol
+import RealRooted.BoundarySpecializationRight
 import RealRooted.CauchyInterlacing
 import RealRooted.Challenges.AissenSchoenbergWhitney
 import RealRooted.Challenges.BorceaBranden
@@ -195,21 +195,35 @@ import RealRooted.Mathlib.Algebra.Polynomial.Homogenize
 import RealRooted.Mathlib.Algebra.Polynomial.Roots
 import RealRooted.Mathlib.Algebra.Polynomial.Splits
 import RealRooted.Mathlib.Analysis.Complex.OpenMapping
+import RealRooted.Mathlib.Analysis.SpecialFunctions.ExpIntegral
 import RealRooted.Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
 import RealRooted.Mathlib.Combinatorics.Enumerative.OrderedSubsetPairs
+import RealRooted.Mathlib.Data.Fin.Basic
+import RealRooted.Mathlib.Data.List.Basic
+import RealRooted.Mathlib.Data.List.Destutter
 import RealRooted.Mathlib.Data.List.Interleave
+import RealRooted.Mathlib.Data.List.OfFn
 import RealRooted.Mathlib.Data.List.Zip
 import RealRooted.Mathlib.Data.Nat.Cast.Basic
 import RealRooted.Mathlib.Data.Nat.Choose.Cast
 import RealRooted.Mathlib.LinearAlgebra.Matrix.Determinant.Basic
+import RealRooted.Mathlib.LinearAlgebra.Matrix.Determinant.CauchyBinet
+import RealRooted.Mathlib.LinearAlgebra.Matrix.Determinant.Integral
+import RealRooted.Mathlib.LinearAlgebra.Matrix.Gaussian
 import RealRooted.Mathlib.LinearAlgebra.Matrix.KernelSignVariation
+import RealRooted.Mathlib.LinearAlgebra.Matrix.SignRegular
+import RealRooted.Mathlib.LinearAlgebra.Matrix.SignRegularRankDeficient
+import RealRooted.Mathlib.LinearAlgebra.Matrix.SignRegularStrictification
+import RealRooted.Mathlib.LinearAlgebra.Matrix.SignRegularVariation
 import RealRooted.Mathlib.LinearAlgebra.Matrix.SignVariation
+import RealRooted.Mathlib.LinearAlgebra.Matrix.SignVariationTopology
 import RealRooted.Mathlib.LinearAlgebra.Matrix.TotallyNonneg
 import RealRooted.Mathlib.LinearAlgebra.Matrix.VariationDiminishing
+import RealRooted.Mathlib.LinearAlgebra.Vandermonde
 import RealRooted.MatrixInterlacing
-import RealRooted.MultiaffineReciprocalRight
 import RealRooted.Multiaffine
 import RealRooted.MultiaffineReciprocal
+import RealRooted.MultiaffineReciprocalRight
 import RealRooted.MultiplierSequence
 import RealRooted.MultivariateStability
 import RealRooted.NarayanaTransformation

RealRooted/ASWKarlinKernel.lean

@@ -2,6 +2,7 @@ import RealRooted.ASWKarlinMatrix
 import RealRooted.ASWKarlinThreshold
 import RealRooted.ASWKarlinVariation
 import RealRooted.ASWKarlinVectors
+import RealRooted.Mathlib.LinearAlgebra.Matrix.SignRegularRankDeficient
 import Mathlib.Analysis.Complex.Basic
 import Mathlib.Analysis.SpecialFunctions.Complex.Arg
 
@@ -120,6 +121,49 @@ lemma complex_root_ne_zero_of_coeff_zero_pos {p : ℝ[X]} {z : ℂ}
     exact heval
   linarith
 
+/-- Karlin's repeated matrices force a linear lower bound on the sampled sine
+vector's sign variations, up to the fixed two-endpoint perturbation loss. -/
+theorem aswKarlinRepeatedSineVariationLowerBound
+    {p : ℝ[X]} {z : ℂ} (hz : z ∈ (p.map (algebraMap ℝ ℂ)).roots)
+    (hdegree : 0 < p.natDegree) (hconst : 0 < p.coeff 0)
+    (hpf : IsPolyaFreqSeq p.coeff) {order blocks : ℕ}
+    (horder : 0 < order) (hblocks : 0 < blocks) (him : z.im ≠ 0) :
+    blocks * order - 1 ≤
+      Fin.signVariations
+        (aswKarlinSineVector z.arg p.natDegree order blocks) + 2 := by
+  have hwidth : 0 < blocks * (p.natDegree + order - 1) :=
+    Nat.mul_pos hblocks (by lia)
+  have hcols :
+      blocks * (p.natDegree + order - 1) + 1 =
+        (blocks * (p.natDegree + order - 1) - 1) + 2 := by
+    lia
+  have hnodal :
+      ∀ i : Fin (blocks * (p.natDegree + order - 1) - 1),
+        aswKarlinRootVector z p.natDegree order blocks
+            (Fin.cast hcols.symm i.succ.castSucc) = 0 →
+          aswKarlinRootVector z p.natDegree order blocks
+              (Fin.cast hcols.symm i.castSucc.castSucc) *
+            aswKarlinRootVector z p.natDegree order blocks
+              (Fin.cast hcols.symm i.succ.succ) < 0 := by
+    intro i hi
+    change (z ^ ((i : ℕ) + 1)).im = 0 at hi
+    change (z ^ (i : ℕ)).im * (z ^ ((i : ℕ) + 2)).im < 0
+    exact
+      im_pow_mul_im_pow_add_two_neg_of_im_pow_add_one_eq_zero him i hi
+  have hbound :=
+    Matrix.IsTotallyNonnegRect.card_sub_one_le_signVariations_add_two_of_surjective_of_card_eq
+      (hpf.aswKarlinMatrix_isTotallyNonnegRect
+        p.natDegree order blocks)
+      hcols
+      (aswKarlinMatrix_mulVec_surjective p.natDegree order blocks
+        hdegree horder hconst)
+      (aswKarlinMatrix_mulVec_rootVector hz order blocks hdegree horder)
+      hnodal
+  rw [signVariations_aswKarlinRootVector_eq_sine
+    (complex_root_ne_zero_of_coeff_zero_pos hz hconst)
+    p.natDegree order blocks] at hbound
+  exact hbound
+
 /-- A real complex root of a positive-constant PF polynomial lies on the
 negative real ray. -/
 lemma arg_eq_pi_of_real_complex_root_of_isPolyaFreqSeq_coeff {p : ℝ[X]} {z : ℂ}
@@ -194,19 +238,83 @@ theorem aswKarlinSectorThreshold_le_abs_arg_of_im_ne_zero_of_classicalInput
 /-- Karlin's finite-order sector estimate for a nonreal complex root of a
 positive constant-coefficient PF polynomial.
 
-The checked algebraic inputs above provide the repeated totally nonnegative
-coefficient-window matrix, its full row rank from the positive constant
-coefficient, and the root-supplied kernel vector.  The remaining hard ingredient
-is the classical variation-diminishing/sign-regular kernel theorem. -/
+The proof uses the repeated totally nonnegative coefficient-window matrices,
+their full row rank, the root-supplied kernel vectors, and the sampled-sine
+floor bound. Taking sufficiently many blocks absorbs the fixed two-endpoint
+perturbation loss. -/
 theorem aswKarlinSectorThreshold_le_abs_arg_of_im_ne_zero {p : ℝ[X]} {z : ℂ}
     (hz : z ∈ (p.map (algebraMap ℝ ℂ)).roots)
     (hdegree : 0 < p.natDegree) (hconst : 0 < p.coeff 0)
     (hpf : IsPolyaFreqSeq p.coeff) {order : ℕ} (horder : 0 < order)
     (him : z.im ≠ 0) :
-    aswSectorThreshold p.natDegree order ≤ |z.arg| :=
-  aswKarlinSectorThreshold_le_abs_arg_of_im_ne_zero_of_classicalInput
-    aswKarlinKernelSignVariationClassicalInput hz hdegree hconst hpf horder
-    him
+    aswSectorThreshold p.natDegree order ≤ |z.arg| := by
+  by_contra hnot
+  have hθlt :
+      |z.arg| < aswSectorThreshold p.natDegree order :=
+    lt_of_not_ge hnot
+  have hden_pos :=
+    aswSectorThreshold_denom_pos p.natDegree order hdegree horder
+  have hspan_cast :
+      ((p.natDegree + order - 1 : ℕ) : ℝ) =
+        (order : ℝ) + p.natDegree - 1 := by
+    rw [Nat.cast_sub (by lia)]
+    push_cast
+    ring
+  have hmul := mul_lt_mul_of_pos_left hθlt hden_pos
+  have hnormalize :
+      ((order : ℝ) + p.natDegree - 1) *
+          aswSectorThreshold p.natDegree order =
+        (order : ℝ) * Real.pi := by
+    rw [aswSectorThreshold]
+    field_simp [hden_pos.ne']
+  rw [hnormalize] at hmul
+  have hslope_lt :
+      (((p.natDegree + order - 1 : ℕ) : ℝ) * |z.arg|) /
+          Real.pi < (order : ℝ) := by
+    apply (div_lt_iff₀ Real.pi_pos).2
+    rw [hspan_cast]
+    exact hmul
+  let gap : ℝ :=
+    (order : ℝ) -
+      (((p.natDegree + order - 1 : ℕ) : ℝ) * |z.arg|) / Real.pi
+  have hgap : 0 < gap := by
+    dsimp [gap]
+    linarith
+  obtain ⟨blocks, hblocks⟩ := exists_nat_gt (3 / gap)
+  have hblocks_pos : 0 < blocks := by
+    have hfrac : (0 : ℝ) < 3 / gap := by positivity
+    exact_mod_cast hfrac.trans hblocks
+  have hlarge : (3 : ℝ) < (blocks : ℝ) * gap := by
+    have hmulGap := mul_lt_mul_of_pos_right hblocks hgap
+    rw [div_mul_cancel₀ _ hgap.ne'] at hmulGap
+    exact hmulGap
+  have hlower :=
+    aswKarlinRepeatedSineVariationLowerBound
+      hz hdegree hconst hpf horder hblocks_pos him
+  have hupper :=
+    signVariations_aswKarlinSineVector_le_floor_div_pi_abs
+      z.arg p.natDegree order blocks
+  let x : ℝ :=
+    (((blocks * (p.natDegree + order - 1) : ℕ) : ℝ) * |z.arg|) /
+      Real.pi
+  have hnat : blocks * order ≤ ⌊x⌋₊ + 3 := by
+    dsimp [x]
+    lia
+  have hcast : ((blocks * order : ℕ) : ℝ) ≤ (⌊x⌋₊ : ℝ) + 3 := by
+    exact_mod_cast hnat
+  have hfloor : (⌊x⌋₊ : ℝ) ≤ x := Nat.floor_le (by dsimp [x]; positivity)
+  have hx_eq :
+      x =
+        (blocks : ℝ) *
+          ((((p.natDegree + order - 1 : ℕ) : ℝ) * |z.arg|) /
+            Real.pi) := by
+    dsimp [x]
+    push_cast
+    ring
+  rw [hx_eq] at hcast hfloor
+  dsimp [gap] at hlarge
+  push_cast at hcast
+  linarith
 
 /-- Conditional Karlin finite-order sector estimate for one complex root, with
 the classical sign-variation input supplied explicitly. -/
@@ -231,8 +339,12 @@ theorem aswKarlinSectorThreshold_le_abs_arg {p : ℝ[X]} {z : ℂ}
     (hz : z ∈ (p.map (algebraMap ℝ ℂ)).roots)
     (hdegree : 0 < p.natDegree) (hconst : 0 < p.coeff 0)
     (hpf : IsPolyaFreqSeq p.coeff) {order : ℕ} (horder : 0 < order) :
-    aswSectorThreshold p.natDegree order ≤ |z.arg| :=
-  aswKarlinSectorThreshold_le_abs_arg_of_classicalInput
-    aswKarlinKernelSignVariationClassicalInput hz hdegree hconst hpf horder
+    aswSectorThreshold p.natDegree order ≤ |z.arg| := by
+  by_cases him : z.im = 0
+  · rw [arg_eq_pi_of_real_complex_root_of_isPolyaFreqSeq_coeff hz hconst hpf him,
+      abs_of_pos Real.pi_pos]
+    exact aswSectorThreshold_le_pi p.natDegree order hdegree horder
+  · exact aswKarlinSectorThreshold_le_abs_arg_of_im_ne_zero
+      hz hdegree hconst hpf horder him
 
 end RealRooted

RealRooted/ASWKarlinSineBounds.lean

@@ -226,6 +226,50 @@ lemma signVariations_sin_mul_lt_of_last_le_nat_mul_pi
               simp [k]
             exact lt_trans hlt hk_lt
 
+/-- The sampled sine vector has at most the number of completed half-turns in
+its final angle. -/
+lemma signVariations_sin_mul_le_floor_div_pi
+    {N : ℕ} {θ : ℝ} (hθ0 : 0 ≤ θ) :
+    Fin.signVariations
+        (fun j : Fin (N + 1) => Real.sin ((j : ℕ) * θ)) ≤
+      ⌊((N : ℝ) * θ) / Real.pi⌋₊ := by
+  let r : ℕ := ⌊((N : ℝ) * θ) / Real.pi⌋₊
+  have hquot :
+      ((N : ℝ) * θ) / Real.pi < ((r + 1 : ℕ) : ℝ) := by
+    simpa only [r, Nat.cast_add, Nat.cast_one] using
+      Nat.lt_floor_add_one (((N : ℝ) * θ) / Real.pi)
+  have hlast :
+      (N : ℝ) * θ ≤ ((r + 1 : ℕ) : ℝ) * Real.pi := by
+    have hmul := mul_lt_mul_of_pos_right hquot Real.pi_pos
+    rw [div_mul_cancel₀ _ Real.pi_ne_zero] at hmul
+    exact hmul.le
+  have hlt :=
+    signVariations_sin_mul_lt_of_last_le_nat_mul_pi
+      (N := N) (order := r + 1) (by positivity) hθ0 hlast
+  exact Nat.lt_succ_iff.mp
+    (by simpa only [Nat.succ_eq_add_one] using hlt)
+
+/-- Absolute-angle form of the sampled-sine floor bound for Karlin's repeated
+vector. -/
+lemma signVariations_aswKarlinSineVector_le_floor_div_pi_abs
+    (θ : ℝ) (degree order blocks : ℕ) :
+    Fin.signVariations (aswKarlinSineVector θ degree order blocks) ≤
+      ⌊(((blocks * (degree + order - 1) : ℕ) : ℝ) * |θ|) /
+        Real.pi⌋₊ := by
+  by_cases hθ : 0 ≤ θ
+  · rw [abs_of_nonneg hθ]
+    change Fin.signVariations
+        (fun j : Fin (blocks * (degree + order - 1) + 1) =>
+          Real.sin ((j : ℕ) * θ)) ≤ _
+    exact signVariations_sin_mul_le_floor_div_pi hθ
+  · have hθneg : θ < 0 := lt_of_not_ge hθ
+    rw [← signVariations_aswKarlinSineVector_neg θ degree order blocks,
+      abs_of_neg hθneg]
+    change Fin.signVariations
+        (fun j : Fin (blocks * (degree + order - 1) + 1) =>
+          Real.sin ((j : ℕ) * -θ)) ≤ _
+    exact signVariations_sin_mul_le_floor_div_pi (neg_nonneg.mpr hθneg.le)
+
 /-- One-block Karlin sine vectors inherit the general sampled-sine
 sign-variation bound from a last-angle estimate. -/
 lemma signVariations_aswKarlinSineVector_lt_of_last_le_order_pi

RealRooted/ASWKarlinVariation.lean

@@ -63,31 +63,6 @@ theorem IsPolyaFreqSeq.aswKarlinKernelSignVariationLowerBound_of_classicalInput
   exact hclassical hdegree horder hconst hlead hsupport htn hsurj
     hker hvec_ne
 
-/-- Remaining classical sign-regular kernel lower bound for a full-row-rank
-totally nonnegative one-block Karlin coefficient-window matrix.
-
-This is the only remaining non-elementary input in the current Karlin sector
-proof.  It should eventually be proved from the specialized sign-regular
-variation-diminishing theorem for a full-row-rank totally nonnegative Toeplitz
-window matrix. -/
-theorem aswKarlinKernelSignVariationClassicalInput :
-    AswKarlinKernelSignVariationClassicalInputStatement := by
-  intro u degree order hdegree horder hconst hlead hsupport htn hsurj v hker hvec_ne
-  -- Remaining classical step: use `htn`, `hsurj`, the endpoint/support data,
-  -- `hker`, and `hvec_ne` to prove the kernel sign-variation lower bound.
-  sorry
-
-/-- Classical sign-regular kernel lower bound for a PF one-block Karlin
-coefficient-window matrix. -/
-theorem IsPolyaFreqSeq.aswKarlinKernelSignVariationLowerBound
-    {u : ℕ → ℝ} (hpf : IsPolyaFreqSeq u) (degree order : ℕ)
-    (hdegree : 0 < degree) (horder : 0 < order) (hconst : 0 < u 0)
-    (hlead : 0 < u degree) (hsupport : ∀ k, degree < k → u k = 0) :
-    AswKarlinKernelSignVariationLowerBound degree order u := by
-  exact hpf.aswKarlinKernelSignVariationLowerBound_of_classicalInput
-    aswKarlinKernelSignVariationClassicalInput degree order hdegree horder
-    hconst hlead hsupport
-
 /-- The final sector inequality follows once the two sign-variation bounds are
 available: a lower bound from the full-row-rank TN kernel theorem and an upper
 bound for the sampled sine vector inside the forbidden sector. -/

RealRooted/ASWKarlinVectors.lean

@@ -46,6 +46,72 @@ lemma im_pow_eq_norm_pow_mul_sin_arg (z : ℂ) (n : ℕ) :
     Complex.exp_im]
   simp
 
+/-- If a nonreal complex geometric progression has an interior zero imaginary
+part, the adjacent imaginary parts have opposite strict signs. -/
+lemma im_pow_mul_im_pow_add_two_neg_of_im_pow_add_one_eq_zero
+    {z : ℂ} (him : z.im ≠ 0) (i : ℕ)
+    (hzero : (z ^ (i + 1)).im = 0) :
+    (z ^ i).im * (z ^ (i + 2)).im < 0 := by
+  let θ := z.arg
+  have hz : z ≠ 0 := by
+    intro hz
+    apply him
+    simp [hz]
+  have hnorm : 0 < ‖z‖ := norm_pos_iff.mpr hz
+  have hsin : Real.sin θ ≠ 0 := by
+    have hpolar := im_pow_eq_norm_pow_mul_sin_arg z 1
+    simp only [pow_one, Nat.cast_one, one_mul] at hpolar
+    intro hs
+    apply him
+    rw [hpolar, hs, mul_zero]
+  have hzeroSin : Real.sin ((i + 1 : ℕ) * θ) = 0 := by
+    rw [im_pow_eq_norm_pow_mul_sin_arg] at hzero
+    exact (mul_eq_zero.mp hzero).resolve_left (pow_ne_zero _ hnorm.ne')
+  have hcos : Real.cos ((i + 1 : ℕ) * θ) ≠ 0 := by
+    intro hc
+    have hsq := Real.sin_sq_add_cos_sq ((i + 1 : ℕ) * θ)
+    rw [hzeroSin, hc] at hsq
+    norm_num at hsq
+  have hprev :
+      Real.sin (i * θ) =
+        -Real.cos ((i + 1 : ℕ) * θ) * Real.sin θ := by
+    have harg :
+        (i : ℝ) * θ = ((i + 1 : ℕ) : ℝ) * θ - θ := by
+      push_cast
+      ring
+    rw [harg, Real.sin_sub, hzeroSin]
+    ring
+  have hnext :
+      Real.sin ((i + 2 : ℕ) * θ) =
+        Real.cos ((i + 1 : ℕ) * θ) * Real.sin θ := by
+    have harg :
+        ((i + 2 : ℕ) : ℝ) * θ =
+          ((i + 1 : ℕ) : ℝ) * θ + θ := by
+      push_cast
+      ring
+    rw [harg, Real.sin_add, hzeroSin]
+    ring
+  have htrig :
+      Real.sin (i * θ) * Real.sin ((i + 2 : ℕ) * θ) < 0 := by
+    rw [hprev, hnext]
+    calc
+      (-Real.cos ((i + 1 : ℕ) * θ) * Real.sin θ) *
+          (Real.cos ((i + 1 : ℕ) * θ) * Real.sin θ) =
+          -(Real.cos ((i + 1 : ℕ) * θ) ^ 2 * Real.sin θ ^ 2) := by
+            ring
+      _ < 0 := neg_lt_zero.mpr
+        (mul_pos (sq_pos_of_ne_zero hcos) (sq_pos_of_ne_zero hsin))
+  rw [im_pow_eq_norm_pow_mul_sin_arg,
+    im_pow_eq_norm_pow_mul_sin_arg]
+  calc
+    (‖z‖ ^ i * Real.sin (i * θ)) *
+        (‖z‖ ^ (i + 2) * Real.sin ((i + 2 : ℕ) * θ)) =
+        (‖z‖ ^ i * ‖z‖ ^ (i + 2)) *
+          (Real.sin (i * θ) * Real.sin ((i + 2 : ℕ) * θ)) := by
+            ring
+    _ < 0 := mul_neg_of_pos_of_neg
+      (mul_pos (pow_pos hnorm _) (pow_pos hnorm _)) htrig
+
 /-- A nonzero complex number's root vector and sampled sine vector have the
 same coordinate signs. -/
 lemma signVariations_aswKarlinRootVector_eq_sine {z : ℂ} (hz : z ≠ 0)

RealRooted/AissenSchoenbergWhitney.lean

@@ -301,9 +301,12 @@ theorem aswSectorThreshold_le_abs_arg_of_isPolyaFreqSeq_coeff {p : ℝ[X]} {z :
     (hdegree : 0 < p.natDegree) (hconst : 0 < p.coeff 0)
     (hpf : IsPolyaFreqSeq p.coeff)
     (hz : z ∈ (p.map (algebraMap ℝ ℂ)).roots) (order : ℕ) :
-    aswSectorThreshold p.natDegree order ≤ |z.arg| :=
-  aswSectorThreshold_le_abs_arg_of_isPolyaFreqSeq_coeff_of_classicalInput
-    aswKarlinKernelSignVariationClassicalInput hdegree hconst hpf hz order
+    aswSectorThreshold p.natDegree order ≤ |z.arg| := by
+  by_cases horder : order = 0
+  · simp [aswSectorThreshold, horder]
+  · exact aswKarlinSectorThreshold_le_abs_arg
+      (p := p) (z := z) hz hdegree hconst hpf
+      (horder := Nat.pos_of_ne_zero horder)
 
 /-! ### Reduction to positive constant coefficient -/