From 2d909492ac6b9ece9736801da4bb10915bd89541 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Wed, 21 Oct 2026 11:14:40 +0000 Subject: [PATCH 1/4] Golf OddPart, Hyperbolicity Statements unchanged; 181 lines shorter. Proofs drafted by a Codex worker, checked with the lakefile options and built locally. Co-Authored-By: Claude Opus 5.5 --- RealRooted/EdreiThoma/OddPart.lean | 182 ++++++------------------ RealRooted/Hyperbolicity.lean | 219 +++++++++-------------------- 2 files changed, 110 insertions(+), 291 deletions(-) diff --git a/RealRooted/EdreiThoma/OddPart.lean b/RealRooted/EdreiThoma/OddPart.lean index de66788f0..d2c2f4360 100644 --- a/RealRooted/EdreiThoma/OddPart.lean +++ b/RealRooted/EdreiThoma/OddPart.lean @@ -2,14 +2,12 @@ import RealRooted.Mathlib.Analysis.Complex.BorelGrowth section Quotient_part - /-! # Proximity of `e^G` when `e^G · M = K` with `M, K` entire This is where the first main theorem of value distribution theory (as in Mathlib) is used. -/ - open Complex Real Filter ValueDistribution noncomputable section @@ -17,8 +15,7 @@ noncomputable section namespace RealRooted.EdreiThoma private theorem posLog_norm_exp (w : ℂ) : log⁺ ‖Complex.exp w‖ = max w.re 0 := by - rw [Complex.norm_exp] - simp [Real.posLog, Real.log_exp, max_comm] + simp [Complex.norm_exp, Real.posLog, Real.log_exp, max_comm] /-- If `e^G · M = K` with `M, K` entire and `M ≢ 0`, then `posMean G r ≤ m(r, K) + m(r, M) + C` for `r ≥ 1`. -/ @@ -42,15 +39,11 @@ private theorem posMean_le_of_exp_mul_eq {G K M : ℂ → ℂ} have h2 := proximity_congr_codiscrete (a := ⊤) hcod hr0 have h3 := proximity_mul_top_le hKm hMm.inv r have h4 : proximity M⁻¹ ⊤ r ≤ characteristic M⁻¹ ⊤ r := by - unfold characteristic - simp only [Pi.add_apply, le_add_iff_nonneg_right] - exact logCounting_nonneg hr + simpa only [characteristic, Pi.add_apply, le_add_iff_nonneg_right] using logCounting_nonneg hr have h5 := characteristic_sub_characteristic_inv_of_ne_zero hMm hr0 have h6 : logCounting M ⊤ = 0 := by rw [logCounting_top] - have : (MeromorphicOn.divisor M Set.univ)⁻ = 0 := - negPart_eq_zero.mpr (MeromorphicOn.AnalyticOnNhd.divisor_nonneg hMa) - rw [this, map_zero] + rw [negPart_eq_zero.mpr (MeromorphicOn.AnalyticOnNhd.divisor_nonneg hMa), map_zero] have h7 : characteristic M ⊤ r = proximity M ⊤ r := by unfold characteristic; simp [h6] have h8 : proximity K ⊤ r = circleAverage (fun z => log⁺ ‖K z‖) 0 r := by @@ -66,7 +59,6 @@ end Quotient_part section KeyGrowth_part - /-! # The key growth estimate (an elementary substitute for the second main theorem) @@ -80,7 +72,6 @@ the first main theorem bounds `posMean g` by `m(r, K) + m(r, M)`, which only inv on a larger circle) and the growth of `P, Q`. Borel's lemma absorbs the logarithmic terms. -/ - open Complex Real Filter Topology noncomputable section @@ -102,8 +93,7 @@ private theorem circleAverage_posLog_le {K : ℂ → ℂ} (hK : Differentiable · exact MeromorphicOn.circleIntegrable_posLog_norm (fun z _ => (hK.analyticAt z).meromorphicAt) · intro z hz - rw [mem_sphere_zero_iff_norm, abs_of_pos hr] at hz - exact h z hz + rw [mem_sphere_zero_iff_norm, abs_of_pos hr] at hz; exact h z hz private theorem norm_deriv_le_exp {P : ℂ → ℂ} (hP : Differentiable ℂ P) {C : ℝ} (hC : 0 ≤ C) (hb : ∀ z, ‖P z‖ ≤ Real.exp (C * (1 + ‖z‖) ^ 2)) (z : ℂ) : @@ -140,8 +130,7 @@ private theorem posLog_norm_add_le (a b : ℂ) : (posLog_le_posLog (by linarith [norm_nonneg (a + b)]) (norm_add_le a b)).trans posLog_add private theorem posLog_norm_mul_le (a b : ℂ) : - log⁺ ‖a * b‖ ≤ log⁺ ‖a‖ + log⁺ ‖b‖ := by - rw [norm_mul]; exact posLog_mul + log⁺ ‖a * b‖ ≤ log⁺ ‖a‖ + log⁺ ‖b‖ := by rw [norm_mul]; exact posLog_mul private theorem posLog_norm_le_of_exp_bound {P : ℂ → ℂ} {C : ℝ} (hC : 0 ≤ C) (hb : ∀ z, ‖P z‖ ≤ Real.exp (C * (1 + ‖z‖) ^ 2)) (z : ℂ) : @@ -163,9 +152,7 @@ private theorem posMean_F_le {g F P Q : ℂ → ℂ} (hg : Differentiable ℂ g) ∃ C₁, 0 ≤ C₁ ∧ ∀ r, 1 ≤ r → posMean F r ≤ posMean g r + C₁ * (1 + r) ^ 2 := by set K : ℂ → ℂ := fun z => Complex.exp (g z / 2) * P z + Complex.exp (-(g z) / 2) * P (-z) - have hK : Differentiable ℂ K := by - have : Differentiable ℂ (fun z => P (-z)) := hP.comp differentiable_neg - fun_prop + have hK : Differentiable ℂ K := by simp only [K]; fun_prop have hM : Differentiable ℂ (fun z => 2 * Q z) := by fun_prop obtain ⟨C₀, hC₀⟩ := posMean_le_of_exp_mul_eq (G := F) hK hM (x₀ := 0) (by simp [hQ0]) (fun z => by simp only [K]; rw [heq z]; ring) @@ -225,10 +212,6 @@ private theorem posMean_F_le {g F P Q : ℂ → ℂ} (hg : Differentiable ℂ g) have h2 := mul_le_mul_of_nonneg_left hsq (abs_nonneg (g 0).re) have h3 := mul_le_mul_of_nonneg_left hsq (abs_nonneg C₀) have h4 : |(g 0).re| / 2 ≤ |(g 0).re| := by linarith [abs_nonneg (g 0).re] - have e : (3 * C + |(g 0).re| + 2 + |C₀|) * (1 + r) ^ 2 = - 3 * C * (1 + r) ^ 2 + |(g 0).re| * (1 + r) ^ 2 + - 2 * (1 + r) ^ 2 + |C₀| * (1 + r) ^ 2 := by ring - rw [e] linarith /-- The Wronskian-type combination `M`. -/ @@ -254,9 +237,8 @@ private theorem wronskian_identity {g F P Q : ℂ → ℂ} (hg : Differentiable (hg z).hasDerivAt.div_const 2 have h2 : HasDerivAt (fun w => -(g w) / 2) (-(deriv g z) / 2) z := (hg z).hasDerivAt.neg.div_const 2 - have h3 : HasDerivAt (fun w => P (-w)) (deriv P (-z) * (-1)) z := by - have := (hP (-z)).hasDerivAt.comp z (hasDerivAt_neg z) - exact this + have h3 : HasDerivAt (fun w => P (-w)) (deriv P (-z) * (-1)) z := + (hP (-z)).hasDerivAt.comp z (hasDerivAt_neg z) exact ((h1.cexp.mul (hP z).hasDerivAt)).add (h2.cexp.mul h3) have hR : HasDerivAt (fun w => 2 * Complex.exp (F w) * Q w) (2 * (Complex.exp (F z) * deriv F z) * Q z + 2 * Complex.exp (F z) * deriv Q z) z := @@ -357,20 +339,16 @@ private theorem norm_wM_bound {a b p p' q q' : ℂ} {E : ℝ} (hE : 0 ≤ E) (hq : ‖q‖ ≤ E) (hq' : ‖q'‖ ≤ E) : ‖q * (a / 2 * p + p') - (b * q + q') * p‖ ≤ E ^ 2 * (‖a‖ + ‖b‖ + 2) := by have h1 : ‖q * (a / 2 * p + p')‖ ≤ E * (‖a‖ * E + E) := by - rw [norm_mul] - apply mul_le_mul hq _ (norm_nonneg _) hE - refine (norm_add_le _ _).trans ?_ - rw [norm_mul, norm_div] + rw [norm_mul]; apply mul_le_mul hq _ (norm_nonneg _) hE + refine (norm_add_le _ _).trans ?_; rw [norm_mul, norm_div] simp only [Complex.norm_ofNat] have : ‖a‖ / 2 * ‖p‖ ≤ ‖a‖ * E := by have := mul_le_mul_of_nonneg_left hp (norm_nonneg a) nlinarith [norm_nonneg a, norm_nonneg p] linarith have h2 : ‖(b * q + q') * p‖ ≤ (‖b‖ * E + E) * E := by - rw [norm_mul] - apply mul_le_mul _ hp (norm_nonneg _) (by positivity) - refine (norm_add_le _ _).trans ?_ - rw [norm_mul] + rw [norm_mul]; apply mul_le_mul _ hp (norm_nonneg _) (by positivity) + refine (norm_add_le _ _).trans ?_; rw [norm_mul] have := mul_le_mul_of_nonneg_left hq (norm_nonneg b) linarith calc _ ≤ ‖q * (a / 2 * p + p')‖ + ‖(b * q + q') * p‖ := norm_sub_le _ _ @@ -381,26 +359,11 @@ private theorem norm_wK_bound {a b p p' q q' : ℂ} {E : ℝ} (hE : 0 ≤ E) (hp : ‖p‖ ≤ E) (hp' : ‖p'‖ ≤ E) (hq : ‖q‖ ≤ E) (hq' : ‖q'‖ ≤ E) : ‖(b * q + q') * p - q * (-p' - a / 2 * p)‖ ≤ E ^ 2 * (‖a‖ + ‖b‖ + 2) := by - have h1 : ‖(b * q + q') * p‖ ≤ (‖b‖ * E + E) * E := by - rw [norm_mul] - apply mul_le_mul _ hp (norm_nonneg _) (by positivity) - refine (norm_add_le _ _).trans ?_ - rw [norm_mul] - have := mul_le_mul_of_nonneg_left hq (norm_nonneg b) - linarith - have h2 : ‖q * (-p' - a / 2 * p)‖ ≤ E * (E + ‖a‖ * E) := by - rw [norm_mul] - apply mul_le_mul hq _ (norm_nonneg _) hE - refine (norm_sub_le _ _).trans ?_ - rw [norm_neg, norm_mul, norm_div] - simp only [Complex.norm_ofNat] - have : ‖a‖ / 2 * ‖p‖ ≤ ‖a‖ * E := by - have := mul_le_mul_of_nonneg_left hp (norm_nonneg a) - nlinarith [norm_nonneg a, norm_nonneg p] - linarith - calc _ ≤ ‖(b * q + q') * p‖ + ‖q * (-p' - a / 2 * p)‖ := norm_sub_le _ _ - _ ≤ (‖b‖ * E + E) * E + E * (E + ‖a‖ * E) := add_le_add h1 h2 - _ = E ^ 2 * (‖a‖ + ‖b‖ + 2) := by ring + calc + _ = ‖-(q * ((-a) / 2 * p + (-p')) - (b * q + q') * p)‖ := by congr 1; ring + _ = ‖q * ((-a) / 2 * p + (-p')) - (b * q + q') * p‖ := norm_neg _ + _ ≤ E ^ 2 * (‖-a‖ + ‖b‖ + 2) := norm_wM_bound hE hp (by simpa using hp') hq hq' + _ = E ^ 2 * (‖a‖ + ‖b‖ + 2) := by rw [norm_neg] private theorem differentiable_deriv' {f : ℂ → ℂ} (hf : Differentiable ℂ f) : Differentiable ℂ (deriv f) := @@ -428,7 +391,6 @@ private theorem key_GI {g F P Q : ℂ → ℂ} (hg : Differentiable ℂ g) linarith by_cases hdeg : ∀ z, wM g F P Q z = 0 · obtain ⟨l, hl2, hl⟩ := degenerate_identity hg hF hP hQ hP0 hQ0 heq hdeg - have hPm : Differentiable ℂ (fun z => P (-z)) := hP.comp differentiable_neg have hK : Differentiable ℂ (fun z => l * Q z * P (-z)) := by fun_prop have hM : Differentiable ℂ (fun z => (2 - l) * P z * Q z) := by fun_prop obtain ⟨C₀, hC₀⟩ := posMean_le_of_exp_mul_eq (G := g) hK hM (x₀ := 0) @@ -439,9 +401,8 @@ private theorem key_GI {g F P Q : ℂ → ℂ} (hg : Differentiable ℂ g) refine ⟨log⁺ ‖l‖ + log⁺ ‖2 - l‖ + |C₀| + 4 * C, hC', fun r ρ hr hrρ => ?_⟩ have hr0 : 0 < r := by linarith have hKb : circleAverage (fun z => log⁺ ‖l * Q z * P (-z)‖) 0 r ≤ - log⁺ ‖l‖ + 2 * C * (1 + r) ^ 2 := by - apply circleAverage_posLog_le hK hr0 - intro z hz + log⁺ ‖l‖ + 2 * C * (1 + r) ^ 2 := + circleAverage_posLog_le hK hr0 fun z hz => by have e1 := posLog_norm_mul_le (l * Q z) (P (-z)) have e2 := posLog_norm_mul_le l (Q z) have p1 := posLog_norm_le_of_exp_bound hC hQb z @@ -449,9 +410,8 @@ private theorem key_GI {g F P Q : ℂ → ℂ} (hg : Differentiable ℂ g) rw [hz] at p1; rw [norm_neg, hz] at p2 linarith have hMb : circleAverage (fun z => log⁺ ‖(2 - l) * P z * Q z‖) 0 r ≤ - log⁺ ‖2 - l‖ + 2 * C * (1 + r) ^ 2 := by - apply circleAverage_posLog_le hM hr0 - intro z hz + log⁺ ‖2 - l‖ + 2 * C * (1 + r) ^ 2 := + circleAverage_posLog_le hM hr0 fun z hz => by have e1 := posLog_norm_mul_le ((2 - l) * P z) (Q z) have e2 := posLog_norm_mul_le (2 - l) (P z) have p1 := posLog_norm_le_of_exp_bound hC hQb z @@ -466,10 +426,6 @@ private theorem key_GI {g F P Q : ℂ → ℂ} (hg : Differentiable ℂ g) have a2 := mul_le_mul_of_nonneg_left hsq (posLog_nonneg (x := ‖2 - l‖)) have a3 := mul_le_mul_of_nonneg_left hsq (abs_nonneg C₀) have a4 := le_abs_self C₀ - have e : (log⁺ ‖l‖ + log⁺ ‖2 - l‖ + |C₀| + 4 * C) * (1 + r) ^ 2 = - log⁺ ‖l‖ * (1 + r) ^ 2 + log⁺ ‖2 - l‖ * (1 + r) ^ 2 + |C₀| * (1 + r) ^ 2 + - 4 * C * (1 + r) ^ 2 := by ring - rw [e] linarith · push Not at hdeg obtain ⟨x₀, hx₀⟩ := hdeg @@ -477,8 +433,6 @@ private theorem key_GI {g F P Q : ℂ → ℂ} (hg : Differentiable ℂ g) have hF' := differentiable_deriv' hF have hP' := differentiable_deriv' hP have hQ' := differentiable_deriv' hQ - have hPm : Differentiable ℂ (fun z => P (-z)) := hP.comp differentiable_neg - have hPm' : Differentiable ℂ (fun z => deriv P (-z)) := hP'.comp differentiable_neg have hK : Differentiable ℂ (wK g F P Q) := by unfold wK; fun_prop have hM : Differentiable ℂ (wM g F P Q) := by unfold wM; fun_prop obtain ⟨C₀, hC₀⟩ := posMean_le_of_exp_mul_eq (G := g) hK hM hx₀ @@ -504,16 +458,8 @@ private theorem key_GI {g F P Q : ℂ → ℂ} (hg : Differentiable ℂ g) have b2 := mul_le_mul_of_nonneg_left hsq (abs_nonneg (F 0).re) have b3 := neg_le_abs (g 0).re have b4 := neg_le_abs (F 0).re - have e : C₂ * (1 + ρ) ^ 2 = 2 * (C₁ * (1 + ρ) ^ 2) + |(g 0).re| * (1 + ρ) ^ 2 + - |(F 0).re| * (1 + ρ) ^ 2 := by rw [hC₂]; ring - rw [e] - linarith - calc ‖deriv g z‖ + ‖deriv F z‖ - ≤ 2 * ρ / (ρ - r) ^ 2 * (2 * posMean g ρ - (g 0).re) + - 2 * ρ / (ρ - r) ^ 2 * (2 * posMean F ρ - (F 0).re) := add_le_add h1 h2 - _ = 2 * ρ / (ρ - r) ^ 2 * ((2 * posMean g ρ - (g 0).re) + - (2 * posMean F ρ - (F 0).re)) := by ring - _ ≤ D := mul_le_mul_of_nonneg_left hin hfac + nlinarith [hC₂] + nlinarith [mul_le_mul_of_nonneg_left hin hfac] set E := Real.exp (C * (2 + r) ^ 2) with hE have hE0 : 0 ≤ E := (Real.exp_pos _).le have hle : Real.exp (C * (1 + r) ^ 2) ≤ E := Real.exp_le_exp.mpr @@ -528,11 +474,9 @@ private theorem key_GI {g F P Q : ℂ → ℂ} (hg : Differentiable ℂ g) rw [hE, sq, ← Real.exp_add]; ring_nf rw [← this]; exact hX have hKb : circleAverage (fun z => log⁺ ‖wK g F P Q z‖) 0 r ≤ - 2 * C * (2 + r) ^ 2 + Real.log (D + 2) := by - apply circleAverage_posLog_le hK hr0 - intro z hz + 2 * C * (2 + r) ^ 2 + Real.log (D + 2) := + circleAverage_posLog_le hK hr0 fun z hz => by apply hlogb - have hd := hder z hz refine (norm_wK_bound (a := deriv g z) (b := deriv F z) (p := P (-z)) (p' := deriv P (-z)) (q := Q z) (q' := deriv Q z) hE0 ((hPb (-z)).trans (by rw [norm_neg, hz]; exact hle)) @@ -540,12 +484,11 @@ private theorem key_GI {g F P Q : ℂ → ℂ} (hg : Differentiable ℂ g) ((hQb z).trans (by rw [hz]; exact hle)) ((norm_deriv_le_exp hQ hC hQb z).trans (by rw [hz]))).trans ?_ gcongr + exact hder z hz have hMb : circleAverage (fun z => log⁺ ‖wM g F P Q z‖) 0 r ≤ - 2 * C * (2 + r) ^ 2 + Real.log (D + 2) := by - apply circleAverage_posLog_le hM hr0 - intro z hz + 2 * C * (2 + r) ^ 2 + Real.log (D + 2) := + circleAverage_posLog_le hM hr0 fun z hz => by apply hlogb - have hd := hder z hz refine (norm_wM_bound (a := deriv g z) (b := deriv F z) (p := P z) (p' := deriv P z) (q := Q z) (q' := deriv Q z) hE0 ((hPb z).trans (by rw [hz]; exact hle)) @@ -553,6 +496,7 @@ private theorem key_GI {g F P Q : ℂ → ℂ} (hg : Differentiable ℂ g) ((hQb z).trans (by rw [hz]; exact hle)) ((norm_deriv_le_exp hQ hC hQb z).trans (by rw [hz]))).trans ?_ gcongr + exact hder z hz have h := hC₀ r hr -- compare `log (D + 2)` with the target logarithm have hDle : D + 2 ≤ 2 + 2 * ρ / (ρ - r) ^ 2 * @@ -570,9 +514,6 @@ private theorem key_GI {g F P Q : ℂ → ℂ} (hg : Differentiable ℂ g) have a3 := mul_le_mul_of_nonneg_left hsq (abs_nonneg C₀) have a4 := le_abs_self C₀ have a5 : 0 ≤ C₂ * (1 + r) ^ 2 := by positivity - have e : (C₂ + 16 * C + |C₀|) * (1 + r) ^ 2 = - C₂ * (1 + r) ^ 2 + 16 * (C * (1 + r) ^ 2) + |C₀| * (1 + r) ^ 2 := by ring - rw [e] linarith /-- **Key growth estimate.** Under the functional identity @@ -597,12 +538,10 @@ end KeyGrowth_part section Products_part - /-! # Genus-zero products `∏ (1 + a_i z)` with `a_i ≥ 0` summable -/ - open Complex Real Filter Topology noncomputable section @@ -614,8 +553,7 @@ private def gprod (a : ℕ → ℝ) (z : ℂ) : ℂ := ∏' i, (1 + (a i : ℂ) variable {a : ℕ → ℝ} -private theorem gprod_zero (a : ℕ → ℝ) : gprod a 0 = 1 := by - simp [gprod] +private theorem gprod_zero (a : ℕ → ℝ) : gprod a 0 = 1 := by simp [gprod] private theorem gprod_differentiable (ha : ∀ i, 0 ≤ a i) (s : Summable a) : Differentiable ℂ (gprod a) := by @@ -636,9 +574,7 @@ private theorem gprod_differentiable (ha : ∀ i, 0 ≤ a i) (s : Summable a) : apply DifferentiableOn.fun_finsetProd intro i _ fun_prop - apply hd.differentiableAt - apply hU.mem_nhds - simp [R] + exact hd.differentiableAt (hU.mem_nhds (by simp [R])) private theorem norm_gprod_le (ha : ∀ i, 0 ≤ a i) (s : Summable a) (z : ℂ) : ‖gprod a z‖ ≤ Real.exp ((∑' i, a i) * ‖z‖) := by @@ -673,12 +609,10 @@ end Products_part section Assembly_part - /-! # Assembly: from Edrei's functional identity to the quadratic growth of the odd part -/ - open Complex Real Filter Topology noncomputable section @@ -698,15 +632,11 @@ private theorem odd_quadratic_is_linear {g : ℂ → ℂ} (hodd : ∀ z, g (-z) rw [hgp, Polynomial.eval_eq_sum_range' (n := 3) (by lia)] simp [Finset.sum_range_succ] have h0 : p.coeff 0 = 0 := by - have := hodd 0 - rw [neg_zero] at this - have h : g 0 = p.coeff 0 := by simpa using hev 0 - have : g 0 = 0 := by linear_combination this / 2 - rw [this] at h; exact h.symm + have h := hodd 0; rw [neg_zero] at h + have hg0 : g 0 = 0 := by linear_combination h / 2 + simpa [hg0] using (hev 0).symm have h2 : p.coeff 2 = 0 := by - have a := hodd 1 - rw [hev, hev] at a - rw [h0] at a + have a := hodd 1; rw [hev, hev, h0] at a linear_combination a / 2 refine ⟨p.coeff 1 / 2, fun z => ?_⟩ rw [hev, h0, h2]; ring @@ -737,20 +667,8 @@ private theorem entire_identity {φ φs : ℂ → ℂ} (hφ : Differentiable ℂ Complex.exp (φ (-z)) * (gprod α (-z) * gprod β (-z) * gprod βs (-(-z) ^ 2)) set R : ℂ → ℂ := fun z => 2 * Complex.exp (φs (z ^ 2)) * (gprod αs (z ^ 2) * gprod β (-z) * gprod β z) - have hL : Differentiable ℂ L := by - have h1 : Differentiable ℂ (fun z => φ (-z)) := hφ.comp differentiable_neg - have h2 : Differentiable ℂ (fun z : ℂ => gprod α (-z)) := dα.comp differentiable_neg - have h3 : Differentiable ℂ (fun z : ℂ => gprod β (-z)) := dβ.comp differentiable_neg - have h4 : Differentiable ℂ (fun z : ℂ => gprod βs (-z ^ 2)) := - dβs.comp (by fun_prop) - have h5 : Differentiable ℂ (fun z : ℂ => gprod βs (-(-z) ^ 2)) := - dβs.comp (by fun_prop) - fun_prop - have hR : Differentiable ℂ R := by - have h3 : Differentiable ℂ (fun z : ℂ => gprod β (-z)) := dβ.comp differentiable_neg - have h6 : Differentiable ℂ (fun z : ℂ => gprod αs (z ^ 2)) := dαs.comp (by fun_prop) - have h7 : Differentiable ℂ (fun z : ℂ => φs (z ^ 2)) := hφs.comp (by fun_prop) - fun_prop + have hL : Differentiable ℂ L := by simp only [L]; fun_prop + have hR : Differentiable ℂ R := by simp only [R]; fun_prop -- the three denominators are nonzero near `0` have c1 : ∀ᶠ z in 𝓝 (0 : ℂ), gprod β (-z) ≠ 0 := ((dβ.comp differentiable_neg).continuous.continuousAt (x := 0)).eventually_ne @@ -771,9 +689,8 @@ private theorem entire_identity {φ φs : ℂ → ℂ} (hφ : Differentiable ℂ simp only [L, R, neg_sq] field_simp at h linear_combination h - have := AnalyticOnNhd.eq_of_eventuallyEq (fun z _ => hL.analyticAt z) - (fun z _ => hR.analyticAt z) hev - exact fun z => congrFun this z + exact fun z => congrFun (AnalyticOnNhd.eq_of_eventuallyEq + (fun z _ => hL.analyticAt z) (fun z _ => hR.analyticAt z) hev) z /-- Under the hypotheses of `odd_part_linear`, the odd part `g(z) = φ(z) - φ(-z)` satisfies `T(r, e^g) = posMean g r ≤ A (1 + r)^2`. -/ @@ -800,18 +717,10 @@ private theorem odd_part_growth {φ φs : ℂ → ℂ} (hφ : Differentiable ℂ set F : ℂ → ℂ := fun z => φs (z ^ 2) - (φ z + φ (-z)) / 2 with hF_def set P : ℂ → ℂ := fun z => gprod α z * gprod β z * gprod βs (-z ^ 2) with hP_def set Q : ℂ → ℂ := fun z => gprod αs (z ^ 2) * gprod β (-z) * gprod β z with hQ_def - have hφm : Differentiable ℂ (fun z => φ (-z)) := hφ.comp differentiable_neg have hg : Differentiable ℂ g := by simp only [hg_def]; fun_prop - have hF : Differentiable ℂ F := by - have : Differentiable ℂ (fun z : ℂ => φs (z ^ 2)) := hφs.comp (by fun_prop) - simp only [hF_def]; fun_prop - have hP : Differentiable ℂ P := by - have h4 : Differentiable ℂ (fun z : ℂ => gprod βs (-z ^ 2)) := dβs.comp (by fun_prop) - simp only [hP_def]; fun_prop - have hQ : Differentiable ℂ Q := by - have h3 : Differentiable ℂ (fun z : ℂ => gprod β (-z)) := dβ.comp differentiable_neg - have h6 : Differentiable ℂ (fun z : ℂ => gprod αs (z ^ 2)) := dαs.comp (by fun_prop) - simp only [hQ_def]; fun_prop + have hF : Differentiable ℂ F := by simp only [hF_def]; fun_prop + have hP : Differentiable ℂ P := by simp only [hP_def]; fun_prop + have hQ : Differentiable ℂ Q := by simp only [hQ_def]; fun_prop have hP0 : P 0 = 1 := by simp [hP_def, gprod_zero] have hQ0 : Q 0 = 1 := by simp [hQ_def, gprod_zero] set C := (∑' i, α i) + 2 * (∑' i, β i) + (∑' i, βs i) + (∑' i, αs i) with hC_def @@ -823,8 +732,7 @@ private theorem odd_part_growth {φ φs : ℂ → ℂ} (hφ : Differentiable ℂ have hz1 : ∀ z : ℂ, ‖z‖ ≤ (1 + ‖z‖) ^ 2 := fun z => by nlinarith [norm_nonneg z] have hz2 : ∀ z : ℂ, ‖z‖ ^ 2 ≤ (1 + ‖z‖) ^ 2 := fun z => by nlinarith [norm_nonneg z] have hPb : ∀ z, ‖P z‖ ≤ Real.exp (C * (1 + ‖z‖) ^ 2) := by - intro z - simp only [hP_def, norm_mul] + intro z; simp only [hP_def, norm_mul] have b1 := norm_gprod_le hα sα z have b2 := norm_gprod_le hβ sβ z have b3 := norm_gprod_le hβs sβs (-z ^ 2) @@ -838,7 +746,6 @@ private theorem odd_part_growth {φ φs : ℂ → ℂ} (hφ : Differentiable ℂ rw [Real.exp_add, Real.exp_add] _ ≤ Real.exp (C * (1 + ‖z‖) ^ 2) := by apply Real.exp_le_exp.mpr - have := hz1 z; have := hz2 z have a1 := mul_le_mul_of_nonneg_left (hz1 z) hSα have a2 := mul_le_mul_of_nonneg_left (hz1 z) hSβ have a3 := mul_le_mul_of_nonneg_left (hz2 z) hSβs @@ -846,8 +753,7 @@ private theorem odd_part_growth {φ φs : ℂ → ℂ} (hφ : Differentiable ℂ simp only [hC_def] nlinarith have hQb : ∀ z, ‖Q z‖ ≤ Real.exp (C * (1 + ‖z‖) ^ 2) := by - intro z - simp only [hQ_def, norm_mul] + intro z; simp only [hQ_def, norm_mul] have b1 := norm_gprod_le hαs sαs (z ^ 2) have b2 := norm_gprod_le hβ sβ (-z) have b3 := norm_gprod_le hβ sβ z diff --git a/RealRooted/Hyperbolicity.lean b/RealRooted/Hyperbolicity.lean index a60238fa0..2b32b66b3 100644 --- a/RealRooted/Hyperbolicity.lean +++ b/RealRooted/Hyperbolicity.lean @@ -60,20 +60,9 @@ theorem continuous_coeff_affineLineRestriction_comp (continuous_const : Continuous fun _ : T => (Polynomial.C r).coeff k) | add P Q hP hQ => - have hP' : Continuous fun t => - ((MvPolynomial.eval₂Hom Polynomial.C - (fun i => Polynomial.C (a t i) + - Polynomial.C (b i) * Polynomial.X) P)).coeff k := by - simpa [MvPolynomial.affineLineRestriction] using hP k - have hQ' : Continuous fun t => - ((MvPolynomial.eval₂Hom Polynomial.C - (fun i => Polynomial.C (a t i) + - Polynomial.C (b i) * Polynomial.X) Q)).coeff k := by - simpa [MvPolynomial.affineLineRestriction] using hQ k - change Continuous fun t => - ((MvPolynomial.eval₂Hom Polynomial.C - (fun i => Polynomial.C (a t i) + - Polynomial.C (b i) * Polynomial.X) (P + Q))).coeff k + have hP' := hP k + have hQ' := hQ k + simp only [MvPolynomial.affineLineRestriction] at hP' hQ' ⊢ simp_rw [map_add, coeff_add] fun_prop | mul_X P i hP => @@ -155,11 +144,9 @@ theorem MvPolynomial.HyperbolicAt.affineLineRestriction_splits_ne_zero (x : σ → ℝ) : (MvPolynomial.affineLineRestriction x e P).Splits ∧ MvPolynomial.affineLineRestriction x e P ≠ 0 := by - refine ⟨hP.2 x, ?_⟩ - intro hzero + refine ⟨hP.2 x, fun hzero => hP.1 ?_⟩ have hcoeff := MvPolynomial.IsHomogeneous.coeff_realAffineLineRestriction hhom x e - apply hP.1 rw [realAffineLineRestriction_eq_affineLineRestriction, hzero] at hcoeff simpa using hcoeff.symm @@ -170,10 +157,8 @@ theorem MvPolynomial.eval_ne_zero_of_affineLineRestriction_isRoot_neg (hneg : ∀ r, (MvPolynomial.affineLineRestriction u e P).IsRoot r → r < 0) : MvPolynomial.eval u P ≠ 0 := by intro hu - have hroot : (MvPolynomial.affineLineRestriction u e P).IsRoot 0 := by - rw [Polynomial.IsRoot, MvPolynomial.eval_affineLineRestriction] - simpa using hu - exact (lt_irrefl 0) (hneg 0 hroot) + exact (hneg 0 (by simpa [Polynomial.IsRoot, + MvPolynomial.eval_affineLineRestriction] using hu)).false /-- Along a path in the nonvanishing locus from a hyperbolic direction, the roots of the affine restriction in that direction stay strictly negative. -/ @@ -187,14 +172,8 @@ theorem MvPolynomial.HyperbolicAt.affineLineRestriction_isRoot_neg_of_joinedIn let q : unitInterval → ℝ[X] := fun t => Polynomial.C c * MvPolynomial.affineLineRestriction (γ t) e P have hrestrictionDegree (t : unitInterval) : - (MvPolynomial.affineLineRestriction (γ t) e P).natDegree = d := by - apply Polynomial.natDegree_eq_of_le_of_coeff_ne_zero - · simpa [← realAffineLineRestriction_eq_affineLineRestriction] using - MvPolynomial.IsHomogeneous.natDegree_realAffineLineRestriction_le - hhom (γ t) e - · simpa [← realAffineLineRestriction_eq_affineLineRestriction] using - (MvPolynomial.IsHomogeneous.coeff_realAffineLineRestriction - hhom (γ t) e).trans_ne he.1 + (MvPolynomial.affineLineRestriction (γ t) e P).natDegree = d := + hhom.natDegree_affineLineRestriction_eq (γ t) e he.1 have hdegree (t : unitInterval) : (q t).natDegree = d := by rw [show q t = Polynomial.C c * MvPolynomial.affineLineRestriction (γ t) e P by rfl, @@ -202,13 +181,8 @@ theorem MvPolynomial.HyperbolicAt.affineLineRestriction_isRoot_neg_of_joinedIn hrestrictionDegree] have hmonic (t : unitInterval) : (q t).Monic := by apply Polynomial.monic_C_mul_of_mul_leadingCoeff_eq_one - rw [Polynomial.leadingCoeff, hrestrictionDegree] - simp only [c] - rw [show (MvPolynomial.affineLineRestriction (γ t) e P).coeff d = - MvPolynomial.eval e P by - simpa [← realAffineLineRestriction_eq_affineLineRestriction] using - MvPolynomial.IsHomogeneous.coeff_realAffineLineRestriction - hhom (γ t) e] + rw [Polynomial.leadingCoeff, hrestrictionDegree, + hhom.coeff_affineLineRestriction] exact inv_mul_cancel₀ he.1 have hsplits (t : unitInterval) : (q t).Splits := (he.2 (γ t)).C_mul c @@ -227,10 +201,7 @@ theorem MvPolynomial.HyperbolicAt.affineLineRestriction_isRoot_neg_of_joinedIn rw [Polynomial.eval_mul, Polynomial.eval_C, MvPolynomial.eval_affineLineRestriction] simpa [c] using mul_ne_zero (inv_ne_zero he.1) hpath - have hr0 : r ≠ 0 := by - intro hrzero - subst r - exact hqzero hr + have hr0 : r ≠ 0 := fun hrzero => hqzero (by simpa [hrzero] using hr) exact lt_or_gt_of_ne hr0 have hstart : ∀ r, (q (0 : unitInterval)).IsRoot r → r ∈ Set.Iio 0 := by intro r hr @@ -252,11 +223,7 @@ theorem MvPolynomial.HyperbolicAt.affineLineRestriction_isRoot_neg_of_joinedIn have htransport : ∀ r, (q (1 : unitInterval)).IsRoot r → r ∈ Set.Iio 0 := by apply Polynomial.forall_isRoot_mem_of_isPreconnected q hmonic hdegree hd hcoeff hsplits isOpen_Iio isOpen_Ioi - · exact Set.disjoint_left.mpr (by - intro r hrneg hrpos - change r < 0 at hrneg - change 0 < r at hrpos - exact (not_lt_of_ge hrpos.le) hrneg) + · exact Set.Ioi_disjoint_Iio_same.symm · exact hcover · exact isPreconnected_univ · exact Set.mem_univ (0 : unitInterval) @@ -282,16 +249,8 @@ theorem MvPolynomial.HyperbolicAt.linearPlaneRestriction_mvRealStable have hq0 : q ≠ 0 := (MvPolynomial.HyperbolicAt.affineLineRestriction_splits_ne_zero he hhom u).2 - have hqle : q.natDegree ≤ d := by - simpa [q, realAffineLineRestriction_eq_affineLineRestriction] using - MvPolynomial.IsHomogeneous.natDegree_realAffineLineRestriction_le - hhom u e - have hqcoeff : q.coeff d = MvPolynomial.eval e P := by - simpa [q, realAffineLineRestriction_eq_affineLineRestriction] using - MvPolynomial.IsHomogeneous.coeff_realAffineLineRestriction hhom u e - have hqd : q.natDegree = d := - Polynomial.natDegree_eq_of_le_of_coeff_ne_zero hqle - (hqcoeff.trans_ne he.1) + have hqd : q.natDegree = d := by + simpa only [q] using hhom.natDegree_affineLineRestriction_eq u e he.1 rw [MvPolynomial.IsHomogeneous.linearPlaneRestriction_eq_homogenize hhom e u, ← hqd] exact BorceaBranden.homogenizeBivariate_stable_of_splits_nonpos @@ -325,14 +284,10 @@ theorem MvPolynomial.HyperbolicAt.complex_affineLineRestriction_isRoot_im_neg hhom.map Complex.ofRealHom have hueval : MvPolynomial.eval uC (complexifyMv P) = (MvPolynomial.eval u P : ℂ) := by - unfold uC complexifyMv - change MvPolynomial.eval (Complex.ofRealHom ∘ u) - (MvPolynomial.map Complex.ofRealHom P) = - Complex.ofRealHom (MvPolynomial.eval u P) - exact (MvPolynomial.map_eval Complex.ofRealHom u P).symm - have hueval0 : MvPolynomial.eval uC (complexifyMv P) ≠ 0 := by - rw [hueval] - exact Complex.ofReal_ne_zero.mpr hu + simpa [uC, complexifyMv, Function.comp_def] using + (MvPolynomial.map_eval Complex.ofRealHom u P).symm + have hueval0 : MvPolynomial.eval uC (complexifyMv P) ≠ 0 := + hueval.trans_ne (Complex.ofReal_ne_zero.mpr hu) have hrestrictionDegree (γ : ℝ) : (MvPolynomial.affineLineRestriction (a γ) uC (complexifyMv P)).natDegree = d := @@ -348,22 +303,20 @@ theorem MvPolynomial.HyperbolicAt.complex_affineLineRestriction_isRoot_im_neg hhomC.coeff_affineLineRestriction, hueval] exact inv_mul_cancel₀ (Complex.ofReal_ne_zero.mpr hu) have hcoeff (k : ℕ) : Continuous fun γ => (q γ).coeff k := by - have ha (i : σ) : Continuous fun γ : ℝ => a γ i := by - dsimp only [a, eC] - fun_prop - have hrestriction := continuous_coeff_affineLineRestriction_comp - (complexifyMv P) a ha uC k - simpa [q, c, Polynomial.coeff_C_mul] using hrestriction.const_mul c + simpa [q, c, Polynomial.coeff_C_mul] using + (continuous_coeff_affineLineRestriction_comp (complexifyMv P) a + (by intro i; dsimp only [a, eC]; fun_prop) uC k).const_mul c + have hqroot (γ : ℝ) (z : ℂ) (hz : (q γ).IsRoot z) : + MvPolynomial.eval (fun i => a γ i + uC i * z) (complexifyMv P) = 0 := by + rw [Polynomial.IsRoot] at hz + dsimp only [q] at hz + rw [Polynomial.eval_mul, Polynomial.eval_C, + MvPolynomial.eval_affineLineRestriction] at hz + exact (mul_eq_zero.mp hz).resolve_left + (inv_ne_zero (Complex.ofReal_ne_zero.mpr hu)) have havoid (γ : ℝ) (z : ℂ) (hz : (q γ).IsRoot z) : z.im ≠ 0 := by intro hzim - have hbaseeval : MvPolynomial.eval - (fun i => a γ i + uC i * z) (complexifyMv P) = 0 := by - rw [Polynomial.IsRoot] at hz - dsimp only [q] at hz - rw [Polynomial.eval_mul, Polynomial.eval_C, - MvPolynomial.eval_affineLineRestriction] at hz - exact (mul_eq_zero.mp hz).resolve_left - (inv_ne_zero (Complex.ofReal_ne_zero.mpr hu)) + have hbaseeval := hqroot γ z hz let y : σ → ℝ := fun i => γ * x i + z.re * u i have hreval : (realAffineLineRestriction y e P).aeval (Complex.I * (α : ℂ)) = 0 := by @@ -406,14 +359,7 @@ theorem MvPolynomial.HyperbolicAt.complex_affineLineRestriction_isRoot_im_neg exfalso apply hstable rw [eval_complexifyMv_linearPlaneRestriction] - have hbaseeval : MvPolynomial.eval - (fun i => a 0 i + uC i * z) (complexifyMv P) = 0 := by - rw [Polynomial.IsRoot] at hz - dsimp only [q] at hz - rw [Polynomial.eval_mul, Polynomial.eval_C, - MvPolynomial.eval_affineLineRestriction] at hz - exact (mul_eq_zero.mp hz).resolve_left - (inv_ne_zero (Complex.ofReal_ne_zero.mpr hu)) + have hbaseeval := hqroot 0 z hz convert hbaseeval using 1 apply congrArg (fun w : σ → ℂ => MvPolynomial.eval w (complexifyMv P)) @@ -468,14 +414,10 @@ theorem MvPolynomial.HyperbolicAt.of_affineLineRestriction_isRoot_neg hhom.map Complex.ofRealHom have hueval : MvPolynomial.eval uC (complexifyMv P) = (MvPolynomial.eval u P : ℂ) := by - unfold uC complexifyMv - change MvPolynomial.eval (Complex.ofRealHom ∘ u) - (MvPolynomial.map Complex.ofRealHom P) = - Complex.ofRealHom (MvPolynomial.eval u P) - exact (MvPolynomial.map_eval Complex.ofRealHom u P).symm - have hueval0 : MvPolynomial.eval uC (complexifyMv P) ≠ 0 := by - rw [hueval] - exact Complex.ofReal_ne_zero.mpr hu + simpa [uC, complexifyMv, Function.comp_def] using + (MvPolynomial.map_eval Complex.ofRealHom u P).symm + have hueval0 : MvPolynomial.eval uC (complexifyMv P) ≠ 0 := + hueval.trans_ne (Complex.ofReal_ne_zero.mpr hu) have hrestrictionDegree (α : ℝ) : (MvPolynomial.affineLineRestriction (a α) uC (complexifyMv P)).natDegree = d := @@ -491,12 +433,9 @@ theorem MvPolynomial.HyperbolicAt.of_affineLineRestriction_isRoot_neg hhomC.coeff_affineLineRestriction, hueval] exact inv_mul_cancel₀ (Complex.ofReal_ne_zero.mpr hu) have hcoeff (k : ℕ) : Continuous fun α => (q α).coeff k := by - have ha (i : σ) : Continuous fun α : ℝ => a α i := by - dsimp only [a, eC] - fun_prop - have hrestriction := continuous_coeff_affineLineRestriction_comp - (complexifyMv P) a ha uC k - simpa [q, c, Polynomial.coeff_C_mul] using hrestriction.const_mul c + simpa [q, c, Polynomial.coeff_C_mul] using + (continuous_coeff_affineLineRestriction_comp (complexifyMv P) a + (by intro i; dsimp only [a, eC]; fun_prop) uC k).const_mul c have hnoUpper (w : ℂ) (hw : (MvPolynomial.affineLineRestriction x u P).aeval w = 0) (hwpos : 0 < w.im) : False := by @@ -570,15 +509,12 @@ theorem MvPolynomial.HyperbolicAt.linearPlaneRestriction_mvRealStable_of_joinedI {σ : Type*} {P : MvPolynomial σ ℝ} {d : ℕ} {e u : σ → ℝ} (he : P.HyperbolicAt e) (hhom : P.IsHomogeneous d) (hd : d ≠ 0) (hjoin : JoinedIn {x | MvPolynomial.eval x P ≠ 0} e u) : - MvRealStable (MvPolynomial.linearPlaneRestriction e u P) := by - apply MvPolynomial.HyperbolicAt.linearPlaneRestriction_mvRealStable - he hhom - intro r hr - apply (MvPolynomial.HyperbolicAt.affineLineRestriction_isRoot_neg_of_joinedIn - he hhom hd hjoin r ?_).le - exact (Polynomial.mem_roots - (MvPolynomial.HyperbolicAt.affineLineRestriction_splits_ne_zero - he hhom u).2).mp hr + MvRealStable (MvPolynomial.linearPlaneRestriction e u P) := + MvPolynomial.HyperbolicAt.linearPlaneRestriction_mvRealStable he hhom fun r hr => + (MvPolynomial.HyperbolicAt.affineLineRestriction_isRoot_neg_of_joinedIn + he hhom hd hjoin r <| (Polynomial.mem_roots + (MvPolynomial.HyperbolicAt.affineLineRestriction_splits_ne_zero + he hhom u).2).mp hr).le /-- Hyperbolicity is constant on a path component of the nonvanishing locus of a homogeneous polynomial. -/ @@ -589,10 +525,7 @@ theorem MvPolynomial.HyperbolicAt.of_joinedIn P.HyperbolicAt u := by by_cases hd : d = 0 · subst d - have hP0 : P ≠ 0 := by - intro hzero - apply he.1 - simp [hzero] + have hP0 : P ≠ 0 := fun hzero => he.1 (by simp [hzero]) have hconst : P = MvPolynomial.C (P.coeff 0) := MvPolynomial.totalDegree_eq_zero_iff_eq_C.mp (hhom.totalDegree hP0) rw [hconst] at he ⊢ @@ -628,12 +561,10 @@ theorem mvRealStable_of_forall_hyperbolicAt_pos (hhom : P.IsHomogeneous d) (hP : ∀ e : σ → ℝ, (∀ i, 0 < e i) → P.HyperbolicAt e) : MvRealStable P := by - apply mvRealStable_of_forall_realAffineLineRestriction - intro a b hb - have hh := hP b hb + refine mvRealStable_of_forall_realAffineLineRestriction fun a b hb => ?_ simpa [realAffineLineRestriction_eq_affineLineRestriction] using MvPolynomial.HyperbolicAt.affineLineRestriction_splits_ne_zero - hh hhom a + (hP b hb) hhom a /-- A homogeneous polynomial is real stable exactly when it is hyperbolic in every strictly positive direction. -/ @@ -657,13 +588,10 @@ private theorem restriction_ordinaryHomogenization_eq_of_none_ne_zero intro t rw [eval_realAffineLineRestriction, Polynomial.eval_mul, Polynomial.eval_C, eval_realAffineLineRestriction] - have hvec : - (fun o => x o + Option.elim o 0 b * t) = - fun o => Option.elim o (x none) - (fun i => x (some i) + b i * t) := by - funext o - cases o <;> simp - rw [hvec, + rw [show (fun o => x o + Option.elim o 0 b * t) = + fun o => Option.elim o (x none) (fun i => x (some i) + b i * t) by + funext o + cases o <;> simp, MvPolynomial.eval_ordinaryHomogenization_eq_pow_mul_eval_div P le_rfl hx] congr 1 @@ -681,12 +609,11 @@ private theorem restriction_ordinaryHomogenization_eq_of_none_eq_zero apply Polynomial.funext intro t rw [eval_realAffineLineRestriction, eval_realAffineLineRestriction] - have hvec : - (fun o => x o + Option.elim o 0 b * t) = - fun o => Option.elim o 0 (fun i => x (some i) + b i * t) := by - funext o - cases o <;> simp [hx] - rw [hvec, MvPolynomial.eval_ordinaryHomogenization_zero] + rw [show (fun o => x o + Option.elim o 0 b * t) = + fun o => Option.elim o 0 (fun i => x (some i) + b i * t) by + funext o + cases o <;> simp [hx], + MvPolynomial.eval_ordinaryHomogenization_zero] private theorem realAffineLineRestriction_neg_direction {σ : Type*} (P : MvPolynomial σ ℝ) (a b : σ → ℝ) : @@ -710,10 +637,8 @@ theorem MvRealStable.ordinaryHomogenization_hyperbolicAt_boundary let Htop := MvPolynomial.homogeneousComponent P.totalDegree P have hHtopNe : Htop ≠ 0 := MvPolynomial.homogeneousComponent_totalDegree_ne_zero hP - have hHtopNN : MvPolynomial.HasNonnegCoeffs Htop := - hnn.homogeneousComponent P.totalDegree have hEvalTopPos : 0 < MvPolynomial.eval b Htop := - hHtopNN.eval_pos hHtopNe hb + (hnn.homogeneousComponent P.totalDegree).eval_pos hHtopNe hb have hEval : MvPolynomial.eval e H = MvPolynomial.eval b Htop := by simpa [e, H, Htop] using MvPolynomial.eval_ordinaryHomogenization_zero P P.totalDegree b @@ -729,18 +654,14 @@ theorem MvRealStable.ordinaryHomogenization_hyperbolicAt_boundary rcases lt_or_gt_of_ne hx with hxneg | hxpos · let a : σ → ℝ := fun i => x (some i) / x none let c : σ → ℝ := fun i => -(b i / x none) - have hc : ∀ i, 0 < c i := by - intro i - exact neg_pos.mpr (div_neg_of_pos_of_neg (hb i) hxneg) + have hc : ∀ i, 0 < c i := fun i => + neg_pos.mpr (div_neg_of_pos_of_neg (hb i) hxneg) have hsplits := (hst.realAffineLineRestriction_splits_ne_zero a c hc).1 - have hreflect : - realAffineLineRestriction (fun i => x (some i) / x none) - (fun i => b i / x none) P = - (realAffineLineRestriction a c P).comp (-Polynomial.X) := by - simpa [a, c] using - realAffineLineRestriction_neg_direction P a c - rw [hreflect] + rw [show realAffineLineRestriction (fun i => x (some i) / x none) + (fun i => b i / x none) P = + (realAffineLineRestriction a c P).comp (-Polynomial.X) by + simpa [a, c] using realAffineLineRestriction_neg_direction P a c] exact hsplits.comp_neg_X.C_mul _ · exact ((hst.realAffineLineRestriction_splits_ne_zero (fun i => x (some i) / x none) (fun i => b i / x none) @@ -815,13 +736,10 @@ theorem MvRealStable.commonRotationStable_complexify_of_hasNonnegCoeffs {σ : Type*} {P : MvPolynomial σ ℝ} (hst : MvRealStable P) (hnn : MvPolynomial.HasNonnegCoeffs P) : MvCommonRotationStable (complexifyMv P) := by - have hhomogenized := hst.ordinaryHomogenization hnn hst.ne_zero - have hrotation := + simpa only [MvPolynomial.dehomogenize_ordinaryHomogenization] using (mvRealStable_iff_commonRotation_dehomogenize (MvPolynomial.ordinaryHomogenization_isHomogeneous P P.totalDegree)).mp - hhomogenized - rw [MvPolynomial.dehomogenize_ordinaryHomogenization] at hrotation - exact hrotation + (hst.ordinaryHomogenization hnn hst.ne_zero) /-- Ordinary homogenization in any degree at least the total degree preserves real stability for nonzero polynomials with nonnegative coefficients. -/ @@ -854,12 +772,7 @@ theorem mvUpperHalfPlaneStableOrZero_complexify_ordinaryHomogenization · left rw [hzero] simp [complexifyMv, MvPolynomial.ordinaryHomogenization] - · have hP : P ≠ 0 := by - intro hzero - subst P - have h := hst (fun _ => Complex.I) (fun _ => by simp) - exact h (by simp [complexifyMv]) - exact Or.inr (hst.ordinaryHomogenization_of_totalDegree_le hnn hP hdeg) + · exact Or.inr (hst.ordinaryHomogenization_of_totalDegree_le hnn hst.ne_zero hdeg) end From 8a2ea50d7a1ec87f3268db3e0054428ea9ea1834 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Wed, 21 Oct 2026 11:19:18 +0000 Subject: [PATCH 2/4] Golf GeneralizedSnakePosets, MorrisDFlow Statements unchanged; 229 lines shorter. Proofs drafted by a Codex worker, checked with the lakefile options and built locally. Co-Authored-By: Claude Opus 5.5 --- RealRooted/GeneralizedSnakePosets.lean | 308 ++++---------- .../MultivariateStability/MorrisDFlow.lean | 397 +++++++----------- 2 files changed, 238 insertions(+), 467 deletions(-) diff --git a/RealRooted/GeneralizedSnakePosets.lean b/RealRooted/GeneralizedSnakePosets.lean index c39582ad3..052d9752a 100644 --- a/RealRooted/GeneralizedSnakePosets.lean +++ b/RealRooted/GeneralizedSnakePosets.lean @@ -76,9 +76,7 @@ def partitionPrefix (lam : List ℕ) (i : ℕ) : List ℕ := theorem partitionPrefix_getD_of_lt {lam : List ℕ} {row i : ℕ} (hrow : row < i) : (partitionPrefix lam i).getD row 0 = lam.getD row 0 := by - rw [partitionPrefix, List.getD_eq_getElem?_getD, - List.getD_eq_getElem?_getD, List.getElem?_take] - simp [hrow] + simp [partitionPrefix, List.getD_eq_getElem?_getD, hrow] /-- A list of row lengths is an integer partition in Braun--Jal's sense: positive parts in weakly decreasing order. -/ @@ -92,13 +90,7 @@ def firstColumnCells (lam : List ℕ) : Finset (ℕ × ℕ) := @[simp] theorem mem_firstColumnCells {lam : List ℕ} {a : ℕ × ℕ} : a ∈ firstColumnCells lam ↔ a.1 < lam.length ∧ a.2 = 1 := by classical - rw [firstColumnCells, Finset.mem_image] - constructor - · rintro ⟨row, hrow, rfl⟩ - exact ⟨Finset.mem_range.mp hrow, rfl⟩ - · rintro ⟨hrow, hcol⟩ - refine ⟨a.1, Finset.mem_range.mpr hrow, ?_⟩ - ext <;> simp [hcol] + simp [firstColumnCells, Prod.ext_iff, eq_comm] /-- Remove a first-column rook and shift all remaining columns left by one. -/ def firstColumnRemainder (i : ℕ) (P : Finset (ℕ × ℕ)) : @@ -188,12 +180,8 @@ def nonNestingPlacementsWithFirstColumn (lam : List ℕ) : ∃ a ∈ firstColumnCells lam, a ∈ P := by classical rw [nonNestingPlacementsWithFirstColumn, Finset.mem_biUnion] - constructor - · rintro ⟨a, ha, hP⟩ - rw [mem_nonNestingPlacementsWithCell] at hP - exact ⟨hP.1, ⟨a, ha, hP.2⟩⟩ - · rintro ⟨hP, a, ha, haP⟩ - exact ⟨a, ha, mem_nonNestingPlacementsWithCell.mpr ⟨hP, haP⟩⟩ + simp only [mem_nonNestingPlacementsWithCell] + grind /-- First-column-free placements and placements using the first column are disjoint. -/ @@ -203,13 +191,9 @@ theorem disjoint_nonNestingPlacementsWithoutFirstColumn_withFirstColumn (nonNestingPlacementsWithFirstColumn lam) := by classical rw [Finset.disjoint_left] - intro P hfree hfirst - rw [mem_nonNestingPlacementsWithoutFirstColumn] at hfree - rw [mem_nonNestingPlacementsWithFirstColumn] at hfirst - rcases hfirst.2 with ⟨a, ha, haP⟩ - have hcol : a.2 = 1 := (mem_firstColumnCells.mp ha).2 - have hcell : (a.1, 1) = a := by ext <;> simp [hcol] - exact hfree.2 a.1 (by simpa [hcell] using haP) + simp only [mem_nonNestingPlacementsWithoutFirstColumn, + mem_nonNestingPlacementsWithFirstColumn, mem_firstColumnCells] + grind /-- Valid Ferrers placements split into those avoiding the first column and those using it. -/ @@ -220,18 +204,17 @@ theorem union_nonNestingPlacementsWithoutFirstColumn_withFirstColumn (ferrers lam).nonNestingPlacements := by classical ext P - rw [Finset.mem_union, mem_nonNestingPlacementsWithoutFirstColumn, + simp only [Finset.mem_union, mem_nonNestingPlacementsWithoutFirstColumn, mem_nonNestingPlacementsWithFirstColumn, mem_nonNestingPlacements] constructor - · rintro (h | h) <;> exact h.1 + · grind · intro hP by_cases hfirst : ∃ row, (row, 1) ∈ P - · rcases hfirst with ⟨row, hrowP⟩ - have hcell := hP.1 hrowP - rw [mem_ferrers_cells] at hcell - exact Or.inr ⟨hP, ⟨(row, 1), mem_firstColumnCells.mpr - ⟨hcell.1, rfl⟩, hrowP⟩⟩ - · exact Or.inl ⟨hP, fun row hrowP => hfirst ⟨row, hrowP⟩⟩ + · obtain ⟨row, hrowP⟩ := hfirst + right + refine ⟨hP, (row, 1), ?_, hrowP⟩ + exact mem_firstColumnCells.mpr ⟨(mem_ferrers_cells.mp (hP.1 hrowP)).1, rfl⟩ + · exact Or.inl ⟨hP, by grind⟩ /-- A valid placement can contain at most one first-column cell. -/ theorem pairwiseDisjoint_nonNestingPlacementsWithCell_firstColumn @@ -248,14 +231,11 @@ theorem pairwiseDisjoint_nonNestingPlacementsWithCell_firstColumn subst Q have hcol_a : a.2 = 1 := (mem_firstColumnCells.mp ha).2 have hcol_b : b.2 = 1 := (mem_firstColumnCells.mp hb).2 - by_cases hrow : a.1 = b.1 - · have hab : a = b := by ext <;> simp [hrow, hcol_a, hcol_b] - exact hne hab - · rcases Nat.lt_or_gt_of_ne hrow with hlt | hgt - · have hcol := hPa.1.2.2 a hPa.2 b hQ.2 hlt - simp [hcol_a, hcol_b] at hcol - · have hcol := hPa.1.2.2 b hQ.2 a hPa.2 hgt - simp [hcol_a, hcol_b] at hcol + rcases lt_trichotomy a.1 b.1 with hlt | hrow | hgt + · simpa [hcol_a, hcol_b] using hPa.1.2.2 a hPa.2 b hQ.2 hlt + · apply hne + ext <;> simp_all + · simpa [hcol_a, hcol_b] using hPa.1.2.2 b hQ.2 a hPa.2 hgt /-- The sum over placements using the first column is the sum over fixed first-column cells. -/ @@ -283,10 +263,10 @@ theorem sum_nonNestingPlacements_eq_withoutFirstColumn_add_withFirstColumn ((ferrers lam).nonNestingPlacementsWithCell a).sum (fun P => (X : ℝ[X]) ^ P.card)) := by classical - rw [← union_nonNestingPlacementsWithoutFirstColumn_withFirstColumn lam] - rw [Finset.sum_union - (disjoint_nonNestingPlacementsWithoutFirstColumn_withFirstColumn lam)] - rw [sum_nonNestingPlacementsWithFirstColumn] + rw [← union_nonNestingPlacementsWithoutFirstColumn_withFirstColumn lam, + Finset.sum_union + (disjoint_nonNestingPlacementsWithoutFirstColumn_withFirstColumn lam), + sum_nonNestingPlacementsWithFirstColumn] /-- Deleting the first column sends a first-column-free placement in `lam` to a placement in `partitionSubOne lam`. -/ @@ -316,10 +296,7 @@ theorem deleteFirstColumnPlacement_isNonNestingPlacement rw [deleteFirstColumnPlacement] at hx hy rcases Finset.mem_image.mp hx with ⟨a, ha, rfl⟩ rcases Finset.mem_image.mp hy with ⟨b, hb, rfl⟩ - have hab : a ≠ b := by - intro hab - subst b - exact hxy rfl + have hab : a ≠ b := by grind exact hP.2.1 a ha b hb hab · intro x hx y hy hxy rw [deleteFirstColumnPlacement] at hx hy @@ -358,10 +335,7 @@ theorem addFirstColumnPlacement_isNonNestingPlacement rw [addFirstColumnPlacement] at hx hy rcases Finset.mem_image.mp hx with ⟨a, ha, rfl⟩ rcases Finset.mem_image.mp hy with ⟨b, hb, rfl⟩ - have hab : a ≠ b := by - intro hab - subst b - exact hxy rfl + have hab : a ≠ b := by grind exact hP.2.1 a ha b hb hab · intro x hx y hy hxy rw [addFirstColumnPlacement] at hx hy @@ -388,19 +362,7 @@ theorem deleteFirstColumnPlacement_addFirstColumnPlacement deleteFirstColumnPlacement (addFirstColumnPlacement P) = P := by classical ext x - constructor - · intro hx - rw [deleteFirstColumnPlacement, addFirstColumnPlacement] at hx - rcases Finset.mem_image.mp hx with ⟨y, hy, hxy⟩ - rcases Finset.mem_image.mp hy with ⟨a, ha, hay⟩ - subst y - have hxa : x = a := by simpa using hxy.symm - simpa [hxa] using ha - · intro hx - rw [deleteFirstColumnPlacement, addFirstColumnPlacement] - refine Finset.mem_image.mpr ⟨(x.1, x.2 + 1), ?_, ?_⟩ - · exact Finset.mem_image.mpr ⟨x, hx, rfl⟩ - · simp + simp [deleteFirstColumnPlacement, addFirstColumnPlacement, Prod.ext_iff] /-- Adding back a deleted first column recovers a placement that avoided the first column. -/ @@ -409,21 +371,24 @@ theorem addFirstColumnPlacement_deleteFirstColumnPlacement addFirstColumnPlacement (deleteFirstColumnPlacement P) = P := by classical ext x + simp only [addFirstColumnPlacement, deleteFirstColumnPlacement, + Finset.mem_image] constructor + · rintro ⟨_, ⟨a, ha, rfl⟩, rfl⟩ + simpa [Nat.sub_add_cancel (Nat.le_of_lt (hcol a ha))] using ha · intro hx - rw [addFirstColumnPlacement, deleteFirstColumnPlacement] at hx - rcases Finset.mem_image.mp hx with ⟨y, hy, hxy⟩ - rcases Finset.mem_image.mp hy with ⟨a, ha, hay⟩ - subst y - have hone : 1 ≤ a.2 := Nat.le_of_lt (hcol a ha) - have hxa : x = a := by simpa [Nat.sub_add_cancel hone] using hxy.symm - simpa [hxa] using ha - · intro hx - rw [addFirstColumnPlacement, deleteFirstColumnPlacement] - refine Finset.mem_image.mpr ⟨(x.1, x.2 - 1), ?_, ?_⟩ - · exact Finset.mem_image.mpr ⟨x, hx, rfl⟩ - · have hone : 1 ≤ x.2 := Nat.le_of_lt (hcol x hx) - ext <;> simp [Nat.sub_add_cancel hone] + exact ⟨(x.1, x.2 - 1), ⟨x, hx, rfl⟩, + by simp [Nat.sub_add_cancel (Nat.le_of_lt (hcol x hx))]⟩ + +private theorem shiftLeft_injOn {P : Finset (ℕ × ℕ)} + (hcol : ∀ a ∈ P, 1 < a.2) : + Set.InjOn (fun a : ℕ × ℕ => (a.1, a.2 - 1)) ↑P := by + intro a ha b hb hmap + have hrow : a.1 = b.1 := by simpa using congrArg Prod.fst hmap + have hcol_sub : a.2 - 1 = b.2 - 1 := by simpa using congrArg Prod.snd hmap + apply Prod.ext hrow + rw [← Nat.sub_add_cancel (Nat.le_of_lt (hcol a ha)), hcol_sub, + Nat.sub_add_cancel (Nat.le_of_lt (hcol b hb))] /-- Deleting the first column preserves cardinality for placements avoiding that column. -/ @@ -432,19 +397,7 @@ theorem deleteFirstColumnPlacement_card (deleteFirstColumnPlacement P).card = P.card := by classical rw [deleteFirstColumnPlacement] - have hinj : Set.InjOn (fun a : ℕ × ℕ => (a.1, a.2 - 1)) ↑P := by - intro a ha b hb hmap - have hrow : a.1 = b.1 := by simpa using congrArg (fun x : ℕ × ℕ => x.1) hmap - have hcol_sub : a.2 - 1 = b.2 - 1 := by simpa using congrArg (fun x : ℕ × ℕ => x.2) hmap - have haone : 1 ≤ a.2 := Nat.le_of_lt (hcol a ha) - have hbone : 1 ≤ b.2 := Nat.le_of_lt (hcol b hb) - have hcol_eq : a.2 = b.2 := by - calc - a.2 = (a.2 - 1) + 1 := (Nat.sub_add_cancel haone).symm - _ = (b.2 - 1) + 1 := by rw [hcol_sub] - _ = b.2 := Nat.sub_add_cancel hbone - exact Prod.ext hrow hcol_eq - exact Finset.card_image_of_injOn hinj + exact Finset.card_image_of_injOn (shiftLeft_injOn hcol) /-- A first-column-free valid placement has every rook strictly after the first column. -/ @@ -506,28 +459,12 @@ theorem sum_nonNestingPlacementsWithoutFirstColumn_eq_partitionSubOne (fun P => (X : ℝ[X]) ^ P.card) = ferrersRookPolynomial (partitionSubOne lam) := by classical - let S := nonNestingPlacementsWithoutFirstColumn lam - let T := (ferrers (partitionSubOne lam)).nonNestingPlacements - have himage : S.image deleteFirstColumnPlacement = T := by - simpa [S, T] using deleteFirstColumnPlacement_image_withoutFirstColumn lam - have hinj : Set.InjOn deleteFirstColumnPlacement ↑S := by - simpa [S] using deleteFirstColumnPlacement_injOn_withoutFirstColumn lam - have hsum_image : - (S.image deleteFirstColumnPlacement).sum (fun Q => (X : ℝ[X]) ^ Q.card) = - S.sum (fun P => (X : ℝ[X]) ^ (deleteFirstColumnPlacement P).card) := by - simpa using - (Finset.sum_image (s := S) (g := deleteFirstColumnPlacement) - (f := fun Q => (X : ℝ[X]) ^ Q.card) hinj) - calc - S.sum (fun P => (X : ℝ[X]) ^ P.card) - = S.sum (fun P => (X : ℝ[X]) ^ (deleteFirstColumnPlacement P).card) := by - apply Finset.sum_congr rfl - intro P hP - rw [deleteFirstColumnPlacement_card - (one_lt_col_of_mem_withoutFirstColumn (by simpa [S] using hP))] - _ = T.sum (fun Q => (X : ℝ[X]) ^ Q.card) := by rw [← hsum_image, himage] - _ = ferrersRookPolynomial (partitionSubOne lam) := by - rw [ferrersRookPolynomial, rookPolynomial_eq_nonNestingPlacements_sum] + rw [ferrersRookPolynomial, rookPolynomial_eq_nonNestingPlacements_sum, + ← deleteFirstColumnPlacement_image_withoutFirstColumn lam, + Finset.sum_image (deleteFirstColumnPlacement_injOn_withoutFirstColumn lam)] + apply Finset.sum_congr rfl + intro P hP + rw [deleteFirstColumnPlacement_card (one_lt_col_of_mem_withoutFirstColumn hP)] /-- After erasing a first-column rook, every remaining rook lies in a row above it. -/ @@ -594,10 +531,7 @@ theorem firstColumnRemainder_isNonNestingPlacement rcases Finset.mem_image.mp hy with ⟨b, hb, rfl⟩ have haP : a ∈ P := (Finset.mem_erase.mp ha).2 have hbP : b ∈ P := (Finset.mem_erase.mp hb).2 - have hab : a ≠ b := by - intro hab - subst b - exact hxy rfl + have hab : a ≠ b := by grind exact hP.2.1 a haP b hbP hab · intro x hx y hy hxy rw [firstColumnRemainder] at hx hy @@ -610,6 +544,15 @@ theorem firstColumnRemainder_isNonNestingPlacement rw [mem_ferrers_cells] at hb_cell exact Nat.sub_lt_sub_right hb_cell.2.1 hcol +private theorem row_lt_of_mem_partitionPrefix_subOne + {lam : List ℕ} {Q : Finset (ℕ × ℕ)} {i : ℕ} + (hQ : + (ferrers (partitionPrefix (partitionSubOne lam) i)).IsNonNestingPlacement Q) + {a : ℕ × ℕ} (ha : a ∈ Q) : a.1 < i := by + have hlen := (mem_ferrers_cells.mp (hQ.1 ha)).1 + rw [partitionPrefix_length] at hlen + exact (lt_min_iff.mp (by simpa [partitionSubOne] using hlen)).1 + /-- Reinsert a first-column rook and shift a valid remainder right by one column. -/ theorem firstColumnExtension_isNonNestingPlacement @@ -628,10 +571,9 @@ theorem firstColumnExtension_isNonNestingPlacement rcases a with ⟨row, col⟩ have ha_cell := hQ.1 ha rw [mem_ferrers_cells] at ha_cell ⊢ - have hrow_pair : row < i ∧ row < lam.length := by - have hlen := ha_cell.1 - rw [partitionPrefix_length] at hlen - exact lt_min_iff.mp (by simpa [partitionSubOne] using hlen) + have hrow_pair : row < i ∧ row < lam.length := + ⟨row_lt_of_mem_partitionPrefix_subOne hQ ha, + (lt_min_iff.mp (by simpa [partitionSubOne] using ha_cell.1)).2⟩ refine ⟨hrow_pair.2, by lia, ?_⟩ rw [partitionPrefix_getD_of_lt hrow_pair.1, partitionSubOne_getD] at ha_cell lia @@ -641,28 +583,13 @@ theorem firstColumnExtension_isNonNestingPlacement · rcases Finset.mem_insert.mp hy with rfl | hy · exact (hxy rfl).elim · rcases Finset.mem_image.mp hy with ⟨b, hb, rfl⟩ - have hb_cell := hQ.1 hb - rw [mem_ferrers_cells] at hb_cell - have hrow_lt : b.1 < i := by - have hlen := hb_cell.1 - rw [partitionPrefix_length] at hlen - exact (lt_min_iff.mp (by simpa [partitionSubOne] using hlen)).1 - exact ne_of_gt hrow_lt + exact ne_of_gt (row_lt_of_mem_partitionPrefix_subOne hQ (a := b) hb) · rcases Finset.mem_insert.mp hy with rfl | hy · rcases Finset.mem_image.mp hx with ⟨a, ha, rfl⟩ - have ha_cell := hQ.1 ha - rw [mem_ferrers_cells] at ha_cell - have hrow_lt : a.1 < i := by - have hlen := ha_cell.1 - rw [partitionPrefix_length] at hlen - exact (lt_min_iff.mp (by simpa [partitionSubOne] using hlen)).1 - exact ne_of_lt hrow_lt + exact ne_of_lt (row_lt_of_mem_partitionPrefix_subOne hQ (a := a) ha) · rcases Finset.mem_image.mp hx with ⟨a, ha, rfl⟩ rcases Finset.mem_image.mp hy with ⟨b, hb, rfl⟩ - have hab : a ≠ b := by - intro hab - subst b - exact hxy rfl + have hab : a ≠ b := by grind exact hQ.2.1 a ha b hb hab · intro x hx y hy hxy rw [firstColumnExtension] at hx hy @@ -670,13 +597,8 @@ theorem firstColumnExtension_isNonNestingPlacement · rcases Finset.mem_insert.mp hy with rfl | hy · exact (Nat.lt_irrefl i hxy).elim · rcases Finset.mem_image.mp hy with ⟨b, hb, rfl⟩ - have hb_cell := hQ.1 hb - rw [mem_ferrers_cells] at hb_cell - have hrow_lt : b.1 < i := by - have hlen := hb_cell.1 - rw [partitionPrefix_length] at hlen - exact (lt_min_iff.mp (by simpa [partitionSubOne] using hlen)).1 - exact (not_lt_of_ge (Nat.le_of_lt hrow_lt) hxy).elim + exact (not_lt_of_ge + (Nat.le_of_lt (row_lt_of_mem_partitionPrefix_subOne hQ hb)) hxy).elim · rcases Finset.mem_insert.mp hy with rfl | hy · rcases Finset.mem_image.mp hx with ⟨a, ha, rfl⟩ have ha_cell := hQ.1 ha @@ -695,22 +617,8 @@ theorem firstColumnRemainder_card_add_one (firstColumnRemainder i P).card + 1 = P.card := by classical rw [firstColumnRemainder] - have hinj : - Set.InjOn (fun a : ℕ × ℕ => (a.1, a.2 - 1)) ↑(P.erase (i, 1)) := by - intro a ha b hb hmap - have hrow : a.1 = b.1 := by simpa using congrArg (fun x : ℕ × ℕ => x.1) hmap - have hcol_sub : a.2 - 1 = b.2 - 1 := by simpa using congrArg (fun x : ℕ × ℕ => x.2) hmap - have haone : 1 ≤ a.2 := - Nat.le_of_lt (one_lt_col_of_mem_erase_firstColumn hP hfirst a ha) - have hbone : 1 ≤ b.2 := - Nat.le_of_lt (one_lt_col_of_mem_erase_firstColumn hP hfirst b hb) - have hcol : a.2 = b.2 := by - calc - a.2 = (a.2 - 1) + 1 := (Nat.sub_add_cancel haone).symm - _ = (b.2 - 1) + 1 := by rw [hcol_sub] - _ = b.2 := Nat.sub_add_cancel hbone - exact Prod.ext hrow hcol - rw [Finset.card_image_of_injOn hinj] + rw [Finset.card_image_of_injOn + (shiftLeft_injOn (one_lt_col_of_mem_erase_firstColumn hP hfirst))] exact Finset.card_erase_add_one hfirst /-- Shifting a valid fixed-row remainder right and inserting first-column @@ -726,13 +634,7 @@ theorem firstColumnExtension_card intro hi rcases Finset.mem_image.mp hi with ⟨a, ha, hmap⟩ have hrow : a.1 = i := by simpa using congrArg (fun x : ℕ × ℕ => x.1) hmap - have ha_cell := hQ.1 ha - rw [mem_ferrers_cells] at ha_cell - have hrow_lt : a.1 < i := by - have hlen := ha_cell.1 - rw [partitionPrefix_length] at hlen - exact (lt_min_iff.mp (by simpa [partitionSubOne] using hlen)).1 - exact (ne_of_lt hrow_lt hrow).elim + exact (ne_of_lt (row_lt_of_mem_partitionPrefix_subOne hQ ha) hrow).elim have hinj : Set.InjOn (fun a : ℕ × ℕ => (a.1, a.2 + 1)) ↑Q := by intro a _ha b _hb hmap @@ -752,13 +654,7 @@ theorem firstColumnRook_not_mem_addFirstColumnPlacement rw [addFirstColumnPlacement] at hi rcases Finset.mem_image.mp hi with ⟨a, ha, hmap⟩ have hrow : a.1 = i := by simpa using congrArg (fun x : ℕ × ℕ => x.1) hmap - have ha_cell := hQ.1 ha - rw [mem_ferrers_cells] at ha_cell - have hrow_lt : a.1 < i := by - have hlen := ha_cell.1 - rw [partitionPrefix_length] at hlen - exact (lt_min_iff.mp (by simpa [partitionSubOne] using hlen)).1 - exact (ne_of_lt hrow_lt hrow).elim + exact (ne_of_lt (row_lt_of_mem_partitionPrefix_subOne hQ ha) hrow).elim /-- Taking the remainder of an extended fixed-row placement recovers the original remainder. -/ @@ -843,35 +739,15 @@ theorem sum_nonNestingPlacementsWithFirstColumnCell_eq_mul_partitionPrefix (fun P => (X : ℝ[X]) ^ P.card) = X * ferrersRookPolynomial (partitionPrefix (partitionSubOne lam) i) := by classical - let S := (ferrers lam).nonNestingPlacementsWithCell (i, 1) - let T := (ferrers (partitionPrefix (partitionSubOne lam) i)).nonNestingPlacements - have himage : S.image (firstColumnRemainder i) = T := by - simpa [S, T] - using firstColumnRemainder_image_nonNestingPlacementsWithCell hfirst_cell - have hinj : Set.InjOn (firstColumnRemainder i) ↑S := by - simpa [S] using - (firstColumnRemainder_injOn_nonNestingPlacementsWithCell (lam := lam) - (i := i)) - have hsum_image : - (S.image (firstColumnRemainder i)).sum (fun Q => (X : ℝ[X]) ^ Q.card) = - S.sum (fun P => (X : ℝ[X]) ^ (firstColumnRemainder i P).card) := by - simpa using - (Finset.sum_image (s := S) (g := firstColumnRemainder i) - (f := fun Q => (X : ℝ[X]) ^ Q.card) hinj) - calc - S.sum (fun P => (X : ℝ[X]) ^ P.card) - = S.sum (fun P => X * X ^ (firstColumnRemainder i P).card) := by - apply Finset.sum_congr rfl - intro P hP - have hPvalid : (ferrers lam).IsNonNestingPlacement P ∧ (i, 1) ∈ P := by - simpa [S] using mem_nonNestingPlacementsWithCell.mp hP - have hcard := firstColumnRemainder_card_add_one hPvalid.1 hPvalid.2 - rw [← hcard, pow_succ] - ring - _ = X * S.sum (fun P => X ^ (firstColumnRemainder i P).card) := by rw [Finset.mul_sum] - _ = X * T.sum (fun Q => X ^ Q.card) := by rw [← hsum_image, himage] - _ = X * ferrersRookPolynomial (partitionPrefix (partitionSubOne lam) i) := by - rw [ferrersRookPolynomial, rookPolynomial_eq_nonNestingPlacements_sum] + rw [ferrersRookPolynomial, rookPolynomial_eq_nonNestingPlacements_sum, + ← firstColumnRemainder_image_nonNestingPlacementsWithCell hfirst_cell, + Finset.sum_image firstColumnRemainder_injOn_nonNestingPlacementsWithCell, + Finset.mul_sum] + apply Finset.sum_congr rfl + intro P hP + rw [mem_nonNestingPlacementsWithCell] at hP + rw [← firstColumnRemainder_card_add_one hP.1 hP.2, pow_succ] + ring /-- In an integer partition, every row index in `firstColumnCells` is a genuine Ferrers-board first-column cell. -/ @@ -933,26 +809,10 @@ theorem ferrersRookPolynomial_firstColumnDeletion (lam : List ℕ) ferrersRookPolynomial (partitionSubOne lam) + X * ((List.range lam.length).map fun i => ferrersRookPolynomial (partitionPrefix (partitionSubOne lam) i)).sum := by - calc - ferrersRookPolynomial lam - = ((ferrers lam).nonNestingPlacements).sum - (fun P => (X : ℝ[X]) ^ P.card) := by - rw [ferrersRookPolynomial, rookPolynomial_eq_nonNestingPlacements_sum] - _ = (nonNestingPlacementsWithoutFirstColumn lam).sum - (fun P => (X : ℝ[X]) ^ P.card) + - (firstColumnCells lam).sum (fun a => - ((ferrers lam).nonNestingPlacementsWithCell a).sum - (fun P => (X : ℝ[X]) ^ P.card)) := - sum_nonNestingPlacements_eq_withoutFirstColumn_add_withFirstColumn lam - _ = ferrersRookPolynomial (partitionSubOne lam) + - (firstColumnCells lam).sum (fun a => - ((ferrers lam).nonNestingPlacementsWithCell a).sum - (fun P => (X : ℝ[X]) ^ P.card)) := by - rw [sum_nonNestingPlacementsWithoutFirstColumn_eq_partitionSubOne] - _ = ferrersRookPolynomial (partitionSubOne lam) + - X * ((List.range lam.length).map fun i => - ferrersRookPolynomial (partitionPrefix (partitionSubOne lam) i)).sum := by - rw [sum_firstColumnCells_nonNestingPlacementsWithCell_eq_mul_sum lam hpart] + rw [ferrersRookPolynomial, rookPolynomial_eq_nonNestingPlacements_sum, + sum_nonNestingPlacements_eq_withoutFirstColumn_add_withFirstColumn, + sum_nonNestingPlacementsWithoutFirstColumn_eq_partitionSubOne, + sum_firstColumnCells_nonNestingPlacementsWithCell_eq_mul_sum lam hpart] end FiniteSkewBoard diff --git a/RealRooted/MultivariateStability/MorrisDFlow.lean b/RealRooted/MultivariateStability/MorrisDFlow.lean index 89fd03493..a4537b78b 100644 --- a/RealRooted/MultivariateStability/MorrisDFlow.lean +++ b/RealRooted/MultivariateStability/MorrisDFlow.lean @@ -463,6 +463,18 @@ def morrisAFlowContinuous (q N : ℕ) (t : ℝ) : MorrisDegreeCoords q N →L[ℝ] MorrisDegreeCoords q N := LinearMap.toContinuousLinearMap (morrisAFlowCoords q N t) +private theorem continuous_conj_apply_of_apply_eq_smul (q N : ℕ) + (T : MorrisDegreeSpace q N →ₗ[ℝ] MorrisDegreeSpace q N) + (x : MorrisDegreeSpace q N) (c : ℝ) (hx : T x = c • x) : + LinearMap.toContinuousLinearMap (endOnMorrisDegreeCoords q N T) + (morrisDegreeEquiv q N x) = c • morrisDegreeEquiv q N x := by + change endOnMorrisDegreeCoords q N T (morrisDegreeEquiv q N x) = _ + rw [endOnMorrisDegreeCoords, LinearEquiv.conj_apply] + simp only [LinearMap.comp_apply] + change morrisDegreeEquiv q N + (T ((morrisDegreeEquiv q N).symm (morrisDegreeEquiv q N x))) = _ + rw [(morrisDegreeEquiv q N).symm_apply_apply, hx, map_smul] + private def morrisMsymmDegree (q N : ℕ) (i : MorrisDegreeIndex q N) : MorrisDegreeSpace q N := ⟨morrisMsymm q N i, morrisMsymm_mem q N i⟩ @@ -473,23 +485,10 @@ theorem morrisAContinuous_morrisMsymm (q N : ℕ) (morrisDegreeEquiv q N (morrisMsymmDegree q N i)) = (morrisAWeight i.2.1 : ℝ) • morrisDegreeEquiv q N (morrisMsymmDegree q N i) := by - simp only [morrisAContinuous] - change morrisACoords q N - (morrisDegreeEquiv q N (morrisMsymmDegree q N i)) = _ - rw [morrisACoords, endOnMorrisDegreeCoords, - LinearEquiv.conj_apply] - simp only [LinearMap.comp_apply] - change morrisDegreeEquiv q N (morrisAOnDegree q N - ((morrisDegreeEquiv q N).symm - (morrisDegreeEquiv q N (morrisMsymmDegree q N i)))) = _ - rw [(morrisDegreeEquiv q N).symm_apply_apply] - rw [show morrisAOnDegree q N (morrisMsymmDegree q N i) = - (morrisAWeight i.2.1 : ℝ) • morrisMsymmDegree q N i by - apply Subtype.ext - simpa [morrisMsymmDegree, morrisAOnDegree, morrisMsymm, - Nat.cast_smul_eq_nsmul] using - morrisA_msymm (R := ℝ) i.2.1] - exact map_smul (morrisDegreeEquiv q N) _ _ + apply continuous_conj_apply_of_apply_eq_smul + apply Subtype.ext + simpa [morrisMsymmDegree, morrisAOnDegree, morrisMsymm, + Nat.cast_smul_eq_nsmul] using morrisA_msymm (R := ℝ) i.2.1 theorem morrisAFlowContinuous_morrisMsymm (q N : ℕ) (t : ℝ) (i : MorrisDegreeIndex q N) : @@ -497,65 +496,82 @@ theorem morrisAFlowContinuous_morrisMsymm (q N : ℕ) (t : ℝ) (morrisDegreeEquiv q N (morrisMsymmDegree q N i)) = Real.exp (-t * morrisAWeight i.2.1) • morrisDegreeEquiv q N (morrisMsymmDegree q N i) := by - simp only [morrisAFlowContinuous] - change morrisAFlowCoords q N t - (morrisDegreeEquiv q N (morrisMsymmDegree q N i)) = _ - rw [morrisAFlowCoords, endOnMorrisDegreeCoords, - LinearEquiv.conj_apply] - simp only [LinearMap.comp_apply] - change morrisDegreeEquiv q N (morrisAFlowOnDegree q N t - ((morrisDegreeEquiv q N).symm - (morrisDegreeEquiv q N (morrisMsymmDegree q N i)))) = _ - rw [(morrisDegreeEquiv q N).symm_apply_apply] - rw [show morrisAFlowOnDegree q N t (morrisMsymmDegree q N i) = - Real.exp (-t * morrisAWeight i.2.1) • - morrisMsymmDegree q N i by - apply Subtype.ext - simpa [morrisAFlowOnDegree, morrisMsymmDegree, morrisMsymm] using - morrisAFlow_msymm t i.2.1] - exact map_smul (morrisDegreeEquiv q N) _ _ + apply continuous_conj_apply_of_apply_eq_smul + apply Subtype.ext + simpa [morrisAFlowOnDegree, morrisMsymmDegree, morrisMsymm] using + morrisAFlow_msymm t i.2.1 + +private theorem span_degreeSubtype_eq_top {q N : ℕ} {ι : Type*} + (b : ι → MvPolynomial (Fin q) ℝ) + (hb : ∀ i, b i ∈ morrisDegreeSubmodule q N) + (hspan : Submodule.span ℝ (Set.range b) = morrisDegreeSubmodule q N) : + Submodule.span ℝ (Set.range fun i => + (⟨b i, hb i⟩ : MorrisDegreeSpace q N)) = ⊤ := by + let b' : ι → MorrisDegreeSpace q N := fun i => ⟨b i, hb i⟩ + apply top_unique + rintro ⟨P, hPd⟩ - + have hPb : P ∈ Submodule.span ℝ (Set.range b) := by + rw [hspan] + exact hPd + revert hPd + induction hPb using Submodule.span_induction with + | mem P hP => + intro _ + obtain ⟨i, rfl⟩ := hP + exact Submodule.subset_span ⟨i, Subtype.ext rfl⟩ + | zero => + intro hzero + change (0 : MorrisDegreeSpace q N) ∈ Submodule.span ℝ (Set.range b') + exact Submodule.zero_mem _ + | add P Q hPb hQb hP hQ => + intro hPQ + have hPd : P ∈ morrisDegreeSubmodule q N := by rw [← hspan]; exact hPb + have hQd : Q ∈ morrisDegreeSubmodule q N := by rw [← hspan]; exact hQb + change (⟨P, hPd⟩ + ⟨Q, hQd⟩ : MorrisDegreeSpace q N) ∈ _ + exact Submodule.add_mem _ (hP hPd) (hQ hQd) + | smul r P hPb hP => + intro hrP + have hPd : P ∈ morrisDegreeSubmodule q N := by rw [← hspan]; exact hPb + change (r • ⟨P, hPd⟩ : MorrisDegreeSpace q N) ∈ _ + exact Submodule.smul_mem _ r (hP hPd) + +private theorem continuousLinearMap_ext_of_eq_on_span {q N : ℕ} {ι : Type*} + (b : ι → MvPolynomial (Fin q) ℝ) + (hb : ∀ i, b i ∈ morrisDegreeSubmodule q N) + (hspan : Submodule.span ℝ (Set.range b) = morrisDegreeSubmodule q N) + (F G : MorrisDegreeCoords q N →L[ℝ] MorrisDegreeCoords q N) + (hFG : ∀ i, F (morrisDegreeEquiv q N ⟨b i, hb i⟩) = + G (morrisDegreeEquiv q N ⟨b i, hb i⟩)) : F = G := by + let b' : ι → MorrisDegreeSpace q N := fun i => ⟨b i, hb i⟩ + have htop : Submodule.span ℝ (Set.range b') = ⊤ := by + simpa [b'] using span_degreeSubtype_eq_top b hb hspan + apply ContinuousLinearMap.ext + intro z + obtain ⟨x, rfl⟩ := (morrisDegreeEquiv q N).surjective z + have hx : x ∈ Submodule.span ℝ (Set.range b') := by rw [htop]; trivial + induction hx using Submodule.span_induction with + | mem x hx => + obtain ⟨i, rfl⟩ := hx + exact hFG i + | zero => simp + | add x y _ _ hx hy => simpa only [map_add] using congrArg₂ (· + ·) hx hy + | smul r x _ hx => simpa only [map_smul] using congrArg (r • ·) hx theorem exp_neg_morrisAContinuous_eq_flow (q N : ℕ) (t : ℝ) : NormedSpace.exp ((-t) • morrisAContinuous q N) = morrisAFlowContinuous q N t := by - apply ContinuousLinearMap.ext - intro x - obtain ⟨P, rfl⟩ := (morrisDegreeEquiv q N).surjective x - rcases P with ⟨P, hP⟩ - induction hP using Submodule.span_induction with - | mem P hP => - obtain ⟨i, rfl⟩ := hP - let x := morrisDegreeEquiv q N (morrisMsymmDegree q N i) - have hx : ((-t) • morrisAContinuous q N) x = - (-t * morrisAWeight i.2.1) • x := by - rw [smul_apply, morrisAContinuous_morrisMsymm] - simp only [x, smul_smul] - change NormedSpace.exp ((-t) • morrisAContinuous q N) x = - morrisAFlowContinuous q N t x - rw [exp_apply_of_eigenvector _ _ _ hx] - exact morrisAFlowContinuous_morrisMsymm q N t i |>.symm - | zero => - change NormedSpace.exp ((-t) • morrisAContinuous q N) - (morrisDegreeEquiv q N (0 : MorrisDegreeSpace q N)) = - morrisAFlowContinuous q N t - (morrisDegreeEquiv q N (0 : MorrisDegreeSpace q N)) - simp - | add P Q hPm hQm hP hQ => - change NormedSpace.exp ((-t) • morrisAContinuous q N) - (morrisDegreeEquiv q N - (⟨P, hPm⟩ + ⟨Q, hQm⟩ : MorrisDegreeSpace q N)) = - morrisAFlowContinuous q N t - (morrisDegreeEquiv q N - (⟨P, hPm⟩ + ⟨Q, hQm⟩ : MorrisDegreeSpace q N)) - simp only [map_add] - rw [hP, hQ] - | smul r P hPm hP => - change NormedSpace.exp ((-t) • morrisAContinuous q N) - (morrisDegreeEquiv q N (r • ⟨P, hPm⟩ : MorrisDegreeSpace q N)) = - morrisAFlowContinuous q N t - (morrisDegreeEquiv q N (r • ⟨P, hPm⟩ : MorrisDegreeSpace q N)) - simp only [map_smul] - rw [hP] + apply continuousLinearMap_ext_of_eq_on_span (morrisMsymm q N) + (morrisMsymm_mem q N) rfl + intro i + let x := morrisDegreeEquiv q N (morrisMsymmDegree q N i) + have hx : ((-t) • morrisAContinuous q N) x = + (-t * morrisAWeight i.2.1) • x := by + rw [smul_apply, morrisAContinuous_morrisMsymm] + simp only [x, smul_smul] + change NormedSpace.exp ((-t) • morrisAContinuous q N) x = + morrisAFlowContinuous q N t x + rw [exp_apply_of_eigenvector _ _ _ hx] + exact morrisAFlowContinuous_morrisMsymm q N t i |>.symm private theorem isSymmetric_prod_esymm_real (q : ℕ) (s : Multiset ℕ) : @@ -646,15 +662,11 @@ ring. -/ def morrisBFlowAmbient (q N : ℕ) (t : ℝ) : MorrisDegreeSpace q N →ₗ[ℝ] MvPolynomial (Fin q) ℝ where toFun P := morrisBFlow q t (morrisDegreeToSymmetric q N P) - map_add' P Q := by - exact congrArg Subtype.val - (map_add (morrisBFlow q t) - (morrisDegreeToSymmetric q N P) - (morrisDegreeToSymmetric q N Q)) - map_smul' r P := by - exact congrArg Subtype.val - (map_smul (morrisBFlow q t) - r (morrisDegreeToSymmetric q N P)) + map_add' P Q := congrArg Subtype.val + (map_add (morrisBFlow q t) (morrisDegreeToSymmetric q N P) + (morrisDegreeToSymmetric q N Q)) + map_smul' r P := congrArg Subtype.val + (map_smul (morrisBFlow q t) r (morrisDegreeToSymmetric q N P)) private theorem morrisBFlow_mem {q N : ℕ} (t : ℝ) {P : MvPolynomial (Fin q) ℝ} @@ -662,74 +674,47 @@ private theorem morrisBFlow_mem {q N : ℕ} (t : ℝ) (morrisBFlow q t ⟨P, isSymmetric_of_mem_morrisDegreeSubmodule hP0⟩ : MvPolynomial (Fin q) ℝ) ∈ morrisDegreeSubmodule q N := by - rw [morrisDegreeSubmodule_eq_elementary] at hP0 ⊢ - induction hP0 using Submodule.span_induction with - | mem E hE => - obtain ⟨i, rfl⟩ := hE - change (morrisBFlow q t - ⟨morrisElementaryPoly q N i, - isSymmetric_of_mem_morrisDegreeSubmodule - (morrisElementary_mem_morrisDegreeSubmodule i.2.1 i.2.2 - (Nat.lt_succ_iff.mp i.1.isLt))⟩ : - MvPolynomial (Fin q) ℝ) ∈ morrisElementarySubmodule q N - have heigen := morrisBFlow_morrisElementary q t i.2.1 i.2.2 - rw [show (morrisBFlow q t + let b : MorrisDegreeIndex q N → MorrisDegreeSpace q N := fun i => + ⟨morrisElementaryPoly q N i, + morrisElementary_mem_morrisDegreeSubmodule i.2.1 i.2.2 + (Nat.lt_succ_iff.mp i.1.isLt)⟩ + have htop : Submodule.span ℝ (Set.range b) = ⊤ := by + simpa [b] using span_degreeSubtype_eq_top (morrisElementaryPoly q N) + (fun i => morrisElementary_mem_morrisDegreeSubmodule i.2.1 i.2.2 + (Nat.lt_succ_iff.mp i.1.isLt)) + (morrisDegreeSubmodule_eq_elementary q N).symm + let x : MorrisDegreeSpace q N := ⟨P, hP0⟩ + have hx : x ∈ Submodule.span ℝ (Set.range b) := by rw [htop]; trivial + change morrisBFlowAmbient q N t x ∈ morrisDegreeSubmodule q N + have hclosed : ∀ y ∈ Submodule.span ℝ (Set.range b), + morrisBFlowAmbient q N t y ∈ morrisDegreeSubmodule q N := by + intro y hy + induction hy using Submodule.span_induction with + | mem E hE => + obtain ⟨i, rfl⟩ := hE + change (morrisBFlow q t ⟨morrisElementaryPoly q N i, isSymmetric_of_mem_morrisDegreeSubmodule (morrisElementary_mem_morrisDegreeSubmodule i.2.1 i.2.2 (Nat.lt_succ_iff.mp i.1.isLt))⟩ : - MvPolynomial (Fin q) ℝ) = - Real.exp (t * morrisBWeight q i.2.1.conjugate) • - morrisElementaryPoly q N i by - exact congrArg Subtype.val heigen] - exact Submodule.smul_mem _ _ - (Submodule.subset_span (Set.mem_range_self i)) - | zero => - have hzero : (0 : MvPolynomial (Fin q) ℝ) ∈ - morrisDegreeSubmodule q N := Submodule.zero_mem _ - change (morrisBFlow q t - ⟨0, isSymmetric_of_mem_morrisDegreeSubmodule hzero⟩ : - MvPolynomial (Fin q) ℝ) ∈ morrisElementarySubmodule q N - have hz : (⟨0, isSymmetric_of_mem_morrisDegreeSubmodule hzero⟩ : - symmetricSubalgebra (Fin q) ℝ) = 0 := Subtype.ext rfl - rw [hz, map_zero] - exact Submodule.zero_mem _ - | add P Q hPe hQe hP hQ => - have hPm : P ∈ morrisDegreeSubmodule q N := by - rw [morrisDegreeSubmodule_eq_elementary] - exact hPe - have hQm : Q ∈ morrisDegreeSubmodule q N := by - rw [morrisDegreeSubmodule_eq_elementary] - exact hQe - have hPQ : P + Q ∈ morrisDegreeSubmodule q N := - Submodule.add_mem _ hPm hQm - change (morrisBFlow q t - ⟨P + Q, isSymmetric_of_mem_morrisDegreeSubmodule hPQ⟩ : - MvPolynomial (Fin q) ℝ) ∈ morrisElementarySubmodule q N - have hadd : - (⟨P + Q, isSymmetric_of_mem_morrisDegreeSubmodule hPQ⟩ : - symmetricSubalgebra (Fin q) ℝ) = - ⟨P, isSymmetric_of_mem_morrisDegreeSubmodule hPm⟩ + - ⟨Q, isSymmetric_of_mem_morrisDegreeSubmodule hQm⟩ := - Subtype.ext rfl - rw [hadd, map_add] - exact Submodule.add_mem _ (hP hPm) (hQ hQm) - | smul r P hPe hP => - have hPm : P ∈ morrisDegreeSubmodule q N := by - rw [morrisDegreeSubmodule_eq_elementary] - exact hPe - have hrP : r • P ∈ morrisDegreeSubmodule q N := - Submodule.smul_mem _ r hPm - change (morrisBFlow q t - ⟨r • P, isSymmetric_of_mem_morrisDegreeSubmodule hrP⟩ : - MvPolynomial (Fin q) ℝ) ∈ morrisElementarySubmodule q N - have hsmul : - (⟨r • P, isSymmetric_of_mem_morrisDegreeSubmodule hrP⟩ : - symmetricSubalgebra (Fin q) ℝ) = - r • ⟨P, isSymmetric_of_mem_morrisDegreeSubmodule hPm⟩ := - Subtype.ext rfl - rw [hsmul, map_smul] - exact Submodule.smul_mem _ r (hP hPm) + MvPolynomial (Fin q) ℝ) ∈ morrisDegreeSubmodule q N + have heigen := morrisBFlow_morrisElementary q t i.2.1 i.2.2 + rw [show (morrisBFlow q t + ⟨morrisElementaryPoly q N i, + isSymmetric_of_mem_morrisDegreeSubmodule + (morrisElementary_mem_morrisDegreeSubmodule i.2.1 i.2.2 + (Nat.lt_succ_iff.mp i.1.isLt))⟩ : + MvPolynomial (Fin q) ℝ) = + Real.exp (t * morrisBWeight q i.2.1.conjugate) • + morrisElementaryPoly q N i by + exact congrArg Subtype.val heigen] + exact Submodule.smul_mem _ _ + (morrisElementary_mem_morrisDegreeSubmodule i.2.1 i.2.2 + (Nat.lt_succ_iff.mp i.1.isLt)) + | zero => simpa only [map_zero] using Submodule.zero_mem (morrisDegreeSubmodule q N) + | add P Q _ _ hP hQ => simpa only [map_add] using Submodule.add_mem _ hP hQ + | smul r P _ hP => simpa only [map_smul] using Submodule.smul_mem _ r hP + exact hclosed x hx theorem morrisBFlowAmbient_mem {q N : ℕ} (t : ℝ) (P : MorrisDegreeSpace q N) : @@ -765,24 +750,11 @@ theorem morrisBContinuous_morrisElementary (q N : ℕ) (morrisDegreeEquiv q N (morrisElementaryDegree q N i)) = (morrisBWeight q i.2.1.conjugate : ℝ) • morrisDegreeEquiv q N (morrisElementaryDegree q N i) := by - simp only [morrisBContinuous] - change morrisBCoords q N - (morrisDegreeEquiv q N (morrisElementaryDegree q N i)) = _ - rw [morrisBCoords, endOnMorrisDegreeCoords, - LinearEquiv.conj_apply] - simp only [LinearMap.comp_apply] - change morrisDegreeEquiv q N (morrisBOnDegree q N - ((morrisDegreeEquiv q N).symm - (morrisDegreeEquiv q N (morrisElementaryDegree q N i)))) = _ - rw [(morrisDegreeEquiv q N).symm_apply_apply] - rw [show morrisBOnDegree q N (morrisElementaryDegree q N i) = - (morrisBWeight q i.2.1.conjugate : ℝ) • - morrisElementaryDegree q N i by - apply Subtype.ext - simpa [morrisElementaryDegree, morrisElementaryPoly, - morrisBOnDegree, Nat.cast_smul_eq_nsmul] using - morrisB_morrisElementary (R := ℝ) q i.2.1 i.2.2] - exact map_smul (morrisDegreeEquiv q N) _ _ + apply continuous_conj_apply_of_apply_eq_smul + apply Subtype.ext + simpa [morrisElementaryDegree, morrisElementaryPoly, morrisBOnDegree, + Nat.cast_smul_eq_nsmul] using + morrisB_morrisElementary (R := ℝ) q i.2.1 i.2.2 theorem morrisBFlowContinuous_morrisElementary (q N : ℕ) (t : ℝ) (i : MorrisDegreeIndex q N) : @@ -790,90 +762,29 @@ theorem morrisBFlowContinuous_morrisElementary (q N : ℕ) (morrisDegreeEquiv q N (morrisElementaryDegree q N i)) = Real.exp (t * morrisBWeight q i.2.1.conjugate) • morrisDegreeEquiv q N (morrisElementaryDegree q N i) := by - simp only [morrisBFlowContinuous] - change morrisBFlowCoords q N t - (morrisDegreeEquiv q N (morrisElementaryDegree q N i)) = _ - rw [morrisBFlowCoords, endOnMorrisDegreeCoords, - LinearEquiv.conj_apply] - simp only [LinearMap.comp_apply] - change morrisDegreeEquiv q N (morrisBFlowOnDegree q N t - ((morrisDegreeEquiv q N).symm - (morrisDegreeEquiv q N (morrisElementaryDegree q N i)))) = _ - rw [(morrisDegreeEquiv q N).symm_apply_apply] - rw [show morrisBFlowOnDegree q N t (morrisElementaryDegree q N i) = - Real.exp (t * morrisBWeight q i.2.1.conjugate) • - morrisElementaryDegree q N i by - apply Subtype.ext - exact congrArg - (fun P : symmetricSubalgebra (Fin q) ℝ => - (P : MvPolynomial (Fin q) ℝ)) - (morrisBFlow_morrisElementary q t i.2.1 i.2.2)] - exact map_smul (morrisDegreeEquiv q N) _ _ + apply continuous_conj_apply_of_apply_eq_smul + apply Subtype.ext + exact congrArg (fun P : symmetricSubalgebra (Fin q) ℝ => + (P : MvPolynomial (Fin q) ℝ)) + (morrisBFlow_morrisElementary q t i.2.1 i.2.2) theorem exp_morrisBContinuous_eq_flow (q N : ℕ) (t : ℝ) : NormedSpace.exp (t • morrisBContinuous q N) = morrisBFlowContinuous q N t := by - apply ContinuousLinearMap.ext - intro x - obtain ⟨P, rfl⟩ := (morrisDegreeEquiv q N).surjective x - rcases P with ⟨P, hP⟩ - have hPe : P ∈ morrisElementarySubmodule q N := by - rw [← morrisDegreeSubmodule_eq_elementary] - exact hP - revert hP - induction hPe using Submodule.span_induction with - | mem P hE => - intro hPm - obtain ⟨i, rfl⟩ := hE - let x := morrisDegreeEquiv q N (morrisElementaryDegree q N i) - have hx : (t • morrisBContinuous q N) x = - (t * morrisBWeight q i.2.1.conjugate) • x := by - rw [smul_apply, morrisBContinuous_morrisElementary] - simp only [x, smul_smul] - change NormedSpace.exp (t • morrisBContinuous q N) x = - morrisBFlowContinuous q N t x - rw [exp_apply_of_eigenvector _ _ _ hx] - exact morrisBFlowContinuous_morrisElementary q N t i |>.symm - | zero => - intro hzero - change NormedSpace.exp (t • morrisBContinuous q N) - (morrisDegreeEquiv q N (0 : MorrisDegreeSpace q N)) = - morrisBFlowContinuous q N t - (morrisDegreeEquiv q N (0 : MorrisDegreeSpace q N)) - simp - | add P Q hPm hQm hP hQ => - intro hPQ - have hPm' : P ∈ morrisDegreeSubmodule q N := by - rw [morrisDegreeSubmodule_eq_elementary] - exact hPm - have hQm' : Q ∈ morrisDegreeSubmodule q N := by - rw [morrisDegreeSubmodule_eq_elementary] - exact hQm - change NormedSpace.exp (t • morrisBContinuous q N) - (morrisDegreeEquiv q N - (⟨P, hPm'⟩ + ⟨Q, hQm'⟩ : - MorrisDegreeSpace q N)) = - morrisBFlowContinuous q N t - (morrisDegreeEquiv q N - (⟨P, hPm'⟩ + ⟨Q, hQm'⟩ : - MorrisDegreeSpace q N)) - simp only [map_add] - rw [hP hPm', hQ hQm'] - | smul r P hPm hP => - intro hrP - have hPm' : P ∈ morrisDegreeSubmodule q N := by - rw [morrisDegreeSubmodule_eq_elementary] - exact hPm - change NormedSpace.exp (t • morrisBContinuous q N) - (morrisDegreeEquiv q N - (r • ⟨P, hPm'⟩ : - MorrisDegreeSpace q N)) = - morrisBFlowContinuous q N t - (morrisDegreeEquiv q N - (r • ⟨P, hPm'⟩ : - MorrisDegreeSpace q N)) - simp only [map_smul] - rw [hP hPm'] + apply continuousLinearMap_ext_of_eq_on_span (morrisElementaryPoly q N) + (fun i => morrisElementary_mem_morrisDegreeSubmodule i.2.1 i.2.2 + (Nat.lt_succ_iff.mp i.1.isLt)) + (morrisDegreeSubmodule_eq_elementary q N).symm + intro i + let x := morrisDegreeEquiv q N (morrisElementaryDegree q N i) + have hx : (t • morrisBContinuous q N) x = + (t * morrisBWeight q i.2.1.conjugate) • x := by + rw [smul_apply, morrisBContinuous_morrisElementary] + simp only [x, smul_smul] + change NormedSpace.exp (t • morrisBContinuous q N) x = + morrisBFlowContinuous q N t x + rw [exp_apply_of_eigenvector _ _ _ hx] + exact morrisBFlowContinuous_morrisElementary q N t i |>.symm /-- The polynomial with coordinate vector `x` in `MorrisDegreeSpace q N`. -/ def morrisDegreePolynomial (q N : ℕ) (x : MorrisDegreeCoords q N) : From 13e4c864900f89154b5ed2c5533d7016dd5d6e9b Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Wed, 21 Oct 2026 11:19:44 +0000 Subject: [PATCH 3/4] Golf SymbolBridge, Continuation, Converse Statements unchanged; 132 lines shorter. Proofs drafted by a Codex worker, checked with the lakefile options and built locally. Co-Authored-By: Claude Opus 5.5 --- .../Transcendental/SymbolBridge.lean | 114 ++++++------------ RealRooted/EdreiThoma/Continuation.lean | 113 +++++------------ RealRooted/EdreiThoma/Converse.lean | 107 +++++----------- 3 files changed, 101 insertions(+), 233 deletions(-) diff --git a/RealRooted/BorceaBranden/Transcendental/SymbolBridge.lean b/RealRooted/BorceaBranden/Transcendental/SymbolBridge.lean index d25185ddc..59e87a509 100644 --- a/RealRooted/BorceaBranden/Transcendental/SymbolBridge.lean +++ b/RealRooted/BorceaBranden/Transcendental/SymbolBridge.lean @@ -26,11 +26,12 @@ theorem MvUpperHalfPlaneStable.invertVariableAt MvUpperHalfPlaneStable (invertVariableAt d i p) := by unfold RealRooted.BorceaBranden.invertVariableAt apply MvUpperHalfPlaneStable.rename - apply MvUpperHalfPlaneStable.invertVariable - · have hrename := MvPolynomial.degreeOf_rename_of_injective - (Equiv.optionSubtypeNe i).symm.injective i (p := p) - simpa using hrename.trans_le hdegree - · exact hp.rename + exact MvUpperHalfPlaneStable.invertVariable + (by + have hrename := MvPolynomial.degreeOf_rename_of_injective + (Equiv.optionSubtypeNe i).symm.injective i (p := p) + simpa using hrename.trans_le hdegree) + hp.rename private theorem coeff_invertVariable_of_degree {υ : Type*} {p : MvPolynomial (Option υ) ℂ} (d : ℕ) @@ -77,11 +78,8 @@ private theorem degreeOf_invertVariable_none_le (invertVariable d p).degreeOf none ≤ d := by rw [MvPolynomial.degreeOf_le_iff] intro e he - rw [MvPolynomial.mem_support_iff] at he - rw [coeff_invertVariable_of_degree d hdegree e] at he - by_contra hle - rw [ite_eq_right hle] at he - exact he rfl + rw [MvPolynomial.mem_support_iff, coeff_invertVariable_of_degree d hdegree e] at he + split_ifs at he <;> simp_all private theorem degreeOf_invertVariable_some_le {υ : Type*} {p : MvPolynomial (Option υ) ℂ} (d : ℕ) @@ -89,8 +87,7 @@ private theorem degreeOf_invertVariable_some_le (invertVariable d p).degreeOf (some j) ≤ p.degreeOf (some j) := by rw [MvPolynomial.degreeOf_le_iff] intro e he - rw [MvPolynomial.mem_support_iff] at he - rw [coeff_invertVariable_of_degree d hdegree e] at he + rw [MvPolynomial.mem_support_iff, coeff_invertVariable_of_degree d hdegree e] at he by_cases hle : e none ≤ d · rw [ite_eq_left hle] at he have hin : p.coeff (e.some.optionElim (d - e none)) ≠ 0 := @@ -98,8 +95,7 @@ private theorem degreeOf_invertVariable_some_le have hbound := MvPolynomial.monomial_le_degreeOf (some j) (MvPolynomial.mem_support_iff.mpr hin) simpa using hbound - · rw [ite_eq_right hle] at he - exact (he rfl).elim + · simp [hle] at he private theorem degreeOf_invertVariableAt_self_le {υ : Type*} [DecidableEq υ] {p : MvPolynomial υ ℂ} @@ -111,10 +107,9 @@ private theorem degreeOf_invertVariableAt_self_le ((Equiv.optionSubtypeNe i) none) ≤ d rw [MvPolynomial.degreeOf_rename_of_injective (Equiv.optionSubtypeNe i).injective] - apply degreeOf_invertVariable_none_le d have hrename := MvPolynomial.degreeOf_rename_of_injective (Equiv.optionSubtypeNe i).symm.injective i (p := p) - simpa using hrename.trans_le hdegree + exact degreeOf_invertVariable_none_le d (by simpa using hrename.trans_le hdegree) private theorem degreeOf_invertVariableAt_of_ne_le {υ : Type*} [DecidableEq υ] {p : MvPolynomial υ ℂ} @@ -259,8 +254,7 @@ private theorem coeff_invertVariables_of_nodup complementOnList d (i :: s) m := by ext j by_cases hji : j = i - · subst j - simp [complementOnList, hs.1] + · subst j; simp [complementOnList, hs.1] · simp [complementOnList, hji] rw [hcomp] simp only [inversionExponent, List.map_cons, List.sum_cons] @@ -343,6 +337,18 @@ private theorem complementOnList_rightVariableList simp [complementOnList, inr_mem_rightVariableList (τ := τ) i, rightInversionBounds] +omit [Finite τ] [Fintype σ] in +private theorem coeff_eq_zero_of_right_degree + {β : σ →₀ ℕ} {p : MvPolynomial (τ ⊕ σ) ℂ} + (hdegree : ∀ i, p.degreeOf (Sum.inr i) ≤ β i) {e : τ ⊕ σ →₀ ℕ} + (hle : ¬(Finsupp.sumFinsuppEquivProdFinsupp e).2 ≤ β) : p.coeff e = 0 := by + rw [Finsupp.le_def] at hle + push Not at hle + obtain ⟨i, hi⟩ := hle + apply MvPolynomial.notMem_support_iff.mp + exact fun hes => (Nat.not_le_of_gt hi) + ((MvPolynomial.monomial_le_degreeOf (Sum.inr i) hes).trans (hdegree i)) + /-- Complement/sign coefficient formula for the finite right-block composition of `invertVariable`. -/ theorem coeff_invertRightVariables (β : σ →₀ ℕ) @@ -375,15 +381,8 @@ theorem coeff_invertRightVariables (β : σ →₀ ℕ) obtain ⟨i, rfl⟩ := mem_rightVariableList_eq_inr x hx exact hle i · rw [ite_eq_right hle] - rw [Finsupp.le_def] at hle - push Not at hle - obtain ⟨i, hi⟩ := hle - apply MvPolynomial.notMem_support_iff.mp - intro hes - have hmon := MvPolynomial.monomial_le_degreeOf (Sum.inr i) hes - have hout := degreeOf_invertVariables_le d s p hd (Sum.inr i) - change (invertRightVariables β p).degreeOf (Sum.inr i) ≤ β i at hout - exact (Nat.not_le_of_gt hi) (hmon.trans hout) + apply coeff_eq_zero_of_right_degree (hle := hle) + exact fun i => degreeOf_invertVariables_le d s p hd (Sum.inr i) /-- The signed reciprocal in a finite right-coordinate degree box. -/ def signedRightBoxReciprocal (β : σ →₀ ℕ) @@ -416,10 +415,7 @@ theorem coeff_signedRightBoxReciprocal (β : σ →₀ ℕ) rw [signedRightBoxReciprocal, coeff_glue] unfold seriesCoeff rw [MvPolynomial.coeff_coeffPoly] - split_ifs with h - · push_cast - rfl - · simp + split_ifs <;> push_cast <;> simp_all /-- The direct complement/sign formula agrees with the finite right-coordinate composition of `invertVariable`. -/ @@ -428,8 +424,7 @@ theorem invertRightVariables_eq_signedRightBoxReciprocal (hdegree : ∀ i, p.degreeOf (Sum.inr i) ≤ β i) : invertRightVariables β p = signedRightBoxReciprocal β p := by ext e - rw [coeff_invertRightVariables β p hdegree e, - coeff_signedRightBoxReciprocal] + rw [coeff_invertRightVariables β p hdegree e, coeff_signedRightBoxReciprocal] /-- The arbitrary-degree signed right-box reciprocal preserves stability. -/ theorem MvUpperHalfPlaneStable.signedRightBoxReciprocal @@ -456,10 +451,7 @@ theorem coeff_paperRightBoxReciprocal (β : σ →₀ ℕ) rw [paperRightBoxReciprocal, coeff_glue] unfold seriesCoeff rw [MvPolynomial.coeff_coeffPoly] - split_ifs with h - · push_cast - rfl - · simp + split_ifs <;> push_cast <;> simp_all private theorem neg_one_pow_box_sub (β α : σ →₀ ℕ) (hαβ : α ≤ β) : (-1 : ℂ) ^ (∑ i, β i) * (-1 : ℂ) ^ (∑ i, (β i - α i)) = @@ -498,9 +490,7 @@ theorem MvUpperHalfPlaneStable.paperRightBoxReciprocal (hp : MvUpperHalfPlaneStable p) : MvUpperHalfPlaneStable (paperRightBoxReciprocal β p) := by rw [paperRightBoxReciprocal_eq_globalSign_mul] - apply MvUpperHalfPlaneStable.C_mul - · exact MvUpperHalfPlaneStable.signedRightBoxReciprocal β hdegree hp - · simp + exact (MvUpperHalfPlaneStable.signedRightBoxReciprocal β hdegree hp).C_mul (by simp) /-- The signed right-box reciprocal has right-coordinate degree at most the box. -/ theorem degreeOf_signedRightBoxReciprocal_inr_le @@ -542,9 +532,8 @@ theorem signedRightBoxReciprocal_involutive let E : (τ ⊕ σ →₀ ℕ) ≃ (τ →₀ ℕ) × (σ →₀ ℕ) := Finsupp.sumFinsuppEquivProdFinsupp by_cases hle : (E e).2 ≤ β - · have hle' : (Finsupp.sumFinsuppEquivProdFinsupp e).2 ≤ β := by - simpa only [E] using hle - rw [ite_eq_left hle'] + · change (Finsupp.sumFinsuppEquivProdFinsupp e).2 ≤ β at hle + rw [ite_eq_left hle] rw [coeff_signedRightBoxReciprocal] have hsub : β - (E e).2 ≤ β := fun i => Nat.sub_le _ _ have hpair : @@ -552,39 +541,24 @@ theorem signedRightBoxReciprocal_involutive ((E e).1.sumElim (β - (E e).2)) = ((E e).1, β - (E e).2) := by change E (E.symm ((E e).1, β - (E e).2)) = _ - exact E.apply_symm_apply _ + rw [E.apply_symm_apply] rw [hpair] rw [ite_eq_left hsub] have hsubsub : β - (β - (E e).2) = (E e).2 := by - ext i - exact Nat.sub_sub_self (hle i) + ext i; exact Nat.sub_sub_self (hle i) have he : (E e).1.sumElim (E e).2 = e := by change E.symm (E e) = e - exact E.symm_apply_apply e + rw [E.symm_apply_apply] rw [hsubsub, he, ← mul_assoc] - have houter : - (∑ i, (β i - (Finsupp.sumFinsuppEquivProdFinsupp e).2 i)) = - ∑ i, (β i - (E e).2 i) := by - rfl have hinner : (∑ i, (β i - (β - (E e).2) i)) = ∑ i, (E e).2 i := by apply Finset.sum_congr rfl intro i _hi exact Nat.sub_sub_self (hle i) - rw [houter, hinner] + rw [hinner] rw [neg_one_pow_box_sub_mul β (E e).2 hle] - · have hle' : ¬(Finsupp.sumFinsuppEquivProdFinsupp e).2 ≤ β := by - simpa only [E] using hle - rw [ite_eq_right hle'] - have hpzero : p.coeff e = 0 := by - rw [Finsupp.le_def] at hle' - push Not at hle' - obtain ⟨i, hi⟩ := hle' - apply MvPolynomial.notMem_support_iff.mp - intro hes - have hmon := MvPolynomial.monomial_le_degreeOf (Sum.inr i) hes - exact (Nat.not_le_of_gt hi) (hmon.trans (hdegree i)) - rw [hpzero, mul_zero] + · change ¬(Finsupp.sumFinsuppEquivProdFinsupp e).2 ≤ β at hle + rw [ite_eq_right hle, coeff_eq_zero_of_right_degree hdegree hle, mul_zero] /-- Stability is equivalent before and after the signed right-box reciprocal. -/ theorem signedRightBoxReciprocal_stable_iff @@ -601,7 +575,7 @@ theorem signedRightBoxReciprocal_stable_iff have hne := htwice z hz simp only [MvPolynomial.eval_mul, MvPolynomial.eval_C] at hne exact (mul_ne_zero_iff.mp hne).2 - · exact fun hp => MvUpperHalfPlaneStable.signedRightBoxReciprocal β hdegree hp + · exact MvUpperHalfPlaneStable.signedRightBoxReciprocal β hdegree /-- Stability is equivalent before and after the normalized right-box reciprocal. -/ theorem paperRightBoxReciprocal_stable_iff @@ -618,8 +592,7 @@ theorem paperRightBoxReciprocal_stable_iff simp only [MvPolynomial.eval_mul, MvPolynomial.eval_C] at hne exact (mul_ne_zero_iff.mp hne).2 · intro hp - exact MvUpperHalfPlaneStable.C_mul - ((signedRightBoxReciprocal_stable_iff β p hdegree).mpr hp) (by simp) + exact ((signedRightBoxReciprocal_stable_iff β p hdegree).mpr hp).C_mul (by simp) private theorem fall_mul_signedInvFactorial_eq_boxChoose (α β : σ →₀ ℕ) : @@ -644,13 +617,6 @@ private theorem fall_mul_signedInvFactorial_eq_boxChoose exact_mod_cast Nat.factorial_ne_zero (α i) field_simp -omit [Finite τ] [Fintype σ] in -private theorem coeffPoly_eq_sourceCoefficientGeneral - (p : MvPolynomial (τ ⊕ σ) ℂ) (α : σ →₀ ℕ) : - MvPolynomial.coeffPoly α p = sourceCoefficientGeneral p α := by - ext γ - rw [MvPolynomial.coeff_coeffPoly, coeff_sourceCoefficientGeneral] - omit [Finite τ] in private theorem coeff_algebraicSymbol_at_complement (β : σ →₀ ℕ) (T : MvPolynomial σ ℂ →ₗ[ℂ] MvPolynomial τ ℂ) diff --git a/RealRooted/EdreiThoma/Continuation.lean b/RealRooted/EdreiThoma/Continuation.lean index dcd07fa39..5ed9adf18 100644 --- a/RealRooted/EdreiThoma/Continuation.lean +++ b/RealRooted/EdreiThoma/Continuation.lean @@ -17,18 +17,14 @@ namespace RealRooted.EdreiThoma private lemma summable_norm_genFun {a : ℕ → ℝ} (h : IsPolyaFreqSeq a) (h0 : a 0 = 1) {z : ℂ} (hz : a 1 * ‖z‖ < 1) : Summable fun n => ‖(a n : ℂ) * z ^ n‖ := by - have hz' : a 1 * ‖((‖z‖ : ℝ) : ℂ)‖ < 1 := by simpa using hz - have := (IsPolyaFreqSeq.summable_genFun h h0 hz').norm + have := (IsPolyaFreqSeq.summable_genFun h h0 (by simpa using hz)).norm refine this.congr fun n => ?_ simp [norm_pow, abs_of_nonneg (IsPolyaFreqSeq.nonneg h n)] private lemma eventually_disc (c : ℝ) : ∀ᶠ z in 𝓝 (0 : ℂ), c * ‖z‖ < 1 := by - have : Continuous fun z : ℂ => c * ‖z‖ := continuous_const.mul continuous_norm - exact this.continuousAt.eventually_lt continuousAt_const (by simp) + exact (continuous_const.mul continuous_norm).continuousAt.eventually_lt continuousAt_const + (by simp) -private lemma summable_norm_ofReal {α : ℕ → ℝ} (sα : Summable α) : - Summable fun i => ‖(α i : ℂ)‖ := by - simpa [Complex.norm_real] using (summable_abs_iff.2 sα) namespace E7 /-- Coefficient `k` of the formal product `(∑ a_n z^n) * P(z)`. -/ @@ -52,23 +48,18 @@ private lemma cp_sum (a : ℕ → ℝ) {ι : Type*} (s : Finset ι) (P : ι → classical induction s using Finset.induction_on with | empty => simp [cp] - | insert i s hi ih => rw [Finset.sum_insert hi, Finset.sum_insert hi, cp_add, ih] + | insert i s hi ih => simp only [Finset.sum_insert hi, cp_add, ih] private lemma cp_X_mul_succ (a : ℕ → ℝ) (P : ℝ[X]) (k : ℕ) : cp a (X * P) (k + 1) = cp a P k := by - simp only [cp] - rw [Finset.sum_range_succ'] - simp [coeff_X_mul] + simp [cp, Finset.sum_range_succ', coeff_X_mul] private lemma cp_X_mul_zero (a : ℕ → ℝ) (P : ℝ[X]) : cp a (X * P) 0 = 0 := by simp [cp] private lemma cp_one (a : ℕ → ℝ) (k : ℕ) : cp a 1 k = a k := by simp only [cp, coeff_one] - rw [Finset.sum_eq_single 0] - · simp - · intro b _ hb; simp [hb] - · simp + rw [Finset.sum_eq_single 0] <;> simp_all private lemma cp_C_mul_X_pow (a : ℕ → ℝ) (c : ℝ) (j k : ℕ) : cp a (C c * X ^ j) k = c * tc a ((k : ℤ) - j) := by @@ -139,10 +130,8 @@ private lemma pc_eq_det (a : ℕ → ℝ) (m n k : ℕ) : private lemma toeplitz_eq_tc (a : ℕ → ℝ) (i j : ℕ) : (toeplitz a) i j = tc a ((i : ℤ) - j) := by rw [toeplitz_apply] - unfold tc - by_cases h : j ≤ i - · rw [ite_eq_left h, ite_eq_left (by lia)]; congr 1; lia - · rw [ite_eq_right h, ite_eq_right (by lia)] + simp only [tc] + split_ifs <;> congr 1 <;> lia private lemma det_Mk_nonneg {a : ℕ → ℝ} (hpf : IsPolyaFreqSeq a) {m n k : ℕ} (hk : k ≤ m) : @@ -167,12 +156,8 @@ private lemma pc_nonneg {a : ℕ → ℝ} (hpf : IsPolyaFreqSeq a) exact mul_nonneg (div_nonneg zero_le_one (hP n m).le) (det_Mk_nonneg hpf hk) private lemma pc_succ_eq_zero (a : ℕ → ℝ) (m n : ℕ) : pc a m (n + 1) (m + 1) = 0 := by - rw [pc_eq_det] - have : Matrix.det (Mk a m (n + 1) (m + 1)) = 0 := by - refine Matrix.det_zero_of_row_eq (i := 0) (j := 1) (by simp) ?_ - funext j - simp [Mk] - rw [this, mul_zero] + rw [pc_eq_det, Matrix.det_zero_of_row_eq (i := 0) (j := 1) (by simp) + (by funext j; simp [Mk]), mul_zero] private lemma Q_eq_S_comp (a : ℕ → ℝ) (m n : ℕ) : Q a m n = (S a m n).comp (-X) := by rw [S, comp_neg_X_comp_neg_X] @@ -202,9 +187,8 @@ private lemma pc_succ_sub (a : ℕ → ℝ) (hA : ∀ n m, A a n m ≠ 0) (m n k private lemma pc_succ_sub_zero (a : ℕ → ℝ) (hA : ∀ n m, A a n m ≠ 0) (m n : ℕ) : pc a (m + 1) (n + 1) 0 = pc a m (n + 1) 0 := by - have : pc a (m + 1) (n + 1) 0 - pc a m (n + 1) 0 = 0 := by - rw [pc, pc, ← cp_sub, Q_succ_sub a hA, mul_assoc, cp_C_mul, cp_X_mul_zero, mul_zero] - linarith + rw [← sub_eq_zero, pc, pc, ← cp_sub, Q_succ_sub a hA, mul_assoc, cp_C_mul, + cp_X_mul_zero, mul_zero] private lemma A_zero (a : ℕ → ℝ) (m : ℕ) : A a 0 m = 1 := by simp [A] @@ -229,30 +213,18 @@ private lemma w_zero (a : ℕ → ℝ) (m : ℕ) : w a 0 m = a m := by private lemma rr_eq {a : ℕ → ℝ} (hP : ∀ n m, 0 < A a n m) (m n : ℕ) : rr a m n = w a n (m + 1) / w a n m := by - have h1 := (hP (n + 1) m).ne' - have h2 := (hP n m).ne' - have h3 := (hP (n + 1) (m + 1)).ne' - have h4 := (hP n (m + 1)).ne' simp only [rr, w] - field_simp + field_simp [ne_of_gt (hP _ _)] private lemma gam_eq {a : ℕ → ℝ} (hP : ∀ n m, 0 < A a n m) (m n : ℕ) : gam a m n = w a (n + 1) (m + 1) / w a n m := by - have h1 := (hP (n + 1) m).ne' - have h2 := (hP n m).ne' - have h3 := (hP (n + 1) (m + 1)).ne' - have h4 := (hP (n + 2) (m + 1)).ne' simp only [gam, w] - field_simp + field_simp [ne_of_gt (hP _ _)] private lemma gam_pos {a : ℕ → ℝ} (hP : ∀ n m, 0 < A a n m) (m n : ℕ) : 0 < gam a m n := by rw [gam_eq hP]; exact div_pos (w_pos hP _ _) (w_pos hP _ _) -end E7 - -namespace E7 - /-- `u k ≤ C (L + δ)^k` for every `δ > 0`. -/ private def GrowthBound (u : ℕ → ℝ) (L : ℝ) : Prop := ∀ δ > 0, ∃ C, ∀ k, u k ≤ C * (L + δ) ^ k @@ -401,10 +373,6 @@ private lemma growth_step {u v γ W0 W1 : ℕ → ℝ} {b b' : ℝ} _ ≤ max (u 0) (E / (b' + δ)) * (b' + δ) ^ (k + 1) := mul_le_mul_of_nonneg_right (le_max_right _ _) (by positivity) -end E7 - -namespace E7 - section Limits variable {a : ℕ → ℝ} (hpf : IsPolyaFreqSeq a) (hP : ∀ n m, 0 < A a n m) @@ -454,8 +422,7 @@ private lemma pn_succ_le (n k : ℕ) : | zero => rw [pn_succ_zero hSrec] | succ k => rw [pn_succ_succ hSrec] - have := mul_nonneg (hβ n) (pn_nonneg hpf hP hSlim n k) - linarith + linarith [mul_nonneg (hβ n) (pn_nonneg hpf hP hSlim n k)] include hpf hP hS0 hSlim in private lemma pc_le_pn {μ n k : ℕ} (hk : k ≤ μ) : @@ -489,8 +456,7 @@ private lemma pc_telescope (n k : ℕ) : ∀ M, k ≤ M → | base => simp [pc_succ_eq_zero] | succ M hkM ih => rw [Finset.sum_Ico_succ_top hkM, ← ih] - have := pc_succ_sub a hA M n k - linarith + linarith [pc_succ_sub a hA M n k] include hpf hP hS0 hSlim in private lemma pn_succ_le_T (n k : ℕ) (sγ : Summable fun m => gam a m n) : @@ -516,10 +482,6 @@ private lemma pn_succ_le_T (n k : ℕ) (sγ : Summable fun m => gam a m n) : end Limits -end E7 - -namespace E7 - private lemma hasSum_cp (a : ℕ → ℝ) {z : ℂ} {f : ℂ} (hf : HasSum (fun n => (a n : ℂ) * z ^ n) f) (P : ℝ[X]) : HasSum (fun k => (cp a P k : ℂ) * z ^ k) (f * aeval z P) := by @@ -655,8 +617,7 @@ theorem exists_entire_series_mul_tprod {a : ℕ → ℝ} (hpf : IsPolyaFreqSeq a exact mul_le_mul_of_nonneg_right (pn_le_a n k) (norm_nonneg _) have hmult : Multipliable fun j => (1 - (β j : ℂ) * z) := by have hs : Summable fun j => ‖((-β j : ℝ) : ℂ) * z‖ := by - simpa only [norm_mul] using - (summable_norm_ofReal (α := fun i => -β i) sβ.neg).mul_right ‖z‖ + simpa [norm_mul, Complex.norm_real] using sβ.neg.norm.mul_right ‖z‖ have := multipliable_one_add_of_summable hs convert this using 2 with j push_cast; ring @@ -683,6 +644,15 @@ theorem exists_exp_factorization_of_mul_neg_eq {F G Q N : ℂ → ℂ} classical set K : ℂ → ℂ := fun z => if N z ≠ 0 then F z / N z else Q z / G (-z) with hKdef have hGm : Differentiable ℂ (fun z => G (-z)) := hG.comp differentiable_neg + have hFnz : ∀ z, N z ≠ 0 → F z ≠ 0 := by + intro z hn hf + apply hQz z ?_ hf + exact (mul_eq_zero.mp (by rw [← hFG z, hf, zero_mul])).resolve_right hn + have hQnz : ∀ z, N z = 0 → Q z ≠ 0 := by + intro z hn hq + have hg := hNz z hn + apply hQz z hq + exact (mul_eq_zero.mp (by rw [hFG z, hq, zero_mul])).resolve_right hg have hK : Differentiable ℂ K := by intro w by_cases hw : N w ≠ 0 @@ -702,21 +672,10 @@ theorem exists_exp_factorization_of_mul_neg_eq {F G Q N : ℂ → ℂ} intro z by_cases hn : N z ≠ 0 · simp only [K, ite_eq_left hn] - refine div_ne_zero ?_ hn - intro hf - have : Q z * N z = 0 := by rw [← hFG z, hf, zero_mul] - rcases mul_eq_zero.1 this with h | h - · exact hQz z h hf - · exact hn h + exact div_ne_zero (hFnz z hn) hn · push Not at hn simp only [K, hn, ne_eq, not_true_eq_false, ite_false] - have hg := hNz z hn - refine div_ne_zero ?_ hg - intro hq - have : F z * G (-z) = 0 := by rw [hFG z, hq, zero_mul] - rcases mul_eq_zero.1 this with h | h - · exact hQz z hq h - · exact hg h + exact div_ne_zero (hQnz z hn) (hNz z hn) obtain ⟨φ, hφ, hexp⟩ := hK.exists_log_of_ne_zero hK0 refine ⟨φ, hφ, fun z => ?_, fun z => ?_⟩ · rw [hexp z] @@ -730,24 +689,12 @@ theorem exists_exp_factorization_of_mul_neg_eq {F G Q N : ℂ → ℂ} · rw [Complex.exp_neg, hexp z] by_cases hn : N z ≠ 0 · simp only [K, ite_eq_left hn] - have hf : F z ≠ 0 := by - intro hf - have : Q z * N z = 0 := by rw [← hFG z, hf, zero_mul] - rcases mul_eq_zero.1 this with h | h - · exact hQz z h hf - · exact hn h - field_simp + field_simp [hFnz z hn] linear_combination hFG z · push Not at hn have hg := hNz z hn simp only [K, hn, ne_eq, not_true_eq_false, ite_false] - have hq : Q z ≠ 0 := by - intro hq - have : F z * G (-z) = 0 := by rw [hFG z, hq, zero_mul] - rcases mul_eq_zero.1 this with h | h - · exact hQz z hq h - · exact hg h - field_simp + field_simp [hQnz z hn] end RealRooted.EdreiThoma diff --git a/RealRooted/EdreiThoma/Converse.lean b/RealRooted/EdreiThoma/Converse.lean index 317ba7261..57cd0a138 100644 --- a/RealRooted/EdreiThoma/Converse.lean +++ b/RealRooted/EdreiThoma/Converse.lean @@ -32,9 +32,9 @@ private lemma hasSum_conv_mul {a b : ℕ → ℝ} {z : ℂ} funext n simp only [natCauchyConvolution, Complex.ofReal_sum, Complex.ofReal_mul, Finset.sum_mul] refine Finset.sum_congr rfl fun k hk => ?_ - have hk' : k ≤ n := Nat.lt_succ_iff.1 (Finset.mem_range.1 hk) - have : z ^ n = z ^ k * z ^ (n - k) := by rw [← pow_add, Nat.add_sub_cancel' hk'] - rw [this]; ring + rw [show z ^ n = z ^ k * z ^ (n - k) by + rw [← pow_add, Nat.add_sub_cancel' (Nat.lt_succ_iff.1 (Finset.mem_range.1 hk))]] + ring rw [e, tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm ha hb] exact (summable_norm_sum_mul_range_of_summable_norm ha hb).of_norm.hasSum @@ -50,20 +50,17 @@ private lemma hasSum_expSeq (ε : ℝ) (z : ℂ) : private lemma summable_norm_expSeq (ε : ℝ) (z : ℂ) : Summable fun n => ‖(expSeq ε n : ℂ) * z ^ n‖ := by - have h := (hasSum_expSeq |ε| ‖z‖).summable - refine (h.norm).congr fun n => ?_ - simp [expSeq, norm_pow] + simpa [expSeq, norm_pow] using (hasSum_expSeq |ε| ‖z‖).summable.norm private lemma summable_norm_genFun {a : ℕ → ℝ} (h : IsPolyaFreqSeq a) (h0 : a 0 = 1) {z : ℂ} (hz : a 1 * ‖z‖ < 1) : Summable fun n => ‖(a n : ℂ) * z ^ n‖ := by - have hz' : a 1 * ‖((‖z‖ : ℝ) : ℂ)‖ < 1 := by simpa using hz - have := (IsPolyaFreqSeq.summable_genFun h h0 hz').norm + have := (IsPolyaFreqSeq.summable_genFun h h0 (by simpa using hz)).norm refine this.congr fun n => ?_ simp [norm_pow, abs_of_nonneg (IsPolyaFreqSeq.nonneg h n)] private lemma eventually_disc (c : ℝ) : ∀ᶠ z in 𝓝 (0 : ℂ), c * ‖z‖ < 1 := by - have : Continuous fun z : ℂ => c * ‖z‖ := continuous_const.mul continuous_norm - exact this.continuousAt.eventually_lt continuousAt_const (by simp) + exact (continuous_const.mul continuous_norm).continuousAt.eventually_lt continuousAt_const + (by simp) private lemma eventually_hasSum_genFun {a : ℕ → ℝ} (h : IsPolyaFreqSeq a) (h0 : a 0 = 1) : ∀ᶠ z in 𝓝 (0 : ℂ), @@ -79,10 +76,6 @@ private lemma eventually_hasSum_conv_exp {a : ℕ → ℝ} (h : IsPolyaFreqSeq a have := hasSum_conv_mul (summable_norm_genFun h h0 hz) (summable_norm_expSeq ε z) rwa [(hasSum_expSeq ε z).tsum_eq] at this -end Lib - -namespace Lib - private lemma differentiable_tprod_one_add {c : ℕ → ℂ} (hc : Summable fun i => ‖c i‖) : Differentiable ℂ (fun z => ∏' i, (1 + c i * z)) := by intro z @@ -103,8 +96,6 @@ private lemma tprod_one_add_ne_zero {c : ℕ → ℂ} (hc : Summable fun i => (h : ∀ i, 1 + c i * z ≠ 0) : ∏' i, (1 + c i * z) ≠ 0 := tprod_one_add_ne_zero_of_summable h (by simpa [norm_mul] using hc.mul_right ‖z‖) -private lemma tprod_one_add_zero (c : ℕ → ℂ) : ∏' i, (1 + c i * 0) = 1 := by simp - private lemma countable_zeros_tprod {c : ℕ → ℂ} (hc : Summable fun i => ‖c i‖) : {z : ℂ | ∏' i, (1 + c i * z) = 0}.Countable := by have hsub : {z : ℂ | ∏' i, (1 + c i * z) = 0} ⊆ ⋃ i, {z : ℂ | 1 + c i * z = 0} := by @@ -129,7 +120,7 @@ private lemma countable_preimage_sq {S : Set ℂ} (hS : S.Countable) : intro z hz simp only [Set.mem_ofPred_eq] at hz rw [← hs] at hz - rcases sq_eq_sq_iff_eq_or_eq_neg.1 hz with h | h <;> simp [h] + rcases sq_eq_sq_iff_eq_or_eq_neg.1 hz with h | h <;> simp_all private lemma summable_norm_ofReal {α : ℕ → ℝ} (sα : Summable α) : Summable fun i => ‖(α i : ℂ)‖ := by @@ -145,15 +136,13 @@ private lemma prod_sub_eq (β : ℕ → ℝ) (z : ℂ) : private lemma differentiable_prod_sub {β : ℕ → ℝ} (sβ : Summable β) : Differentiable ℂ (fun z => ∏' i, (1 - (β i : ℂ) * z)) := by - have := differentiable_prod_add (α := fun i => -β i) sβ.neg rw [show (fun z : ℂ => ∏' i, (1 - (β i : ℂ) * z)) = _ from funext (prod_sub_eq β)] - exact this + exact differentiable_prod_add (α := fun i => -β i) sβ.neg private lemma countable_zeros_prod_sub {β : ℕ → ℝ} (sβ : Summable β) : {z : ℂ | ∏' i, (1 - (β i : ℂ) * z) = 0}.Countable := by - have := countable_zeros_tprod (summable_norm_ofReal (α := fun i => -β i) sβ.neg) simp only [prod_sub_eq β] - exact this + exact countable_zeros_tprod (summable_norm_ofReal (α := fun i => -β i) sβ.neg) private lemma prod_sub_zero (β : ℕ → ℝ) : ∏' i, (1 - (β i : ℂ) * 0) = 1 := by simp @@ -180,15 +169,12 @@ private lemma differentiable_powerSeries {c : ℕ → ℂ} exact hd.differentiableAt (hU.mem_nhds (by simp [R])) private lemma tsum_mul_zero_pow (c : ℕ → ℂ) : ∑' n, c n * (0 : ℂ) ^ n = c 0 := by - rw [tsum_eq_single 0] - · simp - · intro b hb; simp [zero_pow hb] + rw [tsum_eq_single 0] <;> simp_all [zero_pow] private lemma hasSum_mul_zero_pow (c : ℕ → ℂ) : HasSum (fun n => c n * (0 : ℂ) ^ n) (c 0) := by - convert hasSum_single (f := fun n => c n * (0 : ℂ) ^ n) 0 ?_ using 1 - · simp - · intro b hb; simp [zero_pow hb] + convert hasSum_single (f := fun n => c n * (0 : ℂ) ^ n) 0 ?_ using 1 <;> + simp_all [zero_pow] private lemma eventually_inverse_mul {a b : ℕ → ℝ} (ha : IsPolyaFreqSeq a) (ha0 : a 0 = 1) (hb : IsPolyaFreqSeq b) @@ -211,15 +197,10 @@ private lemma eventually_inverse_mul {a b : ℕ → ℝ} (ha : IsPolyaFreqSeq a) rw [hrec n] split_ifs <;> simp simp only [hc] at this - refine this.unique ?_ - have h3 : HasSum - (fun n : ℕ => ((fun n : ℕ => if n = 0 then (1 : ℂ) else 0) n) * z ^ n) 1 := by - convert hasSum_ite_eq 0 (1 : ℂ) using 1 - funext n - rcases Nat.eq_zero_or_pos n with rfl | hn - · simp - · simp [hn.ne'] - exact h3 + apply this.unique + convert hasSum_ite_eq 0 (1 : ℂ) using 1 + funext n + rcases Nat.eq_zero_or_pos n with rfl | hn <;> simp_all private lemma eq_neg_inv_of_one_add_mul_eq_zero {c : ℝ} {z : ℂ} (h : 1 + (c : ℂ) * z = 0) : c ≠ 0 ∧ z = ((-(1 / c) : ℝ) : ℂ) := by @@ -306,7 +287,6 @@ private theorem exists_hasSum_exp_mul_prod_div {a : ℕ → ℝ} (hpf : IsPolyaF simp only [hN]; congr 1; funext i; ring have hQneg : ∀ z, Qf (-z) = ∏' i, (1 + (β i : ℂ) * z) := fun z => by simp only [hQf]; congr 1; funext i; ring - -- `p 0 = 1` and `q 0 = 1` have hp0 : p 0 = 1 := by have e := hpe.self_of_nhds rw [Lib.tsum_mul_zero_pow, Lib.tsum_mul_zero_pow, Lib.prod_sub_zero] at e @@ -317,7 +297,6 @@ private theorem exists_hasSum_exp_mul_prod_div {a : ℕ → ℝ} (hpf : IsPolyaF rw [Lib.tsum_mul_zero_pow, Lib.tsum_mul_zero_pow, Lib.prod_sub_zero] at e simp only [mul_one, hb0, Complex.ofReal_one] at e exact_mod_cast e - -- the functional identity `F(z) G(-z) = Q(z) N(z)` have hFG : ∀ z, F z * G (-z) = Qf z * N z := by have t1 : Tendsto (fun z : ℂ => -z) (𝓝 0) (𝓝 0) := by simpa using (continuous_neg.tendsto (0 : ℂ)) @@ -334,14 +313,12 @@ private theorem exists_hasSum_exp_mul_prod_div {a : ℕ → ℝ} (hpf : IsPolyaF have h2 : AnalyticOnNhd ℂ (fun z => Qf z * N z) Set.univ := (dQ.mul dN).differentiableOn.analyticOnNhd isOpen_univ exact congrFun (h1.eq_of_eventuallyEq h2 hev) - -- zeros have hNz : ∀ z, N z = 0 → G (-z) ≠ 0 := by intro z hz - have : ∃ i, 1 + (α i : ℂ) * z = 0 := by + obtain ⟨i, hi⟩ : ∃ i, 1 + (α i : ℂ) * z = 0 := by by_contra hc push Not at hc exact Lib.tprod_one_add_ne_zero (Lib.summable_norm_ofReal sα) hc hz - obtain ⟨i, hi⟩ := this obtain ⟨hai, hzi⟩ := Lib.eq_neg_inv_of_one_add_mul_eq_zero hi have hr : (0 : ℝ) ≤ 1 / α i := div_nonneg zero_le_one (hα i) have := FinalAux.nonneg_series_ge hq hGs hr @@ -350,13 +327,12 @@ private theorem exists_hasSum_exp_mul_prod_div {a : ℕ → ℝ} (hpf : IsPolyaF intro h0'; rw [h0', norm_zero] at this; linarith have hQz : ∀ z, Qf z = 0 → F z ≠ 0 := by intro z hz - have : ∃ i, 1 + ((-β i : ℝ) : ℂ) * z = 0 := by + obtain ⟨i, hi⟩ : ∃ i, 1 + ((-β i : ℝ) : ℂ) * z = 0 := by by_contra hc push Not at hc rw [show Qf z = _ from Lib.prod_sub_eq β z] at hz exact Lib.tprod_one_add_ne_zero (Lib.summable_norm_ofReal (α := fun i => -β i) sβ.neg) hc hz - obtain ⟨i, hi⟩ := this obtain ⟨hbi, hzi⟩ := Lib.eq_neg_inv_of_one_add_mul_eq_zero hi have hr : (0 : ℝ) ≤ -(1 / -β i) := by rw [div_neg, neg_neg]; exact div_nonneg zero_le_one (hβ i) @@ -429,19 +405,13 @@ private theorem isPolyaFreqSeq_even {a : ℕ → ℝ} (h : IsPolyaFreqSeq a) : IsPolyaFreqSeq (fun k => a (2 * k)) := by intro n r c hr hc have hm : StrictMono (fun x : ℕ => 2 * x) := fun x y (hxy : x < y) => by simp only; lia - have hminor := h (rows := fun i => 2 * r i) (cols := fun i => 2 * c i) - (hm.comp hr) (hm.comp hc) have e : (toeplitz fun k => a (2 * k)).submatrix r c = (toeplitz a).submatrix (fun i => 2 * r i) (fun i => 2 * c i) := by ext i j simp only [Matrix.submatrix_apply, toeplitz_apply] - by_cases hij : c j ≤ r i - · rw [ite_eq_left hij, ite_eq_left (by lia)] - congr 1 - lia - · rw [ite_eq_right hij, ite_eq_right (by lia)] + split_ifs <;> congr 1 <;> lia rw [e] - exact hminor + exact h (hm.comp hr) (hm.comp hc) /-- **Edrei's Proposition A for arbitrary PF sequences (E8, via `e^{εz}`).** Apply `exists_hasSum_exp_mul_prod_div` to `a ⋆ exp(z)` and absorb `-z` into `φ`. -/ @@ -520,8 +490,7 @@ private theorem exists_hasSum_edreiFunction_of_property_P {a : ℕ → ℝ} {z | D z = 0} ∪ ({z | D (-z) = 0} ∪ {z | z ^ 2 ∈ {w | Ds w = 0}}) := by intro z hz simp only [hU, Set.mem_compl_iff, Set.mem_ofPred_eq, not_and_or, not_not] at hz - simp only [Set.mem_union, Set.mem_ofPred_eq] - tauto + simpa only [Set.mem_union, Set.mem_ofPred_eq] using hz refine Set.Countable.mono hsub ((Lib.countable_zeros_prod_sub sβ).union (Set.Countable.union ?_ (Lib.countable_preimage_sq (Lib.countable_zeros_prod_sub sβs)))) have := (Lib.countable_zeros_prod_sub sβ).preimage neg_injective @@ -544,24 +513,17 @@ private theorem exists_hasSum_edreiFunction_of_property_P {a : ℕ → ℝ} refine DifferentiableAt.differentiableWithinAt ?_ have e1 : DifferentiableAt ℂ (fun z => Complex.exp (φ z) * N z / D z) z := (((hφ z).cexp).mul (dN z)).div (dD z) h1 - have e2 : DifferentiableAt ℂ (fun z => Complex.exp (φ (-z)) * N (-z) / D (-z)) z := by - have hn : DifferentiableAt ℂ (fun z : ℂ => -z) z := differentiableAt_id.neg - have d1 : DifferentiableAt ℂ (fun z => φ (-z)) z := (hφ (-z)).comp z hn - have d2 : DifferentiableAt ℂ (fun z => N (-z)) z := (dN (-z)).comp z hn - have d3 : DifferentiableAt ℂ (fun z => D (-z)) z := (dD (-z)).comp z hn - exact (d1.cexp.mul d2).div d3 h2 - exact e1.add e2 + have hn : DifferentiableAt ℂ (fun z : ℂ => -z) z := differentiableAt_id.neg + exact e1.add ((((hφ (-z)).comp z hn).cexp.mul ((dN (-z)).comp z hn)).div + ((dD (-z)).comp z hn) h2) have hRa : AnalyticOnNhd ℂ R U := by refine DifferentiableOn.analyticOnNhd (fun z hz => ?_) hUo obtain ⟨-, -, h3⟩ := hz refine DifferentiableAt.differentiableWithinAt ?_ have hs : DifferentiableAt ℂ (fun z : ℂ => z ^ 2) z := differentiableAt_pow 2 - have d1 : DifferentiableAt ℂ (fun z => φs (z ^ 2)) z := (hφs (z ^ 2)).comp z hs - have d2 : DifferentiableAt ℂ (fun z => Ns (z ^ 2)) z := - DifferentiableAt.comp (g := Ns) z (dNs (z ^ 2)) hs - have d3 : DifferentiableAt ℂ (fun z => Ds (z ^ 2)) z := - DifferentiableAt.comp (g := Ds) z (dDs (z ^ 2)) hs - exact ((d1.cexp.const_mul 2).mul d2).div d3 h3 + exact (((((hφs (z ^ 2)).comp z hs).cexp.const_mul 2).mul + (DifferentiableAt.comp (g := Ns) z (dNs (z ^ 2)) hs)).div + (DifferentiableAt.comp (g := Ds) z (dDs (z ^ 2)) hs) h3) have hev : L =ᶠ[𝓝 0] R := by have t1 : Tendsto (fun z : ℂ => -z) (𝓝 0) (𝓝 0) := by simpa using (continuous_neg.tendsto (0 : ℂ)) @@ -583,12 +545,7 @@ private theorem exists_hasSum_edreiFunction_of_property_P {a : ℕ → ℝ} obtain ⟨γ, hγ, hφγ⟩ := exists_nonneg_eq_affine_of_series_zero hφ hc hα hβ sα sβ hp hq have hφ0 : Complex.exp (φ 0) = 1 := by have e0 := hrep.self_of_nhds - have e1 : HasSum (fun n => (a n : ℂ) * (0 : ℂ) ^ n) 1 := by - convert hasSum_single (f := fun n => (a n : ℂ) * (0 : ℂ) ^ n) 0 ?_ using 1 - · simp [h0] - · intro b hb; simp [zero_pow hb] - have := e0.unique e1 - simpa using this + simpa [h0] using e0.unique (Lib.hasSum_mul_zero_pow fun n => (a n : ℂ)) refine ⟨γ, α, β, hγ, hα, hβ, sα, sβ, ?_⟩ filter_upwards [hrep] with z hz convert hz using 1 @@ -599,10 +556,8 @@ private theorem exists_hasSum_edreiFunction_of_property_P {a : ℕ → ℝ} private lemma edreiFun_add_gamma (C γ δ : ℝ) (k : ℕ) (α β : ℕ → ℝ) (z : ℂ) : Complex.EdreiThoma.edreiFunction C (γ + δ) k α β z = Complex.exp (δ * z) * Complex.EdreiThoma.edreiFunction C γ k α β z := by - unfold Complex.EdreiThoma.edreiFunction - push_cast - rw [add_mul, Complex.exp_add] - ring + unfold Complex.EdreiThoma.edreiFunction; push_cast + rw [add_mul, Complex.exp_add]; ring private lemma exists_edreiFunction_eq_mul_exp {a : ℕ → ℝ} (h : IsPolyaFreqSeq a) (h0 : a 0 = 1) {ε : ℝ} (hε : 0 < ε) : From 5a9e96e3d6694b5bb60a4029b4714c5d02edde4f Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Wed, 21 Oct 2026 11:51:49 +0000 Subject: [PATCH 4/4] Golf Boundary, Chow, GustafssonSolus Statements unchanged; 193 lines shorter. Proofs drafted by a Codex worker, checked with the lakefile options and built locally. Co-Authored-By: Claude Opus 5.5 --- RealRooted/AffineFamily/Boundary.lean | 175 ++++-------------- RealRooted/HosterStump/Chow.lean | 175 +++++++----------- .../ThresholdMatrix/GustafssonSolus.lean | 157 +++++----------- 3 files changed, 157 insertions(+), 350 deletions(-) diff --git a/RealRooted/AffineFamily/Boundary.lean b/RealRooted/AffineFamily/Boundary.lean index eefc9fd3b..56fdcc067 100644 --- a/RealRooted/AffineFamily/Boundary.lean +++ b/RealRooted/AffineFamily/Boundary.lean @@ -45,8 +45,6 @@ private lemma affine_family_pair_data {f g : ℝ[X]} have hCt_nonneg : HasNonnegCoeffs (C t * f) := nonnegCoeffs_C_mul ht.le hfnn have hsum_nonneg : HasNonnegCoeffs (C t * f + g) := hCt_nonneg.add hgnn have hXf_nonneg : HasNonnegCoeffs (X * f) := hfnn.X_mul - have hCt_ne : C t * f ≠ 0 := - mul_ne_zero (C_ne_zero.mpr ht.ne') hf0 have hsum_ne : C t * f + g ≠ 0 := add_ne_zero_of_hasNonnegCoeffs_of_right_ne_zero hCt_nonneg hgnn hg0 have hXf_ne : X * f ≠ 0 := mul_ne_zero X_ne_zero hf0 @@ -77,7 +75,6 @@ protected theorem AffineFamily.isRealRooted_of_add_C_mul_right_family_of_natDegr unfold g₀ apply monic_C_mul_of_mul_leadingCoeff_eq_one simp_all - have hf₀_pos : HasPosLeadingCoeff f₀ := hasPosLeadingCoeff_of_monic hf₀_monic have hg₀_pos : HasPosLeadingCoeff g₀ := hasPosLeadingCoeff_of_monic hg₀_monic have hdeg₀ : f₀.natDegree < g₀.natDegree := by simp [f₀, g₀, natDegree_C_mul, hf_lc_ne, hg_lc_ne, hdeg] @@ -103,103 +100,35 @@ protected theorem AffineFamily.isRealRooted_of_add_C_mul_right_family_of_natDegr simp [g₀, f₀] grind lia - have hg₀_rr : (g₀ ≠ 0 ∧ g₀.Splits) := by - have hroots_real : - ∀ z ∈ (g₀.map (algebraMap ℝ ℂ)).roots, z ∈ (algebraMap ℝ ℂ).range := by - intro z hz_mem - have hmap_ne : g₀.map (algebraMap ℝ ℂ) ≠ 0 := by simp_all - have hz_root : (g₀.map (algebraMap ℝ ℂ)).IsRoot z := - (Polynomial.mem_roots hmap_ne).1 hz_mem - have hz_aeval : g₀.aeval z = 0 := by simp_all - by_contra hz_range - have hz_im_ne : z.im ≠ 0 := by - intro hz_im - apply hz_range - refine ⟨z.re, ?_⟩ - apply Complex.ext <;> simp [hz_im] - let δ : ℝ := |z.im| / 2 - let R : ℝ := max ‖z‖ 1 - have hδ_pos : 0 < δ := by grind - have hR_pos : 0 < R := by grind - have hg₀_deg_pos : 0 < g₀.natDegree := lt_of_le_of_lt (Nat.zero_le _) hdeg₀ - have hdeg_nat_ne : g₀.natDegree ≠ 0 := Nat.ne_of_gt hg₀_deg_pos - let u : ℝ := δ / (2 * R) - let ε : ℝ := (u ^ g₀.natDegree) / (g₀.natDegree + 1) - have hu_nonneg : 0 ≤ u := by - unfold u - positivity - have hu_pos : 0 < u := by - unfold u - positivity - have hε_pos : 0 < ε := by - unfold ε - positivity - let μ : ℝ := ε / (coeffSumRange f₀ + 1) - have hcoeff_nonneg : 0 ≤ coeffSumRange f₀ := by - unfold coeffSumRange - exact Finset.sum_nonneg fun _ _ => norm_nonneg _ - have hμ_pos : 0 < μ := by - unfold μ - positivity - have hμ_bound : μ * coeffSumRange f₀ < ε := by - unfold μ - have hden_pos : 0 < coeffSumRange f₀ + 1 := by linarith - have hfrac_lt_one : coeffSumRange f₀ / (coeffSumRange f₀ + 1) < 1 := by - rw [div_lt_iff₀ hden_pos] - linarith - have hcalc : - (ε / (coeffSumRange f₀ + 1)) * coeffSumRange f₀ = - ε * (coeffSumRange f₀ / (coeffSumRange f₀ + 1)) := by - grind - simp_all - have hcoeff : - ∀ i : ℕ, ‖(g₀ + C μ * f₀).coeff i - g₀.coeff i‖ < ε := by - intro i - exact lt_of_le_of_lt - (norm_coeff_sub_add_C_mul_le g₀ f₀ (μ := μ) (M := coeffSumRange f₀) - hμ_pos.le (fun j => coeff_norm_le_coeffSumRange f₀ j) i) - hμ_bound - have hμf_deg_lt : (C μ * f₀).natDegree < g₀.natDegree := by - simpa [natDegree_C_mul hμ_pos.ne'] using hdeg₀ - have hsum_deg : (g₀ + C μ * f₀).natDegree = g₀.natDegree := - natDegree_add_eq_left_of_natDegree_lt_of_posLeadingCoeff hμf_deg_lt hg₀_pos - have hsum_monic : (g₀ + C μ * f₀).Monic := by - unfold Polynomial.Monic Polynomial.leadingCoeff - rw [hsum_deg, coeff_add, coeff_eq_zero_of_natDegree_lt hμf_deg_lt, - hg₀_monic.coeff_natDegree, add_zero] - obtain ⟨w, hw_root, hw_dist⟩ := - exists_complex_aroot_near_of_isRealRooted_of_monic_of_coeff_close - (f := g₀) (g := g₀ + C μ * f₀) (z := z) (ε := ε) - hε_pos hz_aeval hg₀_monic hsum_monic hsum_deg hcoeff - (hfamily₀ hμ_pos).2 - have hw_im_zero : w.im = 0 := - RealRooted.im_eq_zero_of_mem_aroots_of_isRealRooted - (hfamily₀ hμ_pos).1 (hfamily₀ hμ_pos).2 hw_root - have hbound_eq : - ((g₀.natDegree + 1) * ε) ^ ((g₀.natDegree : ℝ)⁻¹) * R = δ / 2 := by - have hmul : - ((g₀.natDegree + 1 : ℝ) * ε) = u ^ g₀.natDegree := by - grind - calc - ((g₀.natDegree + 1) * ε) ^ ((g₀.natDegree : ℝ)⁻¹) * R - = (u ^ g₀.natDegree) ^ ((g₀.natDegree : ℝ)⁻¹) * R := by lia - _ = u * R := by rw [Real.pow_rpow_inv_natCast hu_nonneg hdeg_nat_ne] - _ = δ / 2 := by grind - have hdist_lt_delta : ‖z - w‖ < δ := by grind - have him_le : |z.im| ≤ ‖z - w‖ := by - simpa [Complex.sub_im, hw_im_zero] using (Complex.abs_im_le_norm (z - w)) - grind - have hsplit : g₀.Splits := - Polynomial.Splits.of_splits_map (i := algebraMap ℝ ℂ) - (IsAlgClosed.splits _) hroots_real - exact ⟨hg₀_monic.ne_zero, hsplit⟩ + let δ : ℕ → ℝ := fun M => ((M : ℝ) + 1)⁻¹ + have hδ_pos (M : ℕ) : 0 < δ M := by positivity + have hδ : Filter.Tendsto δ Filter.atTop (nhds 0) := by + simpa [δ, one_div] using tendsto_one_div_add_atTop_nhds_zero_nat (𝕜 := ℝ) + let p : ℕ → ℝ[X] := fun M => g₀ + C (δ M) * f₀ + have hp_deg (M : ℕ) : (p M).natDegree = g₀.natDegree := + natDegree_add_eq_left_of_natDegree_lt_of_posLeadingCoeff + (by simpa [p, natDegree_C_mul (hδ_pos M).ne'] using hdeg₀) hg₀_pos + have hp_monic (M : ℕ) : (p M).Monic := by + unfold Polynomial.Monic Polynomial.leadingCoeff + rw [hp_deg] + dsimp only [p] + rw [coeff_add, hg₀_monic.coeff_natDegree, + coeff_eq_zero_of_natDegree_lt + (p := C (δ M) * f₀) (by simpa [natDegree_C_mul (hδ_pos M).ne'] using hdeg₀), + add_zero] + have hp_coeff (i : ℕ) : Filter.Tendsto (fun M => (p M).coeff i) Filter.atTop + (nhds (g₀.coeff i)) := by + simp only [p, coeff_add, coeff_C_mul] + simpa using tendsto_const_nhds.add (hδ.mul_const (f₀.coeff i)) + have hg₀_rr : g₀ ≠ 0 ∧ g₀.Splits := ⟨hg₀_monic.ne_zero, + splits_of_monic_of_coeff_tendsto hg₀_monic hp_monic hp_deg + (fun M => (hfamily₀ (hδ_pos M)).2) hp_coeff⟩ have hg_scale : C g.leadingCoeff * g₀ = g := by unfold g₀ ext n simp_all - have hg_rr_scaled : ((C g.leadingCoeff * g₀) ≠ 0 ∧ (C g.leadingCoeff * g₀).Splits) := - isRealRooted_C_mul hg₀_rr.1 hg₀_rr.2 hg_lc_ne - lia + rw [← hg_scale] + exact isRealRooted_C_mul hg₀_rr.1 hg₀_rr.2 hg_lc_ne /-- Boundary closure for a right family `g + μ f` when the perturbation has no higher degree than the base polynomial. The equal-degree case is exactly the @@ -343,30 +272,16 @@ private lemma isRealRooted_add_X_mul_right_of_affine_family {s : ℝ} (hs : 0 < s) : ((g + C s * (X * f)) ≠ 0 ∧ (g + C s * (X * f)).Splits) := by have hf_pos : HasPosLeadingCoeff f := hfnn.pos_leadingCoeff hf0 have hg_pos : HasPosLeadingCoeff g := hgnn.pos_leadingCoeff hg0 - have hXf_nonneg : HasNonnegCoeffs (X * f) := hfnn.X_mul - have hXf_ne : X * f ≠ 0 := mul_ne_zero X_ne_zero hf0 - have hCsXf_nonneg : HasNonnegCoeffs (C s * (X * f)) := - nonnegCoeffs_C_mul hs.le hXf_nonneg - have hCsXf_ne : C s * (X * f) ≠ 0 := - mul_ne_zero (C_ne_zero.mpr hs.ne') hXf_ne - have hbase_nonneg : HasNonnegCoeffs (g + C s * (X * f)) := - hgnn.add hCsXf_nonneg - have hbase_ne : g + C s * (X * f) ≠ 0 := - add_ne_zero_of_hasNonnegCoeffs_of_right_ne_zero hgnn hCsXf_nonneg hCsXf_ne have hXf_pos : HasPosLeadingCoeff (X * f) := hf_pos.X_mul have hCsXf_pos : HasPosLeadingCoeff (C s * (X * f)) := hasPosLeadingCoeff_C_mul hs hXf_pos - have hbase_pos : HasPosLeadingCoeff (g + C s * (X * f)) := by - rcases lt_trichotomy g.natDegree (X * f).natDegree with hdeg | hdeg | hdeg - · have hdeg' : g.natDegree < (C s * (X * f)).natDegree := by - simpa [natDegree_C_mul hs.ne'] using hdeg - exact hasPosLeadingCoeff_add_of_natDegree_lt_right hdeg' hCsXf_pos - · have hdeg' : g.natDegree = (C s * (X * f)).natDegree := by - simpa [natDegree_C_mul hs.ne'] using hdeg - exact hasPosLeadingCoeff_add_of_same_natDegree hdeg' hg_pos hCsXf_pos - · have hdeg' : (C s * (X * f)).natDegree < g.natDegree := by - simpa [natDegree_C_mul hs.ne'] using hdeg - exact hasPosLeadingCoeff_add_of_natDegree_lt_left hdeg' hg_pos + have hCsXf_nonneg : HasNonnegCoeffs (C s * (X * f)) := + nonnegCoeffs_C_mul hs.le hfnn.X_mul + have hbase_nonneg := hgnn.add hCsXf_nonneg + have hbase_ne : g + C s * (X * f) ≠ 0 := by + rw [add_comm] + exact add_ne_zero_of_hasNonnegCoeffs_of_right_ne_zero hCsXf_nonneg hgnn hg0 + have hbase_pos := hbase_nonneg.pos_leadingCoeff hbase_ne have hbase_deg : f.natDegree ≤ (g + C s * (X * f)).natDegree := by rcases lt_trichotomy g.natDegree (X * f).natDegree with hdeg | hdeg | hdeg · have hsum_deg : (g + C s * (X * f)).natDegree = (C s * (X * f)).natDegree := @@ -404,12 +319,9 @@ protected lemma AffineFamily.posComboRealRooted_right_of_affine_family (haff : ∀ {s t : ℝ}, 0 < s → 0 < t → ((((C s * X + C t) * f) + g) ≠ 0 ∧ (((C s * X + C t) * f) + g).Splits)) : - PosComboRealRooted g (X * f) := by - refine PosComboRealRooted.of_add_right ?_ - intro s hs - exact - isRealRooted_add_X_mul_right_of_affine_family - hf0 hg0 hfnn hgnn haff hs + PosComboRealRooted g (X * f) := + PosComboRealRooted.of_add_right fun {_} hs => + isRealRooted_add_X_mul_right_of_affine_family hf0 hg0 hfnn hgnn haff hs /-- Data package for the fixed right-hand pair `(g, X * f)` extracted from the affine family after taking the boundary `t → 0`. This is the natural target @@ -428,11 +340,9 @@ protected lemma AffineFamily.affine_family_right_pair_data {f g : ℝ[X]} X * f ≠ 0 ∧ HasPosLeadingCoeff g ∧ HasPosLeadingCoeff (X * f) := by - have hXf_nonneg : HasNonnegCoeffs (X * f) := hfnn.X_mul - have hXf_ne : X * f ≠ 0 := mul_ne_zero X_ne_zero hf0 refine ⟨AffineFamily.posComboRealRooted_right_of_affine_family hf0 hg0 hfnn hgnn haff, - hgnn, hXf_nonneg, hg0, hXf_ne, + hgnn, hfnn.X_mul, hg0, mul_ne_zero X_ne_zero hf0, hgnn.pos_leadingCoeff hg0, (hfnn.pos_leadingCoeff hf0).X_mul⟩ /-! ## Degree control for the affine family @@ -512,18 +422,13 @@ theorem common_right_pair_iff_root_zero_or_common_fg (∃ r, g.IsRoot r ∧ (X * f).IsRoot r) ↔ g.IsRoot 0 ∨ ∃ r, g.IsRoot r ∧ f.IsRoot r := by constructor - · intro h - rcases h with ⟨r, hgr, hXr⟩ + · rintro ⟨r, hgr, hXr⟩ by_cases hr0 : r = 0 · lia - · right - exact ⟨r, hgr, isRoot_of_X_mul_of_ne_zero hr0 hXr⟩ - · intro h - rcases h with hg0 | hcommon + · exact Or.inr ⟨r, hgr, isRoot_of_X_mul_of_ne_zero hr0 hXr⟩ + · rintro (hg0 | ⟨r, hgr, hfr⟩) · exact ⟨0, hg0, by simp [Polynomial.IsRoot.def]⟩ - · rcases hcommon with ⟨r, hgr, hfr⟩ - refine ⟨r, hgr, ?_⟩ - simp_all + · exact ⟨r, hgr, by simp_all⟩ /-- If `g` has nonnegative coefficients and no common root with `X * f`, then every real root of `g` is strictly negative. -/ diff --git a/RealRooted/HosterStump/Chow.lean b/RealRooted/HosterStump/Chow.lean index 65e3673e0..1bd892391 100644 --- a/RealRooted/HosterStump/Chow.lean +++ b/RealRooted/HosterStump/Chow.lean @@ -64,24 +64,19 @@ noncomputable def augChowOfFlagH (n : ℕ) (β : Finset ℕ → ℝ) : ℝ[X] := C (β S) * X ^ S.card * (X + 1) ^ (n + 1 - 2 * S.card) /-- The flag `h`-vector of the dual poset: `β^*(S) = β(n + 1 - S)`. -/ -def dualFlagH (n : ℕ) (β : Finset ℕ → ℝ) : Finset ℕ → ℝ := fun S => β (reflectSet n S) +def dualFlagH (n : ℕ) (β : Finset ℕ → ℝ) : Finset ℕ → ℝ := + fun S => β (reflectSet n S) /-- Membership in `isolatedSubsets`. -/ -lemma mem_isolatedSubsets {U S : Finset ℕ} : S ∈ isolatedSubsets U ↔ S ⊆ U ∧ IsIsolated S := by +lemma mem_isolatedSubsets {U S : Finset ℕ} : + S ∈ isolatedSubsets U ↔ S ⊆ U ∧ IsIsolated S := by simp [isolatedSubsets] /-- Membership in a reflected set. -/ lemma mem_reflectSet {n : ℕ} {S : Finset ℕ} (hS : S ⊆ Finset.range n) {i : ℕ} : i ∈ reflectSet n S ↔ i < n ∧ n - 1 - i ∈ S := by simp only [reflectSet, Finset.mem_image] - constructor - · rintro ⟨s, hs, rfl⟩ - have hs' := Finset.mem_range.1 (hS hs) - refine ⟨by lia, ?_⟩ - have e : n - 1 - (n - 1 - s) = s := by lia - rwa [e] - · rintro ⟨hi, hmem⟩ - exact ⟨n - 1 - i, hmem, by lia⟩ + grind /-- A reflected set lies in `range n`. -/ lemma reflectSet_subset_range {n : ℕ} {S : Finset ℕ} (hS : S ⊆ Finset.range n) : @@ -101,24 +96,15 @@ lemma reflectSet_reflectSet {n : ℕ} {S : Finset ℕ} (hS : S ⊆ Finset.range reflectSet n (reflectSet n S) = S := by ext i rw [mem_reflectSet (reflectSet_subset_range hS), mem_reflectSet hS] - constructor - · rintro ⟨_, _, hm⟩ - have e : n - 1 - (n - 1 - i) = i := by lia - rwa [e] at hm - · intro hi - have h1 := Finset.mem_range.1 (hS hi) - have e : n - 1 - (n - 1 - i) = i := by lia - exact ⟨h1, by lia, by rw [e]; exact hi⟩ + grind /-- Reflection preserves isolated sets. -/ lemma isIsolated_reflectSet {n : ℕ} {S : Finset ℕ} (hS : S ⊆ Finset.range n) (hiso : IsIsolated S) : IsIsolated (reflectSet n S) := by intro i hi hi1 rw [mem_reflectSet hS] at hi hi1 - have := hiso (n - 1 - (i + 1)) hi1.2 - have e : n - 1 - (i + 1) + 1 = n - 1 - i := by lia - rw [e] at this - exact this hi.2 + exact (hiso (n - 1 - (i + 1)) hi1.2) + (by simpa only [show n - 1 - (i + 1) + 1 = n - 1 - i by lia] using hi.2) private lemma sum_isolatedSubsets_reflect {n : ℕ} {U V : Finset ℕ} (hU : U ⊆ Finset.range n) (hV : V ⊆ Finset.range n) (hUV : ∀ i, i < n → (i ∈ V ↔ n - 1 - i ∈ U)) @@ -136,10 +122,7 @@ private lemma sum_isolatedSubsets_reflect {n : ℕ} {U V : Finset ℕ} (hU : U have hDr : D ⊆ Finset.range n := hD.1.trans hV refine ⟨fun i hi => ?_, isIsolated_reflectSet hDr hD.2⟩ rw [mem_reflectSet hDr] at hi - have h1 := hD.1 hi.2 - have := (hUV (n - 1 - i) (by lia)).1 h1 - have e : n - 1 - (n - 1 - i) = i := by lia - rwa [e] at this + grind · intro S hS exact reflectSet_reflectSet ((mem_isolatedSubsets.1 hS).1.trans hU) · intro D hD @@ -169,7 +152,8 @@ noncomputable def flagHOfH (n : ℕ) (h : ℕ → ℝ) : Finset ℕ → ℝ := f ∑ k ∈ Finset.range (n + 1), h k * (desCount n k (reflectSet n S) : ℝ) /-- The vector `flagHOfH n h` satisfies identity (1.3) by definition. -/ -theorem isSimplicialFlagH_flagHOfH (n : ℕ) (h : ℕ → ℝ) : IsSimplicialFlagH n h (flagHOfH n h) := +theorem isSimplicialFlagH_flagHOfH (n : ℕ) (h : ℕ → ℝ) : + IsSimplicialFlagH n h (flagHOfH n h) := fun _ _ => rfl /-! ### Isolated sets and the refined family -/ @@ -199,28 +183,25 @@ private lemma card_le_of_isIsolated_of_subset_Ico {a m : ℕ} {D : Finset ℕ} ( private lemma card_le_of_mem_isolatedSubsets_Icc {n : ℕ} {D : Finset ℕ} (hD : D ∈ isolatedSubsets (Finset.Icc 1 (n - 1))) : D.card ≤ n / 2 := by rw [mem_isolatedSubsets] at hD - have := card_le_of_isIsolated_of_subset_Ico (a := 1) (m := n - 1) hD.2 (fun i hi => by - have := Finset.mem_Icc.1 (hD.1 hi) - rw [Finset.mem_Ico] - lia) + have := card_le_of_isIsolated_of_subset_Ico (a := 1) (m := n - 1) hD.2 fun i hi => by + simp only [Finset.mem_Ico] at * + grind lia private lemma card_le_of_mem_isolatedSubsets_range_pred {n : ℕ} {D : Finset ℕ} (hD : D ∈ isolatedSubsets (Finset.range (n - 1))) : D.card ≤ n / 2 := by rw [mem_isolatedSubsets] at hD - have := card_le_of_isIsolated_of_subset_Ico (a := 0) (m := n - 1) hD.2 (fun i hi => by - have := Finset.mem_range.1 (hD.1 hi) - rw [Finset.mem_Ico] - lia) + have := card_le_of_isIsolated_of_subset_Ico (a := 0) (m := n - 1) hD.2 fun i hi => by + simp only [Finset.mem_Ico] at * + grind lia private lemma card_le_of_mem_isolatedSubsets_range {n : ℕ} {D : Finset ℕ} (hD : D ∈ isolatedSubsets (Finset.range n)) : D.card ≤ (n + 1) / 2 := by rw [mem_isolatedSubsets] at hD - exact card_le_of_isIsolated_of_subset_Ico (a := 0) (m := n) hD.2 (fun i hi => by - have := Finset.mem_range.1 (hD.1 hi) + exact card_le_of_isIsolated_of_subset_Ico (a := 0) (m := n) hD.2 fun i hi => by rw [Finset.mem_Ico] - lia) + exact ⟨Nat.zero_le _, by simpa using Finset.mem_range.1 (hD.1 hi)⟩ private lemma refined_empty_eq_sum_isolatedSubsets {n k : ℕ} (hk : k ≤ n) (T : Finset ℕ) : refined n k ∅ T = @@ -268,7 +249,8 @@ private lemma sum_C_mul_refined_eq (n : ℕ) (h : ℕ → ℝ) (T : Finset ℕ) /-! ### Lemma 3.1: the gamma-polynomials of the Chow polynomials -/ -private lemma sum_isolatedSubsets_eq_gammaTransform {d : ℕ} {T : Finset ℕ} (c : Finset ℕ → ℝ) +private lemma sum_isolatedSubsets_eq_gammaTransform {d : ℕ} {T : Finset ℕ} + (c : Finset ℕ → ℝ) (hcard : ∀ D ∈ isolatedSubsets T, D.card ≤ d / 2) : ∑ D ∈ isolatedSubsets T, C (c D) * X ^ D.card * (X + 1) ^ (d - 2 * D.card) = gammaTransform d (∑ D ∈ isolatedSubsets T, C (c D) * X ^ D.card) := by @@ -277,10 +259,8 @@ private lemma sum_isolatedSubsets_eq_gammaTransform {d : ℕ} {T : Finset ℕ} ( rw [mul_assoc, C_mul_X_pow_eq_monomial, gammaTransform_monomial] simp only [hcard D hD, ↓reduceIte, gammaBasisTerm] -private lemma Icc_subset_range {n : ℕ} : Finset.Icc 1 (n - 1) ⊆ Finset.range n := fun i hi => by - have := Finset.mem_Icc.1 hi - rw [Finset.mem_range] - lia +private lemma Icc_subset_range {n : ℕ} : Finset.Icc 1 (n - 1) ⊆ Finset.range n := + fun i hi => Finset.mem_range.2 (by have := Finset.mem_Icc.1 hi; lia) private lemma range_pred_subset_range {n : ℕ} : Finset.range (n - 1) ⊆ Finset.range n := Finset.range_mono (by lia) @@ -292,8 +272,8 @@ theorem chowOfFlagH_eq_gammaTransform {n : ℕ} {h : ℕ → ℝ} {β : Finset chowOfFlagH n β = gammaTransform n (∑ k ∈ Finset.range (n + 1), C (h k) * refined n k ∅ (Finset.range (n - 1))) := by rw [sum_C_mul_refined_eq] - set b : Finset ℕ → ℝ := fun D => ∑ k ∈ Finset.range (n + 1), h k * (desCount n k D : ℝ) - with hb + set b : Finset ℕ → ℝ := + (fun D => ∑ k ∈ Finset.range (n + 1), h k * (desCount n k D : ℝ)) with hb rw [← sum_isolatedSubsets_eq_gammaTransform b (fun D hD => card_le_of_mem_isolatedSubsets_range_pred hD)] unfold chowOfFlagH @@ -315,8 +295,8 @@ theorem augChowOfFlagH_eq_gammaTransform {n : ℕ} {h : ℕ → ℝ} {β : Finse augChowOfFlagH n β = gammaTransform (n + 1) (∑ k ∈ Finset.range (n + 1), C (h k) * refined n k ∅ (Finset.range n)) := by rw [sum_C_mul_refined_eq] - set b : Finset ℕ → ℝ := fun D => ∑ k ∈ Finset.range (n + 1), h k * (desCount n k D : ℝ) - with hb + set b : Finset ℕ → ℝ := + (fun D => ∑ k ∈ Finset.range (n + 1), h k * (desCount n k D : ℝ)) with hb rw [← sum_isolatedSubsets_eq_gammaTransform b (fun D hD => card_le_of_mem_isolatedSubsets_range hD)] unfold augChowOfFlagH @@ -333,13 +313,14 @@ theorem augChowOfFlagH_eq_gammaTransform {n : ℕ} {h : ℕ → ℝ} {β : Finse /-- Hoster--Stump, Lemma 3.1 (dual Chow polynomial): the `γ`-polynomial of the Chow polynomial of the dual poset is `∑ₖ hₖ p^{[2, n]}_{n,k}`, here `refined n k ∅ (Icc 1 (n - 1))`. -/ -theorem chowOfFlagH_dualFlagH_eq_gammaTransform {n : ℕ} {h : ℕ → ℝ} {β : Finset ℕ → ℝ} +theorem chowOfFlagH_dualFlagH_eq_gammaTransform {n : ℕ} {h : ℕ → ℝ} + {β : Finset ℕ → ℝ} (hβ : IsSimplicialFlagH n h β) : chowOfFlagH n (dualFlagH n β) = gammaTransform n (∑ k ∈ Finset.range (n + 1), C (h k) * refined n k ∅ (Finset.Icc 1 (n - 1))) := by rw [sum_C_mul_refined_eq] - set b : Finset ℕ → ℝ := fun D => ∑ k ∈ Finset.range (n + 1), h k * (desCount n k D : ℝ) - with hb + set b : Finset ℕ → ℝ := + (fun D => ∑ k ∈ Finset.range (n + 1), h k * (desCount n k D : ℝ)) with hb rw [← sum_isolatedSubsets_eq_gammaTransform b (fun D hD => card_le_of_mem_isolatedSubsets_Icc hD)] unfold chowOfFlagH @@ -371,11 +352,7 @@ theorem augChowOfFlagH_dualFlagH (n : ℕ) (β : Finset ℕ → ℝ) : private lemma list_sum_range_map (f : ℕ → ℝ[X]) (m : ℕ) : ((List.range m).map f).sum = ∑ k ∈ Finset.range m, f k := by - induction m with - | zero => simp - | succ m ih => - rw [List.range_succ, List.map_append, List.sum_append, ih, Finset.sum_range_succ] - simp + induction m <;> simp_all [List.range_succ, Finset.sum_range_succ] private theorem isRealRooted_sum_C_mul_of_interl {n : ℕ} (F : ℕ → ℝ[X]) (h : ℕ → ℝ) (hh : ∀ k, 0 ≤ h k) (hnn : ∀ k, HasNonnegCoeffs (F k)) @@ -389,7 +366,7 @@ private theorem isRealRooted_sum_C_mul_of_interl {n : ℕ} (F : ℕ → ℝ[X]) have hpair : gs.Pairwise Interl := by rw [hgs, List.pairwise_map] refine (List.pairwise_lt_range : (List.range (n + 1)).Pairwise (· < ·)).imp_of_mem ?_ - intro i j hi hj hij + intro i j _ hj hij have hj' := List.mem_range.1 hj exact ((hrow i j hij (by lia)).C_mul_left_of_nonneg (hh i)).C_mul_right_of_nonneg (hh j) have hseq : IsInterlacingSeq0Nonneg gs := by @@ -400,20 +377,18 @@ private theorem isRealRooted_sum_C_mul_of_interl {n : ℕ} (F : ℕ → ℝ[X]) have hreal : ∀ f ∈ gs, f ≠ 0 → (f ≠ 0 ∧ f.Splits) := by intro f hf hf0 obtain ⟨k, hk, rfl⟩ := List.mem_map.1 hf - have hk' := List.mem_range.1 hk have hFk : F k ≠ 0 := fun h0 => hf0 (by simp [h0]) - exact ⟨hf0, Polynomial.Splits.mul (Polynomial.Splits.C _) (hsp k (by lia) hFk)⟩ - have := isRealRooted_sum_of_isInterlacingSeq0Nonneg hseq hreal (by rwa [hsum]) - rwa [hsum] at this + exact ⟨hf0, Polynomial.Splits.mul (Polynomial.Splits.C _) + (hsp k (by simpa using List.mem_range.1 hk) hFk)⟩ + simpa only [hsum] using isRealRooted_sum_of_isInterlacingSeq0Nonneg hseq hreal (by rwa [hsum]) private lemma coeff_zero_sum_C_mul_refined (n : ℕ) (h : ℕ → ℝ) (T : Finset ℕ) : (∑ k ∈ Finset.range (n + 1), C (h k) * refined n k ∅ T).coeff 0 = h 0 := by - rw [finsetSum_coeff] - simp only [coeff_C_mul, coeff_zero_refined] - simp + simp [finsetSum_coeff, coeff_zero_refined] private lemma hasNonnegCoeffs_sum_C_mul_refined (n : ℕ) {h : ℕ → ℝ} (hh : ∀ k, 0 ≤ h k) - (S T : Finset ℕ) : HasNonnegCoeffs (∑ k ∈ Finset.range (n + 1), C (h k) * refined n k S T) := + (S T : Finset ℕ) : + HasNonnegCoeffs (∑ k ∈ Finset.range (n + 1), C (h k) * refined n k S T) := hasNonnegCoeffs_finsetSum _ _ fun k _ => nonnegCoeffs_C_mul (hh k) (hasNonnegCoeffs_refined n k S T) @@ -434,9 +409,7 @@ private lemma isRealRooted_sum_C_mul_refined {n : ℕ} {T : Finset ℕ} {h : ℕ (fun k => hasNonnegCoeffs_refined n k ∅ T) hsp hrow ?_ intro hzero have := coeff_zero_sum_C_mul_refined n h T - rw [hzero, coeff_zero_eq_eval_zero] at this - simp only [eval_zero] at this - exact h0.ne this + simp_all private lemma ne_zero_splits_of_natDegree_le_one {γ : ℝ[X]} (h0 : γ.coeff 0 ≠ 0) (hdeg : γ.natDegree ≤ 1) : γ ≠ 0 ∧ γ.Splits := @@ -451,12 +424,13 @@ private lemma erase_zero_range (n : ℕ) : (Finset.range n).erase 0 = Finset.Icc theorem isRealRooted_sum_refined_range_pred {n : ℕ} {h : ℕ → ℝ} (hh : ∀ k, 0 ≤ h k) (h0 : 0 < h 0) : (∑ k ∈ Finset.range (n + 1), C (h k) * refined n k ∅ (Finset.range (n - 1))) ≠ 0 ∧ - (∑ k ∈ Finset.range (n + 1), C (h k) * refined n k ∅ (Finset.range (n - 1))).Splits := by + (∑ k ∈ Finset.range (n + 1), + C (h k) * refined n k ∅ (Finset.range (n - 1))).Splits := by rcases lt_or_ge n 2 with hn | hn - · refine ne_zero_splits_of_natDegree_le_one (by - rw [coeff_zero_sum_C_mul_refined]; exact h0.ne') ?_ - exact (natDegree_sum_C_mul_refined_le n h - (fun D hD => card_le_of_mem_isolatedSubsets_range_pred hD)).trans (by lia) + · exact ne_zero_splits_of_natDegree_le_one + (by rw [coeff_zero_sum_C_mul_refined]; exact h0.ne') + ((natDegree_sum_C_mul_refined_le n h fun D hD => + card_le_of_mem_isolatedSubsets_range_pred hD).trans (by lia)) · have hD := (isInterlacingDiagram_range n hn).2 exact isRealRooted_sum_C_mul_refined hh h0 (fun k hk _ => (hD.splits k hk).2.1) (fun i j hij hj => hD.mid_row i j hij hj) @@ -467,10 +441,10 @@ theorem isRealRooted_sum_refined_range {n : ℕ} {h : ℕ → ℝ} (hh : ∀ k, (∑ k ∈ Finset.range (n + 1), C (h k) * refined n k ∅ (Finset.range n)) ≠ 0 ∧ (∑ k ∈ Finset.range (n + 1), C (h k) * refined n k ∅ (Finset.range n)).Splits := by rcases lt_or_ge n 2 with hn | hn - · refine ne_zero_splits_of_natDegree_le_one (by - rw [coeff_zero_sum_C_mul_refined]; exact h0.ne') ?_ - exact (natDegree_sum_C_mul_refined_le n h - (fun D hD => card_le_of_mem_isolatedSubsets_range hD)).trans (by lia) + · exact ne_zero_splits_of_natDegree_le_one + (by rw [coeff_zero_sum_C_mul_refined]; exact h0.ne') + ((natDegree_sum_C_mul_refined_le n h fun D hD => + card_le_of_mem_isolatedSubsets_range hD).trans (by lia)) · have hD := (isInterlacingDiagram_range n hn).1 exact isRealRooted_sum_C_mul_refined hh h0 (fun k hk _ => (hD.splits k hk).2.1) (fun i j hij hj => hD.mid_row i j hij hj) @@ -479,12 +453,13 @@ theorem isRealRooted_sum_refined_range {n : ℕ} {h : ℕ → ℝ} (hh : ∀ k, theorem isRealRooted_sum_refined_Icc {n : ℕ} {h : ℕ → ℝ} (hh : ∀ k, 0 ≤ h k) (h0 : 0 < h 0) : (∑ k ∈ Finset.range (n + 1), C (h k) * refined n k ∅ (Finset.Icc 1 (n - 1))) ≠ 0 ∧ - (∑ k ∈ Finset.range (n + 1), C (h k) * refined n k ∅ (Finset.Icc 1 (n - 1))).Splits := by + (∑ k ∈ Finset.range (n + 1), + C (h k) * refined n k ∅ (Finset.Icc 1 (n - 1))).Splits := by rcases lt_or_ge n 2 with hn | hn - · refine ne_zero_splits_of_natDegree_le_one (by - rw [coeff_zero_sum_C_mul_refined]; exact h0.ne') ?_ - exact (natDegree_sum_C_mul_refined_le n h - (fun D hD => card_le_of_mem_isolatedSubsets_Icc hD)).trans (by lia) + · exact ne_zero_splits_of_natDegree_le_one + (by rw [coeff_zero_sum_C_mul_refined]; exact h0.ne') + ((natDegree_sum_C_mul_refined_le n h fun D hD => + card_le_of_mem_isolatedSubsets_Icc hD).trans (by lia)) · have hD := (isInterlacingDiagram_range n hn).1 rw [← erase_zero_range] exact isRealRooted_sum_C_mul_refined hh h0 (fun k hk => (hD.splits k hk).1) @@ -582,9 +557,7 @@ private theorem strictInterl_sum_refined_Icc_sum_refined_range_one {h : ℕ → simp [Finset.sum_range_succ, refined, add_comm] rw [e3, e2] rcases (hh 1).eq_or_lt with h1 | h1 - · rw [← h1] - simp only [map_zero, zero_mul, zero_add] - exact StrictInterl.refl (by simpa using h0.ne') (Polynomial.Splits.C _) + · simpa [← h1] using StrictInterl.refl (by simpa using h0.ne') (Polynomial.Splits.C _) · have hdeg : (C (h 1) * X + C (h 0)).natDegree = 1 := natDegree_linear h1.ne' have := ((interlaces_one_linear hdeg).toStrictInterl).C_mul_left h0.ne' simpa using this @@ -596,13 +569,13 @@ poset interlace the roots of the augmented Chow polynomial, that is, Since `augChowOfFlagH n (dualFlagH n β) = augChowOfFlagH n β` (`augChowOfFlagH_dualFlagH`), this is the paper's statement for `P̂^*`. -/ theorem strictInterl_chowOfFlagH_dualFlagH_augChowOfFlagH {n : ℕ} (hn : 1 ≤ n) {h : ℕ → ℝ} - {β : Finset ℕ → ℝ} (hh : ∀ k, 0 ≤ h k) (h0 : 0 < h 0) (hβ : IsSimplicialFlagH n h β) : + {β : Finset ℕ → ℝ} (hh : ∀ k, 0 ≤ h k) (h0 : 0 < h 0) + (hβ : IsSimplicialFlagH n h β) : StrictInterl (chowOfFlagH n (dualFlagH n β)) (augChowOfFlagH n β) := by rw [chowOfFlagH_dualFlagH_eq_gammaTransform hβ, augChowOfFlagH_eq_gammaTransform hβ] have hcoeff : ∀ T : Finset ℕ, - (∑ k ∈ Finset.range (n + 1), C (h k) * refined n k ∅ T).coeff 0 ≠ 0 := fun T => by - rw [coeff_zero_sum_C_mul_refined] - exact h0.ne' + (∑ k ∈ Finset.range (n + 1), C (h k) * refined n k ∅ T).coeff 0 ≠ 0 := + fun _ => by simpa only [coeff_zero_sum_C_mul_refined] using h0.ne' refine (strictInterl_gammaTransform_succ_iff (d := n) (natDegree_sum_C_mul_refined_le n h (fun D hD => card_le_of_mem_isolatedSubsets_Icc hD)) (natDegree_sum_C_mul_refined_le n h (fun D hD => card_le_of_mem_isolatedSubsets_range hD)) @@ -630,7 +603,8 @@ theorem isRealRooted_augChowOfFlagH_flagHOfH {n : ℕ} {h : ℕ → ℝ} (hh : isRealRooted_augChowOfFlagH hh h0 (isSimplicialFlagH_flagHOfH n h) /-- Theorem 1.2 (dual Chow polynomial) for the flag `h`-vector `flagHOfH n h` of (1.3). -/ -theorem isRealRooted_chowOfFlagH_dualFlagH_flagHOfH {n : ℕ} {h : ℕ → ℝ} (hh : ∀ k, 0 ≤ h k) +theorem isRealRooted_chowOfFlagH_dualFlagH_flagHOfH {n : ℕ} {h : ℕ → ℝ} + (hh : ∀ k, 0 ≤ h k) (h0 : 0 < h 0) : chowOfFlagH n (dualFlagH n (flagHOfH n h)) ≠ 0 ∧ (chowOfFlagH n (dualFlagH n (flagHOfH n h))).Splits := @@ -664,13 +638,10 @@ private lemma reflectSet_two_pair : reflectSet 2 {0, 1} = {0, 1} := by decide +k private lemma flagH_two : flagHOfH 2 exampleH ∅ = 1 ∧ flagHOfH 2 exampleH {0} = 3 ∧ flagHOfH 2 exampleH {1} = 5 ∧ flagHOfH 2 exampleH {0, 1} = 3 := by obtain ⟨a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12⟩ := desCount_two - refine ⟨?_, ?_, ?_, ?_⟩ - · simp [flagHOfH, Finset.sum_range_succ, exampleH, reflectSet, a1, a5, a9] - · simp [flagHOfH, Finset.sum_range_succ, exampleH, reflectSet_two_zero, a2, a6, a10] - norm_num - · simp [flagHOfH, Finset.sum_range_succ, exampleH, reflectSet_two_one, a3, a7, a11] - norm_num - · simp [flagHOfH, Finset.sum_range_succ, exampleH, reflectSet_two_pair, a4, a8, a12] + refine ⟨by simp [flagHOfH, Finset.sum_range_succ, exampleH, reflectSet, a1, a5, a9], + by norm_num [flagHOfH, Finset.sum_range_succ, exampleH, reflectSet_two_zero, a2, a6, a10], + by norm_num [flagHOfH, Finset.sum_range_succ, exampleH, reflectSet_two_one, a3, a7, a11], + by simp [flagHOfH, Finset.sum_range_succ, exampleH, reflectSet_two_pair, a4, a8, a12]⟩ private lemma isolatedSubsets_Icc_two : isolatedSubsets (Finset.Icc 1 (2 - 1)) = {∅, {1}} := by decide +kernel @@ -682,26 +653,24 @@ private lemma isolatedSubsets_range_two : isolatedSubsets (Finset.range 2) = { example : chowOfFlagH 2 (flagHOfH 2 exampleH) = X ^ 2 + 7 * X + 1 := by obtain ⟨b0, b1, b2, b3⟩ := flagH_two rw [chowOfFlagH, isolatedSubsets_Icc_two, Finset.sum_pair (by decide), b0, b2] - simp [map_ofNat] - ring + simp [map_ofNat]; ring /-- Example 1.3: `H_{P̂^*}(x) = x² + 5x + 1`. -/ example : chowOfFlagH 2 (dualFlagH 2 (flagHOfH 2 exampleH)) = X ^ 2 + 5 * X + 1 := by obtain ⟨b0, b1, b2, b3⟩ := flagH_two rw [chowOfFlagH, isolatedSubsets_Icc_two, Finset.sum_pair (by decide)] - simp [dualFlagH, reflectSet, b0, b1, map_ofNat] - ring + simp [dualFlagH, reflectSet, b0, b1, map_ofNat]; ring /-- Example 1.3: `H^{aug}_{P̂}(x) = x³ + 11x² + 11x + 1`. -/ example : augChowOfFlagH 2 (flagHOfH 2 exampleH) = X ^ 3 + 11 * X ^ 2 + 11 * X + 1 := by obtain ⟨b0, b1, b2, b3⟩ := flagH_two rw [augChowOfFlagH, isolatedSubsets_range_two, Finset.sum_insert (by decide), Finset.sum_pair (by decide)] - simp [b0, b1, b2, map_ofNat] - ring + simp [b0, b1, b2, map_ofNat]; ring /-- Example 3.2: the `γ`-polynomials `1 + 5x`, `1 + 3x` and `1 + 8x`. -/ -example : (∑ k ∈ Finset.range (2 + 1), C (exampleH k) * refined 2 k ∅ (Finset.range (2 - 1))) = +example : (∑ k ∈ Finset.range (2 + 1), + C (exampleH k) * refined 2 k ∅ (Finset.range (2 - 1))) = 1 + 5 * X ∧ (∑ k ∈ Finset.range (2 + 1), C (exampleH k) * refined 2 k ∅ (Finset.Icc 1 (2 - 1))) = 1 + 3 * X ∧ diff --git a/RealRooted/ThresholdMatrix/GustafssonSolus.lean b/RealRooted/ThresholdMatrix/GustafssonSolus.lean index 929223589..f9d1cc9fc 100644 --- a/RealRooted/ThresholdMatrix/GustafssonSolus.lean +++ b/RealRooted/ThresholdMatrix/GustafssonSolus.lean @@ -20,22 +20,14 @@ namespace GustafssonSolus /-! ### Finite-entry shape helpers -/ private def GS2x2EntryShape (a b c d : ℝ[X]) : Prop := - Threshold2x2EntryTuple a b c d 0 0 0 0 ∨ - Threshold2x2EntryTuple a b c d 0 0 X X ∨ - Threshold2x2EntryTuple a b c d 0 1 0 1 ∨ - Threshold2x2EntryTuple a b c d 0 1 X 0 ∨ - Threshold2x2EntryTuple a b c d 0 1 X 1 ∨ - Threshold2x2EntryTuple a b c d 0 1 X X ∨ - Threshold2x2EntryTuple a b c d 1 1 0 0 ∨ - Threshold2x2EntryTuple a b c d 1 1 0 1 ∨ - Threshold2x2EntryTuple a b c d 1 1 1 1 ∨ - Threshold2x2EntryTuple a b c d 1 1 X 0 ∨ - Threshold2x2EntryTuple a b c d 1 1 X 1 ∨ - Threshold2x2EntryTuple a b c d 1 1 X X ∨ - Threshold2x2EntryTuple a b c d X 0 X 0 ∨ - Threshold2x2EntryTuple a b c d X 0 X X ∨ - Threshold2x2EntryTuple a b c d X 1 X 0 ∨ - Threshold2x2EntryTuple a b c d X 1 X 1 ∨ + Threshold2x2EntryTuple a b c d 0 0 0 0 ∨ Threshold2x2EntryTuple a b c d 0 0 X X ∨ + Threshold2x2EntryTuple a b c d 0 1 0 1 ∨ Threshold2x2EntryTuple a b c d 0 1 X 0 ∨ + Threshold2x2EntryTuple a b c d 0 1 X 1 ∨ Threshold2x2EntryTuple a b c d 0 1 X X ∨ + Threshold2x2EntryTuple a b c d 1 1 0 0 ∨ Threshold2x2EntryTuple a b c d 1 1 0 1 ∨ + Threshold2x2EntryTuple a b c d 1 1 1 1 ∨ Threshold2x2EntryTuple a b c d 1 1 X 0 ∨ + Threshold2x2EntryTuple a b c d 1 1 X 1 ∨ Threshold2x2EntryTuple a b c d 1 1 X X ∨ + Threshold2x2EntryTuple a b c d X 0 X 0 ∨ Threshold2x2EntryTuple a b c d X 0 X X ∨ + Threshold2x2EntryTuple a b c d X 1 X 0 ∨ Threshold2x2EntryTuple a b c d X 1 X 1 ∨ Threshold2x2EntryTuple a b c d X 1 X X ∨ Threshold2x2EntryTuple a b c d X X X X @@ -65,14 +57,11 @@ private lemma GS2x2EntryShape.has2x2 {a b c d : ℝ[X]} · simpa using interl_affine_add_X_affine_mul_X_add_X hs ht · simpa using interl_affine_mul_X_add_X_self hs -private lemma gsEntry_shape - {t₁ t₂ j₁ j₂ : ℕ} {α₁ α₂ : ℝ[X]} - (hα₁ : α₁ = 0 ∨ α₁ = 1) - (hα₂ : α₂ = 0 ∨ α₂ = 1) +private lemma gsEntry_shape {t₁ t₂ j₁ j₂ : ℕ} {α₁ α₂ : ℝ[X]} + (hα₁ : α₁ = 0 ∨ α₁ = 1) (hα₂ : α₂ = 0 ∨ α₂ = 1) (ht : t₁ ≤ t₂) (hj : j₁ ≤ j₂) (hcompat : t₁ = t₂ → α₁ = 0 → α₂ = 0) : - GS2x2EntryShape - (thresholdEntry t₁ α₁ j₁) (thresholdEntry t₁ α₁ j₂) + GS2x2EntryShape (thresholdEntry t₁ α₁ j₁) (thresholdEntry t₁ α₁ j₂) (thresholdEntry t₂ α₂ j₁) (thresholdEntry t₂ α₂ j₂) := by rcases hα₁ with rfl | rfl <;> rcases hα₂ with rfl | rfl <;> simp at hcompat <;> @@ -152,21 +141,16 @@ lemma choiceRows_rowData {choices : List (ℕ × Bool)} dsimp only [choiceRows] at i j ⊢ let i' : Fin choices.length := ⟨i.1, by simpa using i.2⟩ let j' : Fin choices.length := ⟨j.1, by simpa using j.2⟩ - have hij' : i' ≤ j' := hij - have hkey := hmono i' j' hij' - simpa [choiceRows, List.get_eq_getElem, i', j'] using hkey + simpa [choiceRows, List.get_eq_getElem, i', j'] using hmono i' j' hij · intro i j hij heq hdel dsimp only [choiceRows] at i j heq hdel ⊢ let i' : Fin choices.length := ⟨i.1, by simpa using i.2⟩ let j' : Fin choices.length := ⟨j.1, by simpa using j.2⟩ - have hij' : i' ≤ j' := hij have heq' : (choices.get i').1 = (choices.get j').1 := by simpa [choiceRows, List.get_eq_getElem, i', j'] using heq - have hdel_marker : choiceMarker (choices.get i').2 = 0 := by + have hdel' : (choices.get i').2 = true := choiceMarker_eq_zero.mp <| by simpa [choiceRows, List.get_eq_getElem, i'] using hdel - have hdel' : (choices.get i').2 = true := by simpa using hdel_marker - have hdelj := hdelete i' j' hij' heq' hdel' - simpa [choiceRows, List.get_eq_getElem, j', hdelj] + simpa [choiceRows, List.get_eq_getElem, j'] using hdelete i' j' hij heq' hdel' lemma delete_eq_true_of_local {choices : List (ℕ × Bool)} (hmono : ∀ i j : Fin choices.length, i ≤ j → (choices.get i).1 ≤ (choices.get j).1) @@ -183,38 +167,22 @@ lemma delete_eq_true_of_local {choices : List (ℕ × Bool)} (choices.get i).1 := by intro k hik hkj let k' : Fin choices.length := ⟨k, Nat.lt_of_le_of_lt hkj j.2⟩ - have hik' : i ≤ k' := hik - have hkj' : k' ≤ j := hkj - have hle1 : (choices.get i).1 ≤ (choices.get k').1 := hmono i k' hik' - have hle2 : (choices.get k').1 ≤ (choices.get i).1 := by - have hkj_le : (choices.get k').1 ≤ (choices.get j).1 := hmono k' j hkj' - rw [← heq] at hkj_le - exact hkj_le - exact le_antisymm hle2 hle1 + apply le_antisymm + · simpa only [heq] using hmono k' j hkj + · exact hmono i k' hik have hmain := Nat.le_induction (m := i.1) (P := fun n _ => ∀ hnj : n ≤ j.1, (choices.get ⟨n, Nat.lt_of_le_of_lt hnj j.2⟩).2 = true) - (by - intro _ - simpa using hdel) + (by intro _; simpa using hdel) (by intro n hin ih hsuccj have hnle : n ≤ j.1 := Nat.le_of_succ_le hsuccj have hsucc_len : n + 1 < choices.length := Nat.lt_of_le_of_lt hsuccj j.2 have hdeln : (choices.get ⟨n, Nat.lt_of_le_of_lt hnle j.2⟩).2 = true := ih hnle - have heq_step : - (choices.get ⟨n, Nat.lt_trans (Nat.lt_succ_self n) hsucc_len⟩).1 = - (choices.get ⟨n + 1, hsucc_len⟩).1 := by - have hn_eq := hconst n hin hnle - have hisucc : i.1 ≤ n + 1 := Nat.le_trans hin (Nat.le_succ n) - have hsucc_eq := hconst (n + 1) hisucc hsuccj - simpa using hn_eq.trans hsucc_eq.symm - have hdeln' : - (choices.get ⟨n, Nat.lt_trans (Nat.lt_succ_self n) hsucc_len⟩).2 = - true := by - simpa using hdeln - exact hlocal n hsucc_len heq_step hdeln') + have heq_step := + (hconst n hin hnle).trans (hconst (n + 1) (by lia) hsuccj).symm + exact hlocal n hsucc_len (by simpa using heq_step) (by simpa using hdeln)) j.1 hij simpa using hmain le_rfl @@ -403,26 +371,12 @@ private lemma fin_mono_of_adjacent {m : ℕ} {phi : Fin (m + 1) → ℕ} intro i j hij have hmain := Nat.le_induction (m := i.1) (P := fun n _ => ∀ hn : n < m + 1, phi i ≤ phi ⟨n, hn⟩) - (by - intro hn - have hidx : (⟨i.1, hn⟩ : Fin (m + 1)) = i := by ext; rfl - simp [hidx]) + (by intro hn; simp) (by intro n hin ih hsucc - have hn : n < m + 1 := Nat.lt_of_succ_lt hsucc - have hn_m : n < m := by lia - have hle := ih hn - have hstepn := hstep ⟨n, hn_m⟩ - have hleft : (⟨n, hn_m⟩ : Fin m).castSucc = - (⟨n, hn⟩ : Fin (m + 1)) := by - ext - rfl - have hright : (⟨n, hn_m⟩ : Fin m).succ = - (⟨n + 1, hsucc⟩ : Fin (m + 1)) := by - ext - rfl - rw [hleft, hright] at hstepn - exact le_trans hle hstepn) + have hs := hstep ⟨n, by lia⟩ + change phi ⟨n, _⟩ ≤ phi ⟨n + 1, _⟩ at hs + exact (ih (by lia)).trans hs) j.1 hij exact hmain j.2 @@ -433,17 +387,9 @@ private lemma finChoices_mono_of_adjacent {m : ℕ} ((finChoices m phi delete).get i).1 ≤ ((finChoices m phi delete).get j).1 := by intro i j hij - have hi := get_finChoices m phi delete i - have hj := get_finChoices m phi delete j - let i' : Fin (m + 1) := Fin.cast (length_finChoices m phi delete) i - let j' : Fin (m + 1) := Fin.cast (length_finChoices m phi delete) j - have hij' : i' ≤ j' := hij - have hmonoFin : phi i' ≤ phi j' := - fin_mono_of_adjacent hphi i' j' hij' - calc - ((finChoices m phi delete).get i).1 = phi i' := by rw [hi] - _ ≤ phi j' := hmonoFin - _ = ((finChoices m phi delete).get j).1 := by rw [hj] + simpa only [get_finChoices] using fin_mono_of_adjacent hphi + (Fin.cast (length_finChoices m phi delete) i) + (Fin.cast (length_finChoices m phi delete) j) hij private lemma finChoices_local_of_fin {m : ℕ} {phi : Fin (m + 1) → ℕ} {delete : Fin (m + 1) → Bool} @@ -459,27 +405,18 @@ private lemma finChoices_local_of_fin {m : ℕ} intro n hn heq hdel have hn_m : n < m := by simpa [length_finChoices] using hn let i : Fin m := ⟨n, hn_m⟩ - have hleft : (i.castSucc : Fin (m + 1)) = - Fin.cast (length_finChoices m phi delete) - ⟨n, Nat.lt_trans (Nat.lt_succ_self n) hn⟩ := by - ext - rfl + have hleft : (i.castSucc : Fin (m + 1)) = Fin.cast (length_finChoices m phi delete) + ⟨n, Nat.lt_trans (Nat.lt_succ_self n) hn⟩ := Fin.ext rfl have hright : (i.succ : Fin (m + 1)) = - Fin.cast (length_finChoices m phi delete) ⟨n + 1, hn⟩ := by - ext - rfl - have hget_left := get_finChoices m phi delete - ⟨n, Nat.lt_trans (Nat.lt_succ_self n) hn⟩ - have hget_right := get_finChoices m phi delete ⟨n + 1, hn⟩ - have heq' : phi i.castSucc = phi i.succ := by - rw [hget_left, hget_right] at heq - rwa [hleft, hright] - have hdel' : delete i.castSucc = true := by - rw [hget_left] at hdel - rwa [hleft] - have hnext := hlocal i heq' hdel' - rw [hget_right] - rwa [hright] at hnext + Fin.cast (length_finChoices m phi delete) ⟨n + 1, hn⟩ := Fin.ext rfl + have heq' : phi (⟨n, hn_m⟩ : Fin m).castSucc = phi (⟨n, hn_m⟩ : Fin m).succ := by + rw [get_finChoices, get_finChoices, ← hleft, ← hright] at heq + exact heq + have hdel' : delete (⟨n, hn_m⟩ : Fin m).castSucc = true := by + rw [get_finChoices, ← hleft] at hdel + exact hdel + rw [get_finChoices, ← hright] + exact hlocal ⟨n, hn_m⟩ heq' hdel' /-- Gustafsson--Solus Lemma 3.4 in finite-indexed row-choice form. @@ -583,11 +520,9 @@ theorem isInterlacingSeq0Nonneg_rowPolynomials delete i.castSucc = true → delete i.succ = true) (fs : List ℝ[X]) (hfs_len : fs.length = q) (hfs : IsInterlacingSeqNonneg fs) : - IsInterlacingSeq0Nonneg (rowPolynomials q m phi delete fs) := - by - simpa using - GustafssonSolus.isInterlacingSeq0Nonneg_choiceMatrix_finChoices - phi delete hphi hlocal fs hfs_len hfs + IsInterlacingSeq0Nonneg (rowPolynomials q m phi delete fs) := by + simpa using GustafssonSolus.isInterlacingSeq0Nonneg_choiceMatrix_finChoices + phi delete hphi hlocal fs hfs_len hfs /-- Real-rootedness projection of the paper-shaped Gustafsson--Solus polynomial-list recursion. -/ @@ -598,11 +533,9 @@ theorem realRooted_of_mem_rowPolynomials delete i.castSucc = true → delete i.succ = true) (fs : List ℝ[X]) (hfs_len : fs.length = q) (hfs : IsInterlacingSeqNonneg fs) : - ∀ f ∈ rowPolynomials q m phi delete fs, f ≠ 0 → (f ≠ 0 ∧ f.Splits) := - by - simpa using - realRooted_of_mem_choiceMatrix_finChoices - phi delete hphi hlocal fs hfs_len hfs + ∀ f ∈ rowPolynomials q m phi delete fs, f ≠ 0 → (f ≠ 0 ∧ f.Splits) := by + simpa using realRooted_of_mem_choiceMatrix_finChoices + phi delete hphi hlocal fs hfs_len hfs end GustafssonSolus