From c5c5e08e4c4eb64bb60875f4951062171c892852 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Sun, 2 Aug 2026 10:48:04 +0000 Subject: [PATCH 1/5] Add Karlin sign-block aggregation foundations --- .../LinearAlgebra/Matrix/SignVariation.lean | 269 ++++++++++++++++++ .../Matrix/VariationDiminishing.lean | 84 +++++- 2 files changed, 349 insertions(+), 4 deletions(-) diff --git a/RealRooted/Mathlib/LinearAlgebra/Matrix/SignVariation.lean b/RealRooted/Mathlib/LinearAlgebra/Matrix/SignVariation.lean index e1c483eb..b28aefb5 100644 --- a/RealRooted/Mathlib/LinearAlgebra/Matrix/SignVariation.lean +++ b/RealRooted/Mathlib/LinearAlgebra/Matrix/SignVariation.lean @@ -3,6 +3,8 @@ module public import Mathlib.Algebra.Polynomial.RuleOfSigns public import Mathlib.Data.List.ChainOfFn public import Mathlib.Data.List.NodupEquivFin +public import Mathlib.Data.List.SplitBy +public import Mathlib.Order.Monotone.Extension public import Mathlib.Tactic /-! @@ -29,6 +31,10 @@ lemma sign_neg_real (x : ℝ) : SignType.sign (-x) = -SignType.sign x := by · have hneg : -x < 0 := by linarith rw [sign_neg hneg, sign_pos hx] +lemma eq_neg_of_ne_of_ne_zero {s t : SignType} (hs : s ≠ 0) (ht : t ≠ 0) + (hst : s ≠ t) : s = -t := by + cases s <;> cases t <;> simp_all + end SignType namespace List @@ -356,6 +362,78 @@ lemma signVariations_append_nonpos_le_succ (l₁ l₂ : List ℝ) end List +namespace List + +private theorem exists_monotone_destutter_index {α β : Type*} [DecidableEq β] + (key : α → β) : + ∀ (l : List α), l ≠ [] → + ∃ block : Fin l.length → Fin ((l.map key).destutter (· ≠ ·)).length, + Monotone block ∧ Function.Surjective block ∧ + ∀ i, key (l.get i) = ((l.map key).destutter (· ≠ ·)).get (block i) + | [], h => (h rfl).elim + | [a], _ => by + refine ⟨id, monotone_id, Function.surjective_id, ?_⟩ + intro i + fin_cases i + rfl + | a :: b :: l, _ => by + obtain ⟨block, hmono, hsurj, hkey⟩ := + exists_monotone_destutter_index key (b :: l) (by simp) + by_cases hab : key a = key b + · have hdest : + (((a :: b :: l).map key).destutter (· ≠ ·)) = + (((b :: l).map key).destutter (· ≠ ·)) := by + simp only [map_cons, destutter_cons_cons] + rw [if_neg (not_ne_of_eq hab), hab] + rfl + rw [hdest] + let newBlock : + Fin (a :: b :: l).length → + Fin (((b :: l).map key).destutter (· ≠ ·)).length := + Fin.cases (block 0) block + refine ⟨newBlock, ?_, ?_, ?_⟩ + · rw [Fin.monotone_iff_le_succ] + intro i + refine Fin.cases ?_ (fun j => ?_) i + · simp [newBlock] + · simpa [newBlock] using (Fin.monotone_iff_le_succ.mp hmono j) + · intro i + obtain ⟨j, rfl⟩ := hsurj i + exact ⟨j.succ, by simp [newBlock]⟩ + · intro i + refine Fin.cases ?_ (fun j => ?_) i + · simpa [newBlock, hab] using hkey (0 : Fin (b :: l).length) + · simpa [newBlock] using hkey j + · have hdest : + (((a :: b :: l).map key).destutter (· ≠ ·)) = + key a :: ((b :: l).map key).destutter (· ≠ ·) := by + simp only [map_cons, destutter_cons_cons] + rw [if_pos hab] + rfl + rw [hdest] + let newBlock : + Fin (a :: b :: l).length → + Fin (key a :: ((b :: l).map key).destutter (· ≠ ·)).length := + Fin.cases 0 fun i => (block i).succ + refine ⟨newBlock, ?_, ?_, ?_⟩ + · rw [Fin.monotone_iff_le_succ] + intro i + refine Fin.cases ?_ (fun j => ?_) i + · simp [newBlock] + · simpa [newBlock] using + Fin.succ_le_succ (Fin.monotone_iff_le_succ.mp hmono j) + · intro i + refine Fin.cases ?_ (fun j => ?_) i + · exact ⟨0, by simp [newBlock]⟩ + · obtain ⟨k, rfl⟩ := hsurj j + exact ⟨k.succ, by simp [newBlock]⟩ + · intro i + refine Fin.cases ?_ (fun j => ?_) i + · simp [newBlock] + · simpa [newBlock] using hkey j + +end List + namespace Fin /-- The number of sign changes in a finite vector, in index order and ignoring @@ -453,6 +531,197 @@ lemma signVariations_append_nonpos_le_succ {m n : ℕ} (x : Fin m → ℝ) obtain ⟨i, rfl⟩ := ha exact hy i) +/-- A decomposition of a nonzero finite real vector into consecutive sign blocks. + +The block count is one more than the number of sign variations. Every block has +a nonzero coordinate, and zeros are assigned monotonically to neighboring sign +blocks. This is the finite combinatorial decomposition used in Karlin, *Total +Positivity*, Vol. I, Chapter V, Section 1, Theorem 1.2. -/ +structure SignBlockDecomposition {n : ℕ} (x : Fin n → ℝ) where + blockCount : ℕ + blockCount_eq : blockCount = signVariations x + 1 + block : Fin n → Fin blockCount + monotone_block : Monotone block + block_has_nonzero : ∀ b, ∃ i, block i = b ∧ x i ≠ 0 + blockSign : Fin blockCount → SignType + blockSign_ne_zero : ∀ b, blockSign b ≠ 0 + sign_eq_blockSign : ∀ i, x i ≠ 0 → SignType.sign (x i) = blockSign (block i) + adjacent_blockSign : + ∀ {i j}, (i : ℕ) + 1 = (j : ℕ) → blockSign i = -blockSign j + +namespace SignBlockDecomposition + +/-- The consecutive list blocks induced by a sign-block index map. -/ +def blocks {n : ℕ} {x : Fin n → ℝ} (D : SignBlockDecomposition x) : + List (List (Fin n)) := + (List.finRange n).splitBy fun i j => decide (D.block i = D.block j) + +@[simp] +theorem flatten_blocks {n : ℕ} {x : Fin n → ℝ} (D : SignBlockDecomposition x) : + D.blocks.flatten = List.finRange n := by + simp [blocks] + +theorem nil_notMem_blocks {n : ℕ} {x : Fin n → ℝ} + (D : SignBlockDecomposition x) : [] ∉ D.blocks := by + exact List.nil_notMem_splitBy _ _ + +theorem isChain_block_eq_of_mem_blocks {n : ℕ} {x : Fin n → ℝ} + (D : SignBlockDecomposition x) {B : List (Fin n)} (hB : B ∈ D.blocks) : + B.IsChain fun i j => D.block i = D.block j := by + simpa [blocks] using List.isChain_of_mem_splitBy hB + +theorem isChain_block_ne_blocks {n : ℕ} {x : Fin n → ℝ} + (D : SignBlockDecomposition x) : + D.blocks.IsChain fun A B => + ∃ hA hB, D.block (A.getLast hA) ≠ D.block (B.head hB) := by + simpa [blocks] using + List.isChain_getLast_head_splitBy + (fun i j : Fin n => decide (D.block i = D.block j)) (List.finRange n) + +theorem same_block_of_between {n : ℕ} {x : Fin n → ℝ} + (D : SignBlockDecomposition x) {i j k : Fin n} (hik : i ≤ k) (hkj : k ≤ j) + (hij : D.block i = D.block j) : D.block k = D.block i := by + apply le_antisymm + · simpa [hij] using D.monotone_block hkj + · exact D.monotone_block hik + +theorem sign_eq_sign_of_block_eq {n : ℕ} {x : Fin n → ℝ} + (D : SignBlockDecomposition x) {i j : Fin n} (hi : x i ≠ 0) (hj : x j ≠ 0) + (hij : D.block i = D.block j) : SignType.sign (x i) = SignType.sign (x j) := by + rw [D.sign_eq_blockSign i hi, D.sign_eq_blockSign j hj, hij] + +end SignBlockDecomposition + +/-- Every nonzero finite real vector admits its canonical consecutive sign-block +decomposition. Leading zeros are put in block zero, while an extension across +internal zeros may put them in either adjacent block. -/ +theorem exists_signBlockDecomposition {n : ℕ} (x : Fin n → ℝ) (hx : x ≠ 0) : + Nonempty (SignBlockDecomposition x) := by + classical + let support : List (Fin n) := + (List.finRange n).filter fun i => x i ≠ 0 + have hx_exists : ∃ i, x i ≠ 0 := by + by_contra h + push_neg at h + apply hx + funext i + exact h i + have hsupport_ne : support ≠ [] := by + obtain ⟨i, hi⟩ := hx_exists + exact List.ne_nil_of_mem (by simp [support, hi]) + have hsupport_sorted : support.SortedLT := by + exact ((List.sortedLT_finRange n).pairwise.filter _).sortedLT + let key : Fin n → SignType := fun i => SignType.sign (x i) + let d : List SignType := (support.map key).destutter (· ≠ ·) + obtain ⟨run, hrun_mono, hrun_surj, hrun_key⟩ := + List.exists_monotone_destutter_index key support hsupport_ne + have hsigns : + support.map key = + ((List.ofFn x).map SignType.sign).filter (· ≠ 0) := by + simp only [support, key, List.ofFn_eq_map, List.map_map] + rw [List.filter_map] + congr 1 + apply List.filter_congr + intro i hi + simp [SignType.sign_ne_zero] + have hd_ne : d ≠ [] := by + dsimp only [d] + rw [List.destutter_eq_nil] + simpa using hsupport_ne + have hd_pos : 0 < d.length := List.length_pos.mpr hd_ne + have hvariation : signVariations x = d.length - 1 := by + rw [signVariations, List.signVariations, ← hsigns] + rfl + have hcount : d.length = signVariations x + 1 := by + rw [hvariation] + lia + let supportIso : Fin support.length ≃o {i // i ∈ support} := + hsupport_sorted.getIso support + let supportSet : Set (Fin n) := {i | x i ≠ 0} + let partial (i : Fin n) : Fin d.length := + if hi : i ∈ support then + run (supportIso.symm ⟨i, hi⟩) + else + ⟨0, hd_pos⟩ + have hpartial_mono : MonotoneOn partial supportSet := by + intro i hi j hj hij + have himem : i ∈ support := by simp [support, hi] + have hjmem : j ∈ support := by simp [support, hj] + simp only [partial, dif_pos himem, dif_pos hjmem] + apply hrun_mono + apply supportIso.symm.monotone + exact hij + letI : NeZero d.length := ⟨Nat.ne_of_gt hd_pos⟩ + have hbelow : BddBelow (partial '' supportSet) := by + refine ⟨⊥, ?_⟩ + rintro _ ⟨i, hi, rfl⟩ + exact bot_le + have habove : BddAbove (partial '' supportSet) := by + refine ⟨⊤, ?_⟩ + rintro _ ⟨i, hi, rfl⟩ + exact le_top + obtain ⟨block, hblock_mono, hblock_eq⟩ := + hpartial_mono.exists_monotone_extension hbelow habove + have hsupport_get_mem (i : Fin support.length) : support.get i ∈ support := + List.get_mem support i + have hsupport_get_ne (i : Fin support.length) : x (support.get i) ≠ 0 := by + simpa [support] using hsupport_get_mem i + have hsupportIso_symm_get (i : Fin support.length) : + supportIso.symm ⟨support.get i, hsupport_get_mem i⟩ = i := by + simpa [supportIso] using supportIso.symm_apply_apply i + refine ⟨{ + blockCount := d.length + blockCount_eq := hcount + block := block + monotone_block := hblock_mono + block_has_nonzero := ?_ + blockSign := fun b => d.get b + blockSign_ne_zero := ?_ + sign_eq_blockSign := ?_ + adjacent_blockSign := ?_ }⟩ + · intro b + obtain ⟨i, hi⟩ := hrun_surj b + have hne := hsupport_get_ne i + have himem := hsupport_get_mem i + refine ⟨support.get i, ?_, hne⟩ + rw [← hblock_eq (by simpa [supportSet] using hne)] + simp [partial, himem, hsupportIso_symm_get, hi] + · intro b + have hbmem : d.get b ∈ support.map key := + (List.destutter_sublist (support.map key) (· ≠ ·)).subset (List.get_mem d b) + obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hbmem + exact SignType.sign_ne_zero.mpr (by simpa [support] using hi) + · intro i hi + have himem : i ∈ support := by simp [support, hi] + let k : Fin support.length := supportIso.symm ⟨i, himem⟩ + have hget : support.get k = i := by + have h := supportIso.apply_symm_apply ⟨i, himem⟩ + exact congrArg Subtype.val h + have hblock : block i = run k := by + rw [← hblock_eq (by simpa [supportSet] using hi)] + simp [partial, himem, k] + simpa [key, d, hget, hblock] using hrun_key k + · intro i j hij + have hchain : d.IsChain (· ≠ ·) := by + exact List.isChain_destutter (support.map key) (· ≠ ·) + have hne : d.get i ≠ d.get j := by + have hrel := List.isChain_iff_getElem.mp hchain i.val (by lia) + simpa [List.get_eq_getElem, hij] using hrel + exact SignType.eq_neg_of_ne_of_ne_zero + (by + have hbmem : d.get i ∈ support.map key := + (List.destutter_sublist (support.map key) (· ≠ ·)).subset + (List.get_mem d i) + obtain ⟨k, hk, rfl⟩ := List.mem_map.mp hbmem + exact SignType.sign_ne_zero.mpr (by simpa [support] using hk)) + (by + have hbmem : d.get j ∈ support.map key := + (List.destutter_sublist (support.map key) (· ≠ ·)).subset + (List.get_mem d j) + obtain ⟨k, hk, rfl⟩ := List.mem_map.mp hbmem + exact SignType.sign_ne_zero.mpr (by simpa [support] using hk)) + hne + /-- A finite vector split into a nonnegative initial block and a nonpositive final block has at most one sign variation. -/ lemma signVariations_le_one_of_castAdd_nonneg_natAdd_nonpos {m n : ℕ} diff --git a/RealRooted/Mathlib/LinearAlgebra/Matrix/VariationDiminishing.lean b/RealRooted/Mathlib/LinearAlgebra/Matrix/VariationDiminishing.lean index e694e453..08847f6a 100644 --- a/RealRooted/Mathlib/LinearAlgebra/Matrix/VariationDiminishing.lean +++ b/RealRooted/Mathlib/LinearAlgebra/Matrix/VariationDiminishing.lean @@ -47,10 +47,9 @@ lemma Matrix.IsTotallyNonnegRect.aggregate_monotone ``` This is the consecutive-block determinant expansion used in Chapter 5, -Section 1. It requires a finite Cauchy--Binet/multilinearity development not -yet present in the local rectangular-TN API. Until that lemma and the strict -sector and limit lemmas in Steps 4--5 are proved, this file deliberately does -not declare the full theorem with an unproved backend. +Section 1. The lemma is proved below by determinant multilinearity. Until +the strict sector and limit lemmas in Steps 4--5 are proved, this file +deliberately does not declare the full theorem with an unproved backend. -/ public section @@ -69,6 +68,83 @@ end Fin namespace Matrix +/-- Aggregating columns along a monotone block map with nonnegative weights +preserves rectangular total nonnegativity. -/ +lemma IsTotallyNonnegRect.aggregate_monotone + {m n q : ℕ} {M : Matrix (Fin m) (Fin n) ℝ} + (hM : M.IsTotallyNonnegRect) (block : Fin n → Fin q) + (hblock : Monotone block) (weight : Fin n → ℝ) + (hweight : ∀ j, 0 ≤ weight j) : + Matrix.IsTotallyNonnegRect + ((fun i s ↦ ∑ j with block j = s, M i j * weight j) : + Matrix (Fin m) (Fin q) ℝ) := by + classical + intro k rows cols hrows hcols + let fibers : Fin k → Finset (Fin n) := fun s ↦ + Finset.univ.filter fun j ↦ block j = cols s + let sourceCol : Fin k → Fin n → (Fin k → ℝ) := fun _ j i ↦ + M (rows i) j * weight j + have hexpand : + (Matrix.submatrix + ((fun i s ↦ ∑ j with block j = s, M i j * weight j) : + Matrix (Fin m) (Fin q) ℝ) rows cols).det = + ∑ r ∈ Fintype.piFinset fibers, + Matrix.det (fun s i ↦ sourceCol s (r s) i) := by + rw [← Matrix.det_transpose] + have hmatrix : + (Matrix.submatrix + ((fun i s ↦ ∑ j with block j = s, M i j * weight j) : + Matrix (Fin m) (Fin q) ℝ) rows cols)ᵀ = + fun s ↦ ∑ j ∈ fibers s, sourceCol s j := by + ext s i + simp [fibers, sourceCol] + rw [hmatrix] + change + (Matrix.detRowAlternating : (Fin k → ℝ) [⋀^Fin k]→ₗ[ℝ] ℝ).toMultilinearMap + (fun s ↦ ∑ j ∈ fibers s, sourceCol s j) = + ∑ r ∈ Fintype.piFinset fibers, + (Matrix.detRowAlternating : + (Fin k → ℝ) [⋀^Fin k]→ₗ[ℝ] ℝ).toMultilinearMap + (fun s ↦ sourceCol s (r s)) + exact MultilinearMap.map_sum_finset + (Matrix.detRowAlternating : + (Fin k → ℝ) [⋀^Fin k]→ₗ[ℝ] ℝ).toMultilinearMap + sourceCol fibers + rw [hexpand] + refine Finset.sum_nonneg fun r hr ↦ ?_ + have hrmem : ∀ s, r s ∈ fibers s := Fintype.mem_piFinset.mp hr + have hrblock : ∀ s, block (r s) = cols s := by + intro s + simpa [fibers] using hrmem s + have hrmono : StrictMono r := by + intro a b hab + by_contra hnlt + have hrle : r b ≤ r a := le_of_not_gt hnlt + have hblockle : block (r b) ≤ block (r a) := hblock hrle + rw [hrblock b, hrblock a] at hblockle + exact (not_le_of_gt (hcols hab)) hblockle + have hminor : 0 ≤ (M.submatrix rows r).det := hM hrows hrmono + have hprod : 0 ≤ ∏ s, weight (r s) := + Finset.prod_nonneg fun s _ ↦ hweight (r s) + have hdet : + Matrix.det (fun s i ↦ sourceCol s (r s) i) = + (∏ s, weight (r s)) * (M.submatrix rows r).det := by + rw [← Matrix.det_transpose (M.submatrix rows r)] + simp only [sourceCol] + change Matrix.detRowAlternating + (fun s i ↦ M (rows i) (r s) * weight (r s)) = + (∏ s, weight (r s)) * + Matrix.detRowAlternating (fun s i ↦ M (rows i) (r s)) + rw [show (fun s i ↦ M (rows i) (r s) * weight (r s)) = + (fun s ↦ weight (r s) • fun i ↦ M (rows i) (r s)) by + funext s i + simp [mul_comm]] + simpa only [smul_eq_mul] using + (MultilinearMap.map_smul_univ Matrix.detRowAlternating.toMultilinearMap + (fun s ↦ weight (r s)) (fun s i ↦ M (rows i) (r s))) + rw [hdet] + exact mul_nonneg hprod hminor + /-- A common nonzero sign for all maximal minors makes multiplication by the rectangular matrix injective. This is the rank step in Karlin, Chapter 5, Section 1, Theorem 1.1. -/ From b3c111654e9f55503aef674cd30b396396bf50bc Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Sun, 2 Aug 2026 11:09:24 +0000 Subject: [PATCH 2/5] Repair sign-block decomposition elaboration --- .../LinearAlgebra/Matrix/SignVariation.lean | 100 ++++++++++-------- 1 file changed, 58 insertions(+), 42 deletions(-) diff --git a/RealRooted/Mathlib/LinearAlgebra/Matrix/SignVariation.lean b/RealRooted/Mathlib/LinearAlgebra/Matrix/SignVariation.lean index b28aefb5..1be1cb73 100644 --- a/RealRooted/Mathlib/LinearAlgebra/Matrix/SignVariation.lean +++ b/RealRooted/Mathlib/LinearAlgebra/Matrix/SignVariation.lean @@ -384,7 +384,7 @@ private theorem exists_monotone_destutter_index {α β : Type*} [DecidableEq β] (((a :: b :: l).map key).destutter (· ≠ ·)) = (((b :: l).map key).destutter (· ≠ ·)) := by simp only [map_cons, destutter_cons_cons] - rw [if_neg (not_ne_of_eq hab), hab] + rw [if_neg (by simpa using hab), hab] rfl rw [hdest] let newBlock : @@ -395,7 +395,8 @@ private theorem exists_monotone_destutter_index {α β : Type*} [DecidableEq β] · rw [Fin.monotone_iff_le_succ] intro i refine Fin.cases ?_ (fun j => ?_) i - · simp [newBlock] + · change block 0 ≤ block 0 + exact le_rfl · simpa [newBlock] using (Fin.monotone_iff_le_succ.mp hmono j) · intro i obtain ⟨j, rfl⟩ := hsurj i @@ -419,9 +420,11 @@ private theorem exists_monotone_destutter_index {α β : Type*} [DecidableEq β] · rw [Fin.monotone_iff_le_succ] intro i refine Fin.cases ?_ (fun j => ?_) i - · simp [newBlock] - · simpa [newBlock] using - Fin.succ_le_succ (Fin.monotone_iff_le_succ.mp hmono j) + · change (0 : Fin (key a :: ((b :: l).map key).destutter (· ≠ ·)).length) ≤ + (block 0).succ + exact bot_le + · change (block j.castSucc).val + 1 ≤ (block j.succ).val + 1 + exact Nat.succ_le_succ (Fin.monotone_iff_le_succ.mp hmono j) · intro i refine Fin.cases ?_ (fun j => ?_) i · exact ⟨0, by simp [newBlock]⟩ @@ -538,16 +541,20 @@ a nonzero coordinate, and zeros are assigned monotonically to neighboring sign blocks. This is the finite combinatorial decomposition used in Karlin, *Total Positivity*, Vol. I, Chapter V, Section 1, Theorem 1.2. -/ structure SignBlockDecomposition {n : ℕ} (x : Fin n → ℝ) where + /-- The number of consecutive nonzero sign blocks. -/ blockCount : ℕ blockCount_eq : blockCount = signVariations x + 1 + /-- The weakly increasing block index assigned to each vector position. -/ block : Fin n → Fin blockCount monotone_block : Monotone block block_has_nonzero : ∀ b, ∃ i, block i = b ∧ x i ≠ 0 + /-- The nonzero sign carried by each block. -/ blockSign : Fin blockCount → SignType blockSign_ne_zero : ∀ b, blockSign b ≠ 0 sign_eq_blockSign : ∀ i, x i ≠ 0 → SignType.sign (x i) = blockSign (block i) adjacent_blockSign : - ∀ {i j}, (i : ℕ) + 1 = (j : ℕ) → blockSign i = -blockSign j + ∀ {i j : Fin blockCount}, + (i : ℕ) + 1 = (j : ℕ) → blockSign i = -blockSign j namespace SignBlockDecomposition @@ -602,13 +609,16 @@ theorem exists_signBlockDecomposition {n : ℕ} (x : Fin n → ℝ) (hx : x ≠ (List.finRange n).filter fun i => x i ≠ 0 have hx_exists : ∃ i, x i ≠ 0 := by by_contra h - push_neg at h + push Not at h apply hx funext i exact h i have hsupport_ne : support ≠ [] := by obtain ⟨i, hi⟩ := hx_exists - exact List.ne_nil_of_mem (by simp [support, hi]) + intro hs + have himem : i ∈ support := by simp [support, hi] + rw [hs] at himem + simp at himem have hsupport_sorted : support.SortedLT := by exact ((List.sortedLT_finRange n).pairwise.filter _).sortedLT let key : Fin n → SignType := fun i => SignType.sign (x i) @@ -623,40 +633,44 @@ theorem exists_signBlockDecomposition {n : ℕ} (x : Fin n → ℝ) (hx : x ≠ congr 1 apply List.filter_congr intro i hi - simp [SignType.sign_ne_zero] + simp have hd_ne : d ≠ [] := by dsimp only [d] - rw [List.destutter_eq_nil] - simpa using hsupport_ne - have hd_pos : 0 < d.length := List.length_pos.mpr hd_ne + intro hd + have hm : support.map key = [] := + (List.destutter_eq_nil (R := fun s t : SignType => s ≠ t)).mp hd + exact hsupport_ne (by simpa using hm) + have hd_pos : 0 < d.length := by + exact Nat.pos_of_ne_zero (by simpa using hd_ne) have hvariation : signVariations x = d.length - 1 := by rw [signVariations, List.signVariations, ← hsigns] - rfl have hcount : d.length = signVariations x + 1 := by rw [hvariation] lia let supportIso : Fin support.length ≃o {i // i ∈ support} := hsupport_sorted.getIso support let supportSet : Set (Fin n) := {i | x i ≠ 0} - let partial (i : Fin n) : Fin d.length := + let supportBlock : Fin n → Fin d.length := fun i => if hi : i ∈ support then run (supportIso.symm ⟨i, hi⟩) else ⟨0, hd_pos⟩ - have hpartial_mono : MonotoneOn partial supportSet := by + have hpartial_mono : MonotoneOn supportBlock supportSet := by intro i hi j hj hij - have himem : i ∈ support := by simp [support, hi] - have hjmem : j ∈ support := by simp [support, hj] - simp only [partial, dif_pos himem, dif_pos hjmem] + have hi0 : x i ≠ 0 := by simpa [supportSet] using hi + have hj0 : x j ≠ 0 := by simpa [supportSet] using hj + have himem : i ∈ support := by simp [support, hi0] + have hjmem : j ∈ support := by simp [support, hj0] + simp only [supportBlock, dif_pos himem, dif_pos hjmem] apply hrun_mono apply supportIso.symm.monotone exact hij letI : NeZero d.length := ⟨Nat.ne_of_gt hd_pos⟩ - have hbelow : BddBelow (partial '' supportSet) := by + have hbelow : BddBelow (supportBlock '' supportSet) := by refine ⟨⊥, ?_⟩ rintro _ ⟨i, hi, rfl⟩ exact bot_le - have habove : BddAbove (partial '' supportSet) := by + have habove : BddAbove (supportBlock '' supportSet) := by refine ⟨⊤, ?_⟩ rintro _ ⟨i, hi, rfl⟩ exact le_top @@ -665,10 +679,18 @@ theorem exists_signBlockDecomposition {n : ℕ} (x : Fin n → ℝ) (hx : x ≠ have hsupport_get_mem (i : Fin support.length) : support.get i ∈ support := List.get_mem support i have hsupport_get_ne (i : Fin support.length) : x (support.get i) ≠ 0 := by - simpa [support] using hsupport_get_mem i + exact of_decide_eq_true (List.mem_filter.mp (hsupport_get_mem i)).2 have hsupportIso_symm_get (i : Fin support.length) : supportIso.symm ⟨support.get i, hsupport_get_mem i⟩ = i := by - simpa [supportIso] using supportIso.symm_apply_apply i + exact supportIso.symm_apply_apply i + have hd_get_ne (b : Fin d.length) : d.get b ≠ 0 := by + have hbmem : d.get b ∈ support.map key := + (List.destutter_sublist + (R := fun s t : SignType => s ≠ t) (support.map key)).mem (List.get_mem d b) + obtain ⟨i, hi, hkey⟩ := List.mem_map.mp hbmem + rw [← hkey] + exact sign_ne_zero.mpr + (of_decide_eq_true (List.mem_filter.mp hi).2) refine ⟨{ blockCount := d.length blockCount_eq := hcount @@ -685,12 +707,11 @@ theorem exists_signBlockDecomposition {n : ℕ} (x : Fin n → ℝ) (hx : x ≠ have himem := hsupport_get_mem i refine ⟨support.get i, ?_, hne⟩ rw [← hblock_eq (by simpa [supportSet] using hne)] - simp [partial, himem, hsupportIso_symm_get, hi] + rw [show supportBlock (support.get i) = run i by + simpa only [supportBlock, dif_pos himem] using + congrArg run (hsupportIso_symm_get i), hi] · intro b - have hbmem : d.get b ∈ support.map key := - (List.destutter_sublist (support.map key) (· ≠ ·)).subset (List.get_mem d b) - obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hbmem - exact SignType.sign_ne_zero.mpr (by simpa [support] using hi) + exact hd_get_ne b · intro i hi have himem : i ∈ support := by simp [support, hi] let k : Fin support.length := supportIso.symm ⟨i, himem⟩ @@ -699,27 +720,22 @@ theorem exists_signBlockDecomposition {n : ℕ} (x : Fin n → ℝ) (hx : x ≠ exact congrArg Subtype.val h have hblock : block i = run k := by rw [← hblock_eq (by simpa [supportSet] using hi)] - simp [partial, himem, k] - simpa [key, d, hget, hblock] using hrun_key k + simp [supportBlock, himem, k] + calc + SignType.sign (x i) = key (support.get k) := by + simpa only [key] using + (congrArg (fun j => SignType.sign (x j)) hget).symm + _ = d.get (run k) := hrun_key k + _ = d.get (block i) := by rw [hblock] · intro i j hij have hchain : d.IsChain (· ≠ ·) := by - exact List.isChain_destutter (support.map key) (· ≠ ·) + exact List.isChain_destutter + (R := fun s t : SignType => s ≠ t) (support.map key) have hne : d.get i ≠ d.get j := by have hrel := List.isChain_iff_getElem.mp hchain i.val (by lia) simpa [List.get_eq_getElem, hij] using hrel exact SignType.eq_neg_of_ne_of_ne_zero - (by - have hbmem : d.get i ∈ support.map key := - (List.destutter_sublist (support.map key) (· ≠ ·)).subset - (List.get_mem d i) - obtain ⟨k, hk, rfl⟩ := List.mem_map.mp hbmem - exact SignType.sign_ne_zero.mpr (by simpa [support] using hk)) - (by - have hbmem : d.get j ∈ support.map key := - (List.destutter_sublist (support.map key) (· ≠ ·)).subset - (List.get_mem d j) - obtain ⟨k, hk, rfl⟩ := List.mem_map.mp hbmem - exact SignType.sign_ne_zero.mpr (by simpa [support] using hk)) + (hd_get_ne i) (hd_get_ne j) hne /-- A finite vector split into a nonnegative initial block and a nonpositive From e64e44b41f57b478e174c9f168b1829a1197fd31 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Sun, 2 Aug 2026 11:19:16 +0000 Subject: [PATCH 3/5] Extract fiberwise determinant expansion --- .../Matrix/VariationDiminishing.lean | 93 +++++++++++-------- 1 file changed, 54 insertions(+), 39 deletions(-) diff --git a/RealRooted/Mathlib/LinearAlgebra/Matrix/VariationDiminishing.lean b/RealRooted/Mathlib/LinearAlgebra/Matrix/VariationDiminishing.lean index 08847f6a..e2bcbd67 100644 --- a/RealRooted/Mathlib/LinearAlgebra/Matrix/VariationDiminishing.lean +++ b/RealRooted/Mathlib/LinearAlgebra/Matrix/VariationDiminishing.lean @@ -68,54 +68,86 @@ end Fin namespace Matrix -/-- Aggregating columns along a monotone block map with nonnegative weights -preserves rectangular total nonnegativity. -/ -lemma IsTotallyNonnegRect.aggregate_monotone - {m n q : ℕ} {M : Matrix (Fin m) (Fin n) ℝ} - (hM : M.IsTotallyNonnegRect) (block : Fin n → Fin q) - (hblock : Monotone block) (weight : Fin n → ℝ) - (hweight : ∀ j, 0 ≤ weight j) : - Matrix.IsTotallyNonnegRect - ((fun i s ↦ ∑ j with block j = s, M i j * weight j) : - Matrix (Fin m) (Fin q) ℝ) := by +/-- Expanding a minor after fiberwise weighted column aggregation gives the +sum of the corresponding source minors times their weight products. -/ +theorem det_submatrix_fiberwise_sum + {R ι ρ κ σ : Type*} [CommRing R] + [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq σ] + (M : Matrix ρ κ R) (rows : ι → ρ) (cols : ι → σ) + (block : κ → σ) (weight : κ → R) : + (Matrix.submatrix + ((fun i s ↦ ∑ j with block j = s, M i j * weight j) : Matrix ρ σ R) + rows cols).det = + ∑ r ∈ Fintype.piFinset + (fun s : ι ↦ Finset.univ.filter fun j ↦ block j = cols s), + (∏ s, weight (r s)) * (M.submatrix rows r).det := by classical - intro k rows cols hrows hcols - let fibers : Fin k → Finset (Fin n) := fun s ↦ + let fibers : ι → Finset κ := fun s ↦ Finset.univ.filter fun j ↦ block j = cols s - let sourceCol : Fin k → Fin n → (Fin k → ℝ) := fun _ j i ↦ + let sourceCol : ι → κ → (ι → R) := fun _ j i ↦ M (rows i) j * weight j have hexpand : (Matrix.submatrix - ((fun i s ↦ ∑ j with block j = s, M i j * weight j) : - Matrix (Fin m) (Fin q) ℝ) rows cols).det = + ((fun i s ↦ ∑ j with block j = s, M i j * weight j) : Matrix ρ σ R) + rows cols).det = ∑ r ∈ Fintype.piFinset fibers, Matrix.det (fun s i ↦ sourceCol s (r s) i) := by rw [← Matrix.det_transpose] have hmatrix : (Matrix.submatrix - ((fun i s ↦ ∑ j with block j = s, M i j * weight j) : - Matrix (Fin m) (Fin q) ℝ) rows cols)ᵀ = + ((fun i s ↦ ∑ j with block j = s, M i j * weight j) : Matrix ρ σ R) + rows cols)ᵀ = fun s ↦ ∑ j ∈ fibers s, sourceCol s j := by ext s i simp [fibers, sourceCol] rw [hmatrix] change - (Matrix.detRowAlternating : (Fin k → ℝ) [⋀^Fin k]→ₗ[ℝ] ℝ).toMultilinearMap + (Matrix.detRowAlternating : (ι → R) [⋀^ι]→ₗ[R] R).toMultilinearMap (fun s ↦ ∑ j ∈ fibers s, sourceCol s j) = ∑ r ∈ Fintype.piFinset fibers, (Matrix.detRowAlternating : - (Fin k → ℝ) [⋀^Fin k]→ₗ[ℝ] ℝ).toMultilinearMap + (ι → R) [⋀^ι]→ₗ[R] R).toMultilinearMap (fun s ↦ sourceCol s (r s)) exact MultilinearMap.map_sum_finset (Matrix.detRowAlternating : - (Fin k → ℝ) [⋀^Fin k]→ₗ[ℝ] ℝ).toMultilinearMap + (ι → R) [⋀^ι]→ₗ[R] R).toMultilinearMap sourceCol fibers rw [hexpand] + apply Finset.sum_congr rfl + intro r _ + rw [← Matrix.det_transpose (M.submatrix rows r)] + simp only [sourceCol] + change + (Matrix.detRowAlternating : (ι → R) [⋀^ι]→ₗ[R] R).toMultilinearMap + (fun s i ↦ M (rows i) (r s) * weight (r s)) = + (∏ s, weight (r s)) * + (Matrix.detRowAlternating : (ι → R) [⋀^ι]→ₗ[R] R).toMultilinearMap + (fun s i ↦ M (rows i) (r s)) + rw [show (fun s i ↦ M (rows i) (r s) * weight (r s)) = + (fun s ↦ weight (r s) • fun i ↦ M (rows i) (r s)) by + funext s i + simp [mul_comm]] + simpa only [smul_eq_mul] using + (MultilinearMap.map_smul_univ Matrix.detRowAlternating.toMultilinearMap + (fun s ↦ weight (r s)) (fun s i ↦ M (rows i) (r s))) + +/-- Aggregating columns along a monotone block map with nonnegative weights +preserves rectangular total nonnegativity. -/ +lemma IsTotallyNonnegRect.aggregate_monotone + {m n q : ℕ} {M : Matrix (Fin m) (Fin n) ℝ} + (hM : M.IsTotallyNonnegRect) (block : Fin n → Fin q) + (hblock : Monotone block) (weight : Fin n → ℝ) + (hweight : ∀ j, 0 ≤ weight j) : + Matrix.IsTotallyNonnegRect + ((fun i s ↦ ∑ j with block j = s, M i j * weight j) : + Matrix (Fin m) (Fin q) ℝ) := by + classical + intro k rows cols hrows hcols + rw [det_submatrix_fiberwise_sum] refine Finset.sum_nonneg fun r hr ↦ ?_ - have hrmem : ∀ s, r s ∈ fibers s := Fintype.mem_piFinset.mp hr have hrblock : ∀ s, block (r s) = cols s := by intro s - simpa [fibers] using hrmem s + simpa using (Fintype.mem_piFinset.mp hr s) have hrmono : StrictMono r := by intro a b hab by_contra hnlt @@ -126,23 +158,6 @@ lemma IsTotallyNonnegRect.aggregate_monotone have hminor : 0 ≤ (M.submatrix rows r).det := hM hrows hrmono have hprod : 0 ≤ ∏ s, weight (r s) := Finset.prod_nonneg fun s _ ↦ hweight (r s) - have hdet : - Matrix.det (fun s i ↦ sourceCol s (r s) i) = - (∏ s, weight (r s)) * (M.submatrix rows r).det := by - rw [← Matrix.det_transpose (M.submatrix rows r)] - simp only [sourceCol] - change Matrix.detRowAlternating - (fun s i ↦ M (rows i) (r s) * weight (r s)) = - (∏ s, weight (r s)) * - Matrix.detRowAlternating (fun s i ↦ M (rows i) (r s)) - rw [show (fun s i ↦ M (rows i) (r s) * weight (r s)) = - (fun s ↦ weight (r s) • fun i ↦ M (rows i) (r s)) by - funext s i - simp [mul_comm]] - simpa only [smul_eq_mul] using - (MultilinearMap.map_smul_univ Matrix.detRowAlternating.toMultilinearMap - (fun s ↦ weight (r s)) (fun s i ↦ M (rows i) (r s))) - rw [hdet] exact mul_nonneg hprod hminor /-- A common nonzero sign for all maximal minors makes multiplication by the From a340c86b4618ac945299388564fe08c248565123 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Sun, 2 Aug 2026 11:26:13 +0000 Subject: [PATCH 4/5] Prove strict fiberwise aggregate minors --- .../Matrix/VariationDiminishing.lean | 66 +++++++++++++++++++ 1 file changed, 66 insertions(+) diff --git a/RealRooted/Mathlib/LinearAlgebra/Matrix/VariationDiminishing.lean b/RealRooted/Mathlib/LinearAlgebra/Matrix/VariationDiminishing.lean index e2bcbd67..6eb6f448 100644 --- a/RealRooted/Mathlib/LinearAlgebra/Matrix/VariationDiminishing.lean +++ b/RealRooted/Mathlib/LinearAlgebra/Matrix/VariationDiminishing.lean @@ -160,6 +160,72 @@ lemma IsTotallyNonnegRect.aggregate_monotone Finset.prod_nonneg fun s _ ↦ hweight (r s) exact mul_nonneg hprod hminor +/-- If every source minor of the target size is positive and every aggregation +fiber has a positive-weight representative, then the aggregated maximal +minors have a common strict sign. This is the strict-summand step in Karlin, +Chapter 5, Section 1, Theorem 1.2. -/ +lemma strictMaximalMinors_aggregate_monotone + {m n q : ℕ} {M : Matrix (Fin m) (Fin n) ℝ} + (hM : M.IsTotallyNonnegRect) + (hminor : + ∀ ⦃rows : Fin q → Fin m⦄ ⦃cols : Fin q → Fin n⦄, + StrictMono rows → StrictMono cols → + 0 < (M.submatrix rows cols).det) + (block : Fin n → Fin q) (hblock : Monotone block) + (weight : Fin n → ℝ) (hweight : ∀ j, 0 ≤ weight j) + (hfiber : ∀ s, ∃ j, block j = s ∧ 0 < weight j) : + ∀ ⦃rows rows' : Fin q → Fin m⦄, + StrictMono rows → StrictMono rows' → + 0 < + (Matrix.submatrix + ((fun i s ↦ ∑ j with block j = s, M i j * weight j) : + Matrix (Fin m) (Fin q) ℝ) rows id).det * + (Matrix.submatrix + ((fun i s ↦ ∑ j with block j = s, M i j * weight j) : + Matrix (Fin m) (Fin q) ℝ) rows' id).det := by + classical + choose selector hselector_block hselector_weight using hfiber + have hselector_mono : StrictMono selector := by + intro a b hab + apply lt_of_not_ge + intro hba + have hle := hblock hba + rw [hselector_block a, hselector_block b] at hle + exact (not_le_of_gt hab) hle + have hselector_mem : + selector ∈ Fintype.piFinset + (fun s : Fin q ↦ Finset.univ.filter fun j ↦ block j = id s) := by + apply Fintype.mem_piFinset.mpr + intro s + simpa using hselector_block s + have hdet_pos (rows : Fin q → Fin m) (hrows : StrictMono rows) : + 0 < + (Matrix.submatrix + ((fun i s ↦ ∑ j with block j = s, M i j * weight j) : + Matrix (Fin m) (Fin q) ℝ) rows id).det := by + rw [det_submatrix_fiberwise_sum] + apply Finset.sum_pos' + · intro r hr + have hrblock : ∀ s, block (r s) = s := by + intro s + simpa using (Fintype.mem_piFinset.mp hr s) + have hrmono : StrictMono r := by + intro a b hab + apply lt_of_not_ge + intro hba + have hle := hblock hba + rw [hrblock a, hrblock b] at hle + exact (not_le_of_gt hab) hle + exact mul_nonneg + (Finset.prod_nonneg fun s _ ↦ hweight (r s)) + (hM hrows hrmono) + · refine ⟨selector, hselector_mem, ?_⟩ + exact mul_pos + (Finset.prod_pos fun s _ ↦ hselector_weight s) + (hminor hrows hselector_mono) + intro rows rows' hrows hrows' + exact mul_pos (hdet_pos rows hrows) (hdet_pos rows' hrows') + /-- A common nonzero sign for all maximal minors makes multiplication by the rectangular matrix injective. This is the rank step in Karlin, Chapter 5, Section 1, Theorem 1.1. -/ From 1dc6287bf7d5b55f8c501a01dc1a2b3a0237a5df Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Sun, 2 Aug 2026 11:37:13 +0000 Subject: [PATCH 5/5] Prove strict variation diminution by sign blocks --- .../Matrix/VariationDiminishing.lean | 71 +++++++++++++++++++ 1 file changed, 71 insertions(+) diff --git a/RealRooted/Mathlib/LinearAlgebra/Matrix/VariationDiminishing.lean b/RealRooted/Mathlib/LinearAlgebra/Matrix/VariationDiminishing.lean index 6eb6f448..d85a440e 100644 --- a/RealRooted/Mathlib/LinearAlgebra/Matrix/VariationDiminishing.lean +++ b/RealRooted/Mathlib/LinearAlgebra/Matrix/VariationDiminishing.lean @@ -365,6 +365,77 @@ theorem signVariations_mulVec_le_card_sub_one_of_strictMaximalMinors (Fin.exists_strictMono_strictlyAlternates_of_le_signVariations hq hlarge) +/-- A totally nonnegative rectangular matrix with all square minors strictly +positive is variation diminishing in the local `S^-` convention. This follows +Karlin, Chapter 5, Section 1, Theorem 1.2: aggregate consecutive sign blocks, +apply Theorem 1.1 to the aggregate, and use the block count. -/ +theorem IsTotallyNonnegRect.signVariations_mulVec_le_of_posMinors + {m n : ℕ} {M : Matrix (Fin m) (Fin n) ℝ} + (hM : M.IsTotallyNonnegRect) + (hminor : + ∀ ⦃q : ℕ⦄ ⦃rows : Fin q → Fin m⦄ ⦃cols : Fin q → Fin n⦄, + StrictMono rows → StrictMono cols → + 0 < (M.submatrix rows cols).det) + (x : Fin n → ℝ) : + Fin.signVariations (M.mulVec x) ≤ Fin.signVariations x := by + classical + by_cases hx : x = 0 + · subst x + simp [Matrix.mulVec, dotProduct] + obtain ⟨D⟩ := Fin.exists_signBlockDecomposition x hx + let weight : Fin n → ℝ := fun j ↦ |x j| + let blockSign : Fin D.blockCount → ℝ := fun s ↦ D.blockSign s + let A : Matrix (Fin m) (Fin D.blockCount) ℝ := + fun i s ↦ ∑ j with D.block j = s, M i j * weight j + have hfactor (j : Fin n) : + weight j * blockSign (D.block j) = x j := by + change |x j| * (D.blockSign (D.block j) : ℝ) = x j + by_cases hj : x j = 0 + · simp [hj] + · rw [← D.sign_eq_blockSign j hj] + exact abs_mul_sign (x j) + have hmul : A.mulVec blockSign = M.mulVec x := by + ext i + rw [Matrix.mulVec, Matrix.mulVec, dotProduct, dotProduct] + simp only [A, Finset.sum_mul] + calc + (∑ s, ∑ j with D.block j = s, + M i j * weight j * blockSign s) = + ∑ s, ∑ j with D.block j = s, M i j * x j := by + apply Finset.sum_congr rfl + intro s _ + apply Finset.sum_congr rfl + intro j hj + have hjblock : D.block j = s := (Finset.mem_filter.mp hj).2 + rw [← hjblock, mul_assoc, hfactor] + _ = ∑ j, M i j * x j := by + simpa using + (Finset.sum_fiberwise Finset.univ D.block + (fun j ↦ M i j * x j)) + have hfiber : ∀ s, ∃ j, D.block j = s ∧ 0 < weight j := by + intro s + obtain ⟨j, hjblock, hj⟩ := D.block_has_nonzero s + exact ⟨j, hjblock, by simpa [weight] using abs_pos.mpr hj⟩ + have hAminor : + ∀ ⦃rows rows' : Fin D.blockCount → Fin m⦄, + StrictMono rows → StrictMono rows' → + 0 < (A.submatrix rows id).det * (A.submatrix rows' id).det := by + simpa only [A] using + strictMaximalMinors_aggregate_monotone hM + (fun ⦃rows cols⦄ hrows hcols ↦ + hminor (rows := rows) (cols := cols) hrows hcols) + D.block D.monotone_block weight (fun j ↦ abs_nonneg (x j)) hfiber + by_cases hqm : D.blockCount ≤ m + · have hout := + signVariations_mulVec_le_card_sub_one_of_strictMaximalMinors + hqm hAminor blockSign + rw [hmul] at hout + simpa [D.blockCount_eq] using hout + · have hcard := Fin.signVariations_le_card_sub_one (M.mulVec x) + have hlt : m < D.blockCount := Nat.lt_of_not_ge hqm + rw [D.blockCount_eq] at hlt + lia + /-- A totally nonnegative rectangular matrix sends a nonnegative vector to a nonnegative vector. This is the positive one-block sector of the forward variation-diminishing argument. -/