diff --git a/RealRooted.lean b/RealRooted.lean index 4bca6b204..1520c8002 100644 --- a/RealRooted.lean +++ b/RealRooted.lean @@ -21,8 +21,11 @@ import RealRooted.AllCombo import RealRooted.Apolarity import RealRooted.Basic import RealRooted.Bezoutian -import RealRooted.BoundarySpecializationRight +import RealRooted.BorceaBranden.Applications.BidiagonalSymbol +import RealRooted.BorceaBranden.Applications.HomogenizeStable +import RealRooted.BorceaBranden.Applications.UnivariateSymbol import RealRooted.BorceaBranden.BoundarySpecialization +import RealRooted.BorceaBranden.FiniteSymbolBasis import RealRooted.BorceaBranden.FiniteSymbolCoefficient import RealRooted.BorceaBranden.FiniteSymbolContraction import RealRooted.BorceaBranden.FiniteSymbolDegree @@ -32,10 +35,7 @@ import RealRooted.BorceaBranden.FiniteSymbolProduct import RealRooted.BorceaBranden.FiniteSymbolReciprocal import RealRooted.BorceaBranden.FiniteSymbolReconstruction import RealRooted.BorceaBranden.FiniteSymbolReconstructionCore -import RealRooted.BorceaBranden.FiniteSymbolBasis -import RealRooted.BorceaBranden.Applications.BidiagonalSymbol -import RealRooted.BorceaBranden.Applications.HomogenizeStable -import RealRooted.BorceaBranden.Applications.UnivariateSymbol +import RealRooted.BoundarySpecializationRight import RealRooted.CauchyInterlacing import RealRooted.Challenges.AissenSchoenbergWhitney import RealRooted.Challenges.BorceaBranden @@ -195,21 +195,35 @@ import RealRooted.Mathlib.Algebra.Polynomial.Homogenize import RealRooted.Mathlib.Algebra.Polynomial.Roots import RealRooted.Mathlib.Algebra.Polynomial.Splits import RealRooted.Mathlib.Analysis.Complex.OpenMapping +import RealRooted.Mathlib.Analysis.SpecialFunctions.ExpIntegral import RealRooted.Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic import RealRooted.Mathlib.Combinatorics.Enumerative.OrderedSubsetPairs +import RealRooted.Mathlib.Data.Fin.Basic +import RealRooted.Mathlib.Data.List.Basic +import RealRooted.Mathlib.Data.List.Destutter import RealRooted.Mathlib.Data.List.Interleave +import RealRooted.Mathlib.Data.List.OfFn import RealRooted.Mathlib.Data.List.Zip import RealRooted.Mathlib.Data.Nat.Cast.Basic import RealRooted.Mathlib.Data.Nat.Choose.Cast import RealRooted.Mathlib.LinearAlgebra.Matrix.Determinant.Basic +import RealRooted.Mathlib.LinearAlgebra.Matrix.Determinant.CauchyBinet +import RealRooted.Mathlib.LinearAlgebra.Matrix.Determinant.Integral +import RealRooted.Mathlib.LinearAlgebra.Matrix.Gaussian import RealRooted.Mathlib.LinearAlgebra.Matrix.KernelSignVariation +import RealRooted.Mathlib.LinearAlgebra.Matrix.SignRegular +import RealRooted.Mathlib.LinearAlgebra.Matrix.SignRegularRankDeficient +import RealRooted.Mathlib.LinearAlgebra.Matrix.SignRegularStrictification +import RealRooted.Mathlib.LinearAlgebra.Matrix.SignRegularVariation import RealRooted.Mathlib.LinearAlgebra.Matrix.SignVariation +import RealRooted.Mathlib.LinearAlgebra.Matrix.SignVariationTopology import RealRooted.Mathlib.LinearAlgebra.Matrix.TotallyNonneg import RealRooted.Mathlib.LinearAlgebra.Matrix.VariationDiminishing +import RealRooted.Mathlib.LinearAlgebra.Vandermonde import RealRooted.MatrixInterlacing -import RealRooted.MultiaffineReciprocalRight import RealRooted.Multiaffine import RealRooted.MultiaffineReciprocal +import RealRooted.MultiaffineReciprocalRight import RealRooted.MultiplierSequence import RealRooted.MultivariateStability import RealRooted.NarayanaTransformation diff --git a/RealRooted/ASWKarlinKernel.lean b/RealRooted/ASWKarlinKernel.lean index 6b19a5816..d69ee4333 100644 --- a/RealRooted/ASWKarlinKernel.lean +++ b/RealRooted/ASWKarlinKernel.lean @@ -2,6 +2,7 @@ import RealRooted.ASWKarlinMatrix import RealRooted.ASWKarlinThreshold import RealRooted.ASWKarlinVariation import RealRooted.ASWKarlinVectors +import RealRooted.Mathlib.LinearAlgebra.Matrix.SignRegularRankDeficient import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.SpecialFunctions.Complex.Arg @@ -120,6 +121,49 @@ lemma complex_root_ne_zero_of_coeff_zero_pos {p : ℝ[X]} {z : ℂ} exact heval linarith +/-- Karlin's repeated matrices force a linear lower bound on the sampled sine +vector's sign variations, up to the fixed two-endpoint perturbation loss. -/ +theorem aswKarlinRepeatedSineVariationLowerBound + {p : ℝ[X]} {z : ℂ} (hz : z ∈ (p.map (algebraMap ℝ ℂ)).roots) + (hdegree : 0 < p.natDegree) (hconst : 0 < p.coeff 0) + (hpf : IsPolyaFreqSeq p.coeff) {order blocks : ℕ} + (horder : 0 < order) (hblocks : 0 < blocks) (him : z.im ≠ 0) : + blocks * order - 1 ≤ + Fin.signVariations + (aswKarlinSineVector z.arg p.natDegree order blocks) + 2 := by + have hwidth : 0 < blocks * (p.natDegree + order - 1) := + Nat.mul_pos hblocks (by lia) + have hcols : + blocks * (p.natDegree + order - 1) + 1 = + (blocks * (p.natDegree + order - 1) - 1) + 2 := by + lia + have hnodal : + ∀ i : Fin (blocks * (p.natDegree + order - 1) - 1), + aswKarlinRootVector z p.natDegree order blocks + (Fin.cast hcols.symm i.succ.castSucc) = 0 → + aswKarlinRootVector z p.natDegree order blocks + (Fin.cast hcols.symm i.castSucc.castSucc) * + aswKarlinRootVector z p.natDegree order blocks + (Fin.cast hcols.symm i.succ.succ) < 0 := by + intro i hi + change (z ^ ((i : ℕ) + 1)).im = 0 at hi + change (z ^ (i : ℕ)).im * (z ^ ((i : ℕ) + 2)).im < 0 + exact + im_pow_mul_im_pow_add_two_neg_of_im_pow_add_one_eq_zero him i hi + have hbound := + Matrix.IsTotallyNonnegRect.card_sub_one_le_signVariations_add_two_of_surjective_of_card_eq + (hpf.aswKarlinMatrix_isTotallyNonnegRect + p.natDegree order blocks) + hcols + (aswKarlinMatrix_mulVec_surjective p.natDegree order blocks + hdegree horder hconst) + (aswKarlinMatrix_mulVec_rootVector hz order blocks hdegree horder) + hnodal + rw [signVariations_aswKarlinRootVector_eq_sine + (complex_root_ne_zero_of_coeff_zero_pos hz hconst) + p.natDegree order blocks] at hbound + exact hbound + /-- A real complex root of a positive-constant PF polynomial lies on the negative real ray. -/ lemma arg_eq_pi_of_real_complex_root_of_isPolyaFreqSeq_coeff {p : ℝ[X]} {z : ℂ} @@ -194,19 +238,83 @@ theorem aswKarlinSectorThreshold_le_abs_arg_of_im_ne_zero_of_classicalInput /-- Karlin's finite-order sector estimate for a nonreal complex root of a positive constant-coefficient PF polynomial. -The checked algebraic inputs above provide the repeated totally nonnegative -coefficient-window matrix, its full row rank from the positive constant -coefficient, and the root-supplied kernel vector. The remaining hard ingredient -is the classical variation-diminishing/sign-regular kernel theorem. -/ +The proof uses the repeated totally nonnegative coefficient-window matrices, +their full row rank, the root-supplied kernel vectors, and the sampled-sine +floor bound. Taking sufficiently many blocks absorbs the fixed two-endpoint +perturbation loss. -/ theorem aswKarlinSectorThreshold_le_abs_arg_of_im_ne_zero {p : ℝ[X]} {z : ℂ} (hz : z ∈ (p.map (algebraMap ℝ ℂ)).roots) (hdegree : 0 < p.natDegree) (hconst : 0 < p.coeff 0) (hpf : IsPolyaFreqSeq p.coeff) {order : ℕ} (horder : 0 < order) (him : z.im ≠ 0) : - aswSectorThreshold p.natDegree order ≤ |z.arg| := - aswKarlinSectorThreshold_le_abs_arg_of_im_ne_zero_of_classicalInput - aswKarlinKernelSignVariationClassicalInput hz hdegree hconst hpf horder - him + aswSectorThreshold p.natDegree order ≤ |z.arg| := by + by_contra hnot + have hθlt : + |z.arg| < aswSectorThreshold p.natDegree order := + lt_of_not_ge hnot + have hden_pos := + aswSectorThreshold_denom_pos p.natDegree order hdegree horder + have hspan_cast : + ((p.natDegree + order - 1 : ℕ) : ℝ) = + (order : ℝ) + p.natDegree - 1 := by + rw [Nat.cast_sub (by lia)] + push_cast + ring + have hmul := mul_lt_mul_of_pos_left hθlt hden_pos + have hnormalize : + ((order : ℝ) + p.natDegree - 1) * + aswSectorThreshold p.natDegree order = + (order : ℝ) * Real.pi := by + rw [aswSectorThreshold] + field_simp [hden_pos.ne'] + rw [hnormalize] at hmul + have hslope_lt : + (((p.natDegree + order - 1 : ℕ) : ℝ) * |z.arg|) / + Real.pi < (order : ℝ) := by + apply (div_lt_iff₀ Real.pi_pos).2 + rw [hspan_cast] + exact hmul + let gap : ℝ := + (order : ℝ) - + (((p.natDegree + order - 1 : ℕ) : ℝ) * |z.arg|) / Real.pi + have hgap : 0 < gap := by + dsimp [gap] + linarith + obtain ⟨blocks, hblocks⟩ := exists_nat_gt (3 / gap) + have hblocks_pos : 0 < blocks := by + have hfrac : (0 : ℝ) < 3 / gap := by positivity + exact_mod_cast hfrac.trans hblocks + have hlarge : (3 : ℝ) < (blocks : ℝ) * gap := by + have hmulGap := mul_lt_mul_of_pos_right hblocks hgap + rw [div_mul_cancel₀ _ hgap.ne'] at hmulGap + exact hmulGap + have hlower := + aswKarlinRepeatedSineVariationLowerBound + hz hdegree hconst hpf horder hblocks_pos him + have hupper := + signVariations_aswKarlinSineVector_le_floor_div_pi_abs + z.arg p.natDegree order blocks + let x : ℝ := + (((blocks * (p.natDegree + order - 1) : ℕ) : ℝ) * |z.arg|) / + Real.pi + have hnat : blocks * order ≤ ⌊x⌋₊ + 3 := by + dsimp [x] + lia + have hcast : ((blocks * order : ℕ) : ℝ) ≤ (⌊x⌋₊ : ℝ) + 3 := by + exact_mod_cast hnat + have hfloor : (⌊x⌋₊ : ℝ) ≤ x := Nat.floor_le (by dsimp [x]; positivity) + have hx_eq : + x = + (blocks : ℝ) * + ((((p.natDegree + order - 1 : ℕ) : ℝ) * |z.arg|) / + Real.pi) := by + dsimp [x] + push_cast + ring + rw [hx_eq] at hcast hfloor + dsimp [gap] at hlarge + push_cast at hcast + linarith /-- Conditional Karlin finite-order sector estimate for one complex root, with the classical sign-variation input supplied explicitly. -/ @@ -231,8 +339,12 @@ theorem aswKarlinSectorThreshold_le_abs_arg {p : ℝ[X]} {z : ℂ} (hz : z ∈ (p.map (algebraMap ℝ ℂ)).roots) (hdegree : 0 < p.natDegree) (hconst : 0 < p.coeff 0) (hpf : IsPolyaFreqSeq p.coeff) {order : ℕ} (horder : 0 < order) : - aswSectorThreshold p.natDegree order ≤ |z.arg| := - aswKarlinSectorThreshold_le_abs_arg_of_classicalInput - aswKarlinKernelSignVariationClassicalInput hz hdegree hconst hpf horder + aswSectorThreshold p.natDegree order ≤ |z.arg| := by + by_cases him : z.im = 0 + · rw [arg_eq_pi_of_real_complex_root_of_isPolyaFreqSeq_coeff hz hconst hpf him, + abs_of_pos Real.pi_pos] + exact aswSectorThreshold_le_pi p.natDegree order hdegree horder + · exact aswKarlinSectorThreshold_le_abs_arg_of_im_ne_zero + hz hdegree hconst hpf horder him end RealRooted diff --git a/RealRooted/ASWKarlinSineBounds.lean b/RealRooted/ASWKarlinSineBounds.lean index d769962f4..4d11953d9 100644 --- a/RealRooted/ASWKarlinSineBounds.lean +++ b/RealRooted/ASWKarlinSineBounds.lean @@ -226,6 +226,50 @@ lemma signVariations_sin_mul_lt_of_last_le_nat_mul_pi simp [k] exact lt_trans hlt hk_lt +/-- The sampled sine vector has at most the number of completed half-turns in +its final angle. -/ +lemma signVariations_sin_mul_le_floor_div_pi + {N : ℕ} {θ : ℝ} (hθ0 : 0 ≤ θ) : + Fin.signVariations + (fun j : Fin (N + 1) => Real.sin ((j : ℕ) * θ)) ≤ + ⌊((N : ℝ) * θ) / Real.pi⌋₊ := by + let r : ℕ := ⌊((N : ℝ) * θ) / Real.pi⌋₊ + have hquot : + ((N : ℝ) * θ) / Real.pi < ((r + 1 : ℕ) : ℝ) := by + simpa only [r, Nat.cast_add, Nat.cast_one] using + Nat.lt_floor_add_one (((N : ℝ) * θ) / Real.pi) + have hlast : + (N : ℝ) * θ ≤ ((r + 1 : ℕ) : ℝ) * Real.pi := by + have hmul := mul_lt_mul_of_pos_right hquot Real.pi_pos + rw [div_mul_cancel₀ _ Real.pi_ne_zero] at hmul + exact hmul.le + have hlt := + signVariations_sin_mul_lt_of_last_le_nat_mul_pi + (N := N) (order := r + 1) (by positivity) hθ0 hlast + exact Nat.lt_succ_iff.mp + (by simpa only [Nat.succ_eq_add_one] using hlt) + +/-- Absolute-angle form of the sampled-sine floor bound for Karlin's repeated +vector. -/ +lemma signVariations_aswKarlinSineVector_le_floor_div_pi_abs + (θ : ℝ) (degree order blocks : ℕ) : + Fin.signVariations (aswKarlinSineVector θ degree order blocks) ≤ + ⌊(((blocks * (degree + order - 1) : ℕ) : ℝ) * |θ|) / + Real.pi⌋₊ := by + by_cases hθ : 0 ≤ θ + · rw [abs_of_nonneg hθ] + change Fin.signVariations + (fun j : Fin (blocks * (degree + order - 1) + 1) => + Real.sin ((j : ℕ) * θ)) ≤ _ + exact signVariations_sin_mul_le_floor_div_pi hθ + · have hθneg : θ < 0 := lt_of_not_ge hθ + rw [← signVariations_aswKarlinSineVector_neg θ degree order blocks, + abs_of_neg hθneg] + change Fin.signVariations + (fun j : Fin (blocks * (degree + order - 1) + 1) => + Real.sin ((j : ℕ) * -θ)) ≤ _ + exact signVariations_sin_mul_le_floor_div_pi (neg_nonneg.mpr hθneg.le) + /-- One-block Karlin sine vectors inherit the general sampled-sine sign-variation bound from a last-angle estimate. -/ lemma signVariations_aswKarlinSineVector_lt_of_last_le_order_pi diff --git a/RealRooted/ASWKarlinVariation.lean b/RealRooted/ASWKarlinVariation.lean index bc077c242..6c5c16ea4 100644 --- a/RealRooted/ASWKarlinVariation.lean +++ b/RealRooted/ASWKarlinVariation.lean @@ -63,31 +63,6 @@ theorem IsPolyaFreqSeq.aswKarlinKernelSignVariationLowerBound_of_classicalInput exact hclassical hdegree horder hconst hlead hsupport htn hsurj hker hvec_ne -/-- Remaining classical sign-regular kernel lower bound for a full-row-rank -totally nonnegative one-block Karlin coefficient-window matrix. - -This is the only remaining non-elementary input in the current Karlin sector -proof. It should eventually be proved from the specialized sign-regular -variation-diminishing theorem for a full-row-rank totally nonnegative Toeplitz -window matrix. -/ -theorem aswKarlinKernelSignVariationClassicalInput : - AswKarlinKernelSignVariationClassicalInputStatement := by - intro u degree order hdegree horder hconst hlead hsupport htn hsurj v hker hvec_ne - -- Remaining classical step: use `htn`, `hsurj`, the endpoint/support data, - -- `hker`, and `hvec_ne` to prove the kernel sign-variation lower bound. - sorry - -/-- Classical sign-regular kernel lower bound for a PF one-block Karlin -coefficient-window matrix. -/ -theorem IsPolyaFreqSeq.aswKarlinKernelSignVariationLowerBound - {u : ℕ → ℝ} (hpf : IsPolyaFreqSeq u) (degree order : ℕ) - (hdegree : 0 < degree) (horder : 0 < order) (hconst : 0 < u 0) - (hlead : 0 < u degree) (hsupport : ∀ k, degree < k → u k = 0) : - AswKarlinKernelSignVariationLowerBound degree order u := by - exact hpf.aswKarlinKernelSignVariationLowerBound_of_classicalInput - aswKarlinKernelSignVariationClassicalInput degree order hdegree horder - hconst hlead hsupport - /-- The final sector inequality follows once the two sign-variation bounds are available: a lower bound from the full-row-rank TN kernel theorem and an upper bound for the sampled sine vector inside the forbidden sector. -/ diff --git a/RealRooted/ASWKarlinVectors.lean b/RealRooted/ASWKarlinVectors.lean index 64dc177f0..e8e10e674 100644 --- a/RealRooted/ASWKarlinVectors.lean +++ b/RealRooted/ASWKarlinVectors.lean @@ -46,6 +46,72 @@ lemma im_pow_eq_norm_pow_mul_sin_arg (z : ℂ) (n : ℕ) : Complex.exp_im] simp +/-- If a nonreal complex geometric progression has an interior zero imaginary +part, the adjacent imaginary parts have opposite strict signs. -/ +lemma im_pow_mul_im_pow_add_two_neg_of_im_pow_add_one_eq_zero + {z : ℂ} (him : z.im ≠ 0) (i : ℕ) + (hzero : (z ^ (i + 1)).im = 0) : + (z ^ i).im * (z ^ (i + 2)).im < 0 := by + let θ := z.arg + have hz : z ≠ 0 := by + intro hz + apply him + simp [hz] + have hnorm : 0 < ‖z‖ := norm_pos_iff.mpr hz + have hsin : Real.sin θ ≠ 0 := by + have hpolar := im_pow_eq_norm_pow_mul_sin_arg z 1 + simp only [pow_one, Nat.cast_one, one_mul] at hpolar + intro hs + apply him + rw [hpolar, hs, mul_zero] + have hzeroSin : Real.sin ((i + 1 : ℕ) * θ) = 0 := by + rw [im_pow_eq_norm_pow_mul_sin_arg] at hzero + exact (mul_eq_zero.mp hzero).resolve_left (pow_ne_zero _ hnorm.ne') + have hcos : Real.cos ((i + 1 : ℕ) * θ) ≠ 0 := by + intro hc + have hsq := Real.sin_sq_add_cos_sq ((i + 1 : ℕ) * θ) + rw [hzeroSin, hc] at hsq + norm_num at hsq + have hprev : + Real.sin (i * θ) = + -Real.cos ((i + 1 : ℕ) * θ) * Real.sin θ := by + have harg : + (i : ℝ) * θ = ((i + 1 : ℕ) : ℝ) * θ - θ := by + push_cast + ring + rw [harg, Real.sin_sub, hzeroSin] + ring + have hnext : + Real.sin ((i + 2 : ℕ) * θ) = + Real.cos ((i + 1 : ℕ) * θ) * Real.sin θ := by + have harg : + ((i + 2 : ℕ) : ℝ) * θ = + ((i + 1 : ℕ) : ℝ) * θ + θ := by + push_cast + ring + rw [harg, Real.sin_add, hzeroSin] + ring + have htrig : + Real.sin (i * θ) * Real.sin ((i + 2 : ℕ) * θ) < 0 := by + rw [hprev, hnext] + calc + (-Real.cos ((i + 1 : ℕ) * θ) * Real.sin θ) * + (Real.cos ((i + 1 : ℕ) * θ) * Real.sin θ) = + -(Real.cos ((i + 1 : ℕ) * θ) ^ 2 * Real.sin θ ^ 2) := by + ring + _ < 0 := neg_lt_zero.mpr + (mul_pos (sq_pos_of_ne_zero hcos) (sq_pos_of_ne_zero hsin)) + rw [im_pow_eq_norm_pow_mul_sin_arg, + im_pow_eq_norm_pow_mul_sin_arg] + calc + (‖z‖ ^ i * Real.sin (i * θ)) * + (‖z‖ ^ (i + 2) * Real.sin ((i + 2 : ℕ) * θ)) = + (‖z‖ ^ i * ‖z‖ ^ (i + 2)) * + (Real.sin (i * θ) * Real.sin ((i + 2 : ℕ) * θ)) := by + ring + _ < 0 := mul_neg_of_pos_of_neg + (mul_pos (pow_pos hnorm _) (pow_pos hnorm _)) htrig + /-- A nonzero complex number's root vector and sampled sine vector have the same coordinate signs. -/ lemma signVariations_aswKarlinRootVector_eq_sine {z : ℂ} (hz : z ≠ 0) diff --git a/RealRooted/AissenSchoenbergWhitney.lean b/RealRooted/AissenSchoenbergWhitney.lean index 6aded912b..f4c44b771 100644 --- a/RealRooted/AissenSchoenbergWhitney.lean +++ b/RealRooted/AissenSchoenbergWhitney.lean @@ -301,9 +301,12 @@ theorem aswSectorThreshold_le_abs_arg_of_isPolyaFreqSeq_coeff {p : ℝ[X]} {z : (hdegree : 0 < p.natDegree) (hconst : 0 < p.coeff 0) (hpf : IsPolyaFreqSeq p.coeff) (hz : z ∈ (p.map (algebraMap ℝ ℂ)).roots) (order : ℕ) : - aswSectorThreshold p.natDegree order ≤ |z.arg| := - aswSectorThreshold_le_abs_arg_of_isPolyaFreqSeq_coeff_of_classicalInput - aswKarlinKernelSignVariationClassicalInput hdegree hconst hpf hz order + aswSectorThreshold p.natDegree order ≤ |z.arg| := by + by_cases horder : order = 0 + · simp [aswSectorThreshold, horder] + · exact aswKarlinSectorThreshold_le_abs_arg + (p := p) (z := z) hz hdegree hconst hpf + (horder := Nat.pos_of_ne_zero horder) /-! ### Reduction to positive constant coefficient -/ diff --git a/RealRooted/CommonInterleaver/PairBridge.lean b/RealRooted/CommonInterleaver/PairBridge.lean index d6a2178ee..c19fb4996 100644 --- a/RealRooted/CommonInterleaver/PairBridge.lean +++ b/RealRooted/CommonInterleaver/PairBridge.lean @@ -1126,6 +1126,14 @@ theorem posComboNoCommonSuccDegreeSlotData_of_forward_asw_and_rootCrossing posComboNoCommonSuccDegreeSlotData_of_leftSplits_and_rootCrossing (PosComboSuccDegreeLeftSplitsNonnegStatement_of_forward_asw hASW) hcross +/-- Succ-degree slot data from the proved ASW left endpoint and the +descending-root crossing inequalities. -/ +theorem posComboNoCommonSuccDegreeSlotData_of_asw_and_rootCrossing + (hcross : PosComboNoCommonSuccDegreeRootCrossingNonnegStatement) : + PosComboNoCommonSuccDegreeSlotDataNonnegStatement := + posComboNoCommonSuccDegreeSlotData_of_leftSplits_and_rootCrossing + PosComboSuccDegreeLeftSplitsNonnegStatement_of_asw hcross + /-- Succ-degree slot data from the splitting-only ASW target and the root-crossing target. -/ theorem posComboNoCommonSuccDegreeSlotData_of_forward_asw_splits_and_rootCrossing @@ -1145,6 +1153,14 @@ theorem succDegreePairHasCommonInterleaver_nonneg_of_leftSplits_and_rootCrossing (PosComboSuccDegreeLeftSplitsNonnegStatement_of_forward_asw hASW) hcross +/-- Succ-degree pair interleavers from the proved ASW left endpoint and the +descending-root crossing inequalities. -/ +theorem succDegreePairHasCommonInterleaver_nonneg_of_asw_and_rootCrossing + (hcross : PosComboNoCommonSuccDegreeRootCrossingNonnegStatement) : + PosComboNoCommonSuccDegreePairHasCommonInterleaverNonnegStatement := + succDegreePairHasCommonInterleaver_nonneg_of_leftSplits_and_rootCrossing + PosComboSuccDegreeLeftSplitsNonnegStatement_of_asw hcross + /-- Succ-degree pair interleavers from the splitting-only ASW target and the root-crossing target. -/ theorem diff --git a/RealRooted/CommonInterleaver/SuccDegreeEndpoint.lean b/RealRooted/CommonInterleaver/SuccDegreeEndpoint.lean index 6f9c7672f..cd1af54c6 100644 --- a/RealRooted/CommonInterleaver/SuccDegreeEndpoint.lean +++ b/RealRooted/CommonInterleaver/SuccDegreeEndpoint.lean @@ -251,6 +251,25 @@ theorem PosComboRealRooted.left_splits_of_forward_asw hASW hf_pos.ne_zero hfnn hgnn fun {_} hμ => (hfg.isRealRooted_add_right hμ).2 +/-- The succ-degree left endpoint from the proved forward ASW theorem, with no +backend argument required from the caller. -/ +theorem PosComboRealRooted.left_splits_of_asw + {f g : ℝ[X]} + (hfg : PosComboRealRooted f g) + (hf_pos : HasPosLeadingCoeff f) + (hfnn : HasNonnegCoeffs f) (hgnn : HasNonnegCoeffs g) : + f.Splits := + IsPFPolynomial.splits_of_forall_pos_add_C_mul + hf_pos.ne_zero hfnn hgnn + fun {_} hμ => (hfg.isRealRooted_add_right hμ).2 + +/-- Unconditional package form of `PosComboRealRooted.left_splits_of_asw` for +the milestone-B2 endpoint statement. -/ +theorem PosComboSuccDegreeLeftSplitsNonnegStatement_of_asw : + PosComboSuccDegreeLeftSplitsNonnegStatement := by + intro f g hf_pos _ hfnn hgnn hfg _ + exact hfg.left_splits_of_asw hf_pos hfnn hgnn + /-- Conditional package form of `PosComboRealRooted.left_splits_of_forward_asw` for the milestone-B2 endpoint statement. -/ theorem PosComboSuccDegreeLeftSplitsNonnegStatement_of_forward_asw diff --git a/RealRooted/Hadamard.lean b/RealRooted/Hadamard.lean index 84e615737..2386ff783 100644 --- a/RealRooted/Hadamard.lean +++ b/RealRooted/Hadamard.lean @@ -3526,6 +3526,15 @@ theorem polyaFrequencyHadamardCoeff_of_schurPolyaWagner (hSPW (IsPFPolynomial.of_sequence hASW hp) (IsPFPolynomial.of_sequence hASW hq)).to_sequence +/-- Polynomial-coefficient Pólya-frequency closure from Schur--Pólya--Wagner, +using the proved forward ASW theorem rather than a caller-supplied backend. -/ +theorem polyaFrequencyHadamardCoeff_of_schurPolyaWagner_asw + (hSPW : schurPolyaWagnerHadamardPFStatement) : + polyaFrequencyHadamardCoeffStatement := + fun hp hq => + (hSPW (IsPFPolynomial.of_polyaFreqSeq hp) + (IsPFPolynomial.of_polyaFreqSeq hq)).to_sequence + theorem polyaFrequencyHadamardCoeff_of_garloffWagner_prec0 (hASW : aissenSchoenbergWhitneyForwardOrZeroStatement) (hGW : garloffWagnerHadamardPFPrec0Statement) : diff --git a/RealRooted/Mathlib/Analysis/SpecialFunctions/ExpIntegral.lean b/RealRooted/Mathlib/Analysis/SpecialFunctions/ExpIntegral.lean new file mode 100644 index 000000000..23e1803dc --- /dev/null +++ b/RealRooted/Mathlib/Analysis/SpecialFunctions/ExpIntegral.lean @@ -0,0 +1,30 @@ +module + +public import Mathlib.Analysis.SpecialFunctions.ExpDeriv +public import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus + +/-! +# Interval integrals of exponential functions + +This file contains a fundamental-theorem-of-calculus identity for exponential +differences. +-/ + +public section + +open scoped Interval + +namespace Real + +/-- The integral form of the adjacent-difference identity for the exponential kernel. -/ +theorem intervalIntegral_mul_exp_mul (a b z : ℝ) : + (∫ t in a..b, z * exp (t * z)) = exp (b * z) - exp (a * z) := by + apply intervalIntegral.integral_eq_sub_of_hasDerivAt + · intro t _ + simpa [Function.comp_def, mul_comm] using + (Real.hasDerivAt_exp (t * z)).comp t ((hasDerivAt_id t).mul_const z) + · exact + (continuous_const.mul + (Real.continuous_exp.comp (continuous_id.mul continuous_const))).intervalIntegrable _ _ + +end Real diff --git a/RealRooted/Mathlib/Data/Fin/Basic.lean b/RealRooted/Mathlib/Data/Fin/Basic.lean new file mode 100644 index 000000000..6fa9625d2 --- /dev/null +++ b/RealRooted/Mathlib/Data/Fin/Basic.lean @@ -0,0 +1,113 @@ +module + +public import Mathlib.Data.Fin.SuccPred + +/-! +# Additional lemmas about finite indices + +This file contains compatibility lemmas intended for upstreaming to +`Mathlib.Data.Fin.Basic`. +-/ + +public section + +namespace Fin + +/-- `succAbove` preserves three consecutive coordinates lying before the omitted index. -/ +theorem succAbove_triple_eq_castSucc_of_right_lt + {n : ℕ} (p : Fin (n + 3)) (i : Fin n) + (h : i.succ.succ.castSucc < p) : + p.succAbove i.castSucc.castSucc = i.castSucc.castSucc.castSucc ∧ + p.succAbove i.succ.castSucc = i.succ.castSucc.castSucc ∧ + p.succAbove i.succ.succ = i.succ.succ.castSucc := by + change (i : ℕ) + 2 < (p : ℕ) at h + have hleft : i.castSucc.castSucc.castSucc < p := by + change (i : ℕ) < (p : ℕ) + lia + have hcenter : i.succ.castSucc.castSucc < p := by + change (i : ℕ) + 1 < (p : ℕ) + lia + exact ⟨Fin.succAbove_of_castSucc_lt p _ hleft, + Fin.succAbove_of_castSucc_lt p _ hcenter, + Fin.succAbove_of_castSucc_lt p _ h⟩ + +/-- `succAbove` shifts three consecutive coordinates lying after the omitted index. -/ +theorem succAbove_triple_eq_succ_of_le_left + {n : ℕ} (p : Fin (n + 3)) (i : Fin n) + (h : p ≤ i.castSucc.castSucc.castSucc) : + p.succAbove i.castSucc.castSucc = i.castSucc.castSucc.succ ∧ + p.succAbove i.succ.castSucc = i.succ.castSucc.succ ∧ + p.succAbove i.succ.succ = i.succ.succ.succ := by + change (p : ℕ) ≤ (i : ℕ) at h + have hcenter : p ≤ i.succ.castSucc.castSucc := by + change (p : ℕ) ≤ (i : ℕ) + 1 + lia + have hright : p ≤ i.succ.succ.castSucc := by + change (p : ℕ) ≤ (i : ℕ) + 2 + lia + exact ⟨Fin.succAbove_of_le_castSucc p _ h, + Fin.succAbove_of_le_castSucc p _ hcenter, + Fin.succAbove_of_le_castSucc p _ hright⟩ + +/-- Omitting an interior center sends the corresponding new center to its old right +neighbor. -/ +theorem succAbove_center_eq_right (i : Fin n) : + (i.succ.castSucc.castSucc).succAbove i.succ.castSucc = + i.succ.succ.castSucc := by + rw [Fin.succAbove_of_le_castSucc _ _ (by + change (i : ℕ) + 1 ≤ (i : ℕ) + 1 + exact Nat.le_refl _)] + congr + +/-- Omitting the old right neighbor sends the corresponding new center to its old value. -/ +theorem succAbove_center_eq_left (i : Fin n) : + (i.succ.succ.castSucc).succAbove i.succ.castSucc = + i.succ.castSucc.castSucc := by + rw [Fin.succAbove_of_castSucc_lt _ _ (by + change (i : ℕ) + 1 < (i : ℕ) + 2 + lia)] + +/-- Deleting an interior full-vector coordinate agrees with deleting its +corresponding interior coordinate. -/ +theorem succAbove_succ_castSucc + {n : ℕ} (k : Fin (n + 1)) (i : Fin n) : + k.succ.castSucc.succAbove i.succ.castSucc = + (k.succAbove i).succ.castSucc := by + by_cases h : i.castSucc < k + · have h' : i.succ.castSucc.castSucc < k.succ.castSucc := by + change (i : ℕ) + 1 < (k : ℕ) + 1 + exact Nat.succ_lt_succ h + rw [Fin.succAbove_of_castSucc_lt _ _ h', + Fin.succAbove_of_castSucc_lt _ _ h] + exact Fin.ext rfl + · have hki : k ≤ i.castSucc := by + change (k : ℕ) ≤ (i : ℕ) + change ¬(i : ℕ) < (k : ℕ) at h + exact Nat.le_of_not_gt h + have h' : k.succ.castSucc ≤ i.succ.castSucc.castSucc := by + change (k : ℕ) + 1 ≤ (i : ℕ) + 1 + exact Nat.succ_le_succ hki + rw [Fin.succAbove_of_le_castSucc _ _ h', + Fin.succAbove_of_le_castSucc _ _ hki] + exact Fin.ext rfl + +/-- Deleting an interior coordinate preserves the first coordinate. -/ +theorem succAbove_zero_of_interior + {n : ℕ} (k : Fin (n + 1)) : + k.succ.castSucc.succAbove (0 : Fin (n + 2)) = 0 := by + rw [Fin.succAbove_of_castSucc_lt _ _ (by + change 0 < (k : ℕ) + 1 + lia)] + exact Fin.ext rfl + +/-- Deleting an interior coordinate preserves the final coordinate. -/ +theorem succAbove_last_of_interior + {n : ℕ} (k : Fin (n + 1)) : + k.succ.castSucc.succAbove (Fin.last (n + 1)) = + Fin.last (n + 2) := by + rw [Fin.succAbove_of_le_castSucc _ _ (by + change (k : ℕ) + 1 ≤ n + 1 + lia)] + exact Fin.ext rfl + +end Fin diff --git a/RealRooted/Mathlib/Data/List/Basic.lean b/RealRooted/Mathlib/Data/List/Basic.lean new file mode 100644 index 000000000..b14f55fe3 --- /dev/null +++ b/RealRooted/Mathlib/Data/List/Basic.lean @@ -0,0 +1,38 @@ +module + +public import Mathlib.Data.List.Basic + +/-! +# Additional basic list lemmas + +This file contains compatibility lemmas intended for upstreaming to +`Mathlib.Data.List.Basic`. +-/ + +public section + +namespace List + +/-- Erasing an entry rejected by a filter does not change the filtered list. -/ +theorem filter_eraseIdx_eq_of_getElem_not + {α : Type*} {p : α → Bool} {l : List α} {i : ℕ} + (hi : i < l.length) (hpi : ¬p l[i]) : + (l.eraseIdx i).filter p = l.filter p := by + rw [eraseIdx_eq_take_drop_succ, filter_append] + conv_rhs => + rw [← take_append_drop i l, filter_append, + drop_eq_getElem_cons hi, filter_cons_of_neg hpi] + +/-- Erasing an index inside the middle block of a three-block concatenation. -/ +theorem eraseIdx_append_middle + {α : Type*} (pre middle post : List α) (i : ℕ) + (hi : i < middle.length) : + (pre ++ middle ++ post).eraseIdx (pre.length + i) = + pre ++ middle.eraseIdx i ++ post := by + rw [append_assoc, + eraseIdx_append_of_length_le (by simp), + Nat.add_sub_cancel_left, + eraseIdx_append_of_lt_length hi, + append_assoc] + +end List diff --git a/RealRooted/Mathlib/Data/List/Destutter.lean b/RealRooted/Mathlib/Data/List/Destutter.lean new file mode 100644 index 000000000..c08af3b4e --- /dev/null +++ b/RealRooted/Mathlib/Data/List/Destutter.lean @@ -0,0 +1,195 @@ +module + +public import Mathlib.Data.List.Destutter + +/-! +# Additional lemmas about list destuttering + +This file contains compatibility lemmas intended for upstreaming to +`Mathlib.Data.List.Destutter`. +-/ + +public section + +namespace List + +private theorem singleton_prefix_destutter' + {α : Type*} (R : α → α → Prop) [DecidableRel R] + (a : α) (l : List α) : + [a] <+: l.destutter' R a := by + induction l generalizing a with + | nil => + exact ⟨[], rfl⟩ + | cons b l ih => + rw [List.destutter'_cons] + by_cases hab : R a b + · rw [if_pos hab] + exact ⟨l.destutter' R b, rfl⟩ + · rw [if_neg hab] + exact ih a + +private theorem destutter'_prefix_append + {α : Type*} (R : α → α → Prop) [DecidableRel R] + (a : α) (l t : List α) : + l.destutter' R a <+: (l ++ t).destutter' R a := by + induction l generalizing a with + | nil => + exact singleton_prefix_destutter' R a t + | cons b l ih => + simp only [List.cons_append] + rw [List.destutter'_cons, List.destutter'_cons] + by_cases hab : R a b + · rw [if_pos hab, if_pos hab] + rcases ih b with ⟨u, hu⟩ + exact ⟨u, by simpa using congrArg (List.cons a) hu⟩ + · rw [if_neg hab, if_neg hab] + exact ih a + +private theorem destutter_prefix_append + {α : Type*} (R : α → α → Prop) [DecidableRel R] + (l t : List α) : + l.destutter R <+: (l ++ t).destutter R := by + cases l with + | nil => + exact ⟨t.destutter R, by simp⟩ + | cons a l => + exact destutter'_prefix_append R a l t + +/-- Destuttering preserves list prefixhood. -/ +theorem IsPrefix.destutter + {α : Type*} {R : α → α → Prop} [DecidableRel R] + {l₁ l₂ : List α} (h : l₁ <+: l₂) : + l₁.destutter R <+: l₂.destutter R := by + rcases h with ⟨t, rfl⟩ + exact destutter_prefix_append R l₁ t + +private theorem getLast?_cons_eq_tail_of_ne_nil + {α : Type*} {a : α} {l : List α} (hl : l ≠ []) : + (a :: l).getLast? = l.getLast? := by + rw [List.getLast?_cons, List.getLast?_eq_some_getLast hl] + simp + +private theorem getLast?_destutter'_ne + {α : Type*} [DecidableEq α] (a : α) (l : List α) : + (l.destutter' (· ≠ ·) a).getLast? = + (a :: l).getLast? := by + induction l generalizing a with + | nil => + simp + | cons b l ih => + rw [List.destutter'_cons] + by_cases hab : a ≠ b + · rw [if_pos hab] + calc + (a :: l.destutter' (· ≠ ·) b).getLast? = + (l.destutter' (· ≠ ·) b).getLast? := + getLast?_cons_eq_tail_of_ne_nil (List.destutter'_ne_nil _ _) + _ = (b :: l).getLast? := ih b + _ = (a :: b :: l).getLast? := + (getLast?_cons_eq_tail_of_ne_nil (by simp)).symm + · have hab_eq : a = b := not_ne_iff.mp hab + subst b + rw [if_neg (by simp)] + calc + (l.destutter' (· ≠ ·) a).getLast? = + (a :: l).getLast? := ih a + _ = (a :: a :: l).getLast? := + (getLast?_cons_eq_tail_of_ne_nil (by simp)).symm + +/-- Destuttering by disequality preserves the final element. -/ +theorem getLast?_destutter_ne + {α : Type*} [DecidableEq α] (l : List α) : + (l.destutter (· ≠ ·)).getLast? = l.getLast? := by + cases l with + | nil => + simp + | cons a l => + exact getLast?_destutter'_ne a l + +/-- Equal-length destuttered prefixes have the same final element. -/ +theorem IsPrefix.getLast?_eq_of_destutter_length_le + {α : Type*} [DecidableEq α] + {l₁ l₂ : List α} (h : l₁ <+: l₂) + (hlen : + (l₂.destutter (· ≠ ·)).length ≤ + (l₁.destutter (· ≠ ·)).length) : + l₁.getLast? = l₂.getLast? := by + have heq : + l₁.destutter (· ≠ ·) = + l₂.destutter (· ≠ ·) := + (h.destutter (R := fun x y : α => x ≠ y)).eq_of_length_le hlen + simpa only [List.getLast?_destutter_ne] using + congrArg List.getLast? heq + +private theorem destutter'_append_cons_self_ne + {α : Type*} [DecidableEq α] (b a : α) (l₁ l₂ : List α) : + (l₁ ++ a :: a :: l₂).destutter' (· ≠ ·) b = + (l₁ ++ a :: l₂).destutter' (· ≠ ·) b := by + induction l₁ generalizing b with + | nil => + by_cases hba : b = a + · subst b + simp + · simp [hba] + | cons c l ih => + simp only [cons_append, List.destutter'_cons] + by_cases hbc : b ≠ c + · rw [if_pos hbc, if_pos hbc, ih c] + · rw [if_neg hbc, if_neg hbc, ih b] + +/-- Deleting one of two adjacent equal entries does not change disequality destuttering. -/ +theorem destutter_append_cons_self_ne + {α : Type*} [DecidableEq α] (l₁ l₂ : List α) (a : α) : + (l₁ ++ a :: a :: l₂).destutter (· ≠ ·) = + (l₁ ++ a :: l₂).destutter (· ≠ ·) := by + cases l₁ with + | nil => + simp [List.destutter_cons'] + | cons b l => + simp only [cons_append, List.destutter_cons'] + exact destutter'_append_cons_self_ne b a l l₂ + +/-- Deleting the second of two adjacent equal entries after a fixed entry does not change +disequality destuttering. -/ +theorem destutter_append_cons_cons_self_ne + {α : Type*} [DecidableEq α] (l₁ l₂ : List α) (a b : α) : + (l₁ ++ a :: b :: b :: l₂).destutter (· ≠ ·) = + (l₁ ++ a :: b :: l₂).destutter (· ≠ ·) := by + simpa only [append_assoc, singleton_append] using + destutter_append_cons_self_ne (l₁ ++ [a]) l₂ b + +/-- Prepending an entry increases the length after disequality destuttering by at most one. -/ +theorem length_destutter_cons_ne_le_succ + {α : Type*} [DecidableEq α] (a : α) (l : List α) : + ((a :: l).destutter (· ≠ ·)).length ≤ + (l.destutter (· ≠ ·)).length + 1 := by + cases l with + | nil => simp + | cons b l => + simp only [List.destutter_cons', List.destutter'_cons] + split_ifs <;> simp_all + +private theorem length_destutter'_append_singleton_ne_le_succ + {α : Type*} [DecidableEq α] (b a : α) (l : List α) : + ((l ++ [a]).destutter' (· ≠ ·) b).length ≤ + (l.destutter' (· ≠ ·) b).length + 1 := by + induction l generalizing b with + | nil => + simp [List.destutter'_cons] + split_ifs <;> simp + | cons c l ih => + simp only [cons_append, List.destutter'_cons] + split_ifs <;> simp_all + +/-- Appending an entry increases the length after disequality destuttering by at most one. -/ +theorem length_destutter_append_singleton_ne_le_succ + {α : Type*} [DecidableEq α] (l : List α) (a : α) : + ((l ++ [a]).destutter (· ≠ ·)).length ≤ + (l.destutter (· ≠ ·)).length + 1 := by + cases l with + | nil => simp + | cons b l => + simp only [cons_append, List.destutter_cons'] + exact length_destutter'_append_singleton_ne_le_succ b a l + +end List diff --git a/RealRooted/Mathlib/Data/List/OfFn.lean b/RealRooted/Mathlib/Data/List/OfFn.lean new file mode 100644 index 000000000..904129d6d --- /dev/null +++ b/RealRooted/Mathlib/Data/List/OfFn.lean @@ -0,0 +1,61 @@ +module + +public import Mathlib.Data.List.OfFn +public import RealRooted.Mathlib.Data.Fin.Basic + +/-! +# Additional lemmas about lists of finite functions + +This file contains compatibility lemmas intended for upstreaming to +`Mathlib.Data.List.OfFn`. +-/ + +public section + +namespace List + +/-- Removing a finite-function coordinate agrees with erasing that list index. -/ +theorem ofFn_succAbove_eq_eraseIdx + {α : Type*} {n : ℕ} + (f : Fin (n + 1) → α) (p : Fin (n + 1)) : + List.ofFn (fun i : Fin n => f (p.succAbove i)) = + (List.ofFn f).eraseIdx p := by + apply List.ext_getElem + · simp [List.length_eraseIdx, p.isLt] + · intro i hi₁ _ + simp only [List.getElem_ofFn, List.getElem_eraseIdx] + split + · rw [Fin.succAbove_of_castSucc_lt p _ (by + change i < (p : ℕ) + exact ‹i < (p : ℕ)›)] + congr + · rw [Fin.succAbove_of_le_castSucc p _ (by + change (p : ℕ) ≤ i + exact Nat.le_of_not_gt ‹¬i < (p : ℕ)›)] + congr + +/-- Removing an interior coordinate agrees with erasing its interior-list index. -/ +theorem ofFn_interior_succAbove_eq_eraseIdx + {α : Type*} {n : ℕ} + (f : Fin (n + 3) → α) (k : Fin (n + 1)) : + List.ofFn + (fun i : Fin n => + f (k.succ.castSucc.succAbove i.succ.castSucc)) = + (List.ofFn + (fun i : Fin (n + 1) => f i.succ.castSucc)).eraseIdx k := by + simpa only [Fin.succAbove_succ_castSucc] using + List.ofFn_succAbove_eq_eraseIdx + (fun i : Fin (n + 1) => f i.succ.castSucc) k + +/-- A finite-function list splits into its two endpoints and interior coordinates. -/ +theorem ofFn_two_endpoints + {α : Type*} {n : ℕ} (f : Fin (n + 2) → α) : + List.ofFn f = + f 0 :: + (List.ofFn (fun i : Fin n => f i.succ.castSucc) ++ + [f (Fin.last (n + 1))]) := by + rw [List.ofFn_succ, List.ofFn_succ'] + simp only [List.concat_eq_append] + congr + +end List diff --git a/RealRooted/Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean b/RealRooted/Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean index a3cf55b2c..84b4aa3ab 100644 --- a/RealRooted/Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean +++ b/RealRooted/Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean @@ -10,6 +10,12 @@ variable {n R : Type*} [DecidableEq n] [Fintype n] [CommRing R] -- TODO: Replace `det_zero` @[simp] lemma det_zero' [Nonempty n] : (0 : Matrix n n R).det = 0 := det_zero ‹_› +/-- The Leibniz formula for a determinant, with rows indexed before columns. -/ +theorem det_apply_row (M : Matrix n n R) : + M.det = ∑ σ : Equiv.Perm n, Equiv.Perm.sign σ • ∏ i, M i (σ i) := by + rw [← Matrix.det_transpose, Matrix.det_apply] + rfl + /-- The alternating vector of maximal row-deletion minors of a rectangular matrix lies in the kernel of its transpose. This is the Laplace expansion of the matrix obtained by adjoining a duplicate of any chosen column. -/ @@ -33,4 +39,41 @@ theorem transpose_mulVec_alternating_det_submatrix_succAbove {q : ℕ} simp_rw [hminor] at hdet simpa [mulVec, dotProduct, A, mul_comm, mul_left_comm, mul_assoc] using hdet +/-- Expanding a matrix with constant first column after adjacent row subtraction. -/ +theorem det_eq_det_adjacentRowDiff_of_firstColumn_eq_one {n : ℕ} + (A : Matrix (Fin (n + 1)) (Fin (n + 1)) R) + (hA : ∀ i, A i 0 = 1) : + A.det = + (Matrix.of fun (i j : Fin n) => + A i.succ j.succ - A i.castSucc j.succ).det := by + let B : Matrix (Fin (n + 1)) (Fin (n + 1)) R := + fun i j => Fin.cases (A 0 j) + (fun k => A k.succ j - A k.castSucc j) i + have hdet : A.det = B.det := by + apply det_eq_of_forall_row_eq_smul_add_pred (fun _ => 1) + · intro j + simp [B] + · intro i j + simp [B] + rw [hdet, det_succ_column_zero, Fin.sum_univ_succ] + have hminor : + B.submatrix Fin.succ Fin.succ = + Matrix.of fun (i j : Fin n) => + A i.succ j.succ - A i.castSucc j.succ := by + ext i j + rfl + simpa [B, hA] using congrArg Matrix.det hminor + +/-- A submatrix with a noninjective column selector has zero determinant. -/ +theorem det_submatrix_eq_zero_of_not_injective_right + {R m κ q : Type*} [CommRing R] [DecidableEq q] [Fintype q] + (L : Matrix m κ R) (rows : q → m) (f : q → κ) + (hf : ¬ Function.Injective f) : + (L.submatrix rows f).det = 0 := by + obtain ⟨i, j, hfij, hij⟩ := Function.not_injective_iff.mp hf + apply Matrix.det_zero_of_column_eq hij + intro k + simp only [Matrix.submatrix_apply] + rw [hfij] + end Matrix diff --git a/RealRooted/Mathlib/LinearAlgebra/Matrix/Determinant/CauchyBinet.lean b/RealRooted/Mathlib/LinearAlgebra/Matrix/Determinant/CauchyBinet.lean new file mode 100644 index 000000000..232ed4652 --- /dev/null +++ b/RealRooted/Mathlib/LinearAlgebra/Matrix/Determinant/CauchyBinet.lean @@ -0,0 +1,300 @@ +import RealRooted.Mathlib.LinearAlgebra.Matrix.Determinant.Basic +import Mathlib.LinearAlgebra.Basis.VectorSpace +import Mathlib.LinearAlgebra.Matrix.ToLin +import Mathlib.Order.Hom.PowersetCard + +/-! +# Cauchy-Binet determinant expansions + +This file develops the rectangular Cauchy-Binet formula. It expands a selected +minor into a sum over intermediate maps, proves that noninjective maps vanish, +and factors each injective map through the increasing enumeration of its image. +The remaining step transports permutation signs and groups by image subset. +-/ + +open scoped BigOperators + +namespace Matrix + +/-- Leibniz expansion of a selected minor of a rectangular matrix product. -/ +theorem det_submatrix_mul_eq_sum_perm_fun + {R : Type*} [CommRing R] {l n m q : ℕ} + (L : Matrix (Fin l) (Fin n) R) + (A : Matrix (Fin n) (Fin m) R) + (rows : Fin q → Fin l) (cols : Fin q → Fin m) : + ((L * A).submatrix rows cols).det = + ∑ σ : Equiv.Perm (Fin q), Equiv.Perm.sign σ • + ∑ f : Fin q → Fin n, + ∏ i, L (rows (σ i)) (f i) * A (f i) (cols i) := by + rw [Matrix.det_apply] + simp only [Matrix.submatrix_apply, Matrix.mul_apply, Finset.prod_univ_sum] + simp + +/-- Reassemble the permutation sum for each intermediate-index map. -/ +theorem det_submatrix_mul_eq_sum_fun_det + {R : Type*} [CommRing R] {l n m q : ℕ} + (L : Matrix (Fin l) (Fin n) R) + (A : Matrix (Fin n) (Fin m) R) + (rows : Fin q → Fin l) (cols : Fin q → Fin m) : + ((L * A).submatrix rows cols).det = + ∑ f : Fin q → Fin n, + (L.submatrix rows f).det * ∏ i, A (f i) (cols i) := by + rw [det_submatrix_mul_eq_sum_perm_fun] + simp_rw [Finset.smul_sum] + rw [Finset.sum_comm] + apply Fintype.sum_congr + intro f + rw [Matrix.det_apply] + simp only [Matrix.submatrix_apply, Finset.prod_mul_distrib] + rw [Finset.sum_mul] + simp_rw [smul_mul_assoc] + +end Matrix + +private theorem coe_ofFinEmb_eq_range {q : ℕ} {I : Type*} (f : Fin q ↪ I) : + (Set.powersetCard.ofFinEmb q I f : Set I) = Set.range f := by + ext x + simp [Set.powersetCard.ofFinEmb, Set.powersetCard.map] + + +private theorem range_orderEmbOfPowersetCard {q : ℕ} {I : Type*} + [LinearOrder I] (s : Set.powersetCard I q) : + Set.range (Set.powersetCard.ofFinEmbEquiv.symm s) = (s : Set I) := by + let e : Fin q ↪o I := Set.powersetCard.ofFinEmbEquiv.symm s + calc + Set.range e = (Set.powersetCard.ofFinEmb q I e.toEmbedding : Set I) := + (coe_ofFinEmb_eq_range e.toEmbedding).symm + _ = (s : Set I) := congrArg + (fun t : Set.powersetCard I q => (t : Set I)) + (Set.powersetCard.ofFinEmbEquiv.apply_symm_apply s) + +/-- An injective finite map into a linear order factors through the increasing +enumeration of its image and a permutation of its domain. -/ +theorem Set.powersetCard.exists_orderEmb_comp_perm_eq_of_injective + {q : ℕ} {I : Type*} [LinearOrder I] + (f : Fin q → I) (hf : Function.Injective f) : + ∃ s : Set.powersetCard I q, ∃ p : Equiv.Perm (Fin q), + ∀ i, Set.powersetCard.ofFinEmbEquiv.symm s (p i) = f i := by + let emb : Fin q ↪ I := ⟨f, hf⟩ + let s : Set.powersetCard I q := Set.powersetCard.ofFinEmb q I emb + let e : Fin q ↪o I := Set.powersetCard.ofFinEmbEquiv.symm s + have hfRange : Set.range f = (s : Set I) := + (coe_ofFinEmb_eq_range emb).symm + have hRange : Set.range f = Set.range e := + hfRange.trans (range_orderEmbOfPowersetCard s).symm + let ee : Fin q ≃ Set.range e := Equiv.ofInjective e e.injective + let p : Equiv.Perm (Fin q) := + (Equiv.ofInjective f hf).trans + ((Equiv.setCongr hRange).trans ee.symm) + refine ⟨s, p, ?_⟩ + intro i + have hfi : f i ∈ Set.range e := hRange ▸ ⟨i, rfl⟩ + change e (ee.symm ⟨f i, hfi⟩) = f i + exact congrArg Subtype.val (ee.apply_symm_apply ⟨f i, hfi⟩) + +private theorem range_comp_perm {q : ℕ} {I : Type*} + (e : Fin q → I) (p : Equiv.Perm (Fin q)) : + Set.range (fun i => e (p i)) = Set.range e := by + ext x + constructor + · rintro ⟨i, rfl⟩ + exact ⟨p i, rfl⟩ + · rintro ⟨j, rfl⟩ + exact ⟨p.symm j, by simp⟩ + +/-- The ordered-image/permutation representation of an injective finite map is +unique. -/ +theorem Set.powersetCard.orderEmb_comp_perm_injective + {q : ℕ} {I : Type*} [LinearOrder I] : + Function.Injective + (fun z : Set.powersetCard I q × Equiv.Perm (Fin q) => + fun i => Set.powersetCard.ofFinEmbEquiv.symm z.1 (z.2 i)) := by + rintro ⟨s, p⟩ ⟨t, r⟩ h + let es : Fin q ↪o I := Set.powersetCard.ofFinEmbEquiv.symm s + let et : Fin q ↪o I := Set.powersetCard.ofFinEmbEquiv.symm t + have hst : s = t := by + apply Subtype.ext + apply Finset.coe_injective + calc + (s : Set I) = Set.range es := (range_orderEmbOfPowersetCard s).symm + _ = Set.range (fun i => es (p i)) := (range_comp_perm es p).symm + _ = Set.range (fun i => et (r i)) := congrArg Set.range h + _ = Set.range et := range_comp_perm et r + _ = (t : Set I) := range_orderEmbOfPowersetCard t + subst t + have hpr : p = r := by + apply Equiv.ext + intro i + exact es.injective (congrFun h i) + exact Prod.ext rfl hpr + +/-- Ordered image and a domain permutation parameterize all finite embeddings. -/ +noncomputable def Set.powersetCard.orderEmbPermEquivEmbedding + {q : ℕ} {I : Type*} [LinearOrder I] : + Set.powersetCard I q × Equiv.Perm (Fin q) ≃ (Fin q ↪ I) := + Equiv.ofBijective + (fun z => + ⟨fun i => Set.powersetCard.ofFinEmbEquiv.symm z.1 (z.2 i), + (Set.powersetCard.ofFinEmbEquiv.symm z.1).injective.comp + z.2.injective⟩) + ⟨by + intro z w h + apply Set.powersetCard.orderEmb_comp_perm_injective + funext i + exact congrArg (fun g : Fin q ↪ I => g i) h, + by + intro f + obtain ⟨s, p, h⟩ := + Set.powersetCard.exists_orderEmb_comp_perm_eq_of_injective f f.injective + refine ⟨(s, p), ?_⟩ + ext i + exact h i⟩ + +/-- Reindex a sum over finite embeddings by ordered image and permutation. -/ +theorem Set.powersetCard.sum_embedding_eq_sum_orderEmb_perm + {q : ℕ} {I M : Type*} [LinearOrder I] [Fintype I] [AddCommMonoid M] + (g : (Fin q ↪ I) → M) : + ∑ f : Fin q ↪ I, g f = + ∑ s : Set.powersetCard I q, ∑ p : Equiv.Perm (Fin q), + g ⟨fun i => Set.powersetCard.ofFinEmbEquiv.symm s (p i), + (Set.powersetCard.ofFinEmbEquiv.symm s).injective.comp p.injective⟩ := by + calc + ∑ f : Fin q ↪ I, g f = + ∑ z, g (Set.powersetCard.orderEmbPermEquivEmbedding z) := + (Set.powersetCard.orderEmbPermEquivEmbedding.sum_comp g).symm + _ = ∑ s : Set.powersetCard I q, ∑ p : Equiv.Perm (Fin q), + g (Set.powersetCard.orderEmbPermEquivEmbedding (s, p)) := + Fintype.sum_prod_type _ + _ = _ := by + simp [Set.powersetCard.orderEmbPermEquivEmbedding] + +private theorem sum_function_eq_sum_embedding_of_zero_noninjective + {q : ℕ} {I M : Type*} [Fintype I] [AddCommMonoid M] + (g : (Fin q → I) → M) + (hzero : ∀ f, ¬ Function.Injective f → g f = 0) : + ∑ f : Fin q → I, g f = ∑ e : Fin q ↪ I, g e := by + classical + calc + ∑ f : Fin q → I, g f = + (∑ f : {f : Fin q → I // Function.Injective f}, g f) + + ∑ f : {f : Fin q → I // ¬ Function.Injective f}, g f := + (Fintype.sum_subtype_add_sum_subtype Function.Injective g).symm + _ = ∑ f : {f : Fin q → I // Function.Injective f}, g f := by + rw [show (∑ f : {f : Fin q → I // ¬ Function.Injective f}, g f) = 0 by + apply Finset.sum_eq_zero + intro f _ + exact hzero f f.property, add_zero] + _ = ∑ f : Fin q ↪ I, g f := by + exact Fintype.sum_equiv + (Equiv.subtypeInjectiveEquivEmbedding (Fin q) I) _ _ fun _ => rfl + +private theorem sum_perm_det_submatrix_comp_mul_prod_eq + {R : Type*} [CommRing R] {l n m q : ℕ} + (L : Matrix (Fin l) (Fin n) R) + (A : Matrix (Fin n) (Fin m) R) + (rows : Fin q → Fin l) (cols : Fin q → Fin m) + (e : Fin q → Fin n) : + (∑ p : Equiv.Perm (Fin q), + (L.submatrix rows (fun i => e (p i))).det * + ∏ i, A (e (p i)) (cols i)) = + (L.submatrix rows e).det * (A.submatrix e cols).det := by + calc + _ = (L.submatrix rows e).det * + ∑ p : Equiv.Perm (Fin q), + Equiv.Perm.sign p • ∏ i, A (e (p i)) (cols i) := by + rw [Finset.mul_sum] + apply Fintype.sum_congr + intro p + rw [show L.submatrix rows (fun i => e (p i)) = + (L.submatrix rows e).submatrix id p by rfl] + rw [Matrix.det_permute', Units.smul_def, + ← Int.cast_smul_eq_zsmul R, smul_eq_mul] + ac_rfl + _ = (L.submatrix rows e).det * (A.submatrix e cols).det := by + congr 1 + rw [Matrix.det_apply] + rfl + +/-- Rectangular Cauchy--Binet for selected square minors. -/ +theorem Matrix.det_submatrix_mul_eq_sum_powersetCard + {R : Type*} [CommRing R] {l n m q : ℕ} + (L : Matrix (Fin l) (Fin n) R) + (A : Matrix (Fin n) (Fin m) R) + (rows : Fin q → Fin l) (cols : Fin q → Fin m) : + ((L * A).submatrix rows cols).det = + ∑ s : Set.powersetCard (Fin n) q, + (L.submatrix rows + (Set.powersetCard.ofFinEmbEquiv.symm s)).det * + (A.submatrix + (Set.powersetCard.ofFinEmbEquiv.symm s) cols).det := by + classical + rw [Matrix.det_submatrix_mul_eq_sum_fun_det] + rw [sum_function_eq_sum_embedding_of_zero_noninjective] + · rw [Set.powersetCard.sum_embedding_eq_sum_orderEmb_perm] + apply Fintype.sum_congr + intro s + simpa using sum_perm_det_submatrix_comp_mul_prod_eq L A rows cols + (Set.powersetCard.ofFinEmbEquiv.symm s) + · intro f hf + rw [Matrix.det_submatrix_eq_zero_of_not_injective_right L rows f hf, + zero_mul] + +private theorem selected_mulVec_injective + {R : Type*} [Field R] {n m q : ℕ} + (A : Matrix (Fin n) (Fin m) R) + (hA : Function.Injective A.mulVec) + (cols : Fin q → Fin m) (hcols : StrictMono cols) : + Function.Injective (A.submatrix id cols).mulVec := by + rw [Matrix.mulVec_injective_iff] + have h := (Matrix.mulVec_injective_iff.mp hA).comp cols hcols.injective + rw [show (A.submatrix id cols).col = A.col ∘ cols by + ext j i + rfl] + exact h + +private theorem exists_left_inverse_matrix + {R : Type*} [Field R] {n q : ℕ} + (B : Matrix (Fin n) (Fin q) R) + (hB : Function.Injective B.mulVec) : + ∃ C : Matrix (Fin q) (Fin n) R, C * B = 1 := by + let f := Matrix.toLin' B + have hf : LinearMap.ker f = ⊥ := by + rw [LinearMap.ker_eq_bot] + intro x y hxy + apply hB + simpa only [f, Matrix.toLin'_apply] using hxy + obtain ⟨g, hg⟩ := f.exists_leftInverse_of_injective hf + refine ⟨LinearMap.toMatrix' g, ?_⟩ + rw [← LinearMap.toMatrix'_toLin' B, ← LinearMap.toMatrix'_comp, hg, + ← Matrix.toLin'_one, LinearMap.toMatrix'_toLin'] + +/-- Full column rank gives a nonzero maximal minor on strictly increasing rows. + +The proof restricts the independent columns, takes a linear left inverse, and +applies rectangular Cauchy--Binet to the resulting identity matrix. -/ +theorem Matrix.exists_ordered_minor_ne_zero_of_mulVec_injective + {R : Type*} [Field R] {n m q : ℕ} + (A : Matrix (Fin n) (Fin m) R) + (hA : Function.Injective A.mulVec) + (cols : Fin q → Fin m) (hcols : StrictMono cols) : + ∃ rows : Fin q → Fin n, StrictMono rows ∧ + (A.submatrix rows cols).det ≠ 0 := by + classical + let B := A.submatrix id cols + have hB : Function.Injective B.mulVec := by + exact selected_mulVec_injective A hA cols hcols + obtain ⟨C, hCB⟩ := exists_left_inverse_matrix B hB + have hsum : + (∑ s : Set.powersetCard (Fin n) q, + (C.submatrix id + (Set.powersetCard.ofFinEmbEquiv.symm s)).det * + (B.submatrix + (Set.powersetCard.ofFinEmbEquiv.symm s) id).det) ≠ 0 := by + rw [← Matrix.det_submatrix_mul_eq_sum_powersetCard C B id id, hCB] + simp + obtain ⟨s, _, hs⟩ := Finset.exists_ne_zero_of_sum_ne_zero + (s := Finset.univ) (by simpa using hsum) + refine ⟨Set.powersetCard.ofFinEmbEquiv.symm s, + (Set.powersetCard.ofFinEmbEquiv.symm s).strictMono, ?_⟩ + have hminor := (mul_ne_zero_iff.mp hs).2 + simpa [B] using hminor diff --git a/RealRooted/Mathlib/LinearAlgebra/Matrix/Determinant/Integral.lean b/RealRooted/Mathlib/LinearAlgebra/Matrix/Determinant/Integral.lean new file mode 100644 index 000000000..bafbebc06 --- /dev/null +++ b/RealRooted/Mathlib/LinearAlgebra/Matrix/Determinant/Integral.lean @@ -0,0 +1,111 @@ +module + +public import RealRooted.Mathlib.LinearAlgebra.Matrix.Determinant.Basic +public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic +public import Mathlib.MeasureTheory.Integral.Pi +public import Mathlib.Topology.Algebra.Module.FiniteDimension + +/-! +# Determinants and interval integrals + +This file records how determinant multilinearity interacts with interval +integrals in one matrix row. +-/ + +public section + +open scoped Interval + +namespace Matrix + +private noncomputable def detUpdateRowLinearMap + {n : Type*} [DecidableEq n] [Fintype n] (M : Matrix n n ℝ) (i : n) : + (n → ℝ) →ₗ[ℝ] ℝ := + { toFun := fun row => (M.updateRow i row).det + map_add' := fun u v => det_updateRow_add M i u v + map_smul' := fun c u => by + simpa only [RingHom.id_apply, smul_eq_mul] using det_updateRow_smul M i c u } + +/-- A determinant commutes with an interval integral in one fixed row. -/ +theorem det_updateRow_intervalIntegral + {n : Type*} [DecidableEq n] [Fintype n] (M : Matrix n n ℝ) (i : n) + (f : ℝ → n → ℝ) (a b : ℝ) + (hf : IntervalIntegrable f MeasureTheory.volume a b) : + (M.updateRow i (∫ t in a..b, f t)).det = + ∫ t in a..b, (M.updateRow i (f t)).det := by + let L := (detUpdateRowLinearMap M i).toContinuousLinearMap + exact (L.intervalIntegral_comp_comm hf).symm + +/-- A pointwise determinant is integrable under a product measure when every entry is. -/ +theorem integrable_det_rows + {n E : Type*} [DecidableEq n] [Fintype n] [MeasurableSpace E] + (μ : n → MeasureTheory.Measure E) [∀ i, MeasureTheory.SigmaFinite (μ i)] + (f : n → E → n → ℝ) + (hf : ∀ i j, MeasureTheory.Integrable (fun x => f i x j) (μ i)) : + MeasureTheory.Integrable + (fun x : n → E => (Matrix.of fun i j => f i (x i) j).det) + (MeasureTheory.Measure.pi μ) := by + have hfun : + (fun x : n → E => (Matrix.of fun i j => f i (x i) j).det) = + fun x => ∑ σ : Equiv.Perm n, ((Equiv.Perm.sign σ : ℤ) : ℝ) * + ∏ i, f i (x i) (σ i) := by + funext x + rw [Matrix.det_apply_row] + simp_rw [Units.smul_def, ← Int.cast_smul_eq_zsmul ℝ] + rfl + rw [hfun] + apply MeasureTheory.integrable_finsetSum Finset.univ + intro σ _ + exact (MeasureTheory.Integrable.fintype_prod fun i => hf i (σ i)).const_mul _ + +/-- The determinant of rowwise integrals is the integral of the pointwise determinant. -/ +theorem det_integral_rows_eq_integral_det + {n E : Type*} [DecidableEq n] [Fintype n] [MeasurableSpace E] + (μ : n → MeasureTheory.Measure E) [∀ i, MeasureTheory.SigmaFinite (μ i)] + (f : n → E → n → ℝ) + (hf : ∀ i j, MeasureTheory.Integrable (fun x => f i x j) (μ i)) : + (Matrix.of fun i j => ∫ x, f i x j ∂μ i).det = + ∫ x : n → E, + (Matrix.of fun i j => f i (x i) j).det ∂MeasureTheory.Measure.pi μ := by + have hdet (M : Matrix n n ℝ) : + M.det = ∑ σ : Equiv.Perm n, ((Equiv.Perm.sign σ : ℤ) : ℝ) * + ∏ i, M i (σ i) := by + rw [Matrix.det_apply_row] + simp_rw [Units.smul_def, ← Int.cast_smul_eq_zsmul ℝ] + rfl + have hprod (σ : Equiv.Perm n) : + MeasureTheory.Integrable + (fun x : n → E => ∏ i, f i (x i) (σ i)) (MeasureTheory.Measure.pi μ) := + MeasureTheory.Integrable.fintype_prod fun i => hf i (σ i) + calc + (Matrix.of fun i j => ∫ x, f i x j ∂μ i).det = + ∑ σ : Equiv.Perm n, ((Equiv.Perm.sign σ : ℤ) : ℝ) * + ∏ i, ∫ x, f i x (σ i) ∂μ i := + hdet _ + _ = ∑ σ : Equiv.Perm n, ((Equiv.Perm.sign σ : ℤ) : ℝ) * + ∫ x : n → E, ∏ i, f i (x i) (σ i) ∂MeasureTheory.Measure.pi μ := by + apply Finset.sum_congr rfl + intro σ _ + apply congrArg (((Equiv.Perm.sign σ : ℤ) : ℝ) * ·) + exact (MeasureTheory.integral_fintype_prod_eq_prod + (fun i x => f i x (σ i))).symm + _ = ∑ σ : Equiv.Perm n, + ∫ x : n → E, ((Equiv.Perm.sign σ : ℤ) : ℝ) * + ∏ i, f i (x i) (σ i) ∂MeasureTheory.Measure.pi μ := by + apply Finset.sum_congr rfl + intro σ _ + rw [MeasureTheory.integral_const_mul] + _ = ∫ x : n → E, ∑ σ : Equiv.Perm n, + ((Equiv.Perm.sign σ : ℤ) : ℝ) * + ∏ i, f i (x i) (σ i) ∂MeasureTheory.Measure.pi μ := by + symm + apply MeasureTheory.integral_finsetSum + intro σ _ + exact (hprod σ).const_mul _ + _ = ∫ x : n → E, + (Matrix.of fun i j => f i (x i) j).det ∂MeasureTheory.Measure.pi μ := by + apply congrArg fun g : (n → E) → ℝ => ∫ x, g x ∂MeasureTheory.Measure.pi μ + funext x + exact (hdet _).symm + +end Matrix diff --git a/RealRooted/Mathlib/LinearAlgebra/Matrix/Gaussian.lean b/RealRooted/Mathlib/LinearAlgebra/Matrix/Gaussian.lean new file mode 100644 index 000000000..9e30695cc --- /dev/null +++ b/RealRooted/Mathlib/LinearAlgebra/Matrix/Gaussian.lean @@ -0,0 +1,394 @@ +import RealRooted.Mathlib.Analysis.SpecialFunctions.ExpIntegral +import RealRooted.Mathlib.LinearAlgebra.Matrix.Determinant.Integral +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring +import Mathlib.Topology.Instances.Matrix +import RealRooted.Mathlib.LinearAlgebra.Vandermonde + +/-! +# Karlin's finite Gaussian matrices + +This file starts the formalization of Karlin, *Total Positivity*, Vol. I, +Chapter V, Section 1, Proposition 1.1. Karlin uses the Gaussian matrix + +`F(a) i j = exp (-a * (i - j) ^ 2)`. + +The proposition has two parts: `F(a)` tends to the identity as `a` tends to +positive infinity, and `F(a)` is strictly totally positive when `a > 0`. +This file proves Gaussian convergence and strict positivity of all strictly +ordered finite minors using Karlin.s exponential-kernel argument. +-/ + +public section + +open scoped Interval + +open Filter MeasureTheory Topology + +namespace Matrix + +/-- Karlin's finite Gaussian matrix from Proposition V.1.1. -/ +noncomputable def gaussianMatrix (n : ℕ) (a : ℝ) : Matrix (Fin n) (Fin n) ℝ := + fun i j => Real.exp (-a * (((i : ℕ) : ℝ) - ((j : ℕ) : ℝ)) ^ 2) + +@[simp] lemma gaussianMatrix_apply (n : ℕ) (a : ℝ) (i j : Fin n) : + gaussianMatrix n a i j = + Real.exp (-a * (((i : ℕ) : ℝ) - ((j : ℕ) : ℝ)) ^ 2) := + rfl + +@[simp] lemma gaussianMatrix_apply_self (n : ℕ) (a : ℝ) (i : Fin n) : + gaussianMatrix n a i i = 1 := by + simp + +lemma gaussianMatrix_apply_pos (n : ℕ) (a : ℝ) (i j : Fin n) : + 0 < gaussianMatrix n a i j := + Real.exp_pos _ + +/-- Karlin's Gaussian matrix converges entrywise to the identity as its +parameter tends to positive infinity. -/ +theorem tendsto_gaussianMatrix_atTop (n : ℕ) : + Tendsto (gaussianMatrix n) atTop + (𝓝 (1 : Matrix (Fin n) (Fin n) ℝ)) := by + change Tendsto + (fun a => (gaussianMatrix n a : Fin n → Fin n → ℝ)) atTop + (𝓝 ((1 : Matrix (Fin n) (Fin n) ℝ) : Fin n → Fin n → ℝ)) + apply tendsto_pi_nhds.2 + intro i + apply tendsto_pi_nhds.2 + intro j + by_cases hij : i = j + · subst j + simp only [gaussianMatrix_apply_self, one_apply, if_pos] + exact tendsto_const_nhds + · have hcast : + (((i : ℕ) : ℝ) - ((j : ℕ) : ℝ)) ≠ 0 := by + rw [sub_ne_zero] + intro heq + have hval : (i : ℕ) = (j : ℕ) := by + exact_mod_cast heq + exact hij (Fin.ext hval) + have hsquare : + 0 < (((i : ℕ) : ℝ) - ((j : ℕ) : ℝ)) ^ 2 := + sq_pos_of_ne_zero hcast + have hneg : + -(((i : ℕ) : ℝ) - ((j : ℕ) : ℝ)) ^ 2 < 0 := + neg_lt_zero.mpr hsquare + have hlinear : + Tendsto + (fun a : ℝ => + a * -(((i : ℕ) : ℝ) - ((j : ℕ) : ℝ)) ^ 2) + atTop atBot := + tendsto_id.atTop_mul_const_of_neg hneg + have hexp := + Real.tendsto_exp_atBot.comp hlinear + convert hexp using 1 + · funext a + simp only [Function.comp_apply, gaussianMatrix_apply] + ring_nf + · simp [hij] + +/-- The finite restriction of Karlin's exponential kernel `exp (x * y)`. -/ +noncomputable def exponentialKernelMatrix {i j : Type*} + (x : i → ℝ) (y : j → ℝ) : Matrix i j ℝ := + fun i j => Real.exp (x i * y j) + +@[simp] lemma exponentialKernelMatrix_apply {i j : Type*} + (x : i → ℝ) (y : j → ℝ) (r : i) (c : j) : + exponentialKernelMatrix x y r c = Real.exp (x r * y c) := + rfl + +/-- Adjacent exponential-kernel row differences are interval integrals. -/ +lemma exponentialKernelMatrix_succ_sub_castSucc_eq_intervalIntegral {n : ℕ} + (x : Fin (n + 1) → ℝ) (y : Fin n → ℝ) (i j : Fin n) : + exponentialKernelMatrix x y i.succ j - + exponentialKernelMatrix x y i.castSucc j = + ∫ t in x i.castSucc..x i.succ, y j * Real.exp (t * y j) := by + rw [Real.intervalIntegral_mul_exp_mul] + rfl + +/-- The adjacent-difference determinant is a restricted-volume product integral. -/ +theorem det_adjacentRowDiff_exponentialKernelMatrix_eq_integral {n : ℕ} + (x : Fin (n + 1) → ℝ) (y : Fin n → ℝ) (hx : StrictMono x) : + (Matrix.of fun i j => + exponentialKernelMatrix x y i.succ j - + exponentialKernelMatrix x y i.castSucc j).det = + ∫ t : Fin n → ℝ, + (Matrix.of fun i j => y j * Real.exp (t i * y j)).det + ∂Measure.pi (fun i => + volume.restrict (Set.Ioc (x i.castSucc) (x i.succ))) := by + let μ : Fin n → Measure ℝ := fun i => + volume.restrict (Set.Ioc (x i.castSucc) (x i.succ)) + let f : Fin n → ℝ → Fin n → ℝ := fun _ t j => + y j * Real.exp (t * y j) + have hf : ∀ i j, Integrable (fun t => f i t j) (μ i) := by + intro i j + change IntegrableOn (fun t => f i t j) + (Set.Ioc (x i.castSucc) (x i.succ)) volume + rw [← intervalIntegrable_iff_integrableOn_Ioc_of_le + (hx i.castSucc_lt_succ).le] + exact + (continuous_const.mul + (Real.continuous_exp.comp (continuous_id.mul continuous_const))).intervalIntegrable _ _ + have hmatrix : + Matrix.of (fun i j => + exponentialKernelMatrix x y i.succ j - + exponentialKernelMatrix x y i.castSucc j) = + Matrix.of fun i j => ∫ t, f i t j ∂μ i := by + ext i j + simp only [Matrix.of_apply] + rw [exponentialKernelMatrix_succ_sub_castSucc_eq_intervalIntegral] + rw [intervalIntegral.integral_of_le (hx i.castSucc_lt_succ).le] + rw [hmatrix, det_integral_rows_eq_integral_det μ f hf] + +/-- Translating all first coordinates multiplies the exponential-kernel +determinant by an explicit positive column factor. -/ +theorem det_exponentialKernelMatrix_add_const_left {q : ℕ} + (x y : Fin q → ℝ) (c : ℝ) : + (exponentialKernelMatrix (fun i => x i + c) y).det = + (∏ j, Real.exp (c * y j)) * + (exponentialKernelMatrix x y).det := by + have hmatrix : + exponentialKernelMatrix (fun i => x i + c) y = + of fun i j => + Real.exp (c * y j) * exponentialKernelMatrix x y i j := by + ext i j + simp only [exponentialKernelMatrix_apply, of_apply] + rw [show (x i + c) * y j = c * y j + x i * y j by ring, + Real.exp_add] + rw [hmatrix, det_mul_row] + +/-- Translating all second coordinates multiplies the exponential-kernel +determinant by an explicit positive row factor. -/ +theorem det_exponentialKernelMatrix_add_const_right {q : ℕ} + (x y : Fin q → ℝ) (c : ℝ) : + (exponentialKernelMatrix x (fun j => y j + c)).det = + (∏ i, Real.exp (x i * c)) * + (exponentialKernelMatrix x y).det := by + have hmatrix : + exponentialKernelMatrix x (fun j => y j + c) = + of fun i j => + Real.exp (x i * c) * exponentialKernelMatrix x y i j := by + ext i j + simp only [exponentialKernelMatrix_apply, of_apply] + rw [show x i * (y j + c) = x i * c + x i * y j by ring, + Real.exp_add] + rw [hmatrix, det_mul_column] + +theorem det_exponentialKernelMatrix_add_const_left_pos_iff {q : ℕ} + (x y : Fin q → ℝ) (c : ℝ) : + 0 < (exponentialKernelMatrix (fun i => x i + c) y).det ↔ + 0 < (exponentialKernelMatrix x y).det := by + rw [det_exponentialKernelMatrix_add_const_left] + exact mul_pos_iff_of_pos_left (by positivity) + +theorem det_exponentialKernelMatrix_add_const_right_pos_iff {q : ℕ} + (x y : Fin q → ℝ) (c : ℝ) : + 0 < (exponentialKernelMatrix x (fun j => y j + c)).det ↔ + 0 < (exponentialKernelMatrix x y).det := by + rw [det_exponentialKernelMatrix_add_const_right] + exact mul_pos_iff_of_pos_left (by positivity) + +/-- The transpose of the Wronskian matrix of the functions +`t ↦ exp (y i * t)`. -/ +noncomputable def exponentialWronskianMatrix {q : ℕ} + (y : Fin q → ℝ) (t : ℝ) : Matrix (Fin q) (Fin q) ℝ := + fun i j => iteratedDeriv (j : ℕ) (fun s => Real.exp (y i * s)) t + +@[simp] lemma exponentialWronskianMatrix_apply {q : ℕ} + (y : Fin q → ℝ) (t : ℝ) (i j : Fin q) : + exponentialWronskianMatrix y t i j = + y i ^ (j : ℕ) * Real.exp (t * y i) := by + rw [exponentialWronskianMatrix, + congrFun (iteratedDeriv_exp_const_mul (j : ℕ) (y i)) t] + congr 2 + exact mul_comm _ _ + +/-- Karlin's exponential Wronskian is a positive exponential factor times a +Vandermonde determinant. -/ +theorem det_exponentialWronskianMatrix_eq {q : ℕ} + (y : Fin q → ℝ) (t : ℝ) : + (exponentialWronskianMatrix y t).det = + (∏ i, Real.exp (t * y i)) * (vandermonde y).det := by + have hmatrix : + exponentialWronskianMatrix y t = + of fun i j => + Real.exp (t * y i) * vandermonde y i j := by + ext i j + simp only [exponentialWronskianMatrix_apply, of_apply, + vandermonde_apply] + ring + rw [hmatrix, det_mul_column] + +/-- The exponential Wronskian has the positive orientation required in +Karlin's extended-determinant argument. -/ +theorem det_exponentialWronskianMatrix_pos {q : ℕ} + {y : Fin q → ℝ} (hy : StrictMono y) (t : ℝ) : + 0 < (exponentialWronskianMatrix y t).det := by + rw [det_exponentialWronskianMatrix_eq] + exact mul_pos (by positivity) (det_vandermonde_pos_of_strictMono hy) + +/-- A Gaussian minor is an exponential-kernel minor times positive row and +column factors. This is the algebraic reduction in Karlin's proof of +Proposition V.1.1. -/ +theorem det_gaussianMatrix_submatrix_eq {n q : ℕ} (a : ℝ) + (rows cols : Fin q → Fin n) : + ((gaussianMatrix n a).submatrix rows cols).det = + (∏ i, Real.exp (-a * (((rows i : Fin n) : ℕ) : ℝ) ^ 2)) * + (∏ j, Real.exp (-a * (((cols j : Fin n) : ℕ) : ℝ) ^ 2)) * + (exponentialKernelMatrix + (fun i => 2 * a * (((rows i : Fin n) : ℕ) : ℝ)) + (fun j => (((cols j : Fin n) : ℕ) : ℝ))).det := by + let rowFactor : Fin q → ℝ := + fun i => Real.exp (-a * (((rows i : Fin n) : ℕ) : ℝ) ^ 2) + let colFactor : Fin q → ℝ := + fun j => Real.exp (-a * (((cols j : Fin n) : ℕ) : ℝ) ^ 2) + let E : Matrix (Fin q) (Fin q) ℝ := + exponentialKernelMatrix + (fun i => 2 * a * (((rows i : Fin n) : ℕ) : ℝ)) + (fun j => (((cols j : Fin n) : ℕ) : ℝ)) + have hmatrix : + (gaussianMatrix n a).submatrix rows cols = + of fun i j => rowFactor i * (colFactor j * E i j) := by + ext i j + simp only [submatrix_apply, gaussianMatrix_apply, of_apply, rowFactor, + colFactor, E, exponentialKernelMatrix_apply] + rw [show + -a * ((((rows i : Fin n) : ℕ) : ℝ) - + (((cols j : Fin n) : ℕ) : ℝ)) ^ 2 = + -a * (((rows i : Fin n) : ℕ) : ℝ) ^ 2 + + (-a * (((cols j : Fin n) : ℕ) : ℝ) ^ 2 + + (2 * a * (((rows i : Fin n) : ℕ) : ℝ)) * + (((cols j : Fin n) : ℕ) : ℝ)) by ring] + rw [Real.exp_add, Real.exp_add] + have hcol : + (of fun i j => colFactor j * E i j).det = + (∏ j, colFactor j) * E.det := + det_mul_row colFactor E + rw [hmatrix, det_mul_column] + change + (∏ i, rowFactor i) * + (of fun i j => colFactor j * E i j).det = + _ + rw [hcol] + dsimp only [rowFactor, colFactor, E] + ring + +/-- Transfer positivity from the exponential-kernel minor to the corresponding +Gaussian minor. + +The hypothesis is intentionally explicit: it is exactly Karlin III.1's +strict-total-positivity input. Keeping that analytic boundary visible lets us +formalize the Gaussian factorization without assuming Proposition V.1.1. -/ +theorem det_gaussianMatrix_submatrix_pos_of_exponentialKernel {n q : ℕ} + (a : ℝ) (rows cols : Fin q → Fin n) + (hkernel : + 0 < (exponentialKernelMatrix + (fun i => 2 * a * (((rows i : Fin n) : ℕ) : ℝ)) + (fun j => (((cols j : Fin n) : ℕ) : ℝ))).det) : + 0 < ((gaussianMatrix n a).submatrix rows cols).det := by + rw [det_gaussianMatrix_submatrix_eq] + positivity + +/-- The adjacent-difference determinant is positive under the smaller-minor hypothesis. -/ +theorem det_adjacentRowDiff_exponentialKernelMatrix_pos {n : ℕ} + (x : Fin (n + 1) → ℝ) (y : Fin n → ℝ) (hx : StrictMono x) + (hy : ∀ j, 0 < y j) + (hdet : ∀ t : Fin n → ℝ, StrictMono t → + 0 < (exponentialKernelMatrix t y).det) : + 0 < (Matrix.of fun i j => + exponentialKernelMatrix x y i.succ j - + exponentialKernelMatrix x y i.castSucc j).det := by + rw [det_adjacentRowDiff_exponentialKernelMatrix_eq_integral x y hx] + let μ : Fin n → Measure ℝ := fun i => + volume.restrict (Set.Ioc (x i.castSucc) (x i.succ)) + let f : Fin n → ℝ → Fin n → ℝ := fun _ t j => + y j * Real.exp (t * y j) + have hf : ∀ i j, Integrable (fun t => f i t j) (μ i) := by + intro i j + change IntegrableOn (fun t => f i t j) + (Set.Ioc (x i.castSucc) (x i.succ)) volume + rw [← intervalIntegrable_iff_integrableOn_Ioc_of_le + (hx i.castSucc_lt_succ).le] + exact + (continuous_const.mul + (Real.continuous_exp.comp (continuous_id.mul continuous_const))).intervalIntegrable _ _ + have hbox : ∀ᵐ t ∂Measure.pi μ, + ∀ i, t i ∈ Set.Ioc (x i.castSucc) (x i.succ) := by + rw [Filter.eventually_all] + intro i + exact Measure.tendsto_eval_ae_ae.eventually + (ae_restrict_mem measurableSet_Ioc) + have hpoint_pos : ∀ᵐ t ∂Measure.pi μ, + 0 < (Matrix.of fun i j => f i (t i) j).det := by + filter_upwards [hbox] with t ht + have htmono : StrictMono t := by + intro i j hij + exact (ht i).2.trans_lt + ((hx.monotone (Fin.mk_le_mk.mpr (Nat.succ_le_of_lt hij))).trans_lt (ht j).1) + rw [show Matrix.of (fun i j => f i (t i) j) = + Matrix.of fun i j => + y j * exponentialKernelMatrix t y i j by + ext i j + rfl, + Matrix.det_mul_row] + exact mul_pos (Finset.prod_pos fun j _ => hy j) (hdet t htmono) + have hdetInt : Integrable + (fun t : Fin n → ℝ => (Matrix.of fun i j => f i (t i) j).det) + (Measure.pi μ) := + integrable_det_rows μ f hf + have hsupp : Function.support + (fun t : Fin n → ℝ => (Matrix.of fun i j => f i (t i) j).det) =ᵐ[Measure.pi μ] + Set.univ := hpoint_pos.mono fun t ht => by + apply propext + change ((Matrix.of fun i j => f i (t i) j).det ≠ 0) ↔ True + exact iff_true_intro ht.ne' + rw [integral_pos_iff_support_of_nonneg_ae + (hpoint_pos.mono fun _ h => h.le) hdetInt, + measure_congr hsupp, Measure.pi_univ] + rw [pos_iff_ne_zero, Finset.prod_ne_zero_iff] + intro i _ + simpa [μ, Real.volume_Ioc] using hx i.castSucc_lt_succ + +/-- Strictly ordered exponential-kernel minors are positive. -/ +theorem det_exponentialKernelMatrix_pos {q : ℕ} + {x y : Fin q → ℝ} (hx : StrictMono x) (hy : StrictMono y) : + 0 < (exponentialKernelMatrix x y).det := by + induction q with + | zero => simp + | succ n ih => + let y0 : Fin (n + 1) → ℝ := fun j => y j - y 0 + have hy0 : StrictMono y0 := fun _ _ hij => + sub_lt_sub_right (hy hij) _ + have hy00 : y0 0 = 0 := by simp [y0] + have hy_eq : y = fun j => y0 j + y 0 := by + funext j + simp [y0] + rw [hy_eq] + apply (det_exponentialKernelMatrix_add_const_right_pos_iff + x y0 (y 0)).2 + have hfirst : ∀ i, exponentialKernelMatrix x y0 i 0 = 1 := by + intro i + change Real.exp (x i * y0 0) = 1 + rw [hy00] + simp + rw [det_eq_det_adjacentRowDiff_of_firstColumn_eq_one _ hfirst] + let yTail : Fin n → ℝ := fun j => y0 j.succ + have hyTail : StrictMono yTail := hy0.comp Fin.strictMono_succ + have hyTail_pos : ∀ j, 0 < yTail j := by + intro j + exact hy00 ▸ hy0 (by simp) + exact det_adjacentRowDiff_exponentialKernelMatrix_pos + x yTail hx hyTail_pos (fun t ht => ih ht hyTail) + +/-- Strictly ordered minors of Karlin's Gaussian matrix are positive. -/ +theorem det_gaussianMatrix_submatrix_pos {n q : ℕ} + (a : ℝ) (rows cols : Fin q → Fin n) (ha : 0 < a) + (hrows : StrictMono rows) (hcols : StrictMono cols) : + 0 < ((gaussianMatrix n a).submatrix rows cols).det := by + apply det_gaussianMatrix_submatrix_pos_of_exponentialKernel a rows cols + apply det_exponentialKernelMatrix_pos + · exact (Nat.strictMono_cast.comp + (Fin.val_strictMono.comp hrows)).const_mul (by positivity) + · exact Nat.strictMono_cast.comp (Fin.val_strictMono.comp hcols) + +end Matrix diff --git a/RealRooted/Mathlib/LinearAlgebra/Matrix/SignRegular.lean b/RealRooted/Mathlib/LinearAlgebra/Matrix/SignRegular.lean new file mode 100644 index 000000000..11a7dbea7 --- /dev/null +++ b/RealRooted/Mathlib/LinearAlgebra/Matrix/SignRegular.lean @@ -0,0 +1,177 @@ +import RealRooted.Mathlib.LinearAlgebra.Matrix.TotallyNonneg + +/-! +# Sign-consistent and sign-regular rectangular matrices + +This file introduces orientation-free predicates for Karlin's sign-consistent +and sign-regular matrices. Two minors have a common weak (respectively strict) +sign exactly when their product is nonnegative (respectively positive). +-/ + +public section + +namespace Matrix + +variable {R ι κ : Type*} [CommRing R] [PartialOrder R] +variable [Preorder ι] [Preorder κ] + +/-- The minors of order `q` of `M` have a common weak sign. -/ +def IsSignConsistentOrder (M : Matrix ι κ R) (q : ℕ) : Prop := + ∀ ⦃rows rows' : Fin q → ι⦄ ⦃cols cols' : Fin q → κ⦄, + StrictMono rows → StrictMono rows' → StrictMono cols → StrictMono cols' → + 0 ≤ (M.submatrix rows cols).det * (M.submatrix rows' cols').det + +/-- The minors of order `q` of `M` are nonzero and have a common strict sign. -/ +def IsStrictlySignConsistentOrder (M : Matrix ι κ R) (q : ℕ) : Prop := + ∀ ⦃rows rows' : Fin q → ι⦄ ⦃cols cols' : Fin q → κ⦄, + StrictMono rows → StrictMono rows' → StrictMono cols → StrictMono cols' → + 0 < (M.submatrix rows cols).det * (M.submatrix rows' cols').det + +/-- A matrix is sign regular if its minors have a common weak sign at every order. -/ +def IsSignRegular (M : Matrix ι κ R) : Prop := + ∀ q, M.IsSignConsistentOrder q + +/-- A matrix is strictly sign regular if its minors have a common strict sign +at every order. -/ +def IsStrictlySignRegular (M : Matrix ι κ R) : Prop := + ∀ q, M.IsStrictlySignConsistentOrder q + +protected lemma IsSignConsistentOrder.submatrix + {ι' κ' : Type*} [Preorder ι'] [Preorder κ'] {M : Matrix ι κ R} {q : ℕ} + (hM : M.IsSignConsistentOrder q) {rows : ι' → ι} {cols : κ' → κ} + (hrows : StrictMono rows) (hcols : StrictMono cols) : + (M.submatrix rows cols).IsSignConsistentOrder q := by + intro rows₁ rows₂ cols₁ cols₂ hrows₁ hrows₂ hcols₁ hcols₂ + simpa using hM (hrows.comp hrows₁) (hrows.comp hrows₂) + (hcols.comp hcols₁) (hcols.comp hcols₂) + +protected lemma IsStrictlySignConsistentOrder.submatrix + {ι' κ' : Type*} [Preorder ι'] [Preorder κ'] {M : Matrix ι κ R} {q : ℕ} + (hM : M.IsStrictlySignConsistentOrder q) {rows : ι' → ι} {cols : κ' → κ} + (hrows : StrictMono rows) (hcols : StrictMono cols) : + (M.submatrix rows cols).IsStrictlySignConsistentOrder q := by + intro rows₁ rows₂ cols₁ cols₂ hrows₁ hrows₂ hcols₁ hcols₂ + simpa using hM (hrows.comp hrows₁) (hrows.comp hrows₂) + (hcols.comp hcols₁) (hcols.comp hcols₂) + +omit [PartialOrder R] [Preorder ι] [Preorder κ] in +private lemma det_transpose_submatrix + (M : Matrix ι κ R) {q : ℕ} (rows : Fin q → κ) (cols : Fin q → ι) : + (M.transpose.submatrix rows cols).det = (M.submatrix cols rows).det := by + rw [← Matrix.det_transpose (M.submatrix cols rows), Matrix.transpose_submatrix] + +protected lemma IsSignConsistentOrder.transpose {M : Matrix ι κ R} {q : ℕ} + (hM : M.IsSignConsistentOrder q) : M.transpose.IsSignConsistentOrder q := by + intro rows rows' cols cols' hrows hrows' hcols hcols' + rw [det_transpose_submatrix M rows cols, det_transpose_submatrix M rows' cols'] + exact hM hcols hcols' hrows hrows' + +protected lemma IsStrictlySignConsistentOrder.transpose {M : Matrix ι κ R} {q : ℕ} + (hM : M.IsStrictlySignConsistentOrder q) : + M.transpose.IsStrictlySignConsistentOrder q := by + intro rows rows' cols cols' hrows hrows' hcols hcols' + rw [det_transpose_submatrix M rows cols, det_transpose_submatrix M rows' cols'] + exact hM hcols hcols' hrows hrows' + +protected lemma IsSignRegular.submatrix + {ι' κ' : Type*} [Preorder ι'] [Preorder κ'] {M : Matrix ι κ R} + (hM : M.IsSignRegular) {rows : ι' → ι} {cols : κ' → κ} + (hrows : StrictMono rows) (hcols : StrictMono cols) : + (M.submatrix rows cols).IsSignRegular := + fun q ↦ (hM q).submatrix hrows hcols + +protected lemma IsStrictlySignRegular.submatrix + {ι' κ' : Type*} [Preorder ι'] [Preorder κ'] {M : Matrix ι κ R} + (hM : M.IsStrictlySignRegular) {rows : ι' → ι} {cols : κ' → κ} + (hrows : StrictMono rows) (hcols : StrictMono cols) : + (M.submatrix rows cols).IsStrictlySignRegular := + fun q ↦ (hM q).submatrix hrows hcols + +protected lemma IsSignRegular.transpose {M : Matrix ι κ R} + (hM : M.IsSignRegular) : M.transpose.IsSignRegular := + fun q ↦ (hM q).transpose + +protected lemma IsStrictlySignRegular.transpose {M : Matrix ι κ R} + (hM : M.IsStrictlySignRegular) : M.transpose.IsStrictlySignRegular := + fun q ↦ (hM q).transpose + +protected lemma IsStrictlySignConsistentOrder.toSignConsistentOrder + {M : Matrix ι κ R} {q : ℕ} (hM : M.IsStrictlySignConsistentOrder q) : + M.IsSignConsistentOrder q := by + intro rows rows' cols cols' hrows hrows' hcols hcols' + exact (hM hrows hrows' hcols hcols').le + +protected lemma IsStrictlySignRegular.toSignRegular {M : Matrix ι κ R} + (hM : M.IsStrictlySignRegular) : M.IsSignRegular := + fun q ↦ (hM q).toSignConsistentOrder + +section OrderedRing + +variable [IsStrictOrderedRing R] +variable {ι' κ' : Type*} [PartialOrder ι'] [PartialOrder κ'] + +lemma IsTotallyNonnegRect.isSignConsistentOrder {M : Matrix ι' κ' R} + (hM : M.IsTotallyNonnegRect) (q : ℕ) : M.IsSignConsistentOrder q := by + intro rows rows' cols cols' hrows hrows' hcols hcols' + exact mul_nonneg (hM hrows hcols) (hM hrows' hcols') + +lemma IsTotallyNonnegRect.isSignRegular {M : Matrix ι' κ' R} + (hM : M.IsTotallyNonnegRect) : M.IsSignRegular := + fun q ↦ hM.isSignConsistentOrder q + +lemma isStrictlySignConsistentOrder_of_posMinors {M : Matrix ι κ R} {q : ℕ} + (hM : + ∀ ⦃rows : Fin q → ι⦄ ⦃cols : Fin q → κ⦄, + StrictMono rows → StrictMono cols → 0 < (M.submatrix rows cols).det) : + M.IsStrictlySignConsistentOrder q := by + intro rows rows' cols cols' hrows hrows' hcols hcols' + exact mul_pos (hM hrows hcols) (hM hrows' hcols') + +end OrderedRing + +lemma IsSignConsistentOrder.minorProduct_nonneg {M : Matrix ι κ R} {q : ℕ} + (hM : M.IsSignConsistentOrder q) {cols : Fin q → κ} (hcols : StrictMono cols) : + ∀ ⦃rows rows' : Fin q → ι⦄, + StrictMono rows → StrictMono rows' → + 0 ≤ (M.submatrix rows cols).det * (M.submatrix rows' cols).det := by + intro rows rows' hrows hrows' + exact hM hrows hrows' hcols hcols + +lemma IsStrictlySignConsistentOrder.minorProduct_pos + {M : Matrix ι κ R} {q : ℕ} (hM : M.IsStrictlySignConsistentOrder q) + {cols : Fin q → κ} (hcols : StrictMono cols) : + ∀ ⦃rows rows' : Fin q → ι⦄, + StrictMono rows → StrictMono rows' → + 0 < (M.submatrix rows cols).det * (M.submatrix rows' cols).det := by + intro rows rows' hrows hrows' + exact hM hrows hrows' hcols hcols + +section LinearOrder + +variable {S : Type*} [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] + +lemma IsSignConsistentOrder.minor_nonneg_of_pos + {M : Matrix ι κ S} {q : ℕ} (hM : M.IsSignConsistentOrder q) + {rows₀ : Fin q → ι} {cols₀ : Fin q → κ} + (hrows₀ : StrictMono rows₀) (hcols₀ : StrictMono cols₀) + (href : 0 < (M.submatrix rows₀ cols₀).det) + {rows : Fin q → ι} {cols : Fin q → κ} + (hrows : StrictMono rows) (hcols : StrictMono cols) : + 0 ≤ (M.submatrix rows cols).det := + nonneg_of_mul_nonneg_left + (hM hrows hrows₀ hcols hcols₀) href + +lemma IsSignConsistentOrder.minor_nonpos_of_neg + {M : Matrix ι κ S} {q : ℕ} (hM : M.IsSignConsistentOrder q) + {rows₀ : Fin q → ι} {cols₀ : Fin q → κ} + (hrows₀ : StrictMono rows₀) (hcols₀ : StrictMono cols₀) + (href : (M.submatrix rows₀ cols₀).det < 0) + {rows : Fin q → ι} {cols : Fin q → κ} + (hrows : StrictMono rows) (hcols : StrictMono cols) : + (M.submatrix rows cols).det ≤ 0 := + nonpos_of_mul_nonneg_left + (hM hrows hrows₀ hcols hcols₀) href + +end LinearOrder + +end Matrix diff --git a/RealRooted/Mathlib/LinearAlgebra/Matrix/SignRegularRankDeficient.lean b/RealRooted/Mathlib/LinearAlgebra/Matrix/SignRegularRankDeficient.lean new file mode 100644 index 000000000..debb5ae47 --- /dev/null +++ b/RealRooted/Mathlib/LinearAlgebra/Matrix/SignRegularRankDeficient.lean @@ -0,0 +1,930 @@ +import Mathlib.LinearAlgebra.LinearIndependent.Lemmas +import Mathlib.LinearAlgebra.Matrix.Rank +import RealRooted.Mathlib.LinearAlgebra.Matrix.SignRegularVariation + +/-! +# Rank-deficient sign-consistent matrices + +This file develops the rank-deficient induction in Karlin, *Total Positivity*, +Volume I, Chapter V, Section 1, Theorem 1.3. The first lemmas formalize the +selected-row kernel perturbation in equations (1.1) on printed pages 221--222. +-/ + +/-- A finite matrix of rank `r` has a nonzero `r`-minor with increasingly +ordered row and column selectors. -/ +theorem Matrix.exists_ordered_minor_ne_zero_of_rank_eq + {R : Type*} [Field R] {n m r : ℕ} + (A : Matrix (Fin n) (Fin m) R) (hrank : A.rank = r) : + ∃ rows : Fin r → Fin n, ∃ cols : Fin r → Fin m, + StrictMono rows ∧ StrictMono cols ∧ + (A.submatrix rows cols).det ≠ 0 := by + obtain ⟨κ, a, ha, hspan, hli⟩ := + exists_linearIndependent' R A.col + letI : Finite κ := Finite.of_injective a ha + letI : Fintype κ := Fintype.ofFinite κ + have hcard : Fintype.card κ = r := by + calc + Fintype.card κ = + Module.finrank R (Submodule.span R (Set.range (A.col ∘ a))) := + (finrank_span_eq_card hli).symm + _ = Module.finrank R (Submodule.span R (Set.range A.col)) := by + rw [hspan] + _ = A.rank := (Matrix.rank_eq_finrank_span_cols A).symm + _ = r := hrank + let e : Fin r ≃ κ := (Fintype.equivFinOfCardEq hcard).symm + let f : Fin r → Fin m := a ∘ e + have hf : Function.Injective f := ha.comp e.injective + let B : Matrix (Fin n) (Fin r) R := A.submatrix id f + have hB : Function.Injective B.mulVec := by + rw [Matrix.mulVec_injective_iff] + change LinearIndependent R (A.col ∘ f) + simpa only [f, Function.comp_assoc] using hli.comp e e.injective + obtain ⟨rows, hrows, hdet⟩ := + Matrix.exists_ordered_minor_ne_zero_of_mulVec_injective + B hB id strictMono_id + have hdetf : (A.submatrix rows f).det ≠ 0 := by + simpa only [B, Matrix.submatrix_submatrix, Function.id_comp, + Function.comp_id] using hdet + obtain ⟨s, p, hp⟩ := + Set.powersetCard.exists_orderEmb_comp_perm_eq_of_injective f hf + let cols : Fin r ↪o Fin m := Set.powersetCard.ofFinEmbEquiv.symm s + refine ⟨rows, cols, hrows, cols.strictMono, ?_⟩ + intro hzero + apply hdetf + have hmatrix : + A.submatrix rows f = + (A.submatrix rows cols).submatrix id p := by + ext i j + simp only [Matrix.submatrix_apply, id_eq] + rw [hp j] + rw [hmatrix, Matrix.det_permute', hzero, mul_zero] + +/-- Karlin's signed row-cofactor vector of a singular square matrix lies in +its kernel. The retained-row equations come from the rectangular alternating +minor identity; Laplace expansion supplies the omitted-row equation. -/ +theorem Matrix.mulVec_signedRowCofactor_eq_zero_of_det_eq_zero + {R : Type*} [CommRing R] {k : ℕ} + (B : Matrix (Fin (k + 1)) (Fin (k + 1)) R) + (i0 : Fin (k + 1)) (hdet : B.det = 0) : + B.mulVec (fun j => (-1 : R) ^ (i0 + j : ℕ) * + (B.submatrix i0.succAbove j.succAbove).det) = 0 := by + let C : Matrix (Fin k) (Fin (k + 1)) R := + B.submatrix i0.succAbove id + have hminor (j : Fin (k + 1)) : + ((C.transpose).submatrix j.succAbove id).det = + (B.submatrix i0.succAbove j.succAbove).det := by + rw [← Matrix.det_transpose] + rfl + let z0 : Fin (k + 1) → R := fun j => + (-1 : R) ^ (j : ℕ) * (B.submatrix i0.succAbove j.succAbove).det + let z : Fin (k + 1) → R := fun j => + (-1 : R) ^ (i0 + j : ℕ) * (B.submatrix i0.succAbove j.succAbove).det + have hremoved0 : C.mulVec z0 = 0 := by + have hkernel := + Matrix.transpose_mulVec_alternating_det_submatrix_succAbove C.transpose + rw [Matrix.transpose_transpose] at hkernel + simp_rw [hminor] at hkernel + simpa only [z0] using hkernel + have hz : z = (-1 : R) ^ (i0 : ℕ) • z0 := by + funext j + simp only [z, z0, Pi.smul_apply, smul_eq_mul, pow_add, mul_assoc] + have hremoved : C.mulVec z = 0 := by + rw [hz, Matrix.mulVec_smul, hremoved0, smul_zero] + change B.mulVec z = 0 + apply funext + refine Fin.succAboveCases i0 ?_ (fun i => ?_) + · simp only [Matrix.mulVec, dotProduct, z, Pi.zero_apply] + calc + ∑ j : Fin (k + 1), B i0 j * ((-1 : R) ^ + ((i0 : ℕ) + (j : ℕ)) * + (B.submatrix i0.succAbove j.succAbove).det) = + ∑ j : Fin (k + 1), (-1 : R) ^ ((i0 : ℕ) + (j : ℕ)) * + B i0 j * (B.submatrix i0.succAbove j.succAbove).det := by + apply Finset.sum_congr rfl + intro j _ + ring + _ = B.det := (Matrix.det_succ_row B i0).symm + _ = 0 := hdet + · have hi := congrFun hremoved i + simpa only [C, Matrix.mulVec, dotProduct, Matrix.submatrix_apply, id_eq, + Pi.zero_apply] using hi + +/-- Deleting a column preserves the rank when a maximal nonzero minor avoids +that column. This is the common rank step in Karlin's two deficient-rank +branches; the cofactor and rank-basis kernel constructions remain separate. -/ +theorem Matrix.rank_deleteColumn_eq_of_minor_ne_zero + {R : Type*} [Field R] {n k r : ℕ} + (A : Matrix (Fin n) (Fin (k + 1)) R) + (hrank : A.rank = r) (j0 : Fin (k + 1)) + (rows : Fin r → Fin n) (cols : Fin r → Fin k) + (hminor : + (A.submatrix rows (j0.succAbove ∘ cols)).det ≠ 0) : + (A.submatrix id j0.succAbove).rank = r := by + let A' : Matrix (Fin n) (Fin k) R := A.submatrix id j0.succAbove + have hdet : (A'.submatrix rows cols).det ≠ 0 := by + simpa only [A', Matrix.submatrix_submatrix, Function.id_comp] using hminor + have hunit : IsUnit (A'.submatrix rows cols) := by + rw [Matrix.isUnit_iff_isUnit_det, isUnit_iff_ne_zero] + exact hdet + apply le_antisymm + · calc + A'.rank ≤ A.rank := Matrix.rank_submatrix_le A id j0.succAbove + _ = r := hrank + · calc + r = (A'.submatrix rows cols).rank := by + simpa using (Matrix.rank_of_isUnit _ hunit).symm + _ ≤ A'.rank := Matrix.rank_submatrix_le A' rows cols + +/-- Karlin's nonzero-cofactor branch for a selected singular square submatrix. +The displayed signed cofactor vector witnesses the selected-row kernel, while +the same cofactor proves both the ambient rank and rank-preserving deletion. -/ +theorem Matrix.signedRowCofactor_spec_of_minor_ne_zero + {R : Type*} [Field R] {n k : ℕ} + (A : Matrix (Fin n) (Fin (k + 1)) R) + (rows : Fin (k + 1) → Fin n) (i0 j0 : Fin (k + 1)) + (hrank_lt : A.rank < k + 1) + (hminor : + ((A.submatrix rows id).submatrix + i0.succAbove j0.succAbove).det ≠ 0) : + let B := A.submatrix rows id + let z : Fin (k + 1) → R := fun j => + (-1 : R) ^ (i0 + j : ℕ) * + (B.submatrix i0.succAbove j.succAbove).det + A.rank = k ∧ B.mulVec z = 0 ∧ z j0 ≠ 0 ∧ + (A.submatrix id j0.succAbove).rank = k := by + let B : Matrix (Fin (k + 1)) (Fin (k + 1)) R := + A.submatrix rows id + let z : Fin (k + 1) → R := fun j => + (-1 : R) ^ (i0 + j : ℕ) * + (B.submatrix i0.succAbove j.succAbove).det + change A.rank = k ∧ B.mulVec z = 0 ∧ z j0 ≠ 0 ∧ + (A.submatrix id j0.succAbove).rank = k + have hunit : IsUnit (B.submatrix i0.succAbove j0.succAbove) := by + rw [Matrix.isUnit_iff_isUnit_det, isUnit_iff_ne_zero] + simpa only [B] using hminor + have hcofactor_rank : + (B.submatrix i0.succAbove j0.succAbove).rank = k := by + simpa using Matrix.rank_of_isUnit _ hunit + have hrank_ge : k ≤ A.rank := by + calc + k = (B.submatrix i0.succAbove j0.succAbove).rank := + hcofactor_rank.symm + _ ≤ B.rank := + Matrix.rank_submatrix_le B i0.succAbove j0.succAbove + _ ≤ A.rank := Matrix.rank_submatrix_le A rows id + have hrank : A.rank = k := by + lia + have hdet : B.det = 0 := by + by_contra hdet + have hBunit : IsUnit B := by + rw [Matrix.isUnit_iff_isUnit_det, isUnit_iff_ne_zero] + exact hdet + have hBrank : B.rank = k + 1 := by + simpa using Matrix.rank_of_isUnit B hBunit + have hle : B.rank ≤ A.rank := Matrix.rank_submatrix_le A rows id + rw [hBrank, hrank] at hle + lia + have hkernel : B.mulVec z = 0 := by + exact B.mulVec_signedRowCofactor_eq_zero_of_det_eq_zero i0 hdet + have hzj0 : z j0 ≠ 0 := by + exact mul_ne_zero (pow_ne_zero _ (by simp)) (by + simpa only [B] using hminor) + have hminorA : + (A.submatrix (rows ∘ i0.succAbove) + (j0.succAbove ∘ (id : Fin k → Fin k))).det ≠ 0 := by + simpa only [B, Matrix.submatrix_submatrix, Function.id_comp, + Function.comp_id] using hminor + have hdelete : + (A.submatrix id j0.succAbove).rank = k := + A.rank_deleteColumn_eq_of_minor_ne_zero hrank j0 + (rows ∘ i0.succAbove) id hminorA + exact ⟨hrank, hkernel, hzj0, hdelete⟩ + +/-- A zero coefficient can be removed together with its matrix column when +forming a matrix-vector product. -/ +theorem Matrix.mulVec_eq_deleteColumn_mulVec_removeNth_of_apply_eq_zero + {R : Type*} [NonUnitalNonAssocSemiring R] {n k : ℕ} + (A : Matrix (Fin n) (Fin (k + 1)) R) + (d : Fin (k + 1) → R) (j0 : Fin (k + 1)) + (hd : d j0 = 0) : + A.mulVec d = + (A.submatrix id j0.succAbove).mulVec (Fin.removeNth j0 d) := by + funext i + simp only [Matrix.mulVec, dotProduct, Matrix.submatrix_apply, id_eq, + Fin.removeNth] + rw [Fin.sum_univ_succAbove (fun j => A i j * d j) j0, hd, mul_zero, + zero_add] + +/-- Karlin's coefficient cancellation: perturb by the unique scalar that +zeros coordinate `j0`, then remove that coordinate and its matrix column. -/ +theorem Matrix.mulVec_add_neg_div_smul_eq_deleteColumn_mulVec + {R : Type*} [DivisionRing R] {n k : ℕ} + (A : Matrix (Fin n) (Fin (k + 1)) R) + (c z : Fin (k + 1) → R) (j0 : Fin (k + 1)) + (hz : z j0 ≠ 0) : + A.mulVec (c + (-c j0 / z j0) • z) = + (A.submatrix id j0.succAbove).mulVec + (Fin.removeNth j0 (c + (-c j0 / z j0) • z)) := by + apply A.mulVec_eq_deleteColumn_mulVec_removeNth_of_apply_eq_zero + simp only [Pi.add_apply, Pi.smul_apply, smul_eq_mul] + rw [div_mul_cancel₀ _ hz, add_neg_cancel] + +/-- Perturbing coefficients along a vector annihilated by a selected-row +submatrix does not change the selected coordinates of the matrix-vector +product. -/ +theorem Matrix.mulVec_add_smul_apply_eq_of_submatrix_mulVec_eq_zero + {n m k : ℕ} (A : Matrix (Fin n) (Fin m) ℝ) + (rows : Fin k → Fin n) (c z : Fin m → ℝ) + (hz : (A.submatrix rows id).mulVec z = 0) + (t : ℝ) (i : Fin k) : + A.mulVec (c + t • z) (rows i) = A.mulVec c (rows i) := by + have hzi : A.mulVec z (rows i) = 0 := by + have hi := congrFun hz i + simpa only [Matrix.mulVec, dotProduct, Matrix.submatrix_apply, id_eq, + Pi.zero_apply] using hi + rw [Matrix.mulVec_add, Matrix.mulVec_smul] + simp [hzi] + +/-- A selected alternating witness survives Karlin's kernel perturbation of +the coefficient vector. -/ +theorem Fin.StrictlyAlternates.matrix_mulVec_add_smul + {n m k : ℕ} {A : Matrix (Fin n) (Fin m) ℝ} + {rows : Fin (k + 1) → Fin n} {c z : Fin m → ℝ} + (h : StrictlyAlternates (fun i => A.mulVec c (rows i))) + (hz : (A.submatrix rows id).mulVec z = 0) + (t : ℝ) : + StrictlyAlternates (fun i => A.mulVec (c + t • z) (rows i)) := by + intro i + change + A.mulVec (c + t • z) (rows i.castSucc) * + A.mulVec (c + t • z) (rows i.succ) < 0 + have heq (j : Fin (k + 1)) := + A.mulVec_add_smul_apply_eq_of_submatrix_mulVec_eq_zero rows c z hz t j + rw [heq i.castSucc, heq i.succ] + exact h i + +/-- Karlin's nonzero-cofactor branch contradicts the full-rank variation +bound after the source-prescribed coefficient cancellation and column +deletion. -/ +theorem Matrix.IsSignConsistentOrder.not_strictlyAlternates_mulVec_of_cofactor_ne_zero + {n k : ℕ} {A : Matrix (Fin n) (Fin (k + 1)) ℝ} + (hA : A.IsSignConsistentOrder k) + (hk : 0 < k) + (rows : Fin (k + 1) → Fin n) (hrows : StrictMono rows) + (i0 j0 : Fin (k + 1)) + (hrank_lt : A.rank < k + 1) + (hminor : + ((A.submatrix rows id).submatrix + i0.succAbove j0.succAbove).det ≠ 0) + (c : Fin (k + 1) → ℝ) + (hAlt : Fin.StrictlyAlternates (fun i => A.mulVec c (rows i))) : + False := by + let B : Matrix (Fin (k + 1)) (Fin (k + 1)) ℝ := + A.submatrix rows id + let z : Fin (k + 1) → ℝ := fun j => + (-1 : ℝ) ^ (i0 + j : ℕ) * + (B.submatrix i0.succAbove j.succAbove).det + let A' : Matrix (Fin n) (Fin k) ℝ := + A.submatrix id j0.succAbove + have hcase : + A.rank = k ∧ B.mulVec z = 0 ∧ z j0 ≠ 0 ∧ A'.rank = k := by + simpa only [B, z, A'] using + A.signedRowCofactor_spec_of_minor_ne_zero + rows i0 j0 hrank_lt hminor + obtain ⟨_hrank, hkernel, hzj0, hdelete⟩ := hcase + let t0 : ℝ := -c j0 / z j0 + let d : Fin (k + 1) → ℝ := c + t0 • z + let d' : Fin k → ℝ := Fin.removeNth j0 d + have hAltPert : + Fin.StrictlyAlternates (fun i => A.mulVec d (rows i)) := by + simpa only [d, t0] using + hAlt.matrix_mulVec_add_smul hkernel t0 + have hreassemble : A.mulVec d = A'.mulVec d' := by + simpa only [A', d', d, t0] using + A.mulVec_add_neg_div_smul_eq_deleteColumn_mulVec c z j0 hzj0 + have hAltDeleted : + Fin.StrictlyAlternates (fun i => A'.mulVec d' (rows i)) := by + rw [hreassemble] at hAltPert + exact hAltPert + have hA' : A'.IsSignConsistentOrder k := by + exact hA.submatrix strictMono_id (Fin.strictMono_succAbove j0) + have hk1n : k + 1 ≤ n := by + simpa using Fintype.card_le_of_injective rows hrows.injective + have hkn : k ≤ n := (Nat.le_succ k).trans hk1n + have hA'inj : Function.Injective A'.mulVec := by + rw [Matrix.mulVec_injective_iff, + linearIndependent_iff_card_eq_finrank_span] + simpa only [Fintype.card_fin, Set.finrank] using + hdelete.symm.trans (Matrix.rank_eq_finrank_span_cols A') + have hlower : k ≤ Fin.signVariations (A'.mulVec d') := + hAltDeleted.le_signVariations_of_strictMono hrows + have hupper : Fin.signVariations (A'.mulVec d') ≤ k - 1 := + hA'.signVariations_mulVec_le_card_sub_one hkn hA'inj d' + lia + +/-- Extending a coefficient vector by zero along an injective column selector +turns the ambient matrix-vector product into the selected-column product. -/ +theorem Matrix.mulVec_extend_eq_submatrix_mulVec + {R : Type*} [NonUnitalNonAssocSemiring R] + {ι κ κ' : Type*} [Fintype κ] [Fintype κ'] + (A : Matrix ι κ R) (cols : κ' → κ) + (hcols : Function.Injective cols) (d : κ' → R) : + A.mulVec (Function.extend cols d 0) = + (A.submatrix id cols).mulVec d := by + classical + funext i + simp only [Matrix.mulVec, dotProduct, Matrix.submatrix_apply, id_eq] + symm + apply Fintype.sum_of_injective cols hcols + · intro j hj + rw [Function.extend_apply' d (0 : κ → R) j hj, Pi.zero_apply, + mul_zero] + · intro j + rw [hcols.extend_apply d (0 : κ → R) j] + +/-- Karlin's repaired Case B relation after coordinates of the omitted column +in the retained column basis have been chosen. The relation is explicitly +supported on those basis columns and `j0`; no arbitrary kernel coordinate is +prescribed. -/ +theorem Matrix.supportedColumnRelation_spec + {R : Type*} [Field R] {n m r : ℕ} + (A : Matrix (Fin n) (Fin (m + 1)) R) + (j0 : Fin (m + 1)) + (rows : Fin r → Fin n) (cols : Fin r → Fin m) + (hcols : Function.Injective cols) + (hrank : A.rank = r) + (hminor : + (A.submatrix rows (j0.succAbove ∘ cols)).det ≠ 0) + (d : Fin r → R) + (hcombo : + (A.submatrix id (j0.succAbove ∘ cols)).mulVec d = A.col j0) : + let selected := j0.succAbove ∘ cols + let z : Fin (m + 1) → R := + Function.extend selected d 0 - Pi.single j0 1 + A.mulVec z = 0 ∧ z j0 = -1 ∧ + (A.submatrix id j0.succAbove).rank = r := by + let selected : Fin r → Fin (m + 1) := j0.succAbove ∘ cols + let z : Fin (m + 1) → R := + Function.extend selected d 0 - Pi.single j0 1 + change A.mulVec z = 0 ∧ z j0 = -1 ∧ + (A.submatrix id j0.succAbove).rank = r + have hselected : Function.Injective selected := + (Fin.strictMono_succAbove j0).injective.comp hcols + have hj0 : j0 ∉ Set.range selected := by + rintro ⟨i, hi⟩ + exact (Fin.succAbove_ne j0 (cols i)) (by + simpa only [selected, Function.comp_apply] using hi) + have hkernel : A.mulVec z = 0 := by + change A.mulVec + (Function.extend selected d 0 - Pi.single j0 1) = 0 + rw [Matrix.mulVec_sub, + A.mulVec_extend_eq_submatrix_mulVec selected hselected d, + Matrix.mulVec_single_one] + simpa only [selected] using sub_eq_zero.mpr hcombo + have hzj0 : z j0 = -1 := by + simp only [z, Pi.sub_apply] + rw [Function.extend_apply' d (0 : Fin (m + 1) → R) j0 hj0, + Pi.zero_apply, Pi.single_eq_same, zero_sub] + exact ⟨hkernel, hzj0, + A.rank_deleteColumn_eq_of_minor_ne_zero hrank j0 rows cols hminor⟩ + +/-- A rank-sized minor avoiding `j0` produces Karlin's supported Case B +relation and proves that deleting `j0` preserves rank. The printed source's +arbitrary-coordinate assertion is not used: equality of the retained and +ambient column-space dimensions supplies the omitted column's coordinates. -/ +theorem Matrix.exists_supportedColumnRelation_of_minor_ne_zero + {R : Type*} [Field R] {n m r : ℕ} + (A : Matrix (Fin n) (Fin (m + 1)) R) + (j0 : Fin (m + 1)) + (rows : Fin r → Fin n) (cols : Fin r → Fin m) + (hcols : Function.Injective cols) + (hrank : A.rank = r) + (hminor : + (A.submatrix rows (j0.succAbove ∘ cols)).det ≠ 0) : + ∃ d : Fin r → R, + let selected := j0.succAbove ∘ cols + let z : Fin (m + 1) → R := + Function.extend selected d 0 - Pi.single j0 1 + A.mulVec z = 0 ∧ z j0 = -1 ∧ + (A.submatrix id j0.succAbove).rank = r := by + let selected : Fin r → Fin (m + 1) := j0.succAbove ∘ cols + let B : Matrix (Fin n) (Fin r) R := A.submatrix id selected + have hunit : IsUnit (B.submatrix rows id) := by + rw [Matrix.isUnit_iff_isUnit_det, isUnit_iff_ne_zero] + simpa only [B, selected, Matrix.submatrix_submatrix, + Function.id_comp, Function.comp_id] using hminor + have hminor_rank : (B.submatrix rows id).rank = r := by + simpa using Matrix.rank_of_isUnit _ hunit + have hBge : r ≤ B.rank := by + calc + r = (B.submatrix rows id).rank := hminor_rank.symm + _ ≤ B.rank := Matrix.rank_submatrix_le B rows id + have hBle : B.rank ≤ r := by + calc + B.rank ≤ A.rank := Matrix.rank_submatrix_le A id selected + _ = r := hrank + have hBrank : B.rank = r := le_antisymm hBle hBge + have hrange_le : + LinearMap.range B.mulVecLin ≤ LinearMap.range A.mulVecLin := by + rw [Matrix.range_mulVecLin, Matrix.range_mulVecLin] + apply Submodule.span_mono + rintro _ ⟨j, rfl⟩ + exact ⟨selected j, rfl⟩ + have hrange : + LinearMap.range B.mulVecLin = LinearMap.range A.mulVecLin := + Submodule.eq_of_le_of_finrank_le hrange_le (by + change A.rank ≤ B.rank + rw [hrank, hBrank]) + have hcol : A.col j0 ∈ LinearMap.range B.mulVecLin := by + rw [hrange] + refine ⟨Pi.single j0 1, ?_⟩ + simpa only [Matrix.mulVecLin_apply] using A.mulVec_single_one j0 + obtain ⟨d, hd⟩ := hcol + refine ⟨d, ?_⟩ + have hcombo : + (A.submatrix id (j0.succAbove ∘ cols)).mulVec d = + A.col j0 := by + simpa only [B, selected, Matrix.mulVecLin_apply] using hd + exact A.supportedColumnRelation_spec j0 rows cols hcols hrank + hminor d hcombo + +/-- Karlin's deficient-rank induction adapter. The printed proof's claim that +an arbitrary kernel coordinate can be prescribed is false in general. Instead, +we choose `j0` outside the columns of a nonzero rank-sized minor. That minor +survives deletion of `j0`, while the selected columns express column `j0` +and produce a kernel relation whose `j0` coordinate is nonzero. -/ +theorem Matrix.exists_kernelVector_apply_ne_zero_rank_deleteColumn_eq_of_rank_lt + {R : Type*} [Field R] {n k r : ℕ} + (A : Matrix (Fin n) (Fin (k + 1)) R) + (hrank : A.rank = r) (hrank_lt : r < k + 1) : + ∃ j0 : Fin (k + 1), ∃ z : Fin (k + 1) → R, + A.mulVec z = 0 ∧ z j0 ≠ 0 ∧ + (A.submatrix id j0.succAbove).rank = r := by + classical + obtain ⟨rows, cols, _, hcols, hminor⟩ := + A.exists_ordered_minor_ne_zero_of_rank_eq hrank + have hcols_not_surj : ¬ Function.Surjective cols := by + intro hsurj + apply not_le_of_gt hrank_lt + simpa only [Fintype.card_fin] using + Fintype.card_le_of_surjective cols hsurj + obtain ⟨j0, hj0⟩ : ∃ j0, ∀ i, cols i ≠ j0 := by + simpa only [Function.Surjective, not_forall, not_exists] using + hcols_not_surj + choose cols' hcols' using fun i => + Fin.exists_succAbove_eq (hj0 i) + have hcols_factor : j0.succAbove ∘ cols' = cols := by + funext i + exact hcols' i + have hcols'_inj : Function.Injective cols' := by + intro i j hij + apply hcols.injective + rw [← hcols_factor] + exact congrArg j0.succAbove hij + have hminor' : + (A.submatrix rows (j0.succAbove ∘ cols')).det ≠ 0 := by + simpa only [hcols_factor] using hminor + obtain ⟨d, hkernel, hzj0, hdelete⟩ := + A.exists_supportedColumnRelation_of_minor_ne_zero + j0 rows cols' hcols'_inj hrank hminor' + refine ⟨j0, + Function.extend (j0.succAbove ∘ cols') d 0 - Pi.single j0 1, + hkernel, ?_, hdelete⟩ + rw [hzj0] + exact neg_ne_zero.mpr one_ne_zero + +/-- Karlin's positive-rank, one-column induction step for the deficient-rank +case. The induction hypothesis handles the rank-preserving matrix obtained by +deleting the column selected by +`exists_kernelVector_apply_ne_zero_rank_deleteColumn_eq_of_rank_lt`. -/ +theorem Matrix.IsSignConsistentOrder.signVariations_mulVec_le_rank_sub_one_of_induction + {n k r : ℕ} + {A : Matrix (Fin n) (Fin (k + 1)) ℝ} + (hA : A.IsSignConsistentOrder r) + (hrank : A.rank = r) + (hrank_lt : r < k + 1) + (hr : 0 < r) + (hind : + ∀ {B : Matrix (Fin n) (Fin k) ℝ}, + B.IsSignConsistentOrder r → + B.rank = r → + ∀ d : Fin k → ℝ, + Fin.signVariations (B.mulVec d) ≤ r - 1) + (c : Fin (k + 1) → ℝ) : + Fin.signVariations (A.mulVec c) ≤ r - 1 := by + by_contra hle + have hbad : r ≤ Fin.signVariations (A.mulVec c) := by + lia + obtain ⟨rows, hrows, halt⟩ := + Fin.exists_strictMono_strictlyAlternates_of_le_signVariations hr hbad + obtain ⟨j0, z, hkernel, hzj0, hdelete⟩ := + A.exists_kernelVector_apply_ne_zero_rank_deleteColumn_eq_of_rank_lt + hrank hrank_lt + have hzrows : (A.submatrix rows id).mulVec z = 0 := by + funext i + simpa only [Matrix.mulVec, Matrix.submatrix_apply, id_eq, + Pi.zero_apply] using congrFun hkernel (rows i) + let t : ℝ := -c j0 / z j0 + let d : Fin (k + 1) → ℝ := c + t • z + let B : Matrix (Fin n) (Fin k) ℝ := + A.submatrix id j0.succAbove + let d' : Fin k → ℝ := Fin.removeNth j0 d + have halt_d : + Fin.StrictlyAlternates (fun i => A.mulVec d (rows i)) := by + simpa only [d] using halt.matrix_mulVec_add_smul hzrows t + have hcancel : A.mulVec d = B.mulVec d' := by + simpa only [d, t, B, d'] using + A.mulVec_add_neg_div_smul_eq_deleteColumn_mulVec c z j0 hzj0 + have halt_delete : + Fin.StrictlyAlternates (fun i => B.mulVec d' (rows i)) := by + rw [← hcancel] + exact halt_d + have hB : B.IsSignConsistentOrder r := + hA.submatrix strictMono_id (Fin.strictMono_succAbove j0) + have hupper := hind hB hdelete d' + have hlower := halt_delete.le_signVariations_of_strictMono hrows + lia + +open Filter Topology + +/-- Karlin's rank-sensitive variation bound, proved by induction on the number +of columns. Rank zero gives the zero linear map, full column rank uses the +injective variation bound, and positive deficient rank uses the +rank-preserving deletion step. -/ +theorem Matrix.IsSignConsistentOrder.signVariations_mulVec_le_rank_sub_one + {n m r : ℕ} + {A : Matrix (Fin n) (Fin m) ℝ} + (hA : A.IsSignConsistentOrder r) + (hrank : A.rank = r) + (c : Fin m → ℝ) : + Fin.signVariations (A.mulVec c) ≤ r - 1 := by + have hzero : + ∀ {p : ℕ} {B : Matrix (Fin n) (Fin p) ℝ}, + B.rank = 0 → + ∀ d : Fin p → ℝ, + Fin.signVariations (B.mulVec d) ≤ 0 := by + intro p B hBrank d + have hlin : B.mulVecLin = 0 := + LinearMap.range_eq_bot.mp + (Submodule.finrank_eq_zero.mp hBrank) + rw [← Matrix.mulVecLin_apply, hlin, LinearMap.zero_apply, + Fin.signVariations_zero] + induction m generalizing r with + | zero => + have hrzero : r = 0 := by + have hrle : r ≤ 0 := hrank ▸ A.rank_le_width + exact Nat.eq_zero_of_le_zero hrle + rw [hrzero] at hrank ⊢ + exact hzero hrank c + | succ k ih => + by_cases hrzero : r = 0 + · rw [hrzero] at hrank ⊢ + exact hzero hrank c + · have hrpos : 0 < r := Nat.pos_of_ne_zero hrzero + have hrle : r ≤ k + 1 := by + rw [← hrank] + exact A.rank_le_width + by_cases hrfull : r = k + 1 + · rw [hrfull] at hA hrank ⊢ + have hkn : k + 1 ≤ n := hrank ▸ A.rank_le_height + have hAinj : Function.Injective A.mulVec := by + rw [Matrix.mulVec_injective_iff, + linearIndependent_iff_card_eq_finrank_span] + simpa only [Fintype.card_fin, Set.finrank] using + hrank.symm.trans (Matrix.rank_eq_finrank_span_cols A) + exact hA.signVariations_mulVec_le_card_sub_one hkn hAinj c + · have hrlt : r < k + 1 := lt_of_le_of_ne hrle hrfull + exact hA.signVariations_mulVec_le_rank_sub_one_of_induction + hrank hrlt hrpos ih c + +private lemma mul_mul_nonneg_of_cross_mul_nonneg + {a b c d : ℝ} (hac : 0 ≤ a * c) (hbd : 0 ≤ b * d) : + 0 ≤ (a * b) * (c * d) := by + calc + 0 ≤ (a * c) * (b * d) := mul_nonneg hac hbd + _ = (a * b) * (c * d) := by ring + +/-- Right multiplication by a totally nonnegative rectangular matrix preserves +the common weak sign of ordered minors of a fixed size. Cauchy--Binet expands +the product of two output minors as a double sum; sign consistency controls the +left-minor products and total nonnegativity controls the right-minor products. -/ +theorem Matrix.IsSignConsistentOrder.mul_of_right_isTotallyNonnegRect + {l n m r : ℕ} + {L : Matrix (Fin l) (Fin n) ℝ} + {A : Matrix (Fin n) (Fin m) ℝ} + (hL : L.IsSignConsistentOrder r) + (hA : A.IsTotallyNonnegRect) : + (L * A).IsSignConsistentOrder r := by + classical + intro rows rows' cols cols' hrows hrows' hcols hcols' + rw [Matrix.det_submatrix_mul_eq_sum_powersetCard L A rows cols, + Matrix.det_submatrix_mul_eq_sum_powersetCard L A rows' cols'] + rw [Finset.sum_mul] + apply Finset.sum_nonneg + intro s hs + rw [Finset.mul_sum] + apply Finset.sum_nonneg + intro t ht + let es : Fin r ↪o Fin n := + Set.powersetCard.ofFinEmbEquiv.symm s + let et : Fin r ↪o Fin n := + Set.powersetCard.ofFinEmbEquiv.symm t + have hsign : + 0 ≤ + (L.submatrix rows es).det * + (L.submatrix rows' et).det := + hL hrows hrows' es.strictMono et.strictMono + have hright : + 0 ≤ + (A.submatrix es cols).det * + (A.submatrix et cols').det := + mul_nonneg + (hA es.strictMono hcols) + (hA et.strictMono hcols') + exact mul_mul_nonneg_of_cross_mul_nonneg hsign hright + +/-- The weighted incidence matrix associated with a block map. -/ +def Matrix.weightedIncidence + {n q : ℕ} + (block : Fin n → Fin q) + (weight : Fin n → ℝ) : + Matrix (Fin n) (Fin q) ℝ := + fun j s => if block j = s then weight j else 0 + +@[simp] +theorem Matrix.weightedIncidence_apply + {n q : ℕ} + (block : Fin n → Fin q) + (weight : Fin n → ℝ) + (j : Fin n) + (s : Fin q) : + Matrix.weightedIncidence block weight j s = + if block j = s then weight j else 0 := + rfl + +/-- The minor of a monotone weighted incidence matrix is diagonal or singular. + +This is the elementary incidence-matrix step in Karlin's proof of Theorem V.1.4: +monotonicity forces every nonzero Leibniz term to use the identity permutation. +Thus no separate combinatorial model is needed for this bridge. -/ +theorem Matrix.det_submatrix_monotoneWeightedIncidence + {n q r : ℕ} + (block : Fin n → Fin q) + (hblock : Monotone block) + (weight : Fin n → ℝ) + {rows : Fin r → Fin n} + {cols : Fin r → Fin q} + (hrows : StrictMono rows) + (hcols : StrictMono cols) : + ((Matrix.weightedIncidence block weight).submatrix rows cols).det = + if ∀ i, block (rows i) = cols i then + ∏ i, weight (rows i) + else 0 := by + classical + let W := Matrix.weightedIncidence block weight + change (W.submatrix rows cols).det = + if ∀ i, block (rows i) = cols i then + ∏ i, weight (rows i) + else 0 + by_cases hdiag : ∀ i, block (rows i) = cols i + · rw [if_pos hdiag] + have hmatrix : + W.submatrix rows cols = + Matrix.diagonal (fun i => weight (rows i)) := by + ext i j + simp only [Matrix.submatrix_apply, W, + Matrix.weightedIncidence_apply] + rw [hdiag i] + by_cases hij : i = j + · subst j + simp + · have hc : cols i ≠ cols j := fun h => + hij (hcols.injective h) + simp [hc, hij] + rw [hmatrix, Matrix.det_diagonal] + · rw [if_neg hdiag, Matrix.det_apply'] + apply Finset.sum_eq_zero + intro sigma hsigma + by_cases hterm : ∀ i, block (rows (sigma i)) = cols i + · have hsigma_mono : StrictMono sigma := by + intro i j hij + by_contra hnot + have hle : sigma j ≤ sigma i := le_of_not_gt hnot + have hf : + block (rows (sigma j)) ≤ block (rows (sigma i)) := + (hblock.comp hrows.monotone) hle + rw [hterm j, hterm i] at hf + exact (not_le_of_gt (hcols hij)) hf + have hsigma_eq : ∀ i, sigma i = i := fun i => + le_antisymm (hsigma_mono.le_id i) (hsigma_mono.id_le i) + exfalso + apply hdiag + intro i + simpa only [hsigma_eq i] using hterm i + · simp only [not_forall] at hterm + obtain ⟨i, hi⟩ := hterm + have hprod : + (∏ j, (W.submatrix rows cols) (sigma j) j) = 0 := by + apply Finset.prod_eq_zero (Finset.mem_univ i) + simp only [Matrix.submatrix_apply, W, + Matrix.weightedIncidence_apply] + rw [if_neg hi] + rw [hprod, mul_zero] + +/-- A monotone weighted incidence matrix is totally nonnegative when its weights are +nonnegative. -/ +theorem Matrix.isTotallyNonnegRect_monotoneWeightedIncidence + {n q : ℕ} + (block : Fin n → Fin q) + (hblock : Monotone block) + (weight : Fin n → ℝ) + (hweight : ∀ j, 0 ≤ weight j) : + Matrix.IsTotallyNonnegRect + (Matrix.weightedIncidence block weight) := by + intro r rows cols hrows hcols + rw [Matrix.det_submatrix_monotoneWeightedIncidence + block hblock weight hrows hcols] + split_ifs + · exact Finset.prod_nonneg fun i _ => hweight (rows i) + · exact le_rfl + +/-- Right multiplication by a weighted incidence matrix forms weighted block sums. -/ +theorem Matrix.mul_weightedIncidence_apply + {l n q : ℕ} + (L : Matrix (Fin l) (Fin n) ℝ) + (block : Fin n → Fin q) + (weight : Fin n → ℝ) + (i : Fin l) + (s : Fin q) : + (L * Matrix.weightedIncidence block weight) i s = + ∑ j with block j = s, L i j * weight j := by + rw [Matrix.mul_apply, Finset.sum_filter] + simp only [Matrix.weightedIncidence_apply, mul_ite, mul_zero] + +/-- A weighted incidence matrix sends block coefficients to their weighted +pullback along the block map. -/ +@[simp] +theorem Matrix.weightedIncidence_mulVec + {n q : ℕ} + (block : Fin n → Fin q) + (weight : Fin n → ℝ) + (sign : Fin q → ℝ) : + (Matrix.weightedIncidence block weight).mulVec sign = + fun j => weight j * sign (block j) := by + ext j + simp [Matrix.mulVec, dotProduct] + +/-- Multiplying an aggregated matrix by block coefficients reconstructs the +corresponding coefficient vector before multiplication by the original matrix. -/ +theorem Matrix.mul_weightedIncidence_mulVec + {l n q : ℕ} + (L : Matrix (Fin l) (Fin n) ℝ) + (block : Fin n → Fin q) + (weight : Fin n → ℝ) + (sign : Fin q → ℝ) : + (L * Matrix.weightedIncidence block weight).mulVec sign = + L.mulVec (fun j => weight j * sign (block j)) := by + rw [← Matrix.mulVec_mulVec sign L + (Matrix.weightedIncidence block weight), + Matrix.weightedIncidence_mulVec] + +/-- Aggregating consecutive columns with nonnegative weights preserves sign +consistency of every fixed order. -/ +theorem Matrix.IsSignConsistentOrder.mul_weightedIncidence + {l n q r : ℕ} + {L : Matrix (Fin l) (Fin n) ℝ} + (hL : L.IsSignConsistentOrder r) + (block : Fin n → Fin q) + (hblock : Monotone block) + (weight : Fin n → ℝ) + (hweight : ∀ j, 0 ≤ weight j) : + (L * Matrix.weightedIncidence block weight).IsSignConsistentOrder r := + hL.mul_of_right_isTotallyNonnegRect + (Matrix.isTotallyNonnegRect_monotoneWeightedIncidence + block hblock weight hweight) + +/-- Karlin's V.1.4 inequality from explicit sign-block decomposition data. + +The only remaining finite combinatorial step for the general theorem is to +construct `Fin.SignBlockDecomposition c`; all matrix and rank arguments are +discharged here. -/ +theorem Matrix.IsSignRegular.signVariations_mulVec_le_of_signBlockDecomposition + {l n : ℕ} + {A : Matrix (Fin l) (Fin n) ℝ} + (hA : A.IsSignRegular) + (c : Fin n → ℝ) + (d : Fin.SignBlockDecomposition c) : + Fin.signVariations (A.mulVec c) ≤ Fin.signVariations c := by + let B := + A * Matrix.weightedIncidence d.block d.weight + have hBsign : B.IsSignConsistentOrder B.rank := by + simpa only [B] using + (hA B.rank).mul_weightedIncidence + d.block d.block_mono d.weight d.weight_nonneg + have hbound : + Fin.signVariations (B.mulVec d.coeff) ≤ B.rank - 1 := + hBsign.signVariations_mulVec_le_rank_sub_one rfl d.coeff + have hmul : B.mulVec d.coeff = A.mulVec c := by + calc + B.mulVec d.coeff = + A.mulVec (fun j => d.weight j * d.coeff (d.block j)) := by + simpa only [B] using + Matrix.mul_weightedIncidence_mulVec + A d.block d.weight d.coeff + _ = A.mulVec c := + congrArg A.mulVec (funext fun j => d.reconstruct j) + calc + Fin.signVariations (A.mulVec c) = + Fin.signVariations (B.mulVec d.coeff) := + congrArg Fin.signVariations hmul.symm + _ ≤ B.rank - 1 := hbound + _ ≤ d.numBlocks - 1 := + (Nat.sub_le_sub_right B.rank_le_width) 1 + _ = Fin.signVariations c := d.numBlocks_sub_one + +/-- Karlin's variation-diminishing theorem for sign-regular matrices. -/ +theorem Matrix.IsSignRegular.signVariations_mulVec_le + {l n : ℕ} + {A : Matrix (Fin l) (Fin n) ℝ} + (hA : A.IsSignRegular) (c : Fin n → ℝ) : + Fin.signVariations (A.mulVec c) ≤ Fin.signVariations c := + hA.signVariations_mulVec_le_of_signBlockDecomposition + c (Fin.signBlockDecomposition c) + +/-- Karlin's forward variation-diminishing theorem for finite rectangular +totally nonnegative matrices. -/ +theorem Matrix.IsTotallyNonnegRect.signVariations_mulVec_le + {l n : ℕ} + {A : Matrix (Fin l) (Fin n) ℝ} + (hA : A.IsTotallyNonnegRect) (c : Fin n → ℝ) : + Fin.signVariations (A.mulVec c) ≤ Fin.signVariations c := + hA.isSignRegular.signVariations_mulVec_le c + +/-- A surjective totally nonnegative matrix forces a nodal kernel vector to +have at least the row count minus one sign variations, up to the two endpoint +variations lost under perturbation. -/ +theorem Matrix.IsTotallyNonnegRect.card_sub_one_le_signVariations_add_two_of_surjective_of_nodal + {rows n : ℕ} {A : Matrix (Fin rows) (Fin (n + 2)) ℝ} + (hA : A.IsTotallyNonnegRect) + (hsurj : Function.Surjective A.mulVec) + {x : Fin (n + 2) → ℝ} + (hker : A.mulVec x = 0) + (hnodal : ∀ i : Fin n, x i.succ.castSucc = 0 → + x i.castSucc.castSucc * x i.succ.succ < 0) : + rows - 1 ≤ Fin.signVariations x + 2 := by + cases rows with + | zero => simp + | succ k => + let alt : Fin (k + 1) → ℝ := fun i => (-1 : ℝ) ^ (i : ℕ) + obtain ⟨z, hz⟩ := hsurj alt + let f : ℝ → Fin (n + 2) → ℝ := fun t => x + t • z + have hf : + Tendsto f (nhdsWithin (0 : ℝ) (Set.Ioi 0)) (𝓝 x) := by + have hfull : + Tendsto f (𝓝 (0 : ℝ)) (𝓝 (x + (0 : ℝ) • z)) := + tendsto_const_nhds.add (tendsto_id.smul_const z) + have hle : + nhdsWithin (0 : ℝ) (Set.Ioi 0) ≤ 𝓝 (0 : ℝ) := by + simp only [nhdsWithin] + exact inf_le_left + have hrestricted := hfull.mono_left hle + simpa only [zero_smul, add_zero] using hrestricted + have hbound := + Fin.eventually_signVariations_le_add_two_of_tendsto_of_interior_nodal + hf hnodal + have hpos : + ∀ᶠ t in nhdsWithin (0 : ℝ) (Set.Ioi 0), 0 < t := + self_mem_nhdsWithin + obtain ⟨t, htbound, ht⟩ := (hbound.and hpos).exists + have himage : + A.mulVec (f t) = + fun i : Fin (k + 1) => (-1 : ℝ) ^ (i : ℕ) * t := by + rw [show f t = x + t • z by rfl, Matrix.mulVec_add, + Matrix.mulVec_smul, hker, hz] + funext i + simp only [Pi.smul_apply, zero_add, alt, smul_eq_mul, mul_comm] + have halt : Fin.StrictlyAlternates (A.mulVec (f t)) := by + rw [himage] + exact Fin.strictlyAlternates_alternating k ht + have hlower : k ≤ Fin.signVariations (A.mulVec (f t)) := + halt.le_signVariations_of_strictMono strictMono_id + simpa using + hlower.trans ((hA.signVariations_mulVec_le (f t)).trans htbound) + +/-- Cardinality-equality wrapper for the surjective totally nonnegative nodal +kernel bound. -/ +theorem Matrix.IsTotallyNonnegRect.card_sub_one_le_signVariations_add_two_of_surjective_of_card_eq + {rows cols n : ℕ} {A : Matrix (Fin rows) (Fin cols) ℝ} + (hA : A.IsTotallyNonnegRect) + (hcols : cols = n + 2) + (hsurj : Function.Surjective A.mulVec) + {x : Fin cols → ℝ} + (hker : A.mulVec x = 0) + (hnodal : ∀ i : Fin n, + x (Fin.cast hcols.symm i.succ.castSucc) = 0 → + x (Fin.cast hcols.symm i.castSucc.castSucc) * + x (Fin.cast hcols.symm i.succ.succ) < 0) : + rows - 1 ≤ Fin.signVariations x + 2 := by + subst cols + exact hA.card_sub_one_le_signVariations_add_two_of_surjective_of_nodal + hsurj hker (by simpa using hnodal) diff --git a/RealRooted/Mathlib/LinearAlgebra/Matrix/SignRegularStrictification.lean b/RealRooted/Mathlib/LinearAlgebra/Matrix/SignRegularStrictification.lean new file mode 100644 index 000000000..9367984e7 --- /dev/null +++ b/RealRooted/Mathlib/LinearAlgebra/Matrix/SignRegularStrictification.lean @@ -0,0 +1,102 @@ +import RealRooted.Mathlib.LinearAlgebra.Matrix.Determinant.CauchyBinet +import RealRooted.Mathlib.LinearAlgebra.Matrix.Gaussian +import RealRooted.Mathlib.LinearAlgebra.Matrix.SignRegular + +/-! +# Strictifying sign-consistent matrices + +This file formalizes Karlin, *Total Positivity*, Vol. I, Chapter V, Section 1, +Proposition 1.2. A positive-minor left factor strictifies a full-column-rank +sign-consistent matrix. Karlin applies this with a Gaussian matrix and then +lets the Gaussian parameter tend to infinity. +-/ + +public section + +open Filter +open scoped Topology + +namespace Matrix + +/-- Positive ordered minors in a left factor strictify a full-column-rank +sign-consistent right factor. -/ +theorem IsSignConsistentOrder.isStrictlySignConsistentOrder_mul_of_posMinors + {S : Type*} [Field S] [LinearOrder S] [IsStrictOrderedRing S] + {l n m q : ℕ} {L : Matrix (Fin l) (Fin n) S} + {A : Matrix (Fin n) (Fin m) S} + (hA : A.IsSignConsistentOrder q) + (hAinj : Function.Injective A.mulVec) + (hL : ∀ ⦃rows : Fin q → Fin l⦄ ⦃cols : Fin q → Fin n⦄, + StrictMono rows → StrictMono cols → + 0 < (L.submatrix rows cols).det) : + (L * A).IsStrictlySignConsistentOrder q := by + classical + intro rows rows' cols cols' hrows hrows' hcols hcols' + obtain ⟨rows₀, hrows₀, href_ne⟩ := + exists_ordered_minor_ne_zero_of_mulVec_injective A hAinj cols hcols + rcases lt_or_gt_of_ne href_ne with href_neg | href_pos + · have hneg : ∀ ⦃r : Fin q → Fin l⦄ ⦃c : Fin q → Fin m⦄, + StrictMono r → StrictMono c → + ((L * A).submatrix r c).det < 0 := by + intro r c hr hc + rw [det_submatrix_mul_eq_sum_powersetCard] + apply Finset.sum_neg' + · intro s _ + exact mul_nonpos_of_nonneg_of_nonpos + (hL hr (Set.powersetCard.ofFinEmbEquiv.symm s).strictMono).le + (hA.minor_nonpos_of_neg hrows₀ hcols href_neg + (Set.powersetCard.ofFinEmbEquiv.symm s).strictMono hc) + · obtain ⟨r₁, hr₁, href₁_ne⟩ := + exists_ordered_minor_ne_zero_of_mulVec_injective A hAinj c hc + have href₁_neg : (A.submatrix r₁ c).det < 0 := + lt_of_le_of_ne + (hA.minor_nonpos_of_neg hrows₀ hcols href_neg hr₁ hc) href₁_ne + let e := OrderEmbedding.ofStrictMono r₁ hr₁ + refine ⟨Set.powersetCard.ofFinEmbEquiv e, Finset.mem_univ _, ?_⟩ + simpa [e] using mul_neg_of_pos_of_neg (hL hr hr₁) href₁_neg + exact mul_pos_of_neg_of_neg (hneg hrows hcols) (hneg hrows' hcols') + · have hpos : ∀ ⦃r : Fin q → Fin l⦄ ⦃c : Fin q → Fin m⦄, + StrictMono r → StrictMono c → + 0 < ((L * A).submatrix r c).det := by + intro r c hr hc + rw [det_submatrix_mul_eq_sum_powersetCard] + apply Finset.sum_pos' + · intro s _ + exact mul_nonneg + (hL hr (Set.powersetCard.ofFinEmbEquiv.symm s).strictMono).le + (hA.minor_nonneg_of_pos hrows₀ hcols href_pos + (Set.powersetCard.ofFinEmbEquiv.symm s).strictMono hc) + · obtain ⟨r₁, hr₁, href₁_ne⟩ := + exists_ordered_minor_ne_zero_of_mulVec_injective A hAinj c hc + have href₁_pos : 0 < (A.submatrix r₁ c).det := + lt_of_le_of_ne + (hA.minor_nonneg_of_pos hrows₀ hcols href_pos hr₁ hc) href₁_ne.symm + let e := OrderEmbedding.ofStrictMono r₁ hr₁ + refine ⟨Set.powersetCard.ofFinEmbEquiv e, Finset.mem_univ _, ?_⟩ + simpa [e] using mul_pos (hL hr hr₁) href₁_pos + exact mul_pos (hpos hrows hcols) (hpos hrows' hcols') + +/-- Karlin's Gaussian left multiplier strictifies a full-column-rank +sign-consistent matrix. -/ +theorem IsSignConsistentOrder.isStrictlySignConsistentOrder_gaussianMatrix_mul + {n m q : ℕ} {A : Matrix (Fin n) (Fin m) ℝ} + (hA : A.IsSignConsistentOrder q) (hAinj : Function.Injective A.mulVec) + {a : ℝ} (ha : 0 < a) : + (gaussianMatrix n a * A).IsStrictlySignConsistentOrder q := by + apply hA.isStrictlySignConsistentOrder_mul_of_posMinors hAinj + intro rows cols hrows hcols + exact det_gaussianMatrix_submatrix_pos a rows cols ha hrows hcols + +/-- Gaussian left multiplication converges entrywise to the original matrix. -/ +theorem tendsto_gaussianMatrix_mul_atTop {n m : ℕ} + (A : Matrix (Fin n) (Fin m) ℝ) : + Tendsto (fun a => gaussianMatrix n a * A) atTop (𝓝 A) := by + have hmul : Continuous (fun M : Matrix (Fin n) (Fin n) ℝ => M * A) := + continuous_id.matrix_mul continuous_const + convert hmul.continuousAt.tendsto.comp + (tendsto_gaussianMatrix_atTop n) using 1 + · funext a + rfl + · simp + +end Matrix diff --git a/RealRooted/Mathlib/LinearAlgebra/Matrix/SignRegularVariation.lean b/RealRooted/Mathlib/LinearAlgebra/Matrix/SignRegularVariation.lean new file mode 100644 index 000000000..e2f8e23e0 --- /dev/null +++ b/RealRooted/Mathlib/LinearAlgebra/Matrix/SignRegularVariation.lean @@ -0,0 +1,39 @@ +import RealRooted.Mathlib.LinearAlgebra.Matrix.SignRegularStrictification +import RealRooted.Mathlib.LinearAlgebra.Matrix.SignVariationTopology +import RealRooted.Mathlib.LinearAlgebra.Matrix.VariationDiminishing + +/-! +# Variation bounds for sign-consistent matrices + +This file proves the full-column-rank case of the variation bound in Karlin, +*Total Positivity*, Volume I, Chapter V, Section 1, Theorem 1.3. Gaussian +strictification reduces the result to the strict maximal-minor theorem, and +lower semicontinuity of sign variations passes the bound to the limit. +-/ + +open Filter + +/-- A full-column-rank sign-consistent matrix has at most `q - 1` sign +variations in every vector in its range. -/ +theorem Matrix.IsSignConsistentOrder.signVariations_mulVec_le_card_sub_one + {m q : ℕ} {A : Matrix (Fin m) (Fin q) ℝ} + (hA : A.IsSignConsistentOrder q) + (hqm : q ≤ m) + (hAinj : Function.Injective A.mulVec) + (x : Fin q → ℝ) : + Fin.signVariations (A.mulVec x) ≤ q - 1 := by + refine Fin.signVariations_le_of_tendsto + (l := (atTop : Filter ℝ)) + (f := fun a => (Matrix.gaussianMatrix m a * A).mulVec x) ?_ ?_ + · have hcont : Continuous + (fun M : Matrix (Fin m) (Fin q) ℝ => M.mulVec x) := + continuous_id.matrix_mulVec continuous_const + exact hcont.continuousAt.tendsto.comp + (Matrix.tendsto_gaussianMatrix_mul_atTop A) + · filter_upwards [Filter.eventually_gt_atTop (0 : ℝ)] with a ha + have hstrict : + (Matrix.gaussianMatrix m a * A).IsStrictlySignConsistentOrder q := + hA.isStrictlySignConsistentOrder_gaussianMatrix_mul hAinj ha + exact Matrix.signVariations_mulVec_le_card_sub_one_of_strictMaximalMinors + hqm (fun ⦃rows rows'⦄ hrows hrows' => + hstrict hrows hrows' strictMono_id strictMono_id) x diff --git a/RealRooted/Mathlib/LinearAlgebra/Matrix/SignVariation.lean b/RealRooted/Mathlib/LinearAlgebra/Matrix/SignVariation.lean index e1c483eb7..3542ae722 100644 --- a/RealRooted/Mathlib/LinearAlgebra/Matrix/SignVariation.lean +++ b/RealRooted/Mathlib/LinearAlgebra/Matrix/SignVariation.lean @@ -4,6 +4,9 @@ public import Mathlib.Algebra.Polynomial.RuleOfSigns public import Mathlib.Data.List.ChainOfFn public import Mathlib.Data.List.NodupEquivFin public import Mathlib.Tactic +public import RealRooted.Mathlib.Data.List.Destutter +public import RealRooted.Mathlib.Data.List.Basic +public import RealRooted.Mathlib.Data.List.OfFn /-! # Sign variations of finite vectors @@ -356,6 +359,237 @@ lemma signVariations_append_nonpos_le_succ (l₁ l₂ : List ℝ) end List +/-- Taking the sign of a sign is the identity. -/ +@[simp] +theorem SignType.sign_sign (s : SignType) : SignType.sign s = s := by + fin_cases s <;> rfl + +private lemma add_one_le_pred_add_two (n : ℕ) : + n + 1 ≤ n - 1 + 1 + 1 := by + cases n <;> simp + +/-- Prepending one sign increases the number of sign variations by at most one. -/ +theorem List.signVariations_cons_le_succ (a : SignType) (l : List SignType) : + (a :: l).signVariations ≤ l.signVariations + 1 := by + have h := List.length_destutter_cons_ne_le_succ a + ((l.map SignType.sign).filter (· ≠ 0)) + by_cases ha : a = 0 + · simp [List.signVariations, ha] + · simpa [List.signVariations, ha] using h.trans (add_one_le_pred_add_two _) + +/-- Appending one sign increases the number of sign variations by at most one. -/ +theorem List.signVariations_append_singleton_signType_le_succ + (l : List SignType) (a : SignType) : + (l ++ [a]).signVariations ≤ l.signVariations + 1 := by + have h := List.length_destutter_append_singleton_ne_le_succ + ((l.map SignType.sign).filter (· ≠ 0)) a + by_cases ha : a = 0 + · simp [List.signVariations, ha] + · simpa [List.signVariations, ha] using h.trans (add_one_le_pred_add_two _) + +/-- Inserting any sign between opposite nonzero signs does not change sign variations. + +This is the finite local step used for nodal interior zeros in Karlin's perturbation +argument: after zero signs are removed, the inserted sign either disappears or duplicates +one of its two neighbors. -/ +theorem List.signVariations_insert_between_opposite + (l₁ l₂ : List SignType) (a b z : SignType) + (ha : a ≠ 0) (hb : b ≠ 0) (hab : a ≠ b) : + (l₁ ++ [a, z, b] ++ l₂).signVariations = + (l₁ ++ [a, b] ++ l₂).signVariations := by + fin_cases a <;> fin_cases b <;> fin_cases z <;> + simp_all [List.signVariations, List.destutter_append_cons_self_ne, + List.destutter_append_cons_cons_self_ne] + +namespace List + +private theorem filter_map_sign_filter_ne_zero (l : List SignType) : + ((l.filter (· ≠ 0)).map SignType.sign).filter (· ≠ 0) = + (l.map SignType.sign).filter (· ≠ 0) := by + have hsign : (SignType.sign : SignType → SignType) = id := funext SignType.sign_sign + simp [hsign] + +/-- Filtering zero signs does not change sign variations. -/ +theorem signVariations_filter_ne_zero (l : List SignType) : + (l.filter (· ≠ 0)).signVariations = l.signVariations := by + simp only [List.signVariations, filter_map_sign_filter_ne_zero] + +/-- One insertion at an interior nodal position. + +This inductive relation is structural data recording an explicit list operation, +not an unproved mathematical assertion packaged as a proposition. -/ +inductive NodalInsertion : List SignType → List SignType → Prop + | insert (l₁ l₂ : List SignType) (a b z : SignType) + (ha : a ≠ 0) (hb : b ≠ 0) (hab : a ≠ b) : + NodalInsertion (l₁ ++ [a, b] ++ l₂) (l₁ ++ [a, z, b] ++ l₂) + +/-- Adding unchanged list context preserves one nodal insertion. -/ +protected theorem NodalInsertion.append_context + {l l' : List SignType} (h : NodalInsertion l l') + (pre post : List SignType) : + NodalInsertion (pre ++ l ++ post) (pre ++ l' ++ post) := by + cases h with + | insert l₁ l₂ a b z ha hb hab => + simpa only [append_assoc] using + NodalInsertion.insert (pre ++ l₁) (l₂ ++ post) a b z ha hb hab + +/-- Erasing an entry between opposite nonzero neighbors is one nodal insertion in reverse. -/ +protected theorem NodalInsertion.eraseIdx_succ + (l : List SignType) (i : ℕ) (hi : i + 2 < l.length) + (ha : l[i] ≠ 0) (hb : l[i + 2] ≠ 0) + (hab : l[i] ≠ l[i + 2]) : + NodalInsertion (l.eraseIdx (i + 1)) l := by + induction l generalizing i with + | nil => simp at hi + | cons x l ih => + cases i with + | zero => + cases l with + | nil => simp at hi + | cons z l => + cases l with + | nil => simp at hi + | cons b l => + exact NodalInsertion.insert [] l x b z + (by simpa using ha) (by simpa using hb) + (by simpa using hab) + | succ i => + have h := ih i + (by + simp only [length_cons] at hi + lia) + (by simpa [Nat.succ_eq_add_one] using ha) + (by simpa [Nat.succ_eq_add_one] using hb) + (by simpa [Nat.succ_eq_add_one] using hab) + simpa [Nat.succ_eq_add_one] using h.append_context [x] [] + +/-- Erasing an entry between opposite nonzero neighbors inside a middle block +is one nodal insertion in reverse, with unchanged surrounding context. -/ +protected theorem NodalInsertion.eraseIdx_append_middle + (pre middle post : List SignType) (i : ℕ) + (hi : i + 2 < middle.length) + (ha : middle[i] ≠ 0) (hb : middle[i + 2] ≠ 0) + (hab : middle[i] ≠ middle[i + 2]) : + NodalInsertion + ((pre ++ middle ++ post).eraseIdx (pre.length + (i + 1))) + (pre ++ middle ++ post) := by + have hi' : i + 1 < middle.length := by lia + rw [List.eraseIdx_append_middle pre middle post (i + 1) hi'] + exact + (NodalInsertion.eraseIdx_succ middle i hi ha hb hab).append_context + pre post + +/-- Deleting the first element of a middle block is a nodal insertion when +its left neighbor is a retained singleton and its right neighbor is the +second middle entry. -/ +protected theorem NodalInsertion.eraseIdx_first_middle + (a : SignType) (middle post : List SignType) + (hmiddle : 1 < middle.length) + (ha : a ≠ 0) + (hb : middle[1] ≠ 0) + (hab : a ≠ middle[1]) : + NodalInsertion + ([a] ++ middle.eraseIdx 0 ++ post) + ([a] ++ middle ++ post) := by + rw [← List.eraseIdx_append_middle [a] middle post 0 (by lia)] + change NodalInsertion + (([a] ++ middle ++ post).eraseIdx 1) + ([a] ++ middle ++ post) + simpa only [List.nil_append, List.length_nil, zero_add, + List.append_assoc] using + NodalInsertion.eraseIdx_append_middle + [] ([a] ++ middle) post 0 + (by + simp only [List.length_append, List.length_singleton] + lia) + (by simpa using ha) + (by simpa using hb) + (by simpa using hab) + +/-- Deleting the final entry of a middle block is one nodal insertion in +reverse when its preceding entry and a retained singleton endpoint have +opposite nonzero signs. -/ +protected theorem NodalInsertion.eraseIdx_last_append_singleton + (pre middle : List SignType) (b : SignType) (i : ℕ) + (hlen : middle.length = i + 2) + (ha : middle[i] ≠ 0) (hb : b ≠ 0) + (hab : middle[i] ≠ b) : + NodalInsertion + (pre ++ middle.eraseIdx (i + 1) ++ [b]) + (pre ++ middle ++ [b]) := by + have hi : i < middle.length := by simp [hlen] + have hiErase : i + 1 < middle.length := by simp [hlen] + have hiLocal : i + 2 < (middle ++ [b]).length := by simp [hlen] + have hleft : (middle ++ [b])[i] = middle[i] := + List.getElem_append_left hi + have hright : (middle ++ [b])[i + 2] = b := by + simp [List.getElem_append_right, hlen] + rw [← List.eraseIdx_append_middle + pre middle [b] (i + 1) hiErase] + simpa only [List.append_nil, List.append_assoc] using + NodalInsertion.eraseIdx_append_middle + pre (middle ++ [b]) [] i hiLocal + (by rw [hleft]; exact ha) + (by rw [hright]; exact hb) + (by rw [hleft, hright]; exact hab) + +/-- Adding unchanged list context preserves repeated nodal insertions. -/ +protected theorem NodalInsertion.reflTransGen_append_context + {l l' : List SignType} + (h : Relation.ReflTransGen NodalInsertion l l') + (pre post : List SignType) : + Relation.ReflTransGen NodalInsertion + (pre ++ l ++ post) (pre ++ l' ++ post) := by + induction h with + | refl => exact .refl + | tail h huv ih => + exact ih.tail (huv.append_context pre post) + +/-- Repeated insertions at interior nodal positions preserve sign variations. -/ +theorem signVariations_eq_of_nodalInsertions + {l l' : List SignType} + (h : Relation.ReflTransGen NodalInsertion l l') : + l'.signVariations = l.signVariations := by + induction h with + | refl => rfl + | tail h huv ih => + cases huv with + | insert l₁ l₂ a b z ha hb hab => + calc + (l₁ ++ [a, z, b] ++ l₂).signVariations = + (l₁ ++ [a, b] ++ l₂).signVariations := + signVariations_insert_between_opposite l₁ l₂ a b z ha hb hab + _ = l.signVariations := ih + +/-- Repeated interior nodal insertions and two arbitrary endpoint insertions increase sign +variations by at most two. -/ +theorem signVariations_endpoints_le_add_two_of_nodalInsertions + {l l' : List SignType} + (h : Relation.ReflTransGen NodalInsertion l l') + (a b : SignType) : + ((a :: l') ++ [b]).signVariations ≤ l.signVariations + 2 := by + calc + ((a :: l') ++ [b]).signVariations ≤ + (l' ++ [b]).signVariations + 1 := by + simpa only [List.cons_append] using + signVariations_cons_le_succ a (l' ++ [b]) + _ ≤ (l'.signVariations + 1) + 1 := + Nat.add_le_add_right + (signVariations_append_singleton_signType_le_succ l' b) 1 + _ = l.signVariations + 2 := by + rw [signVariations_eq_of_nodalInsertions h] + +end List + +/-- A negative product of real numbers has nonzero, opposite signs. -/ +theorem SignType.sign_ne_zero_and_ne_of_mul_neg + {a b : ℝ} (h : a * b < 0) : + SignType.sign a ≠ 0 ∧ SignType.sign b ≠ 0 ∧ + SignType.sign a ≠ SignType.sign b := by + rcases (mul_neg_iff.mp h) with ⟨ha, hb⟩ | ⟨ha, hb⟩ + · simp [SignType.sign, ha, hb, not_lt_of_ge hb.le] + · simp [SignType.sign, ha, hb, not_lt_of_ge ha.le] + namespace Fin /-- The number of sign changes in a finite vector, in index order and ignoring @@ -364,6 +598,557 @@ def signVariations {R : Type*} [Zero R] [LinearOrder R] {n : ℕ} (x : Fin n → R) : ℕ := (List.ofFn x).signVariations +/-- A finite real vector has the same variation count as its explicit sign list. -/ +theorem signVariations_eq_signList {n : ℕ} (x : Fin n → ℝ) : + Fin.signVariations x = + (List.ofFn (SignType.sign ∘ x)).signVariations := by + simp [Fin.signVariations, List.signVariations, Function.comp_def] + +/-- Filtering the explicit sign list computes finite-vector sign variations. -/ +theorem filtered_signList_signVariations {n : ℕ} (x : Fin n → ℝ) : + ((List.ofFn (SignType.sign ∘ x)).filter (· ≠ 0)).signVariations = + Fin.signVariations x := by + simpa only [List.signVariations_filter_ne_zero] using + (Fin.signVariations_eq_signList x).symm + +/-- Perturbed signs at all interior coordinates and at the original nonzero +endpoints. + +Interior zeros are retained because the coordinate-removal induction constructs +them by nodal insertions. A zero original endpoint is omitted and handled by the +final two-endpoint variation bound. -/ +def nodalPerturbationCoreSigns + {n : ℕ} (x y : Fin (n + 2) → ℝ) : List SignType := + (if x 0 = 0 then [] else [SignType.sign (y 0)]) ++ + List.ofFn + (fun i : Fin n => SignType.sign (y i.succ.castSucc)) ++ + (if x (Fin.last (n + 1)) = 0 then [] + else [SignType.sign (y (Fin.last (n + 1)))]) + +/-- At the splice created by deleting a nodal zero, the new center is nonzero. -/ +theorem succAbove_center_ne_zero_of_mul_neg + {n : ℕ} (x : Fin (n + 3) → ℝ) (i : Fin n) + (h : x i.castSucc.castSucc.castSucc * x i.succ.succ.castSucc < 0) : + x ((i.succ.castSucc.castSucc).succAbove i.succ.castSucc) ≠ 0 := by + rw [Fin.succAbove_center_eq_right] + exact right_ne_zero_of_mul (ne_of_lt h) + +/-- If the omitted nodal zero was the old right neighbor, the new center is nonzero. -/ +theorem succAbove_center_ne_zero_of_omit_right_mul_neg + {n : ℕ} (x : Fin (n + 3) → ℝ) (i : Fin n) + (h : x i.succ.castSucc.castSucc * x i.succ.succ.succ < 0) : + x ((i.succ.succ.castSucc).succAbove i.succ.castSucc) ≠ 0 := by + rw [Fin.succAbove_center_eq_left] + exact left_ne_zero_of_mul (ne_of_lt h) + +/-- Deleting an interior nodal zero preserves strict interior nodality. -/ +theorem interiorNodal_succAbove + {n : ℕ} (x : Fin (n + 3) → ℝ) (k : Fin (n + 1)) + (hk : x k.succ.castSucc = 0) + (hnodal : ∀ j : Fin (n + 1), x j.succ.castSucc = 0 → + x j.castSucc.castSucc * x j.succ.succ < 0) : + ∀ i : Fin n, + x (k.succ.castSucc.succAbove i.succ.castSucc) = 0 → + x (k.succ.castSucc.succAbove i.castSucc.castSucc) * + x (k.succ.castSucc.succAbove i.succ.succ) < 0 := by + intro i hi + by_cases hki : (k : ℕ) < (i : ℕ) + · have hp : k.succ.castSucc ≤ i.castSucc.castSucc.castSucc := by + change (k : ℕ) + 1 ≤ (i : ℕ) + lia + rcases Fin.succAbove_triple_eq_succ_of_le_left k.succ.castSucc i hp with + ⟨hleft, hcenter, hright⟩ + rw [hcenter] at hi + rw [hleft, hright] + simpa using hnodal i.succ (by simpa using hi) + · by_cases hik : (i : ℕ) < (k : ℕ) + · by_cases hnext : (k : ℕ) = (i : ℕ) + 1 + · have hkeq : k = i.succ := by + apply Fin.ext + exact hnext + subst k + have hn := hnodal i.succ (by simpa using hk) + have hne := Fin.succAbove_center_ne_zero_of_omit_right_mul_neg x i + (by simpa using hn) + exact (hne (by simpa using hi)).elim + · have hp : i.succ.succ.castSucc < k.succ.castSucc := by + change (i : ℕ) + 2 < (k : ℕ) + 1 + lia + rcases Fin.succAbove_triple_eq_castSucc_of_right_lt k.succ.castSucc i hp with + ⟨hleft, hcenter, hright⟩ + rw [hcenter] at hi + rw [hleft, hright] + simpa using hnodal i.castSucc (by simpa using hi) + · have hkeq : k = i.castSucc := by + apply Fin.ext + change (k : ℕ) = (i : ℕ) + lia + subst k + have hn := hnodal i.castSucc (by simpa using hk) + have hne := Fin.succAbove_center_ne_zero_of_mul_neg x i + (by simpa using hn) + exact (hne (by simpa using hi)).elim + + +/-- Remove one interior zero, apply the shorter nodal-insertion chain, and reinsert it. + +This is the finite induction step in the endpoint-perturbation route used in Karlin's +Chapter 8, Section 3 argument. +-/ +theorem nodalInsertions_coreSigns_remove + {n : ℕ} + (ih : + ∀ {u v : Fin (n + 2) → ℝ}, + (∀ i, u i ≠ 0 → + SignType.sign (v i) = SignType.sign (u i)) → + (∀ i : Fin n, u i.succ.castSucc = 0 → + u i.castSucc.castSucc * u i.succ.succ < 0) → + Relation.ReflTransGen List.NodalInsertion + ((List.ofFn (SignType.sign ∘ u)).filter (· ≠ 0)) + (Fin.nodalPerturbationCoreSigns u v)) + {x y : Fin (n + 3) → ℝ} + (hsign : ∀ i, x i ≠ 0 → + SignType.sign (y i) = SignType.sign (x i)) + (hnodal : ∀ i : Fin (n + 1), x i.succ.castSucc = 0 → + x i.castSucc.castSucc * x i.succ.succ < 0) + (k : Fin (n + 1)) + (hk : x k.succ.castSucc = 0) : + Relation.ReflTransGen List.NodalInsertion + ((List.ofFn (SignType.sign ∘ x)).filter (· ≠ 0)) + (Fin.nodalPerturbationCoreSigns x y) := by + let p : Fin (n + 3) := k.succ.castSucc + let x' : Fin (n + 2) → ℝ := fun i => x (p.succAbove i) + let y' : Fin (n + 2) → ℝ := fun i => y (p.succAbove i) + have hsign' : + ∀ i, x' i ≠ 0 → + SignType.sign (y' i) = SignType.sign (x' i) := by + intro i hi + simpa only [x', y'] using + hsign (p.succAbove i) (by simpa only [x'] using hi) + have hnodal' : + ∀ i : Fin n, x' i.succ.castSucc = 0 → + x' i.castSucc.castSucc * x' i.succ.succ < 0 := by + simpa only [x', p] using + Fin.interiorNodal_succAbove x k hk hnodal + have hrec : + Relation.ReflTransGen List.NodalInsertion + ((List.ofFn (SignType.sign ∘ x')).filter (· ≠ 0)) + (Fin.nodalPerturbationCoreSigns x' y') := + ih hsign' hnodal' + have hofFn : + List.ofFn (fun i => SignType.sign (x' i)) = + (List.ofFn (fun i => SignType.sign (x i))).eraseIdx p := by + simpa only [x', p] using + List.ofFn_succAbove_eq_eraseIdx + (fun i => SignType.sign (x i)) p + have hlenSource : + (p : ℕ) < + (List.ofFn (fun i => SignType.sign (x i))).length := by + simpa only [List.length_ofFn] using p.isLt + have hvalueSource : + (List.ofFn (fun i => SignType.sign (x i)))[(p : ℕ)] = 0 := by + rw [List.getElem_ofFn hlenSource] + change SignType.sign (x p) = 0 + rw [show p = k.succ.castSucc from rfl, hk] + norm_num [SignType.sign] + have hfilteredSource : + ¬(fun z : SignType => decide (z ≠ 0)) + (List.ofFn (fun i => SignType.sign (x i)))[(p : ℕ)] := by + rw [hvalueSource] + decide + have hsource : + (List.ofFn (fun i => SignType.sign (x' i))).filter (· ≠ 0) = + (List.ofFn (fun i => SignType.sign (x i))).filter (· ≠ 0) := by + rw [hofFn] + exact List.filter_eraseIdx_eq_of_getElem_not + hlenSource hfilteredSource + have hxzero : x' 0 = x 0 := by + simp only [x', p, Fin.succAbove_zero_of_interior] + have hyzero : y' 0 = y 0 := by + simp only [y', p, Fin.succAbove_zero_of_interior] + have hxlast : + x' (Fin.last (n + 1)) = x (Fin.last (n + 2)) := by + simp only [x', p, Fin.succAbove_last_of_interior] + have hylast : + y' (Fin.last (n + 1)) = y (Fin.last (n + 2)) := by + simp only [y', p, Fin.succAbove_last_of_interior] + have hinterior : + List.ofFn + (fun i : Fin n => + SignType.sign (y' i.succ.castSucc)) = + (List.ofFn + (fun i : Fin (n + 1) => + SignType.sign (y i.succ.castSucc))).eraseIdx k := by + simpa only [y', p, Function.comp_apply] using + List.ofFn_interior_succAbove_eq_eraseIdx + (SignType.sign ∘ y) k + let left : List SignType := + if x 0 = 0 then [] else [SignType.sign (y 0)] + let middle : List SignType := + List.ofFn + (fun i : Fin (n + 1) => + SignType.sign (y i.succ.castSucc)) + let right : List SignType := + if x (Fin.last (n + 2)) = 0 then [] + else [SignType.sign (y (Fin.last (n + 2)))] + let full : List SignType := left ++ middle ++ right + let reduced : List SignType := + left ++ middle.eraseIdx k ++ right + have hfull : + Fin.nodalPerturbationCoreSigns x y = full := by + rfl + have hreduced : + Fin.nodalPerturbationCoreSigns x' y' = reduced := by + simp only [Fin.nodalPerturbationCoreSigns, reduced, left, middle, + right, hxzero, hyzero, hxlast, hylast, hinterior] + have hmul : + x k.castSucc.castSucc * x k.succ.succ < 0 := + hnodal k hk + have hxleft : x k.castSucc.castSucc ≠ 0 := + left_ne_zero_of_mul (ne_of_lt hmul) + have hxright : x k.succ.succ ≠ 0 := + right_ne_zero_of_mul (ne_of_lt hmul) + have hopposite : + SignType.sign (y k.castSucc.castSucc) ≠ 0 ∧ + SignType.sign (y k.succ.succ) ≠ 0 ∧ + SignType.sign (y k.castSucc.castSucc) ≠ + SignType.sign (y k.succ.succ) := by + simpa only [hsign k.castSucc.castSucc hxleft, + hsign k.succ.succ hxright] using + SignType.sign_ne_zero_and_ne_of_mul_neg hmul + have hstep : List.NodalInsertion reduced full := by + by_cases hn : n = 0 + · subst n + have hkzero : k = 0 := Fin.eq_zero k + subst k + have hleftIndex : + (0 : Fin 1).castSucc.castSucc = (0 : Fin 3) := by + exact Fin.ext rfl + have hcenterIndex : + (0 : Fin 1).succ.castSucc = (1 : Fin 3) := by + exact Fin.ext rfl + have hrightIndex : + (0 : Fin 1).succ.succ = (2 : Fin 3) := by + exact Fin.ext rfl + have hlastIndex : + (Fin.last 2 : Fin 3) = (2 : Fin 3) := by + exact Fin.ext rfl + have hxzero' : x (0 : Fin 3) ≠ 0 := by + simpa only [hleftIndex] using hxleft + have hxtwo : x (2 : Fin 3) ≠ 0 := by + simpa only [hrightIndex] using hxright + have hsignLeft : SignType.sign (y 0) ≠ 0 := by + simpa only [hleftIndex] using hopposite.1 + have hsignTwo : SignType.sign (y 2) ≠ 0 := by + simpa only [hrightIndex] using hopposite.2.1 + have hsignNe : + SignType.sign (y 0) ≠ SignType.sign (y 2) := by + simpa only [hleftIndex, hrightIndex] using hopposite.2.2 + simpa [full, reduced, left, middle, right, hxzero', hxtwo, + hcenterIndex, hlastIndex] using + List.NodalInsertion.insert [] [] + (SignType.sign (y 0)) + (SignType.sign (y 2)) + (SignType.sign (y 1)) + hsignLeft hsignTwo hsignNe + · have hnpos : 0 < n := Nat.pos_of_ne_zero hn + by_cases hkzero : (k : ℕ) = 0 + · have hkeq : k = 0 := Fin.ext hkzero + subst k + have hxzero' : x 0 ≠ 0 := by + simpa using hxleft + have hmiddleLength : 1 < middle.length := by + simp [middle] + lia + simpa [full, reduced, left, hxzero'] using + List.NodalInsertion.eraseIdx_first_middle + (SignType.sign (y 0)) middle right + hmiddleLength + (by simpa using hopposite.1) + (by simpa [middle] using hopposite.2.1) + (by simpa [middle] using hopposite.2.2) + · by_cases hklast : (k : ℕ) = n + · have hkeq : k = Fin.last n := Fin.ext hklast + subst k + have hxlast' : x (Fin.last (n + 2)) ≠ 0 := by + simpa using hxright + have hpred : n - 1 + 1 = n := by lia + have hlen : middle.length = n - 1 + 2 := by + simp [middle] + lia + have hleftBound : n - 1 < middle.length := by + rw [hlen] + lia + have hleftMiddle : + middle[n - 1]'hleftBound = + SignType.sign + (y (Fin.last n).castSucc.castSucc) := by + rw [List.getElem_ofFn hleftBound] + congr 2 + apply Fin.ext + simp only [Fin.val_castSucc, Fin.val_succ, Fin.val_last] + lia + have hrightEndpoint : + SignType.sign (y (Fin.last (n + 2))) = + SignType.sign (y (Fin.last n).succ.succ) := by + congr 2 + have haMiddle : middle[n - 1] ≠ 0 := by + rw [hleftMiddle] + exact hopposite.1 + have hbEndpoint : + SignType.sign (y (Fin.last (n + 2))) ≠ 0 := by + rw [hrightEndpoint] + exact hopposite.2.1 + have habMiddle : + middle[n - 1] ≠ + SignType.sign (y (Fin.last (n + 2))) := by + rw [hleftMiddle, hrightEndpoint] + exact hopposite.2.2 + simpa [full, reduced, right, hxlast', hpred] using + List.NodalInsertion.eraseIdx_last_append_singleton + left middle + (SignType.sign (y (Fin.last (n + 2)))) + (n - 1) hlen haMiddle hbEndpoint habMiddle + · have hkpos : 0 < (k : ℕ) := Nat.pos_of_ne_zero hkzero + have hklt : (k : ℕ) < n := by lia + have hpred : + (k : ℕ) - 1 + 1 = (k : ℕ) := by lia + have hsucc : + (k : ℕ) - 1 + 2 = (k : ℕ) + 1 := by lia + have hleftBound : + (k : ℕ) - 1 < middle.length := by + simp [middle] + have hrightBound : + (k : ℕ) - 1 + 2 < middle.length := by + simp [middle] + lia + have hleftMiddle : + middle[(k : ℕ) - 1]'hleftBound = + SignType.sign (y k.castSucc.castSucc) := by + rw [List.getElem_ofFn hleftBound] + congr 2 + apply Fin.ext + simp only [Fin.val_castSucc, Fin.val_succ] + lia + have hrightMiddle : + middle[(k : ℕ) - 1 + 2]'hrightBound = + SignType.sign (y k.succ.succ) := by + rw [List.getElem_ofFn hrightBound] + congr 2 + apply Fin.ext + simp only [Fin.val_castSucc, Fin.val_succ] + lia + have haMiddle : middle[(k : ℕ) - 1] ≠ 0 := by + rw [hleftMiddle] + exact hopposite.1 + have hbMiddle : middle[(k : ℕ) - 1 + 2] ≠ 0 := by + rw [hrightMiddle] + exact hopposite.2.1 + have habMiddle : + middle[(k : ℕ) - 1] ≠ + middle[(k : ℕ) - 1 + 2] := by + rw [hleftMiddle, hrightMiddle] + exact hopposite.2.2 + have hlocal : + List.NodalInsertion + ((left ++ middle ++ right).eraseIdx + (left.length + ((k : ℕ) - 1 + 1))) + (left ++ middle ++ right) := + List.NodalInsertion.eraseIdx_append_middle + left middle right ((k : ℕ) - 1) + hrightBound haMiddle hbMiddle habMiddle + have hkMiddle : (k : ℕ) < middle.length := by + simpa [middle] using k.isLt + rw [hpred] at hlocal + rw [List.eraseIdx_append_middle + left middle right (k : ℕ) hkMiddle] at hlocal + simpa [full, reduced] using hlocal + have hstepCore : + List.NodalInsertion + (Fin.nodalPerturbationCoreSigns x' y') + (Fin.nodalPerturbationCoreSigns x y) := by + rw [hreduced, hfull] + exact hstep + have hsourceComp : + (List.ofFn (SignType.sign ∘ x')).filter (· ≠ 0) = + (List.ofFn (SignType.sign ∘ x)).filter (· ≠ 0) := by + calc + _ = (List.ofFn (fun i => SignType.sign (x' i))).filter + (· ≠ 0) := by + congr 2 + _ = (List.ofFn (fun i => SignType.sign (x i))).filter + (· ≠ 0) := hsource + _ = _ := by + congr 2 + rw [hsourceComp] at hrec + exact hrec.tail hstepCore + +/-- If there is no interior zero, filtering the original signs already gives +the perturbed core signs. -/ +theorem nodalPerturbationCoreSigns_eq_of_no_interior_zero + {n : ℕ} {x y : Fin (n + 2) → ℝ} + (hsign : ∀ i, x i ≠ 0 → + SignType.sign (y i) = SignType.sign (x i)) + (hinterior : ∀ i : Fin n, x i.succ.castSucc ≠ 0) : + (List.ofFn (SignType.sign ∘ x)).filter (· ≠ 0) = + Fin.nodalPerturbationCoreSigns x y := by + let sourceMiddle : List SignType := + List.ofFn (fun i : Fin n => + SignType.sign (x i.succ.castSucc)) + let targetMiddle : List SignType := + List.ofFn (fun i : Fin n => + SignType.sign (y i.succ.castSucc)) + have hsourceMiddle : + sourceMiddle.filter (· ≠ 0) = sourceMiddle := by + apply List.filter_eq_self.2 + intro s hs + simp only [sourceMiddle, List.mem_ofFn] at hs + obtain ⟨i, rfl⟩ := hs + exact decide_eq_true (sign_ne_zero.mpr (hinterior i)) + have hmiddle : sourceMiddle = targetMiddle := by + simp only [sourceMiddle, targetMiddle] + congr 1 + funext i + exact (hsign i.succ.castSucc (hinterior i)).symm + have hfilterEndpoint (i : Fin (n + 2)) : + [SignType.sign (x i)].filter (· ≠ 0) = + if x i = 0 then [] else [SignType.sign (y i)] := by + by_cases hi : x i = 0 + · simp [hi, SignType.sign] + · rw [if_neg hi, List.filter_singleton] + have hs := sign_ne_zero.mpr hi + have hp : decide (SignType.sign (x i) ≠ 0) = true := + decide_eq_true hs + rw [hp] + change [SignType.sign (x i)] = [SignType.sign (y i)] + rw [hsign i hi] + rw [List.ofFn_two_endpoints] + change + (([SignType.sign (x 0)] ++ sourceMiddle ++ + [SignType.sign (x (Fin.last (n + 1)))]).filter (· ≠ 0)) = + (if x 0 = 0 then [] else [SignType.sign (y 0)]) ++ + targetMiddle ++ + (if x (Fin.last (n + 1)) = 0 then [] + else [SignType.sign (y (Fin.last (n + 1)))]) + rw [List.filter_append, List.filter_append, hfilterEndpoint, + hsourceMiddle, hmiddle, hfilterEndpoint] + +/-- Nodal insertions transform the filtered original sign list into the +perturbed core sign list. -/ +theorem nodalInsertions_coreSigns + {n : ℕ} {x y : Fin (n + 2) → ℝ} + (hsign : ∀ i, x i ≠ 0 → + SignType.sign (y i) = SignType.sign (x i)) + (hnodal : ∀ i : Fin n, x i.succ.castSucc = 0 → + x i.castSucc.castSucc * x i.succ.succ < 0) : + Relation.ReflTransGen List.NodalInsertion + ((List.ofFn (SignType.sign ∘ x)).filter (· ≠ 0)) + (Fin.nodalPerturbationCoreSigns x y) := by + induction n with + | zero => + have hinterior : + ∀ i : Fin 0, x i.succ.castSucc ≠ 0 := by + exact fun i => Fin.elim0 i + rw [Fin.nodalPerturbationCoreSigns_eq_of_no_interior_zero + hsign hinterior] + | succ n ih => + by_cases hzero : + ∃ k : Fin (n + 1), x k.succ.castSucc = 0 + · obtain ⟨k, hk⟩ := hzero + exact Fin.nodalInsertions_coreSigns_remove + ih hsign hnodal k hk + · have hinterior : + ∀ i : Fin (n + 1), x i.succ.castSucc ≠ 0 := by + intro i hi + exact hzero ⟨i, hi⟩ + rw [Fin.nodalPerturbationCoreSigns_eq_of_no_interior_zero + hsign hinterior] + +/-- A sign-preserving perturbation increases variations by at most two when +all interior zeros are nodal. + +This is Karlin's finite endpoint-loss estimate: interior nodal insertions cost +nothing, while the two endpoints cost at most one variation each. +-/ +theorem signVariations_le_add_two_of_sign_eq_on_nonzero_of_interior_nodal + {n : ℕ} {x y : Fin (n + 2) → ℝ} + (hsign : ∀ i, x i ≠ 0 → + SignType.sign (y i) = SignType.sign (x i)) + (hnodal : ∀ i : Fin n, x i.succ.castSucc = 0 → + x i.castSucc.castSucc * x i.succ.succ < 0) : + Fin.signVariations y ≤ Fin.signVariations x + 2 := by + let middle : List SignType := + List.ofFn (fun i : Fin n => + SignType.sign (y i.succ.castSucc)) + let core := Fin.nodalPerturbationCoreSigns x y + have hchain : + Relation.ReflTransGen List.NodalInsertion + ((List.ofFn (SignType.sign ∘ x)).filter (· ≠ 0)) core := by + exact Fin.nodalInsertions_coreSigns hsign hnodal + have hcore : core.signVariations = Fin.signVariations x := by + rw [List.signVariations_eq_of_nodalInsertions hchain] + exact Fin.filtered_signList_signVariations x + have hsplit : + List.ofFn (SignType.sign ∘ y) = + SignType.sign (y 0) :: + (middle ++ [SignType.sign (y (Fin.last (n + 1)))]) := by + simpa only [middle, Function.comp_apply] using + List.ofFn_two_endpoints (SignType.sign ∘ y) + rw [Fin.signVariations_eq_signList, hsplit] + by_cases hzero : x 0 = 0 + · by_cases hlast : x (Fin.last (n + 1)) = 0 + · have hfull : + SignType.sign (y 0) :: + (middle ++ [SignType.sign (y (Fin.last (n + 1)))]) = + (SignType.sign (y 0) :: core) ++ + [SignType.sign (y (Fin.last (n + 1)))] := by + simp [core, middle, Fin.nodalPerturbationCoreSigns, + hzero, hlast] + rw [hfull] + calc + ((SignType.sign (y 0) :: core) ++ + [SignType.sign (y (Fin.last (n + 1)))]).signVariations ≤ + (SignType.sign (y 0) :: core).signVariations + 1 := + List.signVariations_append_singleton_signType_le_succ _ _ + _ ≤ (core.signVariations + 1) + 1 := + Nat.add_le_add_right + (List.signVariations_cons_le_succ (SignType.sign (y 0)) core) 1 + _ = Fin.signVariations x + 2 := by rw [hcore] + · have hfull : + SignType.sign (y 0) :: + (middle ++ [SignType.sign (y (Fin.last (n + 1)))]) = + SignType.sign (y 0) :: core := by + simp [core, middle, Fin.nodalPerturbationCoreSigns, + hzero, hlast] + rw [hfull] + calc + (SignType.sign (y 0) :: core).signVariations ≤ + core.signVariations + 1 := + List.signVariations_cons_le_succ _ _ + _ ≤ Fin.signVariations x + 2 := by rw [hcore]; lia + · by_cases hlast : x (Fin.last (n + 1)) = 0 + · have hfull : + SignType.sign (y 0) :: + (middle ++ [SignType.sign (y (Fin.last (n + 1)))]) = + core ++ [SignType.sign (y (Fin.last (n + 1)))] := by + simp [core, middle, Fin.nodalPerturbationCoreSigns, + hzero, hlast] + rw [hfull] + calc + (core ++ + [SignType.sign (y (Fin.last (n + 1)))]).signVariations ≤ + core.signVariations + 1 := + List.signVariations_append_singleton_signType_le_succ _ _ + _ ≤ Fin.signVariations x + 2 := by rw [hcore]; lia + · have hfull : + SignType.sign (y 0) :: + (middle ++ [SignType.sign (y (Fin.last (n + 1)))]) = + core := by + simp [core, middle, Fin.nodalPerturbationCoreSigns, + hzero, hlast] + rw [hfull, hcore] + lia + /-- A finite vector has at most one fewer sign variation than its length. -/ lemma signVariations_le_card_sub_one {R : Type*} [Zero R] [LinearOrder R] {n : ℕ} (x : Fin n → R) : signVariations x ≤ n - 1 := by @@ -530,7 +1315,7 @@ lemma exists_strictMono_strictlyAlternates_of_le_signVariations have hh : q ≤ d.length - 1 := by simpa [signVariations, List.signVariations, d, nz, raw, List.map_ofFn] using h - have hlen : q + 1 ≤ d.length := by omega + have hlen : q + 1 ≤ d.length := by lia have hsub : d.Sublist raw := (List.destutter_sublist (R := fun a b : SignType => a ≠ b) nz).trans List.filter_sublist @@ -547,7 +1332,7 @@ lemma exists_strictMono_strictlyAlternates_of_le_signVariations · intro i let k0 : Fin d.length := Fin.castLE hlen i.castSucc let k1 : Fin d.length := Fin.castLE hlen i.succ - have hklt : (i : ℕ) + 1 < d.length := by omega + have hklt : (i : ℕ) + 1 < d.length := by lia have hchain : d.IsChain (· ≠ ·) := List.isChain_destutter (R := fun a b : SignType => a ≠ b) nz have hkd : d.get k0 ≠ d.get k1 := by @@ -578,6 +1363,84 @@ lemma exists_strictMono_strictlyAlternates_of_le_signVariations · rw [← he0, ← he1] exact hkd +/-- A strictly alternating subsequence gives a lower bound on the sign +variations of the ambient vector. -/ +lemma StrictlyAlternates.le_signVariations_of_strictMono + {m q : ℕ} {y : Fin m → ℝ} + {rows : Fin (q + 1) → Fin m} + (h : StrictlyAlternates (fun i => y (rows i))) + (hrows : StrictMono rows) : q ≤ signVariations y := by + by_cases hq : q = 0 + · simp [hq] + have hnonzero : ∀ i, y (rows i) ≠ 0 := by + intro i + refine Fin.cases ?_ (fun j => ?_) i + · intro hy + let i0 : Fin q := ⟨0, Nat.pos_of_ne_zero hq⟩ + have hneg := h i0 + change y (rows 0) * y (rows i0.succ) < 0 at hneg + rw [hy, zero_mul] at hneg + exact (lt_irrefl 0) hneg + · intro hy + have hneg := h j + change y (rows j.castSucc) * y (rows j.succ) < 0 at hneg + rw [hy, mul_zero] at hneg + exact (lt_irrefl 0) hneg + have hsub : + (List.ofFn (SignType.sign ∘ fun i => y (rows i))).Sublist + (List.ofFn (SignType.sign ∘ y)) := by + rw [List.sublist_iff_exists_fin_orderEmbedding_get_eq] + let e0 : + Fin (List.ofFn (SignType.sign ∘ fun i => y (rows i))).length ≃o + Fin (q + 1) := + Fin.castOrderIso List.length_ofFn + let e1 : Fin (q + 1) ↪o Fin m := + OrderEmbedding.ofStrictMono rows hrows + let e2 : + Fin m ≃o Fin (List.ofFn (SignType.sign ∘ y)).length := + (Fin.castOrderIso List.length_ofFn).symm + refine ⟨e0.toOrderEmbedding.trans (e1.trans e2.toOrderEmbedding), ?_⟩ + intro i + simp only [List.get_ofFn, e0, e1, e2, RelEmbedding.trans_apply, + Function.comp_apply] + apply congrArg SignType.sign + apply congrArg y + apply Fin.ext + rfl + have hfilter : + (List.ofFn (SignType.sign ∘ fun i => y (rows i))).filter + (· ≠ 0) = + List.ofFn (SignType.sign ∘ fun i => y (rows i)) := by + rw [List.filter_eq_self] + intro s hs + simp only [List.mem_ofFn] at hs + obtain ⟨i, rfl⟩ := hs + simp [Function.comp_apply, hnonzero i] + have hsub_nonzero : + (List.ofFn (SignType.sign ∘ fun i => y (rows i))).Sublist + ((List.ofFn (SignType.sign ∘ y)).filter (· ≠ 0)) := by + rw [← hfilter] + exact List.Sublist.filter (· ≠ 0) hsub + have hchain : + (List.ofFn (SignType.sign ∘ fun i => y (rows i))).IsChain + (· ≠ ·) := by + rw [List.isChain_ofFn] + intro i hi + change SignType.sign (y (rows ⟨i, by lia⟩)) ≠ + SignType.sign (y (rows ⟨i + 1, hi⟩)) + have hneg := h (⟨i, by lia⟩ : Fin q) + change y (rows ⟨i, by lia⟩) * y (rows ⟨i + 1, hi⟩) < 0 at hneg + rcases mul_neg_iff.mp hneg with ⟨hleft, hright⟩ | ⟨hleft, hright⟩ + · rw [sign_pos hleft, sign_neg hright] + simp + · rw [sign_neg hleft, sign_pos hright] + simp + have hlen := + List.IsChain.length_le_length_destutter_ne hsub_nonzero hchain + rw [signVariations, List.signVariations, List.map_ofFn] + simp only [List.length_ofFn] at hlen + lia + /-- Two nonzero strictly alternating vectors have pointwise products of one strict sign. -/ lemma StrictlyAlternates.pointwise_mul_pos_or_neg {n : ℕ} @@ -700,3 +1563,254 @@ lemma strictlyAlternates_alternating (n : ℕ) {ε : ℝ} (hε : 0 < ε) : _ < 0 := neg_lt_zero.mpr (sq_pos_of_pos hε) end Fin + +/-- Sign variation is monotone under taking a list prefix. -/ +theorem List.signVariations_mono_of_prefix + {R : Type*} [Zero R] [LinearOrder R] + {l₁ l₂ : List R} (h : l₁ <+: l₂) : + l₁.signVariations ≤ l₂.signVariations := by + rw [List.signVariations, List.signVariations] + have hsign : + (l₁.map SignType.sign).filter (· ≠ 0) <+: + (l₂.map SignType.sign).filter (· ≠ 0) := + (h.map SignType.sign).filter (· ≠ 0) + exact (Nat.sub_le_sub_right + (hsign.destutter (R := fun x y : SignType => x ≠ y)).length_le) 1 + +/-- Taking a list prefix cannot increase sign variation. -/ +theorem List.signVariations_take_le + {R : Type*} [Zero R] [LinearOrder R] + (l : List R) (k : ℕ) : + (l.take k).signVariations ≤ l.signVariations := + List.signVariations_mono_of_prefix (List.take_prefix k l) + +/-- A nonzero endpoint survives sign filtering as the final sign of its prefix. -/ +theorem List.getLast?_filter_sign_take_succ + {R : Type*} [Zero R] [LinearOrder R] + (l : List R) {i : ℕ} (hi : i < l.length) + (hne : l[i] ≠ 0) : + (((l.take (i + 1)).map SignType.sign).filter + (· ≠ 0)).getLast? = some (SignType.sign l[i]) := by + rw [List.take_succ_eq_append_getElem hi, List.map_append, + List.filter_append] + simp [sign_ne_zero.mpr hne] + +/-- Appending one real entry increases sign variation by at most one. -/ +theorem List.signVariations_append_singleton_le_succ + (l : List ℝ) (x : ℝ) : + (l ++ [x]).signVariations ≤ l.signVariations + 1 := by + rcases le_total 0 x with hx | hx + · apply List.signVariations_append_nonneg_le_succ + simpa using hx + · apply List.signVariations_append_nonpos_le_succ + simpa using hx + +/-- Data expressing a finite vector as nonnegative weights pulled back from an +ordered collection of sign blocks. + +This is an interface for the elementary finite-list decomposition in Karlin's +proof, not an assertion that the decomposition already exists. Separating the +data keeps later matrix arguments independent of how maximal same-sign blocks +are constructed and avoids formalizing an unrelated combinatorial model. -/ +structure Fin.SignBlockDecomposition {n : ℕ} (c : Fin n → ℝ) where + numBlocks : ℕ + numBlocks_pos : 0 < numBlocks + block : Fin n → Fin numBlocks + block_mono : Monotone block + weight : Fin n → ℝ + weight_nonneg : ∀ j, 0 ≤ weight j + coeff : Fin numBlocks → ℝ + reconstruct : ∀ j, weight j * coeff (block j) = c j + numBlocks_sub_one : numBlocks - 1 = Fin.signVariations c + +/-- The sign variation of the prefix ending at `j`. -/ +def Fin.prefixSignVariations + {n : ℕ} (c : Fin n → ℝ) (j : Fin n) : ℕ := + ((List.ofFn c).take (j + 1)).signVariations + +/-- Prefix sign variation is at most the index of the prefix endpoint. -/ +theorem Fin.prefixSignVariations_le_val + {n : ℕ} (c : Fin n → ℝ) (j : Fin n) : + Fin.prefixSignVariations c j ≤ j := by + unfold Fin.prefixSignVariations + calc + ((List.ofFn c).take (j + 1)).signVariations ≤ + ((List.ofFn c).take (j + 1)).length - 1 := + List.signVariations_le_length_sub_one _ + _ = j := by simp + +/-- At the final index, prefix sign variation is full-vector sign variation. -/ +theorem Fin.prefixSignVariations_last + {n : ℕ} (c : Fin (n + 1) → ℝ) : + Fin.prefixSignVariations c (Fin.last n) = + Fin.signVariations c := by + rw [Fin.prefixSignVariations, Fin.signVariations] + have hlength : + (Fin.last n : ℕ) + 1 = (List.ofFn c).length := by + simp + rw [hlength, List.take_length] + +/-- Prefix sign variation is monotone in the prefix endpoint. -/ +theorem Fin.monotone_prefixSignVariations + {n : ℕ} (c : Fin n → ℝ) : + Monotone (Fin.prefixSignVariations c) := by + intro i j hij + unfold Fin.prefixSignVariations + apply List.signVariations_mono_of_prefix + exact List.take_prefix_take_left (Nat.add_le_add_right hij 1) + +/-- Prefix sign variation is bounded by full-vector sign variation. -/ +theorem Fin.prefixSignVariations_le_signVariations + {n : ℕ} (c : Fin n → ℝ) (j : Fin n) : + Fin.prefixSignVariations c j ≤ Fin.signVariations c := by + unfold Fin.prefixSignVariations Fin.signVariations + exact List.signVariations_take_le _ _ + +/-- The sign-block index of an entry, counted by prefix sign variation. -/ +@[expose] +def Fin.signBlockIndex + {n : ℕ} (c : Fin n → ℝ) (j : Fin n) : + Fin (Fin.signVariations c + 1) := + ⟨Fin.prefixSignVariations c j, + Nat.lt_succ_of_le (Fin.prefixSignVariations_le_signVariations c j)⟩ + +@[simp] +theorem Fin.val_signBlockIndex + {n : ℕ} (c : Fin n → ℝ) (j : Fin n) : + (Fin.signBlockIndex c j : ℕ) = + Fin.prefixSignVariations c j := + rfl + +@[simp] +theorem Fin.signBlockIndex_last + {n : ℕ} (c : Fin (n + 1) → ℝ) : + Fin.signBlockIndex c (Fin.last n) = + Fin.last (Fin.signVariations c) := by + apply Fin.ext + exact Fin.prefixSignVariations_last c + +/-- Sign-block indices are monotone in the original index. -/ +theorem Fin.monotone_signBlockIndex + {n : ℕ} (c : Fin n → ℝ) : + Monotone (Fin.signBlockIndex c) := by + intro i j hij + exact Fin.monotone_prefixSignVariations c hij + +/-- Adjacent prefix sign-variation values differ by at most one. -/ +theorem Fin.prefixSignVariations_succ_le + {n : ℕ} (c : Fin (n + 1) → ℝ) (i : Fin n) : + Fin.prefixSignVariations c i.succ ≤ + Fin.prefixSignVariations c i.castSucc + 1 := by + unfold Fin.prefixSignVariations + have hindex : + (i : ℕ) + 1 < (List.ofFn c).length := by + simp [i.isLt] + rw [show (i.succ : ℕ) + 1 = ((i : ℕ) + 1) + 1 by simp, + List.take_succ_eq_append_getElem hindex] + exact List.signVariations_append_singleton_le_succ _ _ + +/-- Nonzero entries with equal block index and ordered indices have equal signs. -/ +theorem Fin.sign_eq_of_le_of_signBlockIndex_eq + {n : ℕ} (c : Fin n → ℝ) {i j : Fin n} + (hij : i ≤ j) (hi : c i ≠ 0) (hj : c j ≠ 0) + (hblock : Fin.signBlockIndex c i = Fin.signBlockIndex c j) : + SignType.sign (c i) = SignType.sign (c j) := by + let l := List.ofFn c + let sᵢ := + ((l.take (i + 1)).map SignType.sign).filter (· ≠ 0) + let sⱼ := + ((l.take (j + 1)).map SignType.sign).filter (· ≠ 0) + have hprefix : sᵢ <+: sⱼ := + ((List.take_prefix_take_left + (Nat.add_le_add_right hij 1)).map SignType.sign).filter (· ≠ 0) + have hprefEq : + Fin.prefixSignVariations c i = + Fin.prefixSignVariations c j := by + simpa only [Fin.val_signBlockIndex] using congrArg Fin.val hblock + have hvariationEq : + (sᵢ.destutter (· ≠ ·)).length - 1 = + (sⱼ.destutter (· ≠ ·)).length - 1 := by + change (l.take (i + 1)).signVariations = + (l.take (j + 1)).signVariations at hprefEq + change (sᵢ.destutter (· ≠ ·)).length - 1 = + (sⱼ.destutter (· ≠ ·)).length - 1 at hprefEq + exact hprefEq + have hiIndex : (i : ℕ) < l.length := by simp [l] + have hjIndex : (j : ℕ) < l.length := by simp [l] + have hiValue : l[i] ≠ 0 := by simpa [l] using hi + have hjValue : l[j] ≠ 0 := by simpa [l] using hj + have hlastI : + sᵢ.getLast? = some (SignType.sign (c i)) := by + simpa [sᵢ, l] using + List.getLast?_filter_sign_take_succ l hiIndex hiValue + have hlastJ : + sⱼ.getLast? = some (SignType.sign (c j)) := by + simpa [sⱼ, l] using + List.getLast?_filter_sign_take_succ l hjIndex hjValue + have hdestIPos : 0 < (sᵢ.destutter (· ≠ ·)).length := by + rw [List.length_pos_iff] + intro hd + have hlastDest := List.getLast?_destutter_ne sᵢ + rw [hd, hlastI] at hlastDest + simp at hlastDest + have hdestLengthLe : + (sᵢ.destutter (· ≠ ·)).length ≤ + (sⱼ.destutter (· ≠ ·)).length := + (hprefix.destutter + (R := fun x y : SignType => x ≠ y)).length_le + have hlengthEq : + (sᵢ.destutter (· ≠ ·)).length = + (sⱼ.destutter (· ≠ ·)).length := by + lia + have hlastEq : sᵢ.getLast? = sⱼ.getLast? := + hprefix.getLast?_eq_of_destutter_length_le hlengthEq.ge + rw [hlastI, hlastJ] at hlastEq + exact Option.some.inj hlastEq + +/-- Nonzero entries in the same sign block have equal signs. -/ +theorem Fin.sign_eq_of_signBlockIndex_eq + {n : ℕ} (c : Fin n → ℝ) {i j : Fin n} + (hi : c i ≠ 0) (hj : c j ≠ 0) + (hblock : Fin.signBlockIndex c i = Fin.signBlockIndex c j) : + SignType.sign (c i) = SignType.sign (c j) := by + rcases le_total i j with hij | hji + · exact Fin.sign_eq_of_le_of_signBlockIndex_eq c hij hi hj hblock + · exact (Fin.sign_eq_of_le_of_signBlockIndex_eq + c hji hj hi hblock.symm).symm + +/-- The same-sign block decomposition used in Karlin's variation theorem. + +Zero entries receive weight zero. Each block containing a nonzero entry uses +the sign of one such entry as its coefficient; the same-block sign theorem +makes this choice independent of the representative for reconstruction. -/ +noncomputable def Fin.signBlockDecomposition + {n : ℕ} (c : Fin n → ℝ) : Fin.SignBlockDecomposition c := by + classical + let coeff : Fin (Fin.signVariations c + 1) → ℝ := fun b => + if h : ∃ j, c j ≠ 0 ∧ Fin.signBlockIndex c j = b then + (SignType.sign (c h.choose) : ℝ) + else 0 + refine + { numBlocks := Fin.signVariations c + 1 + numBlocks_pos := Nat.succ_pos _ + block := Fin.signBlockIndex c + block_mono := Fin.monotone_signBlockIndex c + weight := fun j => |c j| + weight_nonneg := fun j => abs_nonneg (c j) + coeff := coeff + reconstruct := ?_ + numBlocks_sub_one := Nat.add_sub_cancel _ _ } + intro j + by_cases hj : c j = 0 + · simp only [hj, abs_zero, zero_mul] + · have hex : + ∃ k, c k ≠ 0 ∧ + Fin.signBlockIndex c k = Fin.signBlockIndex c j := + ⟨j, hj, rfl⟩ + change |c j| * coeff (Fin.signBlockIndex c j) = c j + rw [show coeff (Fin.signBlockIndex c j) = + (SignType.sign (c hex.choose) : ℝ) by + simp only [coeff, dif_pos hex], + ← Fin.sign_eq_of_signBlockIndex_eq c hj + hex.choose_spec.1 hex.choose_spec.2.symm, + abs_mul_sign] diff --git a/RealRooted/Mathlib/LinearAlgebra/Matrix/SignVariationTopology.lean b/RealRooted/Mathlib/LinearAlgebra/Matrix/SignVariationTopology.lean new file mode 100644 index 000000000..48f7fb562 --- /dev/null +++ b/RealRooted/Mathlib/LinearAlgebra/Matrix/SignVariationTopology.lean @@ -0,0 +1,116 @@ +import RealRooted.Mathlib.LinearAlgebra.Matrix.SignVariation + +/-! +# Topological properties of sign variations + +This file proves the finite-dimensional lower semicontinuity of sign variations. +The result supplies the limit step in Karlin's Gaussian approximation argument +for variation-diminishing matrices. +-/ + +open Filter Topology + +namespace Fin + +/-- Nonzero coordinates eventually retain their signs under convergence. -/ +theorem eventually_sign_eq_of_tendsto + {α : Type*} {l : Filter α} [l.NeBot] {n : ℕ} + {f : α → Fin n → ℝ} {x : Fin n → ℝ} + (hf : Tendsto f l (𝓝 x)) : + ∀ᶠ a in l, ∀ i, x i ≠ 0 → + SignType.sign (f a i) = SignType.sign (x i) := by + have hsign : + ∀ i : Fin n, ∀ᶠ a in l, x i ≠ 0 → + SignType.sign (f a i) = SignType.sign (x i) := by + intro i + by_cases hi : x i = 0 + · exact Filter.Eventually.of_forall fun _ hne => (hne hi).elim + · have hiLimit := tendsto_pi_nhds.mp hf i + rcases lt_or_gt_of_ne hi with hneg | hpos + · filter_upwards [hiLimit.eventually_lt_const hneg] with a ha + intro + rw [sign_neg ha, sign_neg hneg] + · filter_upwards [hiLimit.eventually_const_lt hpos] with a ha + intro + rw [sign_pos ha, sign_pos hpos] + exact Filter.eventually_all.mpr hsign + +/-- Sign variations cannot increase when a convergent net reaches its limit. -/ +theorem signVariations_le_of_tendsto + {α : Type*} {l : Filter α} [l.NeBot] {n r : ℕ} + {f : α → Fin n → ℝ} {x : Fin n → ℝ} + (hf : Tendsto f l (𝓝 x)) + (hr : ∀ᶠ a in l, signVariations (f a) ≤ r) : + signVariations x ≤ r := by + let raw : List SignType := List.ofFn (SignType.sign ∘ x) + let nz : List SignType := raw.filter (· ≠ 0) + let d : List SignType := nz.destutter (· ≠ ·) + have hsub : d.Sublist raw := + (List.destutter_sublist (· ≠ ·) nz).trans List.filter_sublist + obtain ⟨e, he⟩ := + List.sublist_iff_exists_fin_orderEmbedding_get_eq.mp hsub + have hrawlen : raw.length = n := by + simp [raw] + let eN : Fin d.length ↪o Fin n := + e.trans (Fin.castOrderIso hrawlen).toOrderEmbedding + have he' (k : Fin d.length) : + d.get k = SignType.sign (x (eN k)) := by + rw [he k] + simp only [raw, List.get_ofFn, Function.comp_apply] + congr 2 + have hd_ne (z : SignType) (hz : z ∈ d) : z ≠ 0 := by + have hz_nz : z ∈ nz := + (List.destutter_sublist (· ≠ ·) nz).mem hz + exact of_decide_eq_true (List.mem_filter.mp hz_nz).2 + have hd_filter : d.filter (· ≠ 0) = d := by + rw [List.filter_eq_self] + intro z hz + simp [hd_ne z hz] + have hsign : + ∀ᶠ a in l, ∀ k : Fin d.length, + d.get k = SignType.sign (f a (eN k)) := by + filter_upwards [eventually_sign_eq_of_tendsto hf] with a ha + intro k + have hxne : x (eN k) ≠ 0 := by + rw [← sign_ne_zero, ← he' k] + exact hd_ne _ (List.get_mem d k) + rw [he' k, ha (eN k) hxne] + have hmono : + ∀ᶠ a in l, signVariations x ≤ signVariations (f a) := by + filter_upwards [hsign] with a ha + let rawA : List SignType := List.ofFn (SignType.sign ∘ f a) + have hrawAlen : rawA.length = n := by + simp [rawA] + let eA : Fin d.length ↪o Fin rawA.length := + eN.trans (Fin.castOrderIso hrawAlen.symm).toOrderEmbedding + have hdsub : d.Sublist rawA := by + apply List.sublist_iff_exists_fin_orderEmbedding_get_eq.mpr + refine ⟨eA, ?_⟩ + intro k + rw [ha k] + simp only [rawA, List.get_ofFn, Function.comp_apply] + congr 2 + have hdsub_nz : d.Sublist (rawA.filter (· ≠ 0)) := by + simpa only [hd_filter] using hdsub.filter (· ≠ 0) + have hlen := + (List.isChain_destutter (· ≠ ·) nz).length_le_length_destutter_ne hdsub_nz + simpa only [signVariations, List.signVariations, List.map_ofFn, d, nz, raw, + rawA] using Nat.sub_le_sub_right hlen 1 + obtain ⟨a, hxa, har⟩ := (hmono.and hr).exists + exact hxa.trans har + +/-- A convergent perturbation of a vector with nodal interior zeros eventually +has at most two additional sign variations. -/ +theorem eventually_signVariations_le_add_two_of_tendsto_of_interior_nodal + {α : Type*} {l : Filter α} [l.NeBot] + {n : ℕ} {f : α → Fin (n + 2) → ℝ} + {x : Fin (n + 2) → ℝ} + (hf : Tendsto f l (𝓝 x)) + (hnodal : ∀ i : Fin n, x i.succ.castSucc = 0 → + x i.castSucc.castSucc * x i.succ.succ < 0) : + ∀ᶠ a in l, + signVariations (f a) ≤ signVariations x + 2 := by + filter_upwards [eventually_sign_eq_of_tendsto hf] with a ha + exact signVariations_le_add_two_of_sign_eq_on_nonzero_of_interior_nodal ha hnodal + +end Fin diff --git a/RealRooted/Mathlib/LinearAlgebra/Vandermonde.lean b/RealRooted/Mathlib/LinearAlgebra/Vandermonde.lean new file mode 100644 index 000000000..34a02cb5c --- /dev/null +++ b/RealRooted/Mathlib/LinearAlgebra/Vandermonde.lean @@ -0,0 +1,27 @@ +import Mathlib.LinearAlgebra.Vandermonde + +/-! +# Ordered Vandermonde determinants + +This file adds the strict positivity consequence of the Vandermonde +determinant formula for a strictly increasing family. +-/ + +public section + +namespace Matrix + +variable {R : Type*} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] + +/-- A Vandermonde determinant on a strictly increasing family is positive. -/ +theorem det_vandermonde_pos_of_strictMono {q : ℕ} + {y : Fin q → R} (hy : StrictMono y) : + 0 < (vandermonde y).det := by + rw [det_vandermonde] + apply Finset.prod_pos + intro i hi + apply Finset.prod_pos + intro j hj + exact sub_pos.mpr (hy (Finset.mem_Ioi.mp hj)) + +end Matrix diff --git a/RealRooted/PFPolynomial.lean b/RealRooted/PFPolynomial.lean index c86839935..0e530ec41 100644 --- a/RealRooted/PFPolynomial.lean +++ b/RealRooted/PFPolynomial.lean @@ -187,6 +187,14 @@ theorem of_sequence let hpnn := hasNonnegCoeffs_of_IsPolyaFreqSeq_coeff hpf ⟨hpnn, hASW hpnn hpf⟩ +/-- Construct a PF polynomial directly from its Pólya-frequency coefficient +sequence using the proved forward ASW theorem. -/ +theorem of_polyaFreqSeq {p : ℝ[X]} + (hpf : IsPolyaFreqSeq (fun n => p.coeff n)) : + IsPFPolynomial p := + let hpnn := hasNonnegCoeffs_of_IsPolyaFreqSeq_coeff hpf + ⟨hpnn, aissenSchoenbergWhitneyForwardOrZero hpnn hpf⟩ + /-- Forward-ASW endpoint closure for positive affine coefficient limits. -/ theorem of_forall_pos_add_C_mul_of_forward (hASW : aissenSchoenbergWhitneyForwardOrZeroStatement) @@ -207,6 +215,25 @@ theorem splits_of_forall_pos_add_C_mul_of_forward p.Splits := (of_forall_pos_add_C_mul_of_forward hASW hpnn hqnn hfamily).ne_zero_and_splits hp0 |>.2 +/-- PF endpoint closure for positive affine coefficient limits, using the +proved forward ASW theorem. -/ +theorem of_forall_pos_add_C_mul + {p q : ℝ[X]} + (hpnn : HasNonnegCoeffs p) (hqnn : HasNonnegCoeffs q) + (hfamily : ∀ {μ : ℝ}, 0 < μ → (p + C μ * q).Splits) : + IsPFPolynomial p := + IsPFPolynomial.of_polyaFreqSeq <| + IsPolyaFreqSeq.of_forall_pos_add_C_mul_splits hpnn hqnn hfamily + +/-- Splitting form of `IsPFPolynomial.of_forall_pos_add_C_mul`. -/ +theorem splits_of_forall_pos_add_C_mul + {p q : ℝ[X]} + (hp0 : p ≠ 0) + (hpnn : HasNonnegCoeffs p) (hqnn : HasNonnegCoeffs q) + (hfamily : ∀ {μ : ℝ}, 0 < μ → (p + C μ * q).Splits) : + p.Splits := + (of_forall_pos_add_C_mul hpnn hqnn hfamily).ne_zero_and_splits hp0 |>.2 + theorem to_sequence {p : ℝ[X]} (hp : IsPFPolynomial p) :