From f159c828b9c598bb41a541c9ad5e2faab0563bd5 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Fri, 2 Oct 2026 14:36:11 +0000 Subject: [PATCH 1/4] Restate proved Garloff-Wagner, Hermite-Biehler, Obreschkoff and threshold-matrix results directly Drop the Statement wrappers whose witnesses are proved, the backend variants that only take a proved statement as hypothesis, and the unused weighted-expansion and Schur double-deleted routes. Co-Authored-By: Claude Opus 5.5 --- .../Stability/Rotation.lean | 2 +- RealRooted/GarloffWagner/Hadamard.lean | 68 ++----- RealRooted/GarloffWagner/Iterated.lean | 149 ++++----------- RealRooted/GarloffWagner/KreinExpansion.lean | 44 ++--- RealRooted/GarloffWagner/Theorem12.lean | 99 ++++------ RealRooted/HermiteBiehler/Basic.lean | 2 +- RealRooted/HermiteBiehler/Converse.lean | 9 +- RealRooted/HermiteBiehler/Forward.lean | 9 +- RealRooted/HermiteBiehler/Hurwitz.lean | 175 +++++++----------- .../ObreschkoffConverse/Derivative.lean | 156 ++++------------ .../ObreschkoffConverse/Regularization.lean | 6 +- .../ThresholdMatrix/GustafssonSolus.lean | 55 ++---- RealRooted/ThresholdMatrix/HaglundZhang.lean | 138 +++----------- 13 files changed, 255 insertions(+), 657 deletions(-) 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/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..39f07a7db 100644 --- a/RealRooted/HermiteBiehler/Converse.lean +++ b/RealRooted/HermiteBiehler/Converse.lean @@ -15,11 +15,10 @@ 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 --/ +/-- Proposition form of the converse Hermite--Biehler theorem +`hermiteBiehlerConverse`: upper-half-plane stability of `f + i g` forces an +interlacing relation between `f` and `g`. It is kept for callers that take the +theorem as a hypothesis. -/ abbrev hermiteBiehlerConverseStatement : Prop := ∀ ⦃f g : ℝ[X]⦄, HasPosLeadingCoeff f → diff --git a/RealRooted/HermiteBiehler/Forward.lean b/RealRooted/HermiteBiehler/Forward.lean index 08fd7d8f8..e6ddf5939 100644 --- a/RealRooted/HermiteBiehler/Forward.lean +++ b/RealRooted/HermiteBiehler/Forward.lean @@ -350,11 +350,10 @@ 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. --/ +/-- Proposition form of the sign-normalized forward Hermite--Biehler theorem +`hermiteBiehlerForwardPos`. Positive leading coefficients on both inputs +exclude the sign counterexample. It is kept for callers that take the theorem +as a hypothesis. -/ abbrev hermiteBiehlerForwardPosStatement : Prop := ∀ {f g : ℝ[X]}, HasPosLeadingCoeff f → diff --git a/RealRooted/HermiteBiehler/Hurwitz.lean b/RealRooted/HermiteBiehler/Hurwitz.lean index da28beee5..4edf6a6ce 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,11 +17,10 @@ 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 --/ +/-- Proposition form of `hermiteBiehlerStableToHurwitzOddEven`: the +Hermite--Biehler stable polynomial `q + i p` gives right-half-plane stability of +`q(x^2) + x p(x^2)`. It is kept for callers that take the theorem as a +hypothesis. -/ abbrev HermiteBiehlerStableToHurwitzOddEvenStatement : Prop := ∀ ⦃p q : ℝ[X]⦄, HasNonnegCoeffs p → @@ -29,98 +28,17 @@ abbrev HermiteBiehlerStableToHurwitzOddEvenStatement : Prop := 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 +90,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/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/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) From 08be740e88edade0b7d044129eec6f0030a44ea5 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Fri, 2 Oct 2026 14:46:56 +0000 Subject: [PATCH 2/4] Retire refuted Hurwitz Schur-product tree; state Hadamard and Schur-Szego results directly The 3x3 in-band Hurwitz Schur-product cores are refuted by the same minor that refutes the infinite TN statement, so delete the statements and every reduction between them, keeping checked negations with explicit propositions. Restate the proved Schur-Szego, Polya-Schur and Garloff-Wagner PF wrappers with plain hypotheses and drop the statement-only tactics. Keep Garloff-Wagner Theorem 1 as the single open target (#1095). Co-Authored-By: Claude Opus 5.5 --- PROOF_STATUS.md | 1 + .../HurwitzCornerZeroedCounterexample.lean | 24 +- ...TotallyNonnegativeHadamardObstruction.lean | 20 +- RealRooted/Hadamard/Consequences.lean | 245 +--- RealRooted/Hadamard/Cubic.lean | 149 +- RealRooted/Hadamard/Finite.lean | 111 +- RealRooted/Hadamard/GarloffWagner.lean | 61 +- RealRooted/Hadamard/Grace.lean | 61 +- RealRooted/Hadamard/Hurwitz.lean | 221 +-- RealRooted/HurwitzMatrix.lean | 1216 ++--------------- RealRooted/Tactic/Examples/Hadamard.lean | 90 -- RealRooted/Tactic/Hadamard.lean | 171 --- 12 files changed, 273 insertions(+), 2097 deletions(-) diff --git a/PROOF_STATUS.md b/PROOF_STATUS.md index be689ece9..a974b681d 100644 --- a/PROOF_STATUS.md +++ b/PROOF_STATUS.md @@ -19,6 +19,7 @@ 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 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/Hadamard/Consequences.lean b/RealRooted/Hadamard/Consequences.lean index 03c15f1f1..3167395fb 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_sequence aissenSchoenbergWhitneyForwardOrZero hp).hadamardProduct + (IsPFPolynomial.of_sequence aissenSchoenbergWhitneyForwardOrZero 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/HurwitzMatrix.lean b/RealRooted/HurwitzMatrix.lean index 4cd7a4b89..a116f4ea1 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,109 +267,10 @@ 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 +/-! ### 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 @@ -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/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/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 From 1443021ee449c28ed09b8fa91f48291542b57ffb Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Fri, 2 Oct 2026 15:43:28 +0000 Subject: [PATCH 3/4] Wrap long docstring line Co-Authored-By: Claude Opus 5.5 --- RealRooted/HurwitzMatrix.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/RealRooted/HurwitzMatrix.lean b/RealRooted/HurwitzMatrix.lean index a116f4ea1..f727c5fb3 100644 --- a/RealRooted/HurwitzMatrix.lean +++ b/RealRooted/HurwitzMatrix.lean @@ -270,9 +270,9 @@ theorem hurwitz_schurProduct_det_fin_three_of_row1_below {a b : ℕ → ℝ} /-! ### 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. -/ +`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) : From 1a3be7cda4a5ab2972de18af9563b35b4fc4b7ad Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Fri, 2 Oct 2026 16:11:46 +0000 Subject: [PATCH 4/4] Drop Lace/Hermite-Biehler propositions left without consumers The Veronese-section Lace interfaces and the three Hermite-Biehler proposition forms were kept only for the vacuous Hadamard reductions and statement-only tactics removed here. Keep the two Lace refutations with explicit propositions. Co-Authored-By: Claude Opus 5.5 --- PROOF_STATUS.md | 13 +--- RealRooted/Hadamard/Consequences.lean | 4 +- RealRooted/HermiteBiehler/Converse.lean | 11 --- RealRooted/HermiteBiehler/Forward.lean | 11 --- RealRooted/HermiteBiehler/Hurwitz.lean | 11 --- .../Tactic/Examples/HermiteBiehler.lean | 12 --- .../Examples/OEIS/ClassicalFamilies.lean | 5 -- RealRooted/Tactic/HermiteBiehler.lean | 22 ------ RealRooted/VeroneseSection.lean | 75 +++++-------------- 9 files changed, 21 insertions(+), 143 deletions(-) diff --git a/PROOF_STATUS.md b/PROOF_STATUS.md index a974b681d..efd413aae 100644 --- a/PROOF_STATUS.md +++ b/PROOF_STATUS.md @@ -22,14 +22,6 @@ theorem, refutation, or production caller. They contain no admission. | `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 | @@ -56,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/Hadamard/Consequences.lean b/RealRooted/Hadamard/Consequences.lean index 3167395fb..c2bdedd84 100644 --- a/RealRooted/Hadamard/Consequences.lean +++ b/RealRooted/Hadamard/Consequences.lean @@ -104,8 +104,8 @@ polynomials `p` and `q`. -/ theorem polyaFrequencyHadamardCoeff {p q : ℝ[X]} (hp : IsPolyaFreqSeq p.coeff) (hq : IsPolyaFreqSeq q.coeff) : IsPolyaFreqSeq (fun n => (hadamardProduct p q).coeff n) := - ((IsPFPolynomial.of_sequence aissenSchoenbergWhitneyForwardOrZero hp).hadamardProduct - (IsPFPolynomial.of_sequence aissenSchoenbergWhitneyForwardOrZero hq)).to_sequence + ((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/HermiteBiehler/Converse.lean b/RealRooted/HermiteBiehler/Converse.lean index 39f07a7db..84babe8ef 100644 --- a/RealRooted/HermiteBiehler/Converse.lean +++ b/RealRooted/HermiteBiehler/Converse.lean @@ -15,17 +15,6 @@ noncomputable section namespace RealRooted -/-- Proposition form of the converse Hermite--Biehler theorem -`hermiteBiehlerConverse`: upper-half-plane stability of `f + i g` forces an -interlacing relation between `f` and `g`. It is kept for callers that take the -theorem as a hypothesis. -/ -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 e6ddf5939..040327393 100644 --- a/RealRooted/HermiteBiehler/Forward.lean +++ b/RealRooted/HermiteBiehler/Forward.lean @@ -350,17 +350,6 @@ theorem isUpperHalfPlaneStable_of_cofactor {f g : ℝ[X]} {r : ℝ} intro h exact hz.ne' (by simpa using congrArg Complex.im h) -/-- Proposition form of the sign-normalized forward Hermite--Biehler theorem -`hermiteBiehlerForwardPos`. Positive leading coefficients on both inputs -exclude the sign counterexample. It is kept for callers that take the theorem -as a hypothesis. -/ -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 4edf6a6ce..145298ea6 100644 --- a/RealRooted/HermiteBiehler/Hurwitz.lean +++ b/RealRooted/HermiteBiehler/Hurwitz.lean @@ -17,17 +17,6 @@ noncomputable section namespace RealRooted -/-- Proposition form of `hermiteBiehlerStableToHurwitzOddEven`: the -Hermite--Biehler stable polynomial `q + i p` gives right-half-plane stability of -`q(x^2) + x p(x^2)`. It is kept for callers that take the theorem as a -hypothesis. -/ -abbrev HermiteBiehlerStableToHurwitzOddEvenStatement : Prop := - ∀ ⦃p q : ℝ[X]⦄, - HasNonnegCoeffs p → - HasNonnegCoeffs q → - IsUpperHalfPlaneStable (hermiteBiehlerPolynomial q p) → - IsRightHalfPlaneStable (complexify (oddEvenPolynomial p q)) - /-- Upper-half-plane substitution form of the forward Hermite--Biehler/Hurwitz 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. 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/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/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