diff --git a/RealRooted.lean b/RealRooted.lean index 4bca6b20..ebac2d9b 100644 --- a/RealRooted.lean +++ b/RealRooted.lean @@ -99,6 +99,8 @@ import RealRooted.DegreeDropDivXPrec import RealRooted.DegreeDropReversal import RealRooted.DegreeIncreasingLocalLowerCount import RealRooted.Derivative +import RealRooted.DerivativeShiftRootMatching +import RealRooted.DerivativeShiftSequence import RealRooted.DifferentialBlocks import RealRooted.ElementaryDifferential import RealRooted.EulerOperator @@ -141,9 +143,12 @@ import RealRooted.LiebSokalPointwise import RealRooted.Linear import RealRooted.LinearPowerFamily import RealRooted.LiuOppositeSigns +import RealRooted.LiuOppositeSigns.BoundedIntervalContinuity import RealRooted.LiuOppositeSigns.CommonInterleaverConsequences import RealRooted.LiuOppositeSigns.Corollary22 import RealRooted.LiuOppositeSigns.DeletionBranches +import RealRooted.LiuOppositeSigns.DerivativeShiftRegularization +import RealRooted.LiuOppositeSigns.DerivativeShiftSequenceRegularization import RealRooted.LiuOppositeSigns.FactorReturnAssembly import RealRooted.LiuOppositeSigns.FactorReturnLeft import RealRooted.LiuOppositeSigns.FactorReturnStatements @@ -162,6 +167,8 @@ import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.RootOrderUpper import RealRooted.LiuOppositeSigns.ForwardLowDegree import RealRooted.LiuOppositeSigns.NonnegCoeffs import RealRooted.LiuOppositeSigns.PositiveSplitPair +import RealRooted.LiuOppositeSigns.RootCountRelStability +import RealRooted.LiuOppositeSigns.RootCountClosure import RealRooted.LiuOppositeSigns.Theorem21Assembly import RealRooted.LiuOppositeSigns.Theorem21Statements import RealRooted.LiuOppositeSigns.XSub.CubicCubic @@ -199,6 +206,8 @@ import RealRooted.Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic import RealRooted.Mathlib.Combinatorics.Enumerative.OrderedSubsetPairs import RealRooted.Mathlib.Data.List.Interleave import RealRooted.Mathlib.Data.List.Zip +import RealRooted.Mathlib.Data.Multiset.Rel +import RealRooted.RootMatchingSort import RealRooted.Mathlib.Data.Nat.Cast.Basic import RealRooted.Mathlib.Data.Nat.Choose.Cast import RealRooted.Mathlib.LinearAlgebra.Matrix.Determinant.Basic @@ -231,6 +240,7 @@ import RealRooted.RectangularConvolutionIdentity import RealRooted.RectangularPolarization import RealRooted.RectangularPolarizationComplement import RealRooted.RecurrenceDiscriminant +import RealRooted.ReflectedRootCountLocalConstancy import RealRooted.RootContinuity import RealRooted.RootCountFinite import RealRooted.RootCountJump diff --git a/RealRooted/AllCombo.lean b/RealRooted/AllCombo.lean index 24c817f1..740519fd 100644 --- a/RealRooted/AllCombo.lean +++ b/RealRooted/AllCombo.lean @@ -87,11 +87,6 @@ lemma allComboRealRooted_iterate_derivative exact allComboRealRooted_derivative (allComboRealRooted_iterate_derivative hall n) -lemma iterateTDeriv_linear_combo (eps α β : ℝ) (n : ℕ) (f g : ℝ[X]) : - iterateTDeriv eps n (C α * f + C β * g) = - C α * iterateTDeriv eps n f + C β * iterateTDeriv eps n g := by - rw [iterateTDeriv_add, iterateTDeriv_C_mul, iterateTDeriv_C_mul] - lemma TDeriv_eq_zero_iff (eps : ℝ) {p : ℝ[X]} : TDeriv eps p = 0 ↔ p = 0 := by constructor diff --git a/RealRooted/CommonInterleaver/RootCountCombinatorics.lean b/RealRooted/CommonInterleaver/RootCountCombinatorics.lean index d41bb945..1eac64ae 100644 --- a/RealRooted/CommonInterleaver/RootCountCombinatorics.lean +++ b/RealRooted/CommonInterleaver/RootCountCombinatorics.lean @@ -462,6 +462,28 @@ theorem succDegreeRootCrossing_of_rootCount rw [card_roots_of_splits hg, hdeg] exact succRootCrossing_of_count_le_two hMcard hNcard hcount +/-- Converse root-count bridge from successor-degree descending-root crossing +to the asymmetric lower-threshold formulation. -/ +theorem succDegreeRootCount_of_rootCrossing + {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits) + (hdeg : g.natDegree = f.natDegree + 1) + (hcross : + (∀ j, 1 ≤ j → j ≤ f.natDegree → + (rootSeqDesc g).getD j 0 ≤ + (rootSeqDesc f).getD (j - 1) 0) ∧ + (∀ j, 1 ≤ j → j < f.natDegree → + (rootSeqDesc f).getD j 0 ≤ + (rootSeqDesc g).getD (j - 1) 0)) : + ∀ x : ℝ, + ((f.roots.filter (· ≤ x)).card : ℤ) - + (g.roots.filter (· ≤ x)).card ≤ 0 ∧ + ((g.roots.filter (· ≤ x)).card : ℤ) - + (f.roots.filter (· ≤ x)).card ≤ 2 := by + have hMcard : f.roots.card = f.natDegree := card_roots_of_splits hf + have hNcard : g.roots.card = f.natDegree + 1 := by + rw [card_roots_of_splits hg, hdeg] + exact count_le_two_of_succRootCrossing hMcard hNcard hcross + /-- Root-count bridge from the upper-threshold formulation to the succ-degree root-crossing target. -/ theorem succDegreeRootCrossing_of_rootCountAbove diff --git a/RealRooted/CommonInterleaverSeq.lean b/RealRooted/CommonInterleaverSeq.lean index a70eb163..07456bbc 100644 --- a/RealRooted/CommonInterleaverSeq.lean +++ b/RealRooted/CommonInterleaverSeq.lean @@ -80,6 +80,20 @@ lemma rootSeqDesc_eq_reverse_of_pairwise · grind · exact Multiset.coe_eq_coe.mp (by simp [rootSeqDesc, hrs_eq, Multiset.sort_eq]) +/-- The canonical descending root sequence is the roots sorted in decreasing order. -/ +lemma rootSeqDesc_eq_sort_ge (f : ℝ[X]) : + rootSeqDesc f = f.roots.sort (· ≥ ·) := by + have hpair : + ((f.roots.sort (· ≥ ·)).reverse).Pairwise (· ≤ ·) := by + simpa using + (Multiset.pairwise_sort (s := f.roots) (r := (· ≥ ·))).reverse + have hroots : + (↑((f.roots.sort (· ≥ ·)).reverse) : Multiset ℝ) = f.roots := by + simp [Multiset.sort_eq] + simpa using + (rootSeqDesc_eq_reverse_of_pairwise (f := f) + (rs := (f.roots.sort (· ≥ ·)).reverse) hpair hroots) + /-- The `j`th Chudnovsky--Seymour interval attached to a descending root sequence `rs = [r₁, ..., r_d]`. diff --git a/RealRooted/Compatibility/Basic.lean b/RealRooted/Compatibility/Basic.lean index f629a269..9a35b601 100644 --- a/RealRooted/Compatibility/Basic.lean +++ b/RealRooted/Compatibility/Basic.lean @@ -106,6 +106,22 @@ lemma derivative {f g : ℝ[X]} (h : Compatible f g) : · rw [hcomb] exact derivative_eq_zero_or_ne_zero_and_splits hrr.2 +/-- Compatibility is preserved by the degree-preserving root regularizer +`iterateTDeriv` at every positive shift. -/ +lemma iterateTDeriv {f g : ℝ[X]} (h : Compatible f g) + {eps : ℝ} (heps : 0 < eps) (n : ℕ) : + Compatible (RealRooted.iterateTDeriv eps n f) + (RealRooted.iterateTDeriv eps n g) := by + intro α β hα hβ + rcases h α β hα hβ with hzero | hrr + · left + rw [← RealRooted.iterateTDeriv_linear_combo, hzero] + simp + · right + rw [← RealRooted.iterateTDeriv_linear_combo] + exact ⟨RealRooted.iterateTDeriv_ne_zero hrr.1, + RealRooted.splits_iterateTDeriv heps hrr.2⟩ + lemma isRealRooted_left {f g : ℝ[X]} (h : Compatible f g) (hf_pos : HasPosLeadingCoeff f) : (f ≠ 0 ∧ f.Splits) := by diff --git a/RealRooted/DegreeDropReversal.lean b/RealRooted/DegreeDropReversal.lean index 895cd2bb..25241097 100644 --- a/RealRooted/DegreeDropReversal.lean +++ b/RealRooted/DegreeDropReversal.lean @@ -296,6 +296,15 @@ theorem splits_reflect_iff {p : K[X]} {N : ℕ} (hN : p.natDegree ≤ N) : Polynomial.natDegree_reflect_le.trans <| by simp_all simpa using splits_reflect_of_splits h hreflect_deg +/-- Reflection sends a nonzero root to its inverse at any valid degree bound. -/ +theorem isRoot_reflect_inv_iff {p : K[X]} {b : K} (hb : b ≠ 0) + {N : ℕ} (hN : p.natDegree ≤ N) : + (reflect N p).IsRoot b⁻¹ ↔ p.IsRoot b := by + letI : Invertible b := invertibleOfNonzero hb + change eval b⁻¹ (reflect N p) = 0 ↔ eval b p = 0 + simpa [Polynomial.eval₂_id, invOf_eq_inv] using + (Polynomial.eval₂_reflect_eq_zero_iff (RingHom.id K) b N p hN) + /-- Reversal preserves and reflects splitting over a field. -/ theorem splits_reverse_iff {p : K[X]} : p.reverse.Splits ↔ p.Splits := by @@ -526,6 +535,26 @@ theorem card_roots_reverse_Ioi {p : K[X]} (hp : p.Splits) (h0 : p.coeff 0 ≠ 0) congrArg Multiset.card (Multiset.filter_congr (fun r _ => mem_Ioi_inv_iff ha)) +/-- Half-line root-count transport under reflection at a degree bound. -/ +theorem card_roots_reflect_Ioi {p : K[X]} (hp : p.Splits) (h0 : p.coeff 0 ≠ 0) + {N : ℕ} (hN : p.natDegree ≤ N) {a : K} (ha : 0 < a) : + ((reflect N p).roots.filter (fun x => a < x)).card = + (p.roots.filter (fun r => 0 < r ∧ r < a⁻¹)).card := by + have hpad : + Multiset.filter (fun x => a < x) + ((N - p.natDegree) • ({0} : Multiset K)) = 0 := by + rw [Multiset.filter_eq_nil] + intro x hx + rw [Multiset.mem_nsmul, Multiset.mem_singleton] at hx + grind + rw [reflect_eq_X_pow_mul_reverse p hN, + Polynomial.roots_mul + (mul_ne_zero (pow_ne_zero _ Polynomial.X_ne_zero) + (reverse_ne_zero_of_coeff_zero_ne h0)), + Multiset.filter_add, Multiset.card_add, Polynomial.roots_pow, + Polynomial.roots_X, card_roots_reverse_Ioi hp h0 ha, hpad, + Multiset.card_zero, zero_add] + /-- No-gap emptiness on a positive interval under reversal. -/ theorem card_roots_reverse_Ioo_eq_zero_iff {p : K[X]} (hp : p.Splits) (h0 : p.coeff 0 ≠ 0) {a b : K} (ha : 0 < a) (hb : 0 < b) : diff --git a/RealRooted/Derivative.lean b/RealRooted/Derivative.lean index 2895eb76..7fb69347 100644 --- a/RealRooted/Derivative.lean +++ b/RealRooted/Derivative.lean @@ -638,6 +638,69 @@ lemma mkInterleaving_sub_multiset (f : ℝ[X]) · -- a ≠ s, a ≠ r₁ grind +/-- The recursively selected witness is the penultimate entry of `ss`. +The product statement permits repeated entries and endpoint equality. -/ +private lemma exists_penultimate_listInterlaces_prod_nonneg : + ∀ {ss rs : List ℝ}, + ss.Pairwise (· ≤ ·) → + ListInterlaces ss rs → + 2 ≤ ss.length → + ∃ c ∈ ss, 0 ≤ (rs.map (c - ·)).prod := by + intro ss + induction ss with + | nil => + intro rs _ _ hlen + simp at hlen + | cons s ss ih => + cases ss with + | nil => + intro rs _ _ hlen + simp at hlen + | cons t ts => + intro rs hss hint _ + cases rs with + | nil => + simp [ListInterlaces] at hint + | cons r₁ rs => + cases rs with + | nil => + simp [ListInterlaces] at hint + | cons r₂ rest => + obtain ⟨hr₁s, hsr₂, htail⟩ := hint + by_cases hts : ts = [] + · subst ts + have hrest_len : rest.length = 1 := by + simpa using + (listInterlaces_cons_length_eq htail).symm + obtain ⟨r₃, rfl⟩ := + List.length_eq_one_iff.mp hrest_len + change r₂ ≤ t ∧ t ≤ r₃ ∧ True at htail + obtain ⟨hr₂t, htr₃, _⟩ := htail + refine ⟨s, by simp, ?_⟩ + have h₁ : 0 ≤ s - r₁ := + sub_nonneg.mpr hr₁s + have h₂ : s - r₂ ≤ 0 := + sub_nonpos.mpr hsr₂ + have h₃ : s - r₃ ≤ 0 := + sub_nonpos.mpr + (hsr₂.trans (hr₂t.trans htr₃)) + simpa [mul_assoc] using + mul_nonneg h₁ + (mul_nonneg_of_nonpos_of_nonpos h₂ h₃) + · have htail_len : 2 ≤ (t :: ts).length := by + grind + have hss_cons := List.pairwise_cons.mp hss + obtain ⟨c, hc, hcprod⟩ := + ih hss_cons.2 htail htail_len + have hsc : s ≤ c := + hss_cons.1 c hc + have hr₁c : r₁ ≤ c := + hr₁s.trans hsc + refine + ⟨c, List.mem_cons_of_mem s hc, ?_⟩ + simpa [List.map, List.prod_cons] using + mul_nonneg (sub_nonneg.mpr hr₁c) hcprod + /-! ## Main theorem -/ /-- **Derivative interlacing**: if `f` is real-rooted of degree ≥ 2, @@ -687,6 +750,40 @@ theorem derivative_interlaces {f : ℝ[X]} (hf : f.Splits) (hdeg : 2 ≤ f.natDe exact ⟨⟨by rintro rfl; simp at hf'_ne, hf⟩, hf'_rr, by rw [f.natDegree_derivative]; lia, rs, ss, hrs_sorted, hss_sorted, hrs_multiset, hss_eq, hss_interlaces⟩ +/-- A positive-leading splitting polynomial of degree at least four is +nonnegative at the penultimate derivative-root occurrence. + +Repeated roots are retained: if the selected derivative root is also a root +of `p`, the conclusion is equality. -/ +theorem exists_derivative_root_eval_nonneg_of_four_le_natDegree + {p : ℝ[X]} (hp : p.Splits) (hp_pos : HasPosLeadingCoeff p) + (hdeg : 4 ≤ p.natDegree) : + ∃ c ∈ p.derivative.roots, 0 ≤ p.eval c := by + obtain + ⟨_, hpd, _, rs, ss, _, hss_sorted, hrs_eq, hss_eq, hint⟩ := + derivative_interlaces hp (by lia) + have hss_length : ss.length = p.derivative.natDegree := by + calc + ss.length = (↑ss : Multiset ℝ).card := by simp + _ = p.derivative.roots.card := congrArg Multiset.card hss_eq + _ = p.derivative.natDegree := card_roots_of_splits hpd.2 + have hss_two : 2 ≤ ss.length := by + rw [hss_length, p.natDegree_derivative] + lia + obtain ⟨c, hc, hcprod⟩ := + exists_penultimate_listInterlaces_prod_nonneg + hss_sorted hint hss_two + have hc_roots : c ∈ p.derivative.roots := by + rw [← hss_eq] + exact Multiset.mem_coe.mpr hc + refine ⟨c, hc_roots, ?_⟩ + have heval : + p.eval c = p.leadingCoeff * (rs.map (c - ·)).prod := by + rw [hp.eval_eq_prod_roots c, ← hrs_eq] + rfl + rw [heval] + exact mul_nonneg hp_pos.le hcprod + /-- A nonzero degree-zero real-rooted polynomial precedes a nonzero degree-one real-rooted polynomial. -/ lemma prec_degree_zero_right_of_degree_one diff --git a/RealRooted/DerivativeShiftRootMatching.lean b/RealRooted/DerivativeShiftRootMatching.lean new file mode 100644 index 00000000..c7ce40b0 --- /dev/null +++ b/RealRooted/DerivativeShiftRootMatching.lean @@ -0,0 +1,60 @@ +import RealRooted.IteratedDerivativeShift +import RealRooted.RootMultiplicityMatching +import RealRooted.SameDegreeMultiplicityLowerCount + +/-! +# Root matching for derivative shifts + +This module combines coefficient continuity of `TDeriv` with the +multiplicity-aware finite matching API. It provides the root transport needed +when derivative shifts are used to regularize a compatible polynomial pair. +-/ + +open Polynomial + +noncomputable section + +namespace RealRooted + +/-- For every positive radius, all roots of a sufficiently small positive +`TDeriv` shift can be matched, with multiplicity, to roots of the original +splitting polynomial within that radius. -/ +theorem exists_delta_roots_rel_TDeriv + {p : ℝ[X]} (hp : p.Splits) {ρ : ℝ} (hρ : 0 < ρ) : + ∃ δ > 0, ∀ ⦃eps : ℝ⦄, 0 < eps → eps < δ → + Multiset.Rel (fun r q ↦ |q - r| < ρ) p.roots (TDeriv eps p).roots := by + obtain ⟨η, hη_pos, hηρ, hsep⟩ := + Multiset.exists_pos_lt_and_two_mul_le_abs_sub_toFinset p.roots hρ + have hshift (nu : ℝ) : + p + C nu * (-p.derivative) = TDeriv nu p := by + simp only [TDeriv, sub_eq_add_neg, mul_neg] + have hp0 : (p + C (0 : ℝ) * (-p.derivative)).Splits := by + simpa using hp + obtain ⟨δ, hδ_pos, hlocal⟩ := + exists_eps_forall_root_count_le_card_filter_near + (f := p) (g := -p.derivative) (μ0 := 0) hp0 η hη_pos + refine ⟨δ, hδ_pos, ?_⟩ + intro eps heps_pos hepsδ + have heps_abs : |eps - 0| < δ := by + simpa [abs_of_pos heps_pos] using hepsδ + have hsplit : (p + C eps * (-p.derivative)).Splits := by + rw [hshift] + exact splits_tderiv heps_pos hp + have hdeg : + (p + C eps * (-p.derivative)).natDegree = + (p + C (0 : ℝ) * (-p.derivative)).natDegree := by + rw [hshift eps, hshift 0, natDegree_TDeriv, natDegree_TDeriv] + have hcount := hlocal eps heps_abs hsplit hdeg + rw [hshift eps, hshift 0] at hcount + have hcount' : ∀ a ∈ p.roots.toFinset, + p.roots.count a ≤ + ((TDeriv eps p).roots.filter (fun q ↦ |q - a| < η)).card := by + simpa [TDeriv] using hcount + have hcard : (TDeriv eps p).roots.card = p.roots.card := by + rw [card_roots_of_splits (splits_tderiv heps_pos hp), natDegree_TDeriv, + card_roots_of_splits hp] + have hrel := + Multiset.rel_of_forall_le_count_of_card_eq hsep hcount' hcard + exact hrel.mono fun _ _ _ _ hclose ↦ lt_trans hclose hηρ + +end RealRooted diff --git a/RealRooted/DerivativeShiftSequence.lean b/RealRooted/DerivativeShiftSequence.lean new file mode 100644 index 00000000..10f561f0 --- /dev/null +++ b/RealRooted/DerivativeShiftSequence.lean @@ -0,0 +1,120 @@ +import RealRooted.IteratedDerivativeShift + +/-! +# Finite sequences of derivative shifts + +This file extends the fixed-parameter iteration of `TDeriv` to a finite list of +possibly different positive parameters. The varying-parameter form is needed +when each derivative shift must satisfy a new local smallness bound. + +The main result is `Polynomial.hasSimpleRoots_applyTDerivList_of_natDegree_le_length`: +after at least `p.natDegree` positive shifts, a nonzero splitting polynomial has +simple roots. Its proof follows the multiplicity descent used for fixed +iterations, tracing a hypothetical multiple root backward through the list. +-/ + +open RealRooted + +namespace Polynomial + +noncomputable section + +/-- Apply the derivative shifts in `epss` from left to right. -/ +def applyTDerivList : List ℝ → ℝ[X] → ℝ[X] + | [], p => p + | eps :: epss, p => applyTDerivList epss (TDeriv eps p) + +@[simp] +theorem applyTDerivList_nil (p : ℝ[X]) : applyTDerivList [] p = p := rfl + +@[simp] +theorem applyTDerivList_cons (eps : ℝ) (epss : List ℝ) (p : ℝ[X]) : + applyTDerivList (eps :: epss) p = applyTDerivList epss (TDeriv eps p) := rfl + +/-- A finite sequence of derivative shifts preserves nonvanishing. -/ +theorem applyTDerivList_ne_zero {epss : List ℝ} {p : ℝ[X]} (hp : p ≠ 0) : + applyTDerivList epss p ≠ 0 := by + induction epss generalizing p with + | nil => simpa + | cons eps epss ih => + simpa using ih (TDeriv_ne_zero hp) + +/-- Positive derivative shifts preserve splitting throughout a finite sequence. -/ +theorem Splits.applyTDerivList {epss : List ℝ} {p : ℝ[X]} + (hp : p.Splits) (hpos : ∀ eps ∈ epss, 0 < eps) : + (applyTDerivList epss p).Splits := by + induction epss generalizing p with + | nil => simpa + | cons eps epss ih => + have heps : 0 < eps := hpos eps (by simp) + have htail : ∀ eta ∈ epss, 0 < eta := + fun eta heta ↦ hpos eta (List.mem_cons_of_mem eps heta) + exact ih (splits_tderiv heps hp) htail + +/-- A finite sequence of derivative shifts preserves natural degree. -/ +@[simp] +theorem natDegree_applyTDerivList (epss : List ℝ) (p : ℝ[X]) : + (applyTDerivList epss p).natDegree = p.natDegree := by + induction epss generalizing p with + | nil => simp + | cons eps epss ih => + rw [applyTDerivList_cons, ih, natDegree_TDeriv] + +/-- A finite sequence of derivative shifts preserves the leading coefficient. -/ +@[simp] +theorem leadingCoeff_applyTDerivList (epss : List ℝ) (p : ℝ[X]) : + (applyTDerivList epss p).leadingCoeff = p.leadingCoeff := by + induction epss generalizing p with + | nil => simp + | cons eps epss ih => + rw [applyTDerivList_cons, ih, leadingCoeff_TDeriv] + +/-- A multiple final root gains one unit of multiplicity at every backward step. -/ +theorem rootMultiplicity_applyTDerivList_eq_add_length_of_ge_two + {epss : List ℝ} {p : ℝ[X]} {a : ℝ} + (hpos : ∀ eps ∈ epss, 0 < eps) (hp : p.Splits) + (hm : 2 ≤ (applyTDerivList epss p).rootMultiplicity a) : + p.rootMultiplicity a = + (applyTDerivList epss p).rootMultiplicity a + epss.length := by + induction epss generalizing p with + | nil => simp + | cons eps epss ih => + have heps : 0 < eps := hpos eps (by simp) + have htail : ∀ eta ∈ epss, 0 < eta := + fun eta heta ↦ hpos eta (List.mem_cons_of_mem eps heta) + have hTsplit : (TDeriv eps p).Splits := splits_tderiv heps hp + have htail_eq := ih htail hTsplit hm + have hm' : + 2 ≤ (applyTDerivList epss (TDeriv eps p)).rootMultiplicity a := by + simpa only [applyTDerivList_cons] using hm + have hTmult : 2 ≤ (TDeriv eps p).rootMultiplicity a := by + rw [htail_eq] + exact le_trans hm' (Nat.le_add_right _ _) + have hstep := rootMultiplicity_eq_succ_of_TDeriv_ge_two heps hp hTmult + simp only [applyTDerivList_cons, List.length_cons] + lia + +/-- Enough positive derivative shifts make every root simple. -/ +theorem hasSimpleRoots_applyTDerivList_of_natDegree_le_length + {epss : List ℝ} {p : ℝ[X]} (hpos : ∀ eps ∈ epss, 0 < eps) + (hp : p ≠ 0) (hsplit : p.Splits) (hdeg : p.natDegree ≤ epss.length) : + HasSimpleRoots (applyTDerivList epss p) := by + intro a ha + have hfinal_ne : applyTDerivList epss p ≠ 0 := applyTDerivList_ne_zero hp + have hmult_pos : 0 < (applyTDerivList epss p).rootMultiplicity a := + (rootMultiplicity_pos hfinal_ne).mpr ha + by_contra hne + have hmult : 2 ≤ (applyTDerivList epss p).rootMultiplicity a := by + lia + have hback := + rootMultiplicity_applyTDerivList_eq_add_length_of_ge_two hpos hsplit hmult + have hmult_le : p.rootMultiplicity a ≤ p.natDegree := by + calc + p.rootMultiplicity a = p.roots.count a := (count_roots p).symm + _ ≤ p.roots.card := p.roots.count_le_card a + _ ≤ p.natDegree := card_roots' p + lia + +end + +end Polynomial diff --git a/RealRooted/IteratedDerivativeShift.lean b/RealRooted/IteratedDerivativeShift.lean index 881223c9..4f120a25 100644 --- a/RealRooted/IteratedDerivativeShift.lean +++ b/RealRooted/IteratedDerivativeShift.lean @@ -343,6 +343,11 @@ lemma iterateTDeriv_C_mul (eps c : ℝ) : rw [iterateTDeriv_succ, iterateTDeriv_succ, iterateTDeriv_C_mul] exact TDeriv_C_mul eps c _ +lemma iterateTDeriv_linear_combo (eps α β : ℝ) (n : ℕ) (f g : ℝ[X]) : + iterateTDeriv eps n (C α * f + C β * g) = + C α * iterateTDeriv eps n f + C β * iterateTDeriv eps n g := by + rw [iterateTDeriv_add, iterateTDeriv_C_mul, iterateTDeriv_C_mul] + private lemma TDeriv_X_sub_C (eps r : ℝ) : TDeriv eps (X - C r) = X - C (r + eps) := by simp [TDeriv] diff --git a/RealRooted/Linear.lean b/RealRooted/Linear.lean index 3ef7cdd5..e93fd8dc 100644 --- a/RealRooted/Linear.lean +++ b/RealRooted/Linear.lean @@ -298,6 +298,17 @@ lemma roots_comp_X_add_C {p : ℝ[X]} (r : ℝ) : (Multiset.count_map_eq_count' (fun y : ℝ => y - r) p.roots (fun a b hab => by simp_all) (x + r)).symm +/-- Translating a polynomial by `a` identifies its roots in `(0, b - a)` +with the original roots in `(a, b)`, including multiplicities. -/ +lemma card_roots_comp_X_add_C_Ioo (p : ℝ[X]) (a b : ℝ) : + ((p.comp (X + C a)).roots.filter (fun x => 0 < x ∧ x < b - a)).card = + (p.roots.filter (fun x => a < x ∧ x < b)).card := by + rw [roots_comp_X_add_C, Multiset.filter_map, Multiset.card_map] + congr 1 + apply Multiset.filter_congr + intro y _ + constructor <;> intro h <;> constructor <;> linarith [h.1, h.2] + /-- Translation by `r` preserves positive leading coefficient. -/ lemma HasPosLeadingCoeff.comp_X_add_C {p : ℝ[X]} (hp : HasPosLeadingCoeff p) (r : ℝ) : diff --git a/RealRooted/LiuOppositeSigns/BoundedIntervalContinuity.lean b/RealRooted/LiuOppositeSigns/BoundedIntervalContinuity.lean new file mode 100644 index 00000000..107129fa --- /dev/null +++ b/RealRooted/LiuOppositeSigns/BoundedIntervalContinuity.lean @@ -0,0 +1,103 @@ +import RealRooted.LiuOppositeSigns.Theorem21Statements +import RealRooted.ReflectedRootCountLocalConstancy + +/-! +# Liu's bounded-interval continuity argument + +This module implements the continuity step in the forward direction of Liu's +Theorem 2.1. A same-owned combined-root gap is followed from the endpoint +polynomial that is root-free on the closed gap. Fixed-degree reflection lets +the root count stay constant even when the original affine pencil drops degree. +-/ + +open Polynomial + +namespace RealRooted + +private theorem false_of_rightFamily_root_of_boundedIntervalContinuity + {p q : ℝ[X]} {a b x μ : ℝ} (hax : a < x) (hxb : x < b) (hμ : 0 < μ) + (hp_no : ∀ z : ℝ, a < z → z < b → ¬ p.IsRoot z) + (ha_no : ∀ η ∈ Set.Icc (0 : ℝ) μ, ¬ (p + C η * q).IsRoot a) + (hsplit : ∀ η ∈ Set.Icc (0 : ℝ) μ, (p + C η * q).Splits) + (hb_no : ∀ η ∈ Set.Icc (0 : ℝ) μ, ¬ (p + C η * q).IsRoot b) + (hxroot : (p + C μ * q).IsRoot x) : False := by + have hcount := rightFamily_card_roots_Ioo_eq_zero_param + (f := p) (g := q) (lt_trans hax hxb) hμ ha_no hsplit hb_no + have hp_card_zero : (p.roots.filter (fun r ↦ a < r ∧ r < b)).card = 0 := by + rw [Multiset.card_eq_zero, Multiset.filter_eq_nil] + intro z hz hzab + exact hp_no z hzab.1 hzab.2 (Polynomial.isRoot_of_mem_roots hz) + have hfamily_card_zero : + ((p + C μ * q).roots.filter (fun r ↦ a < r ∧ r < b)).card = 0 := + hcount.trans hp_card_zero + have hμ_mem : μ ∈ Set.Icc (0 : ℝ) μ := ⟨hμ.le, le_rfl⟩ + have hfamily_ne : p + C μ * q ≠ 0 := by + intro hzero + apply ha_no μ hμ_mem + simp [hzero, Polynomial.IsRoot.def] + have hx_mem : x ∈ (p + C μ * q).roots := + (Polynomial.mem_roots hfamily_ne).mpr hxroot + have hx_filter : x ∈ (p + C μ * q).roots.filter (fun r ↦ a < r ∧ r < b) := + Multiset.mem_filter.mpr ⟨hx_mem, hax, hxb⟩ + have hfilter_zero : + (p + C μ * q).roots.filter (fun r ↦ a < r ∧ r < b) = 0 := + Multiset.card_eq_zero.mp hfamily_card_zero + rw [hfilter_zero] at hx_filter + simp at hx_filter + +/-- Liu's bounded-interval continuity argument forces every parity-relevant +finite combined-root gap to have endpoints owned by opposite polynomials. -/ +theorem LiuOppositeSigns.OppositeLeadingSigns.crossOwnedNotOddGaps_of_boundedIntervalContinuity + {f g : ℝ[X]} (hsgn : OppositeLeadingSigns f g) + (hfg : PosComboRealRooted f g) (hno : NoCommonRoots f g) + (hf : f.Splits) (hg : g.Splits) : + CrossOwnedNotOddGaps f g := by + intro a b x hax hxb ha_root hb_root hgap hnot_odd + have hf_no : ∀ z : ℝ, a < z → z < b → ¬ f.IsRoot z := + fun z haz hzb ↦ (hgap z haz hzb).1 + have hg_no : ∀ z : ℝ, a < z → z < b → ¬ g.IsRoot z := + fun z haz hzb ↦ (hgap z haz hzb).2 + obtain ⟨μ, hμ_pos, hμ_root, _⟩ := + hsgn.exists_unique_pos_crossing_add_right_of_not_odd_intCard_roots_gt_sub + hfg hno hf hg (hf_no x hax hxb) (hg_no x hax hxb) hnot_odd + rcases ha_root with hfa | hga + · rcases hb_root with hfb | hgb + · exact False.elim <| false_of_rightFamily_root_of_boundedIntervalContinuity + (p := g) (q := f) hax hxb (inv_pos.mpr hμ_pos) hg_no + (fun _ _ ↦ hno.symm.rightFamily_not_isRoot_of_right_root hfa) + (fun _ hη ↦ PosComboRealRooted.splits_add_right_of_nonneg + (PosComboRealRooted.comm hfg) hg hη.1) + (fun _ _ ↦ hno.symm.rightFamily_not_isRoot_of_right_root hfb) + ((add_right_isRoot_iff_add_left_inv hμ_pos.ne').mp hμ_root) + · exact Or.inl ⟨hfa, hgb⟩ + · rcases hb_root with hfb | hgb + · exact Or.inr ⟨hga, hfb⟩ + · exact False.elim <| false_of_rightFamily_root_of_boundedIntervalContinuity + (p := f) (q := g) hax hxb hμ_pos hf_no + (fun _ _ ↦ hno.rightFamily_not_isRoot_of_right_root hga) + (fun _ hη ↦ PosComboRealRooted.splits_add_right_of_nonneg hfg hf hη.1) + (fun _ _ ↦ hno.rightFamily_not_isRoot_of_right_root hgb) hμ_root + +/-- Liu's forward implication in the no-common, nonconstant, simple-root regime. + +This is the rigorous part of the reduction used in the proof of Theorem 2.1: +compatibility supplies positive-combination real-rootedness, bounded root-count +continuity rules out same-owner odd gaps, and the finite descent gives the Liu +branch. The paper's assertion that no common zeros imply simple zeros is false +without an additional perturbation argument, so simplicity remains explicit +here rather than being inferred from `hno`. -/ +theorem LiuOppositeSigns.theorem21RootCountBranches_of_compatible_noCommon_nonconstant_of_simple + {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits) + (hsgn : OppositeLeadingSigns f g) (hno : NoCommonRoots f g) + (hf_deg : f.natDegree ≠ 0) (hg_deg : g.natDegree ≠ 0) + (hsimple_f : HasSimpleRoots f) (hsimple_g : HasSimpleRoots g) + (hcompat : Compatible f g) : + theorem21RootCountBranches f g := by + have hfg : PosComboRealRooted f g := + posComboRealRooted_of_compatible_noCommon_nonconstant + hcompat hno hg hg_deg + exact theorem21RootCountBranches_of_crossOwned hsgn hf hg + hf_deg hg_deg hsimple_f hsimple_g hno + (hsgn.crossOwnedNotOddGaps_of_boundedIntervalContinuity hfg hno hf hg) + +end RealRooted diff --git a/RealRooted/LiuOppositeSigns/DerivativeShiftRegularization.lean b/RealRooted/LiuOppositeSigns/DerivativeShiftRegularization.lean new file mode 100644 index 00000000..2f720e8d --- /dev/null +++ b/RealRooted/LiuOppositeSigns/DerivativeShiftRegularization.lean @@ -0,0 +1,67 @@ +import RealRooted.DerivativeShiftRootMatching +import RealRooted.LiuOppositeSigns.Theorem21Statements + +/-! +# Derivative-shift regularization for Liu pairs + +This module proves that sufficiently small common positive derivative shifts +preserve the no-common-root condition used in Liu's finite root-count descent. +-/ + +open Polynomial + +noncomputable section + +namespace RealRooted +namespace LiuOppositeSigns + +/-- A common positive `TDeriv` shift of two nonzero splitting polynomials with +no common roots still has no common roots when the shift is sufficiently +small. -/ +theorem NoCommonRoots.exists_delta_TDeriv + {f g : ℝ[X]} (hno : NoCommonRoots f g) + (hf_ne : f ≠ 0) (hg_ne : g ≠ 0) (hf : f.Splits) (hg : g.Splits) : + ∃ δ > 0, ∀ ⦃eps : ℝ⦄, 0 < eps → eps < δ → + NoCommonRoots (TDeriv eps f) (TDeriv eps g) := by + obtain ⟨η, hη_pos, _, hsep⟩ := + Multiset.exists_pos_lt_and_two_mul_le_abs_sub_toFinset + (f.roots + g.roots) zero_lt_one + obtain ⟨δf, hδf_pos, hfrel⟩ := + exists_delta_roots_rel_TDeriv hf hη_pos + obtain ⟨δg, hδg_pos, hgrel⟩ := + exists_delta_roots_rel_TDeriv hg hη_pos + refine ⟨min δf δg, lt_min hδf_pos hδg_pos, ?_⟩ + intro eps heps_pos hepsδ x hfx hgx + obtain ⟨a, ha_mem, hax⟩ := by + simpa only [Function.flip_def] using + Multiset.exists_mem_of_rel_of_mem + ((Multiset.rel_flip).2 + (hfrel heps_pos (hepsδ.trans_le (min_le_left _ _)))) + ((Polynomial.mem_roots (TDeriv_ne_zero hf_ne)).mpr hfx) + obtain ⟨b, hb_mem, hbx⟩ := by + simpa only [Function.flip_def] using + Multiset.exists_mem_of_rel_of_mem + ((Multiset.rel_flip).2 + (hgrel heps_pos (hepsδ.trans_le (min_le_right _ _)))) + ((Polynomial.mem_roots (TDeriv_ne_zero hg_ne)).mpr hgx) + have hab_ne : a ≠ b := by + rintro rfl + exact (hno a ((Polynomial.mem_roots hf_ne).mp ha_mem)) + ((Polynomial.mem_roots hg_ne).mp hb_mem) + have ha_sum : a ∈ (f.roots + g.roots).toFinset := by + simp [ha_mem] + have hb_sum : b ∈ (f.roots + g.roots).toFinset := by + simp [hb_mem] + have hab_sep : 2 * η ≤ |a - b| := + hsep a ha_sum b hb_sum hab_ne + have hab_lt : |a - b| < 2 * η := by + calc + |a - b| ≤ |a - x| + |x - b| := by + simpa only [sub_add_sub_cancel] using + abs_add_le (a - x) (x - b) + _ = |x - a| + |x - b| := by rw [abs_sub_comm a x] + _ < 2 * η := by linarith + exact (not_lt_of_ge hab_sep) hab_lt + +end LiuOppositeSigns +end RealRooted diff --git a/RealRooted/LiuOppositeSigns/DerivativeShiftSequenceRegularization.lean b/RealRooted/LiuOppositeSigns/DerivativeShiftSequenceRegularization.lean new file mode 100644 index 00000000..06dd948e --- /dev/null +++ b/RealRooted/LiuOppositeSigns/DerivativeShiftSequenceRegularization.lean @@ -0,0 +1,214 @@ +import RealRooted.Compatibility.Basic +import RealRooted.DerivativeShiftSequence +import RealRooted.LiuOppositeSigns.DerivativeShiftRegularization +import RealRooted.Mathlib.Data.Multiset.Rel + +/-! +# Finite derivative-shift regularization for Liu's opposite-sign theorem + +Liu's source proof reduces to endpoints with no common zeros and then treats +those endpoints as if all zeros were simple. That implication is false for +individual endpoints. The theorems below provide the required rigorous +replacement: repeatedly apply a common positive derivative shift, choosing a +new sufficiently small parameter at each stage. + +Every parameter can additionally be bounded by an arbitrary `κ > 0`. This +quantitative bound is retained for the later limiting argument rather than +merely producing one unrelated pair with simple roots. +-/ + +namespace RealRooted +namespace LiuOppositeSigns + +open Polynomial + +noncomputable section + +/-- Choose a prescribed number of bounded positive common derivative shifts. + +At every stage, the next shift is smaller than both `κ` and the local radius +from `NoCommonRoots.exists_delta_TDeriv`. Consequently compatibility and the +absence of common roots survive the entire sequence. +-/ +theorem NoCommonRoots.exists_applyTDerivList + {f g : ℝ[X]} (hcomp : Compatible f g) (hno : NoCommonRoots f g) + (hf_ne : f ≠ 0) (hg_ne : g ≠ 0) (hf : f.Splits) (hg : g.Splits) + {κ : ℝ} (hκ : 0 < κ) (n : ℕ) : + ∃ epss : List ℝ, + epss.length = n ∧ + (∀ eps ∈ epss, 0 < eps ∧ eps < κ) ∧ + Compatible (applyTDerivList epss f) (applyTDerivList epss g) ∧ + NoCommonRoots (applyTDerivList epss f) (applyTDerivList epss g) := by + induction n generalizing f g with + | zero => + exact ⟨[], rfl, by simp, by simpa using hcomp, by simpa using hno⟩ + | succ n ih => + obtain ⟨δ, hδ, hpreserve⟩ := + hno.exists_delta_TDeriv hf_ne hg_ne hf hg + let eps := min δ κ / 2 + have hmin : 0 < min δ κ := lt_min hδ hκ + have heps : 0 < eps := by + dsimp [eps] + linarith + have heps_delta : eps < δ := by + have hle : min δ κ ≤ δ := min_le_left δ κ + dsimp [eps] + linarith + have heps_kappa : eps < κ := by + have hle : min δ κ ≤ κ := min_le_right δ κ + dsimp [eps] + linarith + have hcomp_shift : Compatible (TDeriv eps f) (TDeriv eps g) := by + simpa using hcomp.iterateTDeriv heps 1 + have hno_shift : NoCommonRoots (TDeriv eps f) (TDeriv eps g) := + hpreserve heps heps_delta + obtain ⟨epss, hlength, hbounds, hcomp_final, hno_final⟩ := + ih hcomp_shift hno_shift (TDeriv_ne_zero hf_ne) (TDeriv_ne_zero hg_ne) + (splits_tderiv heps hf) (splits_tderiv heps hg) + refine ⟨eps :: epss, by simp [hlength], ?_, ?_, ?_⟩ + · intro eta heta + rcases List.mem_cons.mp heta with rfl | heta + · exact ⟨heps, heps_kappa⟩ + · exact hbounds eta heta + · simpa using hcomp_final + · simpa using hno_final + +/-- Choose bounded common shifts whose final roots stay uniformly close to the originals. -/ +theorem NoCommonRoots.exists_applyTDerivList_roots_rel + {f g : ℝ[X]} (hcomp : Compatible f g) (hno : NoCommonRoots f g) + (hf_ne : f ≠ 0) (hg_ne : g ≠ 0) (hf : f.Splits) (hg : g.Splits) + {κ ρ : ℝ} (hκ : 0 < κ) (hρ : 0 < ρ) (n : ℕ) : + ∃ epss : List ℝ, + epss.length = n ∧ + (∀ eps ∈ epss, 0 < eps ∧ eps < κ) ∧ + Compatible (applyTDerivList epss f) (applyTDerivList epss g) ∧ + NoCommonRoots (applyTDerivList epss f) (applyTDerivList epss g) ∧ + Multiset.Rel (fun r q ↦ |q - r| < ρ) + f.roots (applyTDerivList epss f).roots ∧ + Multiset.Rel (fun r q ↦ |q - r| < ρ) + g.roots (applyTDerivList epss g).roots := by + induction n generalizing f g ρ with + | zero => + refine ⟨[], rfl, by simp, by simpa using hcomp, by simpa using hno, ?_, ?_⟩ + · apply Multiset.rel_refl_of_refl_on + intro r hr + simpa using hρ + · apply Multiset.rel_refl_of_refl_on + intro r hr + simpa using hρ + | succ n ih => + have hhalf : 0 < ρ / 2 := by linarith + obtain ⟨δno, hδno, hpreserve⟩ := + hno.exists_delta_TDeriv hf_ne hg_ne hf hg + obtain ⟨δf, hδf, hfclose⟩ := + exists_delta_roots_rel_TDeriv hf hhalf + obtain ⟨δg, hδg, hgclose⟩ := + exists_delta_roots_rel_TDeriv hg hhalf + let δ := min δno (min δf (min δg κ)) + have hδ : 0 < δ := lt_min hδno (lt_min hδf (lt_min hδg hκ)) + have hδ_no : δ ≤ δno := min_le_left _ _ + have hδ_tail : δ ≤ min δf (min δg κ) := min_le_right _ _ + have hδ_f : δ ≤ δf := hδ_tail.trans (min_le_left _ _) + have hδ_g : δ ≤ δg := + hδ_tail.trans ((min_le_right _ _).trans (min_le_left _ _)) + have hδ_kappa : δ ≤ κ := + hδ_tail.trans ((min_le_right _ _).trans (min_le_right _ _)) + let eps := δ / 2 + have heps : 0 < eps := by + dsimp [eps] + linarith + have heps_no : eps < δno := by + dsimp [eps] + linarith + have heps_f : eps < δf := by + dsimp [eps] + linarith + have heps_g : eps < δg := by + dsimp [eps] + linarith + have heps_kappa : eps < κ := by + dsimp [eps] + linarith + have hcomp_shift : Compatible (TDeriv eps f) (TDeriv eps g) := by + simpa using hcomp.iterateTDeriv heps 1 + have hno_shift : NoCommonRoots (TDeriv eps f) (TDeriv eps g) := + hpreserve heps heps_no + have hf_step := hfclose heps heps_f + have hg_step := hgclose heps heps_g + obtain ⟨epss, hlength, hbounds, hcomp_final, hno_final, + hf_tail, hg_tail⟩ := + ih hcomp_shift hno_shift (TDeriv_ne_zero hf_ne) (TDeriv_ne_zero hg_ne) + (splits_tderiv heps hf) (splits_tderiv heps hg) hhalf + have hf_final := Multiset.Rel.comp + (fun a b c hab hbc => by + calc + |c - a| = |(c - b) + (b - a)| := by ring_nf + _ ≤ |c - b| + |b - a| := abs_add_le _ _ + _ < ρ / 2 + ρ / 2 := add_lt_add hbc hab + _ = ρ := by ring) + hf_step hf_tail + have hg_final := Multiset.Rel.comp + (fun a b c hab hbc => by + calc + |c - a| = |(c - b) + (b - a)| := by ring_nf + _ ≤ |c - b| + |b - a| := abs_add_le _ _ + _ < ρ / 2 + ρ / 2 := add_lt_add hbc hab + _ = ρ := by ring) + hg_step hg_tail + refine ⟨eps :: epss, by simp [hlength], ?_, ?_, ?_, ?_, ?_⟩ + · intro eta heta + rcases List.mem_cons.mp heta with rfl | heta + · exact ⟨heps, heps_kappa⟩ + · exact hbounds eta heta + · simpa using hcomp_final + · simpa using hno_final + · simpa using hf_final + · simpa using hg_final + +/-- Bounded common shifts regularize both endpoints while preserving all Liu hypotheses. -/ +theorem NoCommonRoots.exists_simple_applyTDerivList + {f g : ℝ[X]} (hcomp : Compatible f g) (hno : NoCommonRoots f g) + (hf_ne : f ≠ 0) (hg_ne : g ≠ 0) (hf : f.Splits) (hg : g.Splits) + (hopp : f.leadingCoeff * g.leadingCoeff < 0) {κ : ℝ} (hκ : 0 < κ) : + ∃ epss : List ℝ, + epss.length = max f.natDegree g.natDegree ∧ + (∀ eps ∈ epss, 0 < eps ∧ eps < κ) ∧ + Compatible (applyTDerivList epss f) (applyTDerivList epss g) ∧ + NoCommonRoots (applyTDerivList epss f) (applyTDerivList epss g) ∧ + applyTDerivList epss f ≠ 0 ∧ + applyTDerivList epss g ≠ 0 ∧ + (applyTDerivList epss f).Splits ∧ + (applyTDerivList epss g).Splits ∧ + (applyTDerivList epss f).natDegree = f.natDegree ∧ + (applyTDerivList epss g).natDegree = g.natDegree ∧ + (applyTDerivList epss f).leadingCoeff = f.leadingCoeff ∧ + (applyTDerivList epss g).leadingCoeff = g.leadingCoeff ∧ + (applyTDerivList epss f).leadingCoeff * + (applyTDerivList epss g).leadingCoeff < 0 ∧ + HasSimpleRoots (applyTDerivList epss f) ∧ + HasSimpleRoots (applyTDerivList epss g) := by + obtain ⟨epss, hlength, hbounds, hcomp_final, hno_final⟩ := + hno.exists_applyTDerivList hcomp hf_ne hg_ne hf hg hκ + (max f.natDegree g.natDegree) + have hpos : ∀ eps ∈ epss, 0 < eps := by + intro eps heps + exact (hbounds eps heps).1 + have hf_simple : HasSimpleRoots (applyTDerivList epss f) := by + apply hasSimpleRoots_applyTDerivList_of_natDegree_le_length hpos hf_ne hf + rw [hlength] + exact Nat.le_max_left _ _ + have hg_simple : HasSimpleRoots (applyTDerivList epss g) := by + apply hasSimpleRoots_applyTDerivList_of_natDegree_le_length hpos hg_ne hg + rw [hlength] + exact Nat.le_max_right _ _ + refine ⟨epss, hlength, hbounds, hcomp_final, hno_final, + applyTDerivList_ne_zero hf_ne, applyTDerivList_ne_zero hg_ne, + hf.applyTDerivList hpos, hg.applyTDerivList hpos, by simp, by simp, + by simp, by simp, ?_, hf_simple, hg_simple⟩ + simpa using hopp + +end + + +end LiuOppositeSigns +end RealRooted diff --git a/RealRooted/LiuOppositeSigns/RootCountClosure.lean b/RealRooted/LiuOppositeSigns/RootCountClosure.lean new file mode 100644 index 00000000..2825d1cb --- /dev/null +++ b/RealRooted/LiuOppositeSigns/RootCountClosure.lean @@ -0,0 +1,571 @@ +import RealRooted.CommonInterleaver.SameDegreeRootCount +import RealRooted.CommonInterleaver.RootCountCombinatorics +import RealRooted.LiuOppositeSigns.RootCountRelStability +import RealRooted.LiuOppositeSigns.Theorem21Statements +import RealRooted.RootMatchingSort + +/-! +# Closure of Liu root-count compatibility + +This file closes finite same-degree and successor-degree root inequalities +under arbitrarily small pointwise perturbations. It is the ordered-root limit +step used after derivative-shift regularization. +-/ + +namespace RealRooted +namespace LiuOppositeSigns + +open Polynomial + +private theorem abs_getD_sub_getD_lt_of_forall₂ + {xs ys : List ℝ} {ρ : ℝ} + (h : List.Forall₂ (fun x y : ℝ => |y - x| < ρ) xs ys) + {i : ℕ} (hxs : i < xs.length) (hys : i < ys.length) : + |ys.getD i 0 - xs.getD i 0| < ρ := by + rw [list_getD_eq_getElem_of_lt ys i 0 hys, + list_getD_eq_getElem_of_lt xs i 0 hxs] + exact h.get hxs hys + +/-- Same-degree root-count compatibility is closed under close finite crossings. -/ +theorem RootCountCompatible.of_forall_pos_exists_close_sameDegreeCrossing + {f g : ℝ[X]} (hf_ne : f ≠ 0) (hg_ne : g ≠ 0) + (hf : f.Splits) (hg : g.Splits) (hdeg : g.natDegree = f.natDegree) + (hclose : ∀ ρ : ℝ, 0 < ρ → + ∃ rf rg : List ℝ, + List.Forall₂ (fun x x' : ℝ => |x' - x| < ρ) (rootSeqDesc f) rf ∧ + List.Forall₂ (fun y y' : ℝ => |y' - y| < ρ) (rootSeqDesc g) rg ∧ + (∀ j, 1 ≤ j → j < f.natDegree → + rg.getD j 0 ≤ rf.getD (j - 1) 0) ∧ + (∀ j, 1 ≤ j → j < f.natDegree → + rf.getD j 0 ≤ rg.getD (j - 1) 0)) : + RootCountCompatible f g := by + have hcross : + (∀ j, 1 ≤ j → j < f.natDegree → + (rootSeqDesc g).getD j 0 ≤ + (rootSeqDesc f).getD (j - 1) 0) ∧ + (∀ j, 1 ≤ j → j < f.natDegree → + (rootSeqDesc f).getD j 0 ≤ + (rootSeqDesc g).getD (j - 1) 0) := by + constructor + · intro j hj1 hj + apply le_of_forall_pos_exists_close_le + intro ρ hρ + obtain ⟨rf, rg, hff, hgg, hfg⟩ := hclose ρ hρ + have hjg : j < (rootSeqDesc g).length := by + simpa only [rootSeqDesc_length hg, hdeg] using hj + have hjf : j - 1 < (rootSeqDesc f).length := by + rw [rootSeqDesc_length hf] + lia + have hjrg : j < rg.length := by simpa only [hgg.length_eq] using hjg + have hjrf : j - 1 < rf.length := by + simpa only [hff.length_eq] using hjf + exact ⟨rg.getD j 0, rf.getD (j - 1) 0, + abs_getD_sub_getD_lt_of_forall₂ hgg hjg hjrg, + abs_getD_sub_getD_lt_of_forall₂ hff hjf hjrf, + hfg.1 j hj1 hj⟩ + · intro j hj1 hj + apply le_of_forall_pos_exists_close_le + intro ρ hρ + obtain ⟨rf, rg, hff, hgg, hfg⟩ := hclose ρ hρ + have hjf : j < (rootSeqDesc f).length := by + simpa only [rootSeqDesc_length hf] using hj + have hjg : j - 1 < (rootSeqDesc g).length := by + rw [rootSeqDesc_length hg, hdeg] + lia + have hjrf : j < rf.length := by simpa only [hff.length_eq] using hjf + have hjrg : j - 1 < rg.length := by + simpa only [hgg.length_eq] using hjg + exact ⟨rf.getD j 0, rg.getD (j - 1) 0, + abs_getD_sub_getD_lt_of_forall₂ hff hjf hjrf, + abs_getD_sub_getD_lt_of_forall₂ hgg hjg hjrg, + hfg.2 j hj1 hj⟩ + have hlower := sameDegreeRootCount_of_rootCrossing hf hg hdeg hcross + have hupper := sameDegreeRootCountAbove_of_rootCount hf hg hdeg hlower + exact RootCountCompatible.of_rootCountAbove_bounds_of_nonRoot + hf_ne hg_ne (fun x _ _ => hupper x) + +/-- Successor-degree root-count compatibility is closed under close finite crossings. -/ +theorem RootCountCompatible.of_forall_pos_exists_close_succDegreeCrossing + {f g : ℝ[X]} (hf_ne : f ≠ 0) (hg_ne : g ≠ 0) + (hf : f.Splits) (hg : g.Splits) + (hdeg : g.natDegree = f.natDegree + 1) + (hclose : ∀ ρ : ℝ, 0 < ρ → + ∃ rf rg : List ℝ, + List.Forall₂ (fun x x' : ℝ => |x' - x| < ρ) (rootSeqDesc f) rf ∧ + List.Forall₂ (fun y y' : ℝ => |y' - y| < ρ) (rootSeqDesc g) rg ∧ + (∀ j, 1 ≤ j → j ≤ f.natDegree → + rg.getD j 0 ≤ rf.getD (j - 1) 0) ∧ + (∀ j, 1 ≤ j → j < f.natDegree → + rf.getD j 0 ≤ rg.getD (j - 1) 0)) : + RootCountCompatible f g := by + have hcross : + (∀ j, 1 ≤ j → j ≤ f.natDegree → + (rootSeqDesc g).getD j 0 ≤ + (rootSeqDesc f).getD (j - 1) 0) ∧ + (∀ j, 1 ≤ j → j < f.natDegree → + (rootSeqDesc f).getD j 0 ≤ + (rootSeqDesc g).getD (j - 1) 0) := by + constructor + · intro j hj1 hj + apply le_of_forall_pos_exists_close_le + intro ρ hρ + obtain ⟨rf, rg, hff, hgg, hfg⟩ := hclose ρ hρ + have hjg : j < (rootSeqDesc g).length := by + rw [rootSeqDesc_length hg, hdeg] + lia + have hjf : j - 1 < (rootSeqDesc f).length := by + rw [rootSeqDesc_length hf] + lia + have hjrg : j < rg.length := by simpa only [hgg.length_eq] using hjg + have hjrf : j - 1 < rf.length := by + simpa only [hff.length_eq] using hjf + exact ⟨rg.getD j 0, rf.getD (j - 1) 0, + abs_getD_sub_getD_lt_of_forall₂ hgg hjg hjrg, + abs_getD_sub_getD_lt_of_forall₂ hff hjf hjrf, + hfg.1 j hj1 hj⟩ + · intro j hj1 hj + apply le_of_forall_pos_exists_close_le + intro ρ hρ + obtain ⟨rf, rg, hff, hgg, hfg⟩ := hclose ρ hρ + have hjf : j < (rootSeqDesc f).length := by + simpa only [rootSeqDesc_length hf] using hj + have hjg : j - 1 < (rootSeqDesc g).length := by + rw [rootSeqDesc_length hg, hdeg] + lia + have hjrf : j < rf.length := by simpa only [hff.length_eq] using hjf + have hjrg : j - 1 < rg.length := by + simpa only [hgg.length_eq] using hjg + exact ⟨rf.getD j 0, rg.getD (j - 1) 0, + abs_getD_sub_getD_lt_of_forall₂ hff hjf hjrf, + abs_getD_sub_getD_lt_of_forall₂ hgg hjg hjrg, + hfg.2 j hj1 hj⟩ + have hlower := succDegreeRootCount_of_rootCrossing hf hg hdeg hcross + have hupper := succDegreeRootCountAbove_of_rootCount hf hg hdeg hlower + exact RootCountCompatible.of_rootCountAbove_bounds_of_nonRoot + hf_ne hg_ne (fun x _ _ => hupper x) + +/-- Same-degree root-count compatibility is closed under close compatible pairs. -/ +theorem RootCountCompatible.of_forall_pos_exists_close_sameDegreeCompatible + {p q : ℝ[X]} (hp_ne : p ≠ 0) (hq_ne : q ≠ 0) + (hp : p.Splits) (hq : q.Splits) + (hdeg : q.natDegree = p.natDegree) + (hclose : ∀ ρ : ℝ, 0 < ρ → + ∃ p' q' : ℝ[X], + p' ≠ 0 ∧ + q' ≠ 0 ∧ + p'.Splits ∧ + q'.Splits ∧ + List.Forall₂ + (fun x x' : ℝ => |x' - x| < ρ) + (rootSeqDesc p) (rootSeqDesc p') ∧ + List.Forall₂ + (fun y y' : ℝ => |y' - y| < ρ) + (rootSeqDesc q) (rootSeqDesc q') ∧ + RootCountCompatible p' q') : + RootCountCompatible p q := by + refine RootCountCompatible.of_forall_pos_exists_close_sameDegreeCrossing + hp_ne hq_ne hp hq hdeg ?_ + intro ρ hρ + obtain ⟨p', q', hp'_ne, hq'_ne, hp'_split, hq'_split, + hpp', hqq', hcompat'⟩ := + hclose ρ hρ + have hpdeg : p'.natDegree = p.natDegree := by + rw [← rootSeqDesc_length hp'_split, ← rootSeqDesc_length hp] + exact hpp'.length_eq.symm + have hqdeg : q'.natDegree = q.natDegree := by + rw [← rootSeqDesc_length hq'_split, ← rootSeqDesc_length hq] + exact hqq'.length_eq.symm + have hdeg' : q'.natDegree = p'.natDegree := by + rw [hqdeg, hpdeg, hdeg] + have hcount' := + sameDegreeRootCountAbove_of_nonRoot_bound hp'_ne hq'_ne + (fun x hpx hqx => + hcompat'.rootCountAbove_bounds_of_nonRoot hp'_ne hq'_ne hpx hqx) + exact ⟨rootSeqDesc p', rootSeqDesc q', hpp', hqq', + by simpa only [hpdeg] using + (rootCrossing_of_rootCountAbove_diff_le_one + hp'_split hq'_split hdeg' hcount')⟩ + +/-- Successor-degree root-count compatibility is closed under close compatible pairs. -/ +theorem RootCountCompatible.of_forall_pos_exists_close_succDegreeCompatible + {p q : ℝ[X]} (hp_ne : p ≠ 0) (hq_ne : q ≠ 0) + (hp : p.Splits) (hq : q.Splits) + (hdeg : q.natDegree = p.natDegree + 1) + (hclose : ∀ ρ : ℝ, 0 < ρ → + ∃ p' q' : ℝ[X], + p' ≠ 0 ∧ + q' ≠ 0 ∧ + p'.Splits ∧ + q'.Splits ∧ + List.Forall₂ + (fun x x' : ℝ => |x' - x| < ρ) + (rootSeqDesc p) (rootSeqDesc p') ∧ + List.Forall₂ + (fun y y' : ℝ => |y' - y| < ρ) + (rootSeqDesc q) (rootSeqDesc q') ∧ + RootCountCompatible p' q') : + RootCountCompatible p q := by + refine RootCountCompatible.of_forall_pos_exists_close_succDegreeCrossing + hp_ne hq_ne hp hq hdeg ?_ + intro ρ hρ + obtain ⟨p', q', hp'_ne, hq'_ne, hp'_split, hq'_split, + hpp', hqq', hcompat'⟩ := + hclose ρ hρ + have hpdeg : p'.natDegree = p.natDegree := by + rw [← rootSeqDesc_length hp'_split, ← rootSeqDesc_length hp] + exact hpp'.length_eq.symm + have hqdeg : q'.natDegree = q.natDegree := by + rw [← rootSeqDesc_length hq'_split, ← rootSeqDesc_length hq] + exact hqq'.length_eq.symm + have hdeg' : q'.natDegree = p'.natDegree + 1 := by + rw [hqdeg, hpdeg, hdeg] + have hcount' := + sameDegreeRootCountAbove_of_nonRoot_bound hp'_ne hq'_ne + (fun x hpx hqx => + hcompat'.rootCountAbove_bounds_of_nonRoot hp'_ne hq'_ne hpx hqx) + exact ⟨rootSeqDesc p', rootSeqDesc q', hpp', hqq', + by simpa only [hpdeg] using + (succDegreeRootCrossing_of_rootCountAbove + hp'_split hq'_split hdeg' hcount')⟩ + +/-- A fixed left branch is closed under close same-degree approximations. -/ +theorem LeftRootCountBranch.of_forall_pos_exists_close_of_sameDegree + {f g : ℝ[X]} {r s : ℝ} + (hf_ne : f ≠ 0) (hg_ne : g ≠ 0) + (hf : f.Splits) (hg : g.Splits) + (hr : IsLargestRoot f r) (hs : IsLargestRoot g s) + (hdeg : f.natDegree = g.natDegree) + (hclose : ∀ ρ : ℝ, 0 < ρ → + ∃ f' g' : ℝ[X], ∃ r' s' : ℝ, + f' ≠ 0 ∧ + g' ≠ 0 ∧ + f'.Splits ∧ + g'.Splits ∧ + Multiset.Rel + (fun x x' : ℝ => |x' - x| < ρ) + f.roots f'.roots ∧ + Multiset.Rel + (fun y y' : ℝ => |y' - y| < ρ) + g.roots g'.roots ∧ + LeftRootCountBranch f' g' r' s') : + LeftRootCountBranch f g r s := by + have hlargest : s ≤ r := by + apply le_of_forall_pos_exists_close_le + intro ρ hρ + obtain ⟨f', g', r', s', hf'_ne, hg'_ne, hf'_split, hg'_split, + hff', hgg', hbranch'⟩ := hclose ρ hρ + exact ⟨s', r', + _root_.RealRooted.IsLargestRoot.abs_sub_lt_of_roots_rel + hg_ne hg'_ne hs hbranch'.g_largest hgg', + _root_.RealRooted.IsLargestRoot.abs_sub_lt_of_roots_rel + hf_ne hf'_ne hr hbranch'.f_largest hff', + hbranch'.largest_ge⟩ + have hdelete_degree : + g.natDegree = (deleteRootFactor f r).natDegree + 1 := by + rw [natDegree_deleteRootFactor] + have hf_degree_pos := hr.natDegree_pos hf_ne + lia + have hcount : RootCountCompatible (deleteRootFactor f r) g := by + refine RootCountCompatible.of_forall_pos_exists_close_succDegreeCompatible + (hr.deleteRootFactor_ne_zero hf_ne) hg_ne + (hr.deleteRootFactor_splits hf) hg hdelete_degree ?_ + intro ρ hρ + obtain ⟨f', g', r', s', hf'_ne, hg'_ne, hf'_split, hg'_split, + hff', hgg', hbranch'⟩ := hclose ρ hρ + refine ⟨deleteRootFactor f' r', g', + hbranch'.f_largest.deleteRootFactor_ne_zero hf'_ne, + hg'_ne, + hbranch'.f_largest.deleteRootFactor_splits hf'_split, + hg'_split, ?_, ?_, hbranch'.count⟩ + · simpa only [rootSeqDesc_eq_sort_ge] using + (forall₂_sort_ge_deleteRootFactor_of_roots_rel + hf_ne hf'_ne hr hbranch'.f_largest hff') + · simpa only [rootSeqDesc_eq_sort_ge] using + (forall₂_sort_ge_of_rel_abs_sub_lt hgg') + exact ⟨hr, hs, hlargest, hcount⟩ + +/-- A fixed left branch is closed when the first degree is one larger. -/ +theorem LeftRootCountBranch.of_forall_pos_exists_close_of_degree_eq_succ + {f g : ℝ[X]} {r s : ℝ} + (hf_ne : f ≠ 0) (hg_ne : g ≠ 0) + (hf : f.Splits) (hg : g.Splits) + (hr : IsLargestRoot f r) (hs : IsLargestRoot g s) + (hdeg : f.natDegree = g.natDegree + 1) + (hclose : ∀ ρ : ℝ, 0 < ρ → + ∃ f' g' : ℝ[X], ∃ r' s' : ℝ, + f' ≠ 0 ∧ + g' ≠ 0 ∧ + f'.Splits ∧ + g'.Splits ∧ + Multiset.Rel + (fun x x' : ℝ => |x' - x| < ρ) + f.roots f'.roots ∧ + Multiset.Rel + (fun y y' : ℝ => |y' - y| < ρ) + g.roots g'.roots ∧ + LeftRootCountBranch f' g' r' s') : + LeftRootCountBranch f g r s := by + have hlargest : s ≤ r := by + apply le_of_forall_pos_exists_close_le + intro ρ hρ + obtain ⟨f', g', r', s', hf'_ne, hg'_ne, hf'_split, hg'_split, + hff', hgg', hbranch'⟩ := hclose ρ hρ + exact ⟨s', r', + _root_.RealRooted.IsLargestRoot.abs_sub_lt_of_roots_rel + hg_ne hg'_ne hs hbranch'.g_largest hgg', + _root_.RealRooted.IsLargestRoot.abs_sub_lt_of_roots_rel + hf_ne hf'_ne hr hbranch'.f_largest hff', + hbranch'.largest_ge⟩ + have hdelete_degree : + g.natDegree = (deleteRootFactor f r).natDegree := by + rw [natDegree_deleteRootFactor] + have hf_degree_pos := hr.natDegree_pos hf_ne + lia + have hcount : RootCountCompatible (deleteRootFactor f r) g := by + refine RootCountCompatible.of_forall_pos_exists_close_sameDegreeCompatible + (hr.deleteRootFactor_ne_zero hf_ne) hg_ne + (hr.deleteRootFactor_splits hf) hg hdelete_degree ?_ + intro ρ hρ + obtain ⟨f', g', r', s', hf'_ne, hg'_ne, hf'_split, hg'_split, + hff', hgg', hbranch'⟩ := hclose ρ hρ + refine ⟨deleteRootFactor f' r', g', + hbranch'.f_largest.deleteRootFactor_ne_zero hf'_ne, + hg'_ne, + hbranch'.f_largest.deleteRootFactor_splits hf'_split, + hg'_split, ?_, ?_, hbranch'.count⟩ + · simpa only [rootSeqDesc_eq_sort_ge] using + (forall₂_sort_ge_deleteRootFactor_of_roots_rel + hf_ne hf'_ne hr hbranch'.f_largest hff') + · simpa only [rootSeqDesc_eq_sort_ge] using + (forall₂_sort_ge_of_rel_abs_sub_lt hgg') + exact ⟨hr, hs, hlargest, hcount⟩ + +/-- A fixed left branch is closed when the first degree is two larger. -/ +theorem LeftRootCountBranch.of_forall_pos_exists_close_of_degree_eq_succ_succ + {f g : ℝ[X]} {r s : ℝ} + (hf_ne : f ≠ 0) (hg_ne : g ≠ 0) + (hf : f.Splits) (hg : g.Splits) + (hr : IsLargestRoot f r) (hs : IsLargestRoot g s) + (hdeg : f.natDegree = g.natDegree + 2) + (hclose : ∀ ρ : ℝ, 0 < ρ → + ∃ f' g' : ℝ[X], ∃ r' s' : ℝ, + f' ≠ 0 ∧ + g' ≠ 0 ∧ + f'.Splits ∧ + g'.Splits ∧ + Multiset.Rel + (fun x x' : ℝ => |x' - x| < ρ) + f.roots f'.roots ∧ + Multiset.Rel + (fun y y' : ℝ => |y' - y| < ρ) + g.roots g'.roots ∧ + LeftRootCountBranch f' g' r' s') : + LeftRootCountBranch f g r s := by + have hlargest : s ≤ r := by + apply le_of_forall_pos_exists_close_le + intro ρ hρ + obtain ⟨f', g', r', s', hf'_ne, hg'_ne, hf'_split, hg'_split, + hff', hgg', hbranch'⟩ := hclose ρ hρ + exact ⟨s', r', + _root_.RealRooted.IsLargestRoot.abs_sub_lt_of_roots_rel + hg_ne hg'_ne hs hbranch'.g_largest hgg', + _root_.RealRooted.IsLargestRoot.abs_sub_lt_of_roots_rel + hf_ne hf'_ne hr hbranch'.f_largest hff', + hbranch'.largest_ge⟩ + have hdelete_degree : + (deleteRootFactor f r).natDegree = g.natDegree + 1 := by + rw [natDegree_deleteRootFactor] + have hf_degree_pos := hr.natDegree_pos hf_ne + lia + have hcount : RootCountCompatible (deleteRootFactor f r) g := by + have hcount_symm : RootCountCompatible g (deleteRootFactor f r) := by + refine RootCountCompatible.of_forall_pos_exists_close_succDegreeCompatible + hg_ne (hr.deleteRootFactor_ne_zero hf_ne) hg + (hr.deleteRootFactor_splits hf) hdelete_degree ?_ + intro ρ hρ + obtain ⟨f', g', r', s', hf'_ne, hg'_ne, hf'_split, hg'_split, + hff', hgg', hbranch'⟩ := hclose ρ hρ + refine ⟨g', deleteRootFactor f' r', + hg'_ne, + hbranch'.f_largest.deleteRootFactor_ne_zero hf'_ne, + hg'_split, + hbranch'.f_largest.deleteRootFactor_splits hf'_split, + ?_, ?_, hbranch'.count.symm⟩ + · simpa only [rootSeqDesc_eq_sort_ge] using + (forall₂_sort_ge_of_rel_abs_sub_lt hgg') + · simpa only [rootSeqDesc_eq_sort_ge] using + (forall₂_sort_ge_deleteRootFactor_of_roots_rel + hf_ne hf'_ne hr hbranch'.f_largest hff') + exact hcount_symm.symm + exact ⟨hr, hs, hlargest, hcount⟩ + +/-- A fixed left branch is closed under close approximations. -/ +theorem LeftRootCountBranch.of_forall_pos_exists_close + {f g : ℝ[X]} {r s : ℝ} + (hf_ne : f ≠ 0) (hg_ne : g ≠ 0) + (hf : f.Splits) (hg : g.Splits) + (hr : IsLargestRoot f r) (hs : IsLargestRoot g s) + (hclose : ∀ ρ : ℝ, 0 < ρ → + ∃ f' g' : ℝ[X], ∃ r' s' : ℝ, + f' ≠ 0 ∧ + g' ≠ 0 ∧ + f'.Splits ∧ + g'.Splits ∧ + Multiset.Rel + (fun x x' : ℝ => |x' - x| < ρ) + f.roots f'.roots ∧ + Multiset.Rel + (fun y y' : ℝ => |y' - y| < ρ) + g.roots g'.roots ∧ + LeftRootCountBranch f' g' r' s') : + LeftRootCountBranch f g r s := by + obtain ⟨f', g', r', s', hf'_ne, hg'_ne, hf'_split, hg'_split, + hff', hgg', hbranch'⟩ := hclose 1 zero_lt_one + have hf_degree : f'.natDegree = f.natDegree := by + calc + f'.natDegree = f'.roots.card := (card_roots_of_splits hf'_split).symm + _ = f.roots.card := (Multiset.card_eq_card_of_rel hff').symm + _ = f.natDegree := card_roots_of_splits hf + have hg_degree : g'.natDegree = g.natDegree := by + calc + g'.natDegree = g'.roots.card := (card_roots_of_splits hg'_split).symm + _ = g.roots.card := (Multiset.card_eq_card_of_rel hgg').symm + _ = g.natDegree := card_roots_of_splits hg + have hdegrees := + hbranch'.natDegree_eq_or_eq_succ_or_eq_succ_succ + hf'_ne hf'_split hg'_split + rw [hf_degree, hg_degree] at hdegrees + rcases hdegrees with hdeg | hdeg | hdeg + · exact LeftRootCountBranch.of_forall_pos_exists_close_of_sameDegree + hf_ne hg_ne hf hg hr hs hdeg hclose + · exact LeftRootCountBranch.of_forall_pos_exists_close_of_degree_eq_succ + hf_ne hg_ne hf hg hr hs hdeg hclose + · exact + LeftRootCountBranch.of_forall_pos_exists_close_of_degree_eq_succ_succ + hf_ne hg_ne hf hg hr hs hdeg hclose + +/-- A fixed right branch is closed under close approximations. -/ +theorem RightRootCountBranch.of_forall_pos_exists_close + {f g : ℝ[X]} {r s : ℝ} + (hf_ne : f ≠ 0) (hg_ne : g ≠ 0) + (hf : f.Splits) (hg : g.Splits) + (hr : IsLargestRoot f r) (hs : IsLargestRoot g s) + (hrlt : r < s) + (hclose : ∀ ρ : ℝ, 0 < ρ → + ∃ f' g' : ℝ[X], ∃ r' s' : ℝ, + f' ≠ 0 ∧ + g' ≠ 0 ∧ + f'.Splits ∧ + g'.Splits ∧ + Multiset.Rel + (fun x x' : ℝ => |x' - x| < ρ) + f.roots f'.roots ∧ + Multiset.Rel + (fun y y' : ℝ => |y' - y| < ρ) + g.roots g'.roots ∧ + RightRootCountBranch f' g' r' s') : + RightRootCountBranch f g r s := by + have hleft : LeftRootCountBranch g f s r := by + apply LeftRootCountBranch.of_forall_pos_exists_close + hg_ne hf_ne hg hf hs hr + intro ρ hρ + obtain ⟨f', g', r', s', hf'_ne, hg'_ne, hf'_split, hg'_split, + hff', hgg', hbranch'⟩ := hclose ρ hρ + exact + ⟨g', f', s', r', + hg'_ne, hf'_ne, + hg'_split, hf'_split, + hgg', hff', + hbranch'.toLeftBranch_symm⟩ + exact hleft.toRightBranch_symm_of_lt hrlt + +/-- Liu's disjunctive root-count branch is closed under close splitting approximations. -/ +theorem theorem21RootCountBranches_of_forall_pos_exists_roots_rel + {f g : ℝ[X]} (hf_ne : f ≠ 0) (hg_ne : g ≠ 0) + (hf : f.Splits) (hg : g.Splits) (hno : NoCommonRoots f g) + (hf_deg : f.natDegree ≠ 0) (hg_deg : g.natDegree ≠ 0) + (hclose : ∀ ρ : ℝ, 0 < ρ → + ∃ f' g' : ℝ[X], + f' ≠ 0 ∧ + g' ≠ 0 ∧ + f'.Splits ∧ + g'.Splits ∧ + Multiset.Rel + (fun x x' : ℝ => |x' - x| < ρ) + f.roots f'.roots ∧ + Multiset.Rel + (fun y y' : ℝ => |y' - y| < ρ) + g.roots g'.roots ∧ + theorem21RootCountBranches f' g') : + theorem21RootCountBranches f g := by + have widenRootsRel {δ ρ : ℝ} (hδρ : δ ≤ ρ) {u v : Multiset ℝ} + (h : Multiset.Rel + (fun x x' : ℝ => |x' - x| < δ) u v) : + Multiset.Rel (fun x x' : ℝ => |x' - x| < ρ) u v := + h.mono fun _ _ _ _ hxy => hxy.trans_le hδρ + obtain ⟨r, hr⟩ := + exists_isLargestRoot hf_ne hf (Nat.pos_of_ne_zero hf_deg) + obtain ⟨s, hs⟩ := + exists_isLargestRoot hg_ne hg (Nat.pos_of_ne_zero hg_deg) + have hrs_ne : r ≠ s := by + intro hrs + subst s + exact (hno r hr.isRoot) hs.isRoot + rcases lt_or_gt_of_ne hrs_ne with hrs | hsr + · apply theorem21RootCountBranches_of_right + apply RightRootCountBranch.of_forall_pos_exists_close + hf_ne hg_ne hf hg hr hs hrs + intro ρ hρ + let δ : ℝ := min ρ ((s - r) / 2) + have hδ : 0 < δ := + lt_min hρ (half_pos (sub_pos.mpr hrs)) + have hδ_le_ρ : δ ≤ ρ := min_le_left _ _ + have hδ_le_gap : δ ≤ (s - r) / 2 := min_le_right _ _ + obtain ⟨f', g', hf'_ne, hg'_ne, hf'_split, hg'_split, + hff', hgg', hbranches⟩ := hclose δ hδ + obtain ⟨r', s', hbranch'⟩ := hbranches + rcases hbranch' with hleft' | hright' + · exfalso + have hr_close := + _root_.RealRooted.IsLargestRoot.abs_sub_lt_of_roots_rel + hf_ne hf'_ne hr hleft'.f_largest hff' + have hs_close := + _root_.RealRooted.IsLargestRoot.abs_sub_lt_of_roots_rel + hg_ne hg'_ne hs hleft'.g_largest hgg' + rw [abs_lt] at hr_close hs_close + linarith [hleft'.largest_ge, hδ_le_gap] + · exact + ⟨f', g', r', s', hf'_ne, hg'_ne, hf'_split, hg'_split, + widenRootsRel hδ_le_ρ hff', + widenRootsRel hδ_le_ρ hgg', + hright'⟩ + · apply theorem21RootCountBranches_of_left + apply LeftRootCountBranch.of_forall_pos_exists_close + hf_ne hg_ne hf hg hr hs + intro ρ hρ + let δ : ℝ := min ρ ((r - s) / 2) + have hδ : 0 < δ := + lt_min hρ (half_pos (sub_pos.mpr hsr)) + have hδ_le_ρ : δ ≤ ρ := min_le_left _ _ + have hδ_le_gap : δ ≤ (r - s) / 2 := min_le_right _ _ + obtain ⟨f', g', hf'_ne, hg'_ne, hf'_split, hg'_split, + hff', hgg', hbranches⟩ := hclose δ hδ + obtain ⟨r', s', hbranch'⟩ := hbranches + rcases hbranch' with hleft' | hright' + · exact + ⟨f', g', r', s', hf'_ne, hg'_ne, hf'_split, hg'_split, + widenRootsRel hδ_le_ρ hff', + widenRootsRel hδ_le_ρ hgg', + hleft'⟩ + · exfalso + have hr_close := + _root_.RealRooted.IsLargestRoot.abs_sub_lt_of_roots_rel + hf_ne hf'_ne hr hright'.f_largest hff' + have hs_close := + _root_.RealRooted.IsLargestRoot.abs_sub_lt_of_roots_rel + hg_ne hg'_ne hs hright'.g_largest hgg' + rw [abs_lt] at hr_close hs_close + linarith [hright'.largest_lt, hδ_le_gap] + +end LiuOppositeSigns +end RealRooted diff --git a/RealRooted/LiuOppositeSigns/RootCountRelStability.lean b/RealRooted/LiuOppositeSigns/RootCountRelStability.lean new file mode 100644 index 00000000..cb6717a1 --- /dev/null +++ b/RealRooted/LiuOppositeSigns/RootCountRelStability.lean @@ -0,0 +1,59 @@ +import RealRooted.LiuOppositeSigns +import RealRooted.Mathlib.Data.Multiset.Rel +import RealRooted.RootMultiplicityMatching + +/-! +# Root-count stability under close multiset matchings + +These lemmas provide the local closedness input for the limiting step in Liu's +opposite-leading-sign theorem. They compare root counts only at thresholds +separated from the original roots and compare the selected largest roots. +-/ + +namespace RealRooted + +open LiuOppositeSigns Polynomial + +/-- A close root matching preserves the root count at a separated threshold. -/ +theorem rootCountAtOrAbove_eq_of_roots_rel_abs_sub_lt + {p q : ℝ[X]} {x δ : ℝ} + (hsep : ∀ r ∈ p.roots, δ ≤ |r - x|) + (hmatch : Multiset.Rel (fun r s ↦ |s - r| < δ) p.roots q.roots) : + rootCountAtOrAbove p x = rootCountAtOrAbove q x := by + unfold rootCountAtOrAbove + apply Multiset.Rel.card_filter_eq hmatch (fun r => x ≤ r) (fun s => x ≤ s) + intro r hr s hs hrs + have habs := abs_lt.mp hrs + constructor + · intro hxr + have hrx : δ ≤ r - x := by + simpa [abs_of_nonneg (sub_nonneg.mpr hxr)] using hsep r hr + linarith [habs.1] + · intro hxs + by_contra hxr + have hrx : δ ≤ x - r := by + have hrx' : r ≤ x := le_of_lt (lt_of_not_ge hxr) + simpa [abs_of_nonpos (sub_nonpos.mpr hrx')] using hsep r hr + linarith [habs.2] + +/-- Largest roots of closely matched nonzero polynomials are close. -/ +theorem IsLargestRoot.abs_sub_lt_of_roots_rel + {p q : ℝ[X]} {r s δ : ℝ} (hp_ne : p ≠ 0) (hq_ne : q ≠ 0) + (hr : IsLargestRoot p r) (hs : IsLargestRoot q s) + (hmatch : Multiset.Rel (fun a b ↦ |b - a| < δ) p.roots q.roots) : + |s - r| < δ := by + have hr_mem : r ∈ p.roots := (Polynomial.mem_roots hp_ne).mpr hr.isRoot + have hs_mem : s ∈ q.roots := (Polynomial.mem_roots hq_ne).mpr hs.isRoot + obtain ⟨b, hb_mem, hrb⟩ := + Multiset.exists_mem_of_rel_of_mem hmatch hr_mem + obtain ⟨a, ha_mem, has⟩ := by + simpa only [Function.flip_def] using + Multiset.exists_mem_of_rel_of_mem ((Multiset.rel_flip).2 hmatch) hs_mem + have hb_le : b ≤ s := hs.roots_le b hb_mem + have ha_le : a ≤ r := hr.roots_le a ha_mem + rw [abs_lt] + constructor + · linarith [(abs_lt.mp hrb).1] + · linarith [(abs_lt.mp has).2] + +end RealRooted diff --git a/RealRooted/LiuOppositeSigns/Theorem21Statements.lean b/RealRooted/LiuOppositeSigns/Theorem21Statements.lean index 8188a22b..fd0679c4 100644 --- a/RealRooted/LiuOppositeSigns/Theorem21Statements.lean +++ b/RealRooted/LiuOppositeSigns/Theorem21Statements.lean @@ -1918,6 +1918,49 @@ def theorem21CompatibleToRootCountBranchesNonconstantStatement : Prop := f.natDegree ≠ 0 → g.natDegree ≠ 0 → Compatible f g → theorem21RootCountBranches f g +/-- The unreduced nonconstant forward statement is false when the endpoints +share their largest root. The minimal counterexample is `X` and `-(X ^ 2)`. -/ +theorem not_theorem21CompatibleToRootCountBranchesNonconstantStatement : + ¬ theorem21CompatibleToRootCountBranchesNonconstantStatement := by + intro hforward + have hbase : Compatible (1 : ℝ[X]) (-X) := + Compatible.of_allComboRealRooted <| + (allComboRealRooted_of_natDegree_le_one + hasPosLeadingCoeff_one + (by unfold HasPosLeadingCoeff; simp) + (by simp) (by simp)).neg_right + have hgsplits : (-(X ^ 2) : ℝ[X]).Splits := by + simpa [pow_two] using + (Polynomial.Splits.X.mul Polynomial.Splits.X).neg + have hcompat : Compatible (X : ℝ[X]) (-(X ^ 2)) := by + simpa [pow_two] using + compatible_mul_common_factor + (d := (X : ℝ[X])) Polynomial.Splits.X hbase + have hsgn : OppositeLeadingSigns (X : ℝ[X]) (-(X ^ 2)) := by + norm_num [OppositeLeadingSigns] + have hfdeg : (X : ℝ[X]).natDegree ≠ 0 := by + simp + have hgdeg : (-(X ^ 2) : ℝ[X]).natDegree ≠ 0 := by + norm_num [Polynomial.natDegree_neg, Polynomial.natDegree_pow] + obtain ⟨r, s, hleft | hright⟩ := + hforward + (f := (X : ℝ[X])) (g := -(X ^ 2)) + Polynomial.Splits.X hgsplits hsgn hfdeg hgdeg hcompat + · have hgap := + hleft.count.natDegree_abs_sub_le_one + (deleteRootFactor_splits_of_isRoot + Polynomial.Splits.X hleft.f_largest.isRoot) + hgsplits + norm_num [natDegree_deleteRootFactor, Polynomial.natDegree_neg, + Polynomial.natDegree_pow] at hgap + · have hr : r = 0 := by + simpa [Polynomial.IsRoot.def] using hright.f_largest.isRoot + have hs : s = 0 := by + simpa [Polynomial.IsRoot.def] using hright.g_largest.isRoot + have hfalse : (0 : ℝ) < 0 := by + simpa [hr, hs] using hright.largest_lt + exact (lt_irrefl 0) hfalse + /-- Reverse half of Liu Theorem 2.1, isolated as a statement target. -/ def theorem21RootCountBranchesToCompatibleStatement : Prop := ∀ {f g : ℝ[X]}, diff --git a/RealRooted/LiuOppositeSignsTheorem.lean b/RealRooted/LiuOppositeSignsTheorem.lean index 7182b3cc..9f0f32cf 100644 --- a/RealRooted/LiuOppositeSignsTheorem.lean +++ b/RealRooted/LiuOppositeSignsTheorem.lean @@ -1,8 +1,14 @@ +import RealRooted.LiuOppositeSigns.BoundedIntervalContinuity import RealRooted.LiuOppositeSigns.CommonInterleaverConsequences +import RealRooted.LiuOppositeSigns.Corollary22 +import RealRooted.LiuOppositeSigns.DerivativeShiftSequenceRegularization import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.RootOrderAssembly import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.RootOrderLower import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.RootOrderUpper +import RealRooted.LiuOppositeSigns.RootCountClosure +import RealRooted.LiuOppositeSigns.Theorem21Assembly import RealRooted.LiuOppositeSigns.XSub.IntervalRootCount +import RealRooted.ObreschkoffConverse /-! # Liu opposite-sign compatibility theorem @@ -18,6 +24,132 @@ open Polynomial Filter namespace RealRooted namespace LiuOppositeSigns +/-- The no-common, nonconstant forward implication in Liu Theorem 2.1. + +The derivative-shift regularization repairs the source's invalid inference +from no common roots to simple roots. The simple-root argument is applied to +arbitrarily close regularizations, and root matching closes the result. -/ +theorem theorem21CompatibleToRootCountBranchesNoCommonNonconstant : + theorem21CompatibleToRootCountBranchesNoCommonNonconstantStatement := by + intro f g hf hg hsgn hno hf_deg hg_deg hcompat + apply theorem21RootCountBranches_of_forall_pos_exists_roots_rel + hsgn.left_ne_zero hsgn.right_ne_zero hf hg hno hf_deg hg_deg + intro ρ hρ + obtain ⟨epss, hlen, hbounds, hcompat', hno', hfrel, hgrel⟩ := + hno.exists_applyTDerivList_roots_rel (κ := 1) (ρ := ρ) + hcompat hsgn.left_ne_zero hsgn.right_ne_zero hf hg + zero_lt_one hρ (max f.natDegree g.natDegree) + let f' : ℝ[X] := applyTDerivList epss f + let g' : ℝ[X] := applyTDerivList epss g + have hpos : ∀ eps ∈ epss, 0 < eps := + fun eps heps => (hbounds eps heps).1 + have hf'_ne : f' ≠ 0 := by + simpa [f'] using + applyTDerivList_ne_zero (epss := epss) hsgn.left_ne_zero + have hg'_ne : g' ≠ 0 := by + simpa [g'] using + applyTDerivList_ne_zero (epss := epss) hsgn.right_ne_zero + have hf'_split : f'.Splits := by + simpa [f'] using hf.applyTDerivList hpos + have hg'_split : g'.Splits := by + simpa [g'] using hg.applyTDerivList hpos + have hf'_deg : f'.natDegree ≠ 0 := by + simpa [f'] using hf_deg + have hg'_deg : g'.natDegree ≠ 0 := by + simpa [g'] using hg_deg + have hsgn' : OppositeLeadingSigns f' g' := by + simpa [f', g', OppositeLeadingSigns] using hsgn + have hf'_simple : HasSimpleRoots f' := by + change HasSimpleRoots (applyTDerivList epss f) + apply hasSimpleRoots_applyTDerivList_of_natDegree_le_length + hpos hsgn.left_ne_zero hf + rw [hlen] + exact Nat.le_max_left _ _ + have hg'_simple : HasSimpleRoots g' := by + change HasSimpleRoots (applyTDerivList epss g) + apply hasSimpleRoots_applyTDerivList_of_natDegree_le_length + hpos hsgn.right_ne_zero hg + rw [hlen] + exact Nat.le_max_right _ _ + have hbranches : theorem21RootCountBranches f' g' := + theorem21RootCountBranches_of_compatible_noCommon_nonconstant_of_simple + hf'_split hg'_split hsgn' hno' hf'_deg hg'_deg + hf'_simple hg'_simple hcompat' + refine + ⟨f', g', hf'_ne, hg'_ne, hf'_split, hg'_split, ?_, ?_, hbranches⟩ + · simpa [f'] using hfrel + · simpa [g'] using hgrel + +/-- The nonconstant no-common-root form of Liu Theorem 2.1. -/ +theorem theorem21CompatibleRootCountNoCommonNonconstant : + theorem21CompatibleRootCountNoCommonNonconstantStatement := by + intro f g hf hg hsgn hno hf_deg hg_deg + exact + ⟨theorem21CompatibleToRootCountBranchesNoCommonNonconstant + hf hg hsgn hno hf_deg hg_deg, + theorem21RootCountBranchesToCompatibleNonconstant_of_xSub + hf hg hsgn hf_deg hg_deg⟩ + +/-- Compatible no-common nonconstant opposite-sign pairs have degree gap at +most two. -/ +theorem natDegree_abs_sub_le_two_of_compatible_noCommon_nonconstant + {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits) + (hsgn : OppositeLeadingSigns f g) (hno : NoCommonRoots f g) + (hf_deg : f.natDegree ≠ 0) (hg_deg : g.natDegree ≠ 0) + (hcompat : Compatible f g) : + |((f.natDegree : ℤ) - (g.natDegree : ℤ))| ≤ 2 := + natDegree_abs_sub_le_two_of_theorem21RootCountBranches hf hg hsgn + (theorem21CompatibleToRootCountBranchesNoCommonNonconstant + hf hg hsgn hno hf_deg hg_deg hcompat) + +/-- Correct nonconstant Liu equivalence with common roots retained explicitly. +The legacy branch-only equivalence is false when the endpoints share a largest +root: the right branch requires a strict largest-root inequality, while deleting +the largest root from only the left endpoint can leave a root-count gap of two. +The common-root deletion alternative is therefore necessary. + +The reduced predicate is the strongest form because its ordinary root-count +branch retains the accompanying `NoCommonRoots` witness. -/ +theorem compatible_iff_theorem21RootCountBranchesReduced_nonconstant + {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits) + (hsgn : OppositeLeadingSigns f g) + (hf_deg : f.natDegree ≠ 0) (hg_deg : g.natDegree ≠ 0) : + Compatible f g ↔ theorem21RootCountBranchesReduced f g := by + constructor + · intro hcompat + by_cases hno : NoCommonRoots f g + · exact Or.inl + ⟨hno, + theorem21CompatibleToRootCountBranchesNoCommonNonconstant + hf hg hsgn hno hf_deg hg_deg hcompat⟩ + · exact Or.inr + (CommonRootDeletionCompatibleBranch.of_compatible_of_not_noCommonRoots + hcompat hno) + · intro hbranches + rcases hbranches with hbranches | hcommon + · exact theorem21RootCountBranchesToCompatibleNonconstant_of_xSub + hf hg hsgn hf_deg hg_deg hbranches.2 + · exact hcommon.compatible + +/-- Public-facing correct nonconstant Liu equivalence. Compared with the +legacy branch-only predicate, this conclusion includes the necessary explicit +common-root deletion alternative. -/ +theorem compatible_iff_theorem21RootCountBranchesWithCommon_nonconstant + {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits) + (hsgn : OppositeLeadingSigns f g) + (hf_deg : f.natDegree ≠ 0) (hg_deg : g.natDegree ≠ 0) : + Compatible f g ↔ theorem21RootCountBranchesWithCommon f g := by + constructor + · intro hcompat + exact theorem21RootCountBranchesReduced.withCommon + ((compatible_iff_theorem21RootCountBranchesReduced_nonconstant + hf hg hsgn hf_deg hg_deg).mp hcompat) + · intro hbranches + rcases hbranches with hbranches | hcommon + · exact theorem21RootCountBranchesToCompatibleNonconstant_of_xSub + hf hg hsgn hf_deg hg_deg hbranches + · exact hcommon.compatible + /-- The isolated forward direction of Liu Theorem 2.1 gives the pointwise root-count gap bound. -/ theorem rootCountAtOrAbove_abs_sub_le_two_of_compatible_of_forward @@ -309,5 +441,164 @@ theorem hforward) hcases + +/-- The constant endpoint omitted by the source formulation of Corollary 2.2: +compatibility with an oppositely signed nonzero constant forces degree at most two. -/ +lemma natDegree_le_two_of_compatible_C_left + {c : ℝ} {p : ℝ[X]} (hp : p.Splits) + (hsgn : OppositeLeadingSigns (C c) p) (hcompat : Compatible (C c) p) : + p.natDegree ≤ 2 := by + by_contra hnot + have hthree : 3 ≤ p.natDegree := by + lia + have shift_ne {q : ℝ[X]} (t : ℝ) (hqdeg : 3 ≤ q.natDegree) : + q - C t ≠ 0 := by + have hdegree : (q - C t).natDegree = q.natDegree := by + apply natDegree_sub_eq_left_of_natDegree_lt + simp only [natDegree_C] + lia + intro hzero + have : q.natDegree = 0 := by + rw [← hdegree, hzero, natDegree_zero] + lia + rcases hsgn.pos_neg_or_neg_pos with hpos | hneg + · have hc_pos : 0 < c := by + simpa [HasPosLeadingCoeff] using hpos.1 + have hneg_three : 3 ≤ (-p).natDegree := by + simpa only [natDegree_neg] using hthree + obtain ⟨t, ht, hshift⟩ := + exists_pos_shift_down_not_isRealRooted_of_isRealRooted_of_natDegree_ge_three + hp.neg hpos.2 hneg_three + have hc_ne : c ≠ 0 := ne_of_gt hc_pos + have hq_ne : (-p) - C t ≠ 0 := shift_ne t hneg_three + have hcomb := + hcompat (t / c) 1 (div_nonneg ht.le hc_pos.le) zero_le_one + have hpoly : + C (t / c) * C c + C 1 * p = -((-p) - C t) := by + calc + C (t / c) * C c + C 1 * p = C ((t / c) * c) + p := by + rw [C_mul, C_1, one_mul] + _ = C t + p := by rw [div_mul_cancel₀ t hc_ne] + _ = -((-p) - C t) := by ring + rw [hpoly] at hcomb + rcases hcomb with hzero | hreal + · exact hq_ne (neg_eq_zero.mp hzero) + · exact hshift ⟨hq_ne, by simpa using hreal.2.neg⟩ + · have hc_pos : 0 < -c := by + simpa [HasPosLeadingCoeff] using hneg.1 + obtain ⟨t, ht, hshift⟩ := + exists_pos_shift_down_not_isRealRooted_of_isRealRooted_of_natDegree_ge_three + hp hneg.2 hthree + have hc_ne : -c ≠ 0 := ne_of_gt hc_pos + have hq_ne : p - C t ≠ 0 := shift_ne t hthree + have hcomb := + hcompat (t / (-c)) 1 (div_nonneg ht.le hc_pos.le) zero_le_one + have hpoly : C (t / (-c)) * C c + C 1 * p = p - C t := by + have hc' : c ≠ 0 := neg_ne_zero.mp hc_ne + calc + C (t / (-c)) * C c + C 1 * p = C ((t / (-c)) * c) + p := by + rw [C_mul, C_1, one_mul] + _ = C (-t) + p := by + congr 2 + field_simp + _ = p - C t := by simp only [map_neg]; ring + rw [hpoly] at hcomb + rcases hcomb with hzero | hreal + · exact hq_ne hzero + · exact hshift hreal + +/-- The right polynomial has degree at most two when the left polynomial is constant. -/ +lemma natDegree_right_le_two_of_compatible_of_left_natDegree_eq_zero + {f g : ℝ[X]} (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) + (hcompat : Compatible f g) (hfdeg : f.natDegree = 0) : + g.natDegree ≤ 2 := by + rw [eq_C_of_natDegree_eq_zero hfdeg] at hsgn hcompat + exact natDegree_le_two_of_compatible_C_left hg hsgn hcompat + +/-- The left polynomial has degree at most two when the right polynomial is constant. -/ +lemma natDegree_left_le_two_of_compatible_of_right_natDegree_eq_zero + {f g : ℝ[X]} (hf : f.Splits) (hsgn : OppositeLeadingSigns f g) + (hcompat : Compatible f g) (hgdeg : g.natDegree = 0) : + f.natDegree ≤ 2 := + natDegree_right_le_two_of_compatible_of_left_natDegree_eq_zero + hf hsgn.symm hcompat.comm hgdeg + +/-- Corollary 2.2's degree bound when the left polynomial is constant. -/ +lemma natDegree_abs_sub_le_two_of_compatible_of_left_natDegree_eq_zero + {f g : ℝ[X]} (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) + (hcompat : Compatible f g) (hfdeg : f.natDegree = 0) : + |((f.natDegree : ℤ) - (g.natDegree : ℤ))| ≤ 2 := by + have hle := + natDegree_right_le_two_of_compatible_of_left_natDegree_eq_zero + hg hsgn hcompat hfdeg + rw [hfdeg] + norm_num + exact_mod_cast hle + +/-- Corollary 2.2's degree bound when the right polynomial is constant. -/ +lemma natDegree_abs_sub_le_two_of_compatible_of_right_natDegree_eq_zero + {f g : ℝ[X]} (hf : f.Splits) (hsgn : OppositeLeadingSigns f g) + (hcompat : Compatible f g) (hgdeg : g.natDegree = 0) : + |((f.natDegree : ℤ) - (g.natDegree : ℤ))| ≤ 2 := by + simpa only [abs_sub_comm] using + natDegree_abs_sub_le_two_of_compatible_of_left_natDegree_eq_zero + hf hsgn.symm hcompat.comm hgdeg + +/-- Liu's Corollary 2.2: compatible real-rooted polynomials with opposite +leading signs have degrees differing by at most two. -/ +theorem corollary22DegreeDiff : corollary22DegreeDiffStatement := by + unfold corollary22DegreeDiffStatement + suffices h : + ∀ n : ℕ, ∀ f g : ℝ[X], f.natDegree + g.natDegree = n → + f.Splits → g.Splits → OppositeLeadingSigns f g → Compatible f g → + |((f.natDegree : ℤ) - (g.natDegree : ℤ))| ≤ 2 by + intro f g hf hg hsgn hcompat + exact h _ f g rfl hf hg hsgn hcompat + intro n + induction n using Nat.strong_induction_on with + | h n ih => + intro f g hsum hf hg hsgn hcompat + by_cases hfdeg : f.natDegree = 0 + · exact + natDegree_abs_sub_le_two_of_compatible_of_left_natDegree_eq_zero + hg hsgn hcompat hfdeg + by_cases hgdeg : g.natDegree = 0 + · exact + natDegree_abs_sub_le_two_of_compatible_of_right_natDegree_eq_zero + hf hsgn hcompat hgdeg + by_cases hno : NoCommonRoots f g + · exact + natDegree_abs_sub_le_two_of_compatible_noCommon_nonconstant + hf hg hsgn hno hfdeg hgdeg hcompat + obtain ⟨r, hfr, hgr⟩ := exists_common_root_of_not_noCommonRoots hno + let f' : ℝ[X] := deleteRootFactor f r + let g' : ℝ[X] := deleteRootFactor g r + have hf'_splits : f'.Splits := + deleteRootFactor_splits_of_isRoot hf hfr + have hg'_splits : g'.Splits := + deleteRootFactor_splits_of_isRoot hg hgr + have hsgn' : OppositeLeadingSigns f' g' := by + simpa [f', g'] using + (hsgn.deleteRootFactor_left hfr).deleteRootFactor_right hgr + have hcompat' : Compatible f' g' := + compatible_deleteRootFactor_of_common_root hcompat hfr hgr + have hf'_degree : f'.natDegree = f.natDegree - 1 := + natDegree_deleteRootFactor f r + have hg'_degree : g'.natDegree = g.natDegree - 1 := + natDegree_deleteRootFactor g r + have hf_pos : 0 < f.natDegree := Nat.pos_of_ne_zero hfdeg + have hg_pos : 0 < g.natDegree := Nat.pos_of_ne_zero hgdeg + have hlt : f'.natDegree + g'.natDegree < n := by + rw [hf'_degree, hg'_degree, ← hsum] + lia + have hrec := + ih (f'.natDegree + g'.natDegree) hlt f' g' rfl + hf'_splits hg'_splits hsgn' hcompat' + rw [hf'_degree, hg'_degree] at hrec + rw [Nat.cast_sub hf_pos, Nat.cast_sub hg_pos] at hrec + norm_num at hrec + simpa only [sub_sub_sub_cancel_right] using hrec + + end LiuOppositeSigns end RealRooted diff --git a/RealRooted/Mathlib/Data/Multiset/Rel.lean b/RealRooted/Mathlib/Data/Multiset/Rel.lean new file mode 100644 index 00000000..952287e2 --- /dev/null +++ b/RealRooted/Mathlib/Data/Multiset/Rel.lean @@ -0,0 +1,149 @@ +import Mathlib.Data.List.Forall2 +import Mathlib.Data.Multiset.Basic +import Mathlib.Data.Multiset.Sort +import Mathlib.Data.Multiset.ZeroCons + +/-! +# Additional lemmas for multiset relations + +This file provides reusable constructors for diagonal multiset relations and +heterogeneous composition. It is intended for upstreaming to +`Mathlib.Data.Multiset.ZeroCons`. +-/ + +namespace Multiset + +/-- Compose multiset relations whose element relations may differ. -/ +theorem Rel.comp {α β γ : Type*} + {R : α → β → Prop} {S : β → γ → Prop} {T : α → γ → Prop} + {xs : Multiset α} {ys : Multiset β} {zs : Multiset γ} + (hcomp : ∀ a b c, R a b → S b c → T a c) + (h₁ : Multiset.Rel R xs ys) (h₂ : Multiset.Rel S ys zs) : + Multiset.Rel T xs zs := by + induction ys using Multiset.induction_on generalizing xs zs with + | empty => + have hxs : xs = 0 := Multiset.rel_zero_right.mp h₁ + have hzs : zs = 0 := Multiset.rel_zero_left.mp h₂ + subst xs + subst zs + exact Rel.zero + | cons b ys ih => + obtain ⟨a, xs', hab, htail₁, rfl⟩ := Multiset.rel_cons_right.mp h₁ + obtain ⟨c, zs', hbc, htail₂, rfl⟩ := Multiset.rel_cons_left.mp h₂ + exact Rel.cons (hcomp a b c hab hbc) (ih htail₁ htail₂) + +/-- Related multisets have equally many elements satisfying corresponding predicates. -/ +theorem Rel.card_filter_eq {α β : Type*} {R : α → β → Prop} + {s : Multiset α} {t : Multiset β} (hrel : Multiset.Rel R s t) + (P : α → Prop) (Q : β → Prop) [DecidablePred P] [DecidablePred Q] + (hpred : ∀ a ∈ s, ∀ b ∈ t, R a b → (P a ↔ Q b)) : + (s.filter P).card = (t.filter Q).card := by + induction hrel with + | zero => simp + | @cons a b s t hab hrel ih => + have hpq : P a ↔ Q b := hpred a (by simp) b (by simp) hab + have htail : ∀ c ∈ s, ∀ d ∈ t, R c d → (P c ↔ Q d) := by + intro c hc d hd hcd + exact hpred c (by simp [hc]) d (by simp [hd]) hcd + by_cases ha : P a + · have hb : Q b := hpq.mp ha + simp [ha, hb, ih htail] + · have hb : ¬Q b := fun hb => ha (hpq.mpr hb) + simp [ha, hb, ih htail] + +private theorem rel_uncross_min_cons {α : Type*} [LinearOrder α] + {R : α → α → Prop} {a b : α} {as bs : Multiset α} + (huncross : ∀ {a c b d}, a ≤ c → b ≤ d → R a d → R c b → + R a b ∧ R c d) + (ha : ∀ c ∈ as, a ≤ c) (hb : ∀ d ∈ bs, b ≤ d) + (hrel : Multiset.Rel R (a ::ₘ as) (b ::ₘ bs)) : + R a b ∧ Multiset.Rel R as bs := by + obtain ⟨d, ds, hdb, hds, heq⟩ := Multiset.rel_cons_right.mp hrel + rcases Multiset.cons_eq_cons.mp heq with hsame | hswap + · rcases hsame with ⟨rfl, rfl⟩ + exact ⟨hdb, hds⟩ + · rcases hswap with ⟨_, cs, has, hds'⟩ + subst as + subst ds + obtain ⟨c, ts, hac, hct, rfl⟩ := Multiset.rel_cons_left.mp hds + have had : a ≤ d := ha d (by simp) + have hbc : b ≤ c := hb c (by simp) + obtain ⟨hab, hdc⟩ := huncross had hbc hac hdb + exact ⟨hab, Multiset.Rel.cons hdc hct⟩ + +/-- An uncrossable multiset relation pairs the corresponding sorted elements. -/ +theorem Rel.forall₂_sort {α : Type*} [LinearOrder α] {R : α → α → Prop} + (huncross : ∀ {a c b d}, a ≤ c → b ≤ d → R a d → R c b → + R a b ∧ R c d) + {s t : Multiset α} (hrel : Multiset.Rel R s t) : + List.Forall₂ R (s.sort (· ≤ ·)) (t.sort (· ≤ ·)) := by + revert t + apply Multiset.strongInductionOn s + (p := fun s => ∀ t, Multiset.Rel R s t → + List.Forall₂ R (s.sort (· ≤ ·)) (t.sort (· ≤ ·))) + intro s ih t hrel + cases hs : s.sort (· ≤ ·) with + | nil => + have hs0 : s = 0 := by + calc + s = ↑(s.sort (· ≤ ·)) := + (Multiset.sort_eq (s := s) (r := (· ≤ ·))).symm + _ = 0 := by simp [hs] + subst s + have ht0 : t = 0 := Multiset.rel_zero_left.mp hrel + subst t + simp + | cons a as => + have hsrepr : s = a ::ₘ (as : Multiset α) := by + calc + s = ↑(s.sort (· ≤ ·)) := + (Multiset.sort_eq (s := s) (r := (· ≤ ·))).symm + _ = a ::ₘ (as : Multiset α) := by simp [hs] + have hsord : (a :: as).Pairwise (· ≤ ·) := by + simpa [hs] using + (Multiset.pairwise_sort (s := s) (r := (· ≤ ·))) + have ha : ∀ c ∈ (as : Multiset α), a ≤ c := by + intro c hc + exact (List.pairwise_cons.mp hsord).1 c (by simpa using hc) + cases ht : t.sort (· ≤ ·) with + | nil => + have ht0 : t = 0 := by + calc + t = ↑(t.sort (· ≤ ·)) := + (Multiset.sort_eq (s := t) (r := (· ≤ ·))).symm + _ = 0 := by simp [ht] + subst t + have hs0 : s = 0 := Multiset.rel_zero_right.mp hrel + rw [hsrepr] at hs0 + simp at hs0 + | cons b bs => + have htrepr : t = b ::ₘ (bs : Multiset α) := by + calc + t = ↑(t.sort (· ≤ ·)) := + (Multiset.sort_eq (s := t) (r := (· ≤ ·))).symm + _ = b ::ₘ (bs : Multiset α) := by simp [ht] + have htord : (b :: bs).Pairwise (· ≤ ·) := by + simpa [ht] using + (Multiset.pairwise_sort (s := t) (r := (· ≤ ·))) + have hb : ∀ d ∈ (bs : Multiset α), b ≤ d := by + intro d hd + exact (List.pairwise_cons.mp htord).1 d (by simpa using hd) + rw [hsrepr, htrepr] at hrel + obtain ⟨hab, htail⟩ := rel_uncross_min_cons huncross ha hb hrel + have hsmall : (as : Multiset α) < s := by + rw [hsrepr] + exact Multiset.lt_cons_self _ _ + have ih_tail := ih (as : Multiset α) hsmall (bs : Multiset α) htail + have hasort : (as : Multiset α).sort (· ≤ ·) = as := by + have h := hs + rw [hsrepr, + Multiset.sort_cons a (as : Multiset α) (· ≤ ·) ha] at h + exact List.cons.inj h |>.2 + have hbsort : (bs : Multiset α).sort (· ≤ ·) = bs := by + have h := ht + rw [htrepr, + Multiset.sort_cons b (bs : Multiset α) (· ≤ ·) hb] at h + exact List.cons.inj h |>.2 + exact List.Forall₂.cons hab (by simpa [hasort, hbsort] using ih_tail) + +end Multiset diff --git a/RealRooted/ObreschkoffConverse.lean b/RealRooted/ObreschkoffConverse.lean index 54053d55..7dc4fb98 100644 --- a/RealRooted/ObreschkoffConverse.lean +++ b/RealRooted/ObreschkoffConverse.lean @@ -1633,8 +1633,94 @@ lemma exists_pos_shift_not_isRealRooted_of_isRealRooted_of_natDegree_ge_two simp_all linarith -/-- Constant shifts eventually destroy real-rootedness once the polynomial has -positive leading coefficient and degree at least `2`. -/ +/-- For an odd-degree positive-leading real-rooted polynomial, a sufficiently +large positive downward constant shift is not real-rooted. Reflecting across +the vertical axis and negating preserves the positive leading coefficient in +odd degree and converts the downward shift into a positive upward shift. -/ +lemma exists_pos_shift_down_not_isRealRooted_of_isRealRooted_of_odd_natDegree + {p : ℝ[X]} (hp_splits : p.Splits) (hp_pos : HasPosLeadingCoeff p) + (hdeg : 2 ≤ p.natDegree) (hodd : Odd p.natDegree) : + ∃ t : ℝ, 0 < t ∧ ¬ ((p - C t) ≠ 0 ∧ (p - C t).Splits) := by + let q : ℝ[X] := -(p.comp (-X)) + have hpow : (-1 : ℝ) ^ p.natDegree = -1 := hodd.neg_one_pow + have hq_splits : q.Splits := by + dsimp [q] + exact hp_splits.comp_neg_X.neg + have hq_pos : HasPosLeadingCoeff q := by + simpa [q, HasPosLeadingCoeff, hpow] using hp_pos + have hq_natDegree : q.natDegree = p.natDegree := by + dsimp [q] + rw [Polynomial.natDegree_neg, + Polynomial.natDegree_comp_eq_of_mul_ne_zero (by simp [hp_pos.ne_zero])] + simp + obtain ⟨t, ht_pos, ht_bad⟩ := + exists_pos_shift_not_isRealRooted_of_isRealRooted_of_natDegree_ge_two + hq_splits hq_pos (by rw [hq_natDegree]; exact hdeg) + refine ⟨t, ht_pos, ?_⟩ + intro hdown + apply ht_bad + have hcomp_ne : (p - C t).comp (-X) ≠ 0 := by + rw [ne_eq, Polynomial.comp_eq_zero_iff] + simp [hdown.1] + have hshift : + C t + q = -((p - C t).comp (-X)) := by + dsimp [q] + rw [Polynomial.sub_comp, Polynomial.C_comp] + ring + rw [hshift] + exact ⟨neg_ne_zero.mpr hcomp_ne, hdown.2.comp_neg_X.neg⟩ + +/-- A positive downward constant shift destroys real-rootedness for every +positive-leading real-rooted polynomial of degree at least three. -/ +lemma exists_pos_shift_down_not_isRealRooted_of_isRealRooted_of_natDegree_ge_three + {p : ℝ[X]} (hp_splits : p.Splits) (hp_pos : HasPosLeadingCoeff p) + (hdeg : 3 ≤ p.natDegree) : + ∃ t : ℝ, 0 < t ∧ ¬ ((p - C t) ≠ 0 ∧ (p - C t).Splits) := by + classical + by_cases hthree : p.natDegree = 3 + · exact + exists_pos_shift_down_not_isRealRooted_of_isRealRooted_of_odd_natDegree + hp_splits hp_pos (by lia) (by norm_num [hthree]) + have hfour : 4 ≤ p.natDegree := by + lia + let t : ℝ := + p.derivative.roots.toFinset.sum (fun c => |p.eval c|) + 1 + have ht_pos : 0 < t := by + dsimp [t] + positivity + refine ⟨t, ht_pos, ?_⟩ + intro hshift + have hC_deg : (C t : ℝ[X]).natDegree < p.natDegree := by + simp only [natDegree_C] + lia + have hshift_deg : (p - C t).natDegree = p.natDegree := + natDegree_sub_eq_left_of_natDegree_lt hC_deg + have hshift_pos : HasPosLeadingCoeff (p - C t) := by + unfold HasPosLeadingCoeff at hp_pos ⊢ + rw [leadingCoeff_sub_of_degree_lt (degree_lt_degree hC_deg)] + exact hp_pos + have hshift_four : 4 ≤ (p - C t).natDegree := by + rw [hshift_deg] + exact hfour + obtain ⟨c, hc_derivative, hc_nonneg⟩ := + exists_derivative_root_eval_nonneg_of_four_le_natDegree + hshift.2 hshift_pos hshift_four + have hc_derivative_p : c ∈ p.derivative.roots := by + simpa only [derivative_sub, derivative_C, sub_zero] using hc_derivative + have hc_finset : c ∈ p.derivative.roots.toFinset := + Multiset.mem_toFinset.mpr hc_derivative_p + have hc_bound : + |p.eval c| ≤ + p.derivative.roots.toFinset.sum (fun x => |p.eval x|) := + Finset.single_le_sum + (f := fun x => |p.eval x|) (fun x _ => abs_nonneg _) hc_finset + have hc_neg : (p - C t).eval c < 0 := by + rw [eval_sub, eval_C] + dsimp [t] + linarith [le_abs_self (p.eval c)] + exact (not_lt_of_ge hc_nonneg) hc_neg + + lemma exists_shift_not_isRealRooted_of_isRealRooted_of_natDegree_ge_two {p : ℝ[X]} (hp_splits : p.Splits) (hp_pos : HasPosLeadingCoeff p) (hdeg : 2 ≤ p.natDegree) : diff --git a/RealRooted/ReflectedRootCountLocalConstancy.lean b/RealRooted/ReflectedRootCountLocalConstancy.lean new file mode 100644 index 00000000..fb9e6e94 --- /dev/null +++ b/RealRooted/ReflectedRootCountLocalConstancy.lean @@ -0,0 +1,152 @@ +import RealRooted.DegreeDropReversal +import RealRooted.Linear +import RealRooted.PositiveParameterLocalLowerCount + +/-! +# Root-count local constancy through degree drops + +Reflection at a common degree bound turns a possible leading-degree drop into +zero-root padding. When the original affine family is nonzero at the left +endpoint of a positive interval, the reflected family therefore has constant +degree, so the existing analytic local-constancy theorem applies. +-/ + +open Polynomial + +namespace RealRooted + +open DegreeDropReversal + +/-- Root counts in `(0, b)` are constant along a split affine family when the +family stays nonzero at both interval endpoints, even if its degree drops. -/ +theorem rightFamily_card_roots_Ioo_zero_eq_zero_param_of_degree_bound + {f g : ℝ[X]} {b μ : ℝ} (hb : 0 < b) (hμ : 0 < μ) {N : ℕ} + (hN : ∀ η ∈ Set.Icc (0 : ℝ) μ, (f + C η * g).natDegree ≤ N) + (hzero : ∀ η ∈ Set.Icc (0 : ℝ) μ, (f + C η * g).coeff 0 ≠ 0) + (hsplit : ∀ η ∈ Set.Icc (0 : ℝ) μ, (f + C η * g).Splits) + (hbroot : ∀ η ∈ Set.Icc (0 : ℝ) μ, ¬ (f + C η * g).IsRoot b) : + ((f + C μ * g).roots.filter (fun r ↦ 0 < r ∧ r < b)).card = + (f.roots.filter (fun r ↦ 0 < r ∧ r < b)).card := by + have hzero_mem : (0 : ℝ) ∈ Set.Icc (0 : ℝ) μ := ⟨le_rfl, hμ.le⟩ + have hμ_mem : μ ∈ Set.Icc (0 : ℝ) μ := ⟨hμ.le, le_rfl⟩ + have hfN : f.natDegree ≤ N := by + simpa using hN 0 hzero_mem + have hfzero : f.coeff 0 ≠ 0 := by + simpa using hzero 0 hzero_mem + have hf_split : f.Splits := by + simpa using hsplit 0 hzero_mem + have hreflect_degree : ∀ η ∈ Set.Icc (0 : ℝ) μ, + (reflect N f + C η * reflect N g).natDegree = + (reflect N f + C (0 : ℝ) * reflect N g).natDegree := by + intro η hη + calc + (reflect N f + C η * reflect N g).natDegree = + (reflect N (f + C η * g)).natDegree := by rw [reflect_add_C_mul] + _ = N := natDegree_reflect_eq_of_coeff_zero_ne (hN η hη) (hzero η hη) + _ = (reflect N f).natDegree := + (natDegree_reflect_eq_of_coeff_zero_ne hfN hfzero).symm + _ = (reflect N f + C (0 : ℝ) * reflect N g).natDegree := by simp + have hreflect_split : ∀ η ∈ Set.Icc (0 : ℝ) μ, + (reflect N f + C η * reflect N g).Splits := by + intro η hη + rw [← reflect_add_C_mul] + exact splits_reflect_of_splits (hsplit η hη) (hN η hη) + have hreflect_not_root : ∀ η ∈ Set.Icc (0 : ℝ) μ, + ¬ (reflect N f + C η * reflect N g).IsRoot b⁻¹ := by + intro η hη + rw [← reflect_add_C_mul] + exact (not_congr (isRoot_reflect_inv_iff hb.ne' (hN η hη))).mpr + (hbroot η hη) + have hreflect_count := + rightFamily_card_roots_gt_eq_zero_param_of_constant_degree + (f := reflect N f) (g := reflect N g) (x := b⁻¹) (hμ_pos := hμ) + hreflect_degree hreflect_split hreflect_not_root + have hcount : + ((reflect N (f + C μ * g)).roots.filter (b⁻¹ < ·)).card = + ((reflect N f).roots.filter (b⁻¹ < ·)).card := by + simpa only [reflect_add_C_mul] using hreflect_count + have hμ_transport := card_roots_reflect_Ioi + (p := f + C μ * g) (hsplit μ hμ_mem) (hzero μ hμ_mem) + (hN μ hμ_mem) (a := b⁻¹) (inv_pos.mpr hb) + have hf_transport := card_roots_reflect_Ioi + (p := f) hf_split hfzero hfN (a := b⁻¹) (inv_pos.mpr hb) + calc + ((f + C μ * g).roots.filter (fun r ↦ 0 < r ∧ r < b)).card = + ((reflect N (f + C μ * g)).roots.filter (b⁻¹ < ·)).card := by + simpa using hμ_transport.symm + _ = ((reflect N f).roots.filter (b⁻¹ < ·)).card := hcount + _ = (f.roots.filter (fun r ↦ 0 < r ∧ r < b)).card := by + simpa using hf_transport + +/-- Root counts in any bounded open interval are constant along a split affine +family whose interval endpoints stay root-free, even if its degree drops. -/ +theorem rightFamily_card_roots_Ioo_eq_zero_param_of_degree_bound + {f g : ℝ[X]} {a b μ : ℝ} (hab : a < b) (hμ : 0 < μ) {N : ℕ} + (hN : ∀ η ∈ Set.Icc (0 : ℝ) μ, (f + C η * g).natDegree ≤ N) + (haroot : ∀ η ∈ Set.Icc (0 : ℝ) μ, ¬ (f + C η * g).IsRoot a) + (hsplit : ∀ η ∈ Set.Icc (0 : ℝ) μ, (f + C η * g).Splits) + (hbroot : ∀ η ∈ Set.Icc (0 : ℝ) μ, ¬ (f + C η * g).IsRoot b) : + ((f + C μ * g).roots.filter (fun r ↦ a < r ∧ r < b)).card = + (f.roots.filter (fun r ↦ a < r ∧ r < b)).card := by + let f' := f.comp (X + C a) + let g' := g.comp (X + C a) + have hfamily_comp (eta : ℝ) : + f' + C eta * g' = (f + C eta * g).comp (X + C a) := by + simp [f', g', Polynomial.add_comp, Polynomial.mul_comp] + have hN' : ∀ eta ∈ Set.Icc (0 : ℝ) μ, (f' + C eta * g').natDegree ≤ N := by + intro eta heta + rw [hfamily_comp, Polynomial.natDegree_comp] + simpa using hN eta heta + have hzero' : ∀ eta ∈ Set.Icc (0 : ℝ) μ, (f' + C eta * g').coeff 0 ≠ 0 := by + intro eta heta + rw [hfamily_comp] + simpa [Polynomial.coeff_zero_eq_eval_zero, Polynomial.eval_comp] using + haroot eta heta + have hsplit' : ∀ eta ∈ Set.Icc (0 : ℝ) μ, (f' + C eta * g').Splits := by + intro eta heta + rw [hfamily_comp] + exact (hsplit eta heta).comp_X_add_C a + have hbroot' : ∀ eta ∈ Set.Icc (0 : ℝ) μ, + ¬ (f' + C eta * g').IsRoot (b - a) := by + intro eta heta + rw [hfamily_comp] + intro hroot + apply hbroot eta heta + change eval b (f + C eta * g) = 0 + change eval (b - a) ((f + C eta * g).comp (X + C a)) = 0 at hroot + simpa [Polynomial.eval_comp] using hroot + have hshifted := rightFamily_card_roots_Ioo_zero_eq_zero_param_of_degree_bound + (f := f') (g := g') (b := b - a) (sub_pos.mpr hab) hμ + hN' hzero' hsplit' hbroot' + have htop := card_roots_comp_X_add_C_Ioo (f + C μ * g) a b + have hbase := card_roots_comp_X_add_C_Ioo f a b + calc + ((f + C μ * g).roots.filter (fun r ↦ a < r ∧ r < b)).card = + (((f + C μ * g).comp (X + C a)).roots.filter + (fun r ↦ 0 < r ∧ r < b - a)).card := htop.symm + _ = ((f' + C μ * g').roots.filter (fun r ↦ 0 < r ∧ r < b - a)).card := by + rw [hfamily_comp] + _ = (f'.roots.filter (fun r ↦ 0 < r ∧ r < b - a)).card := hshifted + _ = (f.roots.filter (fun r ↦ a < r ∧ r < b)).card := hbase + +/-- Root counts in a bounded open interval are constant along a split affine +family whose endpoints stay root-free, with the common degree bound inferred +from the two endpoint polynomials. -/ +theorem rightFamily_card_roots_Ioo_eq_zero_param + {f g : ℝ[X]} {a b μ : ℝ} (hab : a < b) (hμ : 0 < μ) + (haroot : ∀ η ∈ Set.Icc (0 : ℝ) μ, ¬ (f + C η * g).IsRoot a) + (hsplit : ∀ η ∈ Set.Icc (0 : ℝ) μ, (f + C η * g).Splits) + (hbroot : ∀ η ∈ Set.Icc (0 : ℝ) μ, ¬ (f + C η * g).IsRoot b) : + ((f + C μ * g).roots.filter (fun r ↦ a < r ∧ r < b)).card = + (f.roots.filter (fun r ↦ a < r ∧ r < b)).card := by + apply rightFamily_card_roots_Ioo_eq_zero_param_of_degree_bound + (N := max f.natDegree g.natDegree) hab hμ + · intro η _ + exact (Polynomial.natDegree_add_le _ _).trans + (max_le (le_max_left _ _) + ((Polynomial.natDegree_C_mul_le η g).trans (le_max_right _ _))) + · exact haroot + · exact hsplit + · exact hbroot + +end RealRooted diff --git a/RealRooted/RootMatchingSort.lean b/RealRooted/RootMatchingSort.lean new file mode 100644 index 00000000..6242e44d --- /dev/null +++ b/RealRooted/RootMatchingSort.lean @@ -0,0 +1,107 @@ +import RealRooted.LiuOppositeSigns +import RealRooted.Mathlib.Data.Multiset.Rel + +/-! +# Sorted root matching + +An arbitrary close perfect matching of two real multisets can be uncrossed into +a close pointwise matching of their ascending sorts. This is the finite +ordered-root input for limiting interlacing and root-count inequalities. +-/ + +namespace RealRooted + +open LiuOppositeSigns Polynomial + +/-- A close multiset matching pairs corresponding ascending order statistics. -/ +theorem forall₂_sort_of_rel_abs_sub_lt + {s t : Multiset ℝ} {ρ : ℝ} + (hrel : Multiset.Rel (fun x y : ℝ => |y - x| < ρ) s t) : + List.Forall₂ (fun x y : ℝ => |y - x| < ρ) + (s.sort (· ≤ ·)) (t.sort (· ≤ ·)) := by + refine Multiset.Rel.forall₂_sort ?_ hrel + intro a c b d hac hbd had hcb + simp only [abs_lt] at had hcb ⊢ + constructor <;> constructor <;> linarith + +/-- A close multiset matching pairs corresponding descending order statistics. -/ +theorem forall₂_sort_ge_of_rel_abs_sub_lt + {s t : Multiset ℝ} {ρ : ℝ} + (hrel : Multiset.Rel (fun x y : ℝ => |y - x| < ρ) s t) : + List.Forall₂ (fun x y : ℝ => |y - x| < ρ) + (s.sort (· ≥ ·)) (t.sort (· ≥ ·)) := by + change List.Forall₂ + (fun x y : OrderDual ℝ => + |OrderDual.ofDual y - OrderDual.ofDual x| < ρ) + ((show Multiset (OrderDual ℝ) from s).sort (· ≤ ·)) + ((show Multiset (OrderDual ℝ) from t).sort (· ≤ ·)) + apply Multiset.Rel.forall₂_sort + · intro a c b d hac hbd had hcb + change OrderDual.ofDual c ≤ OrderDual.ofDual a at hac + change OrderDual.ofDual d ≤ OrderDual.ofDual b at hbd + simp only [abs_lt] at had hcb ⊢ + constructor <;> constructor <;> linarith + · exact hrel + +/-- A largest root is the head of the descending root list. -/ +theorem LiuOppositeSigns.IsLargestRoot.roots_sort_ge_eq_cons + {p : ℝ[X]} {r : ℝ} (hp_ne : p ≠ 0) (h : IsLargestRoot p r) : + p.roots.sort (· ≥ ·) = + r :: (deleteRootFactor p r).roots.sort (· ≥ ·) := by + rw [h.roots_eq_singleton_add_roots_deleteRootFactor hp_ne, + Multiset.singleton_add] + apply Multiset.sort_cons + intro x hx + exact h.root_deleteRootFactor_le hp_ne + ((Polynomial.mem_roots (h.deleteRootFactor_ne_zero hp_ne)).mp hx) + +/-- Deleting matched largest roots preserves the matching of descending roots. -/ +theorem forall₂_sort_ge_deleteRootFactor_of_roots_rel + {p q : ℝ[X]} {r s ρ : ℝ} (hp_ne : p ≠ 0) (hq_ne : q ≠ 0) + (hr : IsLargestRoot p r) (hs : IsLargestRoot q s) + (hrel : Multiset.Rel + (fun x y : ℝ => |y - x| < ρ) p.roots q.roots) : + List.Forall₂ (fun x y : ℝ => |y - x| < ρ) + ((deleteRootFactor p r).roots.sort (· ≥ ·)) + ((deleteRootFactor q s).roots.sort (· ≥ ·)) := by + have hsort := forall₂_sort_ge_of_rel_abs_sub_lt hrel + rw [hr.roots_sort_ge_eq_cons hp_ne, + hs.roots_sort_ge_eq_cons hq_ne] at hsort + exact (List.forall₂_cons.mp hsort).2 + +/-- A weak scalar inequality is closed under arbitrarily close approximations. -/ +theorem le_of_forall_pos_exists_close_le {x y : ℝ} + (h : ∀ ρ : ℝ, 0 < ρ → + ∃ x' y' : ℝ, |x' - x| < ρ ∧ |y' - y| < ρ ∧ x' ≤ y') : + x ≤ y := by + apply le_of_forall_pos_le_add + intro ε hε + obtain ⟨x', y', hx, hy, hxy⟩ := h (ε / 2) (half_pos hε) + rw [abs_lt] at hx hy + linarith + +/-- Pointwise list inequalities are closed under arbitrarily close approximations. -/ +theorem forall₂_le_of_forall_pos_exists_close + {xs ys : List ℝ} + (h : ∀ ρ : ℝ, 0 < ρ → + ∃ xs' ys' : List ℝ, + List.Forall₂ (fun x x' => |x' - x| < ρ) xs xs' ∧ + List.Forall₂ (fun y y' => |y' - y| < ρ) ys ys' ∧ + List.Forall₂ (· ≤ ·) xs' ys') : + List.Forall₂ (· ≤ ·) xs ys := by + have hlen : xs.length = ys.length := by + obtain ⟨xs', ys', hxs, hys, hxy⟩ := h 1 zero_lt_one + exact hxs.length_eq.trans (hxy.length_eq.trans hys.length_eq.symm) + apply List.forall₂_of_length_eq_of_get hlen + intro i hix hiy + apply le_of_forall_pos_exists_close_le + intro ρ hρ + obtain ⟨xs', ys', hxs, hys, hxy⟩ := h ρ hρ + have hix' : i < xs'.length := by + simpa only [hxs.length_eq] using hix + have hiy' : i < ys'.length := by + simpa only [hys.length_eq] using hiy + exact ⟨xs'.get ⟨i, hix'⟩, ys'.get ⟨i, hiy'⟩, + hxs.get hix hix', hys.get hiy hiy', hxy.get hix' hiy'⟩ + +end RealRooted diff --git a/RealRooted/RootMultiplicityMatching.lean b/RealRooted/RootMultiplicityMatching.lean index 68ef374c..62e648d4 100644 --- a/RealRooted/RootMultiplicityMatching.lean +++ b/RealRooted/RootMultiplicityMatching.lean @@ -142,6 +142,22 @@ theorem exists_rel_le_of_forall_le_count {s t : Multiset ℝ} {δ : ℝ} · exact le_trans (Finset.sum_le_sum fun a ha => (hcluster a ha).1) (sum_filter_ball_le hsep) +/-- Local multiplicity lower bounds give a full proximity matching when the +source and target multisets have the same cardinality. -/ +theorem rel_of_forall_le_count_of_card_eq {s t : Multiset ℝ} {δ : ℝ} + (hsep : ∀ a ∈ s.toFinset, ∀ b ∈ s.toFinset, + a ≠ b → 2 * δ ≤ |a - b|) + (hcount : ∀ a ∈ s.toFinset, + s.count a ≤ (t.filter (fun q => |q - a| < δ)).card) + (hcard : t.card = s.card) : + Rel (fun r q => |q - r| < δ) s t := by + obtain ⟨u, hu, hrel⟩ := + exists_rel_le_of_forall_le_count hsep hcount + have hu_card : u.card = t.card := by + simpa [hcard] using (card_eq_card_of_rel hrel).symm + have hut : u = t := eq_of_le_of_card_le hu hu_card.ge + rwa [hut] at hrel + /-- Finite local-count bridge for same-cardinality perturbations. @@ -158,12 +174,8 @@ theorem card_filter_gt_eq_of_forall_le_count_and_card_eq s.count a ≤ (t.filter (fun q => |q - a| < δ)).card) (hcard : t.card = s.card) : (t.filter (fun q => x < q)).card = (s.filter (fun r => x < r)).card := by - obtain ⟨u, hu, hRel⟩ := - exists_rel_le_of_forall_le_count hsep_centers hcount - have hu_card : u.card = t.card := by - simpa [hcard] using (Multiset.card_eq_card_of_rel hRel).symm - have hut : u = t := Multiset.eq_of_le_of_card_le hu hu_card.ge - rw [hut] at hRel + have hRel := + rel_of_forall_le_count_of_card_eq hsep_centers hcount hcard have hgt : (s.filter (fun r => x < r)).card ≤ (t.filter (fun q => x < q)).card := card_filter_gt_le_of_rel_abs_sub_lt hsep_x hRel diff --git a/RealRooted/RootOrderBridge.lean b/RealRooted/RootOrderBridge.lean index 4fed1d91..e34d0780 100644 --- a/RealRooted/RootOrderBridge.lean +++ b/RealRooted/RootOrderBridge.lean @@ -157,6 +157,94 @@ theorem count_diff_le_one_of_rootCrossing grind grind +/-- Converse of `succRootCrossing_of_count_le_two`. + +If `N` has one more element than `M` and their descending sorted lists satisfy +the successor-degree crossing inequalities, then the lower count for `M` is at +most the lower count for `N`, while the latter is at most two larger. -/ +theorem count_le_two_of_succRootCrossing + {M N : Multiset ℝ} {d : ℕ} + (hM : M.card = d) (hN : N.card = d + 1) + (hcross : + (∀ j, 1 ≤ j → j ≤ d → + ((N.sort (· ≤ ·)).reverse).getD j 0 ≤ + ((M.sort (· ≤ ·)).reverse).getD (j - 1) 0) ∧ + (∀ j, 1 ≤ j → j < d → + ((M.sort (· ≤ ·)).reverse).getD j 0 ≤ + ((N.sort (· ≤ ·)).reverse).getD (j - 1) 0)) : + ∀ x : ℝ, + ((M.filter (· ≤ x)).card : ℤ) - (N.filter (· ≤ x)).card ≤ 0 ∧ + ((N.filter (· ≤ x)).card : ℤ) - (M.filter (· ≤ x)).card ≤ 2 := by + set sM := M.sort (· ≤ ·) + set sN := N.sort (· ≤ ·) + have hM_sorted : sM.Pairwise (· ≤ ·) := Multiset.pairwise_sort _ _ + have hN_sorted : sN.Pairwise (· ≤ ·) := Multiset.pairwise_sort _ _ + have hsM : sM.length = d := by + simpa [sM] using hM + have hsN : sN.length = d + 1 := by + simpa [sN] using hN + have hsM_eq : Multiset.ofList sM = M := Multiset.sort_eq M (· ≤ ·) + have hsN_eq : Multiset.ofList sN = N := Multiset.sort_eq N (· ≤ ·) + have h_helper := sorted_getElem_le_iff_lt_card_filter + have h_reverse_getD (l : List ℝ) (hl : l.length = d) (i : ℕ) (hi : i < d) : + l.reverse.getD i 0 = l[d - 1 - i]! := by + grind + have h_reverse_getD_succ (l : List ℝ) (hl : l.length = d + 1) + (i : ℕ) (hi : i < d + 1) : + l.reverse.getD i 0 = l[d - i]! := by + simp only [List.getD_eq_getElem?_getD, List.length_reverse, hl, + getElem?_pos, hi, List.getElem_reverse, Option.getD_some] + have hidx : d + 1 - 1 - i = d - i := by lia + have hdi : d - i < l.length := by lia + simp only [hidx, getElem!_pos, hdi] + have hint1 : ∀ i, i < d → sN[i]! ≤ sM[i]! := by + grind + have hint2 : ∀ i, i + 1 < d → sM[i]! ≤ sN[i + 2]! := by + intro i hi + let j := d - 1 - i + have hj_pos : 1 ≤ j := by + dsimp [j] + lia + have hj_lt : j < d := by + dsimp [j] + lia + have hjN : j - 1 < d + 1 := by lia + have h := hcross.2 j hj_pos hj_lt + rw [h_reverse_getD sM hsM j hj_lt, + h_reverse_getD_succ sN hsN (j - 1) hjN] at h + have hleft : d - 1 - j = i := by + dsimp [j] + lia + have hright : d - (j - 1) = i + 2 := by + dsimp [j] + lia + simpa only [hleft, hright] using h + intro x + have ha_le_d : (M.filter (· ≤ x)).card ≤ d := + hM ▸ Multiset.card_le_card (Multiset.filter_le _ _) + have hb_le_succ : (N.filter (· ≤ x)).card ≤ d + 1 := + hN ▸ Multiset.card_le_card (Multiset.filter_le _ _) + have hab0 : (M.filter (· ≤ x)).card ≤ (N.filter (· ≤ x)).card := by + by_contra hcon + push Not at hcon + have hb_lt_d : (N.filter (· ≤ x)).card < d := by lia + have hMx : sM[(N.filter (· ≤ x)).card]! ≤ x := by + grind + have hNb : sN[(N.filter (· ≤ x)).card]! ≤ x := + le_trans (hint1 _ hb_lt_d) hMx + grind + have hba2 : + (N.filter (· ≤ x)).card ≤ (M.filter (· ≤ x)).card + 2 := by + by_contra hcon + push Not at hcon + have ha1_lt_d : (M.filter (· ≤ x)).card + 1 < d := by lia + have hNx : sN[(M.filter (· ≤ x)).card + 2]! ≤ x := by + grind + have hMa : sM[(M.filter (· ≤ x)).card]! ≤ x := + le_trans (hint2 _ ha1_lt_d) hNx + grind + grind + /-- Succ-degree version of `rootCrossing_of_count_diff_le_one`. If `N` has one more element than `M`, and at every lower threshold the count diff --git a/RealRooted/SameDegreeCountFromAnalytic.lean b/RealRooted/SameDegreeCountFromAnalytic.lean index 855e37b1..ed865ae9 100644 --- a/RealRooted/SameDegreeCountFromAnalytic.lean +++ b/RealRooted/SameDegreeCountFromAnalytic.lean @@ -57,17 +57,12 @@ theorem exists_eps_card_roots_gt_bounds_near_simple_root ((f + C ν * g).roots.filter (fun q ↦ |q - a| < ρ)).card := fun a ha ↦ by simp_all - obtain ⟨u, hu, hrel⟩ := - Multiset.exists_rel_le_of_forall_le_count (s := p.roots) - (t := (f + C ν * g).roots) hsep_centers hcount_local have hcard : (f + C ν * g).roots.card = p.roots.card := by simpa [hν_split.natDegree_eq_card_roots.symm, hp_split.natDegree_eq_card_roots.symm] using hν_deg - have hu_card : u.card = (f + C ν * g).roots.card := by - simpa [hcard] using (Multiset.card_eq_card_of_rel hrel).symm - have hu_eq : u = (f + C ν * g).roots := - Multiset.eq_of_le_of_card_le hu hu_card.ge - rw [hu_eq] at hrel + have hrel := + Multiset.rel_of_forall_le_count_of_card_eq + hsep_centers hcount_local hcard have hsep_gt : ∀ r ∈ p.roots, x < r → ρ ≤ |r - x| := fun r hr hxr => by have hr_ne : r ≠ x := ne_of_gt hxr exact le_trans (le_of_lt hρ_lt_η)