From 538e029b9fb62638432131e483f33db6e8b9e88c Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 5 Oct 2026 08:54:53 +0000 Subject: [PATCH] Remove forwarding wrapper theorems with no callers Delete 41 declarations whose proof only forwards to another declaration and which nothing in the repository or the downstream workspace projects uses: - renamed or argument-reordered duplicates (strictInterl_shift', deriv_sum_collapse, the Liu--Wang tR aliases, the Set.Iio and right-family restatements, the affine-family _nonneg aliases); - forwarders carrying hypotheses they never use (threshold sine bound, finite Polya--Schur low-degree backward cases, first Branden basis image); - fixed-index instances of normalized_coeff_nonneg_of_isPF; - one-direction halves of hasCommonInterleaver_pair and its left version, and projection aliases of structure fields; - the warmupP compatibility abbrev and its nine mirrored lemmas, and the complexifyLinearMap abbrev (its X_pow simp lemma is restated for complexificationLinearMap); - two Mathlib-folder shims that only restate their hypothesis. Co-Authored-By: Claude Opus 5.5 --- RealRooted/ASWKarlinSineBounds.lean | 7 ---- RealRooted/AffineFamily.lean | 37 ------------------- .../Applications/AffineFiniteSymbol.lean | 22 ++--------- .../SturmDerangementsExc.lean | 27 -------------- RealRooted/CommonInterleaverSeq.lean | 24 ------------ RealRooted/Compatibility/NDCutInvariant.lean | 6 --- RealRooted/Hadamard/Newton.lean | 28 -------------- RealRooted/Interlacing/Residue.lean | 18 --------- RealRooted/InterlacingSequenceBasic.lean | 5 --- RealRooted/LiuWang/Step.lean | 31 ---------------- .../Matrix/PerronFrobenius/Auxiliary.lean | 4 -- .../Matrix/PerronFrobenius/CStarClasses.lean | 3 -- RealRooted/MultiplierSequence.lean | 27 -------------- RealRooted/SameDegreeDerivative.lean | 7 ---- RealRooted/ShiftLemma.lean | 13 ------- RealRooted/SuccDegreeLeftEndpoint.lean | 10 ----- RealRooted/Tactic/PFBidiagonal.lean | 6 --- .../Transforms/BrandenE/ProperPosition.lean | 7 ---- 18 files changed, 3 insertions(+), 279 deletions(-) diff --git a/RealRooted/ASWKarlinSineBounds.lean b/RealRooted/ASWKarlinSineBounds.lean index 355b1863e..f07c7d727 100644 --- a/RealRooted/ASWKarlinSineBounds.lean +++ b/RealRooted/ASWKarlinSineBounds.lean @@ -585,11 +585,4 @@ lemma signVariations_aswKarlinSineVector_degree_one_lt hle.trans (by lia) exact Nat.lt_of_le_pred horder hle' -/-- Threshold-shaped wrapper for the degree-one sine upper bound. -/ -lemma signVariations_aswKarlinSineVector_degree_one_lt_of_lt_threshold - {θ : ℝ} {order : ℕ} (horder : 0 < order) (_hθ0 : 0 ≤ θ) - (_hθ : θ < aswSectorThreshold 1 order) : - Fin.signVariations (aswKarlinSineVector θ 1 order 1) < order := - signVariations_aswKarlinSineVector_degree_one_lt θ horder - end RealRooted diff --git a/RealRooted/AffineFamily.lean b/RealRooted/AffineFamily.lean index f664eeb39..c25d0176a 100644 --- a/RealRooted/AffineFamily.lean +++ b/RealRooted/AffineFamily.lean @@ -833,28 +833,6 @@ theorem allComboRealRooted_of_affine_family_nonneg allComboRealRooted_of_strictInterl (strictInterl_of_affine_family_nonneg hf0 hg0 hfnn hgnn haff) -/-- Public shifted-pair package extracted from a nonnegative affine family. -This is the corrected same-degree seam after the failed boundary-right-pair -target: the affine family automatically promotes the shifted pair -`(g + X * f, f)` into the clean succ-degree positive-combination regime. -/ -theorem shifted_pair_data_of_affine_family_nonneg - {f g : ℝ[X]} - (hf0 : f ≠ 0) (hg0 : g ≠ 0) - (hfnn : HasNonnegCoeffs f) - (hgnn : HasNonnegCoeffs g) - (haff : - ∀ {s t : ℝ}, 0 < s → 0 < t → - ((((C s * X + C t) * f) + g) ≠ 0 ∧ (((C s * X + C t) * f) + g).Splits)) : - PosComboRealRooted (g + X * f) f ∧ - HasNonnegCoeffs (g + X * f) ∧ - HasNonnegCoeffs f ∧ - (g + X * f) ≠ 0 ∧ - f ≠ 0 ∧ - HasPosLeadingCoeff (g + X * f) ∧ - HasPosLeadingCoeff f ∧ - (g + X * f).natDegree = f.natDegree + 1 := - affine_family_shifted_pair_data hf0 hg0 hfnn hgnn haff - /-- A nonnegative affine family already orients the shifted pair: `f ≺ g + X * f`. This is the public corrected replacement for the earlier false attempt to orient every boundary pair `(C t * f + g, X * f)`. -/ @@ -894,21 +872,6 @@ theorem strictInterl_right_pair_of_affine_family_nonneg_sameDegree (strictInterl_shifted_pair_of_affine_family_nonneg hf0 hfnn hgnn haff) hf0 hg0 hfnn hgnn hdeg -/-- Public shifted-pair reduction in the same-degree nonnegative regime: -once the corrected shifted pair satisfies `f ≺ g + X * f`, the original pair -already satisfies `f ≺ g`. This packages the internal subtraction step used in -the affine-family same-degree branch. -/ -theorem strictInterl_of_strictInterl_shifted_pair_sameDegree_nonneg - {f g : ℝ[X]} - (h : StrictInterl f (g + X * f)) - (hf0 : f ≠ 0) (hg0 : g ≠ 0) - (hfnn : HasNonnegCoeffs f) - (hgnn : HasNonnegCoeffs g) - (hdeg : g.natDegree = f.natDegree) : - StrictInterl f g := - strictInterl_of_strictInterl_shifted_pair_sameDegree - h hf0 hg0 hfnn hgnn hdeg - /-- Symmetric degree closeness for positive-combination real-rooted pairs with nonnegative coefficients. -/ theorem natDegree_close_of_posComboRealRooted_of_nonnegCoeffs diff --git a/RealRooted/BorceaBranden/Applications/AffineFiniteSymbol.lean b/RealRooted/BorceaBranden/Applications/AffineFiniteSymbol.lean index 812c4abf9..f8fae21a2 100644 --- a/RealRooted/BorceaBranden/Applications/AffineFiniteSymbol.lean +++ b/RealRooted/BorceaBranden/Applications/AffineFiniteSymbol.lean @@ -17,29 +17,13 @@ namespace RealRooted namespace BorceaBranden -/-- Compatibility name for `complexificationLinearMap`. -/ -noncomputable abbrev complexifyLinearMap - (T : ℝ[X] →ₗ[ℝ] ℝ[X]) : ℂ[X] →ₗ[ℂ] ℂ[X] := - complexificationLinearMap T - -@[simp] lemma complexifyLinearMap_monomial - (T : ℝ[X] →ₗ[ℝ] ℝ[X]) (n : ℕ) (z : ℂ) : - complexifyLinearMap T (Polynomial.monomial n z) = - C z * complexify (T (X ^ n)) := - complexificationLinearMap_monomial T n z - -@[simp] lemma complexifyLinearMap_X_pow +@[simp] lemma complexificationLinearMap_X_pow (T : ℝ[X] →ₗ[ℝ] ℝ[X]) (n : ℕ) : - complexifyLinearMap T ((X : ℂ[X]) ^ n) = + complexificationLinearMap T ((X : ℂ[X]) ^ n) = complexify (T ((X : ℝ[X]) ^ n)) := by - rw [Polynomial.X_pow_eq_monomial, complexifyLinearMap_monomial] + rw [Polynomial.X_pow_eq_monomial, complexificationLinearMap_monomial] simp -lemma complexifyLinearMap_complexify - (T : ℝ[X] →ₗ[ℝ] ℝ[X]) (p : ℝ[X]) : - complexifyLinearMap T (complexify p) = complexify (T p) := - complexificationLinearMap_complexify T p - /-- The complex degree-box bidiagonal operator is the complexification of the real bidiagonal operator on a degree-bounded real input. -/ lemma complexBidiagonalDegreeBox_value diff --git a/RealRooted/CombinatorialExamples/SturmDerangementsExc.lean b/RealRooted/CombinatorialExamples/SturmDerangementsExc.lean index 928199fdd..9b0bdd52f 100644 --- a/RealRooted/CombinatorialExamples/SturmDerangementsExc.lean +++ b/RealRooted/CombinatorialExamples/SturmDerangementsExc.lean @@ -573,31 +573,4 @@ theorem isSturmSeq_sturmDerangementsExcPrefix : simpa [sturmDerangementsExcPrefix, IsSturmSeq] using And.intro (interlaces_sturmDerangementsExc_succ (n := n + 2) (by lia)) ih -/-- Backward-compatible alias while the project transitions away from the old name. -/ -abbrev warmupP := sturmDerangementsExc - -@[simp] lemma warmupP_zero : warmupP 0 = 0 := sturmDerangementsExc_zero - -@[simp] lemma warmupP_one : warmupP 1 = 0 := sturmDerangementsExc_one - -@[simp] lemma warmupP_two : warmupP 2 = X := sturmDerangementsExc_two - -lemma warmupP_recurrence (n : Nat) : warmupP (n + 3) = - X * (((n + 2 : ℝ[X])) * warmupP (n + 1) + - ((n + 2 : ℝ[X])) * warmupP (n + 2) + - (1 - X) * (warmupP (n + 2)).derivative) := - sturmDerangementsExc_recurrence n - -lemma X_dvd_warmupP (n : Nat) : X ∣ warmupP n := - X_dvd_sturmDerangementsExc n - -lemma warmupP_isRoot_zero (n : Nat) : (warmupP n).IsRoot 0 := - sturmDerangementsExc_isRoot_zero n - -lemma warmupP_three : warmupP 3 = X ^ 2 + X := sturmDerangementsExc_three - -lemma warmupP_four : warmupP 4 = X ^ 3 + 7 * X ^ 2 + X := sturmDerangementsExc_four - -lemma warmupP_five : warmupP 5 = X ^ 4 + 21 * X ^ 3 + 21 * X ^ 2 + X := sturmDerangementsExc_five - end RealRooted diff --git a/RealRooted/CommonInterleaverSeq.lean b/RealRooted/CommonInterleaverSeq.lean index b5bf89fda..62d247b99 100644 --- a/RealRooted/CommonInterleaverSeq.lean +++ b/RealRooted/CommonInterleaverSeq.lean @@ -722,30 +722,6 @@ theorem pairHasCommonLeftInterleaver_symm {f g : ℝ[X]} obtain ⟨w, hf, hg⟩ := h exact ⟨w, hg, hf⟩ -/-- Extract the pair existential from `HasCommonInterleaver [f, g]`. -/ -theorem pairHasCommonInterleaver_of_hasCommonInterleaver_pair {f g : ℝ[X]} - (h : HasCommonInterleaver [f, g]) : - ∃ h : ℝ[X], StrictInterl f h ∧ StrictInterl g h := - hasCommonInterleaver_pair.1 h - -/-- Package the pair existential as `HasCommonInterleaver [f, g]`. -/ -theorem hasCommonInterleaver_pair_of_pairHasCommonInterleaver {f g : ℝ[X]} - (h : ∃ h : ℝ[X], StrictInterl f h ∧ StrictInterl g h) : - HasCommonInterleaver [f, g] := - hasCommonInterleaver_pair.2 h - -/-- Extract the left pair existential from `HasCommonLeftInterleaver [f, g]`. -/ -theorem pairHasCommonLeftInterleaver_of_hasCommonLeftInterleaver_pair - {f g : ℝ[X]} (h : HasCommonLeftInterleaver [f, g]) : - ∃ h : ℝ[X], StrictInterl h f ∧ StrictInterl h g := - hasCommonLeftInterleaver_pair.1 h - -/-- Package the left pair existential as `HasCommonLeftInterleaver [f, g]`. -/ -theorem hasCommonLeftInterleaver_pair_of_pairHasCommonLeftInterleaver - {f g : ℝ[X]} (h : ∃ h : ℝ[X], StrictInterl h f ∧ StrictInterl h g) : - HasCommonLeftInterleaver [f, g] := - hasCommonLeftInterleaver_pair.2 h - /-- Extract the pair existential from `PairwiseHasCommonInterleaver [f, g]`. -/ theorem pairHasCommonInterleaver_of_pairwiseHasCommonInterleaver_pair {f g : ℝ[X]} (h : PairwiseHasCommonInterleaver [f, g]) : diff --git a/RealRooted/Compatibility/NDCutInvariant.lean b/RealRooted/Compatibility/NDCutInvariant.lean index ba542dff6..75a1ce5ab 100644 --- a/RealRooted/Compatibility/NDCutInvariant.lean +++ b/RealRooted/Compatibility/NDCutInvariant.lean @@ -67,12 +67,6 @@ structure OrderedNDCutCompatible {m : ℕ} namespace OrderedNDCutCompatible -/-- Receiver-style projection to the generic P/Q cut package. -/ -theorem toOrderedCutCompatible {m : ℕ} {N D : Fin m → ℝ[X]} - (h : OrderedNDCutCompatible N D) : - OrderedCutCompatible (ndCutP N D) (ndCutQ N D) := - h.cutCompatible - /-- Every `N` coordinate has nonnegative coefficients. -/ theorem n_nonneg {m : ℕ} {N D : Fin m → ℝ[X]} (h : OrderedNDCutCompatible N D) (i : Fin m) : diff --git a/RealRooted/Hadamard/Newton.lean b/RealRooted/Hadamard/Newton.lean index 5a73026f0..e24c46ebd 100644 --- a/RealRooted/Hadamard/Newton.lean +++ b/RealRooted/Hadamard/Newton.lean @@ -287,34 +287,6 @@ theorem normalized_coeff_nonneg_of_isPF (n : ℕ) {f : ℝ[X]} div_nonneg (hf.hasNonnegCoeffs k) (by exact_mod_cast Nat.zero_le (Nat.choose n k)) -/-- Constant normalized coefficient nonnegativity for a PF polynomial at -binomial level three. -/ -theorem normalized_coeff_zero_nonneg_of_isPF_three {f : ℝ[X]} - (hf : IsPFPolynomial f) : - 0 ≤ f.coeff 0 / (Nat.choose 3 0 : ℝ) := - normalized_coeff_nonneg_of_isPF 3 hf 0 - -/-- Linear normalized coefficient nonnegativity for a PF polynomial at -binomial level three. -/ -theorem normalized_coeff_one_nonneg_of_isPF_three {f : ℝ[X]} - (hf : IsPFPolynomial f) : - 0 ≤ f.coeff 1 / (Nat.choose 3 1 : ℝ) := - normalized_coeff_nonneg_of_isPF 3 hf 1 - -/-- Quadratic normalized coefficient nonnegativity for a PF polynomial at -binomial level three. -/ -theorem normalized_coeff_two_nonneg_of_isPF_three {f : ℝ[X]} - (hf : IsPFPolynomial f) : - 0 ≤ f.coeff 2 / (Nat.choose 3 2 : ℝ) := - normalized_coeff_nonneg_of_isPF 3 hf 2 - -/-- Cubic normalized coefficient nonnegativity for a PF polynomial at binomial -level three. -/ -theorem normalized_coeff_three_nonneg_of_isPF_three {f : ℝ[X]} - (hf : IsPFPolynomial f) : - 0 ≤ f.coeff 3 / (Nat.choose 3 3 : ℝ) := - normalized_coeff_nonneg_of_isPF 3 hf 3 - /-- Normalized coefficient log-concavity of a degree-`≤ 3` PF polynomial. Writing `γ k = f.coeff k / (3.choose k)`, the adjacent cubic log-concavity diff --git a/RealRooted/Interlacing/Residue.lean b/RealRooted/Interlacing/Residue.lean index 97af7a790..b393fdb7a 100644 --- a/RealRooted/Interlacing/Residue.lean +++ b/RealRooted/Interlacing/Residue.lean @@ -18,24 +18,6 @@ namespace RealRooted /-! ## Derivative and evaluation signs -/ -theorem eval_derivative_eq_sum_real {p : ℝ[X]} (hp : p.Splits) (x : ℝ) : - p.derivative.eval x - = p.leadingCoeff * - (p.roots.map (fun r : ℝ => - ((p.roots.erase r).map (fun s : ℝ => x - s)).prod)).sum := - hp.eval_derivative x - -theorem deriv_sum_collapse (M : Multiset ℝ) (s : ℝ) (hs : s ∈ M) (hcount : M.count s = 1) : - (M.map (fun r : ℝ => ((M.erase r).map (fun t : ℝ => s - t)).prod)).sum - = ((M.erase s).map (fun t : ℝ => s - t)).prod := - derivative_sum_collapse M s hs hcount - -theorem eval_derivative_at_root {p : ℝ[X]} (hp : p.Splits) (s : ℝ) - (hs : s ∈ p.roots) (hcount : p.roots.count s = 1) : - p.derivative.eval s - = p.leadingCoeff * ((p.roots.erase s).map (fun r : ℝ => s - r)).prod := - hp.eval_derivative_at_root_of_roots_count_one s hs hcount - theorem prod_sub_sign_pos (M : Multiset ℝ) (s : ℝ) (hs : s ∉ M) : 0 < (M.map (fun r => s - r)).prod * (-1 : ℝ) ^ (M.countP (fun r => s < r)) := by induction M using Multiset.induction with diff --git a/RealRooted/InterlacingSequenceBasic.lean b/RealRooted/InterlacingSequenceBasic.lean index 8b45b9c29..6369473dd 100644 --- a/RealRooted/InterlacingSequenceBasic.lean +++ b/RealRooted/InterlacingSequenceBasic.lean @@ -282,11 +282,6 @@ def IsInterlacingSeq0NonnegRealRooted (fs : List ℝ[X]) : Prop := namespace IsInterlacingSeq0NonnegRealRooted -lemma interlacingSeq0Nonneg {fs : List ℝ[X]} - (hfs : IsInterlacingSeq0NonnegRealRooted fs) : - IsInterlacingSeq0Nonneg fs := - hfs.1 - lemma interlacingSeq0 {fs : List ℝ[X]} (hfs : IsInterlacingSeq0NonnegRealRooted fs) : IsInterlacingSeq0 fs := diff --git a/RealRooted/LiuWang/Step.lean b/RealRooted/LiuWang/Step.lean index 925502d05..d7ff2889c 100644 --- a/RealRooted/LiuWang/Step.lean +++ b/RealRooted/LiuWang/Step.lean @@ -285,37 +285,6 @@ theorem strictInterl_lw_positive_C_mul_X_mul_lag_of_nonneg_coeffs (roots_nonpos_of_interlaces_of_nonneg_coeffs hgf hf_nonneg) hc hq_nonneg hF_pos hdeg_lo hdeg_hi hno -/-- Family E `t R(t)` Liu--Wang step with an explicit half-line root -certificate. This is a named alias for the existing `X * q` product-lag -wrapper, using `q` as the factor `R`. -/ -theorem strictInterl_lw_tR_lag_of_roots_nonpos {f g a R : ℝ[X]} - (hgf : Interlaces g f) - (hg_pos : HasPosLeadingCoeff g) - (hf_roots : ∀ r, f.IsRoot r → r ≤ 0) - (hR_nonneg : ∀ r, f.IsRoot r → 0 ≤ R.eval r) - (hF_pos : HasPosLeadingCoeff (a * f + (X * R) * g)) - (hdeg_lo : f.natDegree ≤ (a * f + (X * R) * g).natDegree) - (hdeg_hi : (a * f + (X * R) * g).natDegree ≤ f.natDegree + 1) - (hno : ∀ r, f.IsRoot r → ¬ g.IsRoot r) : - StrictInterl f (a * f + (X * R) * g) := - strictInterl_lw_positive_X_mul_lag_of_roots_nonpos - hgf hg_pos hf_roots hR_nonneg hF_pos hdeg_lo hdeg_hi hno - -/-- Family E `t R(t)` Liu--Wang step, deriving the half-line root bound from -nonnegative coefficients of the current row. -/ -theorem strictInterl_lw_tR_lag_of_nonneg_coeffs {f g a R : ℝ[X]} - (hgf : Interlaces g f) - (hg_pos : HasPosLeadingCoeff g) - (hf_nonneg : HasNonnegCoeffs f) - (hR_nonneg : ∀ r, f.IsRoot r → 0 ≤ R.eval r) - (hF_pos : HasPosLeadingCoeff (a * f + (X * R) * g)) - (hdeg_lo : f.natDegree ≤ (a * f + (X * R) * g).natDegree) - (hdeg_hi : (a * f + (X * R) * g).natDegree ≤ f.natDegree + 1) - (hno : ∀ r, f.IsRoot r → ¬ g.IsRoot r) : - StrictInterl f (a * f + (X * R) * g) := - strictInterl_lw_positive_X_mul_lag_of_nonneg_coeffs - hgf hg_pos hf_nonneg hR_nonneg hF_pos hdeg_lo hdeg_hi hno - /-- Family E `t(1-t)` Liu--Wang step with an explicit half-line root certificate. -/ theorem strictInterl_lw_X_mul_one_sub_X_lag_of_roots_nonpos {f g a : ℝ[X]} diff --git a/RealRooted/Mathlib/LinearAlgebra/Matrix/PerronFrobenius/Auxiliary.lean b/RealRooted/Mathlib/LinearAlgebra/Matrix/PerronFrobenius/Auxiliary.lean index 513837e0b..1ab2fbc5c 100644 --- a/RealRooted/Mathlib/LinearAlgebra/Matrix/PerronFrobenius/Auxiliary.lean +++ b/RealRooted/Mathlib/LinearAlgebra/Matrix/PerronFrobenius/Auxiliary.lean @@ -328,10 +328,6 @@ lemma lt_not_le {α : Type*} [PartialOrder α] (x y : α) : x < y → ¬ (x ≥ section ConditionallyCompleteLinearOrder variable {α : Type*} [ConditionallyCompleteLinearOrder α] -/-- If y is an upper bound of a set s, and x is in s, then x ≤ y -/ -lemma le_of_mem_upperBounds {s : Set α} {x : α} {y : α} (hy : y ∈ upperBounds s) (hx : x ∈ s) : - x ≤ y := by - exact hy hx lemma bddAbove_iff_exists_upperBound {s : Set α} : BddAbove s ↔ ∃ b, ∀ x ∈ s, x ≤ b := by exact bddAbove_def diff --git a/RealRooted/Mathlib/LinearAlgebra/Matrix/PerronFrobenius/CStarClasses.lean b/RealRooted/Mathlib/LinearAlgebra/Matrix/PerronFrobenius/CStarClasses.lean index 1430a3b40..b1fbdc656 100644 --- a/RealRooted/Mathlib/LinearAlgebra/Matrix/PerronFrobenius/CStarClasses.lean +++ b/RealRooted/Mathlib/LinearAlgebra/Matrix/PerronFrobenius/CStarClasses.lean @@ -28,9 +28,6 @@ theorem sq_eq_zero {R : Type*} [MonoidWithZero R] [NoZeroDivisors R] {x : R} : rw [pow_two, mul_eq_zero] exact or_self_iff -/-- An element of a nonempty set. -/ -lemma Set.mem_of_nonempty {α : Type*} (s : Set α) (h : s.Nonempty) : ∃ x, x ∈ s := h - /-- An equality between real numbers implies an equality between their complex embeddings. -/ diff --git a/RealRooted/MultiplierSequence.lean b/RealRooted/MultiplierSequence.lean index cc8f38955..f057b347a 100644 --- a/RealRooted/MultiplierSequence.lean +++ b/RealRooted/MultiplierSequence.lean @@ -790,33 +790,6 @@ def finitePolyaSchurNonnegBackwardStatement : Prop := IsPFPolynomial (jensenPolynomial n gamma) → IsFiniteMultiplierSequence n gamma -/-- Low-degree base case of the backward finite Pólya--Schur direction. - -For `n ≤ 1`, the Jensen-polynomial hypothesis is unnecessary: diagonal -operators preserve real-rootedness up to degree one for purely degree reasons. -/ -theorem finitePolyaSchurNonnegBackward_of_natDegree_le_one - {n : ℕ} (hn : n ≤ 1) {gamma : ℕ → ℝ} - (_hgamma : ∀ k, 0 ≤ gamma k) - (_hjensen : IsPFPolynomial (jensenPolynomial n gamma)) : - IsFiniteMultiplierSequence n gamma := - isFiniteMultiplierSequence_of_natDegree_le_one hn gamma - -/-- Degree-zero case of the backward finite Pólya--Schur direction. -/ -theorem finitePolyaSchurNonnegBackward_natDegree_zero - {gamma : ℕ → ℝ} - (_hgamma : ∀ k, 0 ≤ gamma k) - (_hjensen : IsPFPolynomial (jensenPolynomial 0 gamma)) : - IsFiniteMultiplierSequence 0 gamma := - isFiniteMultiplierSequence_natDegree_zero gamma - -/-- Degree-one case of the backward finite Pólya--Schur direction. -/ -theorem finitePolyaSchurNonnegBackward_natDegree_one - {gamma : ℕ → ℝ} - (_hgamma : ∀ k, 0 ≤ gamma k) - (_hjensen : IsPFPolynomial (jensenPolynomial 1 gamma)) : - IsFiniteMultiplierSequence 1 gamma := - isFiniteMultiplierSequence_natDegree_one gamma - /-- Degree at most two case of the backward finite Pólya--Schur direction. -/ theorem finitePolyaSchurNonnegBackward_of_natDegree_le_two {n : ℕ} (hn : n ≤ 2) {gamma : ℕ → ℝ} diff --git a/RealRooted/SameDegreeDerivative.lean b/RealRooted/SameDegreeDerivative.lean index 0d69f329f..9fac1fe3d 100644 --- a/RealRooted/SameDegreeDerivative.lean +++ b/RealRooted/SameDegreeDerivative.lean @@ -138,13 +138,6 @@ theorem roots_derivative_mem_Ioi_of_roots_mem_Ioi {p : ℝ[X]} {u : ℝ} ∀ r ∈ p.derivative.roots, r ∈ Set.Ioi u := lt_roots_derivative_of_lt_roots hp hdeg h -/-- Derivative root left-ray preservation. -/ -theorem roots_derivative_mem_Iio_of_roots_mem_Iio {p : ℝ[X]} {v : ℝ} - (hp : p.Splits) (hdeg : 2 ≤ p.natDegree) - (h : ∀ r ∈ p.roots, r ∈ Set.Iio v) : - ∀ r ∈ p.derivative.roots, r ∈ Set.Iio v := - roots_derivative_lt_of_roots_lt hp hdeg h - /-- Derivative root closed lower-ray preservation. -/ theorem roots_derivative_mem_Ici_of_roots_mem_Ici {p : ℝ[X]} {u : ℝ} (hp : p.Splits) (hdeg : 2 ≤ p.natDegree) diff --git a/RealRooted/ShiftLemma.lean b/RealRooted/ShiftLemma.lean index c1fa25845..e3e0f3651 100644 --- a/RealRooted/ShiftLemma.lean +++ b/RealRooted/ShiftLemma.lean @@ -187,17 +187,4 @@ theorem strictInterl_shift hss_eq, hrs_eq, Or.inr ⟨hsamedeg, halt⟩⟩ hdeg hf_pos hh_pos hf_nonpos hh_nonpos heval -/-- Shift lemma with variables named for applications. -/ -theorem strictInterl_shift' {F H : ℝ[X]} - (hF_ne : F ≠ 0) (hF_splits : F.Splits) (hH_ne : H ≠ 0) (hH_splits : H.Splits) - (hF_nonpos : ∀ r ∈ F.roots, r ≤ 0) - (hH_nonpos : ∀ r ∈ H.roots, r ≤ 0) - (hF_pos : HasPosLeadingCoeff F) - (hH_pos : HasPosLeadingCoeff H) - (hstrictInterl : StrictInterl H F) - (heval : H.eval 0 ≤ F.eval 0) : - StrictInterl F (F + (X - C 1) * H) := - strictInterl_shift hF_ne hF_splits hH_ne hH_splits hF_nonpos hH_nonpos hF_pos hH_pos - hstrictInterl heval - end RealRooted diff --git a/RealRooted/SuccDegreeLeftEndpoint.lean b/RealRooted/SuccDegreeLeftEndpoint.lean index af5d4d936..16d1b747d 100644 --- a/RealRooted/SuccDegreeLeftEndpoint.lean +++ b/RealRooted/SuccDegreeLeftEndpoint.lean @@ -370,16 +370,6 @@ theorem splits_of_closedSegment_family_of_succDegree rw [hEq] at hscaled exact hscaled -/-- Right-family form of the succ-degree endpoint theorem. -/ -theorem splits_right_of_add_C_mul_family_of_succDegree - {f g : ℝ[X]} - (hfamily : ∀ {μ : ℝ}, 0 < μ → ((g + C μ * f) ≠ 0 ∧ (g + C μ * f).Splits)) - (hf_pos : 0 < f.leadingCoeff) - (hg_pos : 0 < g.leadingCoeff) - (hsucc : f.natDegree = g.natDegree + 1) : - g.Splits := - splits_of_add_C_mul_family_of_succDegree hfamily hg_pos hf_pos hsucc - /-- Succ-degree positive-combination families split at the lower-degree endpoint. -/ theorem PosComboRealRooted.left_splits_of_succDegree {f g : ℝ[X]} diff --git a/RealRooted/Tactic/PFBidiagonal.lean b/RealRooted/Tactic/PFBidiagonal.lean index 4af511652..380408bf8 100644 --- a/RealRooted/Tactic/PFBidiagonal.lean +++ b/RealRooted/Tactic/PFBidiagonal.lean @@ -26,12 +26,6 @@ theorem splits_of_isPFPolynomial {p : ℝ[X]} (hp : IsPFPolynomial p) : p.Splits := RealRooted.Tactic.pf_splits hp -/-- Project one row from a PF sequence certificate. -/ -theorem at_of_isPFPolynomial_sequence {P : Nat → ℝ[X]} - (hP : ∀ n : Nat, IsPFPolynomial (P n)) (n : Nat) : - IsPFPolynomial (P n) := - hP n - /-- Project row-wise coefficient nonnegativity from a PF sequence certificate. -/ theorem hasNonnegCoeffs_of_isPFPolynomial_sequence {P : Nat → ℝ[X]} (hP : ∀ n : Nat, IsPFPolynomial (P n)) : diff --git a/RealRooted/Transforms/BrandenE/ProperPosition.lean b/RealRooted/Transforms/BrandenE/ProperPosition.lean index 7183290cc..927fcdb0f 100644 --- a/RealRooted/Transforms/BrandenE/ProperPosition.lean +++ b/RealRooted/Transforms/BrandenE/ProperPosition.lean @@ -278,13 +278,6 @@ theorem brandenBasisImage_zero_strictInterl StrictInterl (brandenBasisImage (R := ℝ) n 0) (brandenBasisImage n k) := brandenBasisImage_strictInterl n 0 k (by lia) hk -/-- The first basis image is in an interlacing relation before every in-range image -in ambient degree at least three. -/ -theorem brandenBasisImage_first_strictInterl - (n k : ℕ) (_hn : 3 ≤ n) (hk : k ≤ n) : - StrictInterl (brandenBasisImage (R := ℝ) n 0) (brandenBasisImage n k) := - brandenBasisImage_zero_strictInterl n k hk - /-- The ordered ambient-degree row of Brändén basis images. -/ def brandenBasisImageRow (n : ℕ) : List ℝ[X] := List.ofFn fun k : Fin (n + 1) ↦ brandenBasisImage n k