diff --git a/PROOF_STATUS.md b/PROOF_STATUS.md index be689ece9..efd413aae 100644 --- a/PROOF_STATUS.md +++ b/PROOF_STATUS.md @@ -19,16 +19,9 @@ theorem, refutation, or production caller. They contain no admission. | `HurwitzOddEvenToReverseFullyInterlacingPairStatement` | Proposed reverse-row replacement for the refuted legacy Hurwitz-to-Lace orientation | | `HurwitzOddEvenToHermiteBiehlerStableStatement` | Converse of the conformal substitution `hermiteBiehlerStableToHurwitzOddEven`; input to `strictInterl_of_isHurwitzStable_oddEvenPolynomial` | | `HermiteBiehlerConverseOrientedStatement` | Oriented converse Hermite--Biehler theorem; the checked `hermiteBiehlerConverse` is disjunctive | +| `hadamardPreservesHurwitzStableStatement` | Garloff--Wagner Theorem 1, Hadamard products preserve Hurwitz stability; issue #1095 | | `iterateThetaPlusOneSelfInterlStatement` | Unused open interlacing target for iterates of `theta + 1` | -The following historical row-orientation interfaces in -`RealRooted.VeroneseSection` have no checked proof and are expected to be false -(numerically, `lacePair (X + 1).coeff (X + 2).coeff` has no negative minor). -They remain only because other modules still take them as hypotheses: -`FullyInterlacingPairToInterlStatement` (`RealRooted.Hadamard.Consequences`) and -`LegacyFullyInterlacingPairToHurwitzOddEvenStableStatement` -(`RealRooted.HurwitzMatrix`). - ## Checked replacements | Topic | Checked declaration | @@ -55,15 +48,12 @@ They remain only because other modules still take them as hypotheses: ## Refuted interfaces retained as counterexamples The following propositions remain only beside checked proofs of their -negations. The two Veronese-section `Legacy` propositions are still mentioned -by vacuous conditional theorems in `RealRooted.Hadamard.Consequences`. +negations. | Proposition | Checked negation | | --- | --- | | `theorem21CompatibleToRootCountBranchesNonconstantStatement` | `not_theorem21CompatibleToRootCountBranchesNonconstantStatement` | | `LegacyHurwitzMatrixTotallyNonnegativeToStableStatement` | `not_hurwitzMatrixTotallyNonnegativeToStableStatement` | -| `LegacyNonnegStrictInterlToFullyInterlacingPairStatement` | `not_legacyNonnegStrictInterlToFullyInterlacingPairStatement` | -| `LegacyHurwitzOddEvenToFullyInterlacingPairStatement` | `not_hurwitzOddEvenToFullyInterlacingPairStatement` | The former homogeneous finite-symbol route was removed entirely because its checked counterexample and the affine-symbol replacement make its conditional diff --git a/RealRooted/Challenges/HurwitzCornerZeroedCounterexample.lean b/RealRooted/Challenges/HurwitzCornerZeroedCounterexample.lean index ef8f3e659..95d225029 100644 --- a/RealRooted/Challenges/HurwitzCornerZeroedCounterexample.lean +++ b/RealRooted/Challenges/HurwitzCornerZeroedCounterexample.lean @@ -3,23 +3,23 @@ import RealRooted.HurwitzMatrix /-! # A corner-zeroed Hurwitz-minor counterexample -This file records checked arithmetic showing that the one-matrix full-band -corner-zeroed route to the Hurwitz Schur-product problem (issue #34) is too -strong. For the -coefficient sequence +This file records checked arithmetic showing that a one-matrix full-band +corner-zeroed inequality for Hurwitz minors fails. For the coefficient +sequence ```text [1, 1, 8, 10, 17, 31, 10, 30] ``` -and the window with rows `6, 7, 8` and columns `0, 1, 2`, all non-total- -nonnegativity side hypotheses of the single-matrix full-band corner-zeroed -statement hold, the full `3 × 3` determinant is `2000`, but the corner-zeroed -expression is `-1000`. +and the window with rows `6, 7, 8` and columns `0, 1, 2`, all band side +conditions of the single-matrix full-band corner-zeroed inequality hold, the +full `3 × 3` determinant is `2000`, but the corner-zeroed expression is +`-1000`. This module does not formalize the infinite total-nonnegativity witness for the -sequence. It is a checked arithmetic diagnostic for the failed one-matrix -reduction route; it does not refute the two-matrix Schur-product target. +sequence; it is a checked arithmetic diagnostic. The two-matrix +Schur-product statement for infinite Hurwitz matrices is refuted separately by +`RealRooted.not_hurwitz_schurProduct_det_fin_three_nonneg`. -/ namespace RealRooted.HurwitzCornerZeroedCounterexample @@ -40,7 +40,7 @@ def cols : Fin 3 → ℕ := ![0, 1, 2] def M (i j : ℕ) : ℝ := hurwitz cseq i j -/-- The corner-zeroed determinant expression in the single-matrix subtarget. -/ +/-- The corner-zeroed determinant expression of the window. -/ def cornerZeroed : ℝ := M 6 0 * (M 7 1 * M 8 2 - M 7 2 * M 8 1) - M 6 1 * (M 7 0 * M 8 2 - M 7 2 * M 8 0) @@ -57,7 +57,7 @@ theorem rows_strictMono : StrictMono rows := by decide /-- The selected column indices are strictly increasing. -/ theorem cols_strictMono : StrictMono cols := by decide -/-- The diagonal band hypotheses of the single-matrix subtarget hold. -/ +/-- The diagonal band hypotheses hold. -/ theorem band : ∀ l : Fin 3, 2 * cols l ≤ rows l := by decide /-- The `(0, 1)` full-band side hypothesis holds. -/ diff --git a/RealRooted/Challenges/TotallyNonnegativeHadamardObstruction.lean b/RealRooted/Challenges/TotallyNonnegativeHadamardObstruction.lean index 352698b09..646199efa 100644 --- a/RealRooted/Challenges/TotallyNonnegativeHadamardObstruction.lean +++ b/RealRooted/Challenges/TotallyNonnegativeHadamardObstruction.lean @@ -3,13 +3,11 @@ import RealRooted.HurwitzMatrix /-! # Totally nonnegative windows do not give the Hurwitz Schur product -This file records a small structural obstruction for the Hurwitz -Schur-product problem (issue #34). -The full Hurwitz Schur-product target is special to Hurwitz matrices: the -corresponding statement for arbitrary totally nonnegative `3` by `3` windows is -false. Thus a proof of the two-matrix Schur-product target must use the Hurwitz -staircase or Toeplitz relations between neighbouring entries, not only total -nonnegativity of the selected windows. +This file records a small structural obstruction for entrywise products of +totally nonnegative matrices: the Hadamard product of two totally nonnegative +`3` by `3` matrices can have negative determinant. For infinite Hurwitz +matrices the Schur-product statement also fails; see +`RealRooted.not_hurwitz_schurProduct_det_fin_three_nonneg`. -/ namespace RealRooted.TotallyNonnegativeHadamardObstruction @@ -95,8 +93,8 @@ theorem exists_totallyNonneg_hadamard_det_neg : ⟨aMat, bMat, aMat_isTotallyNonneg, bMat_isTotallyNonneg, by norm_num [hadamard_det_eq]⟩ -/-- The corner-zeroed Hadamard determinant shape used in the issue #34 -full-band target. -/ +/-- The `3 × 3` Hadamard determinant with the top-right corner contribution +deleted. -/ def hadamardCornerZeroedDet (a b : Matrix (Fin 3) (Fin 3) ℝ) : ℝ := (a 0 0 * b 0 0) * ((a 1 1 * b 1 1) * (a 2 2 * b 2 2) - (a 1 2 * b 1 2) * (a 2 1 * b 2 1)) - @@ -108,8 +106,8 @@ theorem hadamardCornerZeroedDet_eq : hadamardCornerZeroedDet aMat bMat = -2 := b simp [hadamardCornerZeroedDet, aMat, bMat] norm_num -/-- Even the corner-zeroed target cannot be proved from the selected window -minors alone. -/ +/-- Even the corner-zeroed Hadamard determinant can be negative for totally +nonnegative windows. -/ theorem exists_totallyNonneg_hadamardCornerZeroed_neg : ∃ a b : Matrix (Fin 3) (Fin 3) ℝ, a.IsTotallyNonneg ∧ b.IsTotallyNonneg ∧ hadamardCornerZeroedDet a b < 0 := diff --git a/RealRooted/ClassicalHurwitzMatrix/Stability/Rotation.lean b/RealRooted/ClassicalHurwitzMatrix/Stability/Rotation.lean index 9306c931e..4221d265d 100644 --- a/RealRooted/ClassicalHurwitzMatrix/Stability/Rotation.lean +++ b/RealRooted/ClassicalHurwitzMatrix/Stability/Rotation.lean @@ -54,7 +54,7 @@ theorem isRoot_rotateLeftHalfPlaneToUpper_I_mul_iff (p : ℝ[X]) (z : ℂ) : rw [hrotate] /-- Evaluation of the rotated odd/even polynomial at the negative square of -the new variable. This fixes the signs used by the Hermite--Biehler bridge. -/ +the new variable. This fixes the signs used in the Hermite--Biehler step. -/ theorem eval_rotateLeftHalfPlaneToUpper_oddEvenPolynomial (odd even : ℝ[X]) (z : ℂ) : (rotateLeftHalfPlaneToUpper (oddEvenPolynomial odd even)).eval z = diff --git a/RealRooted/GarloffWagner/Hadamard.lean b/RealRooted/GarloffWagner/Hadamard.lean index 9d93c6281..1ff1a8b02 100644 --- a/RealRooted/GarloffWagner/Hadamard.lean +++ b/RealRooted/GarloffWagner/Hadamard.lean @@ -7,38 +7,12 @@ noncomputable section namespace RealRooted /-! -# Garloff--Wagner Hadamard endpoint +# Garloff--Wagner Hadamard interlacing theorem The double-deleted Krein reduction and the final two-pair Hadamard interlacing theorem. -/ -/-- The remaining local core of Garloff--Wagner, Theorem 4(b), after the -fixed-factor cases are discharged: both factors are one-root-deleted Krein -summands. -/ -def gwSchurProductDoubleDeletedKreinStatement : Prop := - ∀ {g q f p : ℝ[X]} {u v : ℝ}, - IsPFPolynomial g → - IsPFPolynomial q → - g ≠ 0 → - q ≠ 0 → - g = (X - C u) * f → - q = (X - C v) * p → - Interl (gwSchurProduct f p) (gwSchurProduct g q) - -/-- Ordinary-Hadamard version of the double-deleted core in the proof of -Garloff--Wagner, Theorem 4(b). This is the statement matching the paragraph -which expands `((X - j)g) ⊙ ((X - u)q)` through `L`, `J`, and `D`. -/ -def gwHadamardProductDoubleDeletedKreinStatement : Prop := - ∀ {g q f p : ℝ[X]} {u v : ℝ}, - IsPFPolynomial g → - IsPFPolynomial q → - g ≠ 0 → - q ≠ 0 → - g = (X - C u) * f → - q = (X - C v) * p → - Interl (hadamardProduct f p) (hadamardProduct g q) - /-- First Schur term in Garloff--Wagner's double-deleted paragraph: the base Hadamard product precedes the `X`-shifted term. -/ theorem gwSchurProduct_firstDoubleDeletedTerm_interl @@ -80,10 +54,14 @@ theorem gwSchurProduct_secondDoubleDeletedTerm_interl simpa [hfactor, gwL_X_sub_C_mul] using hSchur /-- Garloff--Wagner's double-deleted compatibility paragraph in Theorem 4(b), -in the ordinary-Hadamard form needed for the two-pair theorem. -/ -theorem gwHadamardProductDoubleDeletedKrein : - gwHadamardProductDoubleDeletedKreinStatement := by - intro g q f p u v hg hq hg0 hq0 hgfactor hqfactor +in the ordinary-Hadamard form needed for the two-pair theorem: if `f` and `p` +are one-root-deleted factors of the PF polynomials `g` and `q`, then +`f ⊙ p ≪ g ⊙ q`. This is the paragraph which expands +`((X - u)f) ⊙ ((X - v)p)` through `L`, `J`, and `D`. -/ +theorem gwHadamardProductDoubleDeletedKrein {g q f p : ℝ[X]} {u v : ℝ} + (hg : IsPFPolynomial g) (hq : IsPFPolynomial q) (hg0 : g ≠ 0) (hq0 : q ≠ 0) + (hgfactor : g = (X - C u) * f) (hqfactor : q = (X - C v) * p) : + Interl (hadamardProduct f p) (hadamardProduct g q) := by have hfsummand : IsGWKreinSummand g f := Or.inr ⟨u, hgfactor⟩ have hpsummand : IsGWKreinSummand q p := Or.inr ⟨v, hqfactor⟩ have hf : IsPFPolynomial f := hfsummand.isPFPolynomial hg @@ -134,24 +112,6 @@ theorem gwSchurProduct_interl {g q p : ℝ[X]} (h : IsGWKreinSummand g q) gwSchurProductInterl (h.isPFPolynomial hg) hg hp (h.interl hg0 (hg.ne_zero_and_splits hg0).2) -/-- Two arbitrary Krein summands reduce to the genuinely double-deleted case. -/ -theorem gwSchurProduct_interl_of_doubleDeleted - (hDouble : gwSchurProductDoubleDeletedKreinStatement) - {g q f p : ℝ[X]} (hf : IsGWKreinSummand g f) - (hp : IsGWKreinSummand q p) - (hg : IsPFPolynomial g) (hq : IsPFPolynomial q) - (hg0 : g ≠ 0) (hq0 : q ≠ 0) : - Interl (gwSchurProduct f p) (gwSchurProduct g q) := by - rcases hf with hfg_self | ⟨u, hfg_factor⟩ - · rw [hfg_self] - simpa [gwSchurProduct_comm p g, gwSchurProduct_comm q g] using - hp.gwSchurProduct_interl hq hg hq0 - rcases hp with hpq_self | ⟨v, hpq_factor⟩ - · rw [hpq_self] - exact (show IsGWKreinSummand g f from Or.inr ⟨u, hfg_factor⟩).gwSchurProduct_interl - hg hq hg0 - · exact hDouble hg hq hg0 hq0 hfg_factor hpq_factor - /-- Fixed-factor ordinary Hadamard products of a Krein summand precede the parent product. -/ theorem gwHadamardProduct_interl {g q p : ℝ[X]} (h : IsGWKreinSummand g q) @@ -160,10 +120,10 @@ theorem gwHadamardProduct_interl {g q p : ℝ[X]} (h : IsGWKreinSummand g q) gwHadamardProductInterl (h.isPFPolynomial hg) hg hp (h.interl hg0 (hg.ne_zero_and_splits hg0).2) -/-- Two arbitrary Krein summands reduce to the genuinely double-deleted -ordinary-Hadamard case. -/ +/-- Ordinary Hadamard products of two arbitrary Krein summands precede the +parent product; the genuinely double-deleted case is +`gwHadamardProductDoubleDeletedKrein`. -/ theorem gwHadamardProduct_interl_of_doubleDeleted - (hDouble : gwHadamardProductDoubleDeletedKreinStatement) {g q f p : ℝ[X]} (hf : IsGWKreinSummand g f) (hp : IsGWKreinSummand q p) (hg : IsPFPolynomial g) (hq : IsPFPolynomial q) @@ -177,7 +137,7 @@ theorem gwHadamardProduct_interl_of_doubleDeleted · rw [hpq_self] exact (show IsGWKreinSummand g f from Or.inr ⟨u, hfg_factor⟩).gwHadamardProduct_interl hg hq hg0 - · exact hDouble hg hq hg0 hq0 hfg_factor hpq_factor + · exact gwHadamardProductDoubleDeletedKrein hg hq hg0 hq0 hfg_factor hpq_factor end IsGWKreinSummand @@ -224,7 +184,7 @@ theorem hadamardProduct_interl_of_kreinSummandExpansion_left · intro ap hap rcases List.mem_map.mp hap with ⟨ap0, hap0, rfl⟩ exact (hsummand ap0 hap0).gwHadamardProduct_interl_of_doubleDeleted - gwHadamardProductDoubleDeletedKrein hp hg hq hg0 hq0 + hp hg hq hg0 hq0 · intro ap hap rcases List.mem_map.mp hap with ⟨ap0, hap0, rfl⟩ exact diff --git a/RealRooted/GarloffWagner/Iterated.lean b/RealRooted/GarloffWagner/Iterated.lean index d8102e802..d5f6fdebd 100644 --- a/RealRooted/GarloffWagner/Iterated.lean +++ b/RealRooted/GarloffWagner/Iterated.lean @@ -446,44 +446,20 @@ theorem gwJL_factor_strictInterl_of_splits {k : ℕ} {u : ℝ} {f : ℝ[X]} rw [gwJL_X_sub_C_mul_eq_TDeriv] simpa [hD] using hstrictInterl -/-- Theorem 11(a), real-rooted part: `J^k L` preserves real-rootedness. -/ -def gwTheorem11RealRootedStatement : Prop := - ∀ {f : ℝ[X]}, f ≠ 0 → f.Splits → ∀ k, (gwJL k f).Splits - -theorem gwTheorem11RealRooted : - gwTheorem11RealRootedStatement := by - intro f hf0 hfs - exact gwJL_splits_of_splits hf0 hfs - -/-- Theorem 11(b), zero-aware PF-cone form: `J^k L` preserves PF polynomials. -/ -def gwTheorem11PFStatement : Prop := - ∀ {f : ℝ[X]}, IsPFPolynomial f → ∀ k, IsPFPolynomial (gwJL k f) - -theorem gwTheorem11PF_of_realRooted - (h : gwTheorem11RealRootedStatement) : - gwTheorem11PFStatement := by - intro f hf k +/-- Garloff--Wagner, Theorem 11(a), real-rooted part: `J^k L` preserves +real-rootedness. -/ +theorem gwTheorem11RealRooted {f : ℝ[X]} (hf0 : f ≠ 0) (hfs : f.Splits) (k : ℕ) : + (gwJL k f).Splits := + gwJL_splits_of_splits hf0 hfs k + +/-- Garloff--Wagner, Theorem 11(b), zero-aware PF-cone form: `J^k L` preserves +PF polynomials. -/ +theorem gwTheorem11PF {f : ℝ[X]} (hf : IsPFPolynomial f) (k : ℕ) : + IsPFPolynomial (gwJL k f) := by by_cases hf0 : f = 0 · simpa [hf0] using IsPFPolynomial.zero · exact IsPFPolynomial.of_realRooted_nonneg - (hf.hasNonnegCoeffs.gwJL k) (h hf0 (hf.ne_zero_and_splits hf0).2 k) - -theorem gwTheorem11PF : - gwTheorem11PFStatement := - gwTheorem11PF_of_realRooted gwTheorem11RealRooted - -/-- The standard nonpositive-root part of Garloff--Wagner, Theorem 11(b), -without the later simple-root/common-factor strengthening. -/ -def gwTheorem11NonposStatement : Prop := - ∀ {f : ℝ[X]}, - f ≠ 0 → - f.Splits → - HasPosLeadingCoeff f → - (∀ r ∈ f.roots, r ≤ 0) → - ∀ k, - (gwJL k f).Splits ∧ - HasPosLeadingCoeff (gwJL k f) ∧ - ∀ r ∈ (gwJL k f).roots, r ≤ 0 + (hf.hasNonnegCoeffs.gwJL k) (gwTheorem11RealRooted hf0 (hf.ne_zero_and_splits hf0).2 k) theorem gwJL_splits_pos_roots_nonpos_of_splits_pos_roots_nonpos {f : ℝ[X]} (hf0 : f ≠ 0) (hfs : f.Splits) (hfpos : HasPosLeadingCoeff f) @@ -494,14 +470,17 @@ theorem gwJL_splits_pos_roots_nonpos_of_splits_pos_roots_nonpos {f : ℝ[X]} have hfnn : HasNonnegCoeffs f := ((hasNonnegCoeffs_iff_pos_leadingCoeff_and_roots_nonpos hfs).2 ⟨hfpos, hfroots⟩).1 - have hsplit : (gwJL k f).Splits := gwTheorem11RealRooted hf0 hfs k + have hsplit : (gwJL k f).Splits := gwJL_splits_of_splits hf0 hfs k exact ⟨hsplit, hfpos.gwJL k, roots_nonpos_of_nonneg_coeffs hsplit (hfnn.gwJL k)⟩ -theorem gwTheorem11Nonpos : - gwTheorem11NonposStatement := by - intro f hf0 hfs hfpos hfroots k - exact gwJL_splits_pos_roots_nonpos_of_splits_pos_roots_nonpos - hf0 hfs hfpos hfroots k +/-- The standard nonpositive-root part of Garloff--Wagner, Theorem 11(b), +without the later simple-root/common-factor strengthening. -/ +theorem gwTheorem11Nonpos {f : ℝ[X]} (hf0 : f ≠ 0) (hfs : f.Splits) + (hfpos : HasPosLeadingCoeff f) (hfroots : ∀ r ∈ f.roots, r ≤ 0) (k : ℕ) : + (gwJL k f).Splits ∧ + HasPosLeadingCoeff (gwJL k f) ∧ + ∀ r ∈ (gwJL k f).roots, r ≤ 0 := + gwJL_splits_pos_roots_nonpos_of_splits_pos_roots_nonpos hf0 hfs hfpos hfroots k /-- Simple-except-origin part of Garloff--Wagner, Theorem 11(b). -/ theorem gwJL_hasSimpleRootsExcept_zero_of_splits_roots_nonpos_hasSimpleRootsExcept @@ -579,20 +558,6 @@ theorem gwJL_hasSimpleRootsExcept_zero_of_splits_roots_nonpos_hasSimpleRootsExce exact hasSimpleRootsExcept_TDeriv (ihq (k + 1)) hu0 hF0 hFs exact hP f.natDegree rfl hf0 hfs hfroots hfsimple -/-- Theorem 11(b) with the simple-except-origin strengthening included. -/ -def gwTheorem11NonposSimpleExceptStatement : Prop := - ∀ {f : ℝ[X]}, - f ≠ 0 → - f.Splits → - HasPosLeadingCoeff f → - (∀ r ∈ f.roots, r ≤ 0) → - HasSimpleRootsExcept f 0 → - ∀ k, - (gwJL k f).Splits ∧ - HasPosLeadingCoeff (gwJL k f) ∧ - (∀ r ∈ (gwJL k f).roots, r ≤ 0) ∧ - HasSimpleRootsExcept (gwJL k f) 0 - theorem gwJL_splits_pos_roots_nonpos_simpleExcept_of_splits_pos_roots_nonpos_simpleExcept {f : ℝ[X]} (hf0 : f ≠ 0) (hfs : f.Splits) (hfpos : HasPosLeadingCoeff f) (hfroots : ∀ r ∈ f.roots, r ≤ 0) @@ -608,12 +573,17 @@ theorem gwJL_splits_pos_roots_nonpos_simpleExcept_of_splits_pos_roots_nonpos_sim gwJL_hasSimpleRootsExcept_zero_of_splits_roots_nonpos_hasSimpleRootsExcept hf0 hfs hfroots hfsimple k⟩ -theorem gwTheorem11NonposSimpleExcept : - gwTheorem11NonposSimpleExceptStatement := by - intro f hf0 hfs hfpos hfroots hfsimple k - exact - gwJL_splits_pos_roots_nonpos_simpleExcept_of_splits_pos_roots_nonpos_simpleExcept - hf0 hfs hfpos hfroots hfsimple k +/-- Garloff--Wagner, Theorem 11(b), with the simple-except-origin strengthening +included. -/ +theorem gwTheorem11NonposSimpleExcept {f : ℝ[X]} (hf0 : f ≠ 0) (hfs : f.Splits) + (hfpos : HasPosLeadingCoeff f) (hfroots : ∀ r ∈ f.roots, r ≤ 0) + (hfsimple : HasSimpleRootsExcept f 0) (k : ℕ) : + (gwJL k f).Splits ∧ + HasPosLeadingCoeff (gwJL k f) ∧ + (∀ r ∈ (gwJL k f).roots, r ≤ 0) ∧ + HasSimpleRootsExcept (gwJL k f) 0 := + gwJL_splits_pos_roots_nonpos_simpleExcept_of_splits_pos_roots_nonpos_simpleExcept + hf0 hfs hfpos hfroots hfsimple k /-- Garloff--Wagner formula (3) for a standard polynomial with nonpositive roots and simple roots except possibly at the origin. -/ @@ -649,11 +619,6 @@ theorem gwJL_factor_strictInterl_of_nonpos gwJL_factor_strictInterl_of_nonpos_of_hasSimpleRootsExcept_zero hu hf0 hfs hfpos hfroots hfsimple -/-- Theorem 11(c), in the local orientation: -Garloff--Wagner's `g $ f` is represented by `StrictInterl f g`. -/ -def gwTheorem11StrictInterlStatement : Prop := - ∀ {f g : ℝ[X]}, StrictInterl f g → ∀ k, StrictInterl (gwJL k f) (gwJL k g) - /-- Reduction for the Lemma 7/Krein step in Garloff--Wagner, Theorem 11(c): once `g` is expressed as a weighted sum whose `J^k L` images are compatible with the common left bound `J^k L f`, Wagner's finite weighted-sum theorem @@ -668,21 +633,6 @@ theorem gwJL_strictInterl_of_weightedCompatibleExpansion rw [hg, gwJL_weightedSum] exact hcomp.toStrictInterl -/-- Interface isolating the remaining Krein-expansion and Wagner-compatibility -work for Garloff--Wagner, Theorem 11(c). -/ -def gwTheorem11StrictInterlWeightedExpansionStatement : Prop := - ∀ {f g : ℝ[X]}, StrictInterl f g → ∀ k, ∃ l : List (ℝ × ℝ[X]), - g = weightedSum l ∧ - WeightedCompatibleLeft (gwJL k f) - (l.map fun ap => (ap.1, gwJL k ap.2)) - -theorem gwTheorem11StrictInterl_of_weightedCompatibleExpansion - (h : gwTheorem11StrictInterlWeightedExpansionStatement) : - gwTheorem11StrictInterlStatement := by - intro f g hfg k - rcases h hfg k with ⟨l, hg, hcomp⟩ - exact gwJL_strictInterl_of_weightedCompatibleExpansion hg hcomp - /-- Variable-swapped common-right weighted reduction for the Lemma 7/Krein step. If `g` is expanded in summands bounded on the right by `f`, Wagner's common-right finite-sum theorem gives the reverse conclusion @@ -715,25 +665,6 @@ theorem gwJL_weightedExpansion_strictInterl_right rcases hex with ⟨ap, hap, hapos⟩ exact ⟨(ap.1, gwJL k ap.2), List.mem_map.mpr ⟨ap, hap, rfl⟩, hapos⟩) -/-- Interface for the variable-swapped common-right Krein-expansion direction. -This is not the final Theorem 11(c) orientation by itself; see -`gwTheorem11StrictInterlRightWeightedExpansionStatement` for the forward -package. -/ -def gwTheorem11RightWeightedExpansionStatement : Prop := - ∀ {f g : ℝ[X]}, StrictInterl f g → ∀ k, ∃ l : List (ℝ × ℝ[X]), - g = weightedSum l ∧ - (∀ ap ∈ l, 0 ≤ ap.1) ∧ - (∀ ap ∈ l, StrictInterl (gwJL k ap.2) (gwJL k f)) ∧ - (∀ ap ∈ l, HasPosLeadingCoeff (gwJL k ap.2)) ∧ - ∃ ap ∈ l, 0 < ap.1 - -theorem gwTheorem11ReverseStrictInterl_of_rightWeightedExpansion - (h : gwTheorem11RightWeightedExpansionStatement) : - ∀ {f g : ℝ[X]}, StrictInterl f g → ∀ k, StrictInterl (gwJL k g) (gwJL k f) := by - intro f g hfg k - rcases h hfg k with ⟨l, hg, hnonneg, hstrictInterl, hpos, hex⟩ - exact gwJL_weightedExpansion_strictInterl_right hg hnonneg hstrictInterl hpos hex - /-- Common-right weighted reduction in the forward Theorem 11(c) orientation. If the left input `f` is a nonnegative weighted sum whose `J^k L` images all precede the common right bound `J^k L g`, then the image of `f` also precedes @@ -766,22 +697,4 @@ theorem gwJL_strictInterl_of_rightWeightedExpansion rcases hex with ⟨ap, hap, hapos⟩ exact ⟨(ap.1, gwJL k ap.2), List.mem_map.mpr ⟨ap, hap, rfl⟩, hapos⟩) -/-- Forward Theorem 11(c) interface for the common-right Krein expansion: -given `StrictInterl f g`, write the left input `f` as a nonnegative weighted sum of -summands whose `J^k L` images precede `J^k L g`. -/ -def gwTheorem11StrictInterlRightWeightedExpansionStatement : Prop := - ∀ {f g : ℝ[X]}, StrictInterl f g → ∀ k, ∃ l : List (ℝ × ℝ[X]), - f = weightedSum l ∧ - (∀ ap ∈ l, 0 ≤ ap.1) ∧ - (∀ ap ∈ l, StrictInterl (gwJL k ap.2) (gwJL k g)) ∧ - (∀ ap ∈ l, HasPosLeadingCoeff (gwJL k ap.2)) ∧ - ∃ ap ∈ l, 0 < ap.1 - -theorem gwTheorem11StrictInterl_of_rightWeightedExpansion - (h : gwTheorem11StrictInterlRightWeightedExpansionStatement) : - gwTheorem11StrictInterlStatement := by - intro f g hfg k - rcases h hfg k with ⟨l, hf, hnonneg, hstrictInterl, hpos, hex⟩ - exact gwJL_strictInterl_of_rightWeightedExpansion hf hnonneg hstrictInterl hpos hex - end RealRooted diff --git a/RealRooted/GarloffWagner/KreinExpansion.lean b/RealRooted/GarloffWagner/KreinExpansion.lean index 55ffd12b9..0858adca9 100644 --- a/RealRooted/GarloffWagner/KreinExpansion.lean +++ b/RealRooted/GarloffWagner/KreinExpansion.lean @@ -432,21 +432,26 @@ theorem kreinSummandExpansion_of_weightedSum {f g : ℝ[X]} {l : List (ℝ × ∃ ap ∈ l, 0 < ap.1 := ⟨l, hf, hnonneg, hsummand, hex⟩ -/-- Lemma 7-facing interface for Theorem 11(c). After normalizing the right -polynomial to be standard, the left polynomial should expand as a nonnegative -weighted sum of the right polynomial and its one-root-deleted factors. -/ -def gwTheorem11StrictInterlKreinSummandExpansionStatement : Prop := - ∀ {f g : ℝ[X]}, StrictInterl f g → HasPosLeadingCoeff f → HasPosLeadingCoeff g → +/-- Lemma 7 form of Garloff--Wagner, Theorem 11(c). For standard `g`, the left +polynomial expands as a nonnegative weighted sum of `g` and its +one-root-deleted factors. -/ +theorem gwTheorem11StrictInterlKreinSummandExpansion {f g : ℝ[X]} + (hfg : StrictInterl f g) (hfpos : HasPosLeadingCoeff f) (hgpos : HasPosLeadingCoeff g) : ∃ l : List (ℝ × ℝ[X]), f = weightedSum l ∧ (∀ ap ∈ l, 0 ≤ ap.1) ∧ (∀ ap ∈ l, IsGWKreinSummand g ap.2) ∧ - ∃ ap ∈ l, 0 < ap.1 + ∃ ap ∈ l, 0 < ap.1 := by + by_cases hgdeg0 : g.natDegree = 0 + · exact exists_kreinSummandExpansion_nonneg_right_of_natDegree_eq_zero hfg hfpos + hgpos hgdeg0 + · exact exists_kreinSummandExpansion_nonneg_right_of_pos_natDegree hfg hfpos + hgpos (Nat.pos_of_ne_zero hgdeg0) -theorem gwTheorem11StrictInterl_of_kreinSummandExpansion - (h : gwTheorem11StrictInterlKreinSummandExpansionStatement) : - gwTheorem11StrictInterlStatement := by - intro f g hfg k +/-- Garloff--Wagner, Theorem 11(c), in the local orientation: Garloff--Wagner's +`g $ f` is represented by `StrictInterl f g`, and `J^k L` preserves it. -/ +theorem gwTheorem11StrictInterl {f g : ℝ[X]} (hfg : StrictInterl f g) (k : ℕ) : + StrictInterl (gwJL k f) (gwJL k g) := by let sf : ℝ := f.leadingCoeff⁻¹ let sg : ℝ := g.leadingCoeff⁻¹ have hf0 : f ≠ 0 := hfg.1.1 @@ -459,7 +464,8 @@ theorem gwTheorem11StrictInterl_of_kreinSummandExpansion hasPosLeadingCoeff_C_inv_leadingCoeff_mul hf0 have hsg_pos : HasPosLeadingCoeff (C sg * g) := hasPosLeadingCoeff_C_inv_leadingCoeff_mul hg0 - rcases h (f := C sf * f) (g := C sg * g) hfg_scaled hsf_pos hsg_pos with + rcases gwTheorem11StrictInterlKreinSummandExpansion (f := C sf * f) (g := C sg * g) + hfg_scaled hsf_pos hsg_pos with ⟨l, hf, hnonneg, hsummand, hex⟩ have hscaled : StrictInterl (gwJL k (C sf * f)) (gwJL k (C sg * g)) := @@ -478,20 +484,4 @@ theorem gwTheorem11StrictInterl_of_kreinSummandExpansion rw [← mul_assoc, ← C_mul, inv_mul_cancel₀ hsg, C_1, one_mul] simpa [hscale] using hright -/-- Garloff--Wagner, Theorem 11(c), reduced to the checked Krein expansion -package. -/ -theorem gwTheorem11StrictInterlKreinSummandExpansion : - gwTheorem11StrictInterlKreinSummandExpansionStatement := by - intro f g hfg hfpos hgpos - by_cases hgdeg0 : g.natDegree = 0 - · exact exists_kreinSummandExpansion_nonneg_right_of_natDegree_eq_zero hfg hfpos - hgpos hgdeg0 - · exact exists_kreinSummandExpansion_nonneg_right_of_pos_natDegree hfg hfpos - hgpos (Nat.pos_of_ne_zero hgdeg0) - -/-- Garloff--Wagner, Theorem 11(c), in the local `StrictInterl` orientation. -/ -theorem gwTheorem11StrictInterl : - gwTheorem11StrictInterlStatement := - gwTheorem11StrictInterl_of_kreinSummandExpansion gwTheorem11StrictInterlKreinSummandExpansion - end RealRooted diff --git a/RealRooted/GarloffWagner/Theorem12.lean b/RealRooted/GarloffWagner/Theorem12.lean index d825a60b8..a13cee690 100644 --- a/RealRooted/GarloffWagner/Theorem12.lean +++ b/RealRooted/GarloffWagner/Theorem12.lean @@ -322,54 +322,6 @@ theorem gwL_sub_C_mul_gwD_gwL_pf {p : ℝ[X]} {u : ℝ} exact False.elim (hT0 hTzero) · exact IsPFPolynomial.of_realRooted_nonneg hTnn hstrict.1.2 -/-- Theorem 12(a), zero-aware PF-cone form for the factorial Schur product. -/ -def gwSchurProductPFStatement : Prop := - ∀ {f p : ℝ[X]}, - IsPFPolynomial f → - IsPFPolynomial p → - IsPFPolynomial (gwSchurProduct f p) - -/-- Theorem 12(b), one fixed Schur-product factor, in the local orientation. -/ -def gwSchurProductStrictInterlStatement : Prop := - ∀ {f g p : ℝ[X]}, - IsPFPolynomial f → - IsPFPolynomial g → - IsPFPolynomial p → - StrictInterl f g → - Interl (gwSchurProduct f p) (gwSchurProduct g p) - -theorem gwSchurProductPF_of_strictInterl - (h : gwSchurProductStrictInterlStatement) : - gwSchurProductPFStatement := by - intro f p hf hp - by_cases hf0 : f = 0 - · simpa [hf0] using IsPFPolynomial.zero - have hfs := hf.ne_zero_and_splits hf0 - exact IsPFPolynomial.of_interl_self - (hf.hasNonnegCoeffs.gwSchurProduct hp.hasNonnegCoeffs) - (h hf hf hp (StrictInterl.refl hfs.1 hfs.2)) - -theorem gwSchurProductInterl_of_strictInterl - (h : gwSchurProductStrictInterlStatement) : - ∀ {f g p : ℝ[X]}, - IsPFPolynomial f → - IsPFPolynomial g → - IsPFPolynomial p → - Interl f g → - Interl (gwSchurProduct f p) (gwSchurProduct g p) := by - intro f g p hf hg hp hfg - rcases hfg with hf0 | hg0 | hstrict - · simpa [hf0] using interl_zero_left (gwSchurProduct g p) - · simpa [hg0] using interl_zero_right (gwSchurProduct f p) - · exact h hf hg hp hstrict - -theorem gwSchurProduct_derivative_interl_self_of_strictInterl - (h : gwSchurProductStrictInterlStatement) {f p : ℝ[X]} - (hf : IsPFPolynomial f) (hp : IsPFPolynomial p) : - Interl (gwSchurProduct (gwD f) p) (gwSchurProduct f p) := by - simpa [gwD] using - gwSchurProductInterl_of_strictInterl h hf.derivative hf hp hf.derivative_interl_self - /-- Symmetric form of the Theorem 12(a) linear-factor step, used for one-root-deleted Krein summands in Theorem 12(b). -/ theorem gwSchurProduct_interl_left_linearFactor_of_derivative_interl @@ -468,7 +420,10 @@ same-measure result as the common-right PF input for the fixed-factor interlacing statement. All derivative and one-root-deleted calls have strictly smaller total degree. -/ theorem gwSchurProductPFAndStrictInterl : - gwSchurProductPFStatement ∧ gwSchurProductStrictInterlStatement := by + (∀ {f p : ℝ[X]}, IsPFPolynomial f → IsPFPolynomial p → + IsPFPolynomial (gwSchurProduct f p)) ∧ + (∀ {f g p : ℝ[X]}, IsPFPolynomial f → IsPFPolynomial g → IsPFPolynomial p → + StrictInterl f g → Interl (gwSchurProduct f p) (gwSchurProduct g p)) := by classical let P : ℕ → Prop := fun n => (∀ {f p : ℝ[X]}, @@ -627,9 +582,11 @@ theorem gwSchurProductPFAndStrictInterl : · intro f g p hf hg hp hfg exact (hP (g.natDegree + p.natDegree)).2 hf hg hp hfg.toInterl rfl -theorem gwSchurProductPF : - gwSchurProductPFStatement := - gwSchurProductPFAndStrictInterl.1 +/-- Garloff--Wagner, Theorem 12(a): the factorial Schur product preserves the +zero-aware PF cone. -/ +theorem gwSchurProductPF {f p : ℝ[X]} (hf : IsPFPolynomial f) (hp : IsPFPolynomial p) : + IsPFPolynomial (gwSchurProduct f p) := + gwSchurProductPFAndStrictInterl.1 hf hp /-- Ordinary Hadamard products preserve PF polynomials, obtained by applying the Schur-product theorem to the `L`-normalized left input. -/ @@ -659,18 +616,32 @@ theorem gwL_interl {f g : ℝ[X]} (hfg : Interl f g) : exact interl_zero_right (gwL f) · exact (gwL_strictInterl hstrict).toInterl -theorem gwSchurProductStrictInterl : - gwSchurProductStrictInterlStatement := - gwSchurProductPFAndStrictInterl.2 - -theorem gwSchurProductInterl : - ∀ {f g p : ℝ[X]}, - IsPFPolynomial f → - IsPFPolynomial g → - IsPFPolynomial p → - Interl f g → - Interl (gwSchurProduct f p) (gwSchurProduct g p) := - gwSchurProductInterl_of_strictInterl gwSchurProductStrictInterl +/-- Garloff--Wagner, Theorem 12(b), one fixed Schur-product factor, in the local +orientation. -/ +theorem gwSchurProductStrictInterl {f g p : ℝ[X]} + (hf : IsPFPolynomial f) (hg : IsPFPolynomial g) (hp : IsPFPolynomial p) + (hfg : StrictInterl f g) : + Interl (gwSchurProduct f p) (gwSchurProduct g p) := + gwSchurProductPFAndStrictInterl.2 hf hg hp hfg + +/-- Garloff--Wagner, Theorem 12(b), zero-aware form: the factorial Schur product +with a fixed PF factor preserves interlacing. -/ +theorem gwSchurProductInterl {f g p : ℝ[X]} + (hf : IsPFPolynomial f) (hg : IsPFPolynomial g) (hp : IsPFPolynomial p) + (hfg : Interl f g) : + Interl (gwSchurProduct f p) (gwSchurProduct g p) := by + rcases hfg with hf0 | hg0 | hstrict + · simpa [hf0] using interl_zero_left (gwSchurProduct g p) + · simpa [hg0] using interl_zero_right (gwSchurProduct f p) + · exact gwSchurProductStrictInterl hf hg hp hstrict + +/-- The Schur product with a fixed PF factor sends `f' ≪ f` to the +corresponding Schur-product relation. -/ +theorem gwSchurProduct_derivative_interl_self {f p : ℝ[X]} + (hf : IsPFPolynomial f) (hp : IsPFPolynomial p) : + Interl (gwSchurProduct (gwD f) p) (gwSchurProduct f p) := by + simpa [gwD] using + gwSchurProductInterl hf.derivative hf hp hf.derivative_interl_self /-- Symmetric fixed-factor form of `gwSchurProductInterl`. -/ theorem gwSchurProductInterl_left {f p q : ℝ[X]} diff --git a/RealRooted/Hadamard/Consequences.lean b/RealRooted/Hadamard/Consequences.lean index 03c15f1f1..c2bdedd84 100644 --- a/RealRooted/Hadamard/Consequences.lean +++ b/RealRooted/Hadamard/Consequences.lean @@ -9,179 +9,74 @@ namespace RealRooted /-! # Hadamard consequences -Conditional odd/even reductions, PF and interlacing closure, reciprocal -shift transport, and coefficientwise Polya-frequency consequences. +PF and interlacing closure under Hadamard products, reciprocal shift +transport, and coefficientwise Pólya-frequency consequences. -/ -/-- **Garloff--Wagner, Theorem 4(b), reduced to legacy odd/even inputs** -(TODO T9). - -The two-pair interlacing form of the Garloff--Wagner Hadamard theorem follows, -with a fully checked conditional reduction, from the following inputs (the -latter three are pre-existing interfaces from `RealRooted.VeroneseSection`): - -* `hadamardPreservesHurwitzStableStatement` — Garloff--Wagner Theorem 1 - (Hadamard products of Hurwitz-stable polynomials are Hurwitz stable when the - coefficientwise product is nonzero); -* `NonnegStrictInterlToHurwitzOddEvenStatement` — the forward Hermite--Biehler bridge - from interlacing `StrictInterl f g` of nonnegative-coefficient polynomials to - Hurwitz stability of `oddEvenPolynomial f g = g(x²) + x·f(x²)`; -* `LegacyHurwitzOddEvenToFullyInterlacingPairStatement` — the legacy row-oriented - Hurwitz-to-Lace bridge, now known false as a general theorem; and -* `FullyInterlacingPairToInterlStatement` — the converse lace-to-interlacing - bridge back to zero-aware interlacing. - -The bridge between the two-pair and single-polynomial worlds is the proven -algebraic identity `hadamardProduct_oddEvenPolynomial`: -`oddEvenPolynomial f g ⊙ oddEvenPolynomial p q - = oddEvenPolynomial (f ⊙ p) (g ⊙ q)`, -whose even part is `g ⊙ q` and whose odd part is `f ⊙ p`. - -Thus all of the interlacing bookkeeping of Theorem 4(b) is discharged here once -these conditional inputs are supplied. -Note that the odd/even polynomial of an interlacing pair is Hurwitz stable, not -real-rooted (e.g. `f = 1`, `g = X + 1` gives `X² + X + 1`), which is why the -reduction goes through `IsHurwitzStable` (Theorem 1) rather than the -single-polynomial real-rootedness fact -`garloffWagnerHadamardNonnegRealRootedStatement`. -/ -theorem garloffWagnerHadamardNonnegInterl_of_oddEven - (hThm1 : hadamardPreservesHurwitzStableStatement) - (hStrictInterlToHurwitz : NonnegStrictInterlToHurwitzOddEvenStatement) - (hHurwitzToFull : LegacyHurwitzOddEvenToFullyInterlacingPairStatement) - (hFullToInterl : FullyInterlacingPairToInterlStatement) : - ∀ {f g p q : ℝ[X]}, - HasNonnegCoeffs f → HasNonnegCoeffs g → HasNonnegCoeffs p → HasNonnegCoeffs q → - StrictInterl f g → StrictInterl p q → - Interl (hadamardProduct f p) (hadamardProduct g q) := by - intro f g p q hf hg hp hq hfg hpq - by_cases hfp0 : hadamardProduct f p = 0 - · simpa [hfp0] using interl_zero_left (hadamardProduct g q) - by_cases hgq0 : hadamardProduct g q = 0 - · simpa [hgq0] using interl_zero_right (hadamardProduct f p) - have hOE1 : IsHurwitzStable (oddEvenPolynomial f g) := hStrictInterlToHurwitz hf hg hfg - have hOE2 : IsHurwitzStable (oddEvenPolynomial p q) := hStrictInterlToHurwitz hp hq hpq - have hOEprod0 : - hadamardProduct (oddEvenPolynomial f g) (oddEvenPolynomial p q) ≠ 0 := by - rw [hadamardProduct_oddEvenPolynomial] - exact oddEvenPolynomial_ne_zero_iff.mpr (Or.inl hfp0) - exact hFullToInterl (hHurwitzToFull (by - simpa [hadamardProduct_oddEvenPolynomial] using hThm1 hOE1 hOE2 hOEprod0)) - -/-- PF-polynomial wrapper around the checked nonnegative -Garloff--Wagner two-pair theorem. -/ -def garloffWagnerHadamardPFStrictInterlStatement : Prop := - ∀ {f g p q : ℝ[X]}, - IsPFPolynomial f → - IsPFPolynomial g → - IsPFPolynomial p → - IsPFPolynomial q → - StrictInterl f g → - StrictInterl p q → - Interl (hadamardProduct f p) (hadamardProduct g q) - -theorem garloffWagnerHadamardPFStrictInterl_of_nonnegStrictInterl : - garloffWagnerHadamardPFStrictInterlStatement := - fun hf hg hp hq hfg hpq => - garloffWagnerHadamardNonnegInterl hf.hasNonnegCoeffs hg.hasNonnegCoeffs - hp.hasNonnegCoeffs hq.hasNonnegCoeffs hfg hpq - -/-- Zero-aware PF-polynomial wrapper around the checked Garloff--Wagner -two-pair theorem. -/ -def garloffWagnerHadamardPFInterlStatement : Prop := - ∀ {f g p q : ℝ[X]}, - IsPFPolynomial f → - IsPFPolynomial g → - IsPFPolynomial p → - IsPFPolynomial q → - Interl f g → - Interl p q → - Interl (hadamardProduct f p) (hadamardProduct g q) - -theorem garloffWagnerHadamardPFInterl_of_strictInterl - (hGW : garloffWagnerHadamardPFStrictInterlStatement) : - garloffWagnerHadamardPFInterlStatement := by - intro f g p q hf hg hp hq hfg hpq +/-- Garloff--Wagner, Theorem 4(b), for PF polynomials: Hadamard products +preserve strict interlacing of PF pairs, in zero-aware form. -/ +theorem garloffWagnerHadamardPFStrictInterl_of_nonnegStrictInterl {f g p q : ℝ[X]} + (hf : IsPFPolynomial f) (hg : IsPFPolynomial g) + (hp : IsPFPolynomial p) (hq : IsPFPolynomial q) + (hfg : StrictInterl f g) (hpq : StrictInterl p q) : + Interl (hadamardProduct f p) (hadamardProduct g q) := + garloffWagnerHadamardNonnegInterl hf.hasNonnegCoeffs hg.hasNonnegCoeffs + hp.hasNonnegCoeffs hq.hasNonnegCoeffs hfg hpq + +/-- Garloff--Wagner, Theorem 4(b), for PF polynomials and zero-aware +interlacing inputs. -/ +theorem garloffWagnerHadamardPFInterl_of_nonnegStrictInterl {f g p q : ℝ[X]} + (hf : IsPFPolynomial f) (hg : IsPFPolynomial g) + (hp : IsPFPolynomial p) (hq : IsPFPolynomial q) + (hfg : Interl f g) (hpq : Interl p q) : + Interl (hadamardProduct f p) (hadamardProduct g q) := by rcases hfg with rfl | rfl | hfg' · simpa using interl_zero_left (hadamardProduct g q) · simpa using interl_zero_right (hadamardProduct f p) rcases hpq with rfl | rfl | hpq' · simpa using interl_zero_left (hadamardProduct g q) · simpa using interl_zero_right (hadamardProduct f p) - exact hGW hf hg hp hq hfg' hpq' - -theorem garloffWagnerHadamardPFInterl_of_nonnegStrictInterl : - garloffWagnerHadamardPFInterlStatement := - garloffWagnerHadamardPFInterl_of_strictInterl - garloffWagnerHadamardPFStrictInterl_of_nonnegStrictInterl - -/-- PF-polynomial closure under Hadamard product, stated directly from the -zero-aware Garloff--Wagner PF wrapper. -/ -theorem hadamardProduct_preserves_pf_of_garloffWagner - (hGW : garloffWagnerHadamardPFInterlStatement) - {p q : ℝ[X]} (hp : IsPFPolynomial p) (hq : IsPFPolynomial q) : - IsPFPolynomial (hadamardProduct p q) := - IsPFPolynomial.of_interl_self - (hp.hasNonnegCoeffs.hadamardProduct hq.hasNonnegCoeffs) - (hGW hp hp hq hq hp.interl_self hq.interl_self) + exact garloffWagnerHadamardPFStrictInterl_of_nonnegStrictInterl hf hg hp hq hfg' hpq' -theorem hadamardProduct_preserves_pf_of_nonnegStrictInterl : - {p q : ℝ[X]} → IsPFPolynomial p → IsPFPolynomial q → +/-- PF polynomials are closed under coefficientwise Hadamard products. -/ +theorem hadamardProduct_preserves_pf_of_nonnegStrictInterl {p q : ℝ[X]} + (hp : IsPFPolynomial p) (hq : IsPFPolynomial q) : IsPFPolynomial (hadamardProduct p q) := - hadamardProduct_preserves_pf_of_garloffWagner - garloffWagnerHadamardPFInterl_of_nonnegStrictInterl - -theorem hadamardProduct_preserves_pf_of_matrixHadamardBridges - (_hToFull : LegacyNonnegStrictInterlToFullyInterlacingPairStatement) - (_hMatHad : hadamardPreservesHurwitzMatrixTNStatement) - (_hFullToPrec0 : FullyInterlacingPairToInterlStatement) : - {p q : ℝ[X]} → IsPFPolynomial p → IsPFPolynomial q → - IsPFPolynomial (hadamardProduct p q) := - hadamardProduct_preserves_pf_of_nonnegStrictInterl - -theorem hadamardProduct_preserves_pf_of_hurwitzSchur - (_hToFull : LegacyNonnegStrictInterlToFullyInterlacingPairStatement) - (_hFullToPrec0 : FullyInterlacingPairToInterlStatement) : - {p q : ℝ[X]} → IsPFPolynomial p → IsPFPolynomial q → - IsPFPolynomial (hadamardProduct p q) := - hadamardProduct_preserves_pf_of_nonnegStrictInterl - -/-- The nonnegative two-pair Garloff--Wagner theorem gives PF closure under -Hadamard products through the zero-aware PF wrapper. -/ -theorem schurPolyaWagnerHadamardPF_of_garloffWagner_nonnegStrictInterl : - schurPolyaWagnerHadamardPFStatement := - hadamardProduct_preserves_pf_of_nonnegStrictInterl - -/-- The checked PF Hadamard theorem gives the one-polynomial -real-rootedness statement directly. -/ -theorem garloffWagnerHadamardNonnegRealRooted_of_nonnegStrictInterl : - garloffWagnerHadamardNonnegRealRootedStatement := by - intro p q hpnn hqnn hprr hqrr + hp.hadamardProduct hq + +/-- Nonnegative-coefficient Schur--Pólya/Garloff--Wagner real-rootedness for +coefficientwise Hadamard products (Garloff--Wagner, Theorem 4(a)). + +Real-rooted nonzero polynomials with nonnegative coefficients have only +nonpositive roots. The conclusion is zero-aware because the Hadamard product +can vanish when supports are disjoint. -/ +theorem garloffWagnerHadamardNonnegRealRooted_of_nonnegStrictInterl {p q : ℝ[X]} + (hpnn : HasNonnegCoeffs p) (hqnn : HasNonnegCoeffs q) + (hprr : p ≠ 0 ∧ p.Splits) (hqrr : q ≠ 0 ∧ q.Splits) : + (hadamardProduct p q = 0 ∨ (hadamardProduct p q).Splits) ∧ + HasNonnegCoeffs (hadamardProduct p q) ∧ + ∀ r ∈ (hadamardProduct p q).roots, r ≤ 0 := by have hp : IsPFPolynomial p := IsPFPolynomial.of_realRooted_nonneg hpnn hprr.2 have hq : IsPFPolynomial q := IsPFPolynomial.of_realRooted_nonneg hqnn hqrr.2 - have hpf : IsPFPolynomial (hadamardProduct p q) := - hadamardProduct_preserves_pf_of_nonnegStrictInterl hp hq + have hpf : IsPFPolynomial (hadamardProduct p q) := hp.hadamardProduct hq exact ⟨hpf.eq_zero_or_splits, hpf.hasNonnegCoeffs, hpf.roots_nonpos⟩ /-- Fixed-right Hadamard multiplication preserves zero-aware interlacing inside the PF cone. -/ -theorem hadamardProduct_preserves_interl_right - (hGW : garloffWagnerHadamardPFInterlStatement) - {f g p : ℝ[X]} +theorem hadamardProduct_preserves_interl_right {f g p : ℝ[X]} (hf : IsPFPolynomial f) (hg : IsPFPolynomial g) (hp : IsPFPolynomial p) (hfg : Interl f g) : Interl (hadamardProduct f p) (hadamardProduct g p) := - hGW hf hg hp hp hfg hp.interl_self + garloffWagnerHadamardPFInterl_of_nonnegStrictInterl hf hg hp hp hfg hp.interl_self /-- Fixed-left Hadamard multiplication preserves zero-aware interlacing inside the PF cone. -/ -theorem hadamardProduct_preserves_interl_left - (hGW : garloffWagnerHadamardPFInterlStatement) - {f p q : ℝ[X]} +theorem hadamardProduct_preserves_interl_left {f p q : ℝ[X]} (hf : IsPFPolynomial f) (hp : IsPFPolynomial p) (hq : IsPFPolynomial q) (hpq : Interl p q) : Interl (hadamardProduct f p) (hadamardProduct f q) := by simpa [hadamardProduct_comm] using - hadamardProduct_preserves_interl_right hGW hp hq hf hpq + hadamardProduct_preserves_interl_right hp hq hf hpq theorem reciprocalShift_hadamardProduct (D : ℕ) (p q : ℝ[X]) : reciprocalShift D (hadamardProduct p q) = @@ -190,59 +85,27 @@ theorem reciprocalShift_hadamardProduct (D : ℕ) (p q : ℝ[X]) : simp /-- Hadamard closure for the reciprocal-interlacing cone. -/ -def hadamardReciprocalConeClosureStatement : Prop := - ∀ {D : ℕ} {p q : ℝ[X]}, - IsPFPolynomial p → - IsPFPolynomial q → - StrictInterl p (reciprocalShift D p) → - StrictInterl q (reciprocalShift D q) → - Interl (hadamardProduct p q) - (reciprocalShift D (hadamardProduct p q)) - -/-- Hadamard closure for the reciprocal-interlacing cone, obtained from the -zero-aware PF two-pair Garloff--Wagner wrapper. -/ -theorem hadamardReciprocalConeClosure_of_garloffWagner_interl - (hGW : garloffWagnerHadamardPFInterlStatement) : - hadamardReciprocalConeClosureStatement := by - intro D p q hp hq hstrictInterl_p hstrictInterl_q +theorem hadamardReciprocalConeClosure {D : ℕ} {p q : ℝ[X]} + (hp : IsPFPolynomial p) (hq : IsPFPolynomial q) + (hstrictInterl_p : StrictInterl p (reciprocalShift D p)) + (hstrictInterl_q : StrictInterl q (reciprocalShift D q)) : + Interl (hadamardProduct p q) (reciprocalShift D (hadamardProduct p q)) := by have hp_shift : IsPFPolynomial (reciprocalShift D p) := IsPFPolynomial.of_realRooted_nonneg hp.hasNonnegCoeffs.reciprocalShift hstrictInterl_p.2.1.2 have hq_shift : IsPFPolynomial (reciprocalShift D q) := IsPFPolynomial.of_realRooted_nonneg hq.hasNonnegCoeffs.reciprocalShift hstrictInterl_q.2.1.2 simpa [reciprocalShift_hadamardProduct] using - hGW hp hp_shift hq hq_shift hstrictInterl_p.toInterl hstrictInterl_q.toInterl - -theorem hadamardReciprocalConeClosure_of_garloffWagner_strictInterl - (hGW : garloffWagnerHadamardPFStrictInterlStatement) : - hadamardReciprocalConeClosureStatement := - hadamardReciprocalConeClosure_of_garloffWagner_interl - (garloffWagnerHadamardPFInterl_of_strictInterl hGW) - -/-- Polynomial-coefficient form of Polya-frequency closure under termwise -products. This is finite-sequence closure packaged through coefficient -polynomials. -/ -def polyaFrequencyHadamardCoeffStatement : Prop := - ∀ {p q : ℝ[X]}, - IsPolyaFreqSeq p.coeff → - IsPolyaFreqSeq q.coeff → - IsPolyaFreqSeq (fun n => (hadamardProduct p q).coeff n) - -theorem polyaFrequencyHadamardCoeff_of_schurPolyaWagner - (hASW : aissenSchoenbergWhitneyForwardOrZeroStatement) - (hSPW : schurPolyaWagnerHadamardPFStatement) : - polyaFrequencyHadamardCoeffStatement := - fun hp hq => - (hSPW (IsPFPolynomial.of_sequence hASW hp) - (IsPFPolynomial.of_sequence hASW hq)).to_sequence + garloffWagnerHadamardPFInterl_of_nonnegStrictInterl hp hp_shift hq hq_shift + hstrictInterl_p.toInterl hstrictInterl_q.toInterl /-- Finite Pólya-frequency sequences are closed under coefficientwise products. Finite support is encoded by the coefficient sequences of the polynomials `p` and `q`. -/ -theorem polyaFrequencyHadamardCoeff : - polyaFrequencyHadamardCoeffStatement := - polyaFrequencyHadamardCoeff_of_schurPolyaWagner - aissenSchoenbergWhitneyForwardOrZero - schurPolyaWagnerHadamardPF_of_garloffWagner_nonnegStrictInterl +theorem polyaFrequencyHadamardCoeff {p q : ℝ[X]} + (hp : IsPolyaFreqSeq p.coeff) (hq : IsPolyaFreqSeq q.coeff) : + IsPolyaFreqSeq (fun n => (hadamardProduct p q).coeff n) := + ((IsPFPolynomial.of_polyaFreqSeq hp).hadamardProduct + (IsPFPolynomial.of_polyaFreqSeq hq)).to_sequence /-- **Maló's theorem (finite-support Toeplitz form).** The entrywise product of two totally nonnegative lower-triangular Toeplitz matrices is totally diff --git a/RealRooted/Hadamard/Cubic.lean b/RealRooted/Hadamard/Cubic.lean index 81a54f534..294a9198e 100644 --- a/RealRooted/Hadamard/Cubic.lean +++ b/RealRooted/Hadamard/Cubic.lean @@ -9,8 +9,8 @@ namespace RealRooted /-! # Cubic Schur--Szego reductions -Degree-three PF-factor reductions, normalized diagonal base cases, and the -finite Polya--Schur equivalence interfaces. +Degree-three PF-factor reductions of the Schur--Szegő composition to cubic +discriminant inequalities. -/ /-- If the degree-`n` Jensen polynomial is PF and itself has degree at most @@ -132,68 +132,6 @@ theorem cubicDiscr_diagonalOperator_normalized_three_eq_cubicDiscr_schurSzegoCom cubicDiscr (schurSzegoComp 3 f q) := by rw [← schurSzegoComp_eq_diagonalOperator 3 q f, schurSzegoComp_comm] -/-- Level-three normalized diagonal-operator cubic-discriminant base case for -a degree-`≤ 3` PF factor and a splitting factor. -/ -def pfCubicDiscrDiagonalNonnegStatement : Prop := - ∀ {f q : ℝ[X]}, - IsPFPolynomial f → - f.natDegree ≤ 3 → - q.natDegree ≤ 3 → - q.Splits → - 0 ≤ cubicDiscr - (diagonalOperator (fun k => f.coeff k / (Nat.choose 3 k : ℝ)) q) - -/-- The normalized diagonal base case is equivalent to the level-three -Schur--Szego cubic-discriminant base case. -/ -theorem pfCubicDiscrDiagonalNonnegStatement_iff : - pfCubicDiscrDiagonalNonnegStatement ↔ - ∀ {f q : ℝ[X]}, - IsPFPolynomial f → - f.natDegree ≤ 3 → - q.natDegree ≤ 3 → - q.Splits → - 0 ≤ cubicDiscr (schurSzegoComp 3 f q) := by - simp only [pfCubicDiscrDiagonalNonnegStatement, - cubicDiscr_diagonalOperator_normalized_three_eq_cubicDiscr_schurSzegoComp] - -/-- The classical fixed-degree Schur--Szego theorem discharges the isolated -level-three diagonal cubic-discriminant base case. -/ -theorem pfCubicDiscrDiagonalNonnegStatement_of_schurSzego - (hSZ : finiteSchurSzegoCompositionStatement) : - pfCubicDiscrDiagonalNonnegStatement := - pfCubicDiscrDiagonalNonnegStatement_iff.mpr fun {f q} hf hfdeg hqdeg hsplit => by - rcases hSZ hf hfdeg hqdeg hsplit with hzero | hs - · simp [hzero, cubicDiscr] - · exact cubicDiscr_nonneg_of_splits_natDegree_le_three - ((natDegree_schurSzegoComp_le_left 3 f q).trans hfdeg) hs - -/-- The isolated level-three diagonal base case proves the reflected -diagonal-operator discriminant input at every level `n ≥ 3`. -/ -theorem cubicDiscr_reflect_diagonalOperator_nonneg_of_pfCubicDiscrDiagonalNonneg - (h : pfCubicDiscrDiagonalNonnegStatement) - {n : ℕ} (hn : 3 ≤ n) {f p : ℝ[X]} - (hf : IsPFPolynomial f) (hfdeg : f.natDegree ≤ 3) - (hpdeg : p.natDegree ≤ n) (hsplit : p.Splits) : - 0 ≤ cubicDiscr - (diagonalOperator (fun k => f.coeff k / (Nat.choose 3 k : ℝ)) - (reflect 3 ((derivative^[n - 3]) (reflect n p)))) := - h hf hfdeg - (natDegree_reflect_iterate_derivative_reflect_le_three hn hpdeg) - (reflect_iterate_derivative_reflect_splits_of_splits hn hpdeg hsplit) - -/-- The isolated level-three diagonal base case proves high-level -cubic-discriminant nonnegativity for degree-`≤ 3` PF factors. -/ -theorem cubicDiscr_schurSzegoComp_nonneg_of_pf_factor_le_three_of_pfDiagonalBase - (h : pfCubicDiscrDiagonalNonnegStatement) - {n : ℕ} (hn : 3 ≤ n) {f p : ℝ[X]} - (hf : IsPFPolynomial f) (hfdeg : f.natDegree ≤ 3) - (hpdeg : p.natDegree ≤ n) (hsplit : p.Splits) : - 0 ≤ cubicDiscr (schurSzegoComp n f p) := - cubicDiscr_schurSzegoComp_nonneg_of_reflect_diagonalOperator_three - hn hfdeg hpdeg - (cubicDiscr_reflect_diagonalOperator_nonneg_of_pfCubicDiscrDiagonalNonneg - h hn hf hfdeg hpdeg hsplit) - /-- Low-level (`n < 3`) cubic-discriminant nonnegativity for a degree-`≤ 3` PF factor with `f.natDegree ≤ n`. -/ private theorem cubicDiscr_schurSzegoComp_nonneg_of_pf_factor_natDegree_lt_three @@ -207,49 +145,6 @@ private theorem cubicDiscr_schurSzegoComp_nonneg_of_pf_factor_natDegree_lt_three · exact cubicDiscr_nonneg_of_splits_natDegree_le_three ((natDegree_schurSzegoComp_le_left n f p).trans hfdeg) hs -/-- The isolated level-three diagonal base case proves the corrected all-level -cubic-discriminant route retaining `f.natDegree ≤ n`. -/ -theorem cubicDiscr_schurSzegoComp_nonneg_of_pf_factor_le_three_leftNatDegree_of_pfDiagonalBase - (h : pfCubicDiscrDiagonalNonnegStatement) - {n : ℕ} {f p : ℝ[X]} - (hf : IsPFPolynomial f) (hfdeg : f.natDegree ≤ 3) - (hfn : f.natDegree ≤ n) (hpdeg : p.natDegree ≤ n) (hsplit : p.Splits) : - 0 ≤ cubicDiscr (schurSzegoComp n f p) := - (le_or_gt 3 n).elim - (fun hn => - cubicDiscr_schurSzegoComp_nonneg_of_pf_factor_le_three_of_pfDiagonalBase - h hn hf hfdeg hpdeg hsplit) - (fun hn => - cubicDiscr_schurSzegoComp_nonneg_of_pf_factor_natDegree_lt_three - hn hf hfdeg hfn hpdeg hsplit) - -/-- The isolated level-three diagonal base case discharges the high-level -degree-`≤ 3` PF-factor Schur--Szego route. -/ -theorem finiteSchurSzegoComposition_of_pf_factor_le_three_of_pfCubicDiscrDiagonalNonneg - (h : pfCubicDiscrDiagonalNonnegStatement) - {n : ℕ} (hn : 3 ≤ n) {f p : ℝ[X]} - (hf : IsPFPolynomial f) (hfdeg : f.natDegree ≤ 3) - (hpdeg : p.natDegree ≤ n) (hsplit : p.Splits) : - schurSzegoComp n f p = 0 ∨ (schurSzegoComp n f p).Splits := - finiteSchurSzegoComposition_of_pf_factor_natDegree_le_three_cubicDiscr_nonneg - hf hfdeg hpdeg hsplit - (cubicDiscr_schurSzegoComp_nonneg_of_pf_factor_le_three_of_pfDiagonalBase - h hn hf hfdeg hpdeg hsplit) - -/-- Corrected all-level degree-`≤ 3` PF-factor Schur--Szego route from the -isolated level-three diagonal base case, retaining `f.natDegree ≤ n`. -/ -theorem - finiteSchurSzegoComposition_of_pf_factor_le_three_leftNatDegree_of_pfCubicDiscrDiagonalNonneg - (h : pfCubicDiscrDiagonalNonnegStatement) - {n : ℕ} {f p : ℝ[X]} - (hf : IsPFPolynomial f) (hfdeg : f.natDegree ≤ 3) - (hfn : f.natDegree ≤ n) (hpdeg : p.natDegree ≤ n) (hsplit : p.Splits) : - schurSzegoComp n f p = 0 ∨ (schurSzegoComp n f p).Splits := - finiteSchurSzegoComposition_of_pf_factor_natDegree_le_three_cubicDiscr_nonneg - hf hfdeg hpdeg hsplit - (cubicDiscr_schurSzegoComp_nonneg_of_pf_factor_le_three_leftNatDegree_of_pfDiagonalBase - h hf hfdeg hfn hpdeg hsplit) - /-- Degree-`≤ 3` PF-factor Schur--Szegő composition reduced to the denominator-cleared cubic-discriminant numerator at levels `n ≥ 3`. -/ theorem finiteSchurSzegoComposition_of_pf_factor_natDegree_le_three_cubicDiscrNumerator_nonneg @@ -313,44 +208,4 @@ theorem finiteSchurSzegoCompositionNonzero_of_pf_factor_natDegree_le_three_cubic finiteSchurSzegoComposition_of_pf_factor_natDegree_le_three_cubicDiscr_nonneg hf hfdeg hpdeg hsplit hdisc -/-- The full finite Schur--Szegő theorem implies the finite Pólya--Schur -theorem. -/ -theorem finitePolyaSchur_nonneg_of_schurSzego - (hSZ : finiteSchurSzegoCompositionStatement) : - finitePolyaSchurNonnegStatement := - finitePolyaSchur_nonneg_of_backward - (finitePolyaSchurNonnegBackward_of_schurSzego hSZ) - -/-- Fixed-degree Schur--Szegő composition and finite Pólya--Schur are -equivalent classical inputs in the nonnegative-coefficient convention used -here. -/ -theorem finiteSchurSzegoCompositionStatement_iff_finitePolyaSchur : - finiteSchurSzegoCompositionStatement ↔ finitePolyaSchurNonnegStatement := - ⟨finitePolyaSchur_nonneg_of_schurSzego, - finiteSchurSzegoComposition_of_finitePolyaSchur⟩ - -/-- The finite Pólya--Schur theorem implies the nonzero core of fixed-degree -Schur--Szegő composition. -/ -theorem finiteSchurSzegoCompositionNonzero_of_finitePolyaSchur - (hFPS : finitePolyaSchurNonnegStatement) : - finiteSchurSzegoCompositionNonzeroStatement := - finiteSchurSzegoCompositionNonzero_of_full - (finiteSchurSzegoComposition_of_finitePolyaSchur hFPS) - -/-- The nonzero core of fixed-degree Schur--Szegő composition and finite -Pólya--Schur are equivalent classical inputs in the local convention. -/ -theorem finiteSchurSzegoCompositionNonzeroStatement_iff_finitePolyaSchur : - finiteSchurSzegoCompositionNonzeroStatement ↔ finitePolyaSchurNonnegStatement := - ⟨finitePolyaSchur_nonneg_of_schurSzegoNonzero, - finiteSchurSzegoCompositionNonzero_of_finitePolyaSchur⟩ - -/-- The nonzero Schur--Szegő core is equivalent to the hard backward direction -of finite Pólya--Schur. -/ -theorem finiteSchurSzegoCompositionNonzeroStatement_iff_finitePolyaSchurBackward : - finiteSchurSzegoCompositionNonzeroStatement ↔ - finitePolyaSchurNonnegBackwardStatement := - ⟨finitePolyaSchurNonnegBackward_of_schurSzegoNonzero, - fun hBack => - finiteSchurSzegoCompositionNonzero_of_finitePolyaSchur - (finitePolyaSchur_nonneg_of_backward hBack)⟩ end RealRooted diff --git a/RealRooted/Hadamard/Finite.lean b/RealRooted/Hadamard/Finite.lean index fb037f630..db0f2d6f5 100644 --- a/RealRooted/Hadamard/Finite.lean +++ b/RealRooted/Hadamard/Finite.lean @@ -7,119 +7,18 @@ noncomputable section namespace RealRooted /-! -# Finite Schur--Szego composition interfaces +# Low-degree finite Schur--Szego composition -Classical finite composition statements, their finite Polya--Schur reductions, -and the degree-two discriminant base case. +The degree-two Schur--Szegő composition base cases and the discriminant +inequality. The general theorem is `finiteSchurSzegoComposition` in +`RealRooted.Hadamard.Grace`. -/ -/-- **Finite Schur--Szegő composition theorem** (classical input). - -If `f` is a PF polynomial (only real, nonpositive zeros) of degree at most `n` -and `p` has only real zeros, then their fixed-degree Schur--Szegő composition -`schurSzegoComp n f p` again has only real zeros, unless it vanishes -identically. - -This is the classical composition/coincidence result of Schur and Szegő; it is -the single remaining analytic input behind the backward direction of the finite -Pólya--Schur theorem, isolated here as a named statement. -/ -def finiteSchurSzegoCompositionStatement : Prop := - ∀ {n : ℕ} {f p : ℝ[X]}, - IsPFPolynomial f → - f.natDegree ≤ n → - p.natDegree ≤ n → - p.Splits → - schurSzegoComp n f p = 0 ∨ (schurSzegoComp n f p).Splits - -/-- Nonzero core of the finite Schur--Szegő composition theorem. The full -statement is equivalent to this one because the zero cases make the composition -identically zero. -/ -def finiteSchurSzegoCompositionNonzeroStatement : Prop := - ∀ {n : ℕ} {f p : ℝ[X]}, - IsPFPolynomial f → - f ≠ 0 → - f.natDegree ≤ n → - p ≠ 0 → - p.natDegree ≤ n → - p.Splits → - schurSzegoComp n f p = 0 ∨ (schurSzegoComp n f p).Splits - -theorem finiteSchurSzegoCompositionNonzero_of_full - (h : finiteSchurSzegoCompositionStatement) : - finiteSchurSzegoCompositionNonzeroStatement := - fun hf _hf0 hfdeg _hp0 hpdeg hp => h hf hfdeg hpdeg hp - -theorem finiteSchurSzegoComposition_of_nonzero - (h : finiteSchurSzegoCompositionNonzeroStatement) : - finiteSchurSzegoCompositionStatement := by - intro n f p hf hfdeg hpdeg hp - by_cases hf0 : f = 0 - · simp [hf0, schurSzegoComp_zero_left] - by_cases hp0 : p = 0 - · simp [hp0, schurSzegoComp_zero_right] - exact h hf hf0 hfdeg hp0 hpdeg hp - -theorem finiteSchurSzegoCompositionStatement_iff_nonzero : - finiteSchurSzegoCompositionStatement ↔ - finiteSchurSzegoCompositionNonzeroStatement := - ⟨finiteSchurSzegoCompositionNonzero_of_full, - finiteSchurSzegoComposition_of_nonzero⟩ - -/-- The backward direction of the finite Pólya--Schur theorem follows, by a -fully checked reduction, from the finite Schur--Szegő composition theorem: the -diagonal operator attached to `gamma` acting on a polynomial `p` of degree at -most `n` is exactly the Schur--Szegő composition of the PF Jensen polynomial of -`gamma` with `p`. -/ -theorem finitePolyaSchurNonnegBackward_of_schurSzego - (hSZ : finiteSchurSzegoCompositionStatement) : - finitePolyaSchurNonnegBackwardStatement := by - intro n gamma _hgamma hjensen p hp hsplit - have hfdeg : (jensenPolynomial n gamma).natDegree ≤ n := - natDegree_jensenPolynomial_le n gamma - simpa [← schurSzegoComp_jensenPolynomial_eq_diagonalOperator_of_natDegree_le hp] using - hSZ hjensen hfdeg hp hsplit - -/-- The backward finite Pólya--Schur direction follows directly from the -nonzero core of the finite Schur--Szegő theorem. -/ -theorem finitePolyaSchurNonnegBackward_of_schurSzegoNonzero - (hSZ : finiteSchurSzegoCompositionNonzeroStatement) : - finitePolyaSchurNonnegBackwardStatement := - finitePolyaSchurNonnegBackward_of_schurSzego - (finiteSchurSzegoComposition_of_nonzero hSZ) - -/-- Full finite Pólya--Schur from the nonzero core of finite Schur--Szegő. -/ -theorem finitePolyaSchur_nonneg_of_schurSzegoNonzero - (hSZ : finiteSchurSzegoCompositionNonzeroStatement) : - finitePolyaSchurNonnegStatement := - finitePolyaSchur_nonneg_of_backward - (finitePolyaSchurNonnegBackward_of_schurSzegoNonzero hSZ) - -/-- The finite Pólya--Schur theorem implies fixed-degree Schur--Szegő -composition. - -The diagonal sequence used here is the binomially normalized coefficient -sequence of the PF factor. The theorem -`jensenPolynomial_normalized_coeff_eq_of_natDegree_le` identifies its Jensen -polynomial with that factor, and the fixed-degree Schur--Szegő composition is -the corresponding diagonal operator on the other factor. -/ -theorem finiteSchurSzegoComposition_of_finitePolyaSchur - (hFPS : finitePolyaSchurNonnegStatement) : - finiteSchurSzegoCompositionStatement := by - intro n f p hf hfdeg hpdeg hsplit - let gamma : ℕ → ℝ := fun k => f.coeff k / (Nat.choose n k : ℝ) - have hgamma : ∀ k, 0 ≤ gamma k := fun k => - div_nonneg (hf.hasNonnegCoeffs k) (by positivity) - have hjensen : IsPFPolynomial (jensenPolynomial n gamma) := by - simpa [gamma] using hf.jensenPolynomial_normalized_coeff_of_natDegree_le hfdeg - rw [schurSzegoComp_comm] - simpa [gamma, schurSzegoComp_eq_diagonalOperator] using - ((hFPS hgamma).2 hjensen) hpdeg hsplit - /-- Low-degree fixed-degree Schur--Szegő composition, through degree two. This is the specialization of the finite Pólya--Schur route using the checked degree-`≤ 2` backward theorem from `RealRooted.MultiplierSequence`; it does -not use the remaining classical Schur--Szegő input. -/ +not use the general Schur--Szegő theorem. -/ theorem finiteSchurSzegoComposition_of_natDegree_le_two {n : ℕ} (hn : n ≤ 2) {f p : ℝ[X]} (hf : IsPFPolynomial f) (hfdeg : f.natDegree ≤ n) diff --git a/RealRooted/Hadamard/GarloffWagner.lean b/RealRooted/Hadamard/GarloffWagner.lean index 2f2b5426c..ac05661d3 100644 --- a/RealRooted/Hadamard/GarloffWagner.lean +++ b/RealRooted/Hadamard/GarloffWagner.lean @@ -10,10 +10,10 @@ noncomputable section namespace RealRooted /-! -# Garloff--Wagner Hadamard interfaces +# Garloff--Wagner Hadamard theorems Nonnegative coefficient closure, odd/even algebra, and the checked direct -interlacing wrappers around the Garloff--Wagner route. +interlacing theorems of Garloff--Wagner. -/ /-- Nonnegative coefficients are preserved by coefficientwise Hadamard @@ -40,52 +40,12 @@ theorem hadamardProduct_oddEvenPolynomial (p q p' q' : ℝ[X]) : · subst hk simp -/-- Nonnegative-coefficient Schur--Polya/Garloff--Wagner real-rootedness -interface for coefficientwise Hadamard products. - -Garloff--Wagner, Theorem 4(a), proves this in the standard-polynomial setting -with only nonpositive zeros. The hypotheses below are the corresponding -nonnegative-coefficient wrapper: real-rooted nonzero polynomials with -nonnegative coefficients automatically have only nonpositive roots. The conclusion is -zero-aware because the Hadamard product can vanish when supports are disjoint. --/ -def garloffWagnerHadamardNonnegRealRootedStatement : Prop := - ∀ {p q : ℝ[X]}, - HasNonnegCoeffs p → - HasNonnegCoeffs q → - (p ≠ 0 ∧ p.Splits) → - (q ≠ 0 ∧ q.Splits) → - (hadamardProduct p q = 0 ∨ (hadamardProduct p q).Splits) ∧ - HasNonnegCoeffs (hadamardProduct p q) ∧ - ∀ r ∈ (hadamardProduct p q).roots, r ≤ 0 - -theorem IsPFPolynomial.hadamardProduct - (hGW : garloffWagnerHadamardNonnegRealRootedStatement) - {p q : ℝ[X]} +/-- PF polynomials are closed under coefficientwise Hadamard products +(Schur--Pólya--Wagner; Garloff--Wagner, Theorem 4(a)). -/ +theorem IsPFPolynomial.hadamardProduct {p q : ℝ[X]} (hp : IsPFPolynomial p) (hq : IsPFPolynomial q) : - IsPFPolynomial (hadamardProduct p q) := by - by_cases hp0 : p = 0 - · subst p - simpa using IsPFPolynomial.zero - by_cases hq0 : q = 0 - · subst q - simpa using IsPFPolynomial.zero - rcases hGW hp.hasNonnegCoeffs hq.hasNonnegCoeffs - (hp.ne_zero_and_splits hp0) - (hq.ne_zero_and_splits hq0) with ⟨hrr, hnn, hroots⟩ - exact ⟨hnn, hrr, hroots⟩ - -/-- Polynomial PF form of the Schur--Polya--Wagner Hadamard theorem. -/ -def schurPolyaWagnerHadamardPFStatement : Prop := - ∀ {p q : ℝ[X]}, - IsPFPolynomial p → - IsPFPolynomial q → - IsPFPolynomial (hadamardProduct p q) - -theorem schurPolyaWagnerHadamardPF_of_garloffWagner_nonneg - (hGW : garloffWagnerHadamardNonnegRealRootedStatement) : - schurPolyaWagnerHadamardPFStatement := - fun hp hq => hp.hadamardProduct hGW hq + IsPFPolynomial (hadamardProduct p q) := + gwHadamardProductPF hp hq /- Nonnegative-coefficient Garloff--Wagner interlacing interface for coefficientwise Hadamard products. @@ -93,8 +53,8 @@ coefficientwise Hadamard products. This is the `StrictInterl`/`Interl` wrapper around Garloff--Wagner, Theorem 4(b): if two nonnegative-coefficient real-rooted pairs are in the same interlacing relation, then the pair of Hadamard products is again in -interlacing. The conclusion is zero-aware for the same support reason as -`garloffWagnerHadamardNonnegRealRootedStatement`. +interlacing. The conclusion is zero-aware because the Hadamard product can +vanish when supports are disjoint. Orientation audit: in this repository `StrictInterl f g` is the convention `f ≪ g`. In the differ-by-one case, `g` has the rightmost root; in the same-degree case, @@ -104,8 +64,7 @@ roots are `-b` and `-a`. Consequently the Garloff--Wagner hypotheses written as `g $ f` and `q $ p` are represented here as `StrictInterl f g` and `StrictInterl p q`, and the conclusion is `Interl (f ⊙ p) (g ⊙ q)`. -This statement is proved directly in `RealRooted.GarloffWagner`; the wrapper -keeps the historical `Hadamard` API used by downstream theorem bundles. +The proof is `gwHadamardProductNonnegInterl` in `RealRooted.GarloffWagner`. -/ /-- Hadamard product preserves interlacing in the nonnegative setting (Garloff--Wagner, Theorem 4(b)). -/ diff --git a/RealRooted/Hadamard/Grace.lean b/RealRooted/Hadamard/Grace.lean index c21a3fd58..bd2c3e262 100644 --- a/RealRooted/Hadamard/Grace.lean +++ b/RealRooted/Hadamard/Grace.lean @@ -494,21 +494,32 @@ theorem splits_schurSzegoComp_of_isPF (n : Nat) : (p := reflect n p) hinner grind -/-- Nonzero finite Schur--Szegő composition theorem. This is the substantive -classical leaf: `f` is a nonzero PF polynomial, `p` is a nonzero real-rooted -polynomial, both have degree at most `n`, and the fixed-degree Schur--Szegő -composition is either zero or real-rooted. -/ -theorem finiteSchurSzegoCompositionNonzero : - finiteSchurSzegoCompositionNonzeroStatement := - fun {n} {f} {p} hf hf0 hfdeg hp0 hp hsplit => - Or.inr (splits_schurSzegoComp_of_isPF n f p hf hf0 hfdeg hp0 hp hsplit) - -/-- Finite Schur--Szegő composition theorem. The degenerate cases (`f = 0` or -`p = 0`, where the composition vanishes) are discharged by -`finiteSchurSzegoComposition_of_nonzero`; the remaining classical content is -`finiteSchurSzegoCompositionNonzero`. -/ -theorem finiteSchurSzegoComposition : finiteSchurSzegoCompositionStatement := - finiteSchurSzegoComposition_of_nonzero finiteSchurSzegoCompositionNonzero +/-- Nonzero finite Schur--Szegő composition theorem: `f` is a nonzero PF +polynomial, `p` is a nonzero real-rooted polynomial, both have degree at most +`n`, and the fixed-degree Schur--Szegő composition is either zero or +real-rooted. -/ +theorem finiteSchurSzegoCompositionNonzero {n : ℕ} {f p : ℝ[X]} + (hf : IsPFPolynomial f) (hf0 : f ≠ 0) (hfdeg : f.natDegree ≤ n) + (hp0 : p ≠ 0) (hpdeg : p.natDegree ≤ n) (hsplit : p.Splits) : + schurSzegoComp n f p = 0 ∨ (schurSzegoComp n f p).Splits := + Or.inr (splits_schurSzegoComp_of_isPF n f p hf hf0 hfdeg hp0 hpdeg hsplit) + +/-- **Finite Schur--Szegő composition theorem.** + +If `f` is a PF polynomial (only real, nonpositive zeros) of degree at most `n` +and `p` has only real zeros, then their fixed-degree Schur--Szegő composition +`schurSzegoComp n f p` again has only real zeros, unless it vanishes +identically. The degenerate cases `f = 0` and `p = 0` make the composition +vanish; the remaining content is `finiteSchurSzegoCompositionNonzero`. -/ +theorem finiteSchurSzegoComposition {n : ℕ} {f p : ℝ[X]} + (hf : IsPFPolynomial f) (hfdeg : f.natDegree ≤ n) + (hpdeg : p.natDegree ≤ n) (hsplit : p.Splits) : + schurSzegoComp n f p = 0 ∨ (schurSzegoComp n f p).Splits := by + by_cases hf0 : f = 0 + · simp [hf0, schurSzegoComp_zero_left] + by_cases hp0 : p = 0 + · simp [hp0, schurSzegoComp_zero_right] + exact finiteSchurSzegoCompositionNonzero hf hf0 hfdeg hp0 hpdeg hsplit /-- Directly applicable form of the finite Schur--Szegő composition theorem: for a PF polynomial `f` and a real-rooted polynomial `p`, both of degree at most @@ -541,13 +552,17 @@ theorem IsPFPolynomial.schurSzegoComp hf hfdeg hpdeg (hp.eq_zero_or_splits.resolve_left hp0) /-- The backward direction of the finite Pólya--Schur theorem, obtained from the -finite Schur--Szegő composition theorem. -/ -theorem finitePolyaSchurNonnegBackward : finitePolyaSchurNonnegBackwardStatement := - finitePolyaSchurNonnegBackward_of_schurSzegoNonzero finiteSchurSzegoCompositionNonzero - -/-- Classical finite Pólya--Schur theorem (nonnegative-coefficient convention). -The only remaining analytic obligation is isolated in -`finiteSchurSzegoComposition`. -/ +finite Schur--Szegő composition theorem: the diagonal operator attached to +`gamma` acting on a polynomial `p` of degree at most `n` is exactly the +Schur--Szegő composition of the PF Jensen polynomial of `gamma` with `p`. -/ +theorem finitePolyaSchurNonnegBackward : finitePolyaSchurNonnegBackwardStatement := by + intro n gamma _hgamma hjensen p hp hsplit + have hfdeg : (jensenPolynomial n gamma).natDegree ≤ n := + natDegree_jensenPolynomial_le n gamma + simpa [← schurSzegoComp_jensenPolynomial_eq_diagonalOperator_of_natDegree_le hp] using + finiteSchurSzegoComposition hjensen hfdeg hp hsplit + +/-- Classical finite Pólya--Schur theorem (nonnegative-coefficient convention). -/ theorem finitePolyaSchur_nonneg : finitePolyaSchurNonnegStatement := - finitePolyaSchur_nonneg_of_schurSzegoNonzero finiteSchurSzegoCompositionNonzero + finitePolyaSchur_nonneg_of_backward finitePolyaSchurNonnegBackward end RealRooted diff --git a/RealRooted/Hadamard/Hurwitz.lean b/RealRooted/Hadamard/Hurwitz.lean index 84cb666c3..6487d5e75 100644 --- a/RealRooted/Hadamard/Hurwitz.lean +++ b/RealRooted/Hadamard/Hurwitz.lean @@ -8,27 +8,27 @@ noncomputable section namespace RealRooted /-! -# Hurwitz Hadamard reductions +# Hadamard products and Hurwitz stability -The Hurwitz-stability and Hurwitz-matrix interfaces for Garloff--Wagner -Theorem 1, including the checked low-order reductions. +The open Garloff--Wagner Theorem 1 target, and checked low-order facts about +the row-oriented Hurwitz matrix of a Hadamard product. -/ /-- **Hadamard product preserves Hurwitz stability** (Garloff--Wagner, -Theorem 1) — precise external interface. +Theorem 1). Unproved target, tracked in GitHub issue #1095. This is the main theorem of Garloff--Wagner, *Hadamard Products of Stable -Polynomials Are Stable*: the coefficientwise Hadamard product of two -Hurwitz-stable real polynomials is again Hurwitz stable, provided the -coefficientwise product is nonzero. The nonzero side condition is part of the -interface because this project's `IsHurwitzStable` convention excludes the zero -polynomial, while coefficientwise products of two nonzero stable polynomials can -vanish when their coefficient supports are disjoint. This is the genuinely -deep classical input (its classical proofs go through Polya--Schur / -total-nonnegativity machinery that is not available in Mathlib), recorded here -as a precise interface. This is the only new external interface needed below; -the remaining inputs are the Hermite--Biehler odd/even bridges already recorded -in `RealRooted.VeroneseSection`. -/ +Polynomials Are Stable*, J. Math. Anal. Appl. 202 (1996), 797--809: the +coefficientwise Hadamard product of two Hurwitz-stable real polynomials is again +Hurwitz stable, provided the coefficientwise product is nonzero. The nonzero +side condition is needed because this project's `IsHurwitzStable` convention +excludes the zero polynomial, while coefficientwise products of two nonzero +stable polynomials can vanish when their coefficient supports are disjoint. + +The interlacing form, Garloff--Wagner Theorem 4(b), is proved as +`gwHadamardProductInterl_of_strictInterl`. Total nonnegativity of infinite +row-oriented Hurwitz matrices is not closed under entrywise products +(`not_hurwitz_schurProduct_isTotallyNonneg`), so that route does not apply. -/ def hadamardPreservesHurwitzStableStatement : Prop := ∀ {a b : ℝ[X]}, IsHurwitzStable a → @@ -36,60 +36,6 @@ def hadamardPreservesHurwitzStableStatement : Prop := hadamardProduct a b ≠ 0 → IsHurwitzStable (hadamardProduct a b) -/-! ### Sharper sub-interfaces for Garloff--Wagner Theorem 1 - -The Hurwitz-stability conclusion `IsHurwitzStable (hadamardProduct a b)` unfolds -to two parts: nonnegativity of the coefficients and right-half-plane stability -of the complexification. The first part is elementary -(`HasNonnegCoeffs.hadamardProduct`); the genuinely deep content is the second -part. We record that split, and the faithful Hurwitz-matrix decomposition of -Garloff--Wagner Theorem 1, as fully checked reductions. -/ - -/-- The deep half of Garloff--Wagner Theorem 1: the complexified coefficientwise -Hadamard product of two right-half-plane-stable, nonnegative-coefficient -polynomials is again right-half-plane stable when the product is nonzero. -/ -def hadamardPreservesRightHalfPlaneStableStatement : Prop := - ∀ {a b : ℝ[X]}, - HasNonnegCoeffs a → - HasNonnegCoeffs b → - IsRightHalfPlaneStable (complexify a) → - IsRightHalfPlaneStable (complexify b) → - hadamardProduct a b ≠ 0 → - IsRightHalfPlaneStable (complexify (hadamardProduct a b)) - -/-- Reduction of Garloff--Wagner Theorem 1 to its deep half: the -nonnegative-coefficient half of Hurwitz stability is discharged here, so only -right-half-plane stability of the product remains. -/ -theorem hadamardPreservesHurwitzStable_of_rightHalfPlane - (h : hadamardPreservesRightHalfPlaneStableStatement) : - hadamardPreservesHurwitzStableStatement := - fun ha hb hprod => ⟨ha.1.hadamardProduct hb.1, h ha.1 hb.1 ha.2 hb.2 hprod⟩ - -/-- The analytic core is conversely implied by Garloff--Wagner Theorem 1, so the -two interfaces are equivalent: isolating the right-half-plane half loses no -content. -/ -theorem hadamardPreservesRightHalfPlaneStable_of_hurwitzStable - (h : hadamardPreservesHurwitzStableStatement) : - hadamardPreservesRightHalfPlaneStableStatement := - fun hann hbnn harhp hbrhp hprod => (h ⟨hann, harhp⟩ ⟨hbnn, hbrhp⟩ hprod).2 - -/-- Garloff--Wagner Theorem 1 is equivalent to its right-half-plane analytic -core; coefficient nonnegativity of the product is elementary. -/ -theorem hadamardPreservesHurwitzStable_iff_rightHalfPlane : - hadamardPreservesHurwitzStableStatement ↔ - hadamardPreservesRightHalfPlaneStableStatement := - ⟨hadamardPreservesRightHalfPlaneStable_of_hurwitzStable, - hadamardPreservesHurwitzStable_of_rightHalfPlane⟩ - -/-- The combinatorial heart of Garloff--Wagner Theorem 1, as a pure matrix -statement: total nonnegativity of the row-oriented Hurwitz matrix is preserved -under coefficientwise products. -/ -def hadamardPreservesHurwitzMatrixTNStatement : Prop := - ∀ {a b : ℝ[X]}, - (hurwitz a.coeff).IsTotallyNonneg → - (hurwitz b.coeff).IsTotallyNonneg → - (hurwitz (hadamardProduct a b).coeff).IsTotallyNonneg - /-- Hurwitz-matrix form of the coefficientwise Hadamard product of two polynomials. -/ theorem hurwitz_hadamardProduct_matrix (a b : ℝ[X]) : @@ -100,10 +46,9 @@ theorem hurwitz_hadamardProduct_matrix (a b : ℝ[X]) : exact coeff_hadamardProduct a b n] exact hurwitz_mul_entrywise_matrix a.coeff b.coeff -/-- Low-order checked part of the Hurwitz-matrix Hadamard leaf: every minor of -size at most two is nonnegative. The first remaining case for -`hadamardPreservesHurwitzMatrixTNStatement` is the `3 × 3` Hurwitz-specific -minor. -/ +/-- Every minor of size at most two of the Hurwitz matrix of a Hadamard +product of two polynomials with totally nonnegative Hurwitz matrices is +nonnegative. -/ theorem hadamardPreservesHurwitzMatrixTN_det_of_card_le_two {a b : ℝ[X]} (ha : (hurwitz a.coeff).IsTotallyNonneg) (hb : (hurwitz b.coeff).IsTotallyNonneg) @@ -131,134 +76,4 @@ theorem hurwitz_hadamardProduct_det_fin_three_nonneg_of_band_fail 0 ≤ ((hurwitz (hadamardProduct a b).coeff).submatrix rows cols).det := by rw [hurwitz_hadamardProduct_det_fin_three_of_band_fail hrows hcols l hl] -/-- `3 × 3` Hurwitz-matrix Hadamard minors from the pure in-band `3 × 3` -matrix core. The out-of-band case is handled structurally by the -band-fail zero lemma. -/ -theorem hadamardPreservesHurwitzMatrixTN_det_fin_three - (hInBand : HurwitzMatrixSchurProductDetFinThreeInBandStatement) - {a b : ℝ[X]} (ha : (hurwitz a.coeff).IsTotallyNonneg) - (hb : (hurwitz b.coeff).IsTotallyNonneg) - {rows cols : Fin 3 → ℕ} (hrows : StrictMono rows) (hcols : StrictMono cols) : - 0 ≤ ((hurwitz (hadamardProduct a b).coeff).submatrix rows cols).det := by - simpa [hurwitz_hadamardProduct_matrix] using - hurwitz_schurProduct_det_fin_three hInBand ha hb hrows hcols - -/-- Low-order checked part of the Hurwitz-matrix Hadamard leaf through size -three, assuming the pure in-band `3 × 3` matrix core. -/ -theorem hadamardPreservesHurwitzMatrixTN_det_of_card_le_three - (hInBand : HurwitzMatrixSchurProductDetFinThreeInBandStatement) - {a b : ℝ[X]} (ha : (hurwitz a.coeff).IsTotallyNonneg) - (hb : (hurwitz b.coeff).IsTotallyNonneg) - {n : ℕ} {rows cols : Fin n → ℕ} (hrows : StrictMono rows) (hcols : StrictMono cols) - (hn : n ≤ 3) : - 0 ≤ (((hurwitz (hadamardProduct a b).coeff).submatrix rows cols).det) := by - simpa [hurwitz_hadamardProduct_matrix] using - hurwitz_schurProduct_det_of_card_le_three hInBand ha hb hrows hcols hn - -/-- Low-order, size-`≤ 3`, form of the Hurwitz-matrix Hadamard leaf. -/ -def hadamardPreservesHurwitzMatrixTNDetLeThreeStatement : Prop := - ∀ {a b : ℝ[X]}, - (hurwitz a.coeff).IsTotallyNonneg → - (hurwitz b.coeff).IsTotallyNonneg → - ∀ {n : ℕ} {rows cols : Fin n → ℕ}, - StrictMono rows → - StrictMono cols → - n ≤ 3 → - 0 ≤ (((hurwitz (hadamardProduct a b).coeff).submatrix rows cols).det) - -/-- The isolated in-band `3 × 3` core implies the low-order, size-`≤ 3`, -Hurwitz-matrix Hadamard leaf. -/ -theorem hadamardPreservesHurwitzMatrixTNDetLeThree_of_inBand - (hInBand : HurwitzMatrixSchurProductDetFinThreeInBandStatement) : - hadamardPreservesHurwitzMatrixTNDetLeThreeStatement := - @hadamardPreservesHurwitzMatrixTN_det_of_card_le_three hInBand - -/-- The fully in-band top-right subcase of the `3 × 3` Hurwitz Schur-product -core implies the low-order, size-`≤ 3`, Hurwitz-matrix Hadamard leaf. -/ -theorem hadamardPreservesHurwitzMatrixTNDetLeThree_of_fullBand - (hF : HurwitzMatrixSchurProductDetFinThreeCoreFullBandStatement) : - hadamardPreservesHurwitzMatrixTNDetLeThreeStatement := - hadamardPreservesHurwitzMatrixTNDetLeThree_of_inBand - (hurwitzMatrixSchurProductDetFinThreeInBand_of_fullBand hF) - -/-- The single-matrix corner-zeroed determinant subtarget implies the -low-order, size-`≤ 3`, Hurwitz-matrix Hadamard leaf. -/ -theorem hadamardPreservesHurwitzMatrixTNDetLeThree_of_cornerZeroedSingle - (hSingle : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleStatement) : - hadamardPreservesHurwitzMatrixTNDetLeThreeStatement := - hadamardPreservesHurwitzMatrixTNDetLeThree_of_inBand - (hurwitzMatrixSchurProductDetFinThreeInBand_of_cornerZeroedSingle hSingle) - -/-- The column-normalized single-matrix corner-zeroed determinant subtarget -implies the low-order, size-`≤ 3`, Hurwitz-matrix Hadamard leaf. -/ -theorem hadamardPreservesHurwitzMatrixTNDetLeThree_of_cornerZeroedSingleColZero - (hZero : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleColZeroStatement) : - hadamardPreservesHurwitzMatrixTNDetLeThreeStatement := - hadamardPreservesHurwitzMatrixTNDetLeThree_of_cornerZeroedSingle - (hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingle_of_colZero hZero) - -/-- The first-column normal form implies the low-order, size-`≤ 3`, -Hurwitz-matrix Hadamard leaf. -/ -theorem hadamardPreservesHurwitzMatrixTNDetLeThree_of_cornerZeroedSingleFirstCol - (hFirst : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleFirstColStatement) : - hadamardPreservesHurwitzMatrixTNDetLeThreeStatement := - hadamardPreservesHurwitzMatrixTNDetLeThree_of_cornerZeroedSingleColZero - (hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleColZero_of_firstCol - hFirst) - -/-- The strict-remainder first-column branch implies the low-order, -size-`≤ 3`, Hurwitz-matrix Hadamard leaf. -/ -theorem - hadamardPreservesHurwitzMatrixTNDetLeThree_of_cornerZeroedSingleFirstColPositiveRemainder - (hPos : HurwitzMatrixSchurProductDetFirstColPositiveRemainderStatement) : - hadamardPreservesHurwitzMatrixTNDetLeThreeStatement := - hadamardPreservesHurwitzMatrixTNDetLeThree_of_cornerZeroedSingleFirstCol - (hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleFirstCol_of_positiveRemainder - hPos) - -/-- The pure size-`≤ 3` Hurwitz matrix Schur-product statement implies the -Hadamard-product Hurwitz-matrix size-`≤ 3` statement. -/ -theorem hadamardPreservesHurwitzMatrixTNDetLeThree_of_hurwitzLeThree - (hLeThree : HurwitzMatrixSchurProductDetLeThreeStatement) : - hadamardPreservesHurwitzMatrixTNDetLeThreeStatement := - fun {_a _b} ha hb {_n} {_rows} {_cols} hrows hcols hn => by - simpa [hurwitz_hadamardProduct_matrix] using hLeThree ha hb hrows hcols hn - -/-- The full Hurwitz-matrix Hadamard leaf implies its named low-order, -size-`≤ 3`, consequence. -/ -theorem hadamardPreservesHurwitzMatrixTNDetLeThree_of_matrixTN - (h : hadamardPreservesHurwitzMatrixTNStatement) : - hadamardPreservesHurwitzMatrixTNDetLeThreeStatement := - fun {_a _b} ha hb {_n} {_rows} {_cols} hrows hcols _hn => h ha hb hrows hcols - -/-- Odd/even coefficient-subsequence PF consequence of the Hurwitz-matrix -Hadamard leaf. -/ -def hadamardPreservesHurwitzMatrixOddEvenPFStatement : Prop := - ∀ {a b : ℝ[X]}, - (hurwitz a.coeff).IsTotallyNonneg → - (hurwitz b.coeff).IsTotallyNonneg → - IsPolyaFreqSeq (fun n => (hadamardProduct a b).coeff (2 * n + 1)) ∧ - IsPolyaFreqSeq (fun n => (hadamardProduct a b).coeff (2 * n)) - -/-- The Hurwitz-matrix Hadamard leaf makes the odd coefficient subsequence of -the Hadamard product Pólya-frequency. -/ -theorem hadamardProduct_oddCoeff_isPolyaFreqSeq_of_matrixTN - (h : hadamardPreservesHurwitzMatrixTNStatement) - {a b : ℝ[X]} (ha : (hurwitz a.coeff).IsTotallyNonneg) - (hb : (hurwitz b.coeff).IsTotallyNonneg) : - IsPolyaFreqSeq (fun n => (hadamardProduct a b).coeff (2 * n + 1)) := - hurwitz_isPolyaFreqSeq_odd (h ha hb) - -/-- The Hurwitz-matrix Hadamard leaf makes the even coefficient subsequence of -the Hadamard product Pólya-frequency. -/ -theorem hadamardProduct_evenCoeff_isPolyaFreqSeq_of_matrixTN - (h : hadamardPreservesHurwitzMatrixTNStatement) - {a b : ℝ[X]} (ha : (hurwitz a.coeff).IsTotallyNonneg) - (hb : (hurwitz b.coeff).IsTotallyNonneg) : - IsPolyaFreqSeq (fun n => (hadamardProduct a b).coeff (2 * n)) := - hurwitz_isPolyaFreqSeq_even (h ha hb) - end RealRooted diff --git a/RealRooted/HermiteBiehler/Basic.lean b/RealRooted/HermiteBiehler/Basic.lean index cd9dbae58..bf9f3358f 100644 --- a/RealRooted/HermiteBiehler/Basic.lean +++ b/RealRooted/HermiteBiehler/Basic.lean @@ -8,7 +8,7 @@ import Mathlib.Basic.Complex.Basic # Foundational Hermite--Biehler definitions This module contains real-polynomial complexification, univariate half-plane -stability, the Hermite--Biehler polynomial, and the splitness/stability bridge. +stability, the Hermite--Biehler polynomial, and the splitness/stability lemmas. It is independent of the forward and converse interlacing arguments. -/ diff --git a/RealRooted/HermiteBiehler/Converse.lean b/RealRooted/HermiteBiehler/Converse.lean index d04e6d357..84babe8ef 100644 --- a/RealRooted/HermiteBiehler/Converse.lean +++ b/RealRooted/HermiteBiehler/Converse.lean @@ -15,18 +15,6 @@ noncomputable section namespace RealRooted -/-- Planning stub for the converse Hermite--Biehler theorem. - -The exact orientation hypotheses may still be adjusted, but the target is that -upper-half-plane stability of `f + i g` forces an interlacing relation between --/ -abbrev hermiteBiehlerConverseStatement : Prop := - ∀ ⦃f g : ℝ[X]⦄, - HasPosLeadingCoeff f → - HasPosLeadingCoeff g → - IsUpperHalfPlaneStable (hermiteBiehlerPolynomial f g) → - StrictInterl g f ∨ StrictInterl f g - theorem isUpperHalfPlaneStable_cofactor_of_stable {f g : ℝ[X]} {r : ℝ} (hrf : f.IsRoot r) (hrg : g.IsRoot r) (hstab : IsUpperHalfPlaneStable (hermiteBiehlerPolynomial f g)) : diff --git a/RealRooted/HermiteBiehler/Forward.lean b/RealRooted/HermiteBiehler/Forward.lean index 08fd7d8f8..040327393 100644 --- a/RealRooted/HermiteBiehler/Forward.lean +++ b/RealRooted/HermiteBiehler/Forward.lean @@ -350,18 +350,6 @@ theorem isUpperHalfPlaneStable_of_cofactor {f g : ℝ[X]} {r : ℝ} intro h exact hz.ne' (by simpa using congrArg Complex.im h) -/-- Sign-normalized forward Hermite--Biehler bridge. - -This is the minimal sign-stable form used in downstream plumbing: -positive leading coefficients on both inputs prevent the false counterexample. --/ -abbrev hermiteBiehlerForwardPosStatement : Prop := - ∀ {f g : ℝ[X]}, - HasPosLeadingCoeff f → - HasPosLeadingCoeff g → - StrictInterl g f → - IsUpperHalfPlaneStable (hermiteBiehlerPolynomial f g) - theorem hermiteBiehlerForwardPos_general {f g : ℝ[X]} (hf : HasPosLeadingCoeff f) (hg : HasPosLeadingCoeff g) (hpq : StrictInterl g f) : IsUpperHalfPlaneStable (hermiteBiehlerPolynomial f g) := by diff --git a/RealRooted/HermiteBiehler/Hurwitz.lean b/RealRooted/HermiteBiehler/Hurwitz.lean index da28beee5..145298ea6 100644 --- a/RealRooted/HermiteBiehler/Hurwitz.lean +++ b/RealRooted/HermiteBiehler/Hurwitz.lean @@ -6,9 +6,9 @@ import RealRooted.HermiteBiehler.OddEven # Hermite--Biehler to Hurwitz stability This file applies the general converse Hermite--Biehler theorem to the -conformal odd/even substitution. It separates the analytic substitution -interfaces and the right-half-plane stability endpoint from the converse -root-geometry proof. +conformal odd/even substitution. It separates the upper-half-plane and +first-quadrant substitution lemmas and the right-half-plane stability theorem +from the converse root-geometry proof. -/ open Polynomial @@ -17,110 +17,17 @@ noncomputable section namespace RealRooted -/-- Analytic bridge from the Hermite--Biehler stable polynomial `q + i p` to -right-half-plane stability of `q(x^2) + x p(x^2)`. - -This isolates the classical conformal-substitution part of the --/ -abbrev HermiteBiehlerStableToHurwitzOddEvenStatement : Prop := - ∀ ⦃p q : ℝ[X]⦄, - HasNonnegCoeffs p → - HasNonnegCoeffs q → - IsUpperHalfPlaneStable (hermiteBiehlerPolynomial q p) → - IsRightHalfPlaneStable (complexify (oddEvenPolynomial p q)) - -/-! ## Reduction of the forward Hermite--Biehler/Hurwitz bridge to a -first-quadrant conformal-substitution interface -/ - -/-- First-quadrant form of the forward Hermite--Biehler/Hurwitz conformal -substitution: it suffices to exclude roots of `q(x²) + x p(x²)` in the open -first quadrant `{Re > 0, Im > 0}`. -/ -abbrev HermiteBiehlerStableToHurwitzOddEvenFirstQuadrantStatement : Prop := - ∀ ⦃p q : ℝ[X]⦄, - HasNonnegCoeffs p → - HasNonnegCoeffs q → - IsUpperHalfPlaneStable (hermiteBiehlerPolynomial q p) → - ∀ z : ℂ, 0 < z.re → 0 < z.im → - (complexify (oddEvenPolynomial p q)).eval z ≠ 0 - /-- Upper-half-plane substitution form of the forward Hermite--Biehler/Hurwitz -bridge: for any upper-half-plane point `w` with a right-half-plane square root -`z`, the Hurwitz combination `q(w) + z·p(w)` is nonzero. - -This is the genuinely analytic conformal-substitution core: the quadratic map -`z ↦ z²` sends the open first quadrant onto the open upper half-plane, so this -interface and the first-quadrant interface above carry exactly the same -content. -/ -abbrev HermiteBiehlerStableToHurwitzOddEvenUpperHalfSubstitutionStatement : Prop := - ∀ ⦃p q : ℝ[X]⦄, - HasNonnegCoeffs p → - HasNonnegCoeffs q → - IsUpperHalfPlaneStable (hermiteBiehlerPolynomial q p) → - ∀ ⦃w z : ℂ⦄, 0 < w.im → z ^ 2 = w → 0 < z.re → - (complexify q).eval w + z * (complexify p).eval w ≠ 0 - -/-- The first-quadrant interface follows from the upper-half-plane substitution -interface: for `z` in the open first quadrant, `w = z²` lies in the open upper -half-plane and `z` is a right-half-plane square root of `w`. -/ -theorem hermiteBiehlerStableToHurwitzOddEvenFirstQuadrant_of_upperHalfSubstitution - (h : HermiteBiehlerStableToHurwitzOddEvenUpperHalfSubstitutionStatement) : - HermiteBiehlerStableToHurwitzOddEvenFirstQuadrantStatement := - fun p q h_p h_q h_stable z hzre hzim => by - rw [eval_complexify_oddEvenPolynomial] - have h_w : 0 < (z ^ 2).im := by - rw [pow_two, Complex.mul_im] - positivity - simp [*] - -/-- Checked reduction of the forward Hermite--Biehler/Hurwitz odd/even bridge to -its first-quadrant conformal-substitution core. - -`HermiteBiehlerStableToHurwitzOddEvenStatement` follows from -`HermiteBiehlerStableToHurwitzOddEvenFirstQuadrantStatement`: the real-axis case -`Im z = 0` is handled by positivity of the nonnegative-coefficient polynomial -`q(x²) + x p(x²)`, and the lower half-plane case `Im z < 0` is reduced to the -first quadrant by complex conjugation. -/ -theorem hermiteBiehlerStableToHurwitzOddEven_of_firstQuadrant - (h : HermiteBiehlerStableToHurwitzOddEvenFirstQuadrantStatement) : - HermiteBiehlerStableToHurwitzOddEvenStatement := by - intro p q h_p h_q h_stable z hzre - -- The odd/even polynomial is nonzero, otherwise the stability hypothesis fails. - have h_f_ne : oddEvenPolynomial p q ≠ 0 := by - intro h₀ - rw [oddEvenPolynomial_eq_zero_iff] at h₀ - obtain ⟨hp₀, hq₀⟩ := h₀ - have h_I := h_stable Complex.I (by simp) - simp_all - rcases lt_trichotomy z.im 0 with h_im | h_im | h_im - · -- Lower half-plane: reduce to the first quadrant by conjugation. - have h_conj := eval_complexify_conj (oddEvenPolynomial p q) z - have h_re : 0 < (starRingEnd ℂ z).re := by simp [*] - have h_ci : 0 < (starRingEnd ℂ z).im := by simp [*] - have h_ne : (complexify (oddEvenPolynomial p q)).eval (starRingEnd ℂ z) ≠ 0 := - h h_p h_q h_stable (starRingEnd ℂ z) h_re h_ci - intro h₀ - apply h_ne - rw [h_conj, h₀, map_zero] - · -- Real axis: positivity of the nonnegative-coefficient polynomial. - have h_z : z = ((z.re : ℝ) : ℂ) := by apply Complex.ext <;> simp [h_im] - rw [h_z, eval_complexify_ofReal] - have h_pos : 0 < (oddEvenPolynomial p q).eval z.re := - eval_pos_of_hasNonnegCoeffs (hasNonnegCoeffs_oddEvenPolynomial h_p h_q) h_f_ne hzre - simpa using h_pos.ne' - · -- First quadrant: the interface applies directly. - exact h h_p h_q h_stable z hzre h_im - -/-- Composite reduction: the forward Hermite--Biehler/Hurwitz odd/even bridge -follows from the upper-half-plane substitution interface. -/ -theorem hermiteBiehlerStableToHurwitzOddEven_of_upperHalfSubstitution - (h : HermiteBiehlerStableToHurwitzOddEvenUpperHalfSubstitutionStatement) : - HermiteBiehlerStableToHurwitzOddEvenStatement := - hermiteBiehlerStableToHurwitzOddEven_of_firstQuadrant - (hermiteBiehlerStableToHurwitzOddEvenFirstQuadrant_of_upperHalfSubstitution h) - -theorem hermiteBiehlerStableToHurwitzOddEven_upperHalfSubstitution : - HermiteBiehlerStableToHurwitzOddEvenUpperHalfSubstitutionStatement := by - intro p q h_p h_q h_stable w z hwim hzw hzre +odd/even theorem: for any upper-half-plane point `w` with a right-half-plane +square root `z`, the Hurwitz combination `q(w) + z·p(w)` is nonzero. + +This is the analytic conformal-substitution core: the quadratic map `z ↦ z²` +sends the open first quadrant onto the open upper half-plane. -/ +theorem hermiteBiehlerStableToHurwitzOddEven_upperHalfSubstitution ⦃p q : ℝ[X]⦄ + (h_p : HasNonnegCoeffs p) (h_q : HasNonnegCoeffs q) + (h_stable : IsUpperHalfPlaneStable (hermiteBiehlerPolynomial q p)) + ⦃w z : ℂ⦄ (hwim : 0 < w.im) (hzw : z ^ 2 = w) (hzre : 0 < z.re) : + (complexify q).eval w + z * (complexify p).eval w ≠ 0 := by have h_zim : 0 < z.im := by have h_we : w.im = 2 * z.re * z.im := by rw [← hzw, pow_two, Complex.mul_im]; ring simp_all @@ -172,11 +79,60 @@ theorem hermiteBiehlerStableToHurwitzOddEven_upperHalfSubstitution : rw [complexify, eq_C_of_natDegree_eq_zero h_p_deg₀]; simp simp_all +/-- First-quadrant form of the forward Hermite--Biehler/Hurwitz conformal +substitution: `q(x²) + x p(x²)` has no roots in the open first quadrant +`{Re > 0, Im > 0}`. For `z` in the open first quadrant, `w = z²` lies in the +open upper half-plane and `z` is a right-half-plane square root of `w`. -/ +theorem hermiteBiehlerStableToHurwitzOddEven_firstQuadrant ⦃p q : ℝ[X]⦄ + (h_p : HasNonnegCoeffs p) (h_q : HasNonnegCoeffs q) + (h_stable : IsUpperHalfPlaneStable (hermiteBiehlerPolynomial q p)) + (z : ℂ) (hzre : 0 < z.re) (hzim : 0 < z.im) : + (complexify (oddEvenPolynomial p q)).eval z ≠ 0 := by + have h := hermiteBiehlerStableToHurwitzOddEven_upperHalfSubstitution h_p h_q h_stable + rw [eval_complexify_oddEvenPolynomial] + have h_w : 0 < (z ^ 2).im := by + rw [pow_two, Complex.mul_im] + positivity + simp [*] + +/-- Forward Hermite--Biehler/Hurwitz odd/even theorem: if `q + i p` is +upper-half-plane stable and `p`, `q` have nonnegative coefficients, then +`q(x²) + x p(x²)` is right-half-plane stable. + +The first quadrant is `hermiteBiehlerStableToHurwitzOddEven_firstQuadrant`; the +real-axis case `Im z = 0` is handled by positivity of the nonnegative-coefficient +polynomial, and the lower half-plane case `Im z < 0` is reduced to the first +quadrant by complex conjugation. -/ theorem hermiteBiehlerStableToHurwitzOddEven {p q : ℝ[X]} - (hp : HasNonnegCoeffs p) (hq : HasNonnegCoeffs q) - (h : IsUpperHalfPlaneStable (hermiteBiehlerPolynomial q p)) : - IsRightHalfPlaneStable (complexify (oddEvenPolynomial p q)) := - hermiteBiehlerStableToHurwitzOddEven_of_upperHalfSubstitution - hermiteBiehlerStableToHurwitzOddEven_upperHalfSubstitution hp hq h + (h_p : HasNonnegCoeffs p) (h_q : HasNonnegCoeffs q) + (h_stable : IsUpperHalfPlaneStable (hermiteBiehlerPolynomial q p)) : + IsRightHalfPlaneStable (complexify (oddEvenPolynomial p q)) := by + intro z hzre + -- The odd/even polynomial is nonzero, otherwise the stability hypothesis fails. + have h_f_ne : oddEvenPolynomial p q ≠ 0 := by + intro h₀ + rw [oddEvenPolynomial_eq_zero_iff] at h₀ + obtain ⟨hp₀, hq₀⟩ := h₀ + have h_I := h_stable Complex.I (by simp) + simp_all + rcases lt_trichotomy z.im 0 with h_im | h_im | h_im + · -- Lower half-plane: reduce to the first quadrant by conjugation. + have h_conj := eval_complexify_conj (oddEvenPolynomial p q) z + have h_re : 0 < (starRingEnd ℂ z).re := by simp [*] + have h_ci : 0 < (starRingEnd ℂ z).im := by simp [*] + have h_ne : (complexify (oddEvenPolynomial p q)).eval (starRingEnd ℂ z) ≠ 0 := + hermiteBiehlerStableToHurwitzOddEven_firstQuadrant h_p h_q h_stable + (starRingEnd ℂ z) h_re h_ci + intro h₀ + apply h_ne + rw [h_conj, h₀, map_zero] + · -- Real axis: positivity of the nonnegative-coefficient polynomial. + have h_z : z = ((z.re : ℝ) : ℂ) := by apply Complex.ext <;> simp [h_im] + rw [h_z, eval_complexify_ofReal] + have h_pos : 0 < (oddEvenPolynomial p q).eval z.re := + eval_pos_of_hasNonnegCoeffs (hasNonnegCoeffs_oddEvenPolynomial h_p h_q) h_f_ne hzre + simpa using h_pos.ne' + · -- First quadrant: the interface applies directly. + exact hermiteBiehlerStableToHurwitzOddEven_firstQuadrant h_p h_q h_stable z hzre h_im end RealRooted diff --git a/RealRooted/HurwitzMatrix.lean b/RealRooted/HurwitzMatrix.lean index 4cd7a4b89..f727c5fb3 100644 --- a/RealRooted/HurwitzMatrix.lean +++ b/RealRooted/HurwitzMatrix.lean @@ -10,9 +10,10 @@ namespace RealRooted /-! # Hurwitz matrix criterion interface -This file records checked interface lemmas for the row-oriented Hurwitz matrix -used by the Lace and Veronese developments. The classical Hurwitz criterion -does not hold for this orientation; both proposed directions are refuted below. +This file records checked lemmas for the row-oriented Hurwitz matrix used by +the Lace and Veronese developments. The classical Hurwitz criterion does not +hold for this orientation, and neither does closure of total nonnegativity +under entrywise products; both are refuted below. -/ @[simp] theorem hurwitz_coeff_even_row (p : ℝ[X]) (i j : ℕ) : @@ -96,9 +97,9 @@ theorem hurwitz_isPolyaFreqSeq_even {c : ℕ → ℝ} simpa [IsPolyaFreqSeq, ← hurwitz_submatrix_odd_eq_toeplitz] using hc.submatrix (strictMono_nat_of_lt_succ fun _ => by lia) strictMono_id -/- The row-oriented Hurwitz-matrix criterion and converse are retained only as -explicit `Legacy` scaffolding. Counterexamples below show that these are not -valid theorem targets for the current coefficient convention. -/ +/- The row-oriented converse Hurwitz-matrix criterion is retained only beside +its checked counterexample `not_hurwitzMatrixTotallyNonnegativeToStableStatement`. +It is not a valid theorem for the current coefficient convention. -/ /-- Legacy row-oriented converse Hurwitz-matrix criterion. The nonzero hypothesis rules out the zero-polynomial typo, but the statement remains false @@ -107,17 +108,6 @@ for the current row convention; see abbrev LegacyHurwitzMatrixTotallyNonnegativeToStableStatement : Prop := ∀ ⦃p : ℝ[X]⦄, p ≠ 0 → (hurwitz p.coeff).IsTotallyNonneg → IsHurwitzStable p -/-- The legacy converse Hurwitz-matrix criterion gives the converse odd/even -Lace bridge by the explicit Hurwitz/Lace matrix identity. -/ -theorem fullyInterlacingPairToHurwitzOddEvenStable_of_matrixTNN - (hMatrixToStable : LegacyHurwitzMatrixTotallyNonnegativeToStableStatement) : - LegacyFullyInterlacingPairToHurwitzOddEvenStableStatement := - fun {p q} hpq0 hfull => - hMatrixToStable - (oddEvenPolynomial_ne_zero_iff.mpr hpq0) - ((hurwitzMatrixTotallyNonnegative_oddEvenPolynomial_iff_fullyInterlacingPair p q).2 - hfull) - /-- Entrywise product identity for Hurwitz matrices. The Hurwitz matrix of a coefficientwise product of sequences agrees, entrywise, with the product of the two Hurwitz matrices. -/ @@ -134,27 +124,10 @@ theorem hurwitz_mul_entrywise_matrix (a b : ℕ → ℝ) : ext i j simpa using hurwitz_mul_entrywise a b i j -/-- False proposed extension of a finite nonsingular result proved by -Garloff--Wagner, *Hadamard products of stable polynomials are stable*, J. Math. -Anal. Appl. 202 (1996), 797--809, Theorem 13. - -The cited source proves Hadamard stability and discusses closure for finite -nonsingular Hurwitz matrices. It does not justify closure for arbitrary -infinite, possibly singular matrices in the row-oriented convention below. -The unrestricted statement is refuted by -`not_hurwitzMatrixSchurProductTNStatement`, whose `3 x 3` minor is `-4`. -It must not be used as an available theorem backend. -/ -abbrev HurwitzMatrixSchurProductTNStatement : Prop := - ∀ {a b : ℕ → ℝ}, - (hurwitz a).IsTotallyNonneg → - (hurwitz b).IsTotallyNonneg → - (Matrix.of fun i j => hurwitz a i j * hurwitz b i j).IsTotallyNonneg - -/-! ### Low-order cases of the Schur-product core -/ +/-! ### Entrywise products of Hurwitz matrices: low-order minors -/ /-- Every entry of the entrywise product of two totally nonnegative Hurwitz -matrices is nonnegative. This is the `1 × 1` minor case of -`HurwitzMatrixSchurProductTNStatement`. -/ +matrices is nonnegative. -/ theorem hurwitz_schurProduct_entry_nonneg {a b : ℕ → ℝ} (ha : (hurwitz a).IsTotallyNonneg) (hb : (hurwitz b).IsTotallyNonneg) (i j : ℕ) : @@ -217,44 +190,9 @@ theorem hurwitz_schurProduct_det_fin_three_nonneg_of_band_fail {a b : ℕ → 0 ≤ ((Matrix.of fun i j => hurwitz a i j * hurwitz b i j).submatrix rows cols).det := by rw [hurwitz_schurProduct_det_fin_three_of_band_fail hrows hcols l hl] -/-- In-band `3 × 3` core of the Hurwitz Schur-product theorem. - -Together with `hurwitz_schurProduct_det_fin_three_nonneg_of_band_fail`, this -is equivalent to the full `3 × 3` case. The condition -`2 * cols l ≤ rows l` says that every selected row/column pair lies in the -nonzero staircase of a Hurwitz matrix. -/ -def HurwitzMatrixSchurProductDetFinThreeInBandStatement : Prop := - ∀ {a b : ℕ → ℝ}, - (hurwitz a).IsTotallyNonneg → - (hurwitz b).IsTotallyNonneg → - ∀ {rows cols : Fin 3 → ℕ}, - StrictMono rows → - StrictMono cols → - (∀ l : Fin 3, 2 * cols l ≤ rows l) → - 0 ≤ ((Matrix.of fun i j => hurwitz a i j * hurwitz b i j).submatrix rows cols).det - -/-- Full `3 × 3` Hurwitz Schur-product minor from the in-band core. - -The out-of-band case is already structural: if some `rows l < 2 * cols l`, -then the determinant is zero by `hurwitz_schurProduct_det_fin_three_of_band_fail`. --/ -theorem hurwitz_schurProduct_det_fin_three - (hInBand : HurwitzMatrixSchurProductDetFinThreeInBandStatement) - {a b : ℕ → ℝ} - (ha : (hurwitz a).IsTotallyNonneg) (hb : (hurwitz b).IsTotallyNonneg) - {rows cols : Fin 3 → ℕ} (hrows : StrictMono rows) (hcols : StrictMono cols) : - 0 ≤ ((Matrix.of fun i j => hurwitz a i j * hurwitz b i j).submatrix rows cols).det := by - by_cases hfail : ∃ l : Fin 3, rows l < 2 * cols l - · rcases hfail with ⟨l, hl⟩ - exact hurwitz_schurProduct_det_fin_three_nonneg_of_band_fail hrows hcols l hl - · have hband : ∀ l : Fin 3, 2 * cols l ≤ rows l := - fun l => not_lt.mp (fun hl => hfail ⟨l, hl⟩) - exact hInBand ha hb hrows hcols hband - /-- Every minor of size at most two of the entrywise product of two totally -nonnegative Hurwitz matrices is nonnegative. This packages the complete -low-order part of `HurwitzMatrixSchurProductTNStatement`; the first remaining -case is the genuinely Hurwitz-specific `3 × 3` minor. -/ +nonnegative Hurwitz matrices is nonnegative. This fails already for `3 × 3` +minors; see `not_hurwitz_schurProduct_det_fin_three_nonneg`. -/ theorem hurwitz_schurProduct_det_of_card_le_two {a b : ℕ → ℝ} (ha : (hurwitz a).IsTotallyNonneg) (hb : (hurwitz b).IsTotallyNonneg) {n : ℕ} {rows cols : Fin n → ℕ} (hrows : StrictMono rows) (hcols : StrictMono cols) @@ -262,22 +200,6 @@ theorem hurwitz_schurProduct_det_of_card_le_two {a b : ℕ → ℝ} 0 ≤ ((Matrix.of fun i j => hurwitz a i j * hurwitz b i j).submatrix rows cols).det := ha.hadamard_det_of_card_le_two hb hrows hcols hn -/-- Every minor of size at most three of the entrywise product of two totally -nonnegative Hurwitz matrices is nonnegative, assuming the in-band `3 × 3` -Hurwitz core. -/ -theorem hurwitz_schurProduct_det_of_card_le_three - (hInBand : HurwitzMatrixSchurProductDetFinThreeInBandStatement) - {a b : ℕ → ℝ} - (ha : (hurwitz a).IsTotallyNonneg) (hb : (hurwitz b).IsTotallyNonneg) - {n : ℕ} {rows cols : Fin n → ℕ} (hrows : StrictMono rows) (hcols : StrictMono cols) - (hn : n ≤ 3) : - 0 ≤ ((Matrix.of fun i j => hurwitz a i j * hurwitz b i j).submatrix rows cols).det := by - by_cases hn2 : n ≤ 2 - · exact hurwitz_schurProduct_det_of_card_le_two ha hb hrows hcols hn2 - · have hn3 : n = 3 := by lia - subst n - exact hurwitz_schurProduct_det_fin_three hInBand ha hb hrows hcols - /-- In-band entry formula: on the nonzero staircase `2 * j ≤ i`, every Hurwitz matrix entry is a single coefficient. -/ theorem hurwitz_apply_of_band (c : ℕ → ℝ) {i j : ℕ} (h : 2 * j ≤ i) : @@ -345,111 +267,12 @@ theorem hurwitz_schurProduct_det_fin_three_of_row1_below {a b : ℕ → ℝ} hurwitz_apply_eq_zero_of_lt a (by lia : rows 0 < 2 * cols 2)] linarith [mul_nonneg hM22 h2] -/-- Refined in-band `3 × 3` Hurwitz Schur-product core after the two triangular -reductions have been removed. The remaining case has -`2 * cols 1 ≤ rows 0` and `2 * cols 2 ≤ rows 1`, so the top `2 × 3` block lies -on the nonzero staircase. -/ -def HurwitzMatrixSchurProductDetFinThreeCoreStatement : Prop := - ∀ {a b : ℕ → ℝ}, - (hurwitz a).IsTotallyNonneg → - (hurwitz b).IsTotallyNonneg → - ∀ {rows cols : Fin 3 → ℕ}, - StrictMono rows → - StrictMono cols → - (∀ l : Fin 3, 2 * cols l ≤ rows l) → - 2 * cols 1 ≤ rows 0 → - 2 * cols 2 ≤ rows 1 → - 0 ≤ ((Matrix.of fun i j => hurwitz a i j * hurwitz b i j).submatrix rows cols).det - -/-- The original in-band `3 × 3` core implies the refined triangular-free core. -/ -theorem hurwitzMatrixSchurProductDetFinThreeCore_of_inBand - (hInBand : HurwitzMatrixSchurProductDetFinThreeInBandStatement) : - HurwitzMatrixSchurProductDetFinThreeCoreStatement := - fun {_a _b} ha hb {_rows} {_cols} hrows hcols hband _h01 _h12 => - hInBand ha hb hrows hcols hband - -/-- The refined triangular-free core implies the original in-band `3 × 3` core. -/ -theorem hurwitzMatrixSchurProductDetFinThreeInBand_of_core - (hcore : HurwitzMatrixSchurProductDetFinThreeCoreStatement) : - HurwitzMatrixSchurProductDetFinThreeInBandStatement := by - intro a b ha hb rows cols hrows hcols hband - by_cases h0 : rows 0 < 2 * cols 1 - · exact hurwitz_schurProduct_det_fin_three_of_row0_below ha hb hrows hcols h0 - · by_cases h1 : rows 1 < 2 * cols 2 - · exact hurwitz_schurProduct_det_fin_three_of_row1_below ha hb hrows hcols h1 - · exact hcore ha hb hrows hcols hband (by lia) (by lia) - -/-- The in-band `3 × 3` Hurwitz Schur-product core is equivalent to its -triangular-free refinement. -/ -theorem hurwitzMatrixSchurProductDetFinThreeInBand_iff_core : - HurwitzMatrixSchurProductDetFinThreeInBandStatement ↔ - HurwitzMatrixSchurProductDetFinThreeCoreStatement := - ⟨hurwitzMatrixSchurProductDetFinThreeCore_of_inBand, - hurwitzMatrixSchurProductDetFinThreeInBand_of_core⟩ - -/-- Low-order, size-`≤ 3`, form of the Hurwitz matrix Schur-product core. -/ -def HurwitzMatrixSchurProductDetLeThreeStatement : Prop := - ∀ {a b : ℕ → ℝ}, - (hurwitz a).IsTotallyNonneg → - (hurwitz b).IsTotallyNonneg → - ∀ {n : ℕ} {rows cols : Fin n → ℕ}, - StrictMono rows → - StrictMono cols → - n ≤ 3 → - 0 ≤ ((Matrix.of fun i j => hurwitz a i j * hurwitz b i j).submatrix rows cols).det - -/-- The isolated in-band `3 × 3` core implies the low-order, size-`≤ 3`, -Hurwitz matrix Schur-product statement. -/ -theorem hurwitzMatrixSchurProductDetLeThree_of_inBand - (hInBand : HurwitzMatrixSchurProductDetFinThreeInBandStatement) : - HurwitzMatrixSchurProductDetLeThreeStatement := - @hurwitz_schurProduct_det_of_card_le_three hInBand - -/-- The refined triangular-free `3 × 3` core implies the low-order, size-`≤ 3`, -Hurwitz matrix Schur-product statement. -/ -theorem hurwitzMatrixSchurProductDetLeThree_of_core - (hcore : HurwitzMatrixSchurProductDetFinThreeCoreStatement) : - HurwitzMatrixSchurProductDetLeThreeStatement := - hurwitzMatrixSchurProductDetLeThree_of_inBand - (hurwitzMatrixSchurProductDetFinThreeInBand_of_core hcore) - -theorem hurwitzMatrixSchurProductDetLeThree_of_schurProductTN - (hSchur : HurwitzMatrixSchurProductTNStatement) : - HurwitzMatrixSchurProductDetLeThreeStatement := - fun {_a _b} ha hb {_n} {_rows} {_cols} hrows hcols _hn => - hSchur ha hb hrows hcols - -/-- The full Hurwitz matrix Schur-product statement implies the isolated -in-band `3 × 3` core. -/ -theorem hurwitzMatrixSchurProductDetFinThreeInBand_of_schurProductTN - (hSchur : HurwitzMatrixSchurProductTNStatement) : - HurwitzMatrixSchurProductDetFinThreeInBandStatement := - fun {_a _b} ha hb {_rows} {_cols} hrows hcols _hband => - hSchur ha hb hrows hcols - -/-- The low-order, size-`≤ 3`, Hurwitz matrix Schur-product statement implies -the isolated in-band `3 × 3` core. -/ -theorem hurwitzMatrixSchurProductDetFinThreeInBand_of_leThree - (hLeThree : HurwitzMatrixSchurProductDetLeThreeStatement) : - HurwitzMatrixSchurProductDetFinThreeInBandStatement := - fun {_a _b} ha hb {_rows} {_cols} hrows hcols _hband => - hLeThree ha hb hrows hcols (by norm_num) - -/-- The low-order, size-`≤ 3`, Hurwitz Schur-product statement is equivalent -to the isolated in-band `3 × 3` core. -/ -theorem hurwitzMatrixSchurProductDetLeThree_iff_inBand : - HurwitzMatrixSchurProductDetLeThreeStatement ↔ - HurwitzMatrixSchurProductDetFinThreeInBandStatement := - ⟨hurwitzMatrixSchurProductDetFinThreeInBand_of_leThree, - hurwitzMatrixSchurProductDetLeThree_of_inBand⟩ - -/-! ### Reusable reductions for the triangular-free `3 × 3` core -/ - -/-- Arithmetic band bookkeeping for the triangular-free `3 × 3` core. Under -the two triangular-free hypotheses `2 * cols 1 ≤ rows 0` and -`2 * cols 2 ≤ rows 1`, monotonicity of the selected rows and columns forces -every selected entry except possibly the top-right corner `(0, 2)` onto the -nonzero staircase. -/ +/-! ### Band bookkeeping and the column-shift structure -/ + +/-- Arithmetic band bookkeeping for a `3 × 3` window. Under the two hypotheses +`2 * cols 1 ≤ rows 0` and `2 * cols 2 ≤ rows 1`, monotonicity of the selected +rows and columns forces every selected entry except possibly the top-right +corner `(0, 2)` onto the nonzero staircase. -/ theorem hurwitz_schurProduct_core_inband_entries {rows cols : Fin 3 → ℕ} (hrows : StrictMono rows) (hcols : StrictMono cols) (h01 : 2 * cols 1 ≤ rows 0) (h12 : 2 * cols 2 ≤ rows 1) : @@ -494,456 +317,9 @@ theorem hurwitz_col_shift_add (c : ℕ → ℝ) (j : ℕ) : rw [hji, hurwitz_col_shift c (by lia)] grind -/-- Fully in-band subcase of the triangular-free `3 × 3` core: the top-right -corner `(0, 2)` also lies on the nonzero staircase. -/ -def HurwitzMatrixSchurProductDetFinThreeCoreFullBandStatement : Prop := - ∀ {a b : ℕ → ℝ}, - (hurwitz a).IsTotallyNonneg → - (hurwitz b).IsTotallyNonneg → - ∀ {rows cols : Fin 3 → ℕ}, - StrictMono rows → - StrictMono cols → - (∀ l : Fin 3, 2 * cols l ≤ rows l) → - 2 * cols 1 ≤ rows 0 → - 2 * cols 2 ≤ rows 1 → - 2 * cols 2 ≤ rows 0 → - 0 ≤ - ((Matrix.of fun i j => hurwitz a i j * hurwitz b i j).submatrix rows cols).det - -/-- The full-band `3 × 3` Hadamard determinant with the top-right corner -contribution deleted. This is the remaining determinant after expanding along -the top row and setting the `(0, 2)` entry to zero. -/ -def hurwitzSchurProductFullBandCornerZeroedDet - (a b : ℕ → ℝ) (rows cols : Fin 3 → ℕ) : ℝ := - (hurwitz a (rows 0) (cols 0) * hurwitz b (rows 0) (cols 0)) * - ((hurwitz a (rows 1) (cols 1) * hurwitz b (rows 1) (cols 1)) * - (hurwitz a (rows 2) (cols 2) * hurwitz b (rows 2) (cols 2)) - - (hurwitz a (rows 1) (cols 2) * hurwitz b (rows 1) (cols 2)) * - (hurwitz a (rows 2) (cols 1) * hurwitz b (rows 2) (cols 1))) - - (hurwitz a (rows 0) (cols 1) * hurwitz b (rows 0) (cols 1)) * - ((hurwitz a (rows 1) (cols 0) * hurwitz b (rows 1) (cols 0)) * - (hurwitz a (rows 2) (cols 2) * hurwitz b (rows 2) (cols 2)) - - (hurwitz a (rows 1) (cols 2) * hurwitz b (rows 1) (cols 2)) * - (hurwitz a (rows 2) (cols 0) * hurwitz b (rows 2) (cols 0))) - -/-- Corner-zeroed subtarget for the full-band `3 × 3` Hurwitz Schur-product -core. The full determinant follows from this subtarget by adding the -top-right corner contribution, which is a nonnegative `2 × 2` Hadamard minor. -/ -def HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedStatement : Prop := - ∀ {a b : ℕ → ℝ}, - (hurwitz a).IsTotallyNonneg → - (hurwitz b).IsTotallyNonneg → - ∀ {rows cols : Fin 3 → ℕ}, - StrictMono rows → - StrictMono cols → - (∀ l : Fin 3, 2 * cols l ≤ rows l) → - 2 * cols 1 ≤ rows 0 → - 2 * cols 2 ≤ rows 1 → - 2 * cols 2 ≤ rows 0 → - 0 ≤ hurwitzSchurProductFullBandCornerZeroedDet a b rows cols - -/-- Single-matrix full-band corner-zeroed determinant subtarget. - -This is the sharper one-matrix inequality isolated by an earlier Aristotle -corner-zeroed run. It is retained as a named historical branch for existing -reductions, but it is too strong as a proof route: see -`RealRooted.Challenges.HurwitzCornerZeroedCounterexample` for checked -arithmetic showing a candidate window where the full determinant is positive -while the corner-zeroed expression is negative. The two-matrix issue #34 -target is not refuted by that arithmetic witness. -/ -def HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleStatement : Prop := - ∀ {a : ℕ → ℝ}, - (hurwitz a).IsTotallyNonneg → - ∀ {rows cols : Fin 3 → ℕ}, - StrictMono rows → - StrictMono cols → - (∀ l : Fin 3, 2 * cols l ≤ rows l) → - 2 * cols 1 ≤ rows 0 → - 2 * cols 2 ≤ rows 1 → - 2 * cols 2 ≤ rows 0 → - 0 ≤ hurwitz a (rows 0) (cols 0) * - (hurwitz a (rows 1) (cols 1) * hurwitz a (rows 2) (cols 2) - - hurwitz a (rows 1) (cols 2) * hurwitz a (rows 2) (cols 1)) - - hurwitz a (rows 0) (cols 1) * - (hurwitz a (rows 1) (cols 0) * hurwitz a (rows 2) (cols 2) - - hurwitz a (rows 1) (cols 2) * hurwitz a (rows 2) (cols 0)) - -/-- Column-normalized version of the single-matrix full-band corner-zeroed -determinant subtarget. - -The first selected column is assumed to be `0`. The general single-matrix -subtarget reduces to this normalized form by shifting all selected columns by -`cols 0` and all selected rows by `2 * cols 0`. -/ -def HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleColZeroStatement : - Prop := - ∀ {a : ℕ → ℝ}, - (hurwitz a).IsTotallyNonneg → - ∀ {rows cols : Fin 3 → ℕ}, - StrictMono rows → - StrictMono cols → - (∀ l : Fin 3, 2 * cols l ≤ rows l) → - 2 * cols 1 ≤ rows 0 → - 2 * cols 2 ≤ rows 1 → - 2 * cols 2 ≤ rows 0 → - cols 0 = 0 → - 0 ≤ hurwitz a (rows 0) (cols 0) * - (hurwitz a (rows 1) (cols 1) * hurwitz a (rows 2) (cols 2) - - hurwitz a (rows 1) (cols 2) * hurwitz a (rows 2) (cols 1)) - - hurwitz a (rows 0) (cols 1) * - (hurwitz a (rows 1) (cols 0) * hurwitz a (rows 2) (cols 2) - - hurwitz a (rows 1) (cols 2) * hurwitz a (rows 2) (cols 0)) +/-! ### The corner-zero `3 × 3` case -/ -/-- First-column form of the corner-zeroed single-matrix determinant. -/ -def hurwitzFullBandCornerZeroedSingleFirstColDet - (a : ℕ → ℝ) (row0 row1 row2 col1 col2 : ℕ) : ℝ := - hurwitz a row0 0 * - (hurwitz a (row1 - 2 * col1) 0 * - hurwitz a (row2 - 2 * col2) 0 - - hurwitz a (row1 - 2 * col2) 0 * - hurwitz a (row2 - 2 * col1) 0) - - hurwitz a (row0 - 2 * col1) 0 * - (hurwitz a row1 0 * hurwitz a (row2 - 2 * col2) 0 - - hurwitz a (row1 - 2 * col2) 0 * hurwitz a row2 0) - -/-- The lower-left `2 × 2` minor appearing in the first-column determinant -decomposition. -/ -def hurwitzFullBandCornerZeroedSingleFirstColLowerMinor - (a : ℕ → ℝ) (row1 row2 col1 : ℕ) : ℝ := - hurwitz a row1 0 * hurwitz a (row2 - 2 * col1) 0 - - hurwitz a (row1 - 2 * col1) 0 * hurwitz a row2 0 - -/-- First-column normal form of the single-matrix full-band corner-zeroed -determinant subtarget. - -After the first selected column is normalized to `0`, every remaining selected -column can be shifted back to column `0` by moving rows up by twice that column -index. This is the remaining #34 leaf in pure first-column Hurwitz form. -/ -def HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleFirstColStatement : - Prop := - ∀ {a : ℕ → ℝ}, - (hurwitz a).IsTotallyNonneg → - ∀ {row0 row1 row2 col1 col2 : ℕ}, - row0 < row1 → - row1 < row2 → - 0 < col1 → - col1 < col2 → - 2 * col2 ≤ row0 → - 0 ≤ hurwitzFullBandCornerZeroedSingleFirstColDet a row0 row1 row2 col1 col2 - -/-- Strict-remainder branch of the first-column target. - -The full `3 × 3` determinant supplies the first-column corner-zeroed -determinant plus a product of the shifted top-right entry and the lower-left -`2 × 2` minor. The zero cases of that product are automatic, so the remaining -work is the branch where both factors are strictly positive. -/ -def HurwitzMatrixSchurProductDetFirstColPositiveRemainderStatement : Prop := - ∀ {a : ℕ → ℝ}, - (hurwitz a).IsTotallyNonneg → - ∀ {row0 row1 row2 col1 col2 : ℕ}, - row0 < row1 → - row1 < row2 → - 0 < col1 → - col1 < col2 → - 2 * col2 ≤ row0 → - 0 < hurwitz a (row0 - 2 * col2) 0 → - 0 < hurwitzFullBandCornerZeroedSingleFirstColLowerMinor a row1 row2 col1 → - 0 ≤ hurwitzFullBandCornerZeroedSingleFirstColDet a row0 row1 row2 col1 col2 - -/-- The strict-remainder branch implies the first-column normal form. -/ -theorem - hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleFirstCol_of_positiveRemainder - (hPos : - HurwitzMatrixSchurProductDetFirstColPositiveRemainderStatement) : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleFirstColStatement := by - intro a ha row0 row1 row2 col1 col2 hr01 hr12 hc0 hc12 h02 - let rows : Fin 3 → ℕ := ![row0, row1, row2] - let cols : Fin 3 → ℕ := ![0, col1, col2] - have hrows : StrictMono rows := by - intro i j hij - fin_cases i <;> fin_cases j <;> simp [rows] at hij ⊢ <;> lia - have hcols : StrictMono cols := by - intro i j hij - fin_cases i <;> fin_cases j <;> simp [cols] at hij ⊢ <;> lia - have hrow0_le : ∀ i : Fin 3, row0 ≤ rows i := by - intro i - fin_cases i - · rfl - · exact le_of_lt hr01 - · exact (le_of_lt hr01).trans (le_of_lt hr12) - have hcol_le : ∀ j : Fin 3, cols j ≤ col2 := by - intro j - fin_cases j - · exact Nat.zero_le col2 - · exact le_of_lt hc12 - · rfl - have hall : ∀ i j : Fin 3, 2 * cols j ≤ rows i := by grind - have hshift (i j : Fin 3) : - hurwitz a (rows i) (cols j) = hurwitz a (rows i - 2 * cols j) 0 := by - simpa using - hurwitz_col_shift_add a 0 (cols j) (rows i) (by grind) - have hcorner_nonneg : 0 ≤ hurwitz a (row0 - 2 * col2) 0 := by - have h := ha.nonneg row0 col2 - change 0 ≤ hurwitz a (rows 0) (cols 2) at h - rwa [hshift 0 2] at h - have hminor_nonneg : - 0 ≤ hurwitzFullBandCornerZeroedSingleFirstColLowerMinor a row1 row2 col1 := by - have h := ha (strictMono_pair hr12) (strictMono_pair hc0) - rw [Matrix.det_fin_two] at h - simp only [Matrix.submatrix_apply, Matrix.cons_val_zero, Matrix.cons_val_one] at h - have h10 : hurwitz a row1 col1 = hurwitz a (row1 - 2 * col1) 0 := by - simpa [rows, cols] using hshift 1 1 - have h21 : hurwitz a row2 col1 = hurwitz a (row2 - 2 * col1) 0 := by - simpa [rows, cols] using hshift 2 1 - simpa [hurwitzFullBandCornerZeroedSingleFirstColLowerMinor, h10, h21] using h - have hs01 : hurwitz a row0 col1 = hurwitz a (row0 - 2 * col1) 0 := by - simpa [rows, cols] using hshift 0 1 - have hs02 : hurwitz a row0 col2 = hurwitz a (row0 - 2 * col2) 0 := by - simpa [rows, cols] using hshift 0 2 - have hs11 : hurwitz a row1 col1 = hurwitz a (row1 - 2 * col1) 0 := by - simpa [rows, cols] using hshift 1 1 - have hs12 : hurwitz a row1 col2 = hurwitz a (row1 - 2 * col2) 0 := by - simpa [rows, cols] using hshift 1 2 - have hs21 : hurwitz a row2 col1 = hurwitz a (row2 - 2 * col1) 0 := by - simpa [rows, cols] using hshift 2 1 - have hs22 : hurwitz a row2 col2 = hurwitz a (row2 - 2 * col2) 0 := by - simpa [rows, cols] using hshift 2 2 - have hdet_full : - 0 ≤ hurwitzFullBandCornerZeroedSingleFirstColDet a row0 row1 row2 col1 col2 + - hurwitz a (row0 - 2 * col2) 0 * - hurwitzFullBandCornerZeroedSingleFirstColLowerMinor a row1 row2 col1 := by - have hdet := ha hrows hcols - rw [Matrix.det_fin_three] at hdet - simp only [Matrix.submatrix_apply] at hdet - change - 0 ≤ - hurwitz a row0 0 * hurwitz a row1 col1 * hurwitz a row2 col2 - - hurwitz a row0 0 * hurwitz a row1 col2 * hurwitz a row2 col1 - - hurwitz a row0 col1 * hurwitz a row1 0 * hurwitz a row2 col2 + - hurwitz a row0 col1 * hurwitz a row1 col2 * hurwitz a row2 0 + - hurwitz a row0 col2 * hurwitz a row1 0 * hurwitz a row2 col1 - - hurwitz a row0 col2 * hurwitz a row1 col1 * hurwitz a row2 0 at hdet - rw [hs01, hs02, hs11, hs12, hs21, hs22] at hdet - dsimp [hurwitzFullBandCornerZeroedSingleFirstColDet, - hurwitzFullBandCornerZeroedSingleFirstColLowerMinor] - grind - by_cases hcorner : - hurwitz a (row0 - 2 * col2) 0 = 0 - · simp_all - · by_cases hminor : - hurwitzFullBandCornerZeroedSingleFirstColLowerMinor a row1 row2 col1 = 0 - · simp_all - · exact hPos ha hr01 hr12 hc0 hc12 h02 - (lt_of_le_of_ne hcorner_nonneg (Ne.symm hcorner)) - (lt_of_le_of_ne hminor_nonneg (Ne.symm hminor)) - -/-- The general single-matrix corner-zeroed target specializes to the -column-normalized target. -/ -theorem - hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleColZero_of_single - (hSingle : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleStatement) : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleColZeroStatement := - fun {_a} ha {_rows} {_cols} hrows hcols hband h01 h12 h02 _hcol0 => - hSingle ha hrows hcols hband h01 h12 h02 - -/-- The first-column normal form implies the column-normalized single-matrix -corner-zeroed determinant target. -/ -theorem - hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleColZero_of_firstCol - (hFirst : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleFirstColStatement) : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleColZeroStatement := by - intro a ha rows cols hrows hcols _hband _h01 _h12 h02 hcol0 - have hr01 : rows 0 < rows 1 := hrows (by simp) - have hr12 : rows 1 < rows 2 := hrows (by simp) - have hr02le : rows 0 ≤ rows 2 := (le_of_lt hr01).trans (le_of_lt hr12) - have hc01 : cols 0 < cols 1 := hcols (by simp) - have hc12 : cols 1 < cols 2 := hcols (by simp) - have hc01pos : 0 < cols 1 := by simp_all - have hcol_le_two : ∀ j : Fin 3, cols j ≤ cols 2 := by - intro j - fin_cases j - · simp [hcol0] - · grind - · simp - have hrow_ge_zero : ∀ i : Fin 3, rows 0 ≤ rows i := by - intro i - fin_cases i <;> grind - have hall : ∀ i j : Fin 3, 2 * cols j ≤ rows i := by grind - have hentry (i j : Fin 3) : - hurwitz a (rows i) (cols j) = hurwitz a (rows i - 2 * cols j) 0 := by - simpa using - hurwitz_col_shift_add a 0 (cols j) (rows i) (by grind) - have hfirst := hFirst ha hr01 hr12 hc01pos hc12 h02 - rw [hentry 0 0, hentry 1 1, hentry 2 2, hentry 1 2, hentry 2 1, - hentry 0 1, hentry 1 0, hentry 2 0] - simpa [hurwitzFullBandCornerZeroedSingleFirstColDet, hcol0] using hfirst - -/-- The column-normalized single-matrix target specializes to the first-column -normal form. -/ -theorem - hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleFirstCol_of_colZero - (hZero : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleColZeroStatement) : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleFirstColStatement := by - intro a ha row0 row1 row2 col1 col2 hr01 hr12 hc0 hc12 h02 - let rows : Fin 3 → ℕ := ![row0, row1, row2] - let cols : Fin 3 → ℕ := ![0, col1, col2] - have hrows : StrictMono rows := by - intro i j hij - fin_cases i <;> fin_cases j <;> simp [rows] at hij ⊢ <;> lia - have hcols : StrictMono cols := by - intro i j hij - fin_cases i <;> fin_cases j <;> simp [cols] at hij ⊢ <;> lia - have hband : ∀ l : Fin 3, 2 * cols l ≤ rows l := by - intro l - fin_cases l <;> simp [rows, cols] <;> lia - have h01 : 2 * cols 1 ≤ rows 0 := by - simpa [rows, cols] using le_trans (Nat.mul_le_mul_left 2 (le_of_lt hc12)) h02 - have h12 : 2 * cols 2 ≤ rows 1 := by simpa [rows, cols] using le_trans h02 (le_of_lt hr01) - have h02' : 2 * cols 2 ≤ rows 0 := by simpa [rows, cols] using h02 - have hcol0 : cols 0 = 0 := by simp [cols] - have hres := hZero ha hrows hcols hband h01 h12 h02' hcol0 - have hall : ∀ i j : Fin 3, 2 * cols j ≤ rows i := by - intro i j - fin_cases i <;> fin_cases j <;> simp [rows, cols] <;> lia - have hshift (i j : Fin 3) : - hurwitz a (rows i) (cols j) = hurwitz a (rows i - 2 * cols j) 0 := by - simpa only [Nat.zero_add] using - hurwitz_col_shift_add a 0 (cols j) (rows i) (by simpa using hall i j) - have hs01 : hurwitz a row0 col1 = hurwitz a (row0 - 2 * col1) 0 := by - simpa [rows, cols] using hshift 0 1 - have hs11 : hurwitz a row1 col1 = hurwitz a (row1 - 2 * col1) 0 := by - simpa [rows, cols] using hshift 1 1 - have hs21 : hurwitz a row2 col1 = hurwitz a (row2 - 2 * col1) 0 := by - simpa [rows, cols] using hshift 2 1 - have hs12 : hurwitz a row1 col2 = hurwitz a (row1 - 2 * col2) 0 := by - simpa [rows, cols] using hshift 1 2 - have hs22 : hurwitz a row2 col2 = hurwitz a (row2 - 2 * col2) 0 := by - simpa [rows, cols] using hshift 2 2 - simpa [hurwitzFullBandCornerZeroedSingleFirstColDet, rows, cols, - hs01, hs11, hs21, hs12, hs22] using hres - -/-- The general single-matrix target specializes to the first-column normal -form. -/ -theorem - hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleFirstCol_of_single - (hSingle : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleStatement) : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleFirstColStatement := - hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleFirstCol_of_colZero - (hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleColZero_of_single - hSingle) - -/-- The column-normalized single-matrix corner-zeroed target implies the -general single-matrix corner-zeroed target. -/ -theorem hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingle_of_colZero - (hZero : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleColZeroStatement) : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleStatement := by - intro a ha rows cols hrows hcols hband h01 h12 h02 - let d := cols 0 - let rows' : Fin 3 → ℕ := fun i ↦ rows i - 2 * d - let cols' : Fin 3 → ℕ := fun i ↦ cols i - d - have hr01 : rows 0 ≤ rows 1 := hrows.monotone (by simp) - have hr12 : rows 1 ≤ rows 2 := hrows.monotone (by simp) - have hr02 : rows 0 ≤ rows 2 := hrows.monotone (by simp) - have hc0 : ∀ i : Fin 3, d ≤ cols i := by - intro i - have h0i : (0 : Fin 3) ≤ i := by simp - exact hcols.monotone h0i - have hdrow : ∀ i : Fin 3, 2 * d ≤ rows i := by grind - have hrows' : StrictMono rows' := by - intro i j hij - dsimp [rows'] - have hij' := hrows hij - grind - have hcols' : StrictMono cols' := by - intro i j hij - dsimp [cols'] - have hij' := hcols hij - grind - have hband' : ∀ l : Fin 3, 2 * cols' l ≤ rows' l := by grind - have h01' : 2 * cols' 1 ≤ rows' 0 := by grind - have h12' : 2 * cols' 2 ≤ rows' 1 := by grind - have h02' : 2 * cols' 2 ≤ rows' 0 := by grind - have hcol0' : cols' 0 = 0 := by grind - have hall : ∀ i j : Fin 3, 2 * cols j ≤ rows i := by - intro i j - fin_cases i <;> fin_cases j <;> grind - have hentry (i j : Fin 3) : - hurwitz a (rows i) (cols j) = hurwitz a (rows' i) (cols' j) := by - have : cols' j + d = cols j := by grind - have : rows i - 2 * d = rows' i := by grind - have hs := hurwitz_col_shift_add a (cols' j) d (rows i) <| - by simp_all - simp_all - have hnorm := hZero ha hrows' hcols' hband' h01' h12' h02' hcol0' - simp_all - -/-- The full-band `3 × 3` core follows from the corner-zeroed full-band -subtarget. The missing top-right term factors as the `(0, 2)` entry times a -`2 × 2` Hadamard minor on rows `{1, 2}` and columns `{0, 1}`. -/ -theorem hurwitzMatrixSchurProductDetFinThreeCoreFullBand_of_cornerZeroed - (hCZ : HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedStatement) : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandStatement := by - intro a b ha hb rows cols hrows hcols hband h01 h12 h02 - have hcz := hCZ ha hb hrows hcols hband h01 h12 h02 - have hr12 : rows 1 < rows 2 := hrows (by simp) - have hc01 : cols 0 < cols 1 := hcols (by simp) - have hcorner := ha.hadamard_det_fin_two hb - (strictMono_pair hr12) (strictMono_pair hc01) - rw [Matrix.det_fin_two] at hcorner - simp only [Matrix.submatrix_apply, Matrix.of_apply, Matrix.cons_val_zero, - Matrix.cons_val_one] at hcorner - have hentry : - 0 ≤ hurwitz a (rows 0) (cols 2) * hurwitz b (rows 0) (cols 2) := - mul_nonneg (ha.nonneg _ _) (hb.nonneg _ _) - have hcornerTerm : - 0 ≤ - (hurwitz a (rows 0) (cols 2) * hurwitz b (rows 0) (cols 2)) * - ((hurwitz a (rows 1) (cols 0) * hurwitz b (rows 1) (cols 0)) * - (hurwitz a (rows 2) (cols 1) * hurwitz b (rows 2) (cols 1)) - - (hurwitz a (rows 1) (cols 1) * hurwitz b (rows 1) (cols 1)) * - (hurwitz a (rows 2) (cols 0) * hurwitz b (rows 2) (cols 0))) := - mul_nonneg hentry hcorner - rw [Matrix.det_fin_three] - simp only [Matrix.submatrix_apply, Matrix.of_apply, - hurwitzSchurProductFullBandCornerZeroedDet] at hcz ⊢ - grind - -/-- Corner-zero subcase of the triangular-free `3 × 3` core: the top-right -corner `(0, 2)` lies above the staircase, so that entry vanishes. -/ -def HurwitzMatrixSchurProductDetFinThreeCoreCornerZeroStatement : Prop := - ∀ {a b : ℕ → ℝ}, - (hurwitz a).IsTotallyNonneg → - (hurwitz b).IsTotallyNonneg → - ∀ {rows cols : Fin 3 → ℕ}, - StrictMono rows → - StrictMono cols → - (∀ l : Fin 3, 2 * cols l ≤ rows l) → - 2 * cols 1 ≤ rows 0 → - 2 * cols 2 ≤ rows 1 → - rows 0 < 2 * cols 2 → - 0 ≤ - ((Matrix.of fun i j => hurwitz a i j * hurwitz b i j).submatrix rows cols).det - -/-- Reduction of the triangular-free `3 × 3` core (GitHub issue #34) to its -two top-right-corner subcases. Splitting on whether the corner `(0, 2)` is on -the staircase reduces the sharper core to the fully in-band case and the -corner-zero case. -/ -theorem hurwitzMatrixSchurProductDetFinThreeCore_of_fullBand_cornerZero - (hF : HurwitzMatrixSchurProductDetFinThreeCoreFullBandStatement) - (hZ : HurwitzMatrixSchurProductDetFinThreeCoreCornerZeroStatement) : - HurwitzMatrixSchurProductDetFinThreeCoreStatement := by - intro a b ha hb rows cols hrows hcols hband h01 h12 - by_cases hc : 2 * cols 2 ≤ rows 0 - · exact hF ha hb hrows hcols hband h01 h12 hc - · exact hZ ha hb hrows hcols hband h01 h12 (by lia) - -/-! ### The corner-zero subcase -/ - -/-- Pure `3 × 3` algebraic core of the corner-zero case. For two totally +/-- Pure `3 × 3` algebraic form of the corner-zero case. For two totally nonnegative `3 × 3` matrices whose top-right entry vanishes, the Hadamard product has nonnegative determinant. @@ -977,109 +353,16 @@ theorem hadamard_det_fin_three_cornerZero_nonneg mul_nonneg (mul_nonneg ha12 mA02) (mul_nonneg hb00 mB_r12c12), mul_nonneg (mul_nonneg (mul_nonneg ha01 ha12) ha20) detB] -/-- The two-matrix corner-zeroed full-band subtarget follows from the -single-matrix corner-zeroed determinant subtarget for each factor. - -This is the checked part of the Aristotle corner-zeroed reduction: the -one-matrix inequalities supply the `detA` and `detB` inputs to the existing -positive-combination certificate -`hadamard_det_fin_three_cornerZero_nonneg`; the remaining inputs are ordinary -`2 × 2` minors of the two totally nonnegative Hurwitz matrices. -/ -theorem hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroed_of_single - (hSingle : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleStatement) : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedStatement := by - intro a b ha hb rows cols hrows hcols hband h01 h12 h02 - have hr01 : StrictMono ![rows 0, rows 1] := strictMono_pair (hrows (by simp)) - have hr02 : StrictMono ![rows 0, rows 2] := strictMono_pair (hrows (by simp)) - have hr12 : StrictMono ![rows 1, rows 2] := strictMono_pair (hrows (by simp)) - have hc01 : StrictMono ![cols 0, cols 1] := strictMono_pair (hcols (by simp)) - have hc02 : StrictMono ![cols 0, cols 2] := strictMono_pair (hcols (by simp)) - have hc12 : StrictMono ![cols 1, cols 2] := strictMono_pair (hcols (by simp)) - have mA02 := ha hr02 hc01 - rw [Matrix.det_fin_two] at mA02 - simp only [Matrix.submatrix_apply, Matrix.cons_val_zero, Matrix.cons_val_one] at mA02 - have mAc02 := ha hr12 hc02 - rw [Matrix.det_fin_two] at mAc02 - simp only [Matrix.submatrix_apply, Matrix.cons_val_zero, Matrix.cons_val_one] at mAc02 - have mB01 := hb hr01 hc01 - rw [Matrix.det_fin_two] at mB01 - simp only [Matrix.submatrix_apply, Matrix.cons_val_zero, Matrix.cons_val_one] at mB01 - have mBc12 := hb hr12 hc12 - rw [Matrix.det_fin_two] at mBc12 - simp only [Matrix.submatrix_apply, Matrix.cons_val_zero, Matrix.cons_val_one] at mBc12 - have detA := hSingle ha hrows hcols hband h01 h12 h02 - have detB := hSingle hb hrows hcols hband h01 h12 h02 - have hres := hadamard_det_fin_three_cornerZero_nonneg - (hurwitz a (rows 0) (cols 0)) (hurwitz a (rows 0) (cols 1)) - (hurwitz a (rows 1) (cols 0)) (hurwitz a (rows 1) (cols 1)) - (hurwitz a (rows 1) (cols 2)) (hurwitz a (rows 2) (cols 0)) - (hurwitz a (rows 2) (cols 1)) (hurwitz a (rows 2) (cols 2)) - (hurwitz b (rows 0) (cols 0)) (hurwitz b (rows 0) (cols 1)) - (hurwitz b (rows 1) (cols 0)) (hurwitz b (rows 1) (cols 1)) - (hurwitz b (rows 1) (cols 2)) (hurwitz b (rows 2) (cols 0)) - (hurwitz b (rows 2) (cols 1)) (hurwitz b (rows 2) (cols 2)) - (ha.nonneg (rows 0) (cols 1)) (ha.nonneg (rows 1) (cols 2)) - (ha.nonneg (rows 2) (cols 0)) (hb.nonneg (rows 0) (cols 0)) - (hb.nonneg (rows 1) (cols 1)) (hb.nonneg (rows 2) (cols 2)) - mA02 mAc02 mB01 mBc12 detA detB - simp only [hurwitzSchurProductFullBandCornerZeroedDet] - grind - -/-- The single-matrix corner-zeroed determinant subtarget implies the -full-band `3 × 3` Hurwitz Schur-product subcase. -/ -theorem hurwitzMatrixSchurProductDetFinThreeCoreFullBand_of_cornerZeroedSingle - (hSingle : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleStatement) : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandStatement := - hurwitzMatrixSchurProductDetFinThreeCoreFullBand_of_cornerZeroed - (hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroed_of_single hSingle) - -/-- The column-normalized single-matrix corner-zeroed determinant subtarget -implies the two-matrix corner-zeroed full-band subtarget. -/ -theorem hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroed_of_singleColZero - (hZero : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleColZeroStatement) : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedStatement := - hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroed_of_single - (hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingle_of_colZero hZero) - -/-- The first-column normal form implies the two-matrix corner-zeroed -full-band subtarget. -/ -theorem hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroed_of_singleFirstCol - (hFirst : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleFirstColStatement) : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedStatement := - hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroed_of_singleColZero - (hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleColZero_of_firstCol - hFirst) - -/-- The column-normalized single-matrix corner-zeroed determinant subtarget -implies the full-band `3 × 3` Hurwitz Schur-product subcase. -/ -theorem hurwitzMatrixSchurProductDetFinThreeCoreFullBand_of_cornerZeroedSingleColZero - (hZero : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleColZeroStatement) : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandStatement := - hurwitzMatrixSchurProductDetFinThreeCoreFullBand_of_cornerZeroedSingle - (hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingle_of_colZero hZero) - -/-- The first-column normal form implies the full-band `3 × 3` Hurwitz -Schur-product subcase. -/ -theorem hurwitzMatrixSchurProductDetFinThreeCoreFullBand_of_cornerZeroedSingleFirstCol - (hFirst : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleFirstColStatement) : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandStatement := - hurwitzMatrixSchurProductDetFinThreeCoreFullBand_of_cornerZeroedSingleColZero - (hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleColZero_of_firstCol - hFirst) - -/-- The corner-zero subcase of the triangular-free `3 × 3` Hurwitz -Schur-product core. When the top-right corner `(0, 2)` lies strictly above the -staircase, the corresponding Hadamard-product entry vanishes and the determinant -is nonnegative by `hadamard_det_fin_three_cornerZero_nonneg`. -/ -theorem hurwitzMatrixSchurProductDetFinThreeCoreCornerZero : - HurwitzMatrixSchurProductDetFinThreeCoreCornerZeroStatement := by - intro a b ha hb rows cols hrows hcols _hband _h01 _h12 hcz +/-- Corner-zero `3 × 3` minors of the entrywise product of two totally +nonnegative Hurwitz matrices are nonnegative. When the top-right corner +`(0, 2)` lies strictly above the staircase, the corresponding Hadamard-product +entry vanishes and the determinant is nonnegative by +`hadamard_det_fin_three_cornerZero_nonneg`. -/ +theorem hurwitz_schurProduct_det_fin_three_nonneg_of_cornerZero {a b : ℕ → ℝ} + (ha : (hurwitz a).IsTotallyNonneg) (hb : (hurwitz b).IsTotallyNonneg) + {rows cols : Fin 3 → ℕ} (hrows : StrictMono rows) (hcols : StrictMono cols) + (hcz : rows 0 < 2 * cols 2) : + 0 ≤ ((Matrix.of fun i j => hurwitz a i j * hurwitz b i j).submatrix rows cols).det := by have cza : hurwitz a (rows 0) (cols 2) = 0 := hurwitz_apply_eq_zero_of_lt a hcz have czb : hurwitz b (rows 0) (cols 2) = 0 := @@ -1141,157 +424,11 @@ theorem hurwitzMatrixSchurProductDetFinThreeCoreCornerZero : rw [Matrix.det_fin_three] simp_all -/-- Since the corner-zero subcase is proved, the triangular-free `3 × 3` core -now reduces to the fully in-band top-right subcase alone. -/ -theorem hurwitzMatrixSchurProductDetFinThreeCore_of_fullBand - (hF : HurwitzMatrixSchurProductDetFinThreeCoreFullBandStatement) : - HurwitzMatrixSchurProductDetFinThreeCoreStatement := - hurwitzMatrixSchurProductDetFinThreeCore_of_fullBand_cornerZero hF - hurwitzMatrixSchurProductDetFinThreeCoreCornerZero - -/-- The fully in-band top-right subcase implies the original in-band `3 × 3` -core. -/ -theorem hurwitzMatrixSchurProductDetFinThreeInBand_of_fullBand - (hF : HurwitzMatrixSchurProductDetFinThreeCoreFullBandStatement) : - HurwitzMatrixSchurProductDetFinThreeInBandStatement := - hurwitzMatrixSchurProductDetFinThreeInBand_of_core - (hurwitzMatrixSchurProductDetFinThreeCore_of_fullBand hF) - -/-- The fully in-band top-right subcase implies the low-order, size-`≤ 3`, -Hurwitz matrix Schur-product statement. -/ -theorem hurwitzMatrixSchurProductDetLeThree_of_fullBand - (hF : HurwitzMatrixSchurProductDetFinThreeCoreFullBandStatement) : - HurwitzMatrixSchurProductDetLeThreeStatement := - hurwitzMatrixSchurProductDetLeThree_of_core - (hurwitzMatrixSchurProductDetFinThreeCore_of_fullBand hF) - -/-- The single-matrix corner-zeroed determinant subtarget implies the -triangular-free `3 × 3` Hurwitz Schur-product core. -/ -theorem hurwitzMatrixSchurProductDetFinThreeCore_of_cornerZeroedSingle - (hSingle : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleStatement) : - HurwitzMatrixSchurProductDetFinThreeCoreStatement := - hurwitzMatrixSchurProductDetFinThreeCore_of_fullBand - (hurwitzMatrixSchurProductDetFinThreeCoreFullBand_of_cornerZeroedSingle hSingle) - -/-- The single-matrix corner-zeroed determinant subtarget implies the original -in-band `3 × 3` Hurwitz Schur-product core. -/ -theorem hurwitzMatrixSchurProductDetFinThreeInBand_of_cornerZeroedSingle - (hSingle : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleStatement) : - HurwitzMatrixSchurProductDetFinThreeInBandStatement := - hurwitzMatrixSchurProductDetFinThreeInBand_of_core - (hurwitzMatrixSchurProductDetFinThreeCore_of_cornerZeroedSingle hSingle) - -/-- The single-matrix corner-zeroed determinant subtarget implies the -low-order, size-`≤ 3`, Hurwitz matrix Schur-product statement. -/ -theorem hurwitzMatrixSchurProductDetLeThree_of_cornerZeroedSingle - (hSingle : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleStatement) : - HurwitzMatrixSchurProductDetLeThreeStatement := - hurwitzMatrixSchurProductDetLeThree_of_core - (hurwitzMatrixSchurProductDetFinThreeCore_of_cornerZeroedSingle hSingle) - -/-- The column-normalized single-matrix corner-zeroed determinant subtarget -implies the triangular-free `3 × 3` Hurwitz Schur-product core. -/ -theorem hurwitzMatrixSchurProductDetFinThreeCore_of_cornerZeroedSingleColZero - (hZero : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleColZeroStatement) : - HurwitzMatrixSchurProductDetFinThreeCoreStatement := - hurwitzMatrixSchurProductDetFinThreeCore_of_cornerZeroedSingle - (hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingle_of_colZero hZero) - -/-- The column-normalized single-matrix corner-zeroed determinant subtarget -implies the original in-band `3 × 3` Hurwitz Schur-product core. -/ -theorem hurwitzMatrixSchurProductDetFinThreeInBand_of_cornerZeroedSingleColZero - (hZero : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleColZeroStatement) : - HurwitzMatrixSchurProductDetFinThreeInBandStatement := - hurwitzMatrixSchurProductDetFinThreeInBand_of_cornerZeroedSingle - (hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingle_of_colZero hZero) - -/-- The column-normalized single-matrix corner-zeroed determinant subtarget -implies the low-order, size-`≤ 3`, Hurwitz matrix Schur-product statement. -/ -theorem hurwitzMatrixSchurProductDetLeThree_of_cornerZeroedSingleColZero - (hZero : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleColZeroStatement) : - HurwitzMatrixSchurProductDetLeThreeStatement := - hurwitzMatrixSchurProductDetLeThree_of_cornerZeroedSingle - (hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingle_of_colZero hZero) - -/-- The first-column normal form implies the triangular-free `3 × 3` Hurwitz -Schur-product core. -/ -theorem hurwitzMatrixSchurProductDetFinThreeCore_of_cornerZeroedSingleFirstCol - (hFirst : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleFirstColStatement) : - HurwitzMatrixSchurProductDetFinThreeCoreStatement := - hurwitzMatrixSchurProductDetFinThreeCore_of_cornerZeroedSingleColZero - (hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleColZero_of_firstCol - hFirst) - -/-- The first-column normal form implies the original in-band `3 × 3` Hurwitz -Schur-product core. -/ -theorem hurwitzMatrixSchurProductDetFinThreeInBand_of_cornerZeroedSingleFirstCol - (hFirst : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleFirstColStatement) : - HurwitzMatrixSchurProductDetFinThreeInBandStatement := - hurwitzMatrixSchurProductDetFinThreeInBand_of_cornerZeroedSingleColZero - (hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleColZero_of_firstCol - hFirst) - -/-- The first-column normal form implies the low-order, size-`≤ 3`, Hurwitz -matrix Schur-product statement. -/ -theorem hurwitzMatrixSchurProductDetLeThree_of_cornerZeroedSingleFirstCol - (hFirst : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleFirstColStatement) : - HurwitzMatrixSchurProductDetLeThreeStatement := - hurwitzMatrixSchurProductDetLeThree_of_cornerZeroedSingleColZero - (hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleColZero_of_firstCol - hFirst) - -/-- The triangular-free core immediately gives the fully in-band top-right -subcase. -/ -theorem hurwitzMatrixSchurProductDetFinThreeCoreFullBand_of_core - (hcore : HurwitzMatrixSchurProductDetFinThreeCoreStatement) : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandStatement := - fun {_a _b} ha hb {_rows} {_cols} hrows hcols hband h01 h12 _h02 => - hcore ha hb hrows hcols hband h01 h12 - -/-- After the corner-zero subcase is proved, the triangular-free `3 × 3` core is -equivalent to the fully in-band top-right subcase. -/ -theorem hurwitzMatrixSchurProductDetFinThreeCore_iff_fullBand : - HurwitzMatrixSchurProductDetFinThreeCoreStatement ↔ - HurwitzMatrixSchurProductDetFinThreeCoreFullBandStatement := - ⟨hurwitzMatrixSchurProductDetFinThreeCoreFullBand_of_core, - hurwitzMatrixSchurProductDetFinThreeCore_of_fullBand⟩ - -/-- The triangular-free core immediately gives the corner-zero top-right -subcase. -/ -theorem hurwitzMatrixSchurProductDetFinThreeCoreCornerZero_of_core - (hcore : HurwitzMatrixSchurProductDetFinThreeCoreStatement) : - HurwitzMatrixSchurProductDetFinThreeCoreCornerZeroStatement := - fun {_a _b} ha hb {_rows} {_cols} hrows hcols hband h01 h12 _h02 => - hcore ha hb hrows hcols hband h01 h12 - -/-- The triangular-free `3 × 3` core is equivalent to the conjunction of the -fully in-band top-right subcase and the corner-zero top-right subcase. -/ -theorem hurwitzMatrixSchurProductDetFinThreeCore_iff_fullBand_cornerZero : - HurwitzMatrixSchurProductDetFinThreeCoreStatement ↔ - HurwitzMatrixSchurProductDetFinThreeCoreFullBandStatement ∧ - HurwitzMatrixSchurProductDetFinThreeCoreCornerZeroStatement := - ⟨fun hcore => - ⟨hurwitzMatrixSchurProductDetFinThreeCoreFullBand_of_core hcore, - hurwitzMatrixSchurProductDetFinThreeCoreCornerZero_of_core hcore⟩, - fun h => hurwitzMatrixSchurProductDetFinThreeCore_of_fullBand_cornerZero h.1 h.2⟩ - -/-! ### The first-column normal-form leaf is false - -The leaf -`HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleFirstColStatement` -is strictly stronger than the genuine `3 × 3` minor nonnegativity supplied by -total nonnegativity: the corner-zeroed determinant equals the honest minor -minus the top-right corner contribution, and that subtraction can make it -negative. +/-! ### A single-matrix corner-zeroed inequality is false + +For a single totally nonnegative Hurwitz matrix, the `3 × 3` corner-zeroed +determinant (the honest minor minus the top-right corner contribution) can be +negative, even in first-column normal form. The explicit counterexample below uses the totally nonnegative Hurwitz matrix whose first column is the binomial sequence `k ↦ C(16, k)`, with @@ -1439,12 +576,34 @@ theorem cexA_hurwitz_isTotallyNonneg : (hurwitz cexA).IsTotallyNonneg := by refine hurwitz_isTotallyNonneg_of_firstColumn_isPolyaFreqSeq cexA ?_ simpa [hurwitz_cexA_firstColumn] using cexFirstColumn_isPolyaFreqSeq -/-- The first-column normal-form leaf of GitHub issue #34 is false. Even for +/-- First-column form of the corner-zeroed single-matrix `3 × 3` determinant: +after normalizing the first selected column to `0`, the remaining columns are +shifted back to column `0` by moving rows up by twice the column index. -/ +def hurwitzFullBandCornerZeroedSingleFirstColDet + (a : ℕ → ℝ) (row0 row1 row2 col1 col2 : ℕ) : ℝ := + hurwitz a row0 0 * + (hurwitz a (row1 - 2 * col1) 0 * + hurwitz a (row2 - 2 * col2) 0 - + hurwitz a (row1 - 2 * col2) 0 * + hurwitz a (row2 - 2 * col1) 0) - + hurwitz a (row0 - 2 * col1) 0 * + (hurwitz a row1 0 * hurwitz a (row2 - 2 * col2) 0 - + hurwitz a (row1 - 2 * col2) 0 * hurwitz a row2 0) + +/-- The single-matrix first-column corner-zeroed inequality is false. Even for the concrete totally nonnegative Hurwitz matrix `hurwitz cexA`, the corner-zeroed determinant at `rows = (9, 10, 11)`, `cols = (0, 1, 2)` is negative. -/ -theorem not_hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleFirstCol : - ¬ HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleFirstColStatement := by +theorem not_hurwitzFullBandCornerZeroedSingleFirstColDet_nonneg : + ¬ ∀ {a : ℕ → ℝ}, + (hurwitz a).IsTotallyNonneg → + ∀ {row0 row1 row2 col1 col2 : ℕ}, + row0 < row1 → + row1 < row2 → + 0 < col1 → + col1 < col2 → + 2 * col2 ≤ row0 → + 0 ≤ hurwitzFullBandCornerZeroedSingleFirstColDet a row0 row1 row2 col1 col2 := by intro H have key := H cexA_hurwitz_isTotallyNonneg (row0 := 9) (row1 := 10) (row2 := 11) (col1 := 1) (col2 := 2) (by norm_num) (by norm_num) (by norm_num) (by norm_num) @@ -1453,32 +612,13 @@ theorem not_hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleFi hurwitzFullBandCornerZeroedSingleFirstColDet] at key norm_num [Nat.choose] at key -/-- The column-normalized single-matrix leaf of GitHub issue #34 is false. -/ -theorem not_hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleColZero : - ¬ HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleColZeroStatement := - fun h => not_hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleFirstCol - (hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleFirstCol_of_colZero - h) - -/-- The general single-matrix corner-zeroed leaf of GitHub issue #34 is false. -/ -theorem not_hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingle : - ¬ HurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleStatement := - fun h => not_hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleFirstCol - (hurwitzMatrixSchurProductDetFinThreeCoreFullBandCornerZeroedSingleFirstCol_of_single - h) - -/-! ### Hurwitz staircase/Toeplitz normal form for the full-band Schur product - -The genuine two-matrix issue #34 target is special to Hurwitz matrices, and -(as recorded in `RealRooted.Challenges.TotallyNonnegativeHadamardObstruction`) cannot be -reached from total nonnegativity of the selected `3 × 3` windows alone. The -lemmas below expose the Hurwitz-specific input: the column-shift/staircase -relation `hurwitz_col_shift_add` identifies, on the nonzero staircase, a -Hurwitz matrix entry with a single Toeplitz entry of its column-`0` sequence. -This turns any fully in-band minor of the entrywise product of two Hurwitz -matrices into an honest Toeplitz minor of the pointwise product of the two -column-`0` sequences, and thereby reduces the full-band `3 × 3` core to a -single Pólya-frequency statement about that product sequence. -/ +/-! ### Hurwitz staircase/Toeplitz normal form + +The column-shift/staircase relation `hurwitz_col_shift_add` identifies, on the +nonzero staircase, a Hurwitz matrix entry with a single Toeplitz entry of its +column-`0` sequence. This turns any fully in-band minor of the entrywise +product of two Hurwitz matrices into a Toeplitz minor of the pointwise product +of the two column-`0` sequences. -/ /-- Hurwitz staircase/Toeplitz relation. On the nonzero staircase `2 * j ≤ i`, the `(i, j)` entry of a Hurwitz matrix equals the `(i, 2 * j)` @@ -1517,117 +657,7 @@ theorem hurwitz_schurProduct_det_submatrix_eq_toeplitz_of_band (fun j => 2 * cols j)).det := by rw [hurwitz_schurProduct_submatrix_eq_toeplitz_of_band a b hband] -/-- Reusable reduction of the full-band `3 × 3` Hurwitz Schur-product core -(GitHub issue #34) to a single Pólya-frequency statement. - -If for every pair of totally nonnegative Hurwitz matrices the pointwise product -of their column-`0` sequences is a Pólya-frequency sequence, then the full-band -`3 × 3` core holds. This is faithful to the classical Garloff--Wagner content: -after the staircase change of variables the minor is literally a Toeplitz minor -of that product sequence, so its nonnegativity is exactly the Pólya-frequency -condition. Unlike the refuted single-matrix corner-zeroed route, this genuinely -uses the Hurwitz Toeplitz/staircase structure of both factors. -/ -theorem hurwitzMatrixSchurProductDetFinThreeCoreFullBand_of_polyaFreq - (hPF : ∀ {a b : ℕ → ℝ}, - (hurwitz a).IsTotallyNonneg → - (hurwitz b).IsTotallyNonneg → - IsPolyaFreqSeq (fun k => hurwitz a k 0 * hurwitz b k 0)) : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandStatement := by - intro a b ha hb rows cols hrows hcols _hband _h01 _h12 h02 - have hbandall : ∀ i j : Fin 3, 2 * cols j ≤ rows i := by - intro i j - have hcj : cols j ≤ cols 2 := hcols.monotone (Fin.le_last j) - have hri : rows 0 ≤ rows i := hrows.monotone (Fin.zero_le i) - grind - have hdbl : StrictMono (fun j : Fin 3 ↦ 2 * cols j) := by - intro x y hxy - have := hcols hxy - lia - simpa [hurwitz_schurProduct_det_submatrix_eq_toeplitz_of_band a b hbandall] using - hPF ha hb hrows hdbl - -/-- The Pólya-frequency reduction, transported to the original in-band `3 × 3` -Hurwitz Schur-product core through the existing full-band reduction. -/ -theorem hurwitzMatrixSchurProductDetFinThreeInBand_of_polyaFreq - (hPF : ∀ {a b : ℕ → ℝ}, - (hurwitz a).IsTotallyNonneg → - (hurwitz b).IsTotallyNonneg → - IsPolyaFreqSeq (fun k => hurwitz a k 0 * hurwitz b k 0)) : - HurwitzMatrixSchurProductDetFinThreeInBandStatement := - hurwitzMatrixSchurProductDetFinThreeInBand_of_fullBand - (hurwitzMatrixSchurProductDetFinThreeCoreFullBand_of_polyaFreq hPF) - -/-- The Pólya-frequency reduction, transported to the low-order size-`≤ 3` -Hurwitz Schur-product statement. -/ -theorem hurwitzMatrixSchurProductDetLeThree_of_polyaFreq - (hPF : ∀ {a b : ℕ → ℝ}, - (hurwitz a).IsTotallyNonneg → - (hurwitz b).IsTotallyNonneg → - IsPolyaFreqSeq (fun k => hurwitz a k 0 * hurwitz b k 0)) : - HurwitzMatrixSchurProductDetLeThreeStatement := - hurwitzMatrixSchurProductDetLeThree_of_fullBand - (hurwitzMatrixSchurProductDetFinThreeCoreFullBand_of_polyaFreq hPF) - -/-- Even-column Toeplitz nonnegativity leaf for the column-`0` product -sequence. Only doubled columns `2 * cols j` are selected, so this is strictly -weaker than the false full column-`0` product Pólya-frequency leaf. -/ -def HurwitzColumnZeroProductEvenColToeplitzStatement : Prop := - ∀ {a b : ℕ → ℝ}, - (hurwitz a).IsTotallyNonneg → - (hurwitz b).IsTotallyNonneg → - ∀ {n : ℕ} {rows cols : Fin n → ℕ}, - StrictMono rows → - StrictMono cols → - 0 ≤ ((toeplitz (fun k => hurwitz a k 0 * hurwitz b k 0)).submatrix rows - (fun j => 2 * cols j)).det - -/-- Sharpened reduction of the full-band `3 × 3` Hurwitz Schur-product core -(GitHub issue #34) to the even-column Toeplitz leaf. -/ -theorem hurwitzMatrixSchurProductDetFinThreeCoreFullBand_of_evenColToeplitz - (hEven : HurwitzColumnZeroProductEvenColToeplitzStatement) : - HurwitzMatrixSchurProductDetFinThreeCoreFullBandStatement := by - intro a b ha hb rows cols hrows hcols _hband _h01 _h12 h02 - have hbandall : ∀ i j : Fin 3, 2 * cols j ≤ rows i := by - intro i j - have hcj : cols j ≤ cols 2 := hcols.monotone (Fin.le_last j) - have hri : rows 0 ≤ rows i := hrows.monotone (Fin.zero_le i) - grind - simpa [hurwitz_schurProduct_det_submatrix_eq_toeplitz_of_band a b hbandall] using - hEven ha hb hrows hcols - -/-- The even-column Toeplitz reduction, transported to the original in-band -`3 × 3` Hurwitz Schur-product core. -/ -theorem hurwitzMatrixSchurProductDetFinThreeInBand_of_evenColToeplitz - (hEven : HurwitzColumnZeroProductEvenColToeplitzStatement) : - HurwitzMatrixSchurProductDetFinThreeInBandStatement := - hurwitzMatrixSchurProductDetFinThreeInBand_of_fullBand - (hurwitzMatrixSchurProductDetFinThreeCoreFullBand_of_evenColToeplitz hEven) - -/-- The even-column Toeplitz reduction, transported to the low-order size-`≤ 3` -Hurwitz Schur-product statement. -/ -theorem hurwitzMatrixSchurProductDetLeThree_of_evenColToeplitz - (hEven : HurwitzColumnZeroProductEvenColToeplitzStatement) : - HurwitzMatrixSchurProductDetLeThreeStatement := - hurwitzMatrixSchurProductDetLeThree_of_fullBand - (hurwitzMatrixSchurProductDetFinThreeCoreFullBand_of_evenColToeplitz hEven) - -/-- The full column-`0` product Pólya-frequency leaf implies the sharper -even-column Toeplitz leaf: doubled columns are a special case of arbitrary -columns. The converse is not known and is the point of the sharper leaf. -/ -theorem hurwitzColumnZeroProductEvenColToeplitz_of_polyaFreq - (hPF : ∀ {a b : ℕ → ℝ}, - (hurwitz a).IsTotallyNonneg → - (hurwitz b).IsTotallyNonneg → - IsPolyaFreqSeq (fun k => hurwitz a k 0 * hurwitz b k 0)) : - HurwitzColumnZeroProductEvenColToeplitzStatement := by - intro a b ha hb n rows cols hrows hcols - have hdbl : StrictMono (fun j : Fin n ↦ 2 * cols j) := by - intro x y hxy - have h := hcols hxy - simp_all - exact hPF ha hb hrows hdbl - -/-! ### Hadamard normal form for the even-column Toeplitz leaf +/-! ### Hadamard normal form for even-column Toeplitz minors The even-column Toeplitz minor of the pointwise product of the two column-`0` sequences is, entry by entry, the Hadamard product of the two Hurwitz @@ -1674,10 +704,12 @@ theorem det_hadamard_fin_two_nonneg mul_nonneg (mul_nonneg hM01 hM10) hdN, mul_nonneg hdM (mul_nonneg hN01 hN10), mul_nonneg hdM hdN] -/-- The even-column Toeplitz leaf holds at every size `n ≤ 2`. This is the -size-`≤ 2` part of `HurwitzColumnZeroProductEvenColToeplitzStatement`, obtained -from the Hadamard normal form and the fact that the Hadamard product of two -totally nonnegative matrices has nonnegative determinant in sizes `≤ 2`. -/ +/-- Even-column Toeplitz minors of the column-`0` product sequence of two +totally nonnegative Hurwitz matrices are nonnegative at every size `n ≤ 2`. +This follows from the Hadamard normal form and the fact that the Hadamard +product of two totally nonnegative matrices has nonnegative determinant in +sizes `≤ 2`. It fails at size three; see +`not_hurwitz_schurProduct_det_fin_three_nonneg`. -/ theorem hurwitzColumnZeroProductEvenColToeplitz_of_size_le_two {a b : ℕ → ℝ} (ha : (hurwitz a).IsTotallyNonneg) (hb : (hurwitz b).IsTotallyNonneg) @@ -1695,12 +727,11 @@ theorem hurwitzColumnZeroProductEvenColToeplitz_of_size_le_two exact mul_nonneg (ha.nonneg _ _) (hb.nonneg _ _) · exact det_hadamard_fin_two_nonneg hMa hMb -/-! ### Hurwitz normal form for the even-column Toeplitz leaf +/-! ### Hurwitz normal form for even-column Toeplitz minors The entrywise product of two Hurwitz matrices is again a Hurwitz matrix, namely the Hurwitz matrix of the pointwise product of the two coefficient -sequences. Thus the even-column Toeplitz leaf is equivalent to total -nonnegativity of this pointwise-product Hurwitz matrix. -/ +sequences. -/ /-- The Hurwitz matrix of the pointwise product of two coefficient sequences is the entrywise product of the two Hurwitz matrices. -/ @@ -1751,46 +782,12 @@ theorem toeplitz_colZeroProduct_submatrix_eq_hurwitz_mul simp only [Matrix.submatrix_apply] exact toeplitz_colZeroProduct_apply_eq_hurwitz_mul a b (rows i) (cols j) -/-- Total-nonnegativity leaf in Hurwitz normal form: the Hurwitz matrix of the -pointwise product of two coefficient sequences with totally nonnegative Hurwitz -matrices is itself totally nonnegative. This is the clean Garloff--Wagner -content of GitHub issue #34, equivalent to the even-column Toeplitz leaf. -/ -def HurwitzMulTotallyNonnegStatement : Prop := - ∀ {a b : ℕ → ℝ}, - (hurwitz a).IsTotallyNonneg → - (hurwitz b).IsTotallyNonneg → - (hurwitz (fun k => a k * b k)).IsTotallyNonneg - -/-- The Hurwitz normal-form leaf implies the even-column Toeplitz leaf. -/ -theorem hurwitzColumnZeroProductEvenColToeplitz_of_hurwitzMul - (h : HurwitzMulTotallyNonnegStatement) : - HurwitzColumnZeroProductEvenColToeplitzStatement := - fun {_ _} ha hb {_} {_} {_} hrows hcols => by - simpa [toeplitz_colZeroProduct_submatrix_eq_hurwitz_mul] using - h ha hb hrows hcols - -/-- Conversely, the even-column Toeplitz leaf implies the Hurwitz normal-form -leaf: every minor of the Hurwitz matrix of the pointwise product is an -even-column Toeplitz minor of the column-`0` product sequence. -/ -theorem hurwitzMul_of_hurwitzColumnZeroProductEvenColToeplitz - (h : HurwitzColumnZeroProductEvenColToeplitzStatement) : - HurwitzMulTotallyNonnegStatement := - fun {_ _} ha hb {_} {_} {_} hrows hcols => by - simpa [toeplitz_colZeroProduct_submatrix_eq_hurwitz_mul] using - h ha hb hrows hcols - -/-! ### The column-`0` product Pólya-frequency leaf is false - -The full-band reduction -`hurwitzMatrixSchurProductDetFinThreeCoreFullBand_of_polyaFreq` only shows -that the column-`0` product Pólya-frequency statement is a sufficient condition -for the full-band `3 × 3` Hurwitz Schur-product core. That statement itself is -false: total nonnegativity of a Hurwitz matrix does not force its column-`0` +/-! ### The column-`0` product sequence need not be Pólya-frequency + +Total nonnegativity of a Hurwitz matrix does not force its column-`0` sequence to be Pólya-frequency, and the pointwise product of the column-`0` sequences of two totally nonnegative Hurwitz matrices can fail to be -Pólya-frequency. This rules out this particular Pólya-frequency route to -GitHub issue #34, without bearing on the truth of the classical -Garloff--Wagner theorem itself. -/ +Pólya-frequency. -/ /-- If all odd-indexed entries of a coefficient sequence vanish, then every even row of its Hurwitz matrix is identically zero. -/ @@ -1836,7 +833,14 @@ theorem hurwitz_isTotallyNonneg_of_odd_zero {a : ℕ → ℝ} exact hurwitz_even_row_eq_zero_of_odd_zero hodd _ _ exact le_of_eq (Matrix.det_eq_zero_of_row_eq_zero k hzero).symm -/-! ### The unrestricted infinite Schur-product statement is false -/ +/-! ### Entrywise products of totally nonnegative Hurwitz matrices + +Total nonnegativity of infinite Hurwitz matrices is not preserved by entrywise +products, already for a fully in-band `3 × 3` minor. Garloff--Wagner, +*Hadamard products of stable polynomials are stable*, J. Math. Anal. Appl. 202 +(1996), 797--809, Theorem 13, treats finite nonsingular Hurwitz matrices; it +does not cover arbitrary infinite, possibly singular matrices in the +row-oriented convention used here. -/ /-- First coefficient sequence in the infinite Schur-product counterexample. Its even subsequence is `1, 2, 2, ...`, and its odd coefficients vanish. -/ @@ -1856,31 +860,58 @@ theorem hurwitzSchurCounterexampleRight_odd_zero (n : ℕ) : hurwitzSchurCounterexampleRight (2 * n + 1) = 0 := by simp [hurwitzSchurCounterexampleRight] -/-- The two infinite PF certificates reduce the proposed Hurwitz Schur-product -statement to an explicit `3 × 3` minor with determinant `-4`. -/ -theorem not_hurwitzMatrixSchurProductTNStatement_of_counterexamplePF +/-- The two infinite PF certificates reduce the fully in-band `3 × 3` minor +statement to an explicit minor with determinant `-4`, at rows `(5, 7, 9)` and +columns `(0, 1, 2)`. -/ +theorem not_hurwitz_schurProduct_det_fin_three_nonneg_of_counterexamplePF (hleft : IsPolyaFreqSeq (fun n => hurwitzSchurCounterexampleLeft (2 * n))) (hright : IsPolyaFreqSeq (fun n => hurwitzSchurCounterexampleRight (2 * n))) : - ¬ HurwitzMatrixSchurProductTNStatement := by + ¬ ∀ {a b : ℕ → ℝ}, + (hurwitz a).IsTotallyNonneg → + (hurwitz b).IsTotallyNonneg → + ∀ {rows cols : Fin 3 → ℕ}, + StrictMono rows → + StrictMono cols → + (∀ i j : Fin 3, 2 * cols j ≤ rows i) → + 0 ≤ ((Matrix.of fun i j => hurwitz a i j * hurwitz b i j).submatrix rows cols).det := by intro H have hleftTN : (hurwitz hurwitzSchurCounterexampleLeft).IsTotallyNonneg := hurwitz_isTotallyNonneg_of_odd_zero hurwitzSchurCounterexampleLeft_odd_zero hleft have hrightTN : (hurwitz hurwitzSchurCounterexampleRight).IsTotallyNonneg := hurwitz_isTotallyNonneg_of_odd_zero hurwitzSchurCounterexampleRight_odd_zero hright - have hminor := H hleftTN hrightTN (n := 3) (rows := ![5, 7, 9]) - (cols := ![0, 1, 2]) (by decide) (by decide) + have hminor := H hleftTN hrightTN (rows := ![5, 7, 9]) + (cols := ![0, 1, 2]) (by decide) (by decide) (by decide) erw [Matrix.det_fin_three] at hminor norm_num [Matrix.det_fin_three, Matrix.submatrix_apply, Matrix.of_apply, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two, hurwitz, toeplitz, hurwitzSchurCounterexampleLeft, hurwitzSchurCounterexampleRight] at hminor -/-- The unrestricted, infinite Hurwitz-matrix Schur-product statement is false. -/ -theorem not_hurwitzMatrixSchurProductTNStatement : - ¬ HurwitzMatrixSchurProductTNStatement := by - apply not_hurwitzMatrixSchurProductTNStatement_of_counterexamplePF +/-- Fully in-band `3 × 3` minors of the entrywise product of two totally +nonnegative Hurwitz matrices can be negative. -/ +theorem not_hurwitz_schurProduct_det_fin_three_nonneg : + ¬ ∀ {a b : ℕ → ℝ}, + (hurwitz a).IsTotallyNonneg → + (hurwitz b).IsTotallyNonneg → + ∀ {rows cols : Fin 3 → ℕ}, + StrictMono rows → + StrictMono cols → + (∀ i j : Fin 3, 2 * cols j ≤ rows i) → + 0 ≤ ((Matrix.of fun i j => hurwitz a i j * hurwitz b i j).submatrix rows cols).det := by + apply not_hurwitz_schurProduct_det_fin_three_nonneg_of_counterexamplePF · simpa [hurwitzSchurCounterexampleLeft] using oneThenTwo_isPolyaFreqSeq · simpa [hurwitzSchurCounterexampleRight] using natSucc_isPolyaFreqSeq +/-- The unrestricted, infinite Hurwitz-matrix Schur-product statement is false: +the entrywise product of two totally nonnegative Hurwitz matrices need not be +totally nonnegative. -/ +theorem not_hurwitz_schurProduct_isTotallyNonneg : + ¬ ∀ {a b : ℕ → ℝ}, + (hurwitz a).IsTotallyNonneg → + (hurwitz b).IsTotallyNonneg → + (Matrix.of fun i j => hurwitz a i j * hurwitz b i j).IsTotallyNonneg := + fun H => not_hurwitz_schurProduct_det_fin_three_nonneg + fun {_ _} ha hb {_ _} hrows hcols _hband => H ha hb hrows hcols + /-- Counterexample coefficient sequence `1 + X^2`. -/ def cexOddZero : ℕ → ℝ := fun n => if n = 0 then 1 else if n = 2 then 1 else 0 @@ -1944,7 +975,8 @@ theorem cexOddZero_col0_three : hurwitz cexOddZero 3 0 = 1 := by ite_eq_left (Nat.zero_le 1)] simp [cexOddZero] -/-- The column-`0` product Pólya-frequency leaf of GitHub issue #34 is false. +/-- The column-`0` product sequence of two totally nonnegative Hurwitz +matrices need not be Pólya-frequency. Using `a = b = cexOddZero`, both Hurwitz matrices are totally nonnegative, yet the pointwise product of their column-`0` sequences is `0, 1, 0, 1, 0, …`, diff --git a/RealRooted/ObreschkoffConverse/Derivative.lean b/RealRooted/ObreschkoffConverse/Derivative.lean index b8b94a6f7..3b54615f1 100644 --- a/RealRooted/ObreschkoffConverse/Derivative.lean +++ b/RealRooted/ObreschkoffConverse/Derivative.lean @@ -104,12 +104,6 @@ theorem derivative_roots_sum_le_of_strictInterl_sameDegree_monic {f g : ℝ[X]} have hdeg_pos : 0 < (f.natDegree : ℝ) := by positivity nlinarith -/-- Same-degree branch of the standard fact that differentiation preserves -oriented weak interlacing. -/ -def derivativePreservesStrictInterlSameDegreeStatement : Prop := - ∀ {f g : ℝ[X]}, StrictInterl f g → f.natDegree = g.natDegree → - Interl f.derivative g.derivative - /-- Scaling both sides by nonzero constants preserves zero-aware proper position. -/ private lemma interl_C_mul_left_right {a b : ℝ} (ha : a ≠ 0) (hb : b ≠ 0) @@ -138,38 +132,12 @@ lemma StrictInterl.of_degree_zero_degree_zero · simp [hroots_g] · exact Or.inr ⟨by lia, by simp [ListAlternates]⟩ -/-- Degree-at-least-two same-degree branch of the standard fact that -differentiation preserves oriented weak interlacing. -/ -def derivativePreservesStrictInterlSameDegreeOfTwoLeNatDegreeStatement : Prop := - ∀ {f g : ℝ[X]}, StrictInterl f g → f.natDegree = g.natDegree → 2 ≤ f.natDegree → - Interl f.derivative g.derivative - -/-- Positive-leading-coefficient form of the degree-at-least-two same-degree -derivative-preservation branch. -/ -def derivativePreservesStrictInterlSameDegreeOfTwoLeNatDegreePosLeadingStatement : Prop := - ∀ {f g : ℝ[X]}, HasPosLeadingCoeff f → HasPosLeadingCoeff g → - StrictInterl f g → f.natDegree = g.natDegree → 2 ≤ f.natDegree → - Interl f.derivative g.derivative - -/-- Monic form of the degree-at-least-two same-degree derivative-preservation -branch. -/ -def derivativePreservesStrictInterlSameDegreeOfTwoLeNatDegreeMonicStatement : Prop := - ∀ {f g : ℝ[X]}, f.Monic → g.Monic → - StrictInterl f g → f.natDegree = g.natDegree → 2 ≤ f.natDegree → - Interl f.derivative g.derivative - -/-- Nonzero monic form of the degree-at-least-two same-degree -derivative-preservation branch. -/ -def derivativePreservesStrictInterlSameDegreeOfTwoLeNatDegreeMonicStrictInterlStatement : Prop := - ∀ {f g : ℝ[X]}, f.Monic → g.Monic → - StrictInterl f g → f.natDegree = g.natDegree → 2 ≤ f.natDegree → - StrictInterl f.derivative g.derivative - /-- Monic degree-at-least-two same-degree branch of the standard fact that differentiation preserves oriented weak interlacing. -/ -theorem derivativePreservesStrictInterlSameDegreeOfTwoLeNatDegreeMonic : - derivativePreservesStrictInterlSameDegreeOfTwoLeNatDegreeMonicStatement := by - intro f g hf_monic hg_monic hfg hdeg htwo +theorem derivative_interl_of_strictInterl_sameDegree_monic {f g : ℝ[X]} + (hf_monic : f.Monic) (hg_monic : g.Monic) (hfg : StrictInterl f g) + (hdeg : f.natDegree = g.natDegree) (htwo : 2 ≤ f.natDegree) : + Interl f.derivative g.derivative := by have hfder_ne : f.derivative ≠ 0 := Polynomial.derivative_ne_zero.mpr (by lia) have hgder_ne : g.derivative ≠ 0 := @@ -185,32 +153,14 @@ theorem derivativePreservesStrictInterlSameDegreeOfTwoLeNatDegreeMonic : hf_monic hg_monic hfg hdeg htwo hrev.2.1.2 hrev.1.2 exact (hrev.of_reverse_of_roots_sum_le hdeg_der hsum_der).toInterl -/-- The nonzero monic branch follows from the zero-aware monic branch, -since the degree hypotheses make both derivatives nonzero. -/ -theorem derivativePreservesStrictInterlSameDegree_monicStrictInterl_of_monic - (hmonic : derivativePreservesStrictInterlSameDegreeOfTwoLeNatDegreeMonicStatement) : - derivativePreservesStrictInterlSameDegreeOfTwoLeNatDegreeMonicStrictInterlStatement := by - intro f g hf_monic hg_monic hfg hdeg htwo - have hfder_ne : f.derivative ≠ 0 := - Polynomial.derivative_ne_zero.mpr (by lia) - have hgder_ne : g.derivative ≠ 0 := - Polynomial.derivative_ne_zero.mpr (by lia) - rcases hmonic hf_monic hg_monic hfg hdeg htwo with hfzero | hgzero | hstrictInterl <;> simp_all - -/-- The zero-aware monic branch follows from the nonzero monic branch. -/ -theorem derivativePreservesStrictInterlSameDegree_of_monicStrictInterl - (hmonic : - derivativePreservesStrictInterlSameDegreeOfTwoLeNatDegreeMonicStrictInterlStatement) : - derivativePreservesStrictInterlSameDegreeOfTwoLeNatDegreeMonicStatement := - fun {_ _} hf_monic hg_monic hfg hdeg htwo => - (hmonic hf_monic hg_monic hfg hdeg htwo).toInterl - -/-- The positive-leading-coefficient branch follows from the monic branch by -normalizing both polynomials by their leading coefficients. -/ -theorem derivativePreservesStrictInterlSameDegree_of_monic - (hmonic : derivativePreservesStrictInterlSameDegreeOfTwoLeNatDegreeMonicStatement) : - derivativePreservesStrictInterlSameDegreeOfTwoLeNatDegreePosLeadingStatement := by - intro f g hf_pos hg_pos hfg hdeg htwo +/-- Positive-leading-coefficient degree-at-least-two same-degree branch, +obtained from the monic branch by normalizing both polynomials by their leading +coefficients. -/ +theorem derivative_interl_of_strictInterl_sameDegree_posLeading {f g : ℝ[X]} + (hf_pos : HasPosLeadingCoeff f) (hg_pos : HasPosLeadingCoeff g) + (hfg : StrictInterl f g) (hdeg : f.natDegree = g.natDegree) + (htwo : 2 ≤ f.natDegree) : + Interl f.derivative g.derivative := by have hf_lc_ne : f.leadingCoeff ≠ 0 := ne_of_gt hf_pos have hg_lc_ne : g.leadingCoeff ≠ 0 := ne_of_gt hg_pos let f₀ : ℝ[X] := C f.leadingCoeff⁻¹ * f @@ -232,7 +182,7 @@ theorem derivativePreservesStrictInterlSameDegree_of_monic have htwo₀ : 2 ≤ f₀.natDegree := by simpa [f₀, natDegree_C_mul (inv_ne_zero hf_lc_ne)] using htwo have hscaled : Interl f₀.derivative g₀.derivative := - hmonic hf₀_monic hg₀_monic hfg₀ hdeg₀ htwo₀ + derivative_interl_of_strictInterl_sameDegree_monic hf₀_monic hg₀_monic hfg₀ hdeg₀ htwo₀ have hscaled' : Interl (C f.leadingCoeff⁻¹ * f.derivative) (C g.leadingCoeff⁻¹ * g.derivative) := by @@ -253,13 +203,12 @@ theorem derivativePreservesStrictInterlSameDegree_of_monic simp [hg_lc_ne] simp_all -/-- The degree-at-least-two same-degree branch follows from its +/-- Degree-at-least-two same-degree branch, obtained from the positive-leading-coefficient form by scaling both polynomials by signs. -/ -theorem derivativePreservesStrictInterlSameDegree_of_posLeading - (hpos : - derivativePreservesStrictInterlSameDegreeOfTwoLeNatDegreePosLeadingStatement) : - derivativePreservesStrictInterlSameDegreeOfTwoLeNatDegreeStatement := by - intro f g hfg hdeg htwo +theorem derivative_interl_of_strictInterl_sameDegree_two_le {f g : ℝ[X]} + (hfg : StrictInterl f g) (hdeg : f.natDegree = g.natDegree) + (htwo : 2 ≤ f.natDegree) : + Interl f.derivative g.derivative := by have hf_lc_ne : f.leadingCoeff ≠ 0 := leadingCoeff_ne_zero.mpr hfg.1.1 have hg_lc_ne : g.leadingCoeff ≠ 0 := leadingCoeff_ne_zero.mpr hfg.2.1.1 let sf : ℝ := if 0 < f.leadingCoeff then 1 else -1 @@ -290,7 +239,7 @@ theorem derivativePreservesStrictInterlSameDegree_of_posLeading simpa [f₀, g₀, natDegree_C_mul hsf_ne, natDegree_C_mul hsg_ne] using hdeg have htwo₀ : 2 ≤ f₀.natDegree := by simpa [f₀, natDegree_C_mul hsf_ne] using htwo have hscaled : Interl f₀.derivative g₀.derivative := - hpos hf₀_pos hg₀_pos hfg₀ hdeg₀ htwo₀ + derivative_interl_of_strictInterl_sameDegree_posLeading hf₀_pos hg₀_pos hfg₀ hdeg₀ htwo₀ have hscaled' : Interl (C sf * f.derivative) (C sg * g.derivative) := by simpa [f₀, g₀, derivative_C_mul] using hscaled have hback : @@ -299,15 +248,14 @@ theorem derivativePreservesStrictInterlSameDegree_of_posLeading interl_C_mul_left_right (inv_ne_zero hsf_ne) (inv_ne_zero hsg_ne) hscaled' grind -/-- The same-degree derivative-preservation statement follows from its -degree-at-least-two branch. Degrees zero and one are elementary because the -derivatives are zero or nonzero constants. -/ -theorem derivativePreservesStrictInterlSameDegree_of_two_le_natDegree - (hlarge : derivativePreservesStrictInterlSameDegreeOfTwoLeNatDegreeStatement) : - derivativePreservesStrictInterlSameDegreeStatement := by - intro f g hfg hdeg +/-- Same-degree branch of differentiation preserving weak interlacing. +Degrees zero and one are elementary because the derivatives are zero or nonzero +constants. -/ +theorem derivative_interl_of_strictInterl_sameDegree {f g : ℝ[X]} + (hfg : StrictInterl f g) (hdeg : f.natDegree = g.natDegree) : + Interl f.derivative g.derivative := by by_cases hlarge_deg : 2 ≤ f.natDegree - · exact hlarge hfg hdeg hlarge_deg + · exact derivative_interl_of_strictInterl_sameDegree_two_le hfg hdeg hlarge_deg · by_cases hfdeg0 : f.natDegree = 0 · have hfder : f.derivative = 0 := Polynomial.derivative_eq_zero.mpr hfdeg0 @@ -332,62 +280,28 @@ theorem derivativePreservesStrictInterlSameDegree_of_two_le_natDegree (StrictInterl.of_degree_zero_degree_zero hfder_rr.1 hfder_rr.2 hgder_rr.1 hgder_rr.2 hfder_deg0 hgder_deg0).toInterl -/-- The full zero-aware derivative-preservation statement follows from the -same-degree branch. The differ-by-one branch is -`derivative_interl_of_strictInterl_succDegree`, proved above from the forward and -converse Obreschkoff theorems. -/ -theorem derivativePreservesInterl_of_sameDegree - (hsame : derivativePreservesStrictInterlSameDegreeStatement) : - derivativePreservesInterlStatement := by - intro f g hfg +/-- Differentiation preserves zero-aware weak interlacing (Rolle--Obreschkoff). +The same-degree branch is `derivative_interl_of_strictInterl_sameDegree`; the +differ-by-one branch is `derivative_interl_of_strictInterl_succDegree`, proved +above from the forward and converse Obreschkoff theorems. -/ +theorem derivativePreservesInterl {p q : ℝ[X]} (hfg : Interl p q) : + Interl p.derivative q.derivative := by rcases hfg with hfzero | hgzero | hfg' · rw [hfzero, derivative_zero] exact interl_zero_left _ · rw [hgzero, derivative_zero] exact interl_zero_right _ · rcases hfg'.natDegree_eq_or_eq_succ with hsameDegree | hsuccDegree - · exact hsame hfg' hsameDegree.symm + · exact derivative_interl_of_strictInterl_sameDegree hfg' hsameDegree.symm · exact derivative_interl_of_strictInterl_succDegree hfg' hsuccDegree.symm -/-- Same-degree branch of differentiation preserving weak interlacing. -/ -theorem derivativePreservesStrictInterlSameDegree : - derivativePreservesStrictInterlSameDegreeStatement := - derivativePreservesStrictInterlSameDegree_of_two_le_natDegree <| - derivativePreservesStrictInterlSameDegree_of_posLeading <| - derivativePreservesStrictInterlSameDegree_of_monic - derivativePreservesStrictInterlSameDegreeOfTwoLeNatDegreeMonic - -/-- Differentiation preserves zero-aware weak interlacing. This is the -witness for `derivativePreservesInterlStatement`. -/ -theorem derivativePreservesInterl : derivativePreservesInterlStatement := - derivativePreservesInterl_of_sameDegree derivativePreservesStrictInterlSameDegree - -/-! -### Direct #42 / shared #41 derivative-preservation API - -These wrappers repackage `derivativePreservesStrictInterlSameDegree` and -`derivativePreservesInterl` in applied forms used by the closed-segment and -common-interleaver routes. --/ - -/-- Zero-aware derivative preservation, applied form of `derivativePreservesInterl`. -/ -theorem derivative_interl_of_interl {f g : ℝ[X]} (h : Interl f g) : - Interl f.derivative g.derivative := - derivativePreservesInterl h +/-! ### Strict derivative preservation -/ /-- A `StrictInterl` input yields zero-aware derivative preservation. -/ theorem derivative_interl_of_strictInterl {f g : ℝ[X]} (h : StrictInterl f g) : Interl f.derivative g.derivative := derivativePreservesInterl h.toInterl -/-- Same-degree derivative preservation, applied form of -`derivativePreservesStrictInterlSameDegree`. -/ -theorem derivative_interl_of_strictInterl_sameDegree - {f g : ℝ[X]} (h : StrictInterl f g) - (hdeg : f.natDegree = g.natDegree) : - Interl f.derivative g.derivative := - derivativePreservesStrictInterlSameDegree h hdeg - /-- Strict `StrictInterl` output in the same-degree case. -/ theorem derivative_strictInterl_of_strictInterl_sameDegree {f g : ℝ[X]} (h : StrictInterl f g) @@ -398,7 +312,7 @@ theorem derivative_strictInterl_of_strictInterl_sameDegree have hgder_ne : g.derivative ≠ 0 := Polynomial.derivative_ne_zero.mpr (by lia) exact - (derivativePreservesStrictInterlSameDegree h hdeg).toStrictInterl_of_ne hfder_ne hgder_ne + (derivative_interl_of_strictInterl_sameDegree h hdeg).toStrictInterl_of_ne hfder_ne hgder_ne /-- Strict `StrictInterl` output in the succ-degree case. -/ theorem derivative_strictInterl_of_strictInterl_succDegree diff --git a/RealRooted/ObreschkoffConverse/Regularization.lean b/RealRooted/ObreschkoffConverse/Regularization.lean index 8d1755e1b..97d2c96c3 100644 --- a/RealRooted/ObreschkoffConverse/Regularization.lean +++ b/RealRooted/ObreschkoffConverse/Regularization.lean @@ -904,9 +904,9 @@ real-rooted with simple roots, the remaining proof is only bookkeeping: 2. dispatch to the same-degree / succ-degree simple-pair theorem above; and 3. scale back to the original pair. -This isolates the still-missing bridge in `strictInterl_of_allComboRealRooted`: -producing the `hcombo` hypothesis for the *original* pair from -`AllComboRealRooted` plus the no-common-roots assumption. -/ +`strictInterl_of_allComboRealRooted` applies this after producing the `hcombo` +hypothesis for the *original* pair from `AllComboRealRooted` plus the +no-common-roots assumption. -/ theorem ObreschkoffConverseInternal.strictInterl_of_eq_zero_or_simple_combo_of_no_common {f g : ℝ[X]} (hf_ne : f ≠ 0) (hf_splits : f.Splits) (hg_ne : g ≠ 0) (hg_splits : g.Splits) diff --git a/RealRooted/Tactic/Examples/Hadamard.lean b/RealRooted/Tactic/Examples/Hadamard.lean index e6e2e484d..29dd205b9 100644 --- a/RealRooted/Tactic/Examples/Hadamard.lean +++ b/RealRooted/Tactic/Examples/Hadamard.lean @@ -5,27 +5,6 @@ open Polynomial namespace RealRooted namespace Tactic -example : - finiteSchurSzegoCompositionNonzeroStatement := by - rr_schur_szego_nonzero_statement - -example : - finiteSchurSzegoCompositionStatement := by - rr_schur_szego_statement - -example (hSZ : finiteSchurSzegoCompositionStatement) : - pfCubicDiscrDiagonalNonnegStatement := by - rr_schur_szego_pf_cubic_diagonal_base using - schur_szego := hSZ - -example : - schurPolyaWagnerHadamardPFStatement := by - rr_hadamard_pf_statement - -example : - garloffWagnerHadamardNonnegRealRootedStatement := by - rr_hadamard_nonneg_realrooted_statement - example {n : ℕ} {f p : ℝ[X]} (hf : IsPFPolynomial f) (hfdeg : f.natDegree ≤ n) @@ -213,75 +192,6 @@ example {n : ℕ} {f p : ℝ[X]} cubic_numerator := hnum, nonzero := hout -example {n : ℕ} {f p : ℝ[X]} - (hbase : pfCubicDiscrDiagonalNonnegStatement) - (hn : 3 ≤ n) - (hf : IsPFPolynomial f) - (hfdeg : f.natDegree ≤ 3) - (hpdeg : p.natDegree ≤ n) - (hsplits : p.Splits) : - schurSzegoComp n f p = 0 ∨ (schurSzegoComp n f p).Splits := by - rr_schur_szego_pf_factor_degree_le_three_diagonal_base using - diagonal_base := hbase, - level_ge_three := hn, - pf_factor := hf, - pf_degree_le_three := hfdeg, - input_degree := hpdeg, - input_splits := hsplits - -example {n : ℕ} {f p : ℝ[X]} - (hbase : pfCubicDiscrDiagonalNonnegStatement) - (hn : 3 ≤ n) - (hf : IsPFPolynomial f) - (hfdeg : f.natDegree ≤ 3) - (hpdeg : p.natDegree ≤ n) - (hsplits : p.Splits) - (hout : schurSzegoComp n f p ≠ 0) : - (schurSzegoComp n f p).Splits := by - rr_schur_szego_pf_factor_degree_le_three_diagonal_base_splits using - diagonal_base := hbase, - level_ge_three := hn, - pf_factor := hf, - pf_degree_le_three := hfdeg, - input_degree := hpdeg, - input_splits := hsplits, - nonzero := hout - -example {n : ℕ} {f p : ℝ[X]} - (hbase : pfCubicDiscrDiagonalNonnegStatement) - (hf : IsPFPolynomial f) - (hfdeg : f.natDegree ≤ 3) - (hfn : f.natDegree ≤ n) - (hpdeg : p.natDegree ≤ n) - (hsplits : p.Splits) : - schurSzegoComp n f p = 0 ∨ (schurSzegoComp n f p).Splits := by - rr_schur_szego_pf_factor_degree_le_three_diagonal_base_left_degree using - diagonal_base := hbase, - pf_factor := hf, - pf_degree_le_three := hfdeg, - pf_degree := hfn, - input_degree := hpdeg, - input_splits := hsplits - -example {n : ℕ} {f p : ℝ[X]} - (hbase : pfCubicDiscrDiagonalNonnegStatement) - (hf : IsPFPolynomial f) - (hfdeg : f.natDegree ≤ 3) - (hfn : f.natDegree ≤ n) - (hpdeg : p.natDegree ≤ n) - (hsplits : p.Splits) - (hout : schurSzegoComp n f p ≠ 0) : - (schurSzegoComp n f p).Splits := by - rr_schur_szego_pf_factor_degree_le_three_diagonal_base_left_degree_splits - using - diagonal_base := hbase, - pf_factor := hf, - pf_degree_le_three := hfdeg, - pf_degree := hfn, - input_degree := hpdeg, - input_splits := hsplits, - nonzero := hout - example {n : ℕ} {f p : ℝ[X]} (hf : IsPFPolynomial f) (hfdeg : f.natDegree ≤ 3) diff --git a/RealRooted/Tactic/Examples/HermiteBiehler.lean b/RealRooted/Tactic/Examples/HermiteBiehler.lean index 16fda9a77..86bea8db0 100644 --- a/RealRooted/Tactic/Examples/HermiteBiehler.lean +++ b/RealRooted/Tactic/Examples/HermiteBiehler.lean @@ -5,18 +5,6 @@ open Polynomial namespace RealRooted namespace Tactic -example : - hermiteBiehlerForwardPosStatement := by - rr_hermite_biehler_forward_pos_statement - -example : - hermiteBiehlerConverseStatement := by - rr_hermite_biehler_converse_statement - -example : - HermiteBiehlerStableToHurwitzOddEvenStatement := by - rr_hermite_biehler_odd_even_hurwitz_statement - example {f g : ℝ[X]} (hf : HasPosLeadingCoeff f) (hg : HasPosLeadingCoeff g) (hstrictInterl : StrictInterl g f) : diff --git a/RealRooted/Tactic/Examples/OEIS/ClassicalFamilies.lean b/RealRooted/Tactic/Examples/OEIS/ClassicalFamilies.lean index edca49454..efa10c667 100644 --- a/RealRooted/Tactic/Examples/OEIS/ClassicalFamilies.lean +++ b/RealRooted/Tactic/Examples/OEIS/ClassicalFamilies.lean @@ -15,11 +15,6 @@ open scoped BigOperators namespace RealRooted namespace Tactic -/-- Hermite--Biehler statement exit exposed through the OEIS facade. -/ -example : - hermiteBiehlerForwardPosStatement := by - rr_hermite_biehler_forward_pos_statement - /-- Hermite--Biehler odd/even Hurwitz row-family exit exposed through the OEIS facade. -/ example {P Q : Nat → ℝ[X]} diff --git a/RealRooted/Tactic/Hadamard.lean b/RealRooted/Tactic/Hadamard.lean index fd3cf1c3d..5443c78ba 100644 --- a/RealRooted/Tactic/Hadamard.lean +++ b/RealRooted/Tactic/Hadamard.lean @@ -89,47 +89,6 @@ theorem schurSzegoComp_splits_of_pf_factor_natDegree_le_three_cubicNum hn hf hfdeg hpdeg hsplits hnum) hout -theorem schurSzegoComp_splits_of_pf_factor_degree_le_three_diagonalBase - (hbase : pfCubicDiscrDiagonalNonnegStatement) - {n : ℕ} (hn : 3 ≤ n) {f p : ℝ[X]} - (hf : IsPFPolynomial f) - (hfdeg : f.natDegree ≤ 3) - (hpdeg : p.natDegree ≤ n) - (hsplits : p.Splits) - (hout : schurSzegoComp n f p ≠ 0) : - (schurSzegoComp n f p).Splits := - Or.resolve_left - (finiteSchurSzegoComposition_of_pf_factor_le_three_of_pfCubicDiscrDiagonalNonneg - hbase hn hf hfdeg hpdeg hsplits) - hout - -theorem schurSzegoComp_zero_or_splits_of_diagonalBase_leftDegree - (hbase : pfCubicDiscrDiagonalNonnegStatement) - {n : ℕ} {f p : ℝ[X]} - (hf : IsPFPolynomial f) - (hfdeg : f.natDegree ≤ 3) - (hfn : f.natDegree ≤ n) - (hpdeg : p.natDegree ≤ n) - (hsplits : p.Splits) : - schurSzegoComp n f p = 0 ∨ (schurSzegoComp n f p).Splits := - finiteSchurSzegoComposition_of_pf_factor_le_three_leftNatDegree_of_pfCubicDiscrDiagonalNonneg - hbase hf hfdeg hfn hpdeg hsplits - -theorem schurSzegoComp_splits_of_pf_factor_degree_le_three_diagonalBase_leftDegree - (hbase : pfCubicDiscrDiagonalNonnegStatement) - {n : ℕ} {f p : ℝ[X]} - (hf : IsPFPolynomial f) - (hfdeg : f.natDegree ≤ 3) - (hfn : f.natDegree ≤ n) - (hpdeg : p.natDegree ≤ n) - (hsplits : p.Splits) - (hout : schurSzegoComp n f p ≠ 0) : - (schurSzegoComp n f p).Splits := - Or.resolve_left - (schurSzegoComp_zero_or_splits_of_diagonalBase_leftDegree - hbase hf hfdeg hfn hpdeg hsplits) - hout - theorem schurSzegoComp_splits_of_pf_factor_degree_le_three_num_leftDegree {n : ℕ} {f p : ℝ[X]} (hf : IsPFPolynomial f) @@ -233,23 +192,6 @@ theorem hadamardProduct_sequence_interl {F G P Q : Nat → ℝ[X]} hadamardProduct_interl_of_nonneg_strictInterl (hF i) (hG i) (hP i) (hQ i) (hFG i) (hPQ i) -syntax (name := rr_schur_szego_nonzero_statement_named) - "rr_schur_szego_nonzero_statement" : tactic - -syntax (name := rr_schur_szego_statement_named) - "rr_schur_szego_statement" : tactic - -syntax (name := rr_schur_szego_pf_cubic_diagonal_base_named) - "rr_schur_szego_pf_cubic_diagonal_base" " using " - "schur_szego" ":=" term : - tactic - -syntax (name := rr_hadamard_pf_statement_named) - "rr_hadamard_pf_statement" : tactic - -syntax (name := rr_hadamard_nonneg_realrooted_statement_named) - "rr_hadamard_nonneg_realrooted_statement" : tactic - syntax (name := rr_schur_szego_named) "rr_schur_szego" " using " "pf_factor" ":=" term "," @@ -360,50 +302,6 @@ syntax (name := rr_schur_szego_pf_factor_degree_le_three_num_splits_named) "nonzero" ":=" term : tactic -syntax (name := rr_schur_szego_pf_factor_degree_le_three_diagonal_base_named) - "rr_schur_szego_pf_factor_degree_le_three_diagonal_base" " using " - "diagonal_base" ":=" term "," - "level_ge_three" ":=" term "," - "pf_factor" ":=" term "," - "pf_degree_le_three" ":=" term "," - "input_degree" ":=" term "," - "input_splits" ":=" term : - tactic - -syntax (name := rr_schur_szego_pf_factor_degree_le_three_diagonal_base_splits_named) - "rr_schur_szego_pf_factor_degree_le_three_diagonal_base_splits" " using " - "diagonal_base" ":=" term "," - "level_ge_three" ":=" term "," - "pf_factor" ":=" term "," - "pf_degree_le_three" ":=" term "," - "input_degree" ":=" term "," - "input_splits" ":=" term "," - "nonzero" ":=" term : - tactic - -syntax (name := rr_schur_szego_pf_factor_degree_le_three_diagonal_base_left_degree_named) - "rr_schur_szego_pf_factor_degree_le_three_diagonal_base_left_degree" " using " - "diagonal_base" ":=" term "," - "pf_factor" ":=" term "," - "pf_degree_le_three" ":=" term "," - "pf_degree" ":=" term "," - "input_degree" ":=" term "," - "input_splits" ":=" term : - tactic - -syntax - (name := rr_schur_szego_pf_factor_degree_le_three_diagonal_base_left_degree_splits_named) - "rr_schur_szego_pf_factor_degree_le_three_diagonal_base_left_degree_splits" - " using " - "diagonal_base" ":=" term "," - "pf_factor" ":=" term "," - "pf_degree_le_three" ":=" term "," - "pf_degree" ":=" term "," - "input_degree" ":=" term "," - "input_splits" ":=" term "," - "nonzero" ":=" term : - tactic - syntax (name := rr_schur_szego_pf_factor_degree_le_three_num_left_degree_named) "rr_schur_szego_pf_factor_degree_le_three_num_left_degree" " using " "pf_factor" ":=" term "," @@ -525,20 +423,6 @@ syntax (name := rr_hadamard_sequence_interl_named) tactic macro_rules - | `(tactic| rr_schur_szego_nonzero_statement) => - `(tactic| exact RealRooted.finiteSchurSzegoCompositionNonzero) - | `(tactic| rr_schur_szego_statement) => - `(tactic| exact RealRooted.finiteSchurSzegoComposition) - | `(tactic| - rr_schur_szego_pf_cubic_diagonal_base using - schur_szego := $hSZ:term) => - `(tactic| - exact RealRooted.pfCubicDiscrDiagonalNonnegStatement_of_schurSzego - $hSZ) - | `(tactic| rr_hadamard_pf_statement) => - `(tactic| exact RealRooted.schurPolyaWagnerHadamardPF_of_garloffWagner_nonnegStrictInterl) - | `(tactic| rr_hadamard_nonneg_realrooted_statement) => - `(tactic| exact RealRooted.garloffWagnerHadamardNonnegRealRooted_of_nonnegStrictInterl) | `(tactic| rr_schur_szego using pf_factor := $hf:term, @@ -667,57 +551,6 @@ macro_rules exact RealRooted.Tactic.schurSzegoComp_splits_of_pf_factor_natDegree_le_three_cubicNum $hn $hf $hfdeg $hpdeg $hsplits $hnum $hout) - | `(tactic| - rr_schur_szego_pf_factor_degree_le_three_diagonal_base using - diagonal_base := $hbase:term, - level_ge_three := $hn:term, - pf_factor := $hf:term, - pf_degree_le_three := $hfdeg:term, - input_degree := $hpdeg:term, - input_splits := $hsplits:term) => - `(tactic| - exact - finiteSchurSzegoComposition_of_pf_factor_le_three_of_pfCubicDiscrDiagonalNonneg - $hbase $hn $hf $hfdeg $hpdeg $hsplits) - | `(tactic| - rr_schur_szego_pf_factor_degree_le_three_diagonal_base_splits using - diagonal_base := $hbase:term, - level_ge_three := $hn:term, - pf_factor := $hf:term, - pf_degree_le_three := $hfdeg:term, - input_degree := $hpdeg:term, - input_splits := $hsplits:term, - nonzero := $hout:term) => - `(tactic| - exact - RealRooted.Tactic.schurSzegoComp_splits_of_pf_factor_degree_le_three_diagonalBase - $hbase $hn $hf $hfdeg $hpdeg $hsplits $hout) - | `(tactic| - rr_schur_szego_pf_factor_degree_le_three_diagonal_base_left_degree using - diagonal_base := $hbase:term, - pf_factor := $hf:term, - pf_degree_le_three := $hfdeg:term, - pf_degree := $hfn:term, - input_degree := $hpdeg:term, - input_splits := $hsplits:term) => - `(tactic| - exact - schurSzegoComp_zero_or_splits_of_diagonalBase_leftDegree - $hbase $hf $hfdeg $hfn $hpdeg $hsplits) - | `(tactic| - rr_schur_szego_pf_factor_degree_le_three_diagonal_base_left_degree_splits - using - diagonal_base := $hbase:term, - pf_factor := $hf:term, - pf_degree_le_three := $hfdeg:term, - pf_degree := $hfn:term, - input_degree := $hpdeg:term, - input_splits := $hsplits:term, - nonzero := $hout:term) => - `(tactic| - exact - schurSzegoComp_splits_of_pf_factor_degree_le_three_diagonalBase_leftDegree - $hbase $hf $hfdeg $hfn $hpdeg $hsplits $hout) | `(tactic| rr_schur_szego_pf_factor_degree_le_three_num_left_degree using pf_factor := $hf:term, @@ -809,10 +642,8 @@ macro_rules `(tactic| first | exact RealRooted.hadamardProduct_preserves_interl_right - RealRooted.garloffWagnerHadamardPFInterl_of_nonnegStrictInterl rr_lookup_term rr_lookup_term rr_lookup_term rr_lookup_term | exact RealRooted.hadamardProduct_preserves_interl_left - RealRooted.garloffWagnerHadamardPFInterl_of_nonnegStrictInterl rr_lookup_term rr_lookup_term rr_lookup_term rr_lookup_term | exact RealRooted.garloffWagnerHadamardPFInterl_of_nonnegStrictInterl rr_lookup_term rr_lookup_term rr_lookup_term rr_lookup_term @@ -914,10 +745,8 @@ macro_rules `(tactic| first | exact RealRooted.hadamardProduct_preserves_interl_right - RealRooted.garloffWagnerHadamardPFInterl_of_nonnegStrictInterl rr_lookup_term rr_lookup_term rr_lookup_term rr_lookup_term | exact RealRooted.hadamardProduct_preserves_interl_left - RealRooted.garloffWagnerHadamardPFInterl_of_nonnegStrictInterl rr_lookup_term rr_lookup_term rr_lookup_term rr_lookup_term | exact RealRooted.garloffWagnerHadamardPFInterl_of_nonnegStrictInterl rr_lookup_term rr_lookup_term rr_lookup_term rr_lookup_term diff --git a/RealRooted/Tactic/HermiteBiehler.lean b/RealRooted/Tactic/HermiteBiehler.lean index 667f591c4..d33f325de 100644 --- a/RealRooted/Tactic/HermiteBiehler.lean +++ b/RealRooted/Tactic/HermiteBiehler.lean @@ -68,15 +68,6 @@ theorem hermiteBiehlerOddEven_isHurwitzStable_sequence {P Q : Nat → ℝ[X]} ∀ n : Nat, IsHurwitzStable (oddEvenPolynomial (P n) (Q n)) := fun n => hermiteBiehlerOddEven_isHurwitzStable (hP n) (hQ n) (hstable n) -syntax (name := rr_hermite_biehler_forward_pos_statement_named) - "rr_hermite_biehler_forward_pos_statement" : tactic - -syntax (name := rr_hermite_biehler_converse_statement_named) - "rr_hermite_biehler_converse_statement" : tactic - -syntax (name := rr_hermite_biehler_odd_even_hurwitz_statement_named) - "rr_hermite_biehler_odd_even_hurwitz_statement" : tactic - syntax (name := rr_hermite_biehler_forward_pos_named) "rr_hermite_biehler_forward_pos" " using " "real_pos_lc" ":=" term "," @@ -164,19 +155,6 @@ syntax (name := rr_hermite_biehler_odd_even_hurwitz_stable_sequence_named) tactic macro_rules - | `(tactic| rr_hermite_biehler_forward_pos_statement) => - `(tactic| - exact fun {f g} hf hg hstrictInterl => - RealRooted.hermiteBiehlerForwardPos (f := f) (g := g) hf hg hstrictInterl) - | `(tactic| rr_hermite_biehler_converse_statement) => - `(tactic| - exact fun {f g} hf hg hstable => - RealRooted.hermiteBiehlerConverse (f := f) (g := g) hf hg hstable) - | `(tactic| rr_hermite_biehler_odd_even_hurwitz_statement) => - `(tactic| - exact fun {p q} hp hq hstable => - RealRooted.hermiteBiehlerStableToHurwitzOddEven - (p := p) (q := q) hp hq hstable) | `(tactic| rr_hermite_biehler_forward_pos using real_pos_lc := $hf:term, diff --git a/RealRooted/ThresholdMatrix/GustafssonSolus.lean b/RealRooted/ThresholdMatrix/GustafssonSolus.lean index eec7b649f..d6db3302d 100644 --- a/RealRooted/ThresholdMatrix/GustafssonSolus.lean +++ b/RealRooted/ThresholdMatrix/GustafssonSolus.lean @@ -13,7 +13,7 @@ noncomputable section namespace RealRooted -/-! ## Gustafsson--Solus Lemma 3.4 backend -/ +/-! ## Gustafsson--Solus Lemma 3.4 -/ namespace GustafssonSolus @@ -225,22 +225,16 @@ lemma gsChoice_delete_global_of_local {choices : List (ℕ × Bool)} simpa using hmain le_rfl /-- The finite entrywise Gustafsson--Solus `2 x 2` threshold check. -/ -def GSEntryHas2x2Statement : Prop := - ∀ {t₁ t₂ j₁ j₂ : ℕ} {α₁ α₂ : ℝ[X]}, - (α₁ = 0 ∨ α₁ = 1) → - (α₂ = 0 ∨ α₂ = 1) → - t₁ ≤ t₂ → j₁ ≤ j₂ → - (t₁ = t₂ → α₁ = 0 → α₂ = 0) → +theorem gsEntry_has2x2 {t₁ t₂ j₁ j₂ : ℕ} {α₁ α₂ : ℝ[X]} + (hα₁ : α₁ = 0 ∨ α₁ = 1) (hα₂ : α₂ = 0 ∨ α₂ = 1) + (ht : t₁ ≤ t₂) (hj : j₁ ≤ j₂) (hcompat : t₁ = t₂ → α₁ = 0 → α₂ = 0) : Has2x2InterlacingProperty0 (thresholdEntry t₁ α₁ j₁) (thresholdEntry t₁ α₁ j₂) - (thresholdEntry t₂ α₂ j₁) (thresholdEntry t₂ α₂ j₂) - -theorem gsEntry_has2x2 : GSEntryHas2x2Statement := by - intro t₁ t₂ j₁ j₂ α₁ α₂ hα₁ hα₂ ht hj hcompat - exact (gsEntry_shape hα₁ hα₂ ht hj hcompat).has2x2 + (thresholdEntry t₂ α₂ j₁) (thresholdEntry t₂ α₂ j₂) := + (gsEntry_shape hα₁ hα₂ ht hj hcompat).has2x2 lemma GSData.entry_has2x2 {q : ℕ} {rows : List (ℕ × ℝ[X])} - (hrows : GSData rows) (hentry : GSEntryHas2x2Statement) : + (hrows : GSData rows) : ∀ (i₁ i₂ : Fin rows.length) (j₁ j₂ : Fin q), i₁ ≤ i₂ → j₁ ≤ j₂ → Has2x2InterlacingProperty0 @@ -249,43 +243,22 @@ lemma GSData.entry_has2x2 {q : ℕ} {rows : List (ℕ × ℝ[X])} (thresholdEntry (rows.get i₂).1 (rows.get i₂).2 j₁.1) (thresholdEntry (rows.get i₂).1 (rows.get i₂).2 j₂.1) := by intro i₁ i₂ j₁ j₂ hi hj - exact hentry + exact gsEntry_has2x2 (hrows.alpha_mem (rows.get i₁) (List.get_mem rows i₁)) (hrows.alpha_mem (rows.get i₂) (List.get_mem rows i₂)) (hrows.thresh_mono i₁ i₂ hi) hj (hrows.compat i₁ i₂ hi) -/-- Gustafsson--Solus threshold-recursion backend, reduced to the finite -entrywise `2 x 2` threshold check. -/ -theorem gustafsson_solus_interlacing_recursion_backend - (hentry : GSEntryHas2x2Statement) - {q : ℕ} (rows : List (ℕ × ℝ[X])) (hrows : GSData rows) - (fs : List ℝ[X]) (hfs_len : fs.length = q) - (hfs : IsInterlacingSeqNonneg fs) : - IsInterlacingSeq0Nonneg (matPolyAction (thresholdMatrix q rows) fs) := - thresholdMatrix_preserves_interlacing_seq0_of_entry rows - hrows.alpha_nonneg (hrows.entry_has2x2 hentry) fs hfs_len hfs - +/-- Gustafsson--Solus threshold recursion: threshold matrices preserve +nonnegative interlacing sequences. -/ theorem gustafsson_solus_interlacing_recursion {q : ℕ} (rows : List (ℕ × ℝ[X])) (hrows : GSData rows) (fs : List ℝ[X]) (hfs_len : fs.length = q) (hfs : IsInterlacingSeqNonneg fs) : IsInterlacingSeq0Nonneg (matPolyAction (thresholdMatrix q rows) fs) := - gustafsson_solus_interlacing_recursion_backend gsEntry_has2x2 - rows hrows fs hfs_len hfs - -theorem gustafsson_solus_interlacing_recursion_backend_weak - (hentry : GSEntryHas2x2Statement) - {q : ℕ} (rows : List (ℕ × ℝ[X])) (hrows : GSData rows) - (fs : List ℝ[X]) (hfs_len : fs.length = q) - (hfs : IsInterlacingSeq0Nonneg fs) - (hfs_real : ∀ f ∈ fs, f ≠ 0 → (f ≠ 0 ∧ f.Splits)) : - IsInterlacingSeq0Nonneg (matPolyAction (thresholdMatrix q rows) fs) ∧ - ∀ f ∈ matPolyAction (thresholdMatrix q rows) fs, - f ≠ 0 → (f ≠ 0 ∧ f.Splits) := - thresholdMatrix_preserves_interlacing_seq0_of_entry_weak rows - hrows.alpha_nonneg (hrows.entry_has2x2 hentry) fs hfs_len hfs hfs_real + thresholdMatrix_preserves_interlacing_seq0_of_entry rows + hrows.alpha_nonneg hrows.entry_has2x2 fs hfs_len hfs theorem gustafsson_solus_interlacing_recursion_weak {q : ℕ} (rows : List (ℕ × ℝ[X])) (hrows : GSData rows) @@ -295,8 +268,8 @@ theorem gustafsson_solus_interlacing_recursion_weak IsInterlacingSeq0Nonneg (matPolyAction (thresholdMatrix q rows) fs) ∧ ∀ f ∈ matPolyAction (thresholdMatrix q rows) fs, f ≠ 0 → (f ≠ 0 ∧ f.Splits) := - gustafsson_solus_interlacing_recursion_backend_weak gsEntry_has2x2 - rows hrows fs hfs_len hfs hfs_real + thresholdMatrix_preserves_interlacing_seq0_of_entry_weak rows + hrows.alpha_nonneg hrows.entry_has2x2 fs hfs_len hfs hfs_real theorem gustafsson_solus_interlacing_recursion_choices {q : ℕ} (choices : List (ℕ × Bool)) diff --git a/RealRooted/ThresholdMatrix/HaglundZhang.lean b/RealRooted/ThresholdMatrix/HaglundZhang.lean index 874f4ecf1..1ab113c80 100644 --- a/RealRooted/ThresholdMatrix/HaglundZhang.lean +++ b/RealRooted/ThresholdMatrix/HaglundZhang.lean @@ -4,7 +4,7 @@ import RealRooted.ThresholdMatrix.Basic # Haglund--Zhang threshold matrices and OEIS A046802 The `1`/`1 + X` threshold-entry classification, its matrix-preservation -backend, the binomial Eulerian recursion, and the sequence-facing A046802 +theorem, the binomial Eulerian recursion, and the sequence-facing A046802 surface. -/ @@ -14,7 +14,7 @@ noncomputable section namespace RealRooted -/-! ## Haglund--Zhang / A046802 backend -/ +/-! ## Haglund--Zhang / A046802 -/ namespace OEIS namespace Backend @@ -549,22 +549,16 @@ private lemma hzEntry_shape lia /-- The finite entrywise Haglund--Zhang `2 x 2` threshold check. -/ -def HZEntryHas2x2Statement : Prop := - ∀ {t₁ t₂ j₁ j₂ : ℕ} {α₁ α₂ : ℝ[X]}, - (α₁ = 1 ∨ α₁ = 1 + X) → - (α₂ = 1 ∨ α₂ = 1 + X) → - t₁ ≤ t₂ → j₁ ≤ j₂ → - (t₁ = t₂ → α₁ = 1 + X → α₂ = 1 + X) → +theorem hzEntry_has2x2 {t₁ t₂ j₁ j₂ : ℕ} {α₁ α₂ : ℝ[X]} + (hα₁ : α₁ = 1 ∨ α₁ = 1 + X) (hα₂ : α₂ = 1 ∨ α₂ = 1 + X) + (ht : t₁ ≤ t₂) (hj : j₁ ≤ j₂) (hcompat : t₁ = t₂ → α₁ = 1 + X → α₂ = 1 + X) : Has2x2InterlacingProperty0 (hzEntry t₁ α₁ j₁) (hzEntry t₁ α₁ j₂) - (hzEntry t₂ α₂ j₁) (hzEntry t₂ α₂ j₂) - -theorem hzEntry_has2x2 : HZEntryHas2x2Statement := by - intro t₁ t₂ j₁ j₂ α₁ α₂ hα₁ hα₂ ht hj hcompat - exact (hzEntry_shape hα₁ hα₂ ht hj hcompat).has2x2 + (hzEntry t₂ α₂ j₁) (hzEntry t₂ α₂ j₂) := + (hzEntry_shape hα₁ hα₂ ht hj hcompat).has2x2 lemma HZData.entry_has2x2 {q : ℕ} {rows : List (ℕ × ℝ[X])} - (hrows : HZData rows) (hentry : HZEntryHas2x2Statement) : + (hrows : HZData rows) : ∀ (i₁ i₂ : Fin rows.length) (j₁ j₂ : Fin q), i₁ ≤ i₂ → j₁ ≤ j₂ → Has2x2InterlacingProperty0 @@ -573,43 +567,22 @@ lemma HZData.entry_has2x2 {q : ℕ} {rows : List (ℕ × ℝ[X])} (hzEntry (rows.get i₂).1 (rows.get i₂).2 j₁.1) (hzEntry (rows.get i₂).1 (rows.get i₂).2 j₂.1) := by intro i₁ i₂ j₁ j₂ hi hj - exact hentry + exact hzEntry_has2x2 (hrows.alpha_mem (rows.get i₁) (List.get_mem rows i₁)) (hrows.alpha_mem (rows.get i₂) (List.get_mem rows i₂)) (hrows.thresh_mono i₁ i₂ hi) hj (hrows.compat i₁ i₂ hi) -/-- Haglund--Zhang threshold matrices preserve interlacing once the finite -entrywise `2 x 2` check is available. -/ -theorem haglund_zhang_s_inversion_interlacing_backend - (hentry : HZEntryHas2x2Statement) - {q : ℕ} (rows : List (ℕ × ℝ[X])) (hrows : HZData rows) - (fs : List ℝ[X]) (hfs_len : fs.length = q) - (hfs : IsInterlacingSeqNonneg fs) : - IsInterlacingSeq0Nonneg (matPolyAction (hzMatrix q rows) fs) := - thresholdMatrix_preserves_interlacing_seq0_of_entry rows - hrows.alpha_nonneg (hrows.entry_has2x2 hentry) fs hfs_len hfs - +/-- Haglund--Zhang threshold matrices preserve nonnegative interlacing +sequences. -/ theorem haglund_zhang_s_inversion_interlacing {q : ℕ} (rows : List (ℕ × ℝ[X])) (hrows : HZData rows) (fs : List ℝ[X]) (hfs_len : fs.length = q) (hfs : IsInterlacingSeqNonneg fs) : IsInterlacingSeq0Nonneg (matPolyAction (hzMatrix q rows) fs) := - haglund_zhang_s_inversion_interlacing_backend hzEntry_has2x2 - rows hrows fs hfs_len hfs - -theorem haglund_zhang_s_inversion_interlacing_backend_weak - (hentry : HZEntryHas2x2Statement) - {q : ℕ} (rows : List (ℕ × ℝ[X])) (hrows : HZData rows) - (fs : List ℝ[X]) (hfs_len : fs.length = q) - (hfs : IsInterlacingSeq0Nonneg fs) - (hfs_real : ∀ f ∈ fs, f ≠ 0 → (f ≠ 0 ∧ f.Splits)) : - IsInterlacingSeq0Nonneg (matPolyAction (hzMatrix q rows) fs) ∧ - ∀ f ∈ matPolyAction (hzMatrix q rows) fs, - f ≠ 0 → (f ≠ 0 ∧ f.Splits) := - thresholdMatrix_preserves_interlacing_seq0_of_entry_weak rows - hrows.alpha_nonneg (hrows.entry_has2x2 hentry) fs hfs_len hfs hfs_real + thresholdMatrix_preserves_interlacing_seq0_of_entry rows + hrows.alpha_nonneg hrows.entry_has2x2 fs hfs_len hfs theorem haglund_zhang_s_inversion_interlacing_weak {q : ℕ} (rows : List (ℕ × ℝ[X])) (hrows : HZData rows) @@ -619,11 +592,10 @@ theorem haglund_zhang_s_inversion_interlacing_weak IsInterlacingSeq0Nonneg (matPolyAction (hzMatrix q rows) fs) ∧ ∀ f ∈ matPolyAction (hzMatrix q rows) fs, f ≠ 0 → (f ≠ 0 ∧ f.Splits) := - haglund_zhang_s_inversion_interlacing_backend_weak hzEntry_has2x2 - rows hrows fs hfs_len hfs hfs_real + thresholdMatrix_preserves_interlacing_seq0_of_entry_weak rows + hrows.alpha_nonneg hrows.entry_has2x2 fs hfs_len hfs hfs_real -theorem haglund_zhang_s_inversion_sum_realRooted_backend - (hentry : HZEntryHas2x2Statement) +theorem haglund_zhang_s_inversion_sum_realRooted {q : ℕ} (rows : List (ℕ × ℝ[X])) (hrows : HZData rows) (fs : List ℝ[X]) (hfs_len : fs.length = q) (hfs : IsInterlacingSeq0Nonneg fs) @@ -632,43 +604,22 @@ theorem haglund_zhang_s_inversion_sum_realRooted_backend (matPolyAction (hzMatrix q rows) fs).sum ≠ 0 ∧ ((matPolyAction (hzMatrix q rows) fs).sum).Splits := by have hout := - haglund_zhang_s_inversion_interlacing_backend_weak hentry + haglund_zhang_s_inversion_interlacing_weak rows hrows fs hfs_len hfs hfs_real exact isRealRooted_sum_of_isInterlacingSeq0Nonneg hout.1 hout.2 hsum_ne -theorem haglund_zhang_s_inversion_sum_realRooted - {q : ℕ} (rows : List (ℕ × ℝ[X])) (hrows : HZData rows) - (fs : List ℝ[X]) (hfs_len : fs.length = q) - (hfs : IsInterlacingSeq0Nonneg fs) - (hfs_real : ∀ f ∈ fs, f ≠ 0 → (f ≠ 0 ∧ f.Splits)) - (hsum_ne : (matPolyAction (hzMatrix q rows) fs).sum ≠ 0) : - (matPolyAction (hzMatrix q rows) fs).sum ≠ 0 ∧ - ((matPolyAction (hzMatrix q rows) fs).sum).Splits := - haglund_zhang_s_inversion_sum_realRooted_backend hzEntry_has2x2 - rows hrows fs hfs_len hfs hfs_real hsum_ne - -theorem haglund_zhang_terminal_polynomial_realRooted_backend - (hentry : HZEntryHas2x2Statement) +theorem haglund_zhang_terminal_polynomial_realRooted {q : ℕ} (fs : List ℝ[X]) (hfs_len : fs.length = q) (hfs : IsInterlacingSeq0Nonneg fs) (hfs_real : ∀ f ∈ fs, f ≠ 0 → (f ≠ 0 ∧ f.Splits)) (hterminal_ne : hzTerminalPolynomial q fs ≠ 0) : hzTerminalPolynomial q fs ≠ 0 ∧ (hzTerminalPolynomial q fs).Splits := by have hout := - haglund_zhang_s_inversion_interlacing_backend_weak hentry + haglund_zhang_s_inversion_interlacing_weak hzTerminalRows hzTerminalRows_data fs hfs_len hfs hfs_real exact hout.2 (hzTerminalPolynomial q fs) (hzTerminalPolynomial_mem_matPolyAction q fs) hterminal_ne -theorem haglund_zhang_terminal_polynomial_realRooted - {q : ℕ} (fs : List ℝ[X]) (hfs_len : fs.length = q) - (hfs : IsInterlacingSeq0Nonneg fs) - (hfs_real : ∀ f ∈ fs, f ≠ 0 → (f ≠ 0 ∧ f.Splits)) - (hterminal_ne : hzTerminalPolynomial q fs ≠ 0) : - hzTerminalPolynomial q fs ≠ 0 ∧ (hzTerminalPolynomial q fs).Splits := - haglund_zhang_terminal_polynomial_realRooted_backend hzEntry_has2x2 - fs hfs_len hfs hfs_real hterminal_ne - theorem haglund_zhang_terminal_polynomial_realRooted_of_interlacing {q : ℕ} (fs : List ℝ[X]) (hfs_len : fs.length = q) (hfs : IsInterlacingSeqNonneg fs) @@ -679,17 +630,6 @@ theorem haglund_zhang_terminal_polynomial_realRooted_of_interlacing fs hfs_len hfs_weak.1 hfs_weak.2 hterminal_ne /-- Binomial Eulerian specialization: all diagonal markers are `1 + X`. -/ -theorem haglund_zhang_binomial_eulerian_backend - (hentry : HZEntryHas2x2Statement) - {q : ℕ} (ts : List ℕ) - (hmono : ∀ i j : Fin ts.length, i ≤ j → ts.get i ≤ ts.get j) - (fs : List ℝ[X]) (hfs_len : fs.length = q) - (hfs : IsInterlacingSeqNonneg fs) : - IsInterlacingSeq0Nonneg - (matPolyAction (hzBinomialMatrix q ts) fs) := - haglund_zhang_s_inversion_interlacing_backend hentry _ - (hzBinomialRows_data hmono) fs hfs_len hfs - theorem haglund_zhang_binomial_eulerian {q : ℕ} (ts : List ℕ) (hmono : ∀ i j : Fin ts.length, i ≤ j → ts.get i ≤ ts.get j) @@ -697,8 +637,8 @@ theorem haglund_zhang_binomial_eulerian (hfs : IsInterlacingSeqNonneg fs) : IsInterlacingSeq0Nonneg (matPolyAction (hzBinomialMatrix q ts) fs) := - haglund_zhang_binomial_eulerian_backend hzEntry_has2x2 - ts hmono fs hfs_len hfs + haglund_zhang_s_inversion_interlacing _ + (hzBinomialRows_data hmono) fs hfs_len hfs theorem haglund_zhang_binomial_eulerian_range {q n : ℕ} (fs : List ℝ[X]) (hfs_len : fs.length = q) @@ -708,20 +648,6 @@ theorem haglund_zhang_binomial_eulerian_range haglund_zhang_binomial_eulerian (hzBinomialThresholds n) (hzBinomialThresholds_mono n) fs hfs_len hfs -theorem haglund_zhang_binomial_eulerian_backend_weak - (hentry : HZEntryHas2x2Statement) - {q : ℕ} (ts : List ℕ) - (hmono : ∀ i j : Fin ts.length, i ≤ j → ts.get i ≤ ts.get j) - (fs : List ℝ[X]) (hfs_len : fs.length = q) - (hfs : IsInterlacingSeq0Nonneg fs) - (hfs_real : ∀ f ∈ fs, f ≠ 0 → (f ≠ 0 ∧ f.Splits)) : - IsInterlacingSeq0Nonneg - (matPolyAction (hzBinomialMatrix q ts) fs) ∧ - ∀ f ∈ matPolyAction (hzBinomialMatrix q ts) fs, - f ≠ 0 → (f ≠ 0 ∧ f.Splits) := - haglund_zhang_s_inversion_interlacing_backend_weak hentry - _ (hzBinomialRows_data hmono) fs hfs_len hfs hfs_real - theorem haglund_zhang_binomial_eulerian_weak {q : ℕ} (ts : List ℕ) (hmono : ∀ i j : Fin ts.length, i ≤ j → ts.get i ≤ ts.get j) @@ -732,8 +658,8 @@ theorem haglund_zhang_binomial_eulerian_weak (matPolyAction (hzBinomialMatrix q ts) fs) ∧ ∀ f ∈ matPolyAction (hzBinomialMatrix q ts) fs, f ≠ 0 → (f ≠ 0 ∧ f.Splits) := - haglund_zhang_binomial_eulerian_backend_weak hzEntry_has2x2 - ts hmono fs hfs_len hfs hfs_real + haglund_zhang_s_inversion_interlacing_weak + _ (hzBinomialRows_data hmono) fs hfs_len hfs hfs_real theorem haglund_zhang_binomial_eulerian_range_weak {q n : ℕ} (fs : List ℝ[X]) (hfs_len : fs.length = q) @@ -747,8 +673,7 @@ theorem haglund_zhang_binomial_eulerian_range_weak (hzBinomialThresholds n) (hzBinomialThresholds_mono n) fs hfs_len hfs hfs_real -theorem haglund_zhang_binomial_eulerian_sum_realRooted_backend - (hentry : HZEntryHas2x2Statement) +theorem haglund_zhang_binomial_eulerian_sum_realRooted {q : ℕ} (ts : List ℕ) (hmono : ∀ i j : Fin ts.length, i ≤ j → ts.get i ≤ ts.get j) (fs : List ℝ[X]) (hfs_len : fs.length = q) @@ -759,23 +684,10 @@ theorem haglund_zhang_binomial_eulerian_sum_realRooted_backend (matPolyAction (hzBinomialMatrix q ts) fs).sum ≠ 0 ∧ ((matPolyAction (hzBinomialMatrix q ts) fs).sum).Splits := by have hout := - haglund_zhang_binomial_eulerian_backend_weak hentry + haglund_zhang_binomial_eulerian_weak ts hmono fs hfs_len hfs hfs_real exact isRealRooted_sum_of_isInterlacingSeq0Nonneg hout.1 hout.2 hsum_ne -theorem haglund_zhang_binomial_eulerian_sum_realRooted - {q : ℕ} (ts : List ℕ) - (hmono : ∀ i j : Fin ts.length, i ≤ j → ts.get i ≤ ts.get j) - (fs : List ℝ[X]) (hfs_len : fs.length = q) - (hfs : IsInterlacingSeq0Nonneg fs) - (hfs_real : ∀ f ∈ fs, f ≠ 0 → (f ≠ 0 ∧ f.Splits)) - (hsum_ne : - (matPolyAction (hzBinomialMatrix q ts) fs).sum ≠ 0) : - (matPolyAction (hzBinomialMatrix q ts) fs).sum ≠ 0 ∧ - ((matPolyAction (hzBinomialMatrix q ts) fs).sum).Splits := - haglund_zhang_binomial_eulerian_sum_realRooted_backend hzEntry_has2x2 - ts hmono fs hfs_len hfs hfs_real hsum_ne - theorem haglund_zhang_binomial_eulerian_range_sum_realRooted {q n : ℕ} (fs : List ℝ[X]) (hfs_len : fs.length = q) (hfs : IsInterlacingSeq0Nonneg fs) diff --git a/RealRooted/VeroneseSection.lean b/RealRooted/VeroneseSection.lean index 8794ea446..dfefce380 100644 --- a/RealRooted/VeroneseSection.lean +++ b/RealRooted/VeroneseSection.lean @@ -552,36 +552,8 @@ theorem fullyInterlacingPair_veronesePairSectionPolynomial_coeff The row order of `lacePair` is reversed relative to the polynomial-to-Lace direction: the strictly interlacing nonnegative pair `X + 2`, `X + 1` has a -negative `2 × 2` Lace minor. The propositions carrying a `Legacy` prefix record -that refuted orientation and sit beside their checked negations. -/ - -/-- Polynomial-to-Lace implication in the historical row orientation. It is -false; see `not_legacyNonnegStrictInterlToFullyInterlacingPairStatement`. It is -kept only because `RealRooted.Hadamard.Consequences` still mentions it. -/ -def LegacyNonnegStrictInterlToFullyInterlacingPairStatement : Prop := - ∀ {p q : ℝ[X]}, - HasNonnegCoeffs p → - HasNonnegCoeffs q → - StrictInterl p q → - FullyInterlacingPair p.coeff q.coeff - -/-- Nonnegative-coefficient Hurwitz odd/even implication. It is proved as -`isHurwitzStable_oddEvenPolynomial_of_strictInterl`; the proposition is kept -only because `RealRooted.Hadamard.Consequences` still mentions it. -/ -def NonnegStrictInterlToHurwitzOddEvenStatement : Prop := - ∀ ⦃p q : ℝ[X]⦄, - HasNonnegCoeffs p → - HasNonnegCoeffs q → - StrictInterl p q → - IsHurwitzStable (oddEvenPolynomial p q) - -/-- Hurwitz-to-Lace implication in the historical row orientation. It is -false; see `not_hurwitzOddEvenToFullyInterlacingPairStatement`. It is kept -only because `RealRooted.Hadamard.Consequences` still mentions it. -/ -def LegacyHurwitzOddEvenToFullyInterlacingPairStatement : Prop := - ∀ ⦃p q : ℝ[X]⦄, - IsHurwitzStable (oddEvenPolynomial p q) → - FullyInterlacingPair p.coeff q.coeff +negative `2 × 2` Lace minor. The negations below record that refuted +orientation. -/ /-- Unproved target: Hurwitz stability of `q(x^2) + x p(x^2)` makes the reversed two-row Lace matrix of `q` and `p` totally nonnegative. -/ @@ -605,9 +577,14 @@ private theorem strictInterl_X_add_C_two_one : StrictInterl (X + C (2 : ℝ)) (X rw [StrictInterl.X_add_C_iff] norm_num -/-- `LegacyNonnegStrictInterlToFullyInterlacingPairStatement` is false as stated. -/ -theorem not_legacyNonnegStrictInterlToFullyInterlacingPairStatement : - ¬ LegacyNonnegStrictInterlToFullyInterlacingPairStatement := by +/-- In the historical row orientation, strict interlacing of nonnegative +polynomials does not make their two-row Lace matrix totally nonnegative. -/ +theorem not_nonnegStrictInterl_fullyInterlacingPair : + ¬ ∀ {p q : ℝ[X]}, + HasNonnegCoeffs p → + HasNonnegCoeffs q → + StrictInterl p q → + FullyInterlacingPair p.coeff q.coeff := by intro h have hpnn : HasNonnegCoeffs (X + C (2 : ℝ)) := hasNonnegCoeffs_X_add_C (by norm_num) @@ -628,11 +605,13 @@ theorem isHurwitzStable_oddEvenPolynomial_of_strictInterl {p q : ℝ[X]} (hermiteBiehlerForwardPos (hqnn.pos_leadingCoeff hpq.2.1.1) (hpnn.pos_leadingCoeff hpq.1.1) hpq)⟩ -/-- `LegacyHurwitzOddEvenToFullyInterlacingPairStatement` is false for the -current row-oriented Lace matrix. -/ -theorem not_hurwitzOddEvenToFullyInterlacingPairStatement : - ¬ LegacyHurwitzOddEvenToFullyInterlacingPairStatement := fun h => - not_legacyNonnegStrictInterlToFullyInterlacingPairStatement fun hpnn hqnn hpq => +/-- Hurwitz stability of `q(x^2) + x p(x^2)` does not make the current +row-oriented Lace matrix of `p` and `q` totally nonnegative. -/ +theorem not_isHurwitzStable_oddEven_fullyInterlacingPair : + ¬ ∀ ⦃p q : ℝ[X]⦄, + IsHurwitzStable (oddEvenPolynomial p q) → + FullyInterlacingPair p.coeff q.coeff := fun h => + not_nonnegStrictInterl_fullyInterlacingPair fun hpnn hqnn hpq => h (isHurwitzStable_oddEvenPolynomial_of_strictInterl hpnn hqnn hpq) /-- The forward Hurwitz-matrix criterion is false for the row orientation used @@ -640,28 +619,10 @@ by `hurwitz`: Hurwitz stability does not force the row-oriented Hurwitz matrix to be totally nonnegative. -/ theorem not_forall_isHurwitzStable_hurwitz_isTotallyNonneg : ¬ ∀ ⦃p : ℝ[X]⦄, IsHurwitzStable p → (hurwitz p.coeff).IsTotallyNonneg := fun h => - not_legacyNonnegStrictInterlToFullyInterlacingPairStatement fun hpnn hqnn hpq => + not_nonnegStrictInterl_fullyInterlacingPair fun hpnn hqnn hpq => (hurwitzMatrixTotallyNonnegative_oddEvenPolynomial_iff_fullyInterlacingPair _ _).1 (h (isHurwitzStable_oddEvenPolynomial_of_strictInterl hpnn hqnn hpq)) -/-- Unproved Lace-to-polynomial interface in the historical row orientation. -It is kept only because `RealRooted.Hadamard.Consequences` still mentions it. -It is expected to be false: numerically `lacePair (X + 1).coeff (X + 2).coeff` -has no negative minor, while `Interl (X + 1) (X + 2)` fails. -/ -def FullyInterlacingPairToInterlStatement : Prop := - ∀ {p q : ℝ[X]}, - FullyInterlacingPair p.coeff q.coeff → Interl p q - -/-- Lace-to-Hurwitz interface in the historical row orientation. It is kept -only because `RealRooted.HurwitzMatrix` still mentions it. It is expected to -be false: numerically `lacePair (X + 1).coeff (X + 2).coeff` has no negative -minor, while `X^3 + X^2 + X + 2` is not Hurwitz stable. -/ -def LegacyFullyInterlacingPairToHurwitzOddEvenStableStatement : Prop := - ∀ ⦃p q : ℝ[X]⦄, - p ≠ 0 ∨ q ≠ 0 → - FullyInterlacingPair p.coeff q.coeff → - IsHurwitzStable (oddEvenPolynomial p q) - /-! ## Converse Hermite--Biehler step for odd/even polynomials -/ /-- Unproved target: converse of the conformal substitution