Extend affine finite-symbol sufficiency to degree boxes

RealRooted.lean

@@ -21,7 +21,9 @@ import RealRooted.AllCombo
 import RealRooted.Apolarity
 import RealRooted.Basic
 import RealRooted.Bezoutian
+import RealRooted.BivariateOpenMapping
 import RealRooted.BorceaBranden.Applications.BidiagonalSymbol
+import RealRooted.BorceaBranden.Applications.DegreeBoxPolarization
 import RealRooted.BorceaBranden.Applications.HomogenizeStable
 import RealRooted.BorceaBranden.Applications.UnivariateSymbol
 import RealRooted.BorceaBranden.BoundarySpecialization
@@ -193,6 +195,8 @@ import RealRooted.LowerTriangularMatrix
 import RealRooted.MaWang
 import RealRooted.MagnitudeDominated
 import RealRooted.MaoWangMatrixProduct
+import RealRooted.Mathlib.Algebra.MvPolynomial.Degrees
+import RealRooted.Mathlib.Algebra.MvPolynomial.Equiv
 import RealRooted.Mathlib.Algebra.MvPolynomial.Stability.DegreeBox
 import RealRooted.Mathlib.Algebra.MvPolynomial.Stability.Symbol
 import RealRooted.Mathlib.Algebra.Polynomial.Basic
@@ -230,6 +234,7 @@ 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.Mathlib.RingTheory.MvPolynomial.Symmetric
 import RealRooted.MatrixInterlacing
 import RealRooted.Multiaffine
 import RealRooted.MultiaffineReciprocal
@@ -243,6 +248,7 @@ import RealRooted.ObreschkoffContinuity
 import RealRooted.ObreschkoffConverse
 import RealRooted.OperatorPreservesInterlacing
 import RealRooted.PFPolynomial
+import RealRooted.PartialSymmetrization
 import RealRooted.Polarization
 import RealRooted.PolyaFrequencyConvolution
 import RealRooted.PosCombo

RealRooted/Apolarity.lean

@@ -589,6 +589,43 @@ theorem grace_apolarity_closedBall {n : Nat} {c : ℂ} {r : ℝ} {f g : ℂ[X]}
 def polarDeriv (n : Nat) (ζ : ℂ) (A : ℂ[X]) : ℂ[X] :=
   C (n : ℂ) * A + (C ζ - X) * derivative A
 
+/-- The polar derivative lowers the ambient degree bound by one. This is the
+bounded-degree invariant needed in the Grace apolarity induction. -/
+theorem polarDeriv_natDegree_le
+    {n : Nat} {ζ : ℂ} {A : ℂ[X]}
+    (hn : 1 ≤ n) (hA : A.natDegree ≤ n) :
+    (polarDeriv n ζ A).natDegree ≤ n - 1 := by
+  rw [Polynomial.natDegree_le_iff_degree_le,
+    Polynomial.degree_le_iff_coeff_zero]
+  intro m hm
+  have hm' : n - 1 < m := by exact_mod_cast hm
+  have hnm : n ≤ m := by lia
+  rcases hnm.eq_or_lt with rfl | hlt
+  · have hnext : A.coeff (n + 1) = 0 :=
+      Polynomial.coeff_eq_zero_of_natDegree_lt
+        (lt_of_le_of_lt hA (Nat.lt_succ_self n))
+    unfold polarDeriv
+    rw [sub_mul]
+    simp only [Polynomial.coeff_add, Polynomial.coeff_sub,
+      Polynomial.coeff_C_mul, Polynomial.coeff_derivative, hnext]
+    rw [show n = (n - 1) + 1 by lia, Polynomial.coeff_X_mul,
+      Polynomial.coeff_derivative]
+    norm_num
+    ring
+  · have hm0 : A.coeff m = 0 :=
+      Polynomial.coeff_eq_zero_of_natDegree_lt (lt_of_le_of_lt hA hlt)
+    have hm1 : A.coeff (m + 1) = 0 :=
+      Polynomial.coeff_eq_zero_of_natDegree_lt
+        (lt_of_le_of_lt hA (hlt.trans (Nat.lt_succ_self m)))
+    unfold polarDeriv
+    rw [sub_mul]
+    simp only [Polynomial.coeff_add, Polynomial.coeff_sub,
+      Polynomial.coeff_C_mul, Polynomial.coeff_derivative, hm0, hm1]
+    rw [show m = (m - 1) + 1 by lia, Polynomial.coeff_X_mul,
+      Polynomial.coeff_derivative]
+    rw [show m - 1 + 1 = m by lia, hm0]
+    simp
+
 /-- The coefficient shift dual to the polar derivative:
 `(polarShift ζ f).coeff k = f.coeff k + ζ * f.coeff (k + 1)`. -/
 def polarShift (ζ : ℂ) (f : ℂ[X]) : ℂ[X] := f + C ζ * divX f

RealRooted/BivariateOpenMapping.lean

@@ -0,0 +1,59 @@
+import RealRooted.Mathlib.Analysis.Complex.OpenMapping
+import RealRooted.PartialSymmetrization
+
+/-!
+# Open mapping for bivariate multiaffine quotients
+
+This file supplies the local nonconstancy input for the open-mapping step in
+Borcea--Brändén, Part II, Lemma 1.4.
+-/
+
+open Filter Metric Set
+open scoped Topology
+
+namespace RealRooted
+
+/-- A nonzero cross determinant makes the bivariate quotient injective wherever
+both denominators are nonzero. -/
+theorem bivariateQuotient_ne_of_ne
+    (a b c d z t : ℂ) (hcross : a * d ≠ b * c)
+    (hdenz : c + d * z ≠ 0) (hdent : c + d * t ≠ 0) (hzt : z ≠ t) :
+    (a + b * z) / (c + d * z) ≠
+      (a + b * t) / (c + d * t) := by
+  intro heq
+  have hmul := (div_eq_div_iff hdenz hdent).mp heq
+  have hzero : (a * d - b * c) * (t - z) = 0 := by
+    linear_combination hmul
+  exact (mul_ne_zero (sub_ne_zero.mpr hcross)
+    (sub_ne_zero.mpr hzt.symm)) hzero
+
+/-- Under the denominator half-plane hypothesis, a nonzero cross determinant
+rules out local eventual constancy of the bivariate quotient. -/
+theorem bivariateQuotient_not_eventually_constant
+    (a b c d z : ℂ) (hcross : a * d ≠ b * c)
+    (hcd : 0 < (c / d).im) (hz : 0 < z.im) :
+    ¬∀ᶠ t in 𝓝 z,
+      (a + b * t) / (c + d * t) = (a + b * z) / (c + d * z) := by
+  intro hconst
+  obtain ⟨ε, hε, hball⟩ := Metric.mem_nhds_iff.mp hconst
+  let t : ℂ := z + (ε / 2 : ℝ)
+  have htball : t ∈ ball z ε := by
+    rw [mem_ball]
+    simp [t, Real.norm_eq_abs, abs_of_pos hε]
+    linarith
+  have heq := hball htball
+  have htne : z ≠ t := by
+    intro heq'
+    have hre := congrArg Complex.re heq'
+    simp [t] at hre
+    linarith
+  change (a + b * t) / (c + d * t) =
+    (a + b * z) / (c + d * z) at heq
+  have hdent : c + d * t ≠ 0 :=
+    add_mul_ne_zero_of_im_div_pos c d t hcd (by
+      simpa only [t, Complex.add_im, Complex.ofReal_im, add_zero] using le_of_lt hz)
+  exact bivariateQuotient_ne_of_ne a b c d z t hcross
+    (add_mul_ne_zero_of_im_div_pos c d z hcd (le_of_lt hz))
+    hdent htne heq.symm
+
+end RealRooted

RealRooted/BorceaBranden/Applications/BidiagonalSymbol.lean

@@ -1,4 +1,5 @@
 import RealRooted.BorceaBranden.Applications.UnivariateSymbol
+import RealRooted.BorceaBranden.Applications.DegreeBoxPolarization
 import RealRooted.MultiplierSequence
 
 /-!
@@ -46,4 +47,236 @@ theorem finiteAlgebraicSymbol_bidiagonalLinearMap (alpha beta : ℕ → ℝ) (d
   simp [bidiagonalLinearMap, Polynomial.X_pow_eq_monomial, diagonalOperator_monomial,
     Challenges.BorceaBranden.polynomialInFirstMv]
 
+/-! ## Complex degree-box application -/
+
+/-- Coefficientwise complex diagonal operator. -/
+def complexDiagonalOperator (gamma : ℕ → ℂ) (p : ℂ[X]) : ℂ[X] :=
+  p.sum fun n a => Polynomial.monomial n (gamma n * a)
+
+@[simp] theorem coeff_complexDiagonalOperator
+    (gamma : ℕ → ℂ) (p : ℂ[X]) (n : ℕ) :
+    (complexDiagonalOperator gamma p).coeff n = gamma n * p.coeff n := by
+  classical
+  rw [complexDiagonalOperator, Polynomial.coeff_sum]
+  simp only [Polynomial.coeff_monomial]
+  rw [Polynomial.sum_def]
+  simp_all
+
+theorem complexDiagonalOperator_add (gamma : ℕ → ℂ) (p q : ℂ[X]) :
+    complexDiagonalOperator gamma (p + q) =
+      complexDiagonalOperator gamma p + complexDiagonalOperator gamma q := by
+  ext n
+  simp [mul_add]
+
+theorem complexDiagonalOperator_C_mul
+    (gamma : ℕ → ℂ) (a : ℂ) (p : ℂ[X]) :
+    complexDiagonalOperator gamma (C a * p) =
+      C a * complexDiagonalOperator gamma p := by
+  ext n
+  simp [mul_comm, mul_left_comm]
+
+theorem complexDiagonalOperator_monomial
+    (gamma : ℕ → ℂ) (n : ℕ) (a : ℂ) :
+    complexDiagonalOperator gamma (Polynomial.monomial n a) =
+      Polynomial.monomial n (gamma n * a) := by
+  ext k
+  by_cases hk : k = n
+  · simp_all
+  · simp [Polynomial.coeff_monomial, Ne.symm hk]
+
+/-- Complex-linear extension of the real bidiagonal operator. -/
+def complexBidiagonalLinearMap (alpha beta : ℕ → ℝ) :
+    Polynomial ℂ →ₗ[ℂ] Polynomial ℂ where
+  toFun := fun p =>
+    complexDiagonalOperator (fun k => (alpha k : ℂ)) p +
+      Polynomial.X * complexDiagonalOperator (fun k => (beta k : ℂ)) p
+  map_add' p q := by
+    simp only [complexDiagonalOperator_add, mul_add]
+    abel
+  map_smul' c p := by
+    simp only [smul_eq_C_mul, complexDiagonalOperator_C_mul]
+    simp only [RingHom.id_apply]
+    ring
+
+/-- Regard a complex univariate polynomial as a bivariate polynomial in the
+first variable. -/
+def complexPolynomialInFirstMv (p : ℂ[X]) : MvPolynomial (Fin 2) ℂ :=
+  p.eval₂ (MvPolynomial.C : ℂ →+* MvPolynomial (Fin 2) ℂ)
+    (MvPolynomial.X (0 : Fin 2))
+
+/-- Complex finite algebraic symbol of a complex-linear univariate operator. -/
+def complexFiniteAlgebraicSymbol (d : ℕ) (T : ℂ[X] →ₗ[ℂ] ℂ[X]) :
+    MvPolynomial (Fin 2) ℂ :=
+  ∑ k ∈ Finset.range (d + 1),
+    MvPolynomial.C (Nat.choose d k : ℂ) *
+      complexPolynomialInFirstMv (T ((X : ℂ[X]) ^ k)) *
+        MvPolynomial.X (1 : Fin 2) ^ (d - k)
+
+/-- Restrict a complex univariate operator to the degree-`d` box. -/
+def complexUnivariateDegreeBoxOperator (d : ℕ)
+    (T : ℂ[X] →ₗ[ℂ] ℂ[X]) :
+    MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => d) →ₗ[ℂ]
+      MvPolynomial (Fin 1) ℂ where
+  toFun p :=
+    (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm
+      (T (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) p.1))
+  map_add' p q := by simp
+  map_smul' c p := by simp
+
+lemma rename_uniqueAlgEquiv_symm_eq_complexPolynomialInFirstMv (p : ℂ[X]) :
+    MvPolynomial.rename finOneSumToFinTwo
+        (MvPolynomial.rename (Sum.inl : Fin 1 → Fin 1 ⊕ Fin 1)
+          ((MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm p)) =
+      complexPolynomialInFirstMv p := by
+  induction p using Polynomial.induction_on' with
+  | add p q hp hq =>
+      simpa only [map_add, complexPolynomialInFirstMv, Polynomial.eval₂_add] using
+        congrArg₂ (· + ·) hp hq
+  | monomial n a =>
+      have h := MvPolynomial.uniqueAlgEquiv_symm_monomial
+        (R := ℂ) (σ := Fin 1) (d := Finsupp.single 0 n) (r := a)
+      rw [show (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm
+        (Polynomial.monomial n a) =
+          MvPolynomial.monomial (Finsupp.single 0 n) a by simpa using h]
+      simp [complexPolynomialInFirstMv, finOneSumToFinTwo,
+        MvPolynomial.monomial_eq]
+
+lemma rename_rightComplementMonomial_finOne_complex (d : ℕ)
+    (m : Fin 1 →₀ ℕ) :
+    MvPolynomial.rename finOneSumToFinTwo
+        (MvPolynomial.rightComplementMonomial
+          (R := ℂ) (τ := Fin 1) (fun _ : Fin 1 => d) m) =
+      MvPolynomial.X (1 : Fin 2) ^ (d - m 0) := by
+  simp [MvPolynomial.rightComplementMonomial, finOneSumToFinTwo]
+
+lemma complexUnivariateDegreeBoxOperator_basis (d : ℕ)
+    (T : ℂ[X] →ₗ[ℂ] ℂ[X])
+    (m : {m : Fin 1 →₀ ℕ // ∀ i, m i ≤ d}) :
+    complexUnivariateDegreeBoxOperator d T
+      (MvPolynomial.basisDegreeOfLE (R := ℂ) (fun _ : Fin 1 => d) m) =
+      (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm
+        (T (Polynomial.X ^ m.1 0)) := by
+  change (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm
+      (T (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)
+        ((MvPolynomial.basisDegreeOfLE (R := ℂ) (fun _ : Fin 1 => d) m :
+          MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => d)) :
+            MvPolynomial (Fin 1) ℂ))) = _
+  rw [MvPolynomial.coe_basisDegreeOfLE,
+    MvPolynomial.uniqueAlgEquiv_monomial]
+  simp [Polynomial.X_pow_eq_monomial]
+
+/-- The genuine algebraic symbol of a complex univariate degree-box operator
+is its usual finite algebraic symbol after identifying the two singleton
+variable blocks with `Fin 2`. -/
+theorem rename_algebraicSymbol_complexUnivariateDegreeBoxOperator
+    (d : ℕ) (T : ℂ[X] →ₗ[ℂ] ℂ[X]) :
+    MvPolynomial.rename finOneSumToFinTwo
+        (MvPolynomial.algebraicSymbol (fun _ : Fin 1 => d)
+          (complexUnivariateDegreeBoxOperator d T)) =
+      complexFiniteAlgebraicSymbol d T := by
+  classical
+  rw [MvPolynomial.algebraicSymbol, map_sum]
+  let g : ℕ → MvPolynomial (Fin 2) ℂ := fun k =>
+    MvPolynomial.C (Nat.choose d k : ℂ) *
+      complexPolynomialInFirstMv (T (Polynomial.X ^ k)) *
+        MvPolynomial.X 1 ^ (d - k)
+  calc
+    ∑ m : {m : Fin 1 →₀ ℕ // ∀ i, m i ≤ d},
+        MvPolynomial.rename finOneSumToFinTwo
+          (MvPolynomial.C
+              (MvPolynomial.boxChoose (fun _ : Fin 1 => d) m.1 : ℂ) *
+            MvPolynomial.rename (Sum.inl : Fin 1 → Fin 1 ⊕ Fin 1)
+              (complexUnivariateDegreeBoxOperator d T
+                (MvPolynomial.basisDegreeOfLE
+                  (R := ℂ) (fun _ : Fin 1 => d) m)) *
+            MvPolynomial.rightComplementMonomial
+              (R := ℂ) (τ := Fin 1) (fun _ : Fin 1 => d) m.1) =
+      ∑ m : {m : Fin 1 →₀ ℕ // ∀ i, m i ≤ d}, g (m.1 0) := by
+        apply Fintype.sum_congr
+        intro m
+        simp only [map_mul, MvPolynomial.rename_C]
+        rw [complexUnivariateDegreeBoxOperator_basis,
+          rename_uniqueAlgEquiv_symm_eq_complexPolynomialInFirstMv,
+          rename_rightComplementMonomial_finOne_complex]
+        simp [g, MvPolynomial.boxChoose]
+    _ = ∑ k : Fin (d + 1), g k := by
+      apply Fintype.sum_equiv (degreeOfLEFinOneEquiv d)
+      intro m
+      simp [g, degreeOfLEFinOneEquiv_val]
+    _ = complexFiniteAlgebraicSymbol d T := by
+      simpa [g, complexFiniteAlgebraicSymbol] using
+        Fin.sum_univ_eq_sum_range g (d + 1)
+
+/-- The complex finite symbol of the complexified bidiagonal operator is the
+coefficientwise complexification of the already computed real affine symbol. -/
+theorem complexFiniteAlgebraicSymbol_complexBidiagonalLinearMap
+    (alpha beta : ℕ → ℝ) (d : ℕ) :
+    complexFiniteAlgebraicSymbol d (complexBidiagonalLinearMap alpha beta) =
+      complexifyMv
+        (Challenges.BorceaBranden.finiteAlgebraicSymbol d
+          (bidiagonalLinearMap alpha beta)) := by
+  classical
+  rw [finiteAlgebraicSymbol_bidiagonalLinearMap]
+  simp only [complexFiniteAlgebraicSymbol, affineBidiagonalSymbol,
+    complexifyMv, map_sum]
+  apply Finset.sum_congr rfl
+  intro k _
+  simp [complexPolynomialInFirstMv, complexBidiagonalLinearMap,
+    Polynomial.X_pow_eq_monomial, complexDiagonalOperator_monomial, pow_succ]
+
+/-- Identify the left and right singleton blocks with variables `0` and `1`. -/
+def finOneSumEquivFinTwo : Fin 1 ⊕ Fin 1 ≃ Fin 2 where
+  toFun := finOneSumToFinTwo
+  invFun := Fin.cases (Sum.inl 0) (fun _ => Sum.inr 0)
+  left_inv i := by
+    rcases i with i | i
+    · rw [Subsingleton.elim i 0]
+      rfl
+    · rw [Subsingleton.elim i 0]
+      rfl
+  right_inv i := by
+    fin_cases i <;> rfl
+
+/-- Borcea--Branden, Theorem 1.1, symbol identification for the complexified
+bidiagonal operator. The equality uses the affine, not homogeneous, finite
+symbol computed by `finiteAlgebraicSymbol_bidiagonalLinearMap`. -/
+theorem algebraicSymbol_complexBidiagonalDegreeBoxOperator
+    (alpha beta : ℕ → ℝ) (d : ℕ) :
+    MvPolynomial.algebraicSymbol (fun _ : Fin 1 => d)
+        (complexUnivariateDegreeBoxOperator d
+          (complexBidiagonalLinearMap alpha beta)) =
+      MvPolynomial.rename finOneSumEquivFinTwo.symm
+        (complexifyMv
+          (Challenges.BorceaBranden.finiteAlgebraicSymbol d
+            (bidiagonalLinearMap alpha beta))) := by
+  have h := congrArg (MvPolynomial.rename finOneSumEquivFinTwo.symm)
+    (rename_algebraicSymbol_complexUnivariateDegreeBoxOperator d
+      (complexBidiagonalLinearMap alpha beta))
+  rw [complexFiniteAlgebraicSymbol_complexBidiagonalLinearMap] at h
+  have hcomp : finOneSumEquivFinTwo.symm ∘ finOneSumToFinTwo = id := by
+    funext i
+    exact finOneSumEquivFinTwo.symm_apply_apply i
+  rw [MvPolynomial.rename_rename, hcomp, MvPolynomial.rename_id] at h
+  exact h
+
+/-- Explicit bidiagonal application of finite degree-box symbol sufficiency.
+
+This is exactly the sufficiency implication in Borcea--Branden, Theorem 1.1,
+after equations (2.1)--(2.2). The symbol hypothesis is genuine bivariate
+upper-half-plane stability; no Jensen-pencil or PF conclusion is assumed. -/
+theorem complexBidiagonalDegreeBox_preserves_stability
+    (alpha beta : ℕ → ℝ) (d : ℕ)
+    (hSymbol : MvUpperHalfPlaneStable
+      (complexifyMv
+        (Challenges.BorceaBranden.finiteAlgebraicSymbol d
+          (bidiagonalLinearMap alpha beta))))
+    (f : MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => d))
+    (hf : MvUpperHalfPlaneStable f.1) :
+    MvUpperHalfPlaneStableOrZero
+      (complexUnivariateDegreeBoxOperator d
+        (complexBidiagonalLinearMap alpha beta) f) := by
+  apply finiteSymbol_finOne_preserves_stability d _ ?_ f hf
+  rw [algebraicSymbol_complexBidiagonalDegreeBoxOperator]
+  exact hSymbol.rename
+
 end RealRooted.BorceaBranden