diff --git a/RealRooted.lean b/RealRooted.lean index c2f7bfc3b..6b02de2d0 100644 --- a/RealRooted.lean +++ b/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 diff --git a/RealRooted/Apolarity.lean b/RealRooted/Apolarity.lean index 0de1aea82..46dc2a322 100644 --- a/RealRooted/Apolarity.lean +++ b/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 diff --git a/RealRooted/BivariateOpenMapping.lean b/RealRooted/BivariateOpenMapping.lean new file mode 100644 index 000000000..d1a2271ca --- /dev/null +++ b/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 diff --git a/RealRooted/BorceaBranden/Applications/BidiagonalSymbol.lean b/RealRooted/BorceaBranden/Applications/BidiagonalSymbol.lean index 201c2eeff..31d5c5f39 100644 --- a/RealRooted/BorceaBranden/Applications/BidiagonalSymbol.lean +++ b/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 diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean new file mode 100644 index 000000000..14ff04e65 --- /dev/null +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -0,0 +1,717 @@ +import RealRooted.BorceaBranden.FiniteSymbolBasis +import RealRooted.BorceaBranden.FiniteSymbolDegree +import RealRooted.BorceaBranden.FiniteSymbolPreserver +import RealRooted.Polarization + +/-! +# Source polarization for degree-box operators + +This file implements the source-side operator lift from Borcea--Brändén, +equation (2.2), for a one-variable degree-`n` source box. The lift first +diagonalizes a multiaffine input and then applies the original operator. +-/ + +namespace RealRooted.BorceaBranden + +noncomputable section + +/-- Lift an operator with a one-variable degree-`n` source to a multiaffine +`Fin n` source by precomposing with diagonal projection. -/ +def sourcePolarizedOperator {τ : Type*} (n : ℕ) + (T : MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] + MvPolynomial τ ℂ) : + MvPolynomial.degreeOfLE (Fin n) ℂ (fun _ => 1) →ₗ[ℂ] + MvPolynomial τ ℂ := + T.comp (diagonalProjectionDegreeBox n) + +/-- Source-side equation (2.2): restricting the lifted operator along source +polarization reconstructs the original operator. -/ +theorem sourcePolarizedOperator_comp_polarizationDegreeBoxLinearMap + {τ : Type*} {n : ℕ} + (T : MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] + MvPolynomial τ ℂ) : + (sourcePolarizedOperator n T).comp + (polarizationDegreeBoxLinearMap n) = T := by + apply LinearMap.ext + intro q + change T (diagonalProjectionDegreeBox n + (polarizationDegreeBoxLinearMap n q)) = T q + rw [diagonalProjectionDegreeBox_comp_polarizationDegreeBoxLinearMap q] + +/-- The source-polarized operator sends a multiaffine basis monomial to the +original operator applied to the one-variable basis monomial of the same total +degree. This is the basis-level content of Borcea--Branden Lemma 2.5. -/ +theorem sourcePolarizedOperator_basisDegreeOfLE + {τ : Type*} {n : ℕ} + (T : MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] + MvPolynomial τ ℂ) + (m : {m : Fin n →₀ ℕ // ∀ i, m i ≤ 1}) : + sourcePolarizedOperator n T + (MvPolynomial.basisDegreeOfLE (R := ℂ) (fun _ : Fin n => 1) m) = + T (MvPolynomial.basisDegreeOfLE (R := ℂ) (fun _ : Fin 1 => n) + (diagonalDegreeBoxIndex m)) := by + change T (diagonalProjectionDegreeBox n + (MvPolynomial.basisDegreeOfLE (R := ℂ) (fun _ : Fin n => 1) m)) = _ + rw [diagonalProjectionDegreeBox_basisDegreeOfLE] + +/-- Reindex a sum over multiaffine exponent vectors by their finite supports. +This is the subset reindexing in the source-side proof of Lemma 2.5. -/ +theorem sum_degreeOneExponent_eq_sum_finset + {M : Type*} [AddCommMonoid M] {n : ℕ} + (f : {m : Fin n →₀ ℕ // ∀ i, m i ≤ 1} → M) : + ∑ m, f m = + ∑ s : Finset (Fin n), + f ((degreeOneExponentEquivFinset (Fin n)).symm s) := by + apply Fintype.sum_equiv (degreeOneExponentEquivFinset (Fin n)) + intro m + simp + +/-- Partition a sum over subsets of `Fin n` by subset cardinality. -/ +theorem sum_finset_eq_sum_powersetCard + {M : Type*} [AddCommMonoid M] (n : ℕ) + (f : Finset (Fin n) → M) : + ∑ s, f s = + ∑ k ∈ Finset.range (n + 1), + ∑ s ∈ (Finset.univ : Finset (Fin n)).powersetCard k, f s := by + simpa using + Finset.sum_powerset (Finset.univ : Finset (Fin n)) f + +/-- Summing a cardinality-dependent contribution over subsets of `Fin n` +produces the corresponding binomial coefficients. -/ +theorem sum_finset_cardFunction + {M : Type*} [AddCommMonoid M] (n : ℕ) (g : ℕ → M) : + ∑ s : Finset (Fin n), g s.card = + ∑ k ∈ Finset.range (n + 1), n.choose k • g k := by + rw [sum_finset_eq_sum_powersetCard] + apply Finset.sum_congr rfl + intro k hk + simpa using + Finset.sum_powersetCard k (Finset.univ : Finset (Fin n)) g + +/-- The coefficient grouping for multiaffine source exponents: one term for +each zero-one exponent vector becomes `choose n k` copies of the contribution +of total degree `k`. -/ +theorem sum_degreeOneExponent_degreeFunction + {M : Type*} [AddCommMonoid M] (n : ℕ) (g : ℕ → M) : + ∑ m : {m : Fin n →₀ ℕ // ∀ i, m i ≤ 1}, g m.1.degree = + ∑ k ∈ Finset.range (n + 1), n.choose k • g k := by + rw [sum_degreeOneExponent_eq_sum_finset] + simpa using sum_finset_cardFunction n g + +end + +end RealRooted.BorceaBranden + +namespace MvPolynomial + +/-- The coefficient of source degree `k`, after viewing a polynomial in +`tau ⊕ Fin 1` as a polynomial in the single source variable with coefficients +in the output-variable ring `MvPolynomial tau ℂ`. -/ +/- Source audit: Borcea--Branden, "The Lee--Yang and Polya--Schur Programs. I", +Proposition 2.4, equation (2.2), and Lemma 2.5. This extracts the coefficient +of the source monomial `z^k` while retaining the output-variable polynomial. -/ +noncomputable def sourceCoefficient {τ : Type*} + (P : MvPolynomial (τ ⊕ Fin 1) ℂ) (k : ℕ) : MvPolynomial τ ℂ := + (sumAlgEquiv ℂ (Fin 1) τ + (rename (Equiv.sumComm τ (Fin 1)) P)).coeff + (Finsupp.single default k) + +/-- Polarize only the single source variable of a polynomial whose output +variables are indexed by `τ`. + +This is the one-source-coordinate instance of Borcea--Brändén's operator +`Π↑` from Proposition 2.4 and Lemma 2.5: the source coefficient of degree `k` +is divided by `choose n k`, and the source monomial is replaced by the +elementary symmetric polynomial `e_k` in the `Fin n` source block. -/ +/- This is exactly the paper's source polarization `Pi^up`: the coefficient of +`z^k` is divided by `choose n k` and `z^k` is replaced by the elementary +symmetric polynomial `e_k` in the new source block. -/ +noncomputable def sourceBlockPolarization {τ : Type*} (n : ℕ) + (P : MvPolynomial (τ ⊕ Fin 1) ℂ) : + MvPolynomial (τ ⊕ Fin n) ℂ := + ∑ k ∈ Finset.range (n + 1), + C ((n.choose k : ℂ)⁻¹) * + rename Sum.inl (sourceCoefficient P k) * + rename Sum.inr (esymm (Fin n) ℂ k) + +private theorem + coeff_uniqueAlgEquiv_specializeLeft_eq_eval_sourceCoefficient + {τ : Type*} (P : MvPolynomial (τ ⊕ Fin 1) ℂ) + (x : τ → ℂ) (k : ℕ) : + ((MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)) + (_root_.RealRooted.specializeLeft x P)).coeff k = + MvPolynomial.eval x (sourceCoefficient P k) := by + have hspecial : + _root_.RealRooted.specializeLeft x P = + MvPolynomial.map (MvPolynomial.eval x) + (sumAlgEquiv ℂ (Fin 1) τ + (rename (Equiv.sumComm τ (Fin 1)) P)) := by + unfold _root_.RealRooted.specializeLeft + change + (MvPolynomial.aeval + (Sum.elim (MvPolynomial.C ∘ x) MvPolynomial.X)) P = + ((MvPolynomial.mapAlgHom (MvPolynomial.aeval x)).comp + ((sumAlgEquiv ℂ (Fin 1) τ).toAlgHom.comp + (rename (Equiv.sumComm τ (Fin 1))))) P + congr 1 + apply MvPolynomial.algHom_ext + rintro (i | i) <;> + simp [Function.comp_def, Equiv.sumComm_apply] + rw [MvPolynomial.coeff_uniqueAlgEquiv, hspecial, + MvPolynomial.coeff_map] + change + MvPolynomial.eval x + ((sumAlgEquiv ℂ (Fin 1) τ + (rename (Equiv.sumComm τ (Fin 1)) P)).coeff + (Finsupp.single default k)) = + MvPolynomial.eval x (sourceCoefficient P k) + rfl + +/- Borcea--Branden, arXiv:0809.0401, Proposition 2.4 and equation (2.2). +Specializing the output block commutes with source polarization. The ambient +degree cap remains `n`, even when specialization lowers the source degree. -/ +theorem specializeLeft_sourceBlockPolarization + {τ : Type*} (n : ℕ) (P : MvPolynomial (τ ⊕ Fin 1) ℂ) + (x : τ → ℂ) : + _root_.RealRooted.specializeLeft x + (sourceBlockPolarization n P) = + _root_.RealRooted.polarization n + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) + (_root_.RealRooted.specializeLeft x P)) := by + let p : Polynomial ℂ := + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)) + (_root_.RealRooted.specializeLeft x P) + have hpcoeff (k : ℕ) : + p.coeff k = MvPolynomial.eval x (sourceCoefficient P k) := + coeff_uniqueAlgEquiv_specializeLeft_eq_eval_sourceCoefficient P x k + have houtput (q : MvPolynomial τ ℂ) : + MvPolynomial.aeval + (Sum.elim (MvPolynomial.C ∘ x) MvPolynomial.X) + (rename (Sum.inl : τ → τ ⊕ Fin n) q) = + C (MvPolynomial.eval x q) := by + rw [MvPolynomial.aeval_rename] + change + MvPolynomial.aeval (MvPolynomial.C ∘ x) q = + C (MvPolynomial.eval x q) + induction q using MvPolynomial.induction_on with + | C c => simp + | add q r hq hr => + rw [map_add, hq, hr, map_add] + exact (map_add MvPolynomial.C _ _).symm + | mul_X q i hq => + rw [map_mul, MvPolynomial.aeval_X, hq, map_mul, + MvPolynomial.eval_X] + simpa only [Function.comp_apply] using + (map_mul MvPolynomial.C (MvPolynomial.eval x q) (x i)).symm + have hsource (q : MvPolynomial (Fin n) ℂ) : + MvPolynomial.aeval + (Sum.elim (MvPolynomial.C ∘ x) MvPolynomial.X) + (rename (Sum.inr : Fin n → τ ⊕ Fin n) q) = + q := by + rw [MvPolynomial.aeval_rename] + change MvPolynomial.aeval MvPolynomial.X q = q + exact MvPolynomial.aeval_X_left_apply q + change + _root_.RealRooted.specializeLeft x + (sourceBlockPolarization n P) = + _root_.RealRooted.polarization n p + unfold sourceBlockPolarization _root_.RealRooted.specializeLeft + rw [map_sum] + unfold _root_.RealRooted.polarization + _root_.RealRooted.reducedPolarization + apply Finset.sum_congr rfl + intro k hk + rw [map_mul, map_mul, MvPolynomial.aeval_C, + MvPolynomial.algebraMap_eq, houtput, hsource] + have hbinom : + (_root_.RealRooted.binomialUnlift n p).coeff k = + p.coeff k / (n.choose k : ℂ) := by + unfold _root_.RealRooted.binomialUnlift + rw [Polynomial.finsetSum_coeff, Finset.sum_eq_single k] + · simp only [Polynomial.coeff_monomial_same] + · intro j hj hjk + simp [Polynomial.coeff_monomial, hjk] + · intro hknot + exact (hknot hk).elim + rw [hbinom, hpcoeff] + simp only [div_eq_mul_inv, map_mul] + ring + +/- Borcea--Branden, arXiv:0809.0401, Proposition 2.4. Apply upper-half-plane +polarization stability fiberwise after specializing the output block. The +ambient source-degree cap remains `n` after specialization. -/ +theorem mvUpperHalfPlaneStable_sourceBlockPolarization + {τ : Type*} {n : ℕ} + {P : MvPolynomial (τ ⊕ Fin 1) ℂ} + (hdeg : P.degreeOf (Sum.inr default) ≤ n) + (hstable : _root_.RealRooted.MvUpperHalfPlaneStable P) : + _root_.RealRooted.MvUpperHalfPlaneStable + (sourceBlockPolarization n P) := by + intro z hz + let x : τ → ℂ := fun i => z (Sum.inl i) + let y : Fin n → ℂ := fun i => z (Sum.inr i) + let p : Polynomial ℂ := + MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) + (_root_.RealRooted.specializeLeft x P) + have hx : ∀ i, 0 < (x i).im := + fun i => hz (Sum.inl i) + have hy : ∀ i, 0 < (y i).im := + fun i => hz (Sum.inr i) + have hpdeg : p.natDegree ≤ n := by + exact + (_root_.RealRooted.natDegree_uniqueAlgEquiv_specializeLeft_le_degreeOf + x P).trans hdeg + have hspecial : + _root_.RealRooted.MvUpperHalfPlaneStable + (_root_.RealRooted.specializeLeft x P) := + hstable.specializeLeft hx + have hpstable : + ∀ w : ℂ, 0 < w.im → p.eval w ≠ 0 := by + intro w hw + change + Polynomial.eval₂ (RingHom.id ℂ) w + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) + (_root_.RealRooted.specializeLeft x P)) ≠ 0 + rw [MvPolynomial.eval₂_const_uniqueAlgEquiv] + exact hspecial (fun _ => w) (fun _ => hw) + have hpolar : + _root_.RealRooted.MvUpperHalfPlaneStable + (_root_.RealRooted.polarization n p) := + _root_.RealRooted.mvUpperHalfPlaneStable_polarization + hpdeg hpstable + have hfiber : + _root_.RealRooted.MvUpperHalfPlaneStable + (_root_.RealRooted.specializeLeft x + (sourceBlockPolarization n P)) := by + rw [specializeLeft_sourceBlockPolarization] + exact hpolar + have hnonzero := hfiber y hy + rw [_root_.RealRooted.eval_specializeLeft] at hnonzero + have hxy : Sum.elim x y = z := by + funext i + cases i <;> rfl + simpa only [hxy] using hnonzero + +/-- Extracting a source coefficient commutes with a finite sum. -/ +theorem sourceCoefficient_sum {τ ι : Type*} (s : Finset ι) + (f : ι → MvPolynomial (τ ⊕ Fin 1) ℂ) (k : ℕ) : + sourceCoefficient (∑ i ∈ s, f i) k = + ∑ i ∈ s, sourceCoefficient (f i) k := by + simp [sourceCoefficient, map_sum, coeff_sum] + +/-- Extract the source coefficient of an output polynomial times one source +monomial. -/ +theorem sourceCoefficient_rename_mul_X_pow {τ : Type*} + (q : MvPolynomial τ ℂ) (r k : ℕ) : + sourceCoefficient + (rename (Sum.inl : τ → τ ⊕ Fin 1) q * + X (Sum.inr default) ^ r) k = + if k = r then q else 0 := by + have hpoly : + (sumAlgEquiv ℂ (Fin 1) τ) + (rename (Equiv.sumComm τ (Fin 1)) + (rename (Sum.inl : τ → τ ⊕ Fin 1) q * + X (Sum.inr default) ^ r)) = + C q * X default ^ r := by + simp only [map_mul, map_pow, rename_X, rename_rename, + Equiv.sumComm_apply] + change (sumAlgEquiv ℂ (Fin 1) τ) + (rename (Sum.inr : τ → Fin 1 ⊕ τ) q) * + (sumAlgEquiv ℂ (Fin 1) τ) (X (Sum.inl default)) ^ r = + C q * X default ^ r + rw [show (sumAlgEquiv ℂ (Fin 1) τ) + (rename (Sum.inr : τ → Fin 1 ⊕ τ) q) = C q by + simpa using DFunLike.congr_fun + (sumAlgEquiv_comp_rename_inr ℂ (Fin 1) τ) q] + simp + unfold sourceCoefficient + rw [hpoly, coeff_C_mul, coeff_X_pow] + simp [eq_comm] + +/-- Extract the source coefficient when the output coefficient has an +additional scalar factor. -/ +theorem sourceCoefficient_C_mul_rename_mul_X_pow {τ : Type*} + (a : ℂ) (q : MvPolynomial τ ℂ) (r k : ℕ) : + sourceCoefficient + (C a * rename (Sum.inl : τ → τ ⊕ Fin 1) q * + X (Sum.inr default) ^ r) k = + if k = r then C a * q else 0 := by + have hterm : + C a * rename (Sum.inl : τ → τ ⊕ Fin 1) q * + X (Sum.inr default) ^ r = + rename Sum.inl (C a * q) * X (Sum.inr default) ^ r := by + simp + rw [hterm, sourceCoefficient_rename_mul_X_pow] + +/-- In a degree-`n` algebraic-symbol-shaped sum, source degree `r` selects the +unique operator term indexed by `n - r`. -/ +theorem sourceCoefficient_symbol_sum {τ : Type*} (n r : ℕ) + (hr : r ≤ n) (q : ℕ → MvPolynomial τ ℂ) : + sourceCoefficient + (∑ k ∈ Finset.range (n + 1), + C (n.choose k : ℂ) * rename Sum.inl (q k) * + X (Sum.inr default) ^ (n - k)) r = + C (n.choose (n - r) : ℂ) * q (n - r) := by + rw [sourceCoefficient_sum] + rw [Finset.sum_eq_single (n - r)] + · rw [sourceCoefficient_C_mul_rename_mul_X_pow] + simp [Nat.sub_sub_self hr] + · intro k hk hne + rw [sourceCoefficient_C_mul_rename_mul_X_pow] + have hk_le : k ≤ n := Nat.le_of_lt_succ (Finset.mem_range.mp hk) + have hnr : r ≠ n - k := by + intro heq + apply hne + lia + rw [if_neg hnr] + · intro hnot + exact (hnot (Finset.mem_range.mpr + (Nat.lt_succ_of_le (Nat.sub_le n r)))).elim + +/-- Identify all polarized source variables while leaving output variables +unchanged. -/ +def sourceDiagonalVariableMap {τ : Type*} {n : ℕ} : + τ ⊕ Fin n → τ ⊕ Fin 1 + | Sum.inl i => Sum.inl i + | Sum.inr _ => Sum.inr default + +/-- Diagonalizing source variables leaves the output-variable block +unchanged. -/ +@[simp] theorem rename_sourceDiagonalVariableMap_rename_inl + {τ : Type*} {n : ℕ} (p : MvPolynomial τ ℂ) : + rename (sourceDiagonalVariableMap (τ := τ) (n := n)) + (rename (Sum.inl : τ → τ ⊕ Fin n) p) = + rename (Sum.inl : τ → τ ⊕ Fin 1) p := by + rw [rename_rename] + rfl + +/-- Diagonalizing a complementary zero-one source monomial records only its +complementary total degree. -/ +theorem rename_rightComplementMonomial_one + {τ : Type*} {n : ℕ} (m : Fin n →₀ ℕ) + (hm : ∀ i, m i ≤ 1) : + rename (sourceDiagonalVariableMap (τ := τ) (n := n)) + (rightComplementMonomial (R := ℂ) (τ := τ) + (fun _ : Fin n => 1) m) = + X (Sum.inr default) ^ (n - m.degree) := by + rw [rightComplementMonomial_eq_prod] + simp only [map_prod, map_pow, rename_X, sourceDiagonalVariableMap] + rw [Finset.prod_pow_eq_pow_sum] + congr 1 + simpa using Finsupp.sum_one_sub_eq_card_sub_degree m hm + +end MvPolynomial + +namespace RealRooted.BorceaBranden + +noncomputable section + +open _root_.MvPolynomial + +/-- The source-degree coefficient of a one-variable finite algebraic symbol. + +This is the coefficient calculation on the right-hand side of +Borcea--Brändén Lemma 2.5: source degree `r` corresponds to operator degree +`n - r`, with coefficient `choose n (n - r)`. -/ +theorem sourceCoefficient_algebraicSymbol_finOne + {τ : Type*} (n r : ℕ) + (T : degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] + MvPolynomial τ ℂ) + (hr : r ≤ n) : + sourceCoefficient (algebraicSymbol (fun _ : Fin 1 => n) T) r = + C (n.choose (n - r) : ℂ) * + T (basisDegreeOfLE (R := ℂ) (fun _ : Fin 1 => n) + (finOneDegreeIndex n (n - r))) := by + rw [algebraicSymbol_finOne_eq_sum_range] + exact sourceCoefficient_symbol_sum n r hr fun k => + T (basisDegreeOfLE (R := ℂ) (fun _ : Fin 1 => n) + (finOneDegreeIndex n k)) + +lemma finOneDegreeIndex_degree_eq_diagonalDegreeBoxIndex + {n : ℕ} (m : {m : Fin n →₀ ℕ // ∀ i, m i ≤ 1}) : + finOneDegreeIndex n m.1.degree = diagonalDegreeBoxIndex m := by + have hm_degree : m.1.degree ≤ n := by + rw [← card_support_eq_degree_of_le_one m.1 m.2] + simpa using Finset.card_le_univ m.1.support + apply (degreeOfLEFinOneEquiv n).injective + apply Fin.ext + simp [finOneDegreeIndex, degreeOfLEFinOneEquiv_val, + diagonalDegreeBoxIndex, + Nat.min_eq_left hm_degree] + +/-- Summation over finite subsets is invariant under taking complements. -/ +private theorem sum_finset_compl + {M α : Type*} [AddCommMonoid M] [Fintype α] [DecidableEq α] + (f : Finset α → M) : + ∑ s : Finset α, f sᶜ = ∑ s, f s := by + let e : Finset α ≃ Finset α := + { toFun := fun s => sᶜ + invFun := fun s => sᶜ + left_inv := compl_compl + right_inv := compl_compl } + exact e.sum_comp f + +/-- Complement reindexing exchanges a support cardinality with its codimension. -/ +private theorem sum_finset_card_compl + {M : Type*} [AddCommMonoid M] (n : ℕ) + (f : ℕ → Finset (Fin n) → M) : + ∑ s : Finset (Fin n), f s.card sᶜ = + ∑ s, f (n - s.card) s := by + rw [← sum_finset_compl (fun s : Finset (Fin n) => + f (n - s.card) s)] + apply Finset.sum_congr rfl + intro s _ + rw [Finset.card_compl] + simp only [Fintype.card_fin] + have hs : s.card ≤ n := by simpa using Finset.card_le_univ s + rw [Nat.sub_sub_self hs] + +/-- A degree-one exponent's complementary monomial is indexed by the complement +of the corresponding finite support. -/ +@[simp] +private theorem rightComplementMonomial_one_degreeOneExponentEquivFinset_symm + {τ R : Type*} [CommSemiring R] (n : ℕ) (s : Finset (Fin n)) : + rightComplementMonomial (R := R) (τ := τ) (fun _ : Fin n => 1) + ((degreeOneExponentEquivFinset (Fin n)).symm s).1 = + rename (Sum.inr : Fin n → τ ⊕ Fin n) (∏ i ∈ sᶜ, X i) := by + rw [rightComplementMonomial_one_eq_support_compl + ((degreeOneExponentEquivFinset (Fin n)).symm s).1 + ((degreeOneExponentEquivFinset (Fin n)).symm s).2] + have hsupp : + ((degreeOneExponentEquivFinset (Fin n)).symm s).1.support = s := + (degreeOneExponentEquivFinset (Fin n)).apply_symm_apply s + rw [hsupp] + +/-- Grouping squarefree monomials by support cardinality gives `esymm`. -/ +private theorem sum_finset_card_prod_eq_sum_esymm + {τ : Type*} (n : ℕ) (q : ℕ → MvPolynomial τ ℂ) : + (∑ s : Finset (Fin n), + rename (Sum.inl : τ → τ ⊕ Fin n) (q (n - s.card)) * + rename Sum.inr (∏ i ∈ s, X i)) = + ∑ r ∈ Finset.range (n + 1), + rename (Sum.inl : τ → τ ⊕ Fin n) (q (n - r)) * + rename Sum.inr (esymm (Fin n) ℂ r) := by + rw [sum_finset_eq_sum_powersetCard] + apply Finset.sum_congr rfl + intro r _ + rw [esymm, map_sum, Finset.mul_sum] + simp only [map_prod, rename_X] + apply Finset.sum_congr rfl + intro s hs + rw [(Finset.mem_powersetCard.mp hs).2] + +/-- Complementing zero-one exponent supports and grouping by cardinality gives +the elementary-symmetric expansion used in Borcea--Branden, Lemma 2.5. -/ +private theorem sum_degreeOneExponent_rightComplementMonomial_eq_sum_esymm + {τ : Type*} (n : ℕ) (q : ℕ → MvPolynomial τ ℂ) : + (∑ m : {m : Fin n →₀ ℕ // ∀ i, m i ≤ 1}, + rename (Sum.inl : τ → τ ⊕ Fin n) (q m.1.degree) * + rightComplementMonomial (R := ℂ) (τ := τ) + (fun _ : Fin n => 1) m.1) = + ∑ r ∈ Finset.range (n + 1), + rename (Sum.inl : τ → τ ⊕ Fin n) (q (n - r)) * + rename Sum.inr (esymm (Fin n) ℂ r) := by + rw [sum_degreeOneExponent_eq_sum_finset] + simp only [degree_degreeOneExponentEquivFinset_symm, + rightComplementMonomial_one_degreeOneExponentEquivFinset_symm] + rw [sum_finset_card_compl n (fun k s => + rename (Sum.inl : τ → τ ⊕ Fin n) (q k) * + rename Sum.inr (∏ i ∈ s, X i))] + exact sum_finset_card_prod_eq_sum_esymm n q + +/-- The multiaffine symbol of the lifted operator before source diagonalization. +This is the left-hand expansion in Borcea--Branden, Lemma 2.5. -/ +theorem algebraicSymbol_sourcePolarizedOperator_eq_sum + {τ : Type*} (n : ℕ) + (T : degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] + MvPolynomial τ ℂ) : + algebraicSymbol (fun _ : Fin n => 1) + (sourcePolarizedOperator n T) = + ∑ m : {m : Fin n →₀ ℕ // ∀ i, m i ≤ 1}, + rename (Sum.inl : τ → τ ⊕ Fin n) + (T (basisDegreeOfLE (R := ℂ) (fun _ : Fin 1 => n) + (diagonalDegreeBoxIndex m))) * + rightComplementMonomial (R := ℂ) (τ := τ) + (fun _ : Fin n => 1) m.1 := by + rw [algebraicSymbol_eq_sum] + apply Finset.sum_congr rfl + intro m _ + rw [boxChoose_one_of_le_one m.1 m.2, + sourcePolarizedOperator_basisDegreeOfLE] + simp + +/-- Expanding the paper's `Pi^up` on the one-variable symbol cancels the +binomial coefficient and replaces each source monomial by `e_r`. -/ +theorem sourceBlockPolarization_algebraicSymbol_finOne_eq_sum + {τ : Type*} (n : ℕ) + (T : degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] + MvPolynomial τ ℂ) : + sourceBlockPolarization n + (algebraicSymbol (fun _ : Fin 1 => n) T) = + ∑ r ∈ Finset.range (n + 1), + rename (Sum.inl : τ → τ ⊕ Fin n) + (T (basisDegreeOfLE (R := ℂ) (fun _ : Fin 1 => n) + (finOneDegreeIndex n (n - r)))) * + rename Sum.inr (esymm (Fin n) ℂ r) := by + unfold sourceBlockPolarization + apply Finset.sum_congr rfl + intro r hr + have hr_le : r ≤ n := Nat.le_of_lt_succ (Finset.mem_range.mp hr) + rw [sourceCoefficient_algebraicSymbol_finOne n r T hr_le] + rw [Nat.choose_symm hr_le] + have hchoose : n.choose r ≠ 0 := (Nat.choose_pos hr_le).ne' + rw [map_mul] + simp only [rename_C] + rw [← mul_assoc, ← C_mul] + simp [hchoose] + +/-- Borcea--Branden, Lemma 2.5: source polarization of an operator polarizes +its finite algebraic symbol in the source-variable block. -/ +theorem algebraicSymbol_sourcePolarizedOperator + {τ : Type*} (n : ℕ) + (T : degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] + MvPolynomial τ ℂ) : + algebraicSymbol (fun _ : Fin n => 1) + (sourcePolarizedOperator n T) = + sourceBlockPolarization n + (algebraicSymbol (fun _ : Fin 1 => n) T) := by + rw [algebraicSymbol_sourcePolarizedOperator_eq_sum, + sourceBlockPolarization_algebraicSymbol_finOne_eq_sum] + simpa only [← finOneDegreeIndex_degree_eq_diagonalDegreeBoxIndex] using + sum_degreeOneExponent_rightComplementMonomial_eq_sum_esymm n + (fun k => T (basisDegreeOfLE (R := ℂ) (fun _ : Fin 1 => n) + (finOneDegreeIndex n k))) + +/-- Borcea--Brändén, Lemma 2.5 and Proposition 2.4: stability of a finite +algebraic symbol is preserved when its single source variable is polarized +into a multiaffine source block. -/ +theorem mvUpperHalfPlaneStable_algebraicSymbol_sourcePolarizedOperator + {τ : Type*} (n : ℕ) + (T : degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] + MvPolynomial τ ℂ) + (hstable : + MvUpperHalfPlaneStable + (algebraicSymbol (fun _ : Fin 1 => n) T)) : + MvUpperHalfPlaneStable + (algebraicSymbol (fun _ : Fin n => 1) + (sourcePolarizedOperator n T)) := by + simpa only [algebraicSymbol_sourcePolarizedOperator] using + MvPolynomial.mvUpperHalfPlaneStable_sourceBlockPolarization + (MvPolynomial.degreeOf_algebraicSymbol_inr_le + (fun _ : Fin 1 => n) T default) + hstable + +/-- Finite-symbol sufficiency for a one-variable source degree box. + +This is the source-side specialization of Borcea--Branden, proof of Theorem 1.1, +using equations (2.1)--(2.2), Proposition 2.4, and Lemma 2.5 (Section 2.2, +pp. 10--12). The conclusion is zero-aware because Lemma 2.2 permits the +operator value to vanish. -/ +theorem finiteSymbol_finOne_preserves_stability + {tau : Type*} (n : ℕ) + (T : degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] + MvPolynomial tau ℂ) + (hSymbol : MvUpperHalfPlaneStable + (algebraicSymbol (fun _ : Fin 1 => n) T)) + (f : degreeOfLE (Fin 1) ℂ (fun _ => n)) + (hf : MvUpperHalfPlaneStable f.1) : + MvUpperHalfPlaneStableOrZero (T f) := by + have hdegree : + (uniqueAlgEquiv ℂ (Fin 1) f.1).natDegree ≤ n := by + calc + (uniqueAlgEquiv ℂ (Fin 1) f.1).natDegree = + f.1.degreeOf default := by + simpa only [AlgEquiv.symm_apply_apply] using + (degreeOf_uniqueAlgEquiv_symm (σ := Fin 1) + (uniqueAlgEquiv ℂ (Fin 1) f.1)).symm + _ ≤ n := + (mem_degreeOfLE_iff_degreeOf f.1).mp f.2 default + have hunivariate : + ∀ w : ℂ, 0 < w.im → + (uniqueAlgEquiv ℂ (Fin 1) f.1).eval w ≠ 0 := by + intro w hw + change Polynomial.eval₂ (RingHom.id ℂ) w + (uniqueAlgEquiv ℂ (Fin 1) f.1) ≠ 0 + rw [eval₂_const_uniqueAlgEquiv] + exact hf (fun _ => w) (fun _ => hw) + have hpolarized : MvUpperHalfPlaneStable + (polarizationDegreeBoxLinearMap n f).1 := by + change MvUpperHalfPlaneStable + (polarization n (uniqueAlgEquiv ℂ (Fin 1) f.1)) + exact mvUpperHalfPlaneStable_polarization hdegree hunivariate + have hlifted := finiteSymbol_preserves_stability + (sourcePolarizedOperator n T) + (mvUpperHalfPlaneStable_algebraicSymbol_sourcePolarizedOperator + n T hSymbol) + (polarizationDegreeBoxLinearMap n f) hpolarized + simpa only [sourcePolarizedOperator, LinearMap.comp_apply, + diagonalProjectionDegreeBox_comp_polarizationDegreeBoxLinearMap] using + hlifted + +/-- Termwise form of the source-polarized algebraic symbol after identifying +all polarized source variables. -/ +theorem rename_algebraicSymbol_sourcePolarizedOperator_eq_sum + {τ : Type*} (n : ℕ) + (T : degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] + MvPolynomial τ ℂ) : + MvPolynomial.rename + (MvPolynomial.sourceDiagonalVariableMap (τ := τ) (n := n)) + (algebraicSymbol (fun _ : Fin n => 1) + (sourcePolarizedOperator n T)) = + ∑ m : {m : Fin n →₀ ℕ // ∀ i, m i ≤ 1}, + rename (Sum.inl : τ → τ ⊕ Fin 1) + (T (basisDegreeOfLE (R := ℂ) (fun _ : Fin 1 => n) + (diagonalDegreeBoxIndex m))) * + X (Sum.inr default) ^ (n - m.1.degree) := by + classical + rw [algebraicSymbol, map_sum] + apply Finset.sum_congr rfl + intro m _ + simp only [map_mul, rename_C] + rw [boxChoose_one_of_le_one m.1 m.2, Nat.cast_one, map_one, + one_mul, MvPolynomial.rename_sourceDiagonalVariableMap_rename_inl, + sourcePolarizedOperator_basisDegreeOfLE, + MvPolynomial.rename_rightComplementMonomial_one m.1 m.2] + +/-- Diagonal consequence of the source-side Borcea--Brändén Lemma 2.5 route: +identifying the multiaffine source variables recovers the original degree-box +symbol. The full Lemma 2.5 identity before diagonalization is strictly +stronger and uses `MvPolynomial.sourceBlockPolarization`. -/ +theorem rename_algebraicSymbol_sourcePolarizedOperator + {τ : Type*} (n : ℕ) + (T : degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] + MvPolynomial τ ℂ) : + MvPolynomial.rename + (MvPolynomial.sourceDiagonalVariableMap (τ := τ) (n := n)) + (algebraicSymbol (fun _ : Fin n => 1) + (sourcePolarizedOperator n T)) = + algebraicSymbol (fun _ : Fin 1 => n) T := by + classical + let g : ℕ → MvPolynomial (τ ⊕ Fin 1) ℂ := fun k => + rename (Sum.inl : τ → τ ⊕ Fin 1) + (T (basisDegreeOfLE (R := ℂ) (fun _ : Fin 1 => n) + (finOneDegreeIndex n k))) * + X (Sum.inr default) ^ (n - k) + calc + MvPolynomial.rename + (MvPolynomial.sourceDiagonalVariableMap (τ := τ) (n := n)) + (algebraicSymbol (fun _ : Fin n => 1) + (sourcePolarizedOperator n T)) = + ∑ m : {m : Fin n →₀ ℕ // ∀ i, m i ≤ 1}, + g m.1.degree := by + rw [rename_algebraicSymbol_sourcePolarizedOperator_eq_sum] + apply Finset.sum_congr rfl + intro m _ + simp only [g] + rw [finOneDegreeIndex_degree_eq_diagonalDegreeBoxIndex] + _ = ∑ k ∈ Finset.range (n + 1), n.choose k • g k := + sum_degreeOneExponent_degreeFunction n g + _ = algebraicSymbol (fun _ : Fin 1 => n) T := by + rw [algebraicSymbol_finOne_eq_sum_range] + apply Finset.sum_congr rfl + intro k _ + simp [g, mul_assoc] + +end + +end RealRooted.BorceaBranden diff --git a/RealRooted/BorceaBranden/Applications/UnivariateSymbol.lean b/RealRooted/BorceaBranden/Applications/UnivariateSymbol.lean index d20a5a9a4..46f69b77e 100644 --- a/RealRooted/BorceaBranden/Applications/UnivariateSymbol.lean +++ b/RealRooted/BorceaBranden/Applications/UnivariateSymbol.lean @@ -1,5 +1,6 @@ import RealRooted.Mathlib.Algebra.MvPolynomial.Stability.Symbol import RealRooted.Challenges.BorceaBranden +import RealRooted.BorceaBranden.FiniteSymbolBasis /-! # Univariate compatibility for finite algebraic symbols @@ -33,11 +34,6 @@ noncomputable def univariateDegreeBoxOperator (d : ℕ) (T : ℝ[X] →ₗ[ℝ] map_add' p q := by simp map_smul' r p := by simp -/-- Bounded exponent vectors in one variable are indexed by `Fin (d + 1)`. -/ -noncomputable def degreeOfLEFinOneEquiv (d : ℕ) : - {m : Fin 1 →₀ ℕ // ∀ i, m i ≤ d} ≃ Fin (d + 1) := - (degreeOfLEIndexEquiv (fun _ : Fin 1 => d)).trans (Equiv.piUnique _) - lemma rename_uniqueAlgEquiv_symm_eq_polynomialInFirstMv (p : ℝ[X]) : rename finOneSumToFinTwo (rename (Sum.inl : Fin 1 → Fin 1 ⊕ Fin 1) @@ -61,10 +57,6 @@ lemma rename_rightComplementMonomial_finOne (d : ℕ) (m : Fin 1 →₀ ℕ) : X (1 : Fin 2) ^ (d - m 0) := by simp [rightComplementMonomial, finOneSumToFinTwo] -lemma degreeOfLEFinOneEquiv_val (d : ℕ) (m : {m : Fin 1 →₀ ℕ // ∀ i, m i ≤ d}) : - (degreeOfLEFinOneEquiv d m : ℕ) = m.1 0 := by - rfl - lemma univariateDegreeBoxOperator_basis (d : ℕ) (T : ℝ[X] →ₗ[ℝ] ℝ[X]) (m : {m : Fin 1 →₀ ℕ // ∀ i, m i ≤ d}) : univariateDegreeBoxOperator d T diff --git a/RealRooted/BorceaBranden/FiniteSymbolBasis.lean b/RealRooted/BorceaBranden/FiniteSymbolBasis.lean index f26cb153f..b7da23ce4 100644 --- a/RealRooted/BorceaBranden/FiniteSymbolBasis.lean +++ b/RealRooted/BorceaBranden/FiniteSymbolBasis.lean @@ -1,4 +1,6 @@ +import Mathlib.Data.Finsupp.Weight import RealRooted.BorceaBranden.FiniteSymbolCoefficient +import RealRooted.Mathlib.Algebra.MvPolynomial.Stability.Symbol /-! # Degree-one exponent coordinates for finite symbols @@ -20,20 +22,8 @@ theorem finsupp_eq_indicator_support_of_le_one d = Finsupp.indicator d.support (fun _ _ => 1) := by classical ext i - by_cases hi : i ∈ d.support - · rw [Finsupp.indicator_of_mem hi] - have hne : d i ≠ 0 := Finsupp.mem_support_iff.mp hi - have hle := hd i - cases hdi : d i with - | zero => exact (hne hdi).elim - | succ n => - cases n with - | zero => rfl - | succ n => - rw [hdi] at hle - exact (Nat.not_succ_le_zero n (Nat.le_of_succ_le_succ hle)).elim - · rw [Finsupp.indicator_of_notMem hi] - simpa [Finsupp.mem_support_iff] using hi + rcases Nat.le_one_iff_eq_zero_or_eq_one.mp (hd i) with h | h <;> + simp [Finsupp.indicator, h] /-- Coordinate-wise degree-one exponent vectors are equal exactly when their supports are equal. -/ @@ -48,6 +38,169 @@ theorem finsupp_eq_iff_support_eq_of_le_one rw [finsupp_eq_indicator_support_of_le_one d hd, finsupp_eq_indicator_support_of_le_one e he, hsupport] +/-- Natural-valued exponent vectors bounded by one are equivalent to finite +subsets, via their supports. -/ +noncomputable def degreeOneExponentEquivFinset (sigma : Type*) : + {d : sigma →₀ ℕ // ∀ i, d i ≤ 1} ≃ Finset sigma := by + classical + exact + { toFun := fun d => d.1.support + invFun := fun s => + ⟨Finsupp.indicator s (fun _ _ => 1), fun i => by + by_cases hi : i ∈ s <;> simp [Finsupp.indicator, hi]⟩ + left_inv := fun d => + Subtype.ext (finsupp_eq_indicator_support_of_le_one d.1 d.2).symm + right_inv := fun s => by + ext i + simp [Finsupp.indicator] } + +/-- The total degree of a zero-one exponent vector is the cardinality of its +support. -/ +theorem card_support_eq_degree_of_le_one + {sigma : Type*} (d : sigma →₀ ℕ) (hd : ∀ i, d i ≤ 1) : + d.support.card = d.degree := by + classical + rw [Finsupp.degree_apply] + calc + d.support.card = ∑ i ∈ d.support, 1 := by simp + _ = ∑ i ∈ d.support, d i := by + apply Finset.sum_congr rfl + intro i hi + have hpos : 0 < d i := Finsupp.mem_support_iff.mp hi |>.bot_lt + have hone : d i = 1 := Nat.le_antisymm (hd i) hpos + simp [hone] + +@[simp] +theorem degree_degreeOneExponentEquivFinset_symm + {sigma : Type*} (s : Finset sigma) : + ((degreeOneExponentEquivFinset sigma).symm s).1.degree = s.card := by + let d := (degreeOneExponentEquivFinset sigma).symm s + have hsupp : d.1.support = s := + (degreeOneExponentEquivFinset sigma).apply_symm_apply s + calc + d.1.degree = d.1.support.card := + (card_support_eq_degree_of_le_one d.1 d.2).symm + _ = s.card := congrArg Finset.card hsupp + +end + +end RealRooted.BorceaBranden + +namespace Finsupp + +/-- A one-variable exponent vector is the singleton at its total degree. -/ +@[simp] theorem single_default_degree_fin_one (m : Fin 1 →₀ ℕ) : + single default m.degree = m := by + have hdegree : m.degree = ∑ i, m i := by + rw [degree_apply] + apply Finset.sum_subset (Finset.subset_univ m.support) + intro i _ hi + simpa [mem_support_iff] using hi + apply Finsupp.ext + intro i + have hi : i = 0 := Fin.eq_zero i + subst i + rw [hdegree] + simp + +/-- The complement of a zero-one exponent has total degree equal to the +cardinality of the variable set minus the original total degree. -/ +theorem sum_one_sub_eq_card_sub_degree + {σ : Type*} [Fintype σ] (m : σ →₀ ℕ) + (hm : ∀ i, m i ≤ 1) : + ∑ i, (1 - m i) = Fintype.card σ - m.degree := by + rw [Finset.sum_tsub_distrib Finset.univ (by + intro i _ + exact hm i)] + simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, + Nat.mul_one] + congr 1 + rw [degree_apply] + exact (sum_fintype m (fun _ e => e) (fun _ => rfl)).symm + +end Finsupp + +namespace RealRooted.BorceaBranden + +/-- Bounded exponent vectors in one variable are indexed by `Fin (d + 1)`. -/ +noncomputable def degreeOfLEFinOneEquiv (d : ℕ) : + {m : Fin 1 →₀ ℕ // ∀ i, m i ≤ d} ≃ Fin (d + 1) := + (MvPolynomial.degreeOfLEIndexEquiv (fun _ : Fin 1 => d)).trans + (Equiv.piUnique _) + +lemma degreeOfLEFinOneEquiv_val (d : ℕ) + (m : {m : Fin 1 →₀ ℕ // ∀ i, m i ≤ d}) : + (degreeOfLEFinOneEquiv d m : ℕ) = m.1 0 := by + rfl + +end RealRooted.BorceaBranden + +namespace RealRooted.BorceaBranden + +noncomputable section + +open MvPolynomial + +/-- The canonical one-variable degree-box index associated with a natural +number. The truncation is inactive on `Fin (n + 1)`. -/ +noncomputable def finOneDegreeIndex (n k : ℕ) : + {m : Fin 1 →₀ ℕ // ∀ i, m i ≤ n} := + (degreeOfLEFinOneEquiv n).symm + ⟨min k n, Nat.lt_succ_iff.mpr (Nat.min_le_right k n)⟩ + +@[simp] lemma finOneDegreeIndex_equiv_apply (n : ℕ) + (m : {m : Fin 1 →₀ ℕ // ∀ i, m i ≤ n}) : + finOneDegreeIndex n (degreeOfLEFinOneEquiv n m) = m := by + apply (degreeOfLEFinOneEquiv n).injective + apply Fin.ext + simp [finOneDegreeIndex, degreeOfLEFinOneEquiv_val, m.2 0] + +/-- Expand a one-variable algebraic symbol over its canonical `Fin (n + 1)` +indexing. -/ +theorem algebraicSymbol_finOne_eq_sum_fin + {τ R : Type*} [CommSemiring R] (n : ℕ) + (T : degreeOfLE (Fin 1) R (fun _ => n) →ₗ[R] MvPolynomial τ R) : + algebraicSymbol (fun _ : Fin 1 => n) T = + ∑ k : Fin (n + 1), + C (n.choose k : R) * + rename (Sum.inl : τ → τ ⊕ Fin 1) + (T (basisDegreeOfLE (R := R) (fun _ : Fin 1 => n) + (finOneDegreeIndex n k))) * + X (Sum.inr default) ^ (n - k) := by + classical + rw [algebraicSymbol] + apply Fintype.sum_equiv (degreeOfLEFinOneEquiv n) + intro m + have hindex : finOneDegreeIndex n (m.1 0) = m := by + apply (degreeOfLEFinOneEquiv n).injective + apply Fin.ext + simp [finOneDegreeIndex, degreeOfLEFinOneEquiv_val, + Nat.min_eq_left (m.2 0)] + simp [hindex, boxChoose, + rightComplementMonomial, degreeOfLEFinOneEquiv_val] + +/-- Expand a one-variable algebraic symbol over the natural-number range +`0, ..., n`. -/ +theorem algebraicSymbol_finOne_eq_sum_range + {τ R : Type*} [CommSemiring R] (n : ℕ) + (T : degreeOfLE (Fin 1) R (fun _ => n) →ₗ[R] MvPolynomial τ R) : + algebraicSymbol (fun _ : Fin 1 => n) T = + ∑ k ∈ Finset.range (n + 1), + C (n.choose k : R) * + rename (Sum.inl : τ → τ ⊕ Fin 1) + (T (basisDegreeOfLE (R := R) (fun _ : Fin 1 => n) + (finOneDegreeIndex n k))) * + X (Sum.inr default) ^ (n - k) := by + classical + let g : ℕ → MvPolynomial (τ ⊕ Fin 1) R := fun k => + C (n.choose k : R) * + rename (Sum.inl : τ → τ ⊕ Fin 1) + (T (basisDegreeOfLE (R := R) (fun _ : Fin 1 => n) + (finOneDegreeIndex n k))) * + X (Sum.inr default) ^ (n - k) + rw [algebraicSymbol_finOne_eq_sum_fin (n := n) (T := T)] + simpa [g] using Fin.sum_univ_eq_sum_range g (n + 1) + end end RealRooted.BorceaBranden diff --git a/RealRooted/BorceaBranden/FiniteSymbolDegree.lean b/RealRooted/BorceaBranden/FiniteSymbolDegree.lean index daba03e7e..338db9cfe 100644 --- a/RealRooted/BorceaBranden/FiniteSymbolDegree.lean +++ b/RealRooted/BorceaBranden/FiniteSymbolDegree.lean @@ -28,28 +28,31 @@ variable {sigma tau R : Type*} [CommSemiring R] [Fintype sigma] /-- The finite algebraic symbol for the multiaffine degree box has degree at most one in every source coordinate. No degree bound is imposed on the target variables. -/ -theorem degreeOf_algebraicSymbol_one_inr_le - (T : degreeOfLE sigma R (fun _ => 1) →ₗ[R] MvPolynomial tau R) +/- Borcea--Branden, arXiv:0809.0401, Section 1.1. In each summand of +`G_T(z,w)`, source variable `w_i` has exponent `κ i - α i`, hence at most +`κ i`; the renamed operator value uses only the output-variable block. -/ +theorem degreeOf_algebraicSymbol_inr_le + (κ : sigma → ℕ) + (T : degreeOfLE sigma R κ →ₗ[R] MvPolynomial tau R) (i : sigma) : - (algebraicSymbol (fun _ : sigma => 1) T).degreeOf (Sum.inr i) ≤ 1 := by + (algebraicSymbol κ T).degreeOf (Sum.inr i) ≤ κ i := by classical rcases subsingleton_or_nontrivial R with hR | hR · letI := hR - rw [Subsingleton.elim (algebraicSymbol (fun _ : sigma => 1) T) 0] + rw [Subsingleton.elim (algebraicSymbol κ T) 0] simp · letI := hR rw [algebraicSymbol_eq_sum] refine (degreeOf_sum_le (Sum.inr i) Finset.univ fun m => - C (boxChoose (fun _ : sigma => 1) m.1 : R) * + C (boxChoose κ m.1 : R) * rename (Sum.inl : tau → tau ⊕ sigma) - (T (basisDegreeOfLE (fun _ : sigma => 1) m)) * - rightComplementMonomial (fun _ : sigma => 1) m.1).trans ?_ + (T (basisDegreeOfLE κ m)) * + rightComplementMonomial κ m.1).trans ?_ apply Finset.sup_le - intro m hm + intro m _ have hrename : (rename (Sum.inl : tau → tau ⊕ sigma) - (T (basisDegreeOfLE (fun _ : sigma => 1) m))).degreeOf - (Sum.inr i) = 0 := by + (T (basisDegreeOfLE κ m))).degreeOf (Sum.inr i) = 0 := by apply Nat.le_zero.mp rw [degreeOf_le_iff] intro d hd @@ -57,28 +60,27 @@ theorem degreeOf_algebraicSymbol_one_inr_le by_contra hdi have hmem : Sum.inr i ∈ (rename (Sum.inl : tau → tau ⊕ sigma) - (T (basisDegreeOfLE (fun _ : sigma => 1) m))).vars := by - rw [mem_vars] + (T (basisDegreeOfLE κ m))).vars := by + rw [mem_vars_iff_mem_support] exact ⟨d, hd, Finsupp.mem_support_iff.mpr hdi⟩ obtain ⟨j, _hj, hji⟩ := mem_vars_rename Sum.inl _ hmem exact Sum.inl_ne_inr hji have hleft : - (C (boxChoose (fun _ : sigma => 1) m.1 : R) * + (C (boxChoose κ m.1 : R) * rename (Sum.inl : tau → tau ⊕ sigma) - (T (basisDegreeOfLE (fun _ : sigma => 1) m))).degreeOf - (Sum.inr i) ≤ 0 := by + (T (basisDegreeOfLE κ m))).degreeOf (Sum.inr i) ≤ 0 := by exact (degreeOf_C_mul_le _ _ _).trans_eq hrename have hright : (rightComplementMonomial (R := R) (τ := tau) - (fun _ : sigma => 1) m.1).degreeOf (Sum.inr i) ≤ 1 := by + κ m.1).degreeOf (Sum.inr i) ≤ κ i := by rw [rightComplementMonomial_eq_prod] refine (degreeOf_prod_le (Sum.inr i) Finset.univ fun j => - X (Sum.inr j) ^ (1 - m.1 j)).trans ?_ + X (Sum.inr j) ^ (κ j - m.1 j)).trans ?_ calc ∑ j : sigma, - (X (Sum.inr j) ^ (1 - m.1 j) : + (X (Sum.inr j) ^ (κ j - m.1 j) : MvPolynomial (tau ⊕ sigma) R).degreeOf (Sum.inr i) = - 1 - m.1 i := by + κ i - m.1 i := by rw [Finset.sum_eq_single i] · simp · intro j hj hji @@ -86,9 +88,16 @@ theorem degreeOf_algebraicSymbol_one_inr_le intro hij exact hji (Sum.inr_injective hij).symm · simp - _ ≤ 1 := Nat.sub_le _ _ + _ ≤ κ i := Nat.sub_le _ _ exact (degreeOf_mul_le _ _ _).trans - ((Nat.add_le_add hleft hright).trans_eq (Nat.zero_add 1)) + ((Nat.add_le_add hleft hright).trans_eq + (Nat.zero_add (κ i))) + +theorem degreeOf_algebraicSymbol_one_inr_le + (T : degreeOfLE sigma R (fun _ => 1) →ₗ[R] MvPolynomial tau R) + (i : sigma) : + (algebraicSymbol (fun _ : sigma => 1) T).degreeOf (Sum.inr i) ≤ 1 := by + exact degreeOf_algebraicSymbol_inr_le (fun _ : sigma => 1) T i end diff --git a/RealRooted/GraceHalfPlane.lean b/RealRooted/GraceHalfPlane.lean index e5a1b6916..314ca21b6 100644 --- a/RealRooted/GraceHalfPlane.lean +++ b/RealRooted/GraceHalfPlane.lean @@ -84,6 +84,98 @@ theorem mem_lowerHalf_of_recip_avg {b : ℝ} {w ζ : ℂ} simp_all grind +/-- The reciprocal-average conclusion remains valid when the numerator is an +ambient cardinality at least as large as the multiset cardinality. This is the +half-plane form of adjoining roots at infinity in Grace's theorem. -/ +theorem mem_lowerHalf_of_recip_sum_of_card_le + {b : ℝ} {w ζ : ℂ} {n : ℕ} + (S : Multiset ℂ) (hS : S ≠ 0) (hcard : S.card ≤ n) + (hw : w ∉ lowerHalf b) + (hz : ∀ z ∈ S, z ∈ lowerHalf b) + (hζ : (n : ℂ) / (w - ζ) = + (S.map (fun z ↦ 1 / (w - z))).sum) : + ζ ∈ lowerHalf b := by + have hd : 0 < S.card := Multiset.card_pos.mpr hS + have hn : 0 < n := lt_of_lt_of_le hd hcard + let t : ℝ := (S.card : ℝ) / (n : ℝ) + have ht_pos : 0 < t := by + dsimp [t] + positivity + have ht_le : t ≤ 1 := by + dsimp [t] + rw [div_le_one] + · exact_mod_cast hcard + · exact_mod_cast hn + let ζ' : ℂ := w - (t : ℂ) * (w - ζ) + have hscaled : + (S.card : ℂ) / (w - ζ') = + (S.map (fun z ↦ 1 / (w - z))).sum := by + rw [← hζ] + dsimp [ζ', t] + have hn0 : (n : ℂ) ≠ 0 := by exact_mod_cast hn.ne' + have hd0 : (S.card : ℂ) ≠ 0 := by + exact_mod_cast (Multiset.card_pos.mpr hS).ne' + by_cases hwζ : w - ζ = 0 + · simp [hwζ] + · push_cast + field_simp [hn0, hd0, hwζ] + ring + have hζ' : ζ' ∈ lowerHalf b := + mem_lowerHalf_of_recip_avg S hS hw hz hscaled + have hw_im : b < w.im := by + simpa [lowerHalf] using hw + simp only [mem_lowerHalf] at hζ' ⊢ + dsimp [ζ'] at hζ' + simp only [Complex.sub_im, Complex.mul_im, + Complex.ofReal_re, Complex.ofReal_im, zero_mul, add_zero] at hζ' + nlinarith + +/-- A polar derivative preserves a closed lower half-plane when its ambient +degree only bounds, rather than equals, the polynomial degree. -/ +theorem polarDeriv_rootsIn_lowerHalf_of_natDegree_le + {n : Nat} {b : ℝ} {ζ : ℂ} {A : ℂ[X]} + (hn : 1 ≤ n) (hA : A.natDegree ≤ n) + (hAroots : A.RootsIn (lowerHalf b)) + (hζ : ζ ∉ lowerHalf b) : + (polarDeriv n ζ A).RootsIn (lowerHalf b) := by + intro w hw0 + have hn0 : (n : ℂ) ≠ 0 := by + exact_mod_cast (show n ≠ 0 by lia) + by_cases hA0 : A.natDegree = 0 + · have hder : derivative A = 0 := + Polynomial.derivative_eq_zero.mpr hA0 + apply hAroots w + have h : (n : ℂ) * eval w A = 0 := by + simpa only [IsRoot, polarDeriv, hder, mul_zero, add_zero, + eval_mul, eval_C] using hw0 + exact (mul_eq_zero.mp h).resolve_left hn0 + · by_contra hwmem + have hAw : eval w A ≠ 0 := + fun h ↦ hwmem (hAroots w h) + have heq : (n : ℂ) * eval w A + + (ζ - w) * eval w (derivative A) = 0 := by + have h := hw0 + simp only [IsRoot, polarDeriv, eval_add, eval_mul, + eval_sub, eval_C, eval_X] at h + simp_all + have hwζ : w - ζ ≠ 0 := by grind + have hsplit : A.Splits := IsAlgClosed.splits A + have hcard : A.roots.card = A.natDegree := + splits_iff_card_roots.mp hsplit + have hroots_ne : A.roots ≠ 0 := by + rw [← Multiset.card_pos, hcard] + exact Nat.pos_of_ne_zero hA0 + have hcard_le : A.roots.card ≤ n := hcard.trans_le hA + have hscaled : (n : ℂ) / (w - ζ) = + (A.roots.map (fun z ↦ 1 / (w - z))).sum := by + rw [← hsplit.eval_derivative_div_eval_of_ne_zero hAw] + grind + have : ζ ∈ lowerHalf b := by + exact mem_lowerHalf_of_recip_sum_of_card_le + A.roots hroots_ne hcard_le hwmem + (fun z hz ↦ hAroots z (isRoot_of_mem_roots hz)) hscaled + exact hζ this + theorem multiset_avg_mem_lowerHalf {b : ℝ} (S : Multiset ℂ) (hS : S ≠ 0) (hz : ∀ z ∈ S, z ∈ lowerHalf b) : S.sum / (S.card : ℂ) ∈ lowerHalf b := by @@ -199,7 +291,7 @@ theorem polarDeriv_natDegree_lowerHalf {n : Nat} {b : ℝ} {ζ : ℂ} private theorem grace_aux_lowerHalf {b : ℝ} : ∀ (n : Nat) (f g : ℂ[X]), - (binomialLift n f).natDegree = n → (binomialLift n g).natDegree = n → + (binomialLift n f).natDegree ≤ n → (binomialLift n g).natDegree = n → AreApolar n f g → (binomialLift n f).RootsIn (lowerHalf b) → (binomialLift n g).HasRootIn (lowerHalf b) := by intro n @@ -225,18 +317,17 @@ private theorem grace_aux_lowerHalf {b : ℝ} : by_cases hζ' : ζ ∈ lowerHalf b · exact ⟨ζ, hζ, hζ'⟩ · set f' := polarShift ζ f - have hf' : (binomialLift (n - 1) f').natDegree = n - 1 := by - have hf' : (polarDeriv n ζ (binomialLift n f)).natDegree = n - 1 := by - apply polarDeriv_natDegree_lowerHalf + have hf' : (binomialLift (n - 1) f').natDegree ≤ n - 1 := by + have hf' : (polarDeriv n ζ (binomialLift n f)).natDegree ≤ n - 1 := by + apply polarDeriv_natDegree_le · grind - · simp [*] - · exact hroots - · simp [*] + · exact hf rw [polarDeriv_binomialLift (Nat.pos_of_ne_zero hn) ζ f] at hf' rwa [Polynomial.natDegree_C_mul] at hf' simp_all have hf'_roots : (binomialLift (n - 1) f').RootsIn (lowerHalf b) := by - have := polarDeriv_rootsIn_lowerHalf (Nat.pos_of_ne_zero hn) hf hroots hζ' + have := polarDeriv_rootsIn_lowerHalf_of_natDegree_le + (Nat.pos_of_ne_zero hn) hf hroots hζ' have := polarDeriv_binomialLift (Nat.pos_of_ne_zero hn) ζ f simp_all [RootsIn] grind @@ -264,7 +355,7 @@ private theorem grace_aux_lowerHalf {b : ℝ} : exact ⟨w, by replace hg' := congr_arg (Polynomial.eval w) hg'; simp_all⟩ theorem grace_apolarity_lowerHalf {n : Nat} {b : ℝ} {f g : ℂ[X]} - (hf : (binomialLift n f).natDegree = n) (hg : (binomialLift n g).natDegree = n) + (hf : (binomialLift n f).natDegree ≤ n) (hg : (binomialLift n g).natDegree = n) (hap : AreApolar n f g) (hroots : (binomialLift n f).RootsIn (lowerHalf b)) : (binomialLift n g).HasRootIn (lowerHalf b) := @@ -341,7 +432,7 @@ theorem grace_apolarity_upperHalf {n : Nat} {b : ℝ} {f g : ℂ[X]} simp only [mem_lowerHalf] linarith obtain ⟨w, hwroot, hwmem⟩ := - grace_apolarity_lowerHalf hfhat hghat haphat hroothat + grace_apolarity_lowerHalf hfhat.le hghat haphat hroothat refine ⟨-w, ?_, ?_⟩ · rw [negComp_binomialLift] at hwroot simp only [Polynomial.IsRoot, negComp, Polynomial.eval_comp, Polynomial.eval_neg, diff --git a/RealRooted/Hadamard.lean b/RealRooted/Hadamard.lean index c6f507e65..c8bda487f 100644 --- a/RealRooted/Hadamard.lean +++ b/RealRooted/Hadamard.lean @@ -1933,7 +1933,7 @@ theorem exists_apolarTwist_root_of_grace_lowerHalf {n : Nat} {b : ℝ} (binomialLift n (apolarTwist n z g)).HasRootIn (lowerHalf b) := by have hap : AreApolar n f (apolarTwist n z g) := (areApolar_apolarTwist_iff n f g z).2 hcomp - exact grace_apolarity_lowerHalf hf htw hap hroots + exact grace_apolarity_lowerHalf hf.le htw hap hroots theorem exists_apolarTwist_root_of_grace_upperHalf {n : Nat} {b : ℝ} {f g : ℂ[X]} {z : ℂ} diff --git a/RealRooted/Mathlib/Algebra/MvPolynomial/Degrees.lean b/RealRooted/Mathlib/Algebra/MvPolynomial/Degrees.lean new file mode 100644 index 000000000..b40bcf548 --- /dev/null +++ b/RealRooted/Mathlib/Algebra/MvPolynomial/Degrees.lean @@ -0,0 +1,30 @@ +import Mathlib.Algebra.MvPolynomial.Degrees + +/-! +# Additional total-degree bounds + +This file contains Mathlib-shaped compatibility lemmas for multivariate +polynomial degrees. +-/ + +open scoped BigOperators + +namespace MvPolynomial + +/-- Total degree is at most the sum of the coordinatewise degrees. -/ +theorem totalDegree_le_sum_degreeOf {σ R : Type*} [Fintype σ] [CommSemiring R] + (p : MvPolynomial σ R) : + p.totalDegree ≤ ∑ i, p.degreeOf i := by + classical + rw [totalDegree] + apply Finset.sup_le + intro d hd + calc + d.sum (fun _ e => e) = ∑ i, d i := by + rw [Finsupp.sum_fintype] + intro + rfl + _ ≤ ∑ i, p.degreeOf i := + Finset.sum_le_sum fun i _ => le_degreeOf_of_mem_support i hd + +end MvPolynomial diff --git a/RealRooted/Mathlib/Algebra/MvPolynomial/Equiv.lean b/RealRooted/Mathlib/Algebra/MvPolynomial/Equiv.lean new file mode 100644 index 000000000..bcfae2931 --- /dev/null +++ b/RealRooted/Mathlib/Algebra/MvPolynomial/Equiv.lean @@ -0,0 +1,53 @@ +import Mathlib.Algebra.MvPolynomial.Equiv +import Mathlib.Algebra.Polynomial.Degree.Lemmas + +/-! +# Degree bounds for univariate multivariate-polynomial equivalences + +This file contains Mathlib-shaped compatibility lemmas for +`MvPolynomial.uniqueAlgEquiv`. +-/ + +namespace MvPolynomial + +/-- The degree in the unique variable after converting a univariate polynomial +to an `MvPolynomial` is its natural degree. -/ +theorem degreeOf_uniqueAlgEquiv_symm + {σ R : Type*} [Unique σ] [CommSemiring R] (p : Polynomial R) : + degreeOf default ((MvPolynomial.uniqueAlgEquiv R σ).symm p) = + p.natDegree := by + apply le_antisymm + · rw [degreeOf_le_iff] + intro d hd + have hcoeff : p.coeff (d default) ≠ 0 := by + rw [← MvPolynomial.coeff_uniqueAlgEquiv_symm R p d] + exact MvPolynomial.mem_support_iff.mp hd + exact Polynomial.le_natDegree_of_ne_zero hcoeff + · rw [Polynomial.natDegree_le_iff_coeff_eq_zero] + intro n hn + have hnotmem : + Finsupp.single default n ∉ + ((MvPolynomial.uniqueAlgEquiv R σ).symm p).support := by + apply MvPolynomial.notMem_support_of_degreeOf_lt default + simpa using hn + have hzero := MvPolynomial.notMem_support_iff.mp hnotmem + rw [MvPolynomial.coeff_uniqueAlgEquiv_symm R p + (Finsupp.single default n)] at hzero + simpa using hzero + +/-- Passing from a uniquely indexed multivariate polynomial to a univariate +polynomial does not increase total degree. -/ +theorem natDegree_uniqueAlgEquiv_le_totalDegree + {σ R : Type*} [Unique σ] [CommSemiring R] (p : MvPolynomial σ R) : + (MvPolynomial.uniqueAlgEquiv R σ p).natDegree ≤ p.totalDegree := by + calc + (MvPolynomial.uniqueAlgEquiv R σ p).natDegree = + degreeOf default + ((MvPolynomial.uniqueAlgEquiv R σ).symm + (MvPolynomial.uniqueAlgEquiv R σ p)) := + (degreeOf_uniqueAlgEquiv_symm + (MvPolynomial.uniqueAlgEquiv R σ p)).symm + _ = degreeOf default p := by rw [AlgEquiv.symm_apply_apply] + _ ≤ p.totalDegree := degreeOf_le_totalDegree p default + +end MvPolynomial diff --git a/RealRooted/Mathlib/Algebra/MvPolynomial/Stability/Symbol.lean b/RealRooted/Mathlib/Algebra/MvPolynomial/Stability/Symbol.lean index 131f6ce15..120cb2188 100644 --- a/RealRooted/Mathlib/Algebra/MvPolynomial/Stability/Symbol.lean +++ b/RealRooted/Mathlib/Algebra/MvPolynomial/Stability/Symbol.lean @@ -40,6 +40,16 @@ variable {σ τ R : Type*} [CommSemiring R] [Fintype σ] def boxChoose (κ : σ → ℕ) (m : σ →₀ ℕ) : ℕ := ∏ i, Nat.choose (κ i) (m i) +/-- Every binomial coefficient in a multiaffine source box is one. -/ +@[simp] +theorem boxChoose_one_of_le_one (m : σ →₀ ℕ) (hm : ∀ i, m i ≤ 1) : + boxChoose (fun _ : σ => 1) m = 1 := by + classical + simp only [boxChoose] + apply Finset.prod_eq_one + intro i hi + rcases Nat.le_one_iff_eq_zero_or_eq_one.mp (hm i) with h | h <;> simp [h] + /-- The right-block monomial with exponent vector `κ - m`. -/ noncomputable def rightComplementMonomial (κ : σ → ℕ) (m : σ →₀ ℕ) : MvPolynomial (τ ⊕ σ) R := @@ -51,6 +61,27 @@ theorem rightComplementMonomial_eq_prod (κ : σ → ℕ) (m : σ →₀ ℕ) : ∏ i, X (Sum.inr i) ^ (κ i - m i) := by rfl +/-- In a multiaffine box, the complementary monomial is the product over the +complement of the exponent support. -/ +theorem rightComplementMonomial_one_eq_support_compl [DecidableEq σ] + (m : σ →₀ ℕ) (hm : ∀ i, m i ≤ 1) : + rightComplementMonomial (R := R) (τ := τ) (fun _ : σ => 1) m = + rename (Sum.inr : σ → τ ⊕ σ) (∏ i ∈ m.supportᶜ, X i) := by + rw [rightComplementMonomial_eq_prod] + simp only [map_prod, rename_X] + rw [Finset.compl_eq_univ_sdiff, Finset.sdiff_eq_filter, + Finset.prod_filter] + apply Finset.prod_congr rfl + intro i _ + by_cases hi : i ∈ m.support + · have hmi : m i = 1 := by + rcases Nat.le_one_iff_eq_zero_or_eq_one.mp (hm i) with hzero | hone + · exact (Finsupp.mem_support_iff.mp hi hzero).elim + · exact hone + simp [hi, hmi] + · have hmi : m i = 0 := Finsupp.notMem_support_iff.mp hi + simp [hi, hmi] + /-- The finite algebraic symbol of a linear map on a coordinate-wise degree box. Its monomial-basis expansion is `Σ m, choose(κ, m) * T(X^m) * w^(κ-m)`. -/ diff --git a/RealRooted/Mathlib/Analysis/Complex/OpenMapping.lean b/RealRooted/Mathlib/Analysis/Complex/OpenMapping.lean index 72dbc48ca..5866a23ec 100644 --- a/RealRooted/Mathlib/Analysis/Complex/OpenMapping.lean +++ b/RealRooted/Mathlib/Analysis/Complex/OpenMapping.lean @@ -1,7 +1,7 @@ import Mathlib.Analysis.Complex.OpenMapping /-! -# Complex polynomial consequences of the open mapping theorem +# Complex consequences of the open mapping theorem This file contains general-purpose compatibility lemmas intended for eventual upstreaming to Mathlib. @@ -12,6 +12,39 @@ open scoped Topology noncomputable section +namespace AnalyticAt + +/-- A locally nonconstant analytic map that is eventually confined to the +closed upper half-plane takes its base point into the open upper half-plane. -/ +theorem im_pos_of_eventually_im_nonneg + {f : ℂ → ℂ} {z₀ : ℂ} (hf : AnalyticAt ℂ f z₀) + (hnotconst : ¬∀ᶠ z in 𝓝 z₀, f z = f z₀) + (hzero : 0 ≤ (f z₀).im) + (hnonneg : ∀ᶠ z in 𝓝 z₀, 0 ≤ (f z).im) : + 0 < (f z₀).im := by + by_contra hpos + have himzero : (f z₀).im = 0 := + le_antisymm (le_of_not_gt hpos) hzero + have hmap : 𝓝 (f z₀) ≤ Filter.map f (𝓝 z₀) := + hf.eventually_constant_or_nhds_le_map_nhds_aux.resolve_left hnotconst + have himage : f '' {z | 0 ≤ (f z).im} ∈ 𝓝 (f z₀) := + hmap (image_mem_map hnonneg) + obtain ⟨ε, hε, hball⟩ := Metric.mem_nhds_iff.mp himage + let w : ℂ := f z₀ - (ε / 2 : ℝ) * Complex.I + have hwball : w ∈ ball (f z₀) ε := by + rw [mem_ball] + simp [w, Real.norm_eq_abs, abs_of_pos hε] + linarith + have hwim : w.im < 0 := by + simp [w, himzero] + linarith + obtain ⟨z, hz, hzw⟩ := hball hwball + change 0 ≤ (f z).im at hz + rw [hzw] at hz + linarith + +end AnalyticAt + namespace Polynomial private theorem neg_eval_div_eval_image_mem_nhds diff --git a/RealRooted/Mathlib/RingTheory/MvPolynomial/Symmetric.lean b/RealRooted/Mathlib/RingTheory/MvPolynomial/Symmetric.lean new file mode 100644 index 000000000..1ad97ec57 --- /dev/null +++ b/RealRooted/Mathlib/RingTheory/MvPolynomial/Symmetric.lean @@ -0,0 +1,111 @@ +import Mathlib.RingTheory.MvPolynomial.Symmetric.Defs + +/-! +# Finite-variable symmetrization + +This file defines permutation summation and normalized symmetrization for +multivariate polynomials. These are the algebraic operators used in the +Grace--Walsh--Szegő symmetrization argument. +-/ + +open BigOperators + +namespace MvPolynomial + +/-- The finite indexing type of permutations induced by a finite type. -/ +noncomputable local instance {σ : Type*} [Fintype σ] : + Fintype (Equiv.Perm σ) := + Fintype.ofFinite _ + +/-- Sum all variable permutations of a multivariate polynomial. -/ +noncomputable def symmetrizationSum + {σ R : Type*} [Fintype σ] [CommSemiring R] + (p : MvPolynomial σ R) : MvPolynomial σ R := by + classical + exact ∑ e : Equiv.Perm σ, rename e p + +/-- The permutation sum is symmetric. -/ +theorem symmetrizationSum_isSymmetric + {σ R : Type*} [Fintype σ] [CommSemiring R] + (p : MvPolynomial σ R) : + IsSymmetric (symmetrizationSum p) := by + classical + intro e + simp only [symmetrizationSum, map_sum, rename_rename] + simpa [Function.comp_def] using + Equiv.sum_comp (Equiv.mulLeft e) + (fun f : Equiv.Perm σ => rename f p) + +/-- Average all variable permutations of a complex multivariate polynomial. -/ +noncomputable def fullSymmetrization + {σ R : Type*} [Fintype σ] [Field R] [CharZero R] + (p : MvPolynomial σ R) : MvPolynomial σ R := by + classical + exact C (Fintype.card (Equiv.Perm σ) : R)⁻¹ * + symmetrizationSum p + +/-- Full symmetrization is symmetric. -/ +theorem fullSymmetrization_isSymmetric + {σ R : Type*} [Fintype σ] [Field R] [CharZero R] + (p : MvPolynomial σ R) : + IsSymmetric (fullSymmetrization p) := by + classical + intro e + simp only [fullSymmetrization, map_mul, rename_C] + rw [symmetrizationSum_isSymmetric p e] + +/-- Full symmetrization preserves evaluation at a constant assignment. -/ +theorem eval_fullSymmetrization_const + {σ R : Type*} [Fintype σ] [Field R] [CharZero R] + (p : MvPolynomial σ R) (w : R) : + eval (fun _ : σ => w) (fullSymmetrization p) = + eval (fun _ : σ => w) p := by + classical + have hcard : (Fintype.card (Equiv.Perm σ) : R) ≠ 0 := by + exact_mod_cast Fintype.card_ne_zero + have hconst (e : Equiv.Perm σ) : + (fun _ : σ => w) ∘ e = fun _ : σ => w := by + rfl + simp only [fullSymmetrization, map_mul, eval_C, + symmetrizationSum, map_sum, eval_rename, hconst] + rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, + ← mul_assoc, inv_mul_cancel₀ hcard, one_mul] + +end MvPolynomial + +namespace MvPolynomial + +/-- Convex-form partial symmetrization associated with a permutation. -/ +noncomputable def partialSymmetrization + {σ R : Type*} [CommRing R] + (t : R) (e : Equiv.Perm σ) (p : MvPolynomial σ R) : + MvPolynomial σ R := + C t * p + C (1 - t) * rename e p + +/-- At weight zero, partial symmetrization is variable permutation. -/ +@[simp] theorem partialSymmetrization_zero + {σ R : Type*} [CommRing R] + (e : Equiv.Perm σ) (p : MvPolynomial σ R) : + partialSymmetrization 0 e p = rename e p := by + simp [partialSymmetrization] + +/-- At weight one, partial symmetrization is the original polynomial. -/ +@[simp] theorem partialSymmetrization_one + {σ R : Type*} [CommRing R] + (e : Equiv.Perm σ) (p : MvPolynomial σ R) : + partialSymmetrization 1 e p = p := by + simp [partialSymmetrization] + +/-- Partial symmetrization preserves evaluation at a constant assignment. -/ +theorem eval_partialSymmetrization_const + {σ R : Type*} [CommRing R] + (t w : R) (e : Equiv.Perm σ) (p : MvPolynomial σ R) : + eval (fun _ : σ => w) (partialSymmetrization t e p) = + eval (fun _ : σ => w) p := by + have hconst : (fun _ : σ => w) ∘ e = fun _ : σ => w := by + rfl + simp only [partialSymmetrization, map_add, map_mul, eval_C, + eval_rename, hconst] + ring + +end MvPolynomial diff --git a/RealRooted/Multiaffine.lean b/RealRooted/Multiaffine.lean index b86b863ed..d92a131a9 100644 --- a/RealRooted/Multiaffine.lean +++ b/RealRooted/Multiaffine.lean @@ -1,3 +1,4 @@ +import RealRooted.Mathlib.RingTheory.MvPolynomial.Symmetric import Mathlib.Algebra.MvPolynomial.PDeriv import Mathlib.RingTheory.MvPolynomial.Symmetric.Defs @@ -459,3 +460,16 @@ theorem esymm [Fintype σ] [Nontrivial R] (n : ℕ) : end IsMultiaffine end MvPolynomial + +namespace MvPolynomial + +/-- Partial symmetrization by a permutation preserves multiaffineness. -/ +theorem IsMultiaffine.partialSymmetrization + {σ R : Type*} [CommRing R] + {p : MvPolynomial σ R} (hp : IsMultiaffine p) + (t : R) (e : Equiv.Perm σ) : + IsMultiaffine (MvPolynomial.partialSymmetrization t e p) := by + exact (hp.C_mul t).add + ((hp.rename e.injective).C_mul (1 - t)) + +end MvPolynomial diff --git a/RealRooted/MultivariateStability.lean b/RealRooted/MultivariateStability.lean index 333211e8f..be4d1c764 100644 --- a/RealRooted/MultivariateStability.lean +++ b/RealRooted/MultivariateStability.lean @@ -1,7 +1,9 @@ import Mathlib.Algebra.MvPolynomial.Eval +import Mathlib.Algebra.MvPolynomial.Equiv import Mathlib.Algebra.MvPolynomial.Funext import Mathlib.Algebra.MvPolynomial.Rename import Mathlib.Algebra.Polynomial.Eval.Coeff +import Mathlib.Algebra.Polynomial.Eval.Degree import Mathlib.Algebra.Polynomial.Splits import Mathlib.Data.Complex.Basic import Mathlib.Analysis.Complex.UpperHalfPlane.Basic @@ -489,6 +491,72 @@ theorem eval_specializeLeft {sigma tau : Type*} (x : sigma → ℂ) ext i cases i <;> simp +/-- Specializing one variable block cannot increase the degree in the +remaining singleton block. -/ +theorem natDegree_uniqueAlgEquiv_specializeLeft_le_degreeOf + {τ : Type*} (x : τ → ℂ) + (P : MvPolynomial (τ ⊕ Fin 1) ℂ) : + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) + (specializeLeft x P)).natDegree ≤ + P.degreeOf (Sum.inr default) := by + let e : τ ⊕ Fin 1 ≃ Option τ := + { toFun := fun s => + match s with + | Sum.inl i => some i + | Sum.inr _ => none + invFun := fun o => + match o with + | some i => Sum.inl i + | none => Sum.inr default + left_inv := by + rintro (i | i) + · rfl + · exact congrArg Sum.inr (Subsingleton.elim default i) + right_inv := by + intro o + cases o <;> rfl } + let Q : MvPolynomial (Option τ) ℂ := + MvPolynomial.rename e P + have hQdeg : + (MvPolynomial.optionEquivLeft ℂ τ Q).natDegree = + P.degreeOf (Sum.inr default) := by + rw [MvPolynomial.natDegree_optionEquivLeft] + simpa [Q, e] using + (MvPolynomial.degreeOf_rename_of_injective + (p := P) e.injective (Sum.inr default)) + have hpoly : + MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) + (specializeLeft x P) = + Polynomial.map (MvPolynomial.eval x) + (MvPolynomial.optionEquivLeft ℂ τ Q) := by + apply Polynomial.funext + intro y + change Polynomial.eval₂ (RingHom.id ℂ) y + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) + (specializeLeft x P)) = + Polynomial.eval y + (Polynomial.map (MvPolynomial.eval x) + (MvPolynomial.optionEquivLeft ℂ τ Q)) + rw [MvPolynomial.eval₂_const_uniqueAlgEquiv] + change MvPolynomial.eval (fun _ : Fin 1 => y) + (specializeLeft x P) = _ + rw [eval_specializeLeft] + calc + MvPolynomial.eval (Sum.elim x fun _ => y) P = + MvPolynomial.eval + (fun o => Option.elim o y x) Q := by + dsimp [Q] + rw [MvPolynomial.eval_rename] + apply congrArg (fun z => MvPolynomial.eval z P) + funext i + cases i <;> rfl + _ = Polynomial.eval y + (Polynomial.map (MvPolynomial.eval x) + (MvPolynomial.optionEquivLeft ℂ τ Q)) := + MvPolynomial.optionEquivLeft_elim_eval ℂ τ x y Q + rw [hpoly, ← hQdeg] + exact Polynomial.natDegree_map_le + /-- Specializing the left block inside its regions preserves stability in the right coordinate regions. -/ theorem MvStableIn.specializeLeft diff --git a/RealRooted/PartialSymmetrization.lean b/RealRooted/PartialSymmetrization.lean new file mode 100644 index 000000000..32c090433 --- /dev/null +++ b/RealRooted/PartialSymmetrization.lean @@ -0,0 +1,253 @@ +import Mathlib +import RealRooted.Multiaffine +import RealRooted.MultivariateStability + +/-! +# Partial symmetrization + +This file develops the bivariate coefficient identities used in the +Borcea--Brändén proof that transposition averages preserve stability. +-/ + +namespace RealRooted + +open MvPolynomial + +/-- The first real quadratic form from Borcea--Brändén, Part II, Lemma 1.4. -/ +def bivariateV1 (a b c d : ℂ) (x : ℝ) : ℝ := + (a * star c).im + (a * star d + b * star c).im * x + + (b * star d).im * x ^ 2 + +/-- The second real quadratic form from Borcea--Brändén, Part II, Lemma 1.4. -/ +def bivariateV2 (a b c d : ℂ) (x : ℝ) : ℝ := + bivariateV1 a c b d x + +/-- The four-coefficient bivariate multiaffine polynomial used in Part II, +Lemma 1.4. -/ +noncomputable def bivariateMultiaffinePolynomial (a b c d : ℂ) : + MvPolynomial (Fin 2) ℂ := + C a + C b * X 0 + C c * X 1 + C d * X 0 * X 1 + +/-- Evaluation of the four-coefficient bivariate multiaffine polynomial. -/ +theorem eval_bivariateMultiaffinePolynomial + (a b c d : ℂ) (z : Fin 2 → ℂ) : + MvPolynomial.eval z (bivariateMultiaffinePolynomial a b c d) = + a + b * z 0 + c * z 1 + d * z 0 * z 1 := by + simp [bivariateMultiaffinePolynomial] + +/-- The real-boundary quotient identity for `bivariateV1` from +Borcea--Brändén, Part II, Lemma 1.4. -/ +theorem im_bivariateQuotient_eq_bivariateV1_div_normSq + (a b c d : ℂ) (x : ℝ) : + ((a + b * (x : ℂ)) / (c + d * (x : ℂ))).im = + bivariateV1 a b c d x / + Complex.normSq (c + d * (x : ℂ)) := by + simp [Complex.div_im, Complex.normSq, bivariateV1] + ring + +/-- The symmetric real-boundary quotient identity for `bivariateV2` from +Borcea--Brändén, Part II, Lemma 1.4. -/ +theorem im_bivariateQuotient_eq_bivariateV2_div_normSq + (a b c d : ℂ) (x : ℝ) : + ((a + c * (x : ℂ)) / (b + d * (x : ℂ))).im = + bivariateV2 a b c d x / + Complex.normSq (b + d * (x : ℂ)) := by + exact im_bivariateQuotient_eq_bivariateV1_div_normSq a c b d x + +/-- A positive imaginary part of `c / d` keeps `c + d * z` nonzero on the +closed upper half-plane. This is the denominator observation in Part II, +Lemma 1.4. -/ +theorem right_ne_zero_of_im_div_pos + (c d : ℂ) (h : 0 < (c / d).im) : d ≠ 0 := by + intro hd + simp [hd] at h + +/-- A positive imaginary part of `c / d` keeps `c + d * z` nonzero on the +closed upper half-plane. This is the denominator observation in Part II, +Lemma 1.4. -/ +theorem add_mul_ne_zero_of_im_div_pos + (c d z : ℂ) (h : 0 < (c / d).im) (hz : 0 ≤ z.im) : + c + d * z ≠ 0 := by + intro hzero + have hd := right_ne_zero_of_im_div_pos c d h + have hratio : c / d = -z := by + apply (div_eq_iff hd).2 + linear_combination hzero + rw [hratio] at h + simp at h + linarith + +/-- The real-boundary specialization of +`add_mul_ne_zero_of_im_div_pos`. -/ +theorem add_mul_real_ne_zero_of_im_div_pos + (c d : ℂ) (x : ℝ) (h : 0 < (c / d).im) : + c + d * (x : ℂ) ≠ 0 := by + exact add_mul_ne_zero_of_im_div_pos c d x h (by simp) + +/-- When the cross determinant vanishes, the solved quotient is the constant +`b / d`. This is the constant branch in Part II, Lemma 1.4. -/ +theorem bivariateQuotient_eq_b_div + (a b c d z : ℂ) (hcross : a * d = b * c) + (hd : d ≠ 0) (hden : c + d * z ≠ 0) : + (a + b * z) / (c + d * z) = b / d := by + apply (div_eq_iff hden).2 + field_simp [hd] + linear_combination hcross + +/-- In the constant branch, positivity at infinity gives strict quotient +positivity throughout the closed upper half-plane. -/ +theorem bivariateQuotient_im_pos_of_cross_eq + (a b c d z : ℂ) (hcross : a * d = b * c) + (hbd : 0 < (b / d).im) (hcd : 0 < (c / d).im) + (hz : 0 ≤ z.im) : + 0 < ((a + b * z) / (c + d * z)).im := by + rw [bivariateQuotient_eq_b_div a b c d z hcross + (right_ne_zero_of_im_div_pos b d hbd) + (add_mul_ne_zero_of_im_div_pos c d z hcd hz)] + exact hbd + +/-- A nonzero cross determinant makes the quotient take different values at +`z` and `z + 1`, provided both denominators are nonzero. -/ +theorem bivariateQuotient_ne_add_one + (a b c d z : ℂ) (hcross : a * d ≠ b * c) + (hden : c + d * z ≠ 0) (hden1 : c + d * (z + 1) ≠ 0) : + (a + b * z) / (c + d * z) ≠ + (a + b * (z + 1)) / (c + d * (z + 1)) := by + intro heq + have hmul := (div_eq_div_iff hden hden1).mp heq + apply hcross + linear_combination hmul + +/-- Under the denominator half-plane hypothesis, a nonzero cross determinant +gives an explicit nonconstancy witness within the same closed half-plane. -/ +theorem bivariateQuotient_ne_add_one_of_im_div_pos + (a b c d z : ℂ) (hcross : a * d ≠ b * c) + (hcd : 0 < (c / d).im) (hz : 0 ≤ z.im) : + (a + b * z) / (c + d * z) ≠ + (a + b * (z + 1)) / (c + d * (z + 1)) := by + apply bivariateQuotient_ne_add_one a b c d z hcross + · exact add_mul_ne_zero_of_im_div_pos c d z hcd hz + · apply add_mul_ne_zero_of_im_div_pos c d (z + 1) hcd + simpa using hz + +/-- Solving a bivariate multiaffine expression for its second variable, as in +the proof of Borcea--Brändén, Part II, Lemma 1.4. -/ +theorem bivariate_eq_factor_quotient + (a b c d z w : ℂ) (hden : c + d * z ≠ 0) : + a + b * z + c * w + d * z * w = + (c + d * z) * (w + (a + b * z) / (c + d * z)) := by + calc + a + b * z + c * w + d * z * w = + (c + d * z) * w + (a + b * z) := by ring + _ = (c + d * z) * w + + (c + d * z) * ((a + b * z) / (c + d * z)) := by + rw [mul_div_cancel₀ (a + b * z) hden] + _ = (c + d * z) * (w + (a + b * z) / (c + d * z)) := by ring + +/-- With a nonzero denominator, the bivariate expression has the unique +second-variable zero used in equation (1.2) of Part II. -/ +theorem bivariate_eq_zero_iff + (a b c d z w : ℂ) (hden : c + d * z ≠ 0) : + a + b * z + c * w + d * z * w = 0 ↔ + w = -((a + b * z) / (c + d * z)) := by + rw [bivariate_eq_factor_quotient a b c d z w hden] + simp only [mul_eq_zero, hden, false_or] + constructor <;> intro h <;> linear_combination h + +/-- Positive imaginary part of the solved quotient excludes a zero with the +second variable in the upper half-plane. -/ +theorem bivariate_ne_zero_of_quotient_im_pos + (a b c d z w : ℂ) (hden : c + d * z ≠ 0) + (hq : 0 < ((a + b * z) / (c + d * z)).im) (hw : 0 < w.im) : + a + b * z + c * w + d * z * w ≠ 0 := by + intro hzero + have hroot := (bivariate_eq_zero_iff a b c d z w hden).mp hzero + rw [hroot] at hw + simp at hw + linarith + +/-- The source's quotient-positivity condition implies bivariate nonvanishing +on the upper half-plane. This is the algebraic direction preceding (1.2). -/ +theorem bivariate_ne_zero_of_im_div_pos_of_quotient_im_pos + (a b c d z w : ℂ) (hcd : 0 < (c / d).im) (hz : 0 ≤ z.im) + (hq : 0 < ((a + b * z) / (c + d * z)).im) (hw : 0 < w.im) : + a + b * z + c * w + d * z * w ≠ 0 := by + exact bivariate_ne_zero_of_quotient_im_pos a b c d z w + (add_mul_ne_zero_of_im_div_pos c d z hcd hz) hq hw + +/-- The quotient-positivity condition in (1.2) implies upper-half-plane +stability of the corresponding bivariate multiaffine polynomial. -/ +theorem mvUpperHalfPlaneStable_bivariate_of_quotient_im_pos + (a b c d : ℂ) (hcd : 0 < (c / d).im) + (hq : ∀ z : ℂ, 0 < z.im → + 0 < ((a + b * z) / (c + d * z)).im) : + MvUpperHalfPlaneStable (bivariateMultiaffinePolynomial a b c d) := by + intro z hz + rw [eval_bivariateMultiaffinePolynomial] + exact bivariate_ne_zero_of_im_div_pos_of_quotient_im_pos + a b c d (z 0) (z 1) hcd (le_of_lt (hz 0)) (hq (z 0) (hz 0)) (hz 1) + +/-- Stability forces the solved quotient into the closed upper half-plane. +Upgrading this weak inequality to strict positivity is the separate +open-mapping step in the proof of Part II, Lemma 1.4. -/ +theorem quotient_im_nonneg_of_mvUpperHalfPlaneStable_bivariate + (a b c d : ℂ) + (hP : MvUpperHalfPlaneStable (bivariateMultiaffinePolynomial a b c d)) + (hcd : 0 < (c / d).im) (z : ℂ) (hz : 0 < z.im) : + 0 ≤ ((a + b * z) / (c + d * z)).im := by + by_contra hq + let w := -((a + b * z) / (c + d * z)) + have hw : 0 < w.im := by + dsimp [w] + simp + linarith + have hstable := hP ![z, w] (by + intro i + fin_cases i <;> simp_all) + rw [eval_bivariateMultiaffinePolynomial] at hstable + exact hstable ((bivariate_eq_zero_iff a b c d z w + (add_mul_ne_zero_of_im_div_pos c d z hcd (le_of_lt hz))).2 rfl) + +/-- On the real boundary, positivity of the first quotient imaginary part is +equivalent to positivity of `bivariateV1` when its denominator stays off zero. -/ +theorem im_bivariateQuotient_pos_iff_bivariateV1_pos + (a b c d : ℂ) (x : ℝ) (h : 0 < (c / d).im) : + 0 < ((a + b * (x : ℂ)) / (c + d * (x : ℂ))).im ↔ + 0 < bivariateV1 a b c d x := by + have hden := add_mul_real_ne_zero_of_im_div_pos c d x h + have hnorm : 0 < Complex.normSq (c + d * (x : ℂ)) := + Complex.normSq_pos.mpr hden + rw [im_bivariateQuotient_eq_bivariateV1_div_normSq] + exact div_pos_iff_of_pos_right hnorm + +/-- The symmetric real-boundary positivity equivalence for `bivariateV2`. -/ +theorem im_bivariateQuotient_pos_iff_bivariateV2_pos + (a b c d : ℂ) (x : ℝ) (h : 0 < (b / d).im) : + 0 < ((a + c * (x : ℂ)) / (b + d * (x : ℂ))).im ↔ + 0 < bivariateV2 a b c d x := by + exact im_bivariateQuotient_pos_iff_bivariateV1_pos a c b d x h + +/-- Under partial transposition averaging, V1 is the corresponding convex +combination of the original V1 and V2. -/ +theorem bivariateV1_partialSymmetrization + (a b c d : ℂ) (t x : ℝ) : + bivariateV1 a + ((t : ℂ) * b + (1 - t : ℝ) * c) + ((t : ℂ) * c + (1 - t : ℝ) * b) d x = + t * bivariateV1 a b c d x + + (1 - t) * bivariateV2 a b c d x := by + simp [bivariateV1, bivariateV2, Complex.mul_im] + ring + +/-- Under partial transposition averaging, V2 is the corresponding convex +combination of the original V2 and V1. -/ +theorem bivariateV2_partialSymmetrization + (a b c d : ℂ) (t x : ℝ) : + bivariateV2 a + ((t : ℂ) * b + (1 - t : ℝ) * c) + ((t : ℂ) * c + (1 - t : ℝ) * b) d x = + t * bivariateV2 a b c d x + + (1 - t) * bivariateV1 a b c d x := by + exact bivariateV1_partialSymmetrization a c b d t x + +end RealRooted diff --git a/RealRooted/Polarization.lean b/RealRooted/Polarization.lean index 650b35f10..0cfc1f089 100644 --- a/RealRooted/Polarization.lean +++ b/RealRooted/Polarization.lean @@ -1,6 +1,9 @@ +import RealRooted.Mathlib.Algebra.MvPolynomial.Degrees +import RealRooted.Mathlib.Algebra.MvPolynomial.Equiv +import RealRooted.Mathlib.Algebra.MvPolynomial.Stability.DegreeBox import Mathlib.RingTheory.Polynomial.Vieta import RealRooted.GraceHalfPlane -import RealRooted.Multiaffine +import RealRooted.PartialSymmetrization import RealRooted.MultivariateStability /-! @@ -56,6 +59,58 @@ elementary symmetric polynomial is `p.coeff k / choose n k`. -/ def polarization (n : ℕ) (p : ℂ[X]) : MvPolynomial (Fin n) ℂ := reducedPolarization n (binomialUnlift n p) +private theorem binomialUnlift_add (n : ℕ) (p q : ℂ[X]) : + binomialUnlift n (p + q) = + binomialUnlift n p + binomialUnlift n q := by + unfold binomialUnlift + rw [← Finset.sum_add_distrib] + apply Finset.sum_congr rfl + intro k _ + rw [Polynomial.coeff_add, add_div, map_add] + +private theorem binomialUnlift_smul (n : ℕ) (c : ℂ) (p : ℂ[X]) : + binomialUnlift n (c • p) = c • binomialUnlift n p := by + unfold binomialUnlift + rw [Finset.smul_sum] + apply Finset.sum_congr rfl + intro k _ + simp only [Polynomial.coeff_smul, div_eq_mul_inv] + change (Polynomial.monomial k) + (c * p.coeff k * (n.choose k : ℂ)⁻¹) = + c • (Polynomial.monomial k) + (p.coeff k * (n.choose k : ℂ)⁻¹) + rw [mul_assoc] + exact (Polynomial.smul_monomial c k + (p.coeff k * (n.choose k : ℂ)⁻¹)).symm + +private theorem reducedPolarization_add (n : ℕ) (p q : ℂ[X]) : + reducedPolarization n (p + q) = + reducedPolarization n p + reducedPolarization n q := by + unfold reducedPolarization + rw [← Finset.sum_add_distrib] + apply Finset.sum_congr rfl + intro k _ + simp [add_mul] + +private theorem reducedPolarization_smul (n : ℕ) (c : ℂ) (p : ℂ[X]) : + reducedPolarization n (c • p) = c • reducedPolarization n p := by + unfold reducedPolarization + rw [Finset.smul_sum] + apply Finset.sum_congr rfl + intro k _ + simp [MvPolynomial.smul_eq_C_mul, mul_assoc] + +/-- Polarization as a complex-linear map on univariate polynomials. -/ +noncomputable def polarizationLinearMap (n : ℕ) : + ℂ[X] →ₗ[ℂ] MvPolynomial (Fin n) ℂ where + toFun := polarization n + map_add' p q := by + change polarization n (p + q) = polarization n p + polarization n q + simp only [polarization, binomialUnlift_add, reducedPolarization_add] + map_smul' c p := by + change polarization n (c • p) = c • polarization n p + simp only [polarization, binomialUnlift_smul, reducedPolarization_smul] + theorem isMultiaffine_reducedPolarization (n : ℕ) (p : ℂ[X]) : MvPolynomial.IsMultiaffine (reducedPolarization n p) := by unfold reducedPolarization @@ -116,6 +171,149 @@ theorem eval_polarization_const {n : ℕ} {p : ℂ[X]} (hp : p.natDegree ≤ n) unfold polarization rw [eval_reducedPolarization_const, binomialLift_binomialUnlift hp] +/-- Renaming every polarization variable to the unique variable reconstructs +the original univariate polynomial. This is the diagonal identity for +polarization. -/ +theorem rename_polarization_const {n : ℕ} {p : ℂ[X]} + (hp : p.natDegree ≤ n) : + MvPolynomial.rename (fun _ : Fin n ↦ (0 : Fin 1)) (polarization n p) = + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm p := by + apply (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).injective + rw [AlgEquiv.apply_symm_apply] + apply Polynomial.funext + intro w + change Polynomial.eval₂ (RingHom.id ℂ) w + ((MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)) + (MvPolynomial.rename (fun _ : Fin n ↦ (0 : Fin 1)) + (polarization n p))) = p.eval w + rw [MvPolynomial.eval₂_const_uniqueAlgEquiv] + rw [MvPolynomial.eval₂_rename] + change MvPolynomial.eval (fun _ : Fin n ↦ w) (polarization n p) = p.eval w + exact eval_polarization_const hp w + +/-- Package polarization as the multiaffine source polynomial +`Π↑ₙ p` in the all-ones degree box. -/ +noncomputable def polarizationDegreeBox (n : ℕ) (p : ℂ[X]) : + MvPolynomial.degreeOfLE (Fin n) ℂ (fun _ => 1) := + ⟨polarization n p, + (MvPolynomial.mem_degreeOfLE_iff_degreeOf (polarization n p)).2 + (isMultiaffine_polarization n p)⟩ + +@[simp] +theorem coe_polarizationDegreeBox (n : ℕ) (p : ℂ[X]) : + (polarizationDegreeBox n p : MvPolynomial (Fin n) ℂ) = polarization n p := rfl + +/-- Source polarization `Π↑ₙ` as a linear map from the one-variable degree-`n` +box to the multiaffine all-ones box. -/ +noncomputable def polarizationDegreeBoxLinearMap (n : ℕ) : + MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] + MvPolynomial.degreeOfLE (Fin n) ℂ (fun _ => 1) := + LinearMap.codRestrict (MvPolynomial.degreeOfLE (Fin n) ℂ (fun _ => 1)) + ((polarizationLinearMap n).comp + ((MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).toLinearMap.domRestrict + (MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => n)))) + (fun q => + (MvPolynomial.mem_degreeOfLE_iff_degreeOf _).2 + (isMultiaffine_polarization n + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) q.1))) + +/-- The diagonal projection `Π↓ₙ`, obtained by identifying every polarization +variable with the unique univariate variable. -/ +noncomputable def diagonalProjection (n : ℕ) : + MvPolynomial (Fin n) ℂ →ₗ[ℂ] ℂ[X] where + toFun q := + MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) + (MvPolynomial.rename (fun _ : Fin n => (0 : Fin 1)) q) + map_add' q r := by simp + map_smul' c q := by + simp [MvPolynomial.smul_eq_C_mul, Polynomial.smul_eq_C_mul] + +/-- Diagonal projection of an all-ones degree-box polynomial has degree at +most the size of its polarization block. -/ +theorem natDegree_diagonalProjection_le {n : ℕ} + (q : MvPolynomial.degreeOfLE (Fin n) ℂ (fun _ => 1)) : + (diagonalProjection n q).natDegree ≤ n := by + have hdeg : ∀ i, q.1.degreeOf i ≤ 1 := + (MvPolynomial.mem_degreeOfLE_iff_degreeOf q.1).mp q.2 + change (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) + (MvPolynomial.rename (fun _ : Fin n => (0 : Fin 1)) q.1)).natDegree ≤ n + calc + _ ≤ (MvPolynomial.rename (fun _ : Fin n => (0 : Fin 1)) q.1).totalDegree := + MvPolynomial.natDegree_uniqueAlgEquiv_le_totalDegree _ + _ ≤ q.1.totalDegree := MvPolynomial.totalDegree_rename_le _ _ + _ ≤ ∑ i, q.1.degreeOf i := MvPolynomial.totalDegree_le_sum_degreeOf q.1 + _ ≤ ∑ _ : Fin n, 1 := Finset.sum_le_sum fun i _ => hdeg i + _ = n := by simp + +/-- Diagonal projection as a linear map from the multiaffine source box to the +original one-variable degree box. This is the source-side map `Π↓ₙ`. -/ +noncomputable def diagonalProjectionDegreeBox (n : ℕ) : + MvPolynomial.degreeOfLE (Fin n) ℂ (fun _ => 1) →ₗ[ℂ] + MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => n) := + LinearMap.codRestrict (MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => n)) + (((MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm.toLinearMap.comp + (diagonalProjection n)).domRestrict + (MvPolynomial.degreeOfLE (Fin n) ℂ (fun _ => 1))) + (fun q => by + apply (MvPolynomial.mem_degreeOfLE_iff_degreeOf _).2 + intro i + change MvPolynomial.degreeOf i + ((MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm + (diagonalProjection n q)) ≤ n + rw [Unique.eq_default i, + MvPolynomial.degreeOf_uniqueAlgEquiv_symm] + exact natDegree_diagonalProjection_le q) + +/-- Equation (2.2) on the source side: diagonal projection is a left inverse +to polarization on polynomials of degree at most `n`. -/ +theorem diagonalProjection_polarizationDegreeBox {n : ℕ} {p : ℂ[X]} + (hp : p.natDegree ≤ n) : + diagonalProjection n (polarizationDegreeBox n p) = p := by + change MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) + (MvPolynomial.rename (fun _ : Fin n => (0 : Fin 1)) (polarization n p)) = p + rw [rename_polarization_const hp] + exact (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).apply_symm_apply p + +/-- Degree-box form of the source reconstruction identity +`Π↓ₙ (Π↑ₙ p) = p`. -/ +theorem coe_diagonalProjectionDegreeBox_polarizationDegreeBox + {n : ℕ} {p : ℂ[X]} (hp : p.natDegree ≤ n) : + (diagonalProjectionDegreeBox n (polarizationDegreeBox n p) : + MvPolynomial (Fin 1) ℂ) = + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm p := by + change (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm + (diagonalProjection n (polarizationDegreeBox n p)) = + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm p + rw [diagonalProjection_polarizationDegreeBox hp] + +/-- Source-side equation (2.2): diagonal projection is a left inverse to the +linear polarization map on the one-variable degree box. -/ +theorem diagonalProjectionDegreeBox_comp_polarizationDegreeBoxLinearMap + {n : ℕ} + (q : MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => n)) : + diagonalProjectionDegreeBox n (polarizationDegreeBoxLinearMap n q) = q := by + have hdeg : ∀ i, q.1.degreeOf i ≤ n := + (MvPolynomial.mem_degreeOfLE_iff_degreeOf q.1).mp q.2 + have hp : (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) q.1).natDegree ≤ n := by + calc + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) q.1).natDegree = + q.1.degreeOf default := by + simpa only [AlgEquiv.symm_apply_apply] using + (MvPolynomial.degreeOf_uniqueAlgEquiv_symm (σ := Fin 1) + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) q.1)).symm + _ ≤ n := hdeg default + have hdiag : + diagonalProjection n + (polarization n (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) q.1)) = + MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) q.1 := + diagonalProjection_polarizationDegreeBox hp + apply Subtype.ext + change (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm + (diagonalProjection n + (polarization n (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) q.1))) = q.1 + rw [hdiag] + exact (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm_apply_apply q.1 + /-- Evaluation of a polarization in elementary symmetric functions. -/ theorem eval_polarization (n : ℕ) (p : ℂ[X]) (z : Fin n → ℂ) : MvPolynomial.eval z (polarization n p) = @@ -195,8 +393,12 @@ theorem eval_reducedPolarization_eq_apolarPairing_of_binomialLift_eq_rootPolynom /-- Grace--Walsh--Szego for reduced coefficients: exact-degree upper-half-plane stability is preserved by polarization. -/ +/- Borcea--Branden, arXiv:0809.0401, Proposition 2.4. The source polynomial +has degree at most `n`; exact degree is unnecessary because the upper half-plane +is a convex circular domain in the Grace--Walsh--Szego theorem. The auxiliary +root polynomial used below still has exact degree `n`. -/ theorem mvUpperHalfPlaneStable_reducedPolarization {n : ℕ} {f : ℂ[X]} - (hdeg : (binomialLift n f).natDegree = n) + (hdeg : (binomialLift n f).natDegree ≤ n) (hstable : ∀ w : ℂ, 0 < w.im → (binomialLift n f).eval w ≠ 0) : MvUpperHalfPlaneStable (reducedPolarization n f) := by intro z hz hzero @@ -221,14 +423,100 @@ theorem mvUpperHalfPlaneStable_reducedPolarization {n : ℕ} {f : ℂ[X]} /-- Exact-degree upper-half-plane stability is preserved by univariate polarization. -/ theorem mvUpperHalfPlaneStable_polarization {n : ℕ} {p : ℂ[X]} - (hdeg : p.natDegree = n) + (hdeg : p.natDegree ≤ n) (hstable : ∀ w : ℂ, 0 < w.im → p.eval w ≠ 0) : MvUpperHalfPlaneStable (polarization n p) := by unfold polarization apply mvUpperHalfPlaneStable_reducedPolarization - · rw [binomialLift_binomialUnlift hdeg.le, hdeg] - · simpa [binomialLift_binomialUnlift hdeg.le] using hstable + · simpa only [binomialLift_binomialUnlift hdeg] using hdeg + · simpa only [binomialLift_binomialUnlift hdeg] using hstable end +/-- Diagonal projection sends a bounded multiaffine basis monomial to the +univariate monomial whose exponent is its total degree. -/ +theorem diagonalProjection_basisDegreeOfLE {n : ℕ} + (m : {m : Fin n →₀ ℕ // ∀ i, m i ≤ 1}) : + diagonalProjection n + (MvPolynomial.basisDegreeOfLE (R := ℂ) (fun _ : Fin n => 1) m) = + Polynomial.X ^ m.1.degree := by + change MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) + (MvPolynomial.rename (fun _ : Fin n => (0 : Fin 1)) + ((MvPolynomial.basisDegreeOfLE (R := ℂ) + (fun _ : Fin n => 1) m : + MvPolynomial.degreeOfLE (Fin n) ℂ (fun _ => 1)) : + MvPolynomial (Fin n) ℂ)) = + Polynomial.X ^ m.1.degree + rw [MvPolynomial.coe_basisDegreeOfLE] + rw [MvPolynomial.rename_monomial, MvPolynomial.uniqueAlgEquiv_monomial] + rw [Polynomial.X_pow_eq_monomial] + apply congrArg (fun k : ℕ => Polynomial.monomial k (1 : ℂ)) + calc + (Finsupp.mapDomain (fun _ : Fin n => (0 : Fin 1)) m.1) default = + m.1.sum (fun _ e => e) := by + simp [Finsupp.mapDomain, Finsupp.sum_apply] + _ = m.1.degree := by + rw [Finsupp.degree_apply] + rfl + +private theorem degree_le_fin_card_of_le_one {n : ℕ} + (m : Fin n →₀ ℕ) (hm : ∀ i, m i ≤ 1) : + m.degree ≤ n := by + rw [Finsupp.degree_apply] + calc + ∑ i ∈ m.support, m i ≤ ∑ i ∈ m.support, 1 := + Finset.sum_le_sum fun i hi => hm i + _ = m.support.card := by simp + _ ≤ Fintype.card (Fin n) := Finset.card_le_univ m.support + _ = n := Fintype.card_fin n + +/-- The one-variable degree-box index obtained by diagonalizing a bounded +multiaffine exponent vector. -/ +noncomputable def diagonalDegreeBoxIndex {n : ℕ} + (m : {m : Fin n →₀ ℕ // ∀ i, m i ≤ 1}) : + {d : Fin 1 →₀ ℕ // ∀ i, d i ≤ n} := + ⟨Finsupp.single default m.1.degree, fun i => by + rw [Subsingleton.elim i default, Finsupp.single_eq_same] + exact degree_le_fin_card_of_le_one m.1 m.2⟩ + +/-- Diagonal projection on degree boxes sends a multiaffine basis monomial to +the one-variable basis monomial indexed by its total degree. -/ +theorem diagonalProjectionDegreeBox_basisDegreeOfLE {n : ℕ} + (m : {m : Fin n →₀ ℕ // ∀ i, m i ≤ 1}) : + diagonalProjectionDegreeBox n + (MvPolynomial.basisDegreeOfLE (R := ℂ) (fun _ : Fin n => 1) m) = + MvPolynomial.basisDegreeOfLE (R := ℂ) (fun _ : Fin 1 => n) + (diagonalDegreeBoxIndex m) := by + apply Subtype.ext + change (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm + (diagonalProjection n + (MvPolynomial.basisDegreeOfLE (R := ℂ) (fun _ : Fin n => 1) m)) = + ((MvPolynomial.basisDegreeOfLE (R := ℂ) (fun _ : Fin 1 => n) + (diagonalDegreeBoxIndex m) : + MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => n)) : + MvPolynomial (Fin 1) ℂ) + apply (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).injective + rw [AlgEquiv.apply_symm_apply, diagonalProjection_basisDegreeOfLE, + MvPolynomial.coe_basisDegreeOfLE, + MvPolynomial.uniqueAlgEquiv_monomial] + simp [diagonalDegreeBoxIndex, Polynomial.X_pow_eq_monomial] + +end RealRooted + +namespace RealRooted + +/-- Reduced polarization is symmetric in its polarized variables. -/ +theorem isSymmetric_reducedPolarization (n : ℕ) (f : ℂ[X]) : + MvPolynomial.IsSymmetric (reducedPolarization n f) := by + classical + intro e + simp only [reducedPolarization, map_sum, map_mul, + MvPolynomial.rename_C, MvPolynomial.rename_esymm] + +/-- Polarization is symmetric in its polarized variables. -/ +theorem isSymmetric_polarization (n : ℕ) (p : ℂ[X]) : + MvPolynomial.IsSymmetric (polarization n p) := by + unfold polarization + exact isSymmetric_reducedPolarization n (binomialUnlift n p) + end RealRooted diff --git a/RealRooted/RectangularPolarization.lean b/RealRooted/RectangularPolarization.lean index 27c9e7649..18fd92efa 100644 --- a/RealRooted/RectangularPolarization.lean +++ b/RealRooted/RectangularPolarization.lean @@ -262,7 +262,7 @@ theorem upperHalfPlaneStable_rectangularLeftSlice exact mvUpperHalfPlaneStable_polarization (natDegree_rectangularRightSlice_eq hpdeg hplead (fun hzero => by rw [hzero] at hx - simp at hx)) + simp at hx)).le (upperHalfPlaneStable_rectangularRightSlice hpdeg.le hstable hx) y hy /-- Rectangular polarization preserves upper-half-plane stability. This is the @@ -279,8 +279,8 @@ theorem mvUpperHalfPlaneStable_rectangularPolarization cases i <;> rfl rw [hz_elim, eval_rectangularPolarization_eq_eval_polarization_leftSlice] apply mvUpperHalfPlaneStable_polarization - · exact natDegree_rectangularLeftSlice_eq hpdeg hplead - (fun i => hz (Sum.inr i)) + · exact (natDegree_rectangularLeftSlice_eq hpdeg hplead + (fun i => hz (Sum.inr i))).le · exact upperHalfPlaneStable_rectangularLeftSlice hpdeg hplead hstable (fun i => hz (Sum.inr i)) · exact fun i => hz (Sum.inl i)