From b7282b23bc25cf6893e4e765719897d26f782363 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Wed, 11 Nov 2026 06:11:49 +0000 Subject: [PATCH] Centralize two privately duplicated lemmas MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit listAlternates_of_listInterlaces_cons had identical private copies in PolynomialValueEulerNumerator/Interlacing and Interlacing/QuadraticRemainderCriterion; it now lives once, public, in Basic/RootLists next to the definitions. iteratedPDerivAt_mul_of_pderiv_zero had private copies for ℂ and ℝ; it now lives once, for any commutative semiring, next to iteratedPDerivAt in LiebSokalOperator. Found by scripts/golf/dupbody.py. Co-Authored-By: Claude Opus 5.5 --- RealRooted/Basic/RootLists.lean | 9 +++++++++ .../BorceaBranden/FiniteOrderWeylPreserver.lean | 10 ---------- RealRooted/FiniteFreeAdditive/Stability.lean | 12 +----------- .../Interlacing/QuadraticRemainderCriterion.lean | 9 --------- RealRooted/LiebSokalOperator.lean | 10 ++++++++++ .../PolynomialValueEulerNumerator/Interlacing.lean | 9 --------- 6 files changed, 20 insertions(+), 39 deletions(-) diff --git a/RealRooted/Basic/RootLists.lean b/RealRooted/Basic/RootLists.lean index bfa5aa774..e11a366db 100644 --- a/RealRooted/Basic/RootLists.lean +++ b/RealRooted/Basic/RootLists.lean @@ -39,6 +39,15 @@ def ListAlternates : List ℝ → List ℝ → Prop | s :: ss, r :: rs => s ≤ r ∧ ListInterlaces ss (r :: rs) | _, _ => False +/-- Differ-by-one interleaving with the first right root dropped is same-degree interleaving. -/ +lemma listAlternates_of_listInterlaces_cons : + ∀ {ss rs : List ℝ} {r : ℝ}, ListInterlaces ss (r :: rs) → ListAlternates ss rs + | [], [], _, _ => by simp [ListAlternates] + | s :: ss, r₂ :: rs, r, h => by + simpa [ListInterlaces, ListAlternates] using h.2 + | [], _ :: _, _, h => by simp [ListInterlaces] at h + | _ :: _, [], _, h => by simp [ListInterlaces] at h + /-- If a list is sorted, then its tail interlaces into it. -/ lemma listInterlaces_tail_of_pairwise : ∀ rs : List ℝ, rs.Pairwise (· ≤ ·) → ListInterlaces rs.tail rs diff --git a/RealRooted/BorceaBranden/FiniteOrderWeylPreserver.lean b/RealRooted/BorceaBranden/FiniteOrderWeylPreserver.lean index c74917db2..36f6b2515 100644 --- a/RealRooted/BorceaBranden/FiniteOrderWeylPreserver.lean +++ b/RealRooted/BorceaBranden/FiniteOrderWeylPreserver.lean @@ -264,16 +264,6 @@ private theorem pderiv_spectatorProduct_zero {σ : Type*} [Fintype σ] intro i hi exact (Finset.mem_erase.mp hi).1 -private theorem iteratedPDerivAt_mul_of_pderiv_zero {σ : Type*} - (q : σ) (j : ℕ) (a b : MvPolynomial σ ℂ) - (hb : MvPolynomial.pderiv q b = 0) : - iteratedPDerivAt q j (a * b) = iteratedPDerivAt q j a * b := by - induction j with - | zero => rfl - | succ j ih => - rw [iteratedPDerivAt, ih, MvPolynomial.pderiv_mul, hb, mul_zero, - add_zero, iteratedPDerivAt] - private theorem algebraicSymbol_iteratedPDerivAtDegreeBox_explicit {σ : Type*} [Fintype σ] [DecidableEq σ] (q : σ) (j n : ℕ) (κ : σ → ℕ) diff --git a/RealRooted/FiniteFreeAdditive/Stability.lean b/RealRooted/FiniteFreeAdditive/Stability.lean index db638c3d7..cf2ac0be5 100644 --- a/RealRooted/FiniteFreeAdditive/Stability.lean +++ b/RealRooted/FiniteFreeAdditive/Stability.lean @@ -396,16 +396,6 @@ private theorem pderiv_spectatorProduct_zero_real simp exact hprod (Finset.univ.erase q) fun i hi => (Finset.mem_erase.mp hi).1 -private theorem iteratedPDerivAt_mul_of_pderiv_zero_real {σ : Type*} - (q : σ) (j : ℕ) (a b : MvPolynomial σ ℝ) - (hb : MvPolynomial.pderiv q b = 0) : - iteratedPDerivAt q j (a * b) = iteratedPDerivAt q j a * b := by - induction j with - | zero => rfl - | succ j ih => - rw [iteratedPDerivAt, ih, MvPolynomial.pderiv_mul, hb, mul_zero, - add_zero, iteratedPDerivAt] - private theorem algebraicSymbol_iteratedPDerivAtDegreeBoxReal_explicit {σ : Type*} [Fintype σ] [DecidableEq σ] (q : σ) (j D : ℕ) (κ : σ → ℕ) (hκ : κ q = D) : @@ -417,7 +407,7 @@ private theorem algebraicSymbol_iteratedPDerivAtDegreeBoxReal_explicit (MvPolynomial.X (Sum.inl i) + MvPolynomial.X (Sum.inr i)) ^ κ i := by rw [algebraicSymbol_iteratedPDerivAtDegreeBoxReal, algebraicSymbol_realDegreeBoxInclusion q D κ hκ, - iteratedPDerivAt_mul_of_pderiv_zero_real] + iteratedPDerivAt_mul_of_pderiv_zero] · rw [iteratedPDerivAt_linearForm_pow_real (Sum.inl q) (Sum.inr q) Sum.inl_ne_inr j D] · exact pderiv_spectatorProduct_zero_real q κ diff --git a/RealRooted/Interlacing/QuadraticRemainderCriterion.lean b/RealRooted/Interlacing/QuadraticRemainderCriterion.lean index 72095f69e..752e5084b 100644 --- a/RealRooted/Interlacing/QuadraticRemainderCriterion.lean +++ b/RealRooted/Interlacing/QuadraticRemainderCriterion.lean @@ -819,15 +819,6 @@ theorem normalizedQuadraticFamily_interlaces_mul_X_add_one_of_le simp [normalizedQuadraticFamily_natDegree] simpa only [map_neg, map_one, neg_neg, sub_neg_eq_add] using hfactor.toInterlaces hdeg -private lemma listAlternates_of_listInterlaces_cons : - ∀ {ss rs : List ℝ} {r : ℝ}, - ListInterlaces ss (r :: rs) → ListAlternates ss rs - | [], [], _, _ => by simp [ListAlternates] - | s :: ss, r₂ :: rs, r, h => by - simpa [ListInterlaces, ListAlternates] using h.2 - | [], _ :: _, _, h => by simp [ListInterlaces] at h - | _ :: _, [], _, h => by simp [ListInterlaces] at h - private lemma strictInterl_of_interlaces_mul_X_add_one {f g : ℝ[X]} (h : Interlaces f ((X + C 1) * g)) (hg₀ : g ≠ 0) (hgs : g.Splits) diff --git a/RealRooted/LiebSokalOperator.lean b/RealRooted/LiebSokalOperator.lean index 61a082f36..d84e26e93 100644 --- a/RealRooted/LiebSokalOperator.lean +++ b/RealRooted/LiebSokalOperator.lean @@ -38,6 +38,16 @@ theorem iteratedPDerivAt_eq_pow change MvPolynomial.pderiv i (((MvPolynomial.pderiv i).toLinearMap ^ n) P) = _ simp only [ih, iteratedPDerivAt] +/-- Iterated partial derivatives in `i` commute with multiplication by a factor that is constant +in `i`. -/ +theorem iteratedPDerivAt_mul_of_pderiv_zero {R sigma : Type*} [CommSemiring R] + (i : sigma) (n : ℕ) (a b : MvPolynomial sigma R) (hb : MvPolynomial.pderiv i b = 0) : + iteratedPDerivAt i n (a * b) = iteratedPDerivAt i n a * b := by + induction n with + | zero => rfl + | succ n ih => + rw [iteratedPDerivAt, ih, MvPolynomial.pderiv_mul, hb, mul_zero, add_zero, iteratedPDerivAt] + /-- A fixed enumeration of a finite variable type, used to define iterated partial differentiation without imposing an order on the variable type. -/ def differentialVariableOrder (sigma : Type*) [Fintype sigma] : List sigma := diff --git a/RealRooted/PolynomialValueEulerNumerator/Interlacing.lean b/RealRooted/PolynomialValueEulerNumerator/Interlacing.lean index 06faf216b..f66c3b99c 100644 --- a/RealRooted/PolynomialValueEulerNumerator/Interlacing.lean +++ b/RealRooted/PolynomialValueEulerNumerator/Interlacing.lean @@ -164,15 +164,6 @@ private lemma listAlternates_map_cayleyRoot : | [], _ :: _, h, _, _ => by simp [ListAlternates] at h | _ :: _, [], h, _, _ => by simp [ListAlternates] at h -private lemma listAlternates_of_listInterlaces_cons : - ∀ {ss rs : List ℝ} {r : ℝ}, - ListInterlaces ss (r :: rs) → ListAlternates ss rs - | [], [], _, _ => by simp [ListAlternates] - | s :: ss, r₂ :: rs, r, h => by - simpa [ListInterlaces, ListAlternates] using h.2 - | [], _ :: _, _, h => by simp [ListInterlaces] at h - | _ :: _, [], _, h => by simp [ListInterlaces] at h - private lemma all_ge_head_of_pairwise {r : ℝ} {rs : List ℝ} (h : (r :: rs).Pairwise (· ≤ ·)) : ∀ x ∈ r :: rs, r ≤ x := by