diff --git a/RealRooted.lean b/RealRooted.lean index bb9bdd522..bd8afd445 100644 --- a/RealRooted.lean +++ b/RealRooted.lean @@ -214,6 +214,7 @@ public import RealRooted.Challenges.PolyaFrequency.EdreiThoma public import RealRooted.Challenges.Roots.EnestromKakeya public import RealRooted.Challenges.Combinatorial.EulerBidiagonal public import RealRooted.Challenges.Combinatorial.EulerMultiplier +public import RealRooted.Challenges.Combinatorial.OrbitPerturbation public import RealRooted.Challenges.Combinatorial.Eulerian public import RealRooted.Challenges.Combinatorial.EulerianVariations public import RealRooted.Challenges.Combinatorial.LagTwoEulerianTriangles @@ -526,6 +527,10 @@ public import RealRooted.EulerOperator.Darboux.Basic public import RealRooted.EulerOperator.Darboux.Interlacing public import RealRooted.EulerOperator.Darboux.NegativeRoots public import RealRooted.EulerOperator.EulerMultiplier +public import RealRooted.EulerOperator.OrbitPerturbation +public import RealRooted.EulerOperator.OrbitPerturbationCayley +public import RealRooted.EulerOperator.OrbitPerturbationFamily +public import RealRooted.EulerOperator.OrbitPerturbationInterlacing public import RealRooted.EulerOperator.OrderNumerator.Basic public import RealRooted.EulerOperator.OrderNumerator.Preservation public import RealRooted.EulerOperator.Pencil diff --git a/RealRooted/Challenges/Combinatorial/OrbitPerturbation.lean b/RealRooted/Challenges/Combinatorial/OrbitPerturbation.lean new file mode 100644 index 000000000..2f32547e0 --- /dev/null +++ b/RealRooted/Challenges/Combinatorial/OrbitPerturbation.lean @@ -0,0 +1,114 @@ +module + +import RealRooted.EulerOperator.OrbitPerturbationCayley +import RealRooted.EulerOperator.OrbitPerturbationFamily + +/-! +# Monomial perturbations of the centered Euler orbit + + + + +# Monomial perturbations of the centered Euler orbit + +Let $s\ge1$ and $\kappa\ge s+4$. Let $Q_0=1$, $Q_1=1+2u$, +$Q_2=1+\kappa u+\kappa u^2$ and, for $n\ge3$, with $\theta=u\,\frac{d}{du}$, + +$$ +(n-2)Q_n=\bigl((2n-3)(2u+1)+(n-2)s(u+1)\theta\bigr)Q_{n-1} + -(n-1)(2u+1)\bigl((2u+1)+s(u+1)\theta\bigr)Q_{n-2}. +$$ + +Then every $Q_n$ has simple roots in $(-1,0)$, and $Q_n$ strictly +interlaces $Q_{n+1}$. The theorem accepts any sequence with these seeds and +this recurrence. + +**Proof idea.** With $x=2u+1$, $\alpha=s/2$ and $r=(\kappa-4)/(2s)\ge1/2$, +we have $Q_n=r\,p_n(x)+(1-r)x^n$, where $p_0=1$ and +$p_{n+1}=x\,p_n+\alpha(x^2-1)p_n'$. The polynomials $p_n$ have simple roots +in $(-1,1)$ with $p_n(\pm1)=(\pm1)^n$. For $n\ge5$ every critical value +satisfies $|p_n(c)|\ge1$. This holds for $p_5$ by explicit evaluation, and it +propagates from $p_n$ to $p_{n+1}$ through an inverse Bernstein inequality +$(1-x^2)p_n'(x)^2\ge n^2(1-p_n(x)^2)$ on $[-1,1]$. We prove that inequality +by comparing $p_n(\cos t)$ with a harmonic $a\cos(n(t-\varphi))$, following +Erdélyi, Hardin and Saff +([arXiv:1307.4056](https://arxiv.org/abs/1307.4056)). Degrees at most four +are checked directly. So $h_n=p_n+bx^n$ with $-1 + +This module is a catalog facade. The proofs live in +`RealRooted.EulerOperator.OrbitPerturbation`, +`RealRooted.EulerOperator.OrbitPerturbationInterlacing`, +`RealRooted.EulerOperator.OrbitPerturbationFamily` and +`RealRooted.EulerOperator.OrbitPerturbationCayley`. +-/ diff --git a/RealRooted/EulerOperator/OrbitPerturbation.lean b/RealRooted/EulerOperator/OrbitPerturbation.lean new file mode 100644 index 000000000..a079d4fb8 --- /dev/null +++ b/RealRooted/EulerOperator/OrbitPerturbation.lean @@ -0,0 +1,663 @@ +module + +public import RealRooted.RootLocation.Basic +public import RealRooted.SimpleRoots +public import RealRooted.Basic.ProperPosition + +import RealRooted.IntervalDifferential.LinearInsertion +import RealRooted.Mathlib.Algebra.Polynomial.Derivative +import RealRooted.Mathlib.Analysis.Polynomial.InverseBernstein +import Mathlib.Analysis.Calculus.Deriv.MeanValue +import Mathlib.Analysis.Calculus.Deriv.Polynomial +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# Binomial perturbations of a centered Euler-operator orbit + +We study the operator +`f ↦ X f + α (X² - 1) f'` and its orbit starting at `1`. The inverse +Bernstein estimate used later is deliberately kept as an explicit hypothesis; +see RealRooted issue #2513. +-/ + +@[expose] public section + +open Polynomial Set + +noncomputable section + +namespace RealRooted + +/-- The centered Euler step `f ↦ X f + α (X² - 1) f'`. -/ +def centeredEulerStep (α : ℝ) (f : ℝ[X]) : ℝ[X] := + X * f + C α * (X ^ 2 - 1) * f.derivative + +/-- The orbit of the centered Euler step starting from the constant polynomial `1`. -/ +def centeredEulerOrbit (α : ℝ) : ℕ → ℝ[X] + | 0 => 1 + | n + 1 => centeredEulerStep α (centeredEulerOrbit α n) + +@[simp] theorem centeredEulerOrbit_zero (α : ℝ) : centeredEulerOrbit α 0 = 1 := rfl + +@[simp] theorem centeredEulerOrbit_succ (α : ℝ) (n : ℕ) : + centeredEulerOrbit α (n + 1) = centeredEulerStep α (centeredEulerOrbit α n) := rfl + +@[simp] theorem centeredEulerStep_eval (α x : ℝ) (f : ℝ[X]) : + (centeredEulerStep α f).eval x = + x * f.eval x + α * (x ^ 2 - 1) * f.derivative.eval x := by + simp [centeredEulerStep] + +theorem centeredEulerStep_eval_one (α : ℝ) (f : ℝ[X]) : + (centeredEulerStep α f).eval 1 = f.eval 1 := by + simp [centeredEulerStep_eval] + +theorem centeredEulerStep_eval_neg_one (α : ℝ) (f : ℝ[X]) : + (centeredEulerStep α f).eval (-1) = -f.eval (-1) := by + simp [centeredEulerStep_eval] + +theorem centeredEulerStep_coeff_succ_natDegree + (α : ℝ) (f : ℝ[X]) : + (centeredEulerStep α f).coeff (f.natDegree + 1) = + (1 + α * f.natDegree) * f.leadingCoeff := by + rw [show centeredEulerStep α f = + X * (C 1 * f + (C 0 + C α * X) * f.derivative) - C α * f.derivative by + simp [centeredEulerStep] + ring] + rw [coeff_sub, coeff_X_mul, coeff_C_mul_add_affine_mul_derivative_natDegree, + coeff_C_mul, coeff_derivative, + coeff_eq_zero_of_natDegree_lt (by lia : f.natDegree < f.natDegree + 1 + 1)] + simp + +/-- Exact degree and leading coefficient of one centered Euler step. -/ +theorem centeredEulerStep_degree_leadingCoeff + {α : ℝ} {f : ℝ[X]} (hf : f ≠ 0) (hfactor : 0 < 1 + α * f.natDegree) : + (centeredEulerStep α f).natDegree = f.natDegree + 1 ∧ + (centeredEulerStep α f).leadingCoeff = + (1 + α * f.natDegree) * f.leadingCoeff := by + let A : ℝ[X] := C 1 * f + (C 0 + C α * X) * f.derivative + have htop : (1 + α * (f.natDegree : ℝ)) * f.leadingCoeff ≠ 0 := + mul_ne_zero hfactor.ne' (leadingCoeff_ne_zero.mpr hf) + have hA := natDegree_and_leadingCoeff_C_mul_add_affine_mul_derivative + f 1 0 α (by simpa using htop) + have hA0 : A ≠ 0 := by + intro hzero + have h := congrArg leadingCoeff hzero + rw [show A.leadingCoeff = (1 + α * (f.natDegree : ℝ)) * f.leadingCoeff by + simpa [A] using hA.2] at h + simpa using htop h + have hAdeg : A.natDegree = f.natDegree := by simpa [A] using hA.1 + have hrewrite : centeredEulerStep α f = X * A - C α * f.derivative := by + simp [centeredEulerStep, A] + ring + have hsmall : (C α * f.derivative).natDegree < (X * A).natDegree := by + have hder : (C α * f.derivative).natDegree ≤ f.natDegree - 1 := by + exact (natDegree_C_mul_le _ _).trans_eq f.natDegree_derivative + have hlt : (C α * f.derivative).natDegree < f.natDegree + 1 := by lia + have hXA : (X * A).natDegree = f.natDegree + 1 := by + simpa [hAdeg] using natDegree_X_mul hA0 + rwa [hXA] + rw [hrewrite, natDegree_sub_eq_left_of_natDegree_lt hsmall, + natDegree_X_mul hA0, hAdeg] + constructor + · rfl + · rw [leadingCoeff_sub_of_degree_lt (degree_lt_degree hsmall)] + simpa [A] using hA.2 + +/-- A positive centered Euler step raises the degree and preserves the leading sign. -/ +theorem centeredEulerStep_hasPosLeadingCoeff + {α : ℝ} {f : ℝ[X]} (hα : 0 < α) (hf : HasPosLeadingCoeff f) : + HasPosLeadingCoeff (centeredEulerStep α f) := by + rw [HasPosLeadingCoeff, (centeredEulerStep_degree_leadingCoeff hf.ne_zero (by positivity)).2] + exact mul_pos (by positivity) hf + +/-- One centered Euler step inserts one simple root in every gap and keeps all +roots in `(-1,1)`. -/ +theorem centeredEulerStep_roots + {α : ℝ} {f : ℝ[X]} (hα : 0 < α) + (hf : IsRealRootedIn (Ioo (-1 : ℝ) 1) f) (hsimple : HasSimpleRoots f) + (hf_pos : HasPosLeadingCoeff f) : + IsRealRootedIn (Ioo (-1 : ℝ) 1) (centeredEulerStep α f) ∧ + HasSimpleRoots (centeredEulerStep α f) := by + have hdegree := (centeredEulerStep_degree_leadingCoeff hf.ne_zero (by positivity)).1 + have hnd := hsimple.roots_nodup + have hinside : ∀ z ∈ f.roots, -1 < z ∧ z < 1 := hf.2.2 + have hresult := IntervalDifferential.splits_nodup_interval_of_root_derivative_signs + hf.splits hf.ne_zero hnd hinside hdegree + (fun z hz => by + rw [centeredEulerStep_eval] + have hz0 : f.eval z = 0 := ((mem_roots hf.ne_zero).mp hz).eq_zero + rw [hz0] + have hzmem := hinside z hz + have hsquare : z ^ 2 - 1 < 0 := by + nlinarith [mul_pos (sub_pos.mpr hzmem.2) (by linarith : 0 < 1 + z)] + have hder : f.derivative.eval z ≠ 0 := + hsimple.eval_derivative_ne_zero ((mem_roots hf.ne_zero).mp hz) + have haf : α * (z ^ 2 - 1) < 0 := mul_neg_of_pos_of_neg hα hsquare + nlinarith [mul_neg_of_neg_of_pos haf (sq_pos_of_ne_zero hder)]) + (by + rw [centeredEulerStep_eval_neg_one] + have hne : f.eval (-1) ≠ 0 := by + intro hzero + have hroot : f.IsRoot (-1) := hzero + exact (lt_irrefl (-1 : ℝ)) (hf.mem_of_isRoot hroot).1 + nlinarith [sq_pos_of_ne_zero hne]) + (by + rw [centeredEulerStep_eval_one] + have hne : f.eval 1 ≠ 0 := by + intro hzero + have hroot : f.IsRoot 1 := hzero + exact (lt_irrefl (1 : ℝ)) (hf.mem_of_isRoot hroot).2 + nlinarith [sq_pos_of_ne_zero hne]) + refine ⟨⟨(centeredEulerStep_hasPosLeadingCoeff hα hf_pos).ne_zero, + hresult.1, hresult.2.2⟩, ?_⟩ + exact HasSimpleRoots.of_roots_nodup + (centeredEulerStep_hasPosLeadingCoeff hα hf_pos).ne_zero hresult.2.1 + +@[simp] theorem centeredEulerOrbit_eval_one (α : ℝ) (n : ℕ) : + (centeredEulerOrbit α n).eval 1 = 1 := by + induction n with + | zero => simp + | succ n ih => simpa using congrArg (fun x : ℝ => x) ih + +@[simp] theorem centeredEulerOrbit_eval_neg_one (α : ℝ) (n : ℕ) : + (centeredEulerOrbit α n).eval (-1) = (-1 : ℝ) ^ n := by + induction n with + | zero => simp + | succ n ih => simp [pow_succ, ih] + +/-- The first centered Euler orbit polynomial. -/ +private theorem centeredEulerOrbit_one (α : ℝ) : + centeredEulerOrbit α 1 = X := by + simp [centeredEulerOrbit, centeredEulerStep] + +/-- The second centered Euler orbit polynomial. -/ +private theorem centeredEulerOrbit_two (α : ℝ) : + centeredEulerOrbit α 2 = C (1 + α) * X ^ 2 - C α := by + rw [show centeredEulerOrbit α 2 = centeredEulerStep α (centeredEulerOrbit α 1) by rfl, + centeredEulerOrbit_one] + simp [centeredEulerStep] + ring + +/-- The third centered Euler orbit polynomial. -/ +private theorem centeredEulerOrbit_three (α : ℝ) : + centeredEulerOrbit α 3 = + C ((1 + α) * (1 + 2 * α)) * X ^ 3 - C (α * (3 + 2 * α)) * X := by + rw [show centeredEulerOrbit α 3 = centeredEulerStep α (centeredEulerOrbit α 2) by rfl, + centeredEulerOrbit_two] + simp [centeredEulerStep, derivative_sub, derivative_mul, derivative_pow, map_ofNat] + ring + +/-- The fourth centered Euler orbit polynomial. -/ +private theorem centeredEulerOrbit_four (α : ℝ) : + centeredEulerOrbit α 4 = + C ((1 + α) * (1 + 2 * α) * (1 + 3 * α)) * X ^ 4 - + C (2 * α * (1 + α) * (3 + 4 * α)) * X ^ 2 + + C (α ^ 2 * (3 + 2 * α)) := by + rw [show centeredEulerOrbit α 4 = centeredEulerStep α (centeredEulerOrbit α 3) by rfl, + centeredEulerOrbit_three] + simp [centeredEulerStep, derivative_add, derivative_sub, derivative_mul, derivative_pow, + map_ofNat] + ring + +/-- The explicit degree-five polynomial in the centered Euler orbit. -/ +theorem centeredEulerOrbit_five (α : ℝ) : + centeredEulerOrbit α 5 = + C (24 * α ^ 4 + 50 * α ^ 3 + 35 * α ^ 2 + 10 * α + 1) * X ^ 5 - + C (40 * α ^ 4 + 80 * α ^ 3 + 50 * α ^ 2 + 10 * α) * X ^ 3 + + C (16 * α ^ 4 + 30 * α ^ 3 + 15 * α ^ 2) * X := by + rw [show centeredEulerOrbit α 5 = centeredEulerStep α (centeredEulerOrbit α 4) by rfl, + centeredEulerOrbit_four] + simp [centeredEulerStep, derivative_add, derivative_sub, derivative_mul, derivative_pow, + map_ofNat] + ring + +/-- At six fixed points, the degree-five centered Euler orbit has alternating +values of absolute value at least one. -/ +theorem centeredEulerOrbit_five_alternation {α : ℝ} (hα : 1 / 2 ≤ α) (i : Fin 6) : + 1 ≤ (-1 : ℝ) ^ (5 - (i : ℕ)) * (centeredEulerOrbit α 5).eval + (![-1, -5 / 6, -1 / 3, 1 / 3, 5 / 6, 1] i) := by + let β := α - 1 / 2 + have hβ : 0 ≤ β := by + dsimp [β] + linarith + have hβ_two : 0 ≤ β ^ 2 := pow_nonneg hβ 2 + have hβ_three : 0 ≤ β ^ 3 := pow_nonneg hβ 3 + have hβ_four : 0 ≤ β ^ 4 := pow_nonneg hβ 4 + have hα_eq : α = 1 / 2 + β := by + dsimp [β] + ring + rw [centeredEulerOrbit_five] + fin_cases i <;> norm_num [hα_eq] <;> + nlinarith [hβ_two, hβ_three, hβ_four] + +/-- Every row of the centered Euler orbit has positive leading coefficient. -/ +theorem centeredEulerOrbit_hasPosLeadingCoeff {α : ℝ} (hα : 0 < α) (n : ℕ) : + HasPosLeadingCoeff (centeredEulerOrbit α n) := by + induction n with + | zero => simp [HasPosLeadingCoeff] + | succ n ih => exact centeredEulerStep_hasPosLeadingCoeff hα ih + +/-- The centered Euler orbit has exact degree equal to its index. -/ +theorem centeredEulerOrbit_natDegree {α : ℝ} (hα : 0 < α) (n : ℕ) : + (centeredEulerOrbit α n).natDegree = n := by + induction n with + | zero => simp + | succ n ih => + rw [centeredEulerOrbit_succ, + (centeredEulerStep_degree_leadingCoeff + (centeredEulerOrbit_hasPosLeadingCoeff hα n).ne_zero (by positivity)).1, ih] + +/-- Every row of the centered Euler orbit has simple roots in `(-1,1)`. -/ +theorem centeredEulerOrbit_roots {α : ℝ} (hα : 0 < α) (n : ℕ) : + IsRealRootedIn (Ioo (-1 : ℝ) 1) (centeredEulerOrbit α n) ∧ + HasSimpleRoots (centeredEulerOrbit α n) := by + induction n with + | zero => + exact ⟨IsRealRootedIn.one, hasSimpleRoots_of_natDegree_le_one one_ne_zero (by simp)⟩ + | succ n ih => + exact centeredEulerStep_roots hα ih.1 ih.2 + (centeredEulerOrbit_hasPosLeadingCoeff hα n) + +/-- Degree, leading sign, root location, simplicity, and endpoint normalization +for the centered Euler orbit in the parameter range of issue #2513. -/ +theorem centeredEulerOrbit_package {α : ℝ} (hα : 1 / 2 ≤ α) (n : ℕ) : + (centeredEulerOrbit α n).natDegree = n ∧ + HasPosLeadingCoeff (centeredEulerOrbit α n) ∧ + IsRealRootedIn (Ioo (-1 : ℝ) 1) (centeredEulerOrbit α n) ∧ + HasSimpleRoots (centeredEulerOrbit α n) ∧ + (centeredEulerOrbit α n).eval 1 = 1 ∧ + (centeredEulerOrbit α n).eval (-1) = (-1 : ℝ) ^ n := by + have hαpos : 0 < α := lt_of_lt_of_le (by norm_num) hα + exact ⟨centeredEulerOrbit_natDegree hαpos n, + centeredEulerOrbit_hasPosLeadingCoeff hαpos n, + (centeredEulerOrbit_roots hαpos n).1, + (centeredEulerOrbit_roots hαpos n).2, + centeredEulerOrbit_eval_one α n, + centeredEulerOrbit_eval_neg_one α n⟩ + +/-! ### Propagation of large critical values -/ + +/-- Roots in `(-1, 1)` in the `IsRealRootedIn` form give the root count used by the inverse +Bernstein inequality. -/ +theorem card_roots_filter_Ioo_of_isRealRootedIn {f : ℝ[X]} + (hf : IsRealRootedIn (Ioo (-1 : ℝ) 1) f) : + (f.roots.filter (· ∈ Ioo (-1 : ℝ) 1)).card = f.natDegree := by + rw [Multiset.filter_eq_self.mpr hf.2.2, ← hf.2.1.natDegree_eq_card_roots] + +/-- Signed form of alternation points ending at `p (C n) = 1`. -/ +private theorem signed_alternation {p : ℝ[X]} {n : ℕ} {C : ℕ → ℝ} (hCn : C n = 1) + (hone : p.eval 1 = 1) (hcrit : ∀ k ≤ n, 1 ≤ |p.eval (C k)|) + (hprod : ∀ k < n, p.eval (C k) * p.eval (C (k + 1)) < 0) : + ∀ k ≤ n, 1 ≤ (-1 : ℝ) ^ (n - k) * p.eval (C k) := by + have key : ∀ d k, k + d = n → 1 ≤ (-1 : ℝ) ^ (n - k) * p.eval (C k) := by + intro d + induction d with + | zero => + intro k hk + rw [show k = n by lia, Nat.sub_self, pow_zero, one_mul, hCn, hone] + | succ d ih => + intro k hk + have h1 := ih (k + 1) (by lia) + have h2 := hprod k (by lia) + have h3 := hcrit k (by lia) + rw [show n - k = n - (k + 1) + 1 by lia, pow_succ] + rcases neg_one_pow_eq_or ℝ (n - (k + 1)) with he | he <;> rw [he] at h1 ⊢ + · have hneg : p.eval (C k) < 0 := by nlinarith + rw [abs_of_neg hneg] at h3 + linarith + · have hpos : 0 < p.eval (C k) := by nlinarith + rw [abs_of_pos hpos] at h3 + linarith + intro k hk + exact key (n - k) k (by lia) + +/-- On each monotone branch `(C k, C (k + 1))` of `p` there is a point where the centered Euler +step has the sign `(-1) ^ (n - k)` and absolute value at least one, provided `α n ≥ 1`. -/ +private theorem exists_branch_point {α : ℝ} (hα : 0 ≤ α) {p : ℝ[X]} {n : ℕ} (hn : 0 < n) + (hdeg : p.natDegree = n) (hroots : (p.roots.filter (· ∈ Ioo (-1 : ℝ) 1)).card = n) + (hsimple : p.roots.Nodup) (hone : p.eval 1 = 1) (hmone : p.eval (-1) = (-1) ^ n) + (hcrit : ∀ c ∈ Ioo (-1 : ℝ) 1, p.derivative.eval c = 0 → 1 ≤ |p.eval c|) + (hαn : 1 ≤ α * n) {C : ℕ → ℝ} (hC0 : C 0 = -1) (hCn : C n = 1) + (hstep : ∀ k < n, C k < C (k + 1)) + (hnoz : ∀ k < n, ∀ x ∈ Ioo (C k) (C (k + 1)), p.derivative.eval x ≠ 0) + (hsigned : ∀ k ≤ n, 1 ≤ (-1 : ℝ) ^ (n - k) * p.eval (C k)) {k : ℕ} (hk : k < n) : + ∃ ξ ∈ Ioo (C k) (C (k + 1)), + 1 ≤ (-1 : ℝ) ^ (n - k) * (centeredEulerStep α p).eval ξ := by + have hmono : ∀ a b, a ≤ b → b ≤ n → C a ≤ C b := by + intro a b hab hbn + induction b, hab using Nat.le_induction with + | base => exact le_rfl + | succ b hab ih => exact (ih (by lia)).trans (hstep b (by lia)).le + have hCk1 : C k < 1 := hCn ▸ (hstep k hk).trans_le (hmono (k + 1) n hk le_rfl) + have hCk2 : -1 < C (k + 1) := hC0 ▸ (hmono 0 k (Nat.zero_le _) hk.le).trans_lt (hstep k hk) + have hs0 := hsigned k hk.le + have hs1 := hsigned (k + 1) hk + have hnk : n - k = n - (k + 1) + 1 := by lia + have hIB : ∀ ξ ∈ Ioo (C k) (C (k + 1)), (n : ℝ) ^ 2 * (1 - p.eval ξ ^ 2) ≤ + (1 - ξ ^ 2) * p.derivative.eval ξ ^ 2 := fun ξ hξ ↦ + Polynomial.sq_mul_one_sub_sq_le_of_abs_eval_critical hn hdeg hroots hsimple hone hmone hcrit + ⟨(hC0 ▸ hmono 0 k (Nat.zero_le _) hk.le).trans hξ.1.le, + hξ.2.le.trans (hCn ▸ hmono (k + 1) n hk le_rfl)⟩ + have hξsq : ∀ ξ ∈ Ioo (C k) (C (k + 1)), 0 < 1 - ξ ^ 2 := by + intro ξ hξ + have h1 : -1 < ξ := hC0 ▸ (hmono 0 k (Nat.zero_le _) hk.le).trans_lt hξ.1 + have h2 : ξ < 1 := hξ.2.trans_le (hCn ▸ hmono (k + 1) n hk le_rfl) + nlinarith + rw [hnk, pow_succ] at hs0 ⊢ + rcases neg_one_pow_eq_or ℝ (n - (k + 1)) with he | he <;> rw [he] at hs0 hs1 ⊢ + · -- increasing branch: `p (C k) ≤ -1`, `p (C (k + 1)) ≥ 1`; take `p ξ = -ξ` + obtain ⟨ξ, hξ, hξ0⟩ := exists_Ioo_eq_zero_of_mul_neg + (f := fun t ↦ p.eval t + t) (p.continuous.add continuous_id) (hstep k hk) + (show (p.eval (C k) + C k) * (p.eval (C (k + 1)) + C (k + 1)) < 0 by nlinarith) + have hpξ : p.eval ξ = -ξ := by + have h : p.eval ξ + ξ = 0 := hξ0 + linarith + have hder : 0 < p.derivative.eval ξ := by + rcases Polynomial.derivative_pos_or_neg_of_ne_zero (hnoz k hk) with h | h + · exact h ξ hξ + · exfalso + have hanti : StrictAntiOn (fun z ↦ p.eval z) (Icc (C k) (C (k + 1))) := by + refine strictAntiOn_of_deriv_neg (convex_Icc _ _) p.continuous.continuousOn + fun z hz ↦ ?_ + rw [interior_Icc] at hz + simpa [Polynomial.deriv] using h z hz + have := hanti ⟨le_rfl, (hstep k hk).le⟩ ⟨(hstep k hk).le, le_rfl⟩ (hstep k hk) + simp only at this + linarith + have hsq := hξsq ξ hξ + have hIBξ := hIB ξ hξ + rw [hpξ, neg_sq] at hIBξ + have hn2 : (n : ℝ) ^ 2 ≤ p.derivative.eval ξ ^ 2 := by nlinarith + have hnd : (n : ℝ) ≤ p.derivative.eval ξ := by + have := sq_le_sq.mp hn2 + rwa [abs_of_nonneg (Nat.cast_nonneg n), abs_of_pos hder] at this + refine ⟨ξ, hξ, ?_⟩ + rw [centeredEulerStep_eval, hpξ] + nlinarith [mul_le_mul_of_nonneg_left hnd (mul_nonneg hα hsq.le)] + · -- decreasing branch: `p (C k) ≥ 1`, `p (C (k + 1)) ≤ -1`; take `p ξ = ξ` + obtain ⟨ξ, hξ, hξ0⟩ := exists_Ioo_eq_zero_of_mul_neg + (f := fun t ↦ p.eval t - t) (p.continuous.sub continuous_id) (hstep k hk) + (show (p.eval (C k) - C k) * (p.eval (C (k + 1)) - C (k + 1)) < 0 by nlinarith) + have hpξ : p.eval ξ = ξ := by + have h : p.eval ξ - ξ = 0 := hξ0 + linarith + have hder : p.derivative.eval ξ < 0 := by + rcases Polynomial.derivative_pos_or_neg_of_ne_zero (hnoz k hk) with h | h + · exfalso + have hmono' : StrictMonoOn (fun z ↦ p.eval z) (Icc (C k) (C (k + 1))) := by + refine strictMonoOn_of_deriv_pos (convex_Icc _ _) p.continuous.continuousOn + fun z hz ↦ ?_ + rw [interior_Icc] at hz + simpa [Polynomial.deriv] using h z hz + have := hmono' ⟨le_rfl, (hstep k hk).le⟩ ⟨(hstep k hk).le, le_rfl⟩ (hstep k hk) + simp only at this + linarith + · exact h ξ hξ + have hsq := hξsq ξ hξ + have hIBξ := hIB ξ hξ + rw [hpξ] at hIBξ + have hn2 : (n : ℝ) ^ 2 ≤ p.derivative.eval ξ ^ 2 := by nlinarith + have hnd : (n : ℝ) ≤ -p.derivative.eval ξ := by + have := sq_le_sq.mp hn2 + rwa [abs_of_nonneg (Nat.cast_nonneg n), abs_of_neg hder] at this + refine ⟨ξ, hξ, ?_⟩ + rw [centeredEulerStep_eval, hpξ] + nlinarith [mul_le_mul_of_nonneg_left hnd (mul_nonneg hα hsq.le)] + +/-- Signed alternation `(-1) ^ (N - i) q (η i) ≥ 1` gives the absolute-value and sign-change +hypotheses of `Polynomial.one_le_abs_eval_critical_of_alternation`. -/ +private theorem alternation_of_signed {q : ℝ[X]} {N : ℕ} {η : ℕ → ℝ} + (h : ∀ i ≤ N, 1 ≤ (-1 : ℝ) ^ (N - i) * q.eval (η i)) : + (∀ i ≤ N, 1 ≤ |q.eval (η i)|) ∧ (∀ i < N, q.eval (η i) * q.eval (η (i + 1)) < 0) := by + refine ⟨fun i hi ↦ ?_, fun i hi ↦ ?_⟩ + · have := h i hi + rcases neg_one_pow_eq_or ℝ (N - i) with he | he <;> rw [he] at this + · exact le_abs.mpr (Or.inl (by linarith)) + · exact le_abs.mpr (Or.inr (by linarith)) + · have h1 := h i hi.le + have h2 := h (i + 1) hi + rw [show N - i = N - (i + 1) + 1 by lia, pow_succ] at h1 + rcases neg_one_pow_eq_or ℝ (N - (i + 1)) with he | he <;> rw [he] at h1 h2 <;> nlinarith + +/-- **Propagation.** If `p` has degree `n > 0`, simple roots in `(-1, 1)`, `p 1 = 1`, +`p (-1) = (-1) ^ n`, and all critical values of absolute value at least one, then so does the +centered Euler step `X p + α (X² - 1) p'` whenever `α n ≥ 1`. -/ +theorem centeredEulerStep_critical_values {α : ℝ} (hα : 0 < α) {p : ℝ[X]} {n : ℕ} (hn : 0 < n) + (hp : IsRealRootedIn (Ioo (-1 : ℝ) 1) p) (hsimple : HasSimpleRoots p) + (hdeg : p.natDegree = n) (hpos : HasPosLeadingCoeff p) (hone : p.eval 1 = 1) + (hmone : p.eval (-1) = (-1) ^ n) + (hcrit : ∀ c ∈ Ioo (-1 : ℝ) 1, p.derivative.eval c = 0 → 1 ≤ |p.eval c|) + (hαn : 1 ≤ α * n) : + ∀ c ∈ Ioo (-1 : ℝ) 1, (centeredEulerStep α p).derivative.eval c = 0 → + 1 ≤ |(centeredEulerStep α p).eval c| := by + have hroots := card_roots_filter_Ioo_of_isRealRootedIn hp + rw [hdeg] at hroots + have hnd := hsimple.roots_nodup + obtain ⟨C, hC0, hCn, hstep, hcritC, hprod, hnoz⟩ := + Polynomial.exists_alternation_points hn hdeg hroots hnd hone hmone hcrit + have hsigned := signed_alternation hCn hone hcritC hprod + have hbr : ∀ k < n, ∃ ξ ∈ Ioo (C k) (C (k + 1)), + 1 ≤ (-1 : ℝ) ^ (n - k) * (centeredEulerStep α p).eval ξ := fun k hk ↦ + exists_branch_point hα.le hn hdeg hroots hnd hone hmone hcrit hαn hC0 hCn hstep hnoz + hsigned hk + choose! ξ hξ hξv using hbr + set q := centeredEulerStep α p with hq + have hqdeg : q.natDegree = n + 1 := by + rw [hq, (centeredEulerStep_degree_leadingCoeff hp.1 (by positivity)).1, hdeg] + have hqroots := centeredEulerStep_roots hα hp hsimple hpos + set η : ℕ → ℝ := fun i ↦ if i = 0 then -1 else if i ≤ n then ξ (i - 1) else 1 with hη + have hsignedq : ∀ i ≤ n + 1, 1 ≤ (-1 : ℝ) ^ (n + 1 - i) * q.eval (η i) := by + intro i hi + rcases Nat.eq_zero_or_pos i with rfl | hi0 + · simp only [hη, ↓reduceIte, Nat.sub_zero, hq, centeredEulerStep_eval_neg_one, hmone] + have h2 : ((-1 : ℝ) ^ n) ^ 2 = 1 := by rw [← pow_mul, mul_comm, pow_mul]; norm_num + have h3 : (-1 : ℝ) ^ (n + 1) * -(-1) ^ n = ((-1 : ℝ) ^ n) ^ 2 := by ring + rw [h3, h2] + by_cases hin : i ≤ n + · simp only [hη, hi0.ne', hin, ↓reduceIte] + rw [show n + 1 - i = n - (i - 1) by lia] + exact hξv (i - 1) (by lia) + · have : i = n + 1 := by lia + subst this + simp only [hη, show n + 1 ≠ 0 by lia, show ¬ n + 1 ≤ n by lia, ↓reduceIte, Nat.sub_self, + pow_zero, one_mul, hq, centeredEulerStep_eval_one, hone, le_refl] + obtain ⟨halt, hprodq⟩ := alternation_of_signed hsignedq + have hηinc : ∀ i < n + 1, η i < η (i + 1) := by + intro i hi + rcases Nat.eq_zero_or_pos i with rfl | hi0 + · simp only [hη, ↓reduceIte, show (0 + 1 : ℕ) ≠ 0 by lia, show 0 + 1 ≤ n by lia, + Nat.add_sub_cancel] + exact hC0 ▸ (hξ 0 hn).1 + by_cases hin : i + 1 ≤ n + · simp only [hη, hi0.ne', show i ≤ n by lia, hin, show i + 1 ≠ 0 by lia, ↓reduceIte, + Nat.add_sub_cancel] + have h1 := (hξ (i - 1) (by lia)).2 + rw [show i - 1 + 1 = i by lia] at h1 + exact h1.trans (hξ i (by lia)).1 + · have hin' : i = n := by lia + subst hin' + simp only [hη, hi0.ne', le_refl, show ¬ i + 1 ≤ i by lia, show i + 1 ≠ 0 by lia, + ↓reduceIte] + have h1 := (hξ (i - 1) (by lia)).2 + rwa [show i - 1 + 1 = i by lia, hCn] at h1 + exact Polynomial.one_le_abs_eval_critical_of_alternation (by lia) hqdeg + (by rw [card_roots_filter_Ioo_of_isRealRootedIn hqroots.1, hqdeg]) hqroots.2.roots_nodup + (by simp [hη]) (by simp [hη]) hηinc halt hprodq + +/-- The alternation points `-1, -5/6, -1/3, 1/3, 5/6, 1` of the degree-five row. -/ +private def fiveAlternationPoint : ℕ → ℝ + | 0 => -1 + | 1 => -5 / 6 + | 2 => -1 / 3 + | 3 => 1 / 3 + | 4 => 5 / 6 + | _ => 1 + +private theorem fiveAlternationPoint_eq {i : ℕ} (hi : i ≤ 5) : + fiveAlternationPoint i = ![(-1 : ℝ), -5 / 6, -1 / 3, 1 / 3, 5 / 6, 1] ⟨i, by lia⟩ := by + interval_cases i <;> rfl + +/-- For `α ≥ 1 / 2`, every row `p n` of the centered Euler orbit with `n ≥ 5` has all critical +values in `(-1, 1)` of absolute value at least one. -/ +theorem centeredEulerOrbit_critical_values {α : ℝ} (hα : 1 / 2 ≤ α) {n : ℕ} (hn : 5 ≤ n) : + ∀ c ∈ Ioo (-1 : ℝ) 1, (centeredEulerOrbit α n).derivative.eval c = 0 → + 1 ≤ |(centeredEulerOrbit α n).eval c| := by + induction n, hn using Nat.le_induction with + | base => + obtain ⟨hdeg, -, hroot, hsimple, -, -⟩ := centeredEulerOrbit_package hα 5 + have hs : ∀ i ≤ 5, 1 ≤ (-1 : ℝ) ^ (5 - i) * + (centeredEulerOrbit α 5).eval (fiveAlternationPoint i) := by + intro i hi + have h := centeredEulerOrbit_five_alternation hα ⟨i, by lia⟩ + rw [fiveAlternationPoint_eq hi] + exact h + obtain ⟨halt, hprod⟩ := alternation_of_signed hs + exact Polynomial.one_le_abs_eval_critical_of_alternation (by norm_num) hdeg + (by rw [card_roots_filter_Ioo_of_isRealRootedIn hroot, hdeg]) hsimple.roots_nodup + rfl rfl (fun i hi ↦ by interval_cases i <;> norm_num [fiveAlternationPoint]) halt hprod + | succ n hn ih => + obtain ⟨hdeg, hpos, hroot, hsimple, hone, hmone⟩ := centeredEulerOrbit_package hα n + have h5 : (5 : ℝ) ≤ n := by exact_mod_cast hn + rw [centeredEulerOrbit_succ] + exact centeredEulerStep_critical_values (by linarith) (by lia) hroot hsimple hdeg hpos hone + hmone ih (by nlinarith) + +/-! ### Small degrees -/ + +/-- For the first four nonconstant centered Euler rows, the value at an interior critical +point strictly dominates every perturbation `b * X ^ n` with `|b| ≤ 1`. -/ +theorem centeredEulerOrbit_small_critical {α b : ℝ} (hα : 1 / 2 ≤ α) + (hb : |b| ≤ 1) {n : ℕ} (hn1 : 1 ≤ n) (hn4 : n ≤ 4) {c : ℝ} + (hc : c ∈ Ioo (-1) 1) (hcrit : (centeredEulerOrbit α n).derivative.eval c = 0) : + |b * c ^ n| < |(centeredEulerOrbit α n).eval c| := by + have hαpos : 0 < α := by linarith + interval_cases n + · rw [centeredEulerOrbit_one] at hcrit + simp at hcrit + · have hc0 : c = 0 := by + have hcritical : 1 + α = 0 ∨ c = 0 := by + rw [centeredEulerOrbit_two] at hcrit + simpa [derivative_sub, derivative_mul, derivative_pow, map_ofNat] using hcrit + rcases hcritical with hbad | hc0 + · linarith + · exact hc0 + subst c + rw [centeredEulerOrbit_two] + simpa [abs_of_pos hαpos] using hαpos + · let A := (1 + α) * (1 + 2 * α) + let D := α * (3 + 2 * α) + have hApos : 0 < A := by + dsimp [A] + positivity + have hAge : 3 ≤ A := by + have hfactor : 0 ≤ (2 * α - 1) * (α + 2) := + mul_nonneg (by linarith) (by linarith) + dsimp [A] + nlinarith + have hDpos : 0 < D := by + dsimp [D] + positivity + have hcritical : 3 * A * c ^ 2 = D := by + rw [centeredEulerOrbit_three] at hcrit + simp [derivative_sub, derivative_mul, derivative_pow, map_ofNat] at hcrit + dsimp [A, D] + nlinarith + have hcne : c ≠ 0 := by + intro hc0 + subst c + norm_num at hcritical + linarith + have hcritical_mul : D * c = 3 * A * c ^ 3 := by + rw [← hcritical] + ring + have hvalue : (centeredEulerOrbit α 3).eval c = -(2 * A) * c ^ 3 := by + rw [centeredEulerOrbit_three] + simp [A] + nlinarith [hcritical_mul] + calc + |b * c ^ 3| ≤ |c ^ 3| := by + rw [abs_mul] + nlinarith [abs_nonneg (c ^ 3)] + _ < |(centeredEulerOrbit α 3).eval c| := by + rw [hvalue, abs_mul, abs_neg, abs_of_pos (by positivity : 0 < 2 * A)] + have hcabs : 0 < |c ^ 3| := abs_pos.mpr (pow_ne_zero 3 hcne) + nlinarith + · let A := (1 + α) * (1 + 2 * α) * (1 + 3 * α) + let B := 2 * α * (1 + α) * (3 + 4 * α) + let C₀ := α ^ 2 * (3 + 2 * α) + have hApos : 0 < A := by + dsimp [A] + positivity + have hBpos : 0 < B := by + dsimp [B] + positivity + have hCpos : 0 < C₀ := by + dsimp [C₀] + positivity + have hP : 0 < 24 * α ^ 5 + 92 * α ^ 4 + 160 * α ^ 3 + 112 * α ^ 2 + + 22 * α - 3 := by + nlinarith [pow_nonneg hαpos.le 2, pow_nonneg hαpos.le 3, + pow_nonneg hαpos.le 4, pow_nonneg hαpos.le 5] + have hcertificate : 0 < A * (B ^ 2 - 4 * A * C₀) - B ^ 2 := by + have hfactor : 0 < 4 * α ^ 2 * (1 + α) ^ 2 * + (24 * α ^ 5 + 92 * α ^ 4 + 160 * α ^ 3 + 112 * α ^ 2 + + 22 * α - 3) := by positivity + calc + 0 < 4 * α ^ 2 * (1 + α) ^ 2 * + (24 * α ^ 5 + 92 * α ^ 4 + 160 * α ^ 3 + 112 * α ^ 2 + + 22 * α - 3) := hfactor + _ = A * (B ^ 2 - 4 * A * C₀) - B ^ 2 := by + dsimp [A, B, C₀] + ring + rw [centeredEulerOrbit_four] at hcrit + have hcritical : 2 * c * (2 * A * c ^ 2 - B) = 0 := by + simp [derivative_add, derivative_sub, derivative_mul, derivative_pow, map_ofNat] + at hcrit + dsimp [A, B] + nlinarith + rcases mul_eq_zero.mp hcritical with hc0 | hrelation + · have hc0 : c = 0 := by simpa using hc0 + subst c + rw [centeredEulerOrbit_four] + norm_num [abs_of_pos (by positivity : 0 < α ^ 2 * (3 + 2 * α))] + positivity + · have hrelation : 2 * A * c ^ 2 = B := by nlinarith + have hcne : c ≠ 0 := by + intro hc0 + subst c + norm_num at hrelation + linarith + have hBsq : B ^ 2 = 4 * A ^ 2 * c ^ 4 := by + rw [← hrelation] + ring + have hproduct : 0 < 4 * A ^ 2 * ((A - 1) * c ^ 4 - C₀) := by + calc + 0 < A * (B ^ 2 - 4 * A * C₀) - B ^ 2 := hcertificate + _ = 4 * A ^ 2 * ((A - 1) * c ^ 4 - C₀) := by rw [hBsq]; ring + have hgap : C₀ < (A - 1) * c ^ 4 := by + rcases (mul_pos_iff.mp hproduct) with hpositive | hnegative + · linarith + · exact False.elim ((not_lt_of_ge (sq_nonneg A)) (by nlinarith [hnegative.1])) + have hrelation_mul : B * c ^ 2 = 2 * A * c ^ 4 := by + rw [← hrelation] + ring + have hvalue : (centeredEulerOrbit α 4).eval c = C₀ - A * c ^ 4 := by + rw [centeredEulerOrbit_four] + simp [A, C₀] + nlinarith + have hvalue_neg : C₀ - A * c ^ 4 < 0 := by + nlinarith [pow_pos (show 0 < c ^ 2 by positivity) 2] + calc + |b * c ^ 4| = |b| * c ^ 4 := by + have hc4 : 0 ≤ c ^ 4 := by positivity + rw [abs_mul, abs_of_nonneg hc4] + _ ≤ c ^ 4 := by + have hc4 : 0 ≤ c ^ 4 := by positivity + nlinarith + _ < A * c ^ 4 - C₀ := by nlinarith + _ = |(centeredEulerOrbit α 4).eval c| := by + rw [hvalue, abs_of_neg hvalue_neg] + ring + +end RealRooted diff --git a/RealRooted/EulerOperator/OrbitPerturbationCayley.lean b/RealRooted/EulerOperator/OrbitPerturbationCayley.lean new file mode 100644 index 000000000..03f5bfcb0 --- /dev/null +++ b/RealRooted/EulerOperator/OrbitPerturbationCayley.lean @@ -0,0 +1,110 @@ +module + +public import RealRooted.EulerOperator.OrbitPerturbationFamily +public import RealRooted.Mathlib.Algebra.Polynomial.CayleyTransform.Basic +import RealRooted.Mathlib.Algebra.Polynomial.CayleyTransform.Algebra +import Mathlib.Tactic.ComputeDegree +import Mathlib.Tactic.Ring + +/-! +# The perturbed centered Euler orbit in Eulerian coordinates + +The Cayley transform `T_n f = (1 - X) ^ n f (X / (1 - X))` maps the rows `Q n` of +`RealRooted.EulerOperator.OrbitPerturbationFamily` to Eulerian-type rows. With `s = 2 α`, the +transformed orbit `E n = T_n (p n (2 u + 1))` satisfies `E 0 = 1` and + + E (n + 1) = (1 + (1 + s n) X) E n + s X (1 - X) E n' + +(for `s = 1` these are the Eulerian polynomials), and `T_n (2 u + 1) ^ n = (1 + X) ^ n`. Hence +for `s ≥ 1` and `c ≥ 1 / 2` the rows `c E n + (1 - c) (1 + X) ^ n` are real-rooted +(`splits_C_mul_add_C_mul_one_add_X_pow_of_recurrence`). This is the form of RealRooted #2513, +Theorem 1, that matches the OEIS triangles A141689, A141690, A141696, A141697 (`s = 1`, +`c = 1/2, 2, 3, 7`) and A147565 (`s = 2`, `c = 1/2`). +-/ + +public section + +open Polynomial Set + +noncomputable section + +namespace RealRooted + +/-- The centered Euler orbit in Eulerian coordinates: the degree-`n` Cayley transform of +`p n (2 u + 1)`. -/ +def cayleyEulerOrbit (α : ℝ) (n : ℕ) : ℝ[X] := + cayleyTransform n ((centeredEulerOrbit α n).comp (C 2 * X + C 1)) + +/-- The orbit in the variable `u` has degree at most `n`. -/ +private theorem natDegree_centeredEulerOrbit_comp_le {α : ℝ} (hα : 0 < α) (n : ℕ) : + ((centeredEulerOrbit α n).comp (C 2 * X + C 1)).natDegree ≤ n := by + refine natDegree_comp_le.trans ?_ + rw [centeredEulerOrbit_natDegree hα n] + have h : (C 2 * X + C 1 : ℝ[X]).natDegree ≤ 1 := by compute_degree + nlinarith + +@[simp] theorem cayleyEulerOrbit_zero (α : ℝ) : cayleyEulerOrbit α 0 = 1 := by + simpa [cayleyEulerOrbit] using cayleyTransform_X_pow (R := ℝ) (n := 0) (k := 0) le_rfl + +/-- The Eulerian-type recurrence `E (n + 1) = (1 + (1 + 2 α n) X) E n + 2 α X (1 - X) E n'`. -/ +theorem cayleyEulerOrbit_succ {α : ℝ} (hα : 0 < α) (n : ℕ) : + cayleyEulerOrbit α (n + 1) = + (1 + C (1 + 2 * α * n) * X) * cayleyEulerOrbit α n + + C (2 * α) * X * (1 - X) * (cayleyEulerOrbit α n).derivative := by + have hdeg := natDegree_centeredEulerOrbit_comp_le hα n + unfold cayleyEulerOrbit + rw [centeredEulerOrbit_succ, centeredEulerStep_comp_two_mul_X_add_one] + generalize (centeredEulerOrbit α n).comp (C 2 * X + C 1) = P at hdeg ⊢ + have hθ : (X * P.derivative).natDegree ≤ n := by + by_cases hP : P.derivative = 0 + · simp [hP] + have hlt := natDegree_derivative_lt (p := P) fun h ↦ hP (derivative_of_natDegree_zero h) + have hX : (X : ℝ[X]).natDegree ≤ 1 := natDegree_X_le + have := natDegree_mul_le (p := (X : ℝ[X])) (q := P.derivative) + lia + rw [show (C 2 * X + C 1) * P + C (2 * α) * (X + 1) * (X * P.derivative) = + C 2 * (X * P) + C 1 * P + C (2 * α) * (X * (X * P.derivative) + X * P.derivative) by ring] + rw [cayleyTransform_add, cayleyTransform_add, cayleyTransform_C_mul, cayleyTransform_C_mul, + cayleyTransform_C_mul, cayleyTransform_add, cayleyTransform_succ_X_mul hdeg, + cayleyTransform_succ hdeg, cayleyTransform_succ_X_mul hθ, cayleyTransform_succ hθ, + cayleyTransform_X_mul_derivative hdeg] + simp only [map_add, map_mul, map_one, map_natCast, map_ofNat] + ring + +/-- The Cayley transform of the perturbed row `Q n` is `c E n + (1 - c) (1 + X) ^ n`. -/ +theorem cayleyTransform_orbitPerturbationRow (α c : ℝ) (n : ℕ) : + cayleyTransform n (orbitPerturbationRow α c n) = + C c * cayleyEulerOrbit α n + C (1 - c) * (1 + X) ^ n := by + have hY : cayleyTransform n ((C 2 * X + C 1 : ℝ[X]) ^ n) = (1 + X) ^ n := by + rw [show (C 2 * X + C 1 : ℝ[X]) = 1 + C 2 * X by rw [map_one]; ring] + exact cayleyTransform_twoPascal n + rw [orbitPerturbationRow_eq, cayleyTransform_add, cayleyTransform_C_mul, cayleyTransform_C_mul, + hY, cayleyEulerOrbit] + +/-- **Eulerian form of RealRooted #2513, Theorem 1.** Let `s ≥ 1` and `c ≥ 1 / 2`, and let +`E 0 = 1` and `E (n + 1) = (1 + (1 + s n) X) E n + s X (1 - X) E n'`. Then +`c E n + (1 - c) (1 + X) ^ n` is real-rooted for every `n`. -/ +theorem splits_C_mul_add_C_mul_one_add_X_pow_of_recurrence {s c : ℝ} (hs : 1 ≤ s) + (hc : 1 / 2 ≤ c) {E : ℕ → ℝ[X]} (h0 : E 0 = 1) + (hrec : ∀ n : ℕ, E (n + 1) = + (1 + C (1 + s * n) * X) * E n + C s * X * (1 - X) * (E n).derivative) (n : ℕ) : + (C c * E n + C (1 - c) * (1 + X) ^ n).Splits := by + have hα : 0 < s / 2 := by linarith + have hE : ∀ m, E m = cayleyEulerOrbit (s / 2) m := by + intro m + induction m with + | zero => rw [h0, cayleyEulerOrbit_zero] + | succ m ih => + rw [hrec m, cayleyEulerOrbit_succ hα, ih, + show 2 * (s / 2) = s by ring] + rw [hE n, ← cayleyTransform_orbitPerturbationRow] + have hroot := (orbitPerturbationRow_package (α := s / 2) (by linarith) hc n).1 + refine hroot.splits.cayleyTransform ?_ + rw [orbitPerturbationRow_eq] + refine natDegree_add_le_of_degree_le ((natDegree_C_mul_le _ _).trans + (natDegree_centeredEulerOrbit_comp_le hα n)) ((natDegree_C_mul_le _ _).trans ?_) + refine natDegree_pow_le.trans ?_ + have h1 : (C 2 * X + C 1 : ℝ[X]).natDegree ≤ 1 := by compute_degree + nlinarith + +end RealRooted diff --git a/RealRooted/EulerOperator/OrbitPerturbationFamily.lean b/RealRooted/EulerOperator/OrbitPerturbationFamily.lean new file mode 100644 index 000000000..727059c32 --- /dev/null +++ b/RealRooted/EulerOperator/OrbitPerturbationFamily.lean @@ -0,0 +1,193 @@ +module + +public import RealRooted.EulerOperator.OrbitPerturbation +import RealRooted.EulerOperator.OrbitPerturbationInterlacing +import RealRooted.Linear +import RealRooted.MaWang.Weak.DerivativeSign +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.LinearCombination +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# A three-term θ-recurrence family with interlacing rows + +Let `s ≥ 1` and `κ ≥ s + 4`, and let `Q 0 = 1`, `Q 1 = 1 + 2 u`, `Q 2 = 1 + κ u + κ u²` and, +for `n ≥ 3`, with `θ = u d/du`, + + (n - 2) Q n = ((2 n - 3) (2 u + 1) + (n - 2) s (u + 1) θ) Q (n - 1) + - (n - 1) (2 u + 1) ((2 u + 1) + s (u + 1) θ) Q (n - 2). + +Then every `Q n` has simple roots in `(-1, 0)` and `Q n` strictly interlaces `Q (n + 1)` +(`strictInterl_of_orbitPerturbation_recurrence`). This covers OEIS A141689 `(s, κ) = (1, 5)`, +A141690 `(1, 8)`, A141696 `(1, 10)`, A141697 `(1, 18)` and A147565 `(2, 6)` after the Eulerian +Möbius substitution (RealRooted #2513, Theorem 1). + +With `x = 2 u + 1`, `α = s / 2` and `r = (κ - 4) / (2 s) ≥ 1 / 2`, the rows are +`Q n = r p n (x) + (1 - r) x ^ n`, where `p n` is the centered Euler orbit; the interlacing comes +from `centeredEulerOrbit_add_monomial`. +-/ + +public section + +open Polynomial Set + +noncomputable section + +namespace RealRooted + +/-- One centered Euler step, read in the variable `u` with `x = 2 u + 1`. -/ +theorem centeredEulerStep_comp_two_mul_X_add_one (α : ℝ) (f : ℝ[X]) : + (centeredEulerStep α f).comp (C 2 * X + C 1) = + (C 2 * X + C 1) * f.comp (C 2 * X + C 1) + + C (2 * α) * (X + 1) * (X * (f.comp (C 2 * X + C 1)).derivative) := by + simp [centeredEulerStep, derivative_comp, map_ofNat] + ring + +/-- The rows `r p n (2 u + 1) + (1 - r) (2 u + 1) ^ n` of the centered Euler orbit perturbed +by a monomial, in the variable `u`. -/ +def orbitPerturbationRow (α r : ℝ) (n : ℕ) : ℝ[X] := + (C r * centeredEulerOrbit α n + (1 - C r) * X ^ n).comp (C 2 * X + C 1) + +/-- The perturbed rows expanded: `Q n = r p n (2 u + 1) + (1 - r) (2 u + 1) ^ n`. -/ +theorem orbitPerturbationRow_eq (α r : ℝ) (n : ℕ) : + orbitPerturbationRow α r n = C r * (centeredEulerOrbit α n).comp (C 2 * X + C 1) + + C (1 - r) * (C 2 * X + C 1) ^ n := by + simp [orbitPerturbationRow] + +/-- The perturbed rows as a multiple of `h n = p n + b X ^ n` with `b = (1 - r) / r`. -/ +theorem orbitPerturbationRow_eq_C_mul {α r : ℝ} (hr : r ≠ 0) (n : ℕ) : + orbitPerturbationRow α r n = + C r * (centeredEulerOrbit α n + C ((1 - r) / r) * X ^ n).comp (C 2 * X + C 1) := by + rw [orbitPerturbationRow, ← C_mul_comp, mul_add, ← mul_assoc, ← C_mul, + show r * ((1 - r) / r) = 1 - r by field_simp, map_sub, map_one] + +/-- The perturbed rows satisfy the three-term θ-recurrence of the family with `s = 2 α`. -/ +theorem orbitPerturbationRow_recurrence (α r : ℝ) (n : ℕ) : + ((n : ℝ[X]) + 1) * orbitPerturbationRow α r (n + 3) = + (2 * (n : ℝ[X]) + 3) * (C 2 * X + 1) * orbitPerturbationRow α r (n + 2) + + ((n : ℝ[X]) + 1) * C (2 * α) * (X + 1) * + (X * (orbitPerturbationRow α r (n + 2)).derivative) - + ((n : ℝ[X]) + 2) * (C 2 * X + 1) * + ((C 2 * X + 1) * orbitPerturbationRow α r (n + 1) + + C (2 * α) * (X + 1) * (X * (orbitPerturbationRow α r (n + 1)).derivative)) := by + have hstep : ∀ k, (centeredEulerOrbit α (k + 1)).comp (C 2 * X + C 1) = + (C 2 * X + C 1) * (centeredEulerOrbit α k).comp (C 2 * X + C 1) + + C (2 * α) * (X + 1) * (X * ((centeredEulerOrbit α k).comp (C 2 * X + C 1)).derivative) := + fun k ↦ by rw [centeredEulerOrbit_succ, centeredEulerStep_comp_two_mul_X_add_one] + have h3 : (centeredEulerOrbit α (n + 3)).comp (C 2 * X + C 1) = _ := hstep (n + 2) + have h2 : (centeredEulerOrbit α (n + 2)).comp (C 2 * X + C 1) = _ := hstep (n + 1) + simp only [orbitPerturbationRow, add_comp, mul_comp, sub_comp, C_comp, one_comp, X_pow_comp] + generalize (centeredEulerOrbit α (n + 3)).comp (C 2 * X + C 1) = P3 at * + generalize (centeredEulerOrbit α (n + 2)).comp (C 2 * X + C 1) = P2 at * + generalize (centeredEulerOrbit α (n + 1)).comp (C 2 * X + C 1) = P1 at * + clear hstep + simp only [derivative_add, derivative_mul, derivative_sub, derivative_C, derivative_one, + derivative_pow, derivative_X, derivative_ofNat, map_one, map_ofNat] at h2 h3 ⊢ + push_cast at h2 h3 ⊢ + simp only [map_add, map_natCast, map_ofNat, map_one] at h2 h3 ⊢ + linear_combination ((n : ℝ[X]) + 1) * C r * h3 - ((n : ℝ[X]) + 2) * (2 * X + 1) * C r * h2 + +@[simp] theorem orbitPerturbationRow_zero (α r : ℝ) : orbitPerturbationRow α r 0 = 1 := by + simp [orbitPerturbationRow] + +theorem orbitPerturbationRow_one (α r : ℝ) : orbitPerturbationRow α r 1 = C 2 * X + 1 := by + simp [orbitPerturbationRow, centeredEulerStep] + ring + +/-- For `α ≥ 1 / 2` and `r ≥ 1 / 2`, the perturbed rows have simple roots in `(-1, 0)` and +consecutive rows interlace strictly. -/ +theorem orbitPerturbationRow_package {α r : ℝ} (hαhalf : 1 / 2 ≤ α) (hrhalf : 1 / 2 ≤ r) + (n : ℕ) : + IsRealRootedIn (Ioo (-1 : ℝ) 0) (orbitPerturbationRow α r n) ∧ + HasSimpleRoots (orbitPerturbationRow α r n) ∧ + StrictInterl (orbitPerturbationRow α r n) (orbitPerturbationRow α r (n + 1)) := by + have hrpos : 0 < r := by linarith + -- Transfer from the centered coordinates. + have hloc : (fun x : ℝ ↦ 2 * x + 1) ⁻¹' Ioo (-1 : ℝ) 1 = Ioo (-1 : ℝ) 0 := by + ext x + simp only [mem_preimage, mem_Ioo] + constructor <;> rintro ⟨h₁, h₂⟩ <;> constructor <;> linarith + have hcomp : ∀ f : ℝ[X], f.comp (C 2 * X + C 1) = (f.comp (C 2 * X)).comp (X + C (1 / 2)) := by + intro f + rw [comp_assoc] + congr 1 + simp only [mul_comp, C_comp, X_comp] + rw [mul_add, ← C_mul] + norm_num + rcases Nat.eq_zero_or_pos n with rfl | hn + · rw [orbitPerturbationRow_zero α r] + refine ⟨IsRealRootedIn.one, hasSimpleRoots_of_natDegree_le_one one_ne_zero (by simp), ?_⟩ + rw [zero_add, orbitPerturbationRow_one α r] + exact StrictInterl.of_natDegree_eq_zero_left one_ne_zero (by simp) + (by + intro h + have h' := congrArg (fun p ↦ p.coeff 1) h + simp [coeff_one, coeff_C] at h') + (by compute_degree!) + have hb : -1 < (1 - r) / r := by + rw [lt_div_iff₀ hrpos] + linarith + have hb1 : (1 - r) / r ≤ 1 := by + rw [div_le_iff₀ hrpos] + linarith + obtain ⟨-, -, hroot, hsimple, hint⟩ := centeredEulerOrbit_add_monomial hαhalf hb hb1 hn + rw [orbitPerturbationRow_eq_C_mul hrpos.ne', orbitPerturbationRow_eq_C_mul hrpos.ne'] + refine ⟨?_, ?_, ?_⟩ + · refine IsRealRootedIn.C_mul hrpos.ne' ?_ + rw [← hloc] + exact hroot.comp_C_mul_X_add_C 1 two_ne_zero + · exact (hsimple.comp_C_mul_X_add_C two_ne_zero).C_mul hrpos.ne' + · rw [hcomp, hcomp] + exact (((hint.comp_C_mul_X two_pos).comp_X_add_C _).C_mul_left hrpos.ne').C_mul_right + hrpos.ne' + +/-- **A θ-recurrence family with interlacing rows** (RealRooted #2513, Theorem 1). Let `s ≥ 1` +and `κ ≥ s + 4`, and let `Q` satisfy `Q 0 = 1`, `Q 1 = 2 u + 1`, `Q 2 = κ u² + κ u + 1` and +`(n + 1) Q (n + 3) = (2 n + 3) (2 u + 1) Q (n + 2) + (n + 1) s (u + 1) θ Q (n + 2) + - (n + 2) (2 u + 1) ((2 u + 1) Q (n + 1) + s (u + 1) θ Q (n + 1))` with `θ = u d/du`. +Then every `Q n` has simple roots in `(-1, 0)` and `Q n` strictly interlaces `Q (n + 1)`. -/ +theorem strictInterl_of_orbitPerturbation_recurrence {s κ : ℝ} (hs : 1 ≤ s) (hκ : s + 4 ≤ κ) + {Q : ℕ → ℝ[X]} (h0 : Q 0 = 1) (h1 : Q 1 = C 2 * X + 1) + (h2 : Q 2 = C κ * X ^ 2 + C κ * X + 1) + (hrec : ∀ n : ℕ, ((n : ℝ[X]) + 1) * Q (n + 3) = + (2 * (n : ℝ[X]) + 3) * (C 2 * X + 1) * Q (n + 2) + + ((n : ℝ[X]) + 1) * C s * (X + 1) * (X * (Q (n + 2)).derivative) - + ((n : ℝ[X]) + 2) * (C 2 * X + 1) * + ((C 2 * X + 1) * Q (n + 1) + C s * (X + 1) * (X * (Q (n + 1)).derivative))) (n : ℕ) : + IsRealRootedIn (Ioo (-1 : ℝ) 0) (Q n) ∧ HasSimpleRoots (Q n) ∧ + StrictInterl (Q n) (Q (n + 1)) := by + set α := s / 2 with hα + set r := (κ - 4) / (2 * s) with hr + have hspos : 0 < s := by linarith + have hs2 : 2 * α = s := by rw [hα]; ring + have hαhalf : 1 / 2 ≤ α := by rw [hα]; linarith + have hrhalf : 1 / 2 ≤ r := by + rw [hr, le_div_iff₀ (by positivity)] + linarith + have hrpos : 0 < r := by linarith + have hκr : κ = 4 * (r * α) + 4 := by + rw [hr, hα] + field_simp + ring + -- The sequence is the perturbed orbit. + have hR0 := orbitPerturbationRow_zero α r + have hR1 := orbitPerturbationRow_one α r + have hR2 : orbitPerturbationRow α r 2 = C κ * X ^ 2 + C κ * X + 1 := by + simp [orbitPerturbationRow, centeredEulerStep, hκr, map_ofNat] + ring + have hQ : ∀ m, Q m = orbitPerturbationRow α r m ∧ Q (m + 1) = orbitPerturbationRow α r (m + 1) ∧ + Q (m + 2) = orbitPerturbationRow α r (m + 2) := by + intro m + induction m with + | zero => exact ⟨h0.trans hR0.symm, h1.trans hR1.symm, h2.trans hR2.symm⟩ + | succ m ih => + refine ⟨ih.2.1, ih.2.2, ?_⟩ + have hne : ((m : ℝ[X]) + 1) ≠ 0 := by exact_mod_cast Nat.succ_ne_zero m + apply mul_left_cancel₀ hne + change ((m : ℝ[X]) + 1) * Q (m + 3) = ((m : ℝ[X]) + 1) * orbitPerturbationRow α r (m + 3) + rw [hrec m, orbitPerturbationRow_recurrence, ih.2.1, ih.2.2, hs2] + rw [(hQ n).1, (hQ (n + 1)).1] + exact orbitPerturbationRow_package hαhalf hrhalf n + +end RealRooted diff --git a/RealRooted/EulerOperator/OrbitPerturbationInterlacing.lean b/RealRooted/EulerOperator/OrbitPerturbationInterlacing.lean new file mode 100644 index 000000000..6b56f24ef --- /dev/null +++ b/RealRooted/EulerOperator/OrbitPerturbationInterlacing.lean @@ -0,0 +1,229 @@ +module + +public import RealRooted.EulerOperator.OrbitPerturbation +public import RealRooted.Basic.ProperPosition +import RealRooted.MaWang.CriticalSign +import RealRooted.Mathlib.Analysis.Polynomial.InverseBernstein +import Mathlib.Analysis.Calculus.Deriv.MeanValue +import Mathlib.Analysis.Calculus.Deriv.Polynomial +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# Monomial perturbations of the centered Euler orbit + +Let `p n` be the orbit of `1` under the centered Euler step `f ↦ X f + α (X² - 1) f'`. For +`α ≥ 1 / 2` and `-1 < b ≤ 1` the perturbed rows `h n = p n + b X ^ n` have simple roots in +`(-1, 1)` and consecutive rows interlace strictly (RealRooted #2513, Theorem 1 in centered +coordinates). + +The proof compares `h n` with `p n` at the sign alternation points of `p n`: the critical values +of `p n` dominate `b c ^ n` (`centeredEulerOrbit_critical_values` and +`centeredEulerOrbit_small_critical`), so `h n` changes sign like `p n`. Since +`h (n + 1) = X h n + α (X² - 1) (p n)'`, the root-sign criterion +`strictInterl_of_eval_mul_derivative_neg` gives `h n ≺ h (n + 1)`. +-/ + +public section + +open Polynomial Set + +noncomputable section + +namespace RealRooted + +/-- The leading coefficients of the centered Euler orbit are at least one for `α ≥ 0`. -/ +theorem one_le_leadingCoeff_centeredEulerOrbit {α : ℝ} (hα : 0 ≤ α) (n : ℕ) : + 1 ≤ (centeredEulerOrbit α n).leadingCoeff := by + induction n with + | zero => simp + | succ n ih => + have hne : centeredEulerOrbit α n ≠ 0 := by + intro h0 + rw [h0, leadingCoeff_zero] at ih + linarith + have hnn : 0 ≤ α * ((centeredEulerOrbit α n).natDegree : ℝ) := + mul_nonneg hα (Nat.cast_nonneg _) + rw [centeredEulerOrbit_succ, (centeredEulerStep_degree_leadingCoeff hne (by linarith)).2] + nlinarith + +/-- `p` has the sign of `p (C (k + 1))` on `(C k, C (k + 1))` when `p` changes sign across the +interval and `p'` does not vanish inside it. -/ +private theorem derivative_mul_eval_pos {p : ℝ[X]} {u v r : ℝ} + (hne : ∀ x ∈ Ioo u v, p.derivative.eval x ≠ 0) (hprod : p.eval u * p.eval v < 0) + (hr : r ∈ Ioo u v) : 0 < p.derivative.eval r * p.eval v := by + have huv : u ≤ v := (hr.1.trans hr.2).le + rcases Polynomial.derivative_pos_or_neg_of_ne_zero hne with hd | hd + · have hmono : StrictMonoOn (fun x ↦ p.eval x) (Icc u v) := by + refine strictMonoOn_of_deriv_pos (convex_Icc u v) p.continuous.continuousOn + fun x hx ↦ ?_ + rw [interior_Icc] at hx + simpa [Polynomial.deriv] using hd x hx + have hlt : p.eval u < p.eval v := + hmono ⟨le_rfl, huv⟩ ⟨huv, le_rfl⟩ (hr.1.trans hr.2) + have hv : 0 < p.eval v := by nlinarith + exact mul_pos (hd r hr) hv + · have hanti : StrictAntiOn (fun x ↦ p.eval x) (Icc u v) := by + refine strictAntiOn_of_deriv_neg (convex_Icc u v) p.continuous.continuousOn + fun x hx ↦ ?_ + rw [interior_Icc] at hx + simpa [Polynomial.deriv] using hd x hx + have hlt : p.eval v < p.eval u := + hanti ⟨le_rfl, huv⟩ ⟨huv, le_rfl⟩ (hr.1.trans hr.2) + have hv : p.eval v < 0 := by nlinarith + exact mul_pos_of_neg_of_neg (hd r hr) hv + +/-- Perturbing `p` by `b X ^ n` keeps the sign of `p` at its alternation points when the +critical values of `p` dominate `b c ^ n` and `b > -1`. -/ +private theorem eval_add_monomial_mul_pos {p : ℝ[X]} {n : ℕ} {b : ℝ} (hb : -1 < b) + (hone : p.eval 1 = 1) (hmone : p.eval (-1) = (-1) ^ n) + (hcrit : ∀ c ∈ Ioo (-1 : ℝ) 1, p.derivative.eval c = 0 → |b * c ^ n| < |p.eval c|) + {c : ℝ} (hc : c = -1 ∨ c = 1 ∨ (c ∈ Ioo (-1 : ℝ) 1 ∧ p.derivative.eval c = 0)) : + 0 < (p + C b * X ^ n).eval c * p.eval c := by + have hev : (p + C b * X ^ n).eval c = p.eval c + b * c ^ n := by simp + rw [hev] + rcases hc with rfl | rfl | ⟨hmem, hcr⟩ + · have hsq : ((-1 : ℝ) ^ n) ^ 2 = 1 := by rw [← pow_mul, mul_comm, pow_mul]; norm_num + rw [hmone, show ((-1 : ℝ) ^ n + b * (-1) ^ n) * (-1) ^ n = (1 + b) * ((-1 : ℝ) ^ n) ^ 2 by + ring, hsq] + linarith + · rw [hone, one_pow] + linarith + · have hlt := hcrit _ hmem hcr + have h1 : -(|b * c ^ n| * |p.eval c|) ≤ b * c ^ n * p.eval c := by + rw [← abs_mul] + exact neg_abs_le _ + have h2 : |p.eval c| * |p.eval c| = p.eval c * p.eval c := abs_mul_abs_self _ + nlinarith [mul_pos ((abs_nonneg _).trans_lt hlt) (sub_pos.mpr hlt)] + +/-- Monomial perturbation of one centered Euler step. Let `p` have degree `n > 0`, positive +leading coefficient, simple roots in `(-1, 1)`, `p 1 = 1` and `p (-1) = (-1) ^ n`, and let +`b > -1` be such that `|b c ^ n| < |p c|` at every critical point `c ∈ (-1, 1)` and +`lc p + b > 0`. Then `h = p + b X ^ n` has degree `n`, positive leading coefficient and simple +roots in `(-1, 1)`, and `h` strictly interlaces `X h + α (X² - 1) p' = L p + b X ^ (n + 1)`. -/ +theorem strictInterl_centeredEulerStep_add_monomial {α b : ℝ} (hα : 0 < α) (hb : -1 < b) + {p : ℝ[X]} {n : ℕ} (hn : 0 < n) (hdeg : p.natDegree = n) + (hroot : IsRealRootedIn (Ioo (-1 : ℝ) 1) p) (hsimple : HasSimpleRoots p) + (hpos : HasPosLeadingCoeff p) (hlead : 0 < p.leadingCoeff + b) + (hone : p.eval 1 = 1) (hmone : p.eval (-1) = (-1) ^ n) + (hcrit : ∀ c ∈ Ioo (-1 : ℝ) 1, p.derivative.eval c = 0 → |b * c ^ n| < |p.eval c|) : + (p + C b * X ^ n).natDegree = n ∧ HasPosLeadingCoeff (p + C b * X ^ n) ∧ + IsRealRootedIn (Ioo (-1 : ℝ) 1) (p + C b * X ^ n) ∧ HasSimpleRoots (p + C b * X ^ n) ∧ + StrictInterl (p + C b * X ^ n) (centeredEulerStep α p + C b * X ^ (n + 1)) := by + set h := p + C b * X ^ n with hh + have hcoeff : h.coeff n = p.leadingCoeff + b := by + simp [hh, leadingCoeff, hdeg] + have hhdeg : h.natDegree = n := natDegree_eq_of_le_of_coeff_ne_zero + (natDegree_add_le_of_degree_le hdeg.le (natDegree_C_mul_X_pow_le b n)) + (hcoeff ▸ hlead.ne') + have hhpos : HasPosLeadingCoeff h := by + rw [HasPosLeadingCoeff, leadingCoeff, hhdeg, hcoeff] + exact hlead + have hcard := card_roots_filter_Ioo_of_isRealRootedIn hroot + rw [hdeg] at hcard + obtain ⟨A, hA0, hAn, hAinc, hAcrit, hAprod, hAder⟩ := + Polynomial.exists_sign_alternation_points hn hdeg hcard hsimple.roots_nodup + have hsame : ∀ k ≤ n, 0 < h.eval (A k) * p.eval (A k) := by + intro k hk + refine eval_add_monomial_mul_pos hb hone hmone hcrit ?_ + rcases Nat.eq_zero_or_pos k with rfl | hk0 + · exact Or.inl hA0 + rcases hk.eq_or_lt with rfl | hkn + · exact Or.inr (Or.inl hAn) + · exact Or.inr (Or.inr (hAcrit k hk0 hkn)) + have hsign : ∀ k < n, h.eval (A k) * h.eval (A (k + 1)) < 0 := by + intro k hk + have h1 := hsame k hk.le + have h2 := hsame (k + 1) hk + have h3 := hAprod k hk + nlinarith [mul_pos h1 h2] + obtain ⟨hnodup, hcardh, hloc, hdsign⟩ := Polynomial.roots_of_sign_changes hn hhdeg hAinc hsign + have hmono : ∀ a c, a ≤ c → c ≤ n → A a ≤ A c := by + intro a c hac hcn + induction c, hac using Nat.le_induction with + | base => exact le_rfl + | succ c hac ih => exact (ih (by lia)).trans (hAinc c (by lia)).le + have hinside : ∀ r, h.IsRoot r → r ∈ Ioo (-1 : ℝ) 1 := by + intro r hr + obtain ⟨k, hk, hrk⟩ := hloc r hr + constructor + · linarith [hmono 0 k (Nat.zero_le _) hk.le, hrk.1] + · linarith [hmono (k + 1) n hk le_rfl, hrk.2] + have hne : h ≠ 0 := hhpos.ne_zero + have hsplit : h.Splits := splits_iff_card_roots.mpr (by rw [hcardh, hhdeg]) + have hreal : IsRealRootedIn (Ioo (-1 : ℝ) 1) h := + ⟨hne, hsplit, fun z hz ↦ hinside z ((mem_roots hne).mp hz)⟩ + -- The next row. + set F := centeredEulerStep α p + C b * X ^ (n + 1) with hF + have hFid : F = X * h + C α * (X ^ 2 - 1) * p.derivative := by + simp only [hF, hh, centeredEulerStep] + ring + obtain ⟨hsdeg, hslc⟩ := centeredEulerStep_degree_leadingCoeff (α := α) hpos.ne_zero + (by positivity) + rw [hdeg] at hsdeg hslc + have hFcoeff : F.coeff (n + 1) = (1 + α * n) * p.leadingCoeff + b := by + simp only [hF, coeff_add, coeff_C_mul_X_pow, ↓reduceIte] + rw [← hslc, leadingCoeff, hsdeg] + have hFlc : 0 < (1 + α * n) * p.leadingCoeff + b := by + have hlc : 0 < p.leadingCoeff := hpos + have : 0 ≤ α * n * p.leadingCoeff := by positivity + nlinarith + have hFdeg : F.natDegree = n + 1 := natDegree_eq_of_le_of_coeff_ne_zero + (natDegree_add_le_of_degree_le hsdeg.le (natDegree_C_mul_X_pow_le b _)) + (by rw [hFcoeff]; exact hFlc.ne') + have hFpos : HasPosLeadingCoeff F := by + rw [HasPosLeadingCoeff, leadingCoeff, hFdeg, hFcoeff] + exact hFlc + refine ⟨hhdeg, hhpos, hreal, HasSimpleRoots.of_roots_nodup hne hnodup, + strictInterl_of_eval_mul_derivative_neg hsplit hhpos hFpos (by lia) (by lia) (by lia) ?_⟩ + intro r hr + obtain ⟨k, hk, hrk⟩ := hloc r hr + have hr1 := hinside r hr + have hFr : F.eval r = α * (r ^ 2 - 1) * p.derivative.eval r := by + rw [hFid] + simp [hr.eq_zero] + have hp' := derivative_mul_eval_pos (hAder k hk) (hAprod k hk) hrk + have hh' := hdsign k hk r hrk hr + have hhp := hsame (k + 1) hk + have hprod : 0 < h.derivative.eval r * p.derivative.eval r := by + have hmul : 0 < (h.derivative.eval r * p.derivative.eval r) * + (h.eval (A (k + 1)) * p.eval (A (k + 1))) := by + have := mul_pos hh' hp' + linarith [show (h.derivative.eval r * p.derivative.eval r) * + (h.eval (A (k + 1)) * p.eval (A (k + 1))) = + (h.derivative.eval r * h.eval (A (k + 1))) * + (p.derivative.eval r * p.eval (A (k + 1))) by ring] + exact (mul_pos_iff_of_pos_right hhp).mp hmul + have hsq : r ^ 2 - 1 < 0 := by nlinarith [hr1.1, hr1.2] + rw [hFr, show α * (r ^ 2 - 1) * p.derivative.eval r * h.derivative.eval r = + α * (r ^ 2 - 1) * (h.derivative.eval r * p.derivative.eval r) by ring] + exact mul_neg_of_neg_of_pos (mul_neg_of_pos_of_neg hα hsq) hprod + +/-- **Monomial perturbations of the centered Euler orbit** (RealRooted #2513, Theorem 1 in +centered coordinates). For `α ≥ 1 / 2`, `-1 < b ≤ 1` and `n > 0`, the polynomial +`h n = p n + b X ^ n` has degree `n`, positive leading coefficient and simple roots in `(-1, 1)`, +and `h n` strictly interlaces `h (n + 1)`. -/ +theorem centeredEulerOrbit_add_monomial {α b : ℝ} (hα : 1 / 2 ≤ α) (hb : -1 < b) (hb1 : b ≤ 1) + {n : ℕ} (hn : 0 < n) : + (centeredEulerOrbit α n + C b * X ^ n).natDegree = n ∧ + HasPosLeadingCoeff (centeredEulerOrbit α n + C b * X ^ n) ∧ + IsRealRootedIn (Ioo (-1 : ℝ) 1) (centeredEulerOrbit α n + C b * X ^ n) ∧ + HasSimpleRoots (centeredEulerOrbit α n + C b * X ^ n) ∧ + StrictInterl (centeredEulerOrbit α n + C b * X ^ n) + (centeredEulerOrbit α (n + 1) + C b * X ^ (n + 1)) := by + obtain ⟨hdeg, hpos, hroot, hsimple, hone, hmone⟩ := centeredEulerOrbit_package hα n + have hlc := one_le_leadingCoeff_centeredEulerOrbit (α := α) (by linarith) n + refine strictInterl_centeredEulerStep_add_monomial (by linarith) hb hn hdeg hroot hsimple hpos + (by linarith) hone hmone ?_ + intro c hc hcrit + have hbabs : |b| ≤ 1 := abs_le.mpr ⟨by linarith, hb1⟩ + rcases le_or_gt n 4 with h4 | h5 + · exact centeredEulerOrbit_small_critical hα hbabs hn h4 hc hcrit + · have h1 := centeredEulerOrbit_critical_values hα h5 c hc hcrit + have hcabs : |c| < 1 := abs_lt.mpr ⟨hc.1, hc.2⟩ + calc |b * c ^ n| = |b| * |c| ^ n := by rw [abs_mul, abs_pow] + _ ≤ 1 * |c| ^ n := by gcongr + _ < 1 := by rw [one_mul]; exact pow_lt_one₀ (abs_nonneg c) hcabs (by lia) + _ ≤ _ := h1 + +end RealRooted diff --git a/RealRooted/Mathlib/Algebra/Polynomial/CayleyTransform/Basic.lean b/RealRooted/Mathlib/Algebra/Polynomial/CayleyTransform/Basic.lean index 70e113335..b749c7038 100644 --- a/RealRooted/Mathlib/Algebra/Polynomial/CayleyTransform/Basic.lean +++ b/RealRooted/Mathlib/Algebra/Polynomial/CayleyTransform/Basic.lean @@ -8,6 +8,7 @@ module public import Mathlib.Algebra.Polynomial.Homogenize import RealRooted.Mathlib.Algebra.Polynomial.Homogenize public import Mathlib.Tactic.FinCases +public import Mathlib.Algebra.Polynomial.Derivative import Mathlib.Tactic.Ring /-! @@ -87,4 +88,74 @@ theorem cayleyTransform_eq_sum {p : R[X]} {n : ℕ} (hdeg : p.natDegree ≤ n) : rw [← Polynomial.C_eq_algebraMap] ring +/-- The Cayley transform of a monomial of degree at most `n`. -/ +theorem cayleyTransform_X_pow {n k : ℕ} (hk : k ≤ n) : + cayleyTransform n (X ^ k : R[X]) = X ^ k * (1 - X) ^ (n - k) := by + rw [cayleyTransform_eq_sum ((natDegree_X_pow_le k).trans hk), Finset.sum_eq_single k] + · simp + · intro j _ hj + simp [coeff_X_pow, hj] + · intro hk' + exact absurd (Finset.mem_range.mpr (Nat.lt_succ_of_le hk)) hk' + +/-- A polynomial of degree at most `n` as a sum of monomials. -/ +private theorem eq_sum_C_mul_X_pow {p : R[X]} {n : ℕ} (hp : p.natDegree ≤ n) : + p = ∑ k ∈ Finset.range (n + 1), C (p.coeff k) * X ^ k := by + conv_lhs => rw [as_sum_range' p (n + 1) (Nat.lt_succ_of_le hp)] + simp only [C_mul_X_pow_eq_monomial] + +/-- Raising the transform degree multiplies the Cayley transform by `1 - X`. -/ +theorem cayleyTransform_succ {p : R[X]} {n : ℕ} (hp : p.natDegree ≤ n) : + cayleyTransform (n + 1) p = (1 - X) * cayleyTransform n p := by + rw [eq_sum_C_mul_X_pow hp] + simp only [cayleyTransform_finset_sum, cayleyTransform_C_mul, Finset.mul_sum] + refine Finset.sum_congr rfl fun k hk ↦ ?_ + have hk : k ≤ n := Nat.lt_succ_iff.mp (Finset.mem_range.mp hk) + rw [cayleyTransform_X_pow (by lia), cayleyTransform_X_pow hk, + show n + 1 - k = n - k + 1 by lia, pow_succ] + ring + +/-- Multiplication by `X` commutes with the Cayley transform when the degree goes up by one. -/ +theorem cayleyTransform_succ_X_mul {p : R[X]} {n : ℕ} (hp : p.natDegree ≤ n) : + cayleyTransform (n + 1) (X * p) = X * cayleyTransform n p := by + rw [eq_sum_C_mul_X_pow hp] + simp only [Finset.mul_sum, cayleyTransform_finset_sum, cayleyTransform_C_mul] + refine Finset.sum_congr rfl fun k hk ↦ ?_ + have hk : k ≤ n := Nat.lt_succ_iff.mp (Finset.mem_range.mp hk) + rw [mul_left_comm, ← pow_succ', cayleyTransform_C_mul, cayleyTransform_X_pow (by lia), + cayleyTransform_X_pow hk, show n + 1 - (k + 1) = n - k by lia] + ring + +/-- `θ = X d/dX` on a monomial. -/ +private theorem X_mul_derivative_X_pow (k : ℕ) : + (X : R[X]) * (X ^ k).derivative = C (k : R) * X ^ k := by + rcases k with _ | k + · simp + · rw [derivative_X_pow, Nat.add_sub_cancel, ← mul_assoc, mul_comm X, mul_assoc, ← pow_succ'] + +/-- The Euler operator on the Cayley transform of a monomial. -/ +private theorem cayleyTransform_X_pow_euler {n k : ℕ} (hk : k ≤ n) : + X * (1 - X) * (X ^ k * (1 - X) ^ (n - k) : R[X]).derivative + + C (n : R) * X * (X ^ k * (1 - X) ^ (n - k)) = + C (k : R) * (X ^ k * (1 - X) ^ (n - k)) := by + obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_le hk + rw [Nat.add_sub_cancel_left] + rcases k with _ | k <;> rcases m with _ | m <;> + simp [derivative_mul, derivative_pow] <;> ring + +/-- The Euler operator `θ = X d/dX` under the Cayley transform: +`T (θ p) = X (1 - X) (T p)' + n X (T p)` for `p` of degree at most `n`. -/ +theorem cayleyTransform_X_mul_derivative {p : R[X]} {n : ℕ} (hp : p.natDegree ≤ n) : + cayleyTransform n (X * p.derivative) = + X * (1 - X) * (cayleyTransform n p).derivative + C (n : R) * X * cayleyTransform n p := by + rw [eq_sum_C_mul_X_pow hp] + simp only [derivative_sum, Finset.mul_sum, cayleyTransform_finset_sum, cayleyTransform_C_mul, + derivative_C_mul, ← Finset.sum_add_distrib] + refine Finset.sum_congr rfl fun k hk ↦ ?_ + have hk : k ≤ n := Nat.lt_succ_iff.mp (Finset.mem_range.mp hk) + rw [mul_left_comm, X_mul_derivative_X_pow] + simp only [cayleyTransform_C_mul, cayleyTransform_X_pow hk] + rw [← cayleyTransform_X_pow_euler hk] + ring + end Polynomial diff --git a/RealRooted/Mathlib/Analysis/Polynomial/InverseBernstein.lean b/RealRooted/Mathlib/Analysis/Polynomial/InverseBernstein.lean index 4ed2af302..fa6fb8535 100644 --- a/RealRooted/Mathlib/Analysis/Polynomial/InverseBernstein.lean +++ b/RealRooted/Mathlib/Analysis/Polynomial/InverseBernstein.lean @@ -181,16 +181,16 @@ theorem strictMonoOn_or_strictAntiOn_of_derivative_ne_zero {p : ℝ[X]} {u v : rw [interior_Icc] at hx simpa [Polynomial.deriv] using h x hx -/-- Alternation points: `-1 = C 0 < C 1 < ⋯ < C n = 1` with `|p (C k)| ≥ 1`, consecutive values of -opposite sign, and no zero of `p'` strictly between consecutive points. -/ -theorem exists_alternation_points {p : ℝ[X]} {n : ℕ} +/-- Sign alternation points: `-1 = C 0 < C 1 < ⋯ < C n = 1`, where the interior points are the +critical points of `p`, consecutive values of `p` have opposite signs, and no zero of `p'` lies +strictly between consecutive points. -/ +theorem exists_sign_alternation_points {p : ℝ[X]} {n : ℕ} (hn : 0 < n) (hdeg : p.natDegree = n) (hroots : (p.roots.filter (· ∈ Ioo (-1 : ℝ) 1)).card = n) - (hsimple : p.roots.Nodup) - (hone : p.eval 1 = 1) (hmone : p.eval (-1) = (-1) ^ n) - (hcrit : ∀ c ∈ Ioo (-1 : ℝ) 1, p.derivative.eval c = 0 → 1 ≤ |p.eval c|) : + (hsimple : p.roots.Nodup) : ∃ C : ℕ → ℝ, C 0 = -1 ∧ C n = 1 ∧ (∀ k < n, C k < C (k + 1)) ∧ - (∀ k ≤ n, 1 ≤ |p.eval (C k)|) ∧ (∀ k < n, p.eval (C k) * p.eval (C (k + 1)) < 0) ∧ + (∀ k, 0 < k → k < n → C k ∈ Ioo (-1 : ℝ) 1 ∧ p.derivative.eval (C k) = 0) ∧ + (∀ k < n, p.eval (C k) * p.eval (C (k + 1)) < 0) ∧ (∀ k < n, ∀ x ∈ Ioo (C k) (C (k + 1)), p.derivative.eval x ≠ 0) := by obtain ⟨r, c, hr, hrc, hcz⟩ := exists_roots_critical_points hn hdeg hroots hsimple let C : ℕ → ℝ := fun k ↦ if k = 0 then -1 else if k < n then c (k - 1) else 1 @@ -218,16 +218,12 @@ theorem exists_alternation_points {p : ℝ[X]} {n : ℕ} induction b, hab using Nat.le_induction with | base => exact le_rfl | succ b hab ih => exact (ih (by lia)).trans (hstep b (by lia)).le - have hcrit_C : ∀ k ≤ n, 1 ≤ |p.eval (C k)| := by - intro k hk - rcases Nat.eq_zero_or_pos k with rfl | hk0 - · rw [hC0, hmone, abs_pow, abs_neg, abs_one, one_pow] - by_cases hkn : k < n - · rw [hCmid k hk0 hkn] - have hj := hrc (k - 1) (by lia) - rw [show k - 1 + 1 = k by lia] at hj - refine hcrit _ ⟨(hr (k - 1) (by lia)).1.1.trans hj.1, hj.2.1.trans (hr k hkn).1.2⟩ hj.2.2 - · rw [show k = n by lia, hCn, hone, abs_one] + have hmid : ∀ k, 0 < k → k < n → C k ∈ Ioo (-1 : ℝ) 1 ∧ p.derivative.eval (C k) = 0 := by + intro k hk0 hkn + rw [hCmid k hk0 hkn] + have hj := hrc (k - 1) (by lia) + rw [show k - 1 + 1 = k by lia] at hj + exact ⟨⟨(hr (k - 1) (by lia)).1.1.trans hj.1, hj.2.1.trans (hr k hkn).1.2⟩, hj.2.2⟩ have hnoz : ∀ k < n, ∀ x ∈ Ioo (C k) (C (k + 1)), p.derivative.eval x ≠ 0 := by intro k hk x hx hx0 obtain ⟨j, hj, rfl⟩ := hcz x hx0 @@ -235,7 +231,7 @@ theorem exists_alternation_points {p : ℝ[X]} {n : ℕ} rcases Nat.lt_or_ge (j + 1) (k + 1) with h | h · exact (hx.1.trans_le' (hmono _ _ (by lia) (by lia))).false · exact (hx.2.trans_le (hmono _ _ h (by lia))).false - refine ⟨C, hC0, hCn, hstep, hcrit_C, fun k hk ↦ ?_, hnoz⟩ + refine ⟨C, hC0, hCn, hstep, hmid, fun k hk ↦ ?_, hnoz⟩ have hroot : p.eval (r k) = 0 := (hr k hk).2 have hlo := hC_lt_r k hk have hhi := hr_lt_C k hk @@ -255,6 +251,26 @@ theorem exists_alternation_points {p : ℝ[X]} {n : ℕ} simp only [hroot] at h1 h2 nlinarith + +/-- Alternation points: `-1 = C 0 < C 1 < ⋯ < C n = 1` with `|p (C k)| ≥ 1`, consecutive values of +opposite sign, and no zero of `p'` strictly between consecutive points. -/ +theorem exists_alternation_points {p : ℝ[X]} {n : ℕ} + (hn : 0 < n) (hdeg : p.natDegree = n) + (hroots : (p.roots.filter (· ∈ Ioo (-1 : ℝ) 1)).card = n) + (hsimple : p.roots.Nodup) + (hone : p.eval 1 = 1) (hmone : p.eval (-1) = (-1) ^ n) + (hcrit : ∀ c ∈ Ioo (-1 : ℝ) 1, p.derivative.eval c = 0 → 1 ≤ |p.eval c|) : + ∃ C : ℕ → ℝ, C 0 = -1 ∧ C n = 1 ∧ (∀ k < n, C k < C (k + 1)) ∧ + (∀ k ≤ n, 1 ≤ |p.eval (C k)|) ∧ (∀ k < n, p.eval (C k) * p.eval (C (k + 1)) < 0) ∧ + (∀ k < n, ∀ x ∈ Ioo (C k) (C (k + 1)), p.derivative.eval x ≠ 0) := by + obtain ⟨C, hC0, hCn, hstep, hmid, hprod, hnoz⟩ := + exists_sign_alternation_points hn hdeg hroots hsimple + refine ⟨C, hC0, hCn, hstep, fun k hk ↦ ?_, hprod, hnoz⟩ + rcases Nat.eq_zero_or_pos k with rfl | hk0 + · rw [hC0, hmone, abs_pow, abs_neg, abs_one, one_pow] + by_cases hkn : k < n + · exact hcrit _ (hmid k hk0 hkn).1 (hmid k hk0 hkn).2 + · rw [show k = n by lia, hCn, hone, abs_one] /-- A negative derivative at `x` gives a larger value somewhere in any interval `(a, x)`. -/ theorem _root_.HasDerivAt.exists_Ioo_lt_of_neg {f : ℝ → ℝ} {f' x a : ℝ} (hf : HasDerivAt f f' x) (hf' : f' < 0) (ha : a < x) : ∃ y ∈ Ioo a x, f x < f y := by @@ -775,4 +791,88 @@ theorem sq_mul_one_sub_sq_le_of_abs_eval_critical · rw [hcosx, mul_pow, neg_sq, hsin2] linarith +/-- A real polynomial of degree `n` whose values change sign across `n` consecutive intervals +`(C k, C (k + 1))` has simple roots, exactly one in each interval and no others, and at the root +in `(C k, C (k + 1))` its derivative has the sign of `h (C (k + 1))`. -/ +theorem roots_of_sign_changes {h : ℝ[X]} {n : ℕ} (hn : 0 < n) (hdeg : h.natDegree = n) + {C : ℕ → ℝ} (hC : ∀ k < n, C k < C (k + 1)) + (hsign : ∀ k < n, h.eval (C k) * h.eval (C (k + 1)) < 0) : + h.roots.Nodup ∧ h.roots.card = n ∧ + (∀ r, h.IsRoot r → ∃ k < n, r ∈ Ioo (C k) (C (k + 1))) ∧ + (∀ k < n, ∀ r ∈ Ioo (C k) (C (k + 1)), h.IsRoot r → + 0 < h.derivative.eval r * h.eval (C (k + 1))) := by + have hmono : ∀ a b, a ≤ b → b ≤ n → C a ≤ C b := by + intro a b hab hbn + induction b, hab using Nat.le_induction with + | base => exact le_rfl + | succ b hab ih => exact (ih (by lia)).trans (hC b (by lia)).le + have hne : h ≠ 0 := by + rintro rfl + simp at hdeg + lia + have hex : ∀ k < n, ∃ y ∈ Ioo (C k) (C (k + 1)), h.eval y = 0 := fun k hk ↦ + exists_Ioo_eq_zero_of_mul_neg (f := fun x ↦ h.eval x) h.continuous (hC k hk) (hsign k hk) + choose! z hz hz0 using hex + have hdisj : ∀ i < n, ∀ j < n, ∀ y, y ∈ Ioo (C i) (C (i + 1)) → + y ∈ Ioo (C j) (C (j + 1)) → i = j := by + intro i hi j hj y hyi hyj + by_contra hij + rcases Nat.lt_or_gt_of_ne hij with hlt | hlt + · linarith [hyi.2, hyj.1, hmono (i + 1) j hlt hj.le] + · linarith [hyj.2, hyi.1, hmono (j + 1) i hlt hi.le] + have hinj : Set.InjOn z (Finset.range n) := by + intro i hi j hj hij + have hi' : i < n := by simpa using hi + have hj' : j < n := by simpa using hj + exact hdisj i hi' j hj' (z i) (hz i hi') (hij ▸ hz j hj') + let Z := (Finset.range n).image z + have hZcard : Z.card = n := by rw [Finset.card_image_of_injOn hinj, Finset.card_range] + have hZle : Z.val ≤ h.roots := by + rw [Multiset.le_iff_subset Z.nodup] + intro y hy + obtain ⟨i, hi, rfl⟩ := Finset.mem_image.mp (Finset.mem_val.mp hy) + exact (mem_roots hne).mpr (hz0 i (Finset.mem_range.mp hi)) + have hroots : h.roots = Z.val := (Multiset.eq_of_le_of_card_le hZle (by + rw [Finset.card_val, hZcard, ← hdeg] + exact card_roots' h)).symm + have hroot_mem : ∀ r, h.IsRoot r → ∃ k < n, r = z k := by + intro r hr + have hr' : r ∈ Z := by + rw [← Finset.mem_val, ← hroots] + exact (mem_roots hne).mpr hr + obtain ⟨k, hk, rfl⟩ := Finset.mem_image.mp hr' + exact ⟨k, Finset.mem_range.mp hk, rfl⟩ + have hnodup : h.roots.Nodup := hroots ▸ Z.nodup + refine ⟨hnodup, by rw [hroots, Finset.card_val, hZcard], fun r hr ↦ ?_, ?_⟩ + · obtain ⟨k, hk, rfl⟩ := hroot_mem r hr + exact ⟨k, hk, hz k hk⟩ + intro k hk r hr hroot + have huniq : ∀ y ∈ Ioo (C k) (C (k + 1)), h.IsRoot y → y = z k := by + intro y hy hyr + obtain ⟨j, hj, rfl⟩ := hroot_mem y hyr + rw [hdisj j hj k hk (z j) (hz j hj) hy] + have hd : h.derivative.eval r ≠ 0 := by + intro hd0 + have h1 : 1 < h.rootMultiplicity r := + (one_lt_rootMultiplicity_iff_isRoot hne).mpr ⟨hroot, hd0⟩ + have h2 := Multiset.nodup_iff_count_le_one.mp hnodup r + rw [count_roots] at h2 + lia + have hc : h.eval (C (k + 1)) ≠ 0 := right_ne_zero_of_mul (hsign k hk).ne + by_contra hpos + have hneg : h.eval (C (k + 1)) * h.derivative.eval r < 0 := by + rw [mul_comm] + exact lt_of_le_of_ne (not_lt.mp hpos) (mul_ne_zero hd hc) + have hder : HasDerivAt (fun x ↦ h.eval (C (k + 1)) * h.eval x) + (h.eval (C (k + 1)) * h.derivative.eval r) r := (h.hasDerivAt r).const_mul _ + obtain ⟨y, hy, hgy⟩ := hder.exists_Ioo_gt_of_neg hneg hr.2 + replace hgy : h.eval (C (k + 1)) * h.eval y < 0 := by simpa [hroot.eq_zero] using hgy + obtain ⟨w, hw, hw0⟩ := exists_Ioo_eq_zero_of_mul_neg + (f := fun x ↦ h.eval (C (k + 1)) * h.eval x) (continuous_const.mul h.continuous) hy.2 + (mul_neg_of_neg_of_pos hgy (mul_self_pos.mpr hc)) + have hw' : h.IsRoot w := (mul_eq_zero.mp hw0).resolve_left hc + have := (huniq w ⟨hr.1.trans (hy.1.trans hw.1), hw.2⟩ hw').trans + (huniq r hr hroot).symm + linarith [hy.1, hw.1] + end Polynomial diff --git a/RealRooted/Production.lean b/RealRooted/Production.lean index c6441e8b0..5981f37c5 100644 --- a/RealRooted/Production.lean +++ b/RealRooted/Production.lean @@ -213,6 +213,7 @@ public import RealRooted.Challenges.PolyaFrequency.EdreiThoma public import RealRooted.Challenges.Roots.EnestromKakeya public import RealRooted.Challenges.Combinatorial.EulerBidiagonal public import RealRooted.Challenges.Combinatorial.EulerMultiplier +public import RealRooted.Challenges.Combinatorial.OrbitPerturbation public import RealRooted.Challenges.Combinatorial.Eulerian public import RealRooted.Challenges.Combinatorial.EulerianVariations public import RealRooted.Challenges.Combinatorial.LagTwoEulerianTriangles @@ -525,6 +526,10 @@ public import RealRooted.EulerOperator.Darboux.Basic public import RealRooted.EulerOperator.Darboux.Interlacing public import RealRooted.EulerOperator.Darboux.NegativeRoots public import RealRooted.EulerOperator.EulerMultiplier +public import RealRooted.EulerOperator.OrbitPerturbation +public import RealRooted.EulerOperator.OrbitPerturbationCayley +public import RealRooted.EulerOperator.OrbitPerturbationFamily +public import RealRooted.EulerOperator.OrbitPerturbationInterlacing public import RealRooted.EulerOperator.OrderNumerator.Basic public import RealRooted.EulerOperator.OrderNumerator.Preservation public import RealRooted.EulerOperator.Pencil diff --git a/scripts/import_architecture.json b/scripts/import_architecture.json index 901f0954d..1d2ccb439 100644 --- a/scripts/import_architecture.json +++ b/scripts/import_architecture.json @@ -16,10 +16,10 @@ ], "budgets": { "RealRooted": { - "max_modules": 2216 + "max_modules": 2221 }, "RealRooted.Production": { - "max_modules": 2146 + "max_modules": 2151 }, "RealRooted.Tactic.Examples": { "max_modules": 844