diff --git a/LeanPool/Chudnovsky/Basic.lean b/LeanPool/Chudnovsky/Basic.lean index d2cdcfe305..311a7c8b9a 100644 --- a/LeanPool/Chudnovsky/Basic.lean +++ b/LeanPool/Chudnovsky/Basic.lean @@ -56,11 +56,11 @@ def Lτ (τ : ℍ) : PeriodPair where def q (τ : ℍ) : ℂ := Function.Periodic.qParam 1 τ lemma q_eq (τ : ℍ) : q τ = Complex.exp (2 * π * Complex.I * τ) := by - simp [q, Function.Periodic.qParam] + simp only [q, Function.Periodic.qParam, ofReal_one, div_one] lemma norm_q (τ : ℍ) : ‖q τ‖ = Real.exp (-(2 * π * τ.im)) := by rw [q, Function.Periodic.norm_qParam] - simp [coe_im] + simp only [neg_mul, coe_im, div_one] lemma norm_q_lt_one (τ : ℍ) : ‖q τ‖ < 1 := by rw [norm_q, Real.exp_lt_one_iff, neg_lt_zero] @@ -118,10 +118,10 @@ def Region : Set ℍ := {τ : ℍ | 5 / 4 < τ.im} lemma τ₁₆₃_mem_Region : τ₁₆₃ ∈ Region := by simp only [Region, Set.mem_ofPred_eq, τ₁₆₃_im] - nlinarith [Real.sq_sqrt (by norm_num : (163 : ℝ) ≥ 0).le, Real.sqrt_nonneg (163 : ℝ)] + nlinarith only [Real.sq_sqrt (by norm_num : (163 : ℝ) ≥ 0).le, Real.sqrt_nonneg (163 : ℝ)] lemma τ₈_mem_Region : τ₈ ∈ Region := by simp only [Region, Set.mem_ofPred_eq, τ₈_im] - nlinarith [Real.sq_sqrt (by norm_num : (2 : ℝ) ≥ 0).le, Real.sqrt_nonneg (2 : ℝ)] + nlinarith only [Real.sq_sqrt (by norm_num : (2 : ℝ) ≥ 0).le, Real.sqrt_nonneg (2 : ℝ)] end Chudnovsky diff --git a/LeanPool/Chudnovsky/BernoulliValues.lean b/LeanPool/Chudnovsky/BernoulliValues.lean index f7c86a2229..eca6bdecd8 100644 --- a/LeanPool/Chudnovsky/BernoulliValues.lean +++ b/LeanPool/Chudnovsky/BernoulliValues.lean @@ -25,15 +25,15 @@ lemma bernoulli_four_value : bernoulli 4 = -1 / 30 := by /-- The sixth Bernoulli number, evaluated from the preceding values. -/ lemma bernoulli_six_value : bernoulli 6 = 1 / 42 := by - have h5 : bernoulli' 5 = 0 := bernoulli'_eq_zero_of_odd ⟨2, rfl⟩ (by norm_num) + have h5 : bernoulli' 5 = 0 := bernoulli'_eq_zero_of_odd ⟨2, rfl⟩ (by norm_num1) have h6 : bernoulli' 6 = 1 / 42 := by rw [bernoulli'_def] rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_zero, bernoulli'_zero, bernoulli'_one, bernoulli'_two, bernoulli'_three, bernoulli'_four, h5] - norm_num [Nat.choose] + norm_num only [Nat.choose] rw [bernoulli, h6] - norm_num + norm_num1 end Chudnovsky diff --git a/LeanPool/Chudnovsky/Clausen.lean b/LeanPool/Chudnovsky/Clausen.lean index 1318e54138..64e0f29a2f 100644 --- a/LeanPool/Chudnovsky/Clausen.lean +++ b/LeanPool/Chudnovsky/Clausen.lean @@ -107,8 +107,8 @@ theorem generalizedHypergeometricSeries_apply_zero (n : ℕ) : @[simp] theorem generalizedHypergeometric_zero : ₃F₂ α β γ δ ε (0 : 𝔸) = 1 := by - simp [generalizedHypergeometric_eq_tsum, ← generalizedHypergeometricSeries_apply_eq, - generalizedHypergeometricSeries_apply_zero] + simp only [generalizedHypergeometric_eq_tsum, ← generalizedHypergeometricSeries_apply_eq, + generalizedHypergeometricSeries_apply_zero, tsum_pi_single] end Field @@ -130,10 +130,7 @@ theorem generalizedHypergeometricSeries_radius_eq_one {𝕂 : Type*} (𝔸 : Typ rw [ascPochhammer_eval_eq_zero_iff] at hz obtain ⟨k, _, hk⟩ := hz exact hx k hk - have hxn : ∀ (x : 𝕂) (n : ℕ), (∀ kn : ℕ, (kn : 𝕂) ≠ -x) → x + (n : 𝕂) ≠ 0 := by - intro x n hx he - rw [add_comm] at he - exact hx n (eq_neg_of_add_eq_zero_left he) + -- Cancel the old coefficient factors before taking norms. have key : ∀ n : ℕ, generalizedHypergeometricCoefficient α β γ δ ε n / generalizedHypergeometricCoefficient α β γ δ ε (n + 1) = ((δ + n) * (ε + n) * (1 + n)) / ((α + n) * (β + n) * (γ + n)) := by @@ -143,54 +140,37 @@ theorem generalizedHypergeometricSeries_radius_eq_one {𝕂 : Type*} (𝔸 : Typ have hγ := hpne γ n fun k => (h k).2.2.1 have hδ := hpne δ n fun k => (h k).2.2.2.1 have hε := hpne ε n fun k => (h k).2.2.2.2 - have hαn := hxn α n fun k => (h k).1 - have hβn := hxn β n fun k => (h k).2.1 - have hγn := hxn γ n fun k => (h k).2.2.1 - have hδn := hxn δ n fun k => (h k).2.2.2.1 - have hεn := hxn ε n fun k => (h k).2.2.2.2 - have hfac : ((n ! : 𝕂)) ≠ 0 := Nat.cast_ne_zero.2 (Nat.factorial_ne_zero n) - have hn1 : ((n : 𝕂) + 1) ≠ 0 := Nat.cast_add_one_ne_zero n - have hden : (α + (n : 𝕂)) * (β + n) * (γ + n) ≠ 0 := - mul_ne_zero (mul_ne_zero hαn hβn) hγn - have hcn1 : generalizedHypergeometricCoefficient α β γ δ ε (n + 1) ≠ 0 := by - simp only [generalizedHypergeometricCoefficient] - refine mul_ne_zero (mul_ne_zero (mul_ne_zero (mul_ne_zero (mul_ne_zero ?_ ?_) ?_) ?_) ?_) ?_ - · exact inv_ne_zero (Nat.cast_ne_zero.2 (Nat.factorial_ne_zero _)) - · exact hpne α (n + 1) fun k => (h k).1 - · exact hpne β (n + 1) fun k => (h k).2.1 - · exact hpne γ (n + 1) fun k => (h k).2.2.1 - · exact inv_ne_zero (hpne δ (n + 1) fun k => (h k).2.2.2.1) - · exact inv_ne_zero (hpne ε (n + 1) fun k => (h k).2.2.2.2) - have hrec : generalizedHypergeometricCoefficient α β γ δ ε n * - ((α + (n : 𝕂)) * (β + n) * (γ + n)) = - generalizedHypergeometricCoefficient α β γ δ ε (n + 1) * - ((δ + (n : 𝕂)) * (ε + n) * (1 + n)) := by - simp only [generalizedHypergeometricCoefficient, Nat.factorial_succ, ascPochhammer_succ_eval, - Nat.cast_mul, Nat.cast_succ] - field_simp - ring - exact (div_eq_div_iff hcn1 hden).mpr (hrec.trans (mul_comm _ _)) + have hfac : (n ! : 𝕂) ≠ 0 := Nat.cast_ne_zero.2 (Nat.factorial_ne_zero n) + simp only [generalizedHypergeometricCoefficient, Nat.factorial_succ, + ascPochhammer_succ_eval, Nat.cast_mul, Nat.cast_succ, + div_eq_mul_inv, mul_inv_rev, inv_inv, add_comm (1 : 𝕂) (n : 𝕂)] + calc + _ = ((n ! : 𝕂) * (n ! : 𝕂)⁻¹) + * ((ascPochhammer 𝕂 n).eval α * ((ascPochhammer 𝕂 n).eval α)⁻¹) + * ((ascPochhammer 𝕂 n).eval β * ((ascPochhammer 𝕂 n).eval β)⁻¹) + * ((ascPochhammer 𝕂 n).eval γ * ((ascPochhammer 𝕂 n).eval γ)⁻¹) + * ((ascPochhammer 𝕂 n).eval δ * ((ascPochhammer 𝕂 n).eval δ)⁻¹) + * ((ascPochhammer 𝕂 n).eval ε * ((ascPochhammer 𝕂 n).eval ε)⁻¹) + * ((α + n)⁻¹ * (β + n)⁻¹ * (γ + n)⁻¹ + * (δ + n) * (ε + n) * ((n : 𝕂) + 1)) := by ring + _ = _ := by + rw [mul_inv_cancel₀ hfac, mul_inv_cancel₀ hα, mul_inv_cancel₀ hβ, + mul_inv_cancel₀ hγ, mul_inv_cancel₀ hδ, mul_inv_cancel₀ hε] + simp only [one_mul, mul_one] + ring have limit : Tendsto (fun n : ℕ => ((δ + n) * (ε + n) * (1 + n)) / ((α + n) * (β + n) * (γ + n))) atTop (𝓝 1) := by - have h1 : Tendsto (fun n : ℕ => (δ + (n : 𝕂)) / (α + n)) atTop (𝓝 1) := by - simpa using tendsto_add_mul_div_add_mul_atTop_nhds δ α (1 : 𝕂) (d := 1) one_ne_zero - have h2 : Tendsto (fun n : ℕ => (ε + (n : 𝕂)) / (β + n)) atTop (𝓝 1) := by - simpa using tendsto_add_mul_div_add_mul_atTop_nhds ε β (1 : 𝕂) (d := 1) one_ne_zero - have h3 : Tendsto (fun n : ℕ => (1 + (n : 𝕂)) / (γ + n)) atTop (𝓝 1) := by - simpa using tendsto_add_mul_div_add_mul_atTop_nhds (1 : 𝕂) γ (1 : 𝕂) (d := 1) one_ne_zero - have heq : (fun n : ℕ => ((δ + (n : 𝕂)) * (ε + n) * (1 + n)) / ((α + n) * (β + n) * (γ + n))) - = fun n : ℕ => (δ + (n : 𝕂)) / (α + n) * ((ε + n) / (β + n)) * ((1 + n) / (γ + n)) := by - funext n - simp only [div_eq_mul_inv, mul_inv_rev] - ring - rw [heq] - simpa using (h1.mul h2).mul h3 + have linear_limit (x y : 𝕂) : + Tendsto (fun n : ℕ => (x + (n : 𝕂)) / (y + n)) atTop (𝓝 1) := by + simpa only [one_mul, div_one] using + tendsto_add_mul_div_add_mul_atTop_nhds x y (1 : 𝕂) (d := 1) one_ne_zero + simpa only [@div_mul_div_comm 𝕂 _, mul_one] using + ((linear_limit δ α).mul (linear_limit ε β)).mul (linear_limit 1 γ) have limitn : Tendsto (fun n : ℕ => ‖((δ + (n : 𝕂)) * (ε + n) * (1 + n)) / ((α + n) * (β + n) * (γ + n))‖) - atTop (𝓝 1) := by simpa using Filter.Tendsto.norm limit + atTop (𝓝 1) := by simpa only [norm_one] using Filter.Tendsto.norm limit refine limitn.congr (fun n => ?_) - simp only [Nat.succ_eq_add_one] rw [← norm_div, key n] open Filter Topology in @@ -228,19 +208,19 @@ theorem generalizedHypergeometric_summable (α β γ δ ε : ℂ) {z : ℂ} (hz all_goals first | (rw [show (ascPochhammer ℂ n).eval α = 0 by - rw [show α = -(kn : ℂ) by linear_combination hp] + rw [show α = -(kn : ℂ) by exact neg_eq_iff_eq_neg.mp hp.symm] exact ascPochhammer_eval_neg_coe_nat_of_lt hlt]; simp) | (rw [show (ascPochhammer ℂ n).eval β = 0 by - rw [show β = -(kn : ℂ) by linear_combination hp] + rw [show β = -(kn : ℂ) by exact neg_eq_iff_eq_neg.mp hp.symm] exact ascPochhammer_eval_neg_coe_nat_of_lt hlt]; simp) | (rw [show (ascPochhammer ℂ n).eval γ = 0 by - rw [show γ = -(kn : ℂ) by linear_combination hp] + rw [show γ = -(kn : ℂ) by exact neg_eq_iff_eq_neg.mp hp.symm] exact ascPochhammer_eval_neg_coe_nat_of_lt hlt]; simp) | (rw [show (ascPochhammer ℂ n).eval δ = 0 by - rw [show δ = -(kn : ℂ) by linear_combination hp] + rw [show δ = -(kn : ℂ) by exact neg_eq_iff_eq_neg.mp hp.symm] exact ascPochhammer_eval_neg_coe_nat_of_lt hlt]; simp) | (rw [show (ascPochhammer ℂ n).eval ε = 0 by - rw [show ε = -(kn : ℂ) by linear_combination hp] + rw [show ε = -(kn : ℂ) by exact neg_eq_iff_eq_neg.mp hp.symm] exact ascPochhammer_eval_neg_coe_nat_of_lt hlt]; simp) rw [hc0, zero_mul] @@ -291,7 +271,7 @@ private theorem DiscSummable.shift {c : ℕ → ℂ} (hc : DiscSummable c) : have hρ0 : 0 ≤ ρ := (norm_nonneg w).trans hwρ.le have hρpos : 0 < ρ := lt_of_le_of_lt (norm_nonneg w) hwρ have hg : Summable fun m : ℕ => (m : ℝ) * ‖c m‖ * ρ ^ m := by - simpa using hc.weighted 1 hρ0 hρ1 + simpa only [pow_one] using hc.weighted 1 hρ0 hρ1 have hg1 : Summable fun n : ℕ => ((n + 1 : ℕ) : ℝ) * ‖c (n + 1)‖ * ρ ^ (n + 1) := (summable_nat_add_iff (f := fun m : ℕ => (m : ℝ) * ‖c m‖ * ρ ^ m) 1).2 hg have hbnd : Summable fun n : ℕ => ((n : ℝ) + 1) * ‖c (n + 1)‖ * ρ ^ n := by @@ -393,7 +373,7 @@ private theorem ordinaryHypergeometric_discSummable (a b c : ℂ) (hc : ∀ k : have hkn' : (kn : ℂ) = -a ∨ (kn : ℂ) = -b := by by_contra hcon push Not at hcon - exact absurd (hkn hcon.1) (by simpa using hcon.2) + exact absurd (hkn hcon.1) (by simpa only [ne_eq] using hcon.2) apply summable_of_ne_finset_zero (s := Finset.range (kn + 1)) intro n hn rw [Finset.mem_range, not_lt] at hn @@ -402,10 +382,10 @@ private theorem ordinaryHypergeometric_discSummable (a b c : ℂ) (hc : ∀ k : simp only [ordinaryHypergeometricCoefficient] rcases hkn' with hp | hp · rw [show (ascPochhammer ℂ n).eval a = 0 by - rw [show a = -(kn : ℂ) by linear_combination hp] + rw [show a = -(kn : ℂ) by exact neg_eq_iff_eq_neg.mp hp.symm] exact ascPochhammer_eval_neg_coe_nat_of_lt hlt]; ring · rw [show (ascPochhammer ℂ n).eval b = 0 by - rw [show b = -(kn : ℂ) by linear_combination hp] + rw [show b = -(kn : ℂ) by exact neg_eq_iff_eq_neg.mp hp.symm] exact ascPochhammer_eval_neg_coe_nat_of_lt hlt]; ring rw [hc0, zero_mul, norm_zero] @@ -486,7 +466,7 @@ theorem ordinaryHypergeometric_ode (a b c : ℂ) (hc : ∀ k : ℕ, (k : ℂ) have hd2 : deriv (deriv fun w : ℂ => ₂F₁ a b c w) z = ∑' n : ℕ, C2 n * z ^ n := by have hev : deriv (fun w : ℂ => ₂F₁ a b c w) =ᶠ[nhds z] fun w => ∑' n : ℕ, C1 n * w ^ n := by have hball : Metric.ball (0 : ℂ) 1 ∈ nhds z := - Metric.isOpen_ball.mem_nhds (by simpa [Metric.mem_ball, dist_zero_right] using hz) + Metric.isOpen_ball.mem_nhds (by simpa only [Metric.mem_ball, dist_zero_right] using hz) filter_upwards [hball] with w hw rw [Metric.mem_ball, dist_zero_right] at hw exact (hHD w hw).deriv @@ -589,20 +569,21 @@ private theorem generalizedHypergeometric_discSummable (α β γ δ ε : ℂ) : all_goals first | (rw [show (ascPochhammer ℂ n).eval α = 0 by - rw [show α = -(kn : ℂ) by linear_combination hp] + rw [show α = -(kn : ℂ) by exact neg_eq_iff_eq_neg.mp hp.symm] exact ascPochhammer_eval_neg_coe_nat_of_lt hlt]; ring) | (rw [show (ascPochhammer ℂ n).eval β = 0 by - rw [show β = -(kn : ℂ) by linear_combination hp] + rw [show β = -(kn : ℂ) by exact neg_eq_iff_eq_neg.mp hp.symm] exact ascPochhammer_eval_neg_coe_nat_of_lt hlt]; ring) | (rw [show (ascPochhammer ℂ n).eval γ = 0 by - rw [show γ = -(kn : ℂ) by linear_combination hp] + rw [show γ = -(kn : ℂ) by exact neg_eq_iff_eq_neg.mp hp.symm] exact ascPochhammer_eval_neg_coe_nat_of_lt hlt]; ring) | (rw [show (ascPochhammer ℂ n).eval δ = 0 by - rw [show δ = -(kn : ℂ) by linear_combination hp] - exact ascPochhammer_eval_neg_coe_nat_of_lt hlt]; simp) + rw [show δ = -(kn : ℂ) by exact neg_eq_iff_eq_neg.mp hp.symm] + exact ascPochhammer_eval_neg_coe_nat_of_lt hlt]; simp only [inv_zero, mul_zero, + zero_mul]) | (rw [show (ascPochhammer ℂ n).eval ε = 0 by - rw [show ε = -(kn : ℂ) by linear_combination hp] - exact ascPochhammer_eval_neg_coe_nat_of_lt hlt]; simp) + rw [show ε = -(kn : ℂ) by exact neg_eq_iff_eq_neg.mp hp.symm] + exact ascPochhammer_eval_neg_coe_nat_of_lt hlt]; simp only [inv_zero, mul_zero]) rw [hc0, zero_mul, norm_zero] /-- Paper Thm. `dgl3f2`: on the unit disc, `g = ₃F₂(α, β, γ; δ, ε; ·)` satisfies the third-order @@ -838,12 +819,14 @@ private theorem clausen_coeff_general (a b : ℂ) have hee2 : (∑ k ∈ Finset.range (nn + 1), C k * C (nn - k)) = E nn := rfl rw [hee1, hee2] at key linear_combination key - have ee0 : E 0 = 1 := by simp [hEdef, C0] + have ee0 : E 0 = 1 := by simp only [hEdef, zero_add, Finset.range_one, zero_tsub, C0, mul_one, + Finset.sum_singleton] have hAne : ∀ nn : ℕ, A nn ≠ 0 := by intro nn simp only [hAdef] exact mul_ne_zero (mul_ne_zero (Nat.cast_add_one_ne_zero nn) - (fun h => h₂ nn (by linear_combination h))) (fun h => h₁ nn (by linear_combination h)) + (fun h => h₂ nn (by exact eq_neg_of_add_eq_zero_left h))) + (fun h => h₁ nn (by exact eq_neg_of_add_eq_zero_left h)) have ee_eq_dd : ∀ nn : ℕ, E nn = D nn := by intro nn induction nn with @@ -1048,7 +1031,8 @@ private theorem ee_rec (n : ℕ) : ((n : ℚ) + 1) ^ 3 * ee (n + 1) = AA n * ee /-- Both coefficient sequences satisfy the same recurrence with the same initial value, hence they are equal. -/ -private theorem ee_zero : ee 0 = 1 := by simp [ee, cc_zero] +private theorem ee_zero : ee 0 = 1 := by simp only [ee, zero_add, Finset.range_one, zero_tsub, + cc_zero, mul_one, Finset.sum_singleton] private theorem ee_eq_dd (n : ℕ) : ee n = dd n := by induction n with diff --git a/LeanPool/Chudnovsky/Coefficients.lean b/LeanPool/Chudnovsky/Coefficients.lean index 5b8b1adb55..95dbd7055b 100644 --- a/LeanPool/Chudnovsky/Coefficients.lean +++ b/LeanPool/Chudnovsky/Coefficients.lean @@ -9,6 +9,7 @@ public import LeanPool.Chudnovsky.Estimates import LeanPool.Chudnovsky.ComplexMult import LeanPool.Chudnovsky.MainTheorem import LeanPool.Chudnovsky.Numerics +import LeanPool.Chudnovsky.NumericalBounds import LeanPool.Chudnovsky.SingularModuli import LeanPool.Chudnovsky.SingularModuli.CMRelations import LeanPool.Chudnovsky.SingularModuli.ModularPolynomialZ @@ -55,74 +56,7 @@ private lemma jwert_real_bound {e : ℝ} (hL : (3.80898093700765233822623151647e-18 : ℝ) < e) (hU : e < (3.80898093700765233822623151648e-18 : ℝ)) : |(1 - 240 * e + 2160 * e ^ 2) ^ 3 / (e * (1 + e - e ^ 2) ^ 24) - 640320 ^ 3| < 1 / 2 := by - -- The final tolerance is one half, so coarse rational enclosures suffice. - have hL : (3.808980937007652338e-18 : ℝ) < e := lt_trans (by norm_num) hL - have hU : e < (3.808980937007652339e-18 : ℝ) := lt_trans hU (by norm_num) - have hepos : 0 < e := lt_trans (by norm_num) hL - have he2U : e ^ 2 ≤ (3.808980937007652339e-18 : ℝ) ^ 2 := - pow_le_pow_left₀ hepos.le hU.le 2 - have he2nn : 0 ≤ e ^ 2 := sq_nonneg e - -- enclosures for `g = 1 - 240e + 2160e²` - have hGLg : (1 - 240 * 3.808980937007652339e-18 : ℝ) - ≤ 1 - 240 * e + 2160 * e ^ 2 := by linarith only [hU, he2nn] - have hgGH : 1 - 240 * e + 2160 * e ^ 2 ≤ - (1 - 240 * 3.808980937007652338e-18 - + 2160 * (3.808980937007652339e-18) ^ 2 : ℝ) := by linarith only [hL, he2U] - have hGLpos : (0 : ℝ) < 1 - 240 * 3.808980937007652339e-18 := by norm_num - have hgpos : 0 < 1 - 240 * e + 2160 * e ^ 2 := lt_of_lt_of_le hGLpos hGLg - -- enclosures for `h = 1 + e - e²` - have hHLh : (1 + 3.808980937007652338e-18 - - (3.808980937007652339e-18) ^ 2 : ℝ) ≤ 1 + e - e ^ 2 := by - linarith only [hL, he2U] - have hhHH : 1 + e - e ^ 2 ≤ (1 + 3.808980937007652339e-18 : ℝ) := by - linarith only [hU, he2nn] - have hHLpos : (0 : ℝ) < 1 + 3.808980937007652338e-18 - - (3.808980937007652339e-18) ^ 2 := by norm_num - have hhpos : 0 < 1 + e - e ^ 2 := lt_of_lt_of_le hHLpos hHLh - -- cube / 24-th power the enclosures - have hN_hi : (1 - 240 * e + 2160 * e ^ 2) ^ 3 ≤ - (1 - 240 * 3.808980937007652338e-18 - + 2160 * (3.808980937007652339e-18) ^ 2) ^ 3 := - pow_le_pow_left₀ hgpos.le hgGH 3 - have hN_lo : (1 - 240 * 3.808980937007652339e-18) ^ 3 - ≤ (1 - 240 * e + 2160 * e ^ 2) ^ 3 := pow_le_pow_left₀ hGLpos.le hGLg 3 - have hW_hi : (1 + e - e ^ 2) ^ 24 ≤ (1 + 3.808980937007652339e-18) ^ 24 := - pow_le_pow_left₀ hhpos.le hhHH 24 - have hW_lo : (1 + 3.808980937007652338e-18 - - (3.808980937007652339e-18) ^ 2) ^ 24 ≤ (1 + e - e ^ 2) ^ 24 := - pow_le_pow_left₀ hHLpos.le hHLh 24 - -- the two division enclosures of `S` - have hden_pos : 0 < e * (1 + e - e ^ 2) ^ 24 := mul_pos hepos (pow_pos hhpos 24) - have hSupper : (1 - 240 * e + 2160 * e ^ 2) ^ 3 / (e * (1 + e - e ^ 2) ^ 24) ≤ - (1 - 240 * 3.808980937007652338e-18 - + 2160 * (3.808980937007652339e-18) ^ 2) ^ 3 / - (3.808980937007652338e-18 * - (1 + 3.808980937007652338e-18 - - (3.808980937007652339e-18) ^ 2) ^ 24) := by - apply div_le_div₀ (by positivity) hN_hi - (mul_pos (by norm_num) (pow_pos hHLpos 24)) - exact mul_le_mul hL.le hW_lo (pow_nonneg hHLpos.le 24) hepos.le - have hSlower : (1 - 240 * 3.808980937007652339e-18) ^ 3 / - (3.808980937007652339e-18 * - (1 + 3.808980937007652339e-18) ^ 24) ≤ - (1 - 240 * e + 2160 * e ^ 2) ^ 3 / (e * (1 + e - e ^ 2) ^ 24) := by - apply div_le_div₀ (by positivity) hN_lo hden_pos - exact mul_le_mul hU.le hW_hi (pow_nonneg hhpos.le 24) (by norm_num) - -- the two heavy rational inequalities - have hUpNum : (1 - 240 * 3.808980937007652338e-18 - + 2160 * (3.808980937007652339e-18) ^ 2) ^ 3 / - (3.808980937007652338e-18 * - (1 + 3.808980937007652338e-18 - - (3.808980937007652339e-18) ^ 2) ^ 24) < (640320 : ℝ) ^ 3 + 1 / 2 := by - norm_num - have hLoNum : (640320 : ℝ) ^ 3 - 1 / 2 < - (1 - 240 * 3.808980937007652339e-18) ^ 3 / - (3.808980937007652339e-18 * - (1 + 3.808980937007652339e-18) ^ 24) := by - norm_num - rw [abs_lt] - exact ⟨by linarith only [hLoNum.trans_le hSlower], - by linarith only [hSupper.trans_lt hUpNum]⟩ + exact NumericalBounds.jwert_real_bound hL hU /-- Milla's `jwert2` at `N = 163`, from the integrality input `1728·J(τ₁₆₃) ∈ ℤ` as an explicit hypothesis: the singular value `1728·J(τ₁₆₃) = −640320³`. -/ @@ -202,109 +136,7 @@ private lemma s2tilde_real_bound {e pv sv : ℝ} |(1 - 240 * e + 2160 * e ^ 2) / (1 + 504 * e - 16632 * e ^ 2) * (1 + 24 * e - 72 * e ^ 2 - 3 / (pv * (sv / 2))) * 10996566783048 - 9351571368960| < 1 / 2 := by - -- The final tolerance is one half, so coarse rational enclosures suffice. - have heL : (3e-18 : ℝ) < e := lt_trans (by norm_num) heL - have heU : e < (4e-18 : ℝ) := lt_trans heU (by norm_num) - have hpL : (3.14159265358979 : ℝ) < pv := lt_trans (by norm_num) hpL - have hpU : pv < (3.14159265358980 : ℝ) := lt_trans hpU (by norm_num) - have hsL : (12.7671453348037 : ℝ) < sv := lt_trans (by norm_num) hsL - have hsU : sv < (12.7671453348038 : ℝ) := lt_trans hsU (by norm_num) - have hepos : 0 < e := lt_trans (by norm_num) heL - have hp_pos : 0 < pv := lt_trans (by norm_num) hpL - have hs_pos : 0 < sv := lt_trans (by norm_num) hsL - have hpsv : 0 < pv * (sv / 2) := by positivity - -- enclosures for `e²` - have he2U : e ^ 2 ≤ (4e-18 : ℝ) ^ 2 := - pow_le_pow_left₀ hepos.le heU.le 2 - have he2L : (3e-18 : ℝ) ^ 2 ≤ e ^ 2 := - pow_le_pow_left₀ (by norm_num) heL.le 2 - have he2nn : 0 ≤ e ^ 2 := sq_nonneg e - -- num = 1 − 240e + 2160e² - have hnumL : (1 - 240 * 4e-18 : ℝ) - ≤ 1 - 240 * e + 2160 * e ^ 2 := by linarith only [heU, he2nn] - have hnumH : 1 - 240 * e + 2160 * e ^ 2 ≤ - (1 - 240 * 3e-18 - + 2160 * (4e-18) ^ 2 : ℝ) := by linarith only [heL, he2U] - have hnumpos : 0 < 1 - 240 * e + 2160 * e ^ 2 := lt_of_lt_of_le (by norm_num) hnumL - -- den = 1 + 504e − 16632e² - have hdenL : (1 + 504 * 3e-18 - - 16632 * (4e-18) ^ 2 : ℝ) - ≤ 1 + 504 * e - 16632 * e ^ 2 := by linarith only [heL, he2U] - have hdenH : - 1 + 504 * e - 16632 * e ^ 2 ≤ (1 + 504 * 4e-18 : ℝ) := by - linarith only [heU, he2nn] - have hdenpos : 0 < 1 + 504 * e - 16632 * e ^ 2 := lt_of_lt_of_le (by norm_num) hdenL - -- w = 3/(pv·(sv/2)); `wH` (from `πL, sL`) is the max, `wL` (from `πU, sU`) the min - have hwH : 3 / (pv * (sv / 2)) - ≤ (3 / (3.14159265358979 * (12.7671453348037 / 2)) : ℝ) := - div_le_div_of_nonneg_left (by norm_num) (by positivity) - (mul_le_mul hpL.le (by linarith only [hsL]) (by norm_num) hp_pos.le) - have hwL : (3 / (3.14159265358980 * (12.7671453348038 / 2)) : ℝ) - ≤ 3 / (pv * (sv / 2)) := - div_le_div_of_nonneg_left (by norm_num) hpsv - (mul_le_mul hpU.le (by linarith only [hsU]) (by positivity) (by norm_num)) - -- Z = 1 + 24e − 72e² − w : lower bound subtracts `wH`, upper bound subtracts `wL` - have hZL : (1 + 24 * 3e-18 - - 72 * (4e-18) ^ 2 - - 3 / (3.14159265358979 * (12.7671453348037 / 2)) : ℝ) - ≤ 1 + 24 * e - 72 * e ^ 2 - 3 / (pv * (sv / 2)) := by linarith only [heL, he2U, hwH] - have hZH : 1 + 24 * e - 72 * e ^ 2 - 3 / (pv * (sv / 2)) ≤ - (1 + 24 * 4e-18 - - 72 * (3e-18) ^ 2 - - 3 / (3.14159265358980 * (12.7671453348038 / 2)) : ℝ) := by - linarith only [heU, he2L, hwL] - have hZpos : 0 < 1 + 24 * e - 72 * e ^ 2 - 3 / (pv * (sv / 2)) := - lt_of_lt_of_le (by norm_num) hZL - -- num·Z rational enclosures - have hNZlo : (1 - 240 * 4e-18) - * (1 + 24 * 3e-18 - - 72 * (4e-18) ^ 2 - - 3 / (3.14159265358979 * (12.7671453348037 / 2))) - ≤ (1 - 240 * e + 2160 * e ^ 2) * (1 + 24 * e - 72 * e ^ 2 - 3 / (pv * (sv / 2))) := - mul_le_mul hnumL hZL (by norm_num) hnumpos.le - have hNZhi : (1 - 240 * e + 2160 * e ^ 2) * (1 + 24 * e - 72 * e ^ 2 - 3 / (pv * (sv / 2))) - ≤ (1 - 240 * 3e-18 - + 2160 * (4e-18) ^ 2) - * (1 + 24 * 4e-18 - - 72 * (3e-18) ^ 2 - - 3 / (3.14159265358980 * (12.7671453348038 / 2))) := - mul_le_mul hnumH hZH hZpos.le (by norm_num) - -- rewrite the target quantity as `(num·Z)·b / den` - rw [show (1 - 240 * e + 2160 * e ^ 2) / (1 + 504 * e - 16632 * e ^ 2) - * (1 + 24 * e - 72 * e ^ 2 - 3 / (pv * (sv / 2))) * 10996566783048 - = (1 - 240 * e + 2160 * e ^ 2) * (1 + 24 * e - 72 * e ^ 2 - 3 / (pv * (sv / 2))) - * 10996566783048 / (1 + 504 * e - 16632 * e ^ 2) from by ring] - have hlo : (9351571368960 : ℝ) - 1 / 2 < - (1 - 240 * e + 2160 * e ^ 2) * (1 + 24 * e - 72 * e ^ 2 - 3 / (pv * (sv / 2))) - * 10996566783048 / (1 + 504 * e - 16632 * e ^ 2) := by - rw [lt_div_iff₀ hdenpos] - have hb := mul_le_mul_of_nonneg_right hNZlo (by norm_num : (0 : ℝ) ≤ 10996566783048) - have hD := mul_le_mul_of_nonneg_left hdenH - (by norm_num : (0 : ℝ) ≤ 9351571368960 - 1 / 2) - have hnum : (9351571368960 - 1 / 2 : ℝ) * (1 + 504 * 4e-18) - < (1 - 240 * 4e-18) - * (1 + 24 * 3e-18 - - 72 * (4e-18) ^ 2 - - 3 / (3.14159265358979 * (12.7671453348037 / 2))) - * 10996566783048 := by norm_num - exact hD.trans_lt (hnum.trans_le hb) - have hhi : (1 - 240 * e + 2160 * e ^ 2) * (1 + 24 * e - 72 * e ^ 2 - 3 / (pv * (sv / 2))) - * 10996566783048 / (1 + 504 * e - 16632 * e ^ 2) < (9351571368960 : ℝ) + 1 / 2 := by - rw [div_lt_iff₀ hdenpos] - have hb := mul_le_mul_of_nonneg_right hNZhi (by norm_num : (0 : ℝ) ≤ 10996566783048) - have hD := mul_le_mul_of_nonneg_left hdenL - (by norm_num : (0 : ℝ) ≤ 9351571368960 + 1 / 2) - have hnum : (1 - 240 * 3e-18 - + 2160 * (4e-18) ^ 2) - * (1 + 24 * 4e-18 - - 72 * (3e-18) ^ 2 - - 3 / (3.14159265358980 * (12.7671453348038 / 2))) - * 10996566783048 - < (9351571368960 + 1 / 2 : ℝ) * (1 + 504 * 3e-18 - - 16632 * (4e-18) ^ 2) := by norm_num - exact hb.trans_lt (hnum.trans_le hD) - rw [abs_lt] - exact ⟨by linarith only [hlo], by linarith only [hhi]⟩ + exact NumericalBounds.s2tilde_real_bound heL heU hpL hpU hsL hsU /-- Milla's `s2nenner`/`satzhilfszahlen` at `N = 163`, from the integrality and rationality inputs as explicit hypotheses: `s₂(τ₁₆₃) = 77265280/90856689`. -/ diff --git a/LeanPool/Chudnovsky/ComplexMult.lean b/LeanPool/Chudnovsky/ComplexMult.lean index 3f1e04f14c..89420008d8 100644 --- a/LeanPool/Chudnovsky/ComplexMult.lean +++ b/LeanPool/Chudnovsky/ComplexMult.lean @@ -96,9 +96,9 @@ theorem isIntegral_C_mul_conj {τ : ℍ} {A B C : ℤ} have hconj : (A : ℂ) + B * (starRingEnd ℂ) (τ : ℂ) + C * ((starRingEnd ℂ) (τ : ℂ)) ^ 2 = 0 := by have := congrArg (starRingEnd ℂ) hCM - simpa using this + simpa only [map_add, map_intCast, map_mul, map_pow, map_zero] using this refine ⟨Polynomial.X ^ 2 + (Polynomial.C B * Polynomial.X + Polynomial.C (A * C)), ?_, ?_⟩ - · exact Polynomial.monic_X_pow_add (Polynomial.degree_linear_le.trans_lt (by norm_num)) + · exact Polynomial.monic_X_pow_add (Polynomial.degree_linear_le.trans_lt (by norm_num1)) · simp only [Polynomial.eval₂_add, Polynomial.eval₂_pow, Polynomial.eval₂_mul, Polynomial.eval₂_X, Polynomial.eval₂_C] push_cast @@ -260,10 +260,11 @@ private lemma C_mul_conj_mul {τ : ℍ} {A B C : ℤ} (hCM : (A : ℂ) + B * τ + C * (τ : ℂ) ^ 2 = 0) : ((C : ℂ) * τ) * ((C : ℂ) * (starRingEnd ℂ) (τ : ℂ)) = (A : ℂ) * C := by rcases eq_or_ne ((C : ℂ)) 0 with hC | hC - · simp [hC] + · simp only [hC, zero_mul, mul_zero] · have hconj : (A : ℂ) + B * (starRingEnd ℂ) (τ : ℂ) + C * ((starRingEnd ℂ) (τ : ℂ)) ^ 2 = 0 := by - have := congrArg (starRingEnd ℂ) hCM; simpa using this + have := congrArg (starRingEnd ℂ) hCM; simpa only [map_add, map_intCast, map_mul, map_pow, + map_zero] using this have hX : ((C : ℂ) * τ) ^ 2 + B * ((C : ℂ) * τ) + A * C = 0 := by linear_combination (C : ℂ) * hCM have hY : ((C : ℂ) * (starRingEnd ℂ) (τ : ℂ)) ^ 2 + @@ -307,7 +308,7 @@ private lemma countable_lattice_cm (L : PeriodPair) : (↑L.lattice : Set ℂ).C private helper in `DivisionValues.lean`). -/ private lemma frac_den_one_imp_zero_cm {m : ℕ} (hm : 0 < m) {k : ℤ} (hlt : k.natAbs < m) (h : ((k : ℚ) / (m : ℚ)).den = 1) : k = 0 := by - have hmQ : (m : ℚ) ≠ 0 := by exact_mod_cast hm.ne' + have hmQ : (m : ℚ) ≠ 0 := by exact Nat.cast_ne_zero.mpr hm.ne' set q : ℚ := (k : ℚ) / (m : ℚ) with hqdef have heq : ((q.num : ℤ) : ℚ) = q := (Rat.den_eq_one_iff q).mp h have hqk : (k : ℚ) = q.num * (m : ℚ) := by @@ -316,7 +317,7 @@ private lemma frac_den_one_imp_zero_cm {m : ℕ} (hm : 0 < m) {k : ℤ} have hnat : k.natAbs = q.num.natAbs * m := by rw [hkeq, Int.natAbs_mul, Int.natAbs_natCast] rcases Nat.eq_zero_or_pos q.num.natAbs with h0 | h0 - · rw [hkeq]; simp [Int.natAbs_eq_zero.mp h0] + · rw [hkeq]; simp only [Int.natAbs_eq_zero.mp h0, zero_mul] · exfalso have hle : m ≤ q.num.natAbs * m := Nat.le_mul_of_pos_left m h0 omega @@ -353,9 +354,9 @@ private lemma weierstrassZeta_add_int_cm (L : PeriodPair) {ω et : ℂ} (hω : apply hw have hb : (b : ℂ) * ω ∈ L.lattice := by rw [← zsmul_eq_mul]; exact zsmul_mem hω b - simpa using sub_mem hc hb + simpa only [add_sub_cancel_right] using sub_mem hc hb induction a using Int.induction_on with - | zero => simp + | zero => simp only [Int.cast_zero, zero_mul, add_zero] | succ k ih => rw [show w + ((k + 1 : ℤ) : ℂ) * ω = (w + ((k : ℤ) : ℂ) * ω) + ω by push_cast; ring, hq _ (hmem k), ih] @@ -395,7 +396,7 @@ private def cmSet (B C : ℤ) (M : ℕ) : Finset (Fin M × Fin M) := private lemma mem_cmSet_iff {B C : ℤ} {M : ℕ} {v : Fin M × Fin M} : v ∈ cmSet B C M ↔ C ∣ (v.2 : ℤ) ∧ (M : ℤ) ∣ C * (v.1 : ℤ) - B * (v.2 : ℤ) := by - simp [cmSet] + simp only [cmSet, Finset.mem_filter, Finset.mem_univ, true_and] private lemma zero_mem_cmSet {B C : ℤ} {M : ℕ} [NeZero M] : (0 : Fin M × Fin M) ∈ cmSet B C M := by @@ -585,7 +586,7 @@ private lemma card_cmSet {A B C : ℤ} {M : ℕ} (hA : 0 < A) (hC : 0 < C) calc (C : ℤ) * (((v.1 : ℕ) : ℤ) - B * (y : ℤ)) = C * ((v.1 : ℕ) : ℤ) - B * ((v.2 : ℕ) : ℤ) := by rw [hv2y]; ring _ = (M : ℤ) * d := hd - _ = C * (A * d) := by rw [hMAC]; ring + _ = C * (A * d) := by rw [hMAC]; ac_rfl exact mul_left_cancel₀ hCne hCC have hmod : (B * (y : ℤ)) % A = ((v.1 : ℕ) : ℤ) % A := by conv_rhs => rw [show ((v.1 : ℕ) : ℤ) = B * (y : ℤ) + A * d by linarith only [hAd]] @@ -607,7 +608,7 @@ private lemma card_cmSet {A B C : ℤ} {M : ℕ} (hA : 0 < A) (hC : 0 < C) rw [Nat.add_mul_div_left _ _ ha0, Nat.div_eq_of_lt ((Int.toNat_lt_toNat hA).mpr h1), zero_add] rw [key, Finset.card_univ] - simp [hM] + simp only [Fintype.card_prod, Fintype.card_fin, hM] private lemma cmM_pos {A C : ℤ} {M : ℕ} (hA : 0 < A) (hC : 0 < C) (hMAC : (M : ℤ) = A * C) : 0 < M := by @@ -684,7 +685,7 @@ private lemma analyticAt_mulDiffCM {τ : ℍ} {A B C : ℤ} {M : ℕ} intro hcc exact divPt_sub_notMem_lattice_cm (Lτ τ) hM0 hne (by have h := sub_mem hcc hv₀ - simpa [add_sub_add_left_eq_sub] using h) + simpa only [add_sub_add_left_eq_sub] using h) have hf : AnalyticAt ℂ (fun w : ℂ => w + (Lτ τ).divPt M v) z := by fun_prop exact ((Lτ τ).analyticOnNhd_weierstrassP _ hnl).comp_of_eq hf rfl · apply AnalyticAt.sub @@ -700,7 +701,7 @@ private lemma analyticAt_mulDiffCM {τ : ℍ} {A B C : ℤ} {M : ℕ} · apply Finset.analyticAt_fun_sum intro v hv have hnl : z + (Lτ τ).divPt M v ∉ (Lτ τ).lattice := fun hcc => hmp (by - simpa [mul_add] using + simpa only [mul_add, add_sub_cancel_right] using sub_mem (cm_alpha_mul_mem hCM hcc) (cmSet_mul_divPt_mem hCM hM0 hMAC hv)) have hf : AnalyticAt ℂ (fun w : ℂ => w + (Lτ τ).divPt M v) z := by fun_prop exact ((Lτ τ).analyticOnNhd_weierstrassP _ hnl).comp_of_eq hf rfl @@ -754,7 +755,7 @@ private lemma hasDerivAt_zetaCombCM {τ : ℍ} {A B C : ℤ} {M : ℕ} (-((Lτ τ).weierstrassP (z + (Lτ τ).divPt M v))) z := by intro v hv have hp : z + (Lτ τ).divPt M v ∉ (Lτ τ).lattice := fun hcc => hU (by - simpa [mul_add] using + simpa only [mul_add, add_sub_cancel_right] using sub_mem (cm_alpha_mul_mem hCM hcc) (cmSet_mul_divPt_mem hCM hM0 hMAC hv)) exact (hda _ hp).comp_add_const z _ have hsum : HasDerivAt @@ -765,7 +766,7 @@ private lemma hasDerivAt_zetaCombCM {τ : ℍ} {A B C : ℤ} {M : ℕ} ((C : ℂ) * τ * -((Lτ τ).weierstrassP ((C : ℂ) * τ * z))) z := by have h := HasDerivAt.scomp (𝕜 := ℂ) z (hda _ hU) ((hasDerivAt_id' z).const_mul ((C : ℂ) * τ)) - simpa [Function.comp_def, mul_comm] using h + simpa only [mul_comm, mul_neg, Function.comp_def, mul_one, smul_eq_mul] using h have hterm2 : HasDerivAt (fun w => (C : ℂ) * τ * (Lτ τ).weierstrassZeta ((C : ℂ) * τ * w)) ((C : ℂ) * τ * ((C : ℂ) * τ * -((Lτ τ).weierstrassP ((C : ℂ) * τ * z)))) z := HasDerivAt.const_mul ((C : ℂ) * τ) hcomp2 @@ -831,13 +832,16 @@ private lemma mulDiffCM_const_value {τ : ℍ} {A B C : ℤ} {M : ℕ} set S : Set ℂ := (fun z => (C : ℂ) * τ * z) ⁻¹' (↑(Lτ τ).lattice) with hSdef have hScount : S.Countable := (countable_lattice_cm (Lτ τ)).preimage (mul_right_injective₀ hα0) - have hSclosed : IsClosed S := IsClosed.preimage (by fun_prop) (Lτ τ).isClosed_lattice + have hSclosed : IsClosed S := IsClosed.preimage + SeparatelyContinuousMul.continuous_const_mul (Lτ τ).isClosed_lattice have hUopen : IsOpen (Sᶜ : Set ℂ) := hSclosed.isOpen_compl have hUconn : IsPreconnected (Sᶜ : Set ℂ) := - (hScount.isConnected_compl_of_one_lt_rank (by simp)).isPreconnected + (hScount.isConnected_compl_of_one_lt_rank (by simp only [rank_real_complex, + Nat.one_lt_ofNat])).isPreconnected have hcount2 : (S ∪ (fun z => z + 1) ⁻¹' S).Countable := hScount.union (hScount.preimage (add_left_injective 1)) - obtain ⟨z₀, hz₀⟩ := (hcount2.isConnected_compl_of_one_lt_rank (by simp)).nonempty + obtain ⟨z₀, hz₀⟩ := (hcount2.isConnected_compl_of_one_lt_rank (by simp only [rank_real_complex, + Nat.one_lt_ofNat])).nonempty rw [Set.mem_compl_iff, Set.mem_union, not_or] at hz₀ obtain ⟨hz₀S, hz₀S'⟩ := hz₀ have hUz₀ : (C : ℂ) * τ * z₀ ∉ (Lτ τ).lattice := hz₀S diff --git a/LeanPool/Chudnovsky/DivisionValues.lean b/LeanPool/Chudnovsky/DivisionValues.lean index 5a388929e1..225f3f3d80 100644 --- a/LeanPool/Chudnovsky/DivisionValues.lean +++ b/LeanPool/Chudnovsky/DivisionValues.lean @@ -78,8 +78,10 @@ theorem divPt_notMem_lattice {m : ℕ} [NeZero m] {v : Fin m × Fin m} (hv : v obtain ⟨hd1, hd2⟩ := hmem have e1 := div_den_eq_one_imp hmpos v.1.2 hd1 have e2 := div_den_eq_one_imp hmpos v.2.2 hd2 - have hv1 : v.1 = 0 := Fin.val_injective (by simpa using e1) - have hv2 : v.2 = 0 := Fin.val_injective (by simpa using e2) + have hv1 : v.1 = 0 := Fin.val_injective (by simpa only [Fin.coe_ofNat_eq_mod, Nat.zero_mod, + Fin.val_eq_zero_iff] using e1) + have hv2 : v.2 = 0 := Fin.val_injective (by simpa only [Fin.coe_ofNat_eq_mod, Nat.zero_mod, + Fin.val_eq_zero_iff] using e2) exact hv (Prod.ext hv1 hv2) /-! ## The σ-transformation law (paper Prop. `trafosigma`) @@ -284,7 +286,7 @@ The argument has three steps: /-- A signed fraction `k/m` with integral value and `|k| < m` is zero. -/ private lemma frac_den_one_imp_zero {m : ℕ} (hm : 0 < m) {k : ℤ} (hlt : k.natAbs < m) (h : ((k : ℚ) / (m : ℚ)).den = 1) : k = 0 := by - have hmQ : (m : ℚ) ≠ 0 := by exact_mod_cast hm.ne' + have hmQ : (m : ℚ) ≠ 0 := by exact Nat.cast_ne_zero.mpr hm.ne' set q : ℚ := (k : ℚ) / (m : ℚ) with hqdef have heq : ((q.num : ℤ) : ℚ) = q := (Rat.den_eq_one_iff q).mp h have hqk : (k : ℚ) = q.num * (m : ℚ) := by @@ -293,7 +295,7 @@ private lemma frac_den_one_imp_zero {m : ℕ} (hm : 0 < m) {k : ℤ} have hnat : k.natAbs = q.num.natAbs * m := by rw [hkeq, Int.natAbs_mul, Int.natAbs_natCast] rcases Nat.eq_zero_or_pos q.num.natAbs with h0 | h0 - · rw [hkeq]; simp [Int.natAbs_eq_zero.mp h0] + · rw [hkeq]; simp only [Int.natAbs_eq_zero.mp h0, zero_mul] · exfalso have hle : m ≤ q.num.natAbs * m := Nat.le_mul_of_pos_left m h0 omega @@ -302,7 +304,7 @@ private lemma frac_den_one_imp_zero {m : ℕ} (hm : 0 < m) {k : ℤ} private lemma frac_den_one_of_dvd {m : ℕ} (hm : 0 < m) {k : ℤ} (h : (m : ℤ) ∣ k) : ((k : ℚ) / (m : ℚ)).den = 1 := by obtain ⟨j, rfl⟩ := h - have hmQ : (m : ℚ) ≠ 0 := by exact_mod_cast hm.ne' + have hmQ : (m : ℚ) ≠ 0 := by exact Nat.cast_ne_zero.mpr hm.ne' have : (((m : ℤ) * j : ℤ) : ℚ) / (m : ℚ) = (j : ℚ) := by push_cast rw [mul_comm, mul_div_assoc, div_self hmQ, mul_one] @@ -325,7 +327,7 @@ private lemma mul_mem_lattice_of_add_divPt_mem {m : ℕ} [NeZero m] {z : ℂ} {v have h1 : (m : ℂ) * (z + L.divPt m v) ∈ L.lattice := by rw [← nsmul_eq_mul]; exact nsmul_mem h m have h2 := sub_mem h1 (L.mul_divPt_mem_lattice v) - simpa [mul_add] using h2 + simpa only [mul_add, add_sub_cancel_right] using h2 /-- Division points with distinct indices differ by a non-lattice point. -/ private lemma divPt_sub_notMem_lattice {m : ℕ} [NeZero m] {v v' : Fin m × Fin m} (hne : v ≠ v') : @@ -447,7 +449,7 @@ private lemma analyticAt_mulDiff {m : ℕ} [NeZero m] (z : ℂ) : AnalyticAt ℂ intro hc exact L.divPt_sub_notMem_lattice hne (by have h := sub_mem hc hv₀ - simpa [add_sub_add_left_eq_sub] using h) + simpa only [add_sub_add_left_eq_sub] using h) have hf : AnalyticAt ℂ (fun w : ℂ => w + L.divPt m v) z := by fun_prop exact (L.analyticOnNhd_weierstrassP _ hnl).comp_of_eq hf rfl · apply AnalyticAt.sub @@ -492,14 +494,14 @@ private lemma exists_mulDiff_const {m : ℕ} [NeZero m] : ∃ c : ℂ, ∀ z, L. private lemma weierstrassZeta_add_nat_ω₁ {w : ℂ} (hw : w ∉ L.lattice) (k : ℕ) : L.weierstrassZeta (w + (k : ℂ) * L.ω₁) = L.weierstrassZeta w + (k : ℂ) * L.eta₁ := by induction k with - | zero => simp + | zero => simp only [CharP.cast_eq_zero, zero_mul, add_zero] | succ n ih => have hmem : w + (n : ℂ) * L.ω₁ ∉ L.lattice := by intro hc apply hw have hn : (n : ℂ) * L.ω₁ ∈ L.lattice := by rw [← nsmul_eq_mul]; exact nsmul_mem L.ω₁_mem_lattice n - simpa using sub_mem hc hn + simpa only [add_sub_cancel_right] using sub_mem hc hn rw [show w + (↑(n + 1) : ℂ) * L.ω₁ = (w + (n : ℂ) * L.ω₁) + L.ω₁ by push_cast; ring, L.weierstrassZeta_add_ω₁ _ hmem, ih] push_cast; ring @@ -529,7 +531,7 @@ private lemma hasDerivAt_zetaComb {m : ℕ} [NeZero m] {z : ℂ} (hU : (m : ℂ) have hcomp2 : HasDerivAt (fun w => L.weierstrassZeta ((m : ℂ) * w)) ((m : ℂ) * -(L.weierstrassP ((m : ℂ) * z))) z := by have h := HasDerivAt.scomp (𝕜 := ℂ) z (hda _ hU) ((hasDerivAt_id' z).const_mul (m : ℂ)) - simpa [Function.comp_def, mul_comm] using h + simpa only [mul_comm, mul_neg, Function.comp_def, mul_one, smul_eq_mul] using h have hterm2 : HasDerivAt (fun w => (m : ℂ) * L.weierstrassZeta ((m : ℂ) * w)) ((m : ℂ) * ((m : ℂ) * -(L.weierstrassP ((m : ℂ) * z)))) z := HasDerivAt.const_mul (m : ℂ) hcomp2 @@ -571,11 +573,12 @@ domain `{m·z ∉ L}`, hence is constant; comparing at `z` and `z + ω₁` (wher forces `c·ω₁ = 0`, so `c = 0`. -/ private lemma mulDiff_const_eq_zero {m : ℕ} [NeZero m] {c : ℂ} (hc : ∀ z, L.mulDiff m z = c) : c = 0 := by - have hm0 : (m : ℂ) ≠ 0 := by exact_mod_cast (NeZero.pos m).ne' + have hm0 : (m : ℂ) ≠ 0 := by exact Nat.cast_ne_zero.mpr (NeZero.ne m) set B : Set ℂ := (fun z => (m : ℂ) * z) ⁻¹' (↑L.lattice) with hBdef have hmemB : ∀ x, x ∈ B ↔ (m : ℂ) * x ∈ L.lattice := fun x => Iff.rfl have hBcount : B.Countable := L.countable_lattice'.preimage (mul_right_injective₀ hm0) - have hBclosed : IsClosed B := IsClosed.preimage (by fun_prop) L.isClosed_lattice + have hBclosed : IsClosed B := IsClosed.preimage + SeparatelyContinuousMul.continuous_const_mul L.isClosed_lattice have hUopen : IsOpen (Bᶜ : Set ℂ) := hBclosed.isOpen_compl have hUconn : IsPreconnected (Bᶜ : Set ℂ) := (hBcount.isConnected_compl_of_one_lt_rank (by simp)).isPreconnected @@ -646,7 +649,7 @@ private lemma differentiable_sigmaProd : rw [← differentiableOn_univ] refine (L.hasProdLocallyUniformly_weierstrassSigmaTerm.hasProdLocallyUniformlyOn).differentiableOn (.of_forall fun _ ↦ ?_) isOpen_univ - simpa [Finset.prod_fn] using + simpa only [ne_eq, Finset.prod_fn] using DifferentiableOn.finsetProd fun i _ ↦ (hterm (i.1 : ℂ)).differentiableOn /-- `Q(0) = 1`. -/ @@ -680,7 +683,7 @@ private lemma sigma_meromorphicOrderAt (w : ℂ) : have hAn : AnalyticAt ℂ L.weierstrassSigma w := L.differentiable_weierstrassSigma.analyticAt w rw [hAn.meromorphicOrderAt_eq, analyticOrderAt_eq_zero.mpr (.inr (L.weierstrassSigma_ne_zero hw))] - simp + simp only [ENat.map_zero, CharP.cast_eq_zero, WithTop.coe_zero] /-- Translating the argument of `σ` shifts the base point of the meromorphic order. -/ private lemma sigma_shift_meromorphicOrderAt (a w : ℂ) : @@ -855,7 +858,7 @@ private lemma meromorphicOrderAt_shift (f : ℂ → ℂ) (a w : ℂ) : private lemma weierstrassP_eq_of_sub_mem {w s : ℂ} (h : w - s ∈ L.lattice) : L.weierstrassP s = L.weierstrassP w := by have := L.weierstrassP_sub_coe w ⟨w - s, h⟩ - rwa [show w - ((⟨w - s, h⟩ : L.lattice) : ℂ) = s by simp] at this + rwa [show w - ((⟨w - s, h⟩ : L.lattice) : ℂ) = s by simp only [sub_sub_cancel]] at this /-- The meromorphic order of `℘ − c` is invariant under lattice translation of the base point. -/ @@ -890,7 +893,7 @@ private lemma wpsub_meromorphicOrderAt_eq_two {c a : ℂ} (ha : a ∉ L.lattice) have h2 : 2 ≤ (meromorphicOrderAt f a).untop₀ := L.two_le_untop₀_meromorphicOrderAt ha hc hd have hne : meromorphicOrderAt f a ≠ ⊤ := by - intro htop; rw [htop] at h2; simp at h2 + intro htop; rw [htop] at h2; simp only [WithTop.untop₀_top, Int.reduceLE] at h2 -- upper bound via translation to the fundamental parallelogram and the counting bound obtain ⟨p, hpf, hpl⟩ := L.exists_mem_fund a have hordeq : meromorphicOrderAt f a = meromorphicOrderAt f p := by @@ -899,7 +902,7 @@ private lemma wpsub_meromorphicOrderAt_eq_two {c a : ℂ} (ha : a ∉ L.lattice) exact h have hpnl : p ∉ L.lattice := by intro hplat - exact ha (by simpa using add_mem hplat hpl) + exact ha (by simpa only [add_sub_cancel] using add_mem hplat hpl) have hpc : L.weierstrassP p = c := by rw [L.weierstrassP_eq_of_sub_mem hpl, hc] have hbound := L.sum_untop₀_meromorphicOrderAt_le_two c {p} (fun x hx => by rw [Finset.mem_singleton.mp hx]; exact hpf) @@ -919,8 +922,8 @@ private lemma wpsub_meromorphicOrderAt_eq_zero {c a : ℂ} (ha : a ∉ L.lattice have hAn : AnalyticAt ℂ (fun z => L.weierstrassP z - c) a := by have := L.analyticOnNhd_weierstrassP a ha; fun_prop rw [hAn.meromorphicOrderAt_eq, - analyticOrderAt_eq_zero.mpr (.inr (by simpa using sub_ne_zero.mpr hne))] - simp + analyticOrderAt_eq_zero.mpr (.inr (by simpa only [ne_eq] using sub_ne_zero.mpr hne))] + simp only [ENat.map_zero, CharP.cast_eq_zero, WithTop.coe_zero] /-- The meromorphic order of the σ-quotient `A(w) = σ(w+v)σ(w−v)/σ(w)²` decomposes as a sum of orders of shifted σ's. -/ @@ -932,14 +935,12 @@ private lemma sigmaQuot_meromorphicOrderAt (v z : ℂ) : - 2 * meromorphicOrderAt L.weierstrassSigma z := by have hσa : ∀ x : ℂ, AnalyticAt ℂ L.weierstrassSigma x := fun x => L.differentiable_weierstrassSigma.analyticAt x - have hm1 : MeromorphicAt (fun w => L.weierstrassSigma (w + v)) z := by - have : AnalyticAt ℂ (fun w : ℂ => L.weierstrassSigma (w + v)) z := by - have := hσa (z + v); fun_prop - exact this.meromorphicAt - have hm2 : MeromorphicAt (fun w => L.weierstrassSigma (w - v)) z := by - have : AnalyticAt ℂ (fun w : ℂ => L.weierstrassSigma (w - v)) z := by - have := hσa (z - v); fun_prop - exact this.meromorphicAt + have hm1 : MeromorphicAt (fun w => L.weierstrassSigma (w + v)) z := + ((hσa (z + v)).comp (f := fun w : ℂ => w + v) + (analyticAt_id.add analyticAt_const)).meromorphicAt + have hm2 : MeromorphicAt (fun w => L.weierstrassSigma (w - v)) z := + ((hσa (z - v)).comp (f := fun w : ℂ => w - v) + (analyticAt_id.sub analyticAt_const)).meromorphicAt have hm3 : MeromorphicAt (fun w => L.weierstrassSigma w ^ 2) z := ((hσa z).fun_pow 2).meromorphicAt have hshift1 : meromorphicOrderAt (fun w => L.weierstrassSigma (w + v)) z @@ -948,12 +949,12 @@ private lemma sigmaQuot_meromorphicOrderAt (v z : ℂ) : have hshift2 : meromorphicOrderAt (fun w => L.weierstrassSigma (w - v)) z = meromorphicOrderAt L.weierstrassSigma (z - v) := by have h := L.sigma_shift_meromorphicOrderAt (-v) z - simpa [sub_eq_add_neg] using h + simpa only [sub_eq_add_neg] using h have hpow : meromorphicOrderAt (fun w => L.weierstrassSigma w ^ 2) z = 2 * meromorphicOrderAt L.weierstrassSigma z := by rw [show (fun w => L.weierstrassSigma w ^ 2) = L.weierstrassSigma ^ 2 from rfl, meromorphicOrderAt_pow (hσa z).meromorphicAt] - norm_num + norm_num only rw [show (fun w => L.weierstrassSigma (w + v) * L.weierstrassSigma (w - v) / L.weierstrassSigma w ^ 2) = ((fun w => L.weierstrassSigma (w + v)) * (fun w => L.weierstrassSigma (w - v))) @@ -1223,9 +1224,9 @@ private lemma mul_mem_lattice_of_sub_divPt_mem {m : ℕ} [NeZero m] {z : ℂ} private lemma sigma_mulArg_meromorphicOrderAt (m : ℕ) [NeZero m] (z : ℂ) : meromorphicOrderAt (fun t => L.weierstrassSigma ((m : ℂ) * t)) z = meromorphicOrderAt L.weierstrassSigma ((m : ℂ) * z) := by - have hm : (m : ℂ) ≠ 0 := by exact_mod_cast (NeZero.pos m).ne' + have hm : (m : ℂ) ≠ 0 := by exact Nat.cast_ne_zero.mpr (NeZero.ne m) have hd : deriv (fun t : ℂ => (m : ℂ) * t) z = m := by - simp + simp only [deriv_const_mul_id'] have h := meromorphicOrderAt_comp_of_deriv_ne_zero (f := L.weierstrassSigma) (g := fun t => (m : ℂ) * t) (x := z) (by fun_prop) (by rw [hd]; exact hm) simpa only [Function.comp_def] using h @@ -1431,7 +1432,7 @@ private lemma trailingCoeff_Fm_zero (m : ℕ) [NeZero m] : meromorphicTrailingCoeffAt (L.Fm m) 0 = m := by have hσa : ∀ x : ℂ, AnalyticAt ℂ L.weierstrassSigma x := fun x => L.differentiable_weierstrassSigma.analyticAt x - have hm0 : (m : ℂ) ≠ 0 := by exact_mod_cast (NeZero.pos m).ne' + have hm0 : (m : ℂ) ≠ 0 := by exact Nat.cast_ne_zero.mpr (NeZero.ne m) set Q : ℂ → ℂ := fun z => ∏' l : {l : L.lattice // l ≠ 0}, weierstrassSigmaTerm z (l.1 : ℂ) with hQ have hQan : ∀ x : ℂ, AnalyticAt ℂ Q x := fun x => (L.differentiable_sigmaProd).analyticAt x @@ -1640,12 +1641,12 @@ noncomputable def P : ℕ → Coeff[X] lemma P_three : P 3 = C 3 * X ^ 4 - C (6 * h2) * X ^ 2 - C (12 * h3) * X - C (h2 ^ 2) := by - simp [P] + simp only [P, map_mul, map_pow] lemma P_four : P 4 = C 2 * X ^ 6 - C (10 * h2) * X ^ 4 - C (40 * h3) * X ^ 3 - C (10 * h2 ^ 2) * X ^ 2 - C (8 * h2 * h3) * X - C (16 * h3 ^ 2 - 2 * h2 ^ 3) := by - simp [P] + simp only [P, map_mul, map_pow, map_sub] /-- Recursion case `m = 4k + 1`, `k ≥ 1` (paper `defipm`). -/ lemma P_four_mul_add_one {k : ℕ} (hk : 1 ≤ k) : @@ -2083,10 +2084,10 @@ theorem lemwp2str {z : ℂ} (hz : z ∉ L.lattice) : have hP'' := L.hasDerivAt_derivWeierstrassP hw have hL : HasDerivAt (fun t => L.derivWeierstrassP t ^ 2) (2 * L.derivWeierstrassP w * deriv L.derivWeierstrassP w) w := by - simpa using hP''.fun_pow 2 + simpa only [Nat.cast_ofNat, Nat.add_one_sub_one, pow_one] using hP''.fun_pow 2 have h3 : HasDerivAt (fun t => L.weierstrassP t ^ 3) (3 * L.weierstrassP w ^ 2 * L.derivWeierstrassP w) w := by - simpa using hP'.fun_pow 3 + simpa only [Nat.cast_ofNat, Nat.add_one_sub_one] using hP'.fun_pow 3 have hR : HasDerivAt (fun t => 4 * L.weierstrassP t ^ 3 - L.g₂ * L.weierstrassP t - L.g₃) (4 * (3 * L.weierstrassP w ^ 2 * L.derivWeierstrassP w) @@ -2111,7 +2112,8 @@ theorem lemwp2str {z : ℂ} (hz : z ∉ L.lattice) : have := L.analyticOnNhd_weierstrassP w hw fun_prop have hconn : IsPreconnected ((↑L.lattice : Set ℂ)ᶜ) := - (L.countable_lattice'.isConnected_compl_of_one_lt_rank (by simp)).isPreconnected + (L.countable_lattice'.isConnected_compl_of_one_lt_rank (by simp only [Complex.rank_real_complex, + Nat.one_lt_ofNat])).isPreconnected obtain ⟨hz₀, h2z₀⟩ := L.divPt_three_props set z₀ : ℂ := L.divPt 3 ((1 : Fin 3), (0 : Fin 3)) with hz₀def have hd0 : L.derivWeierstrassP z₀ ≠ 0 := fun h0 => @@ -2142,7 +2144,7 @@ private lemma wp_third_deriv {z : ℂ} (hz : z ∉ L.lattice) : have h2 : HasDerivAt (fun w => 6 * L.weierstrassP w ^ 2 - L.g₂ / 2) (6 * (2 * L.weierstrassP z * L.derivWeierstrassP z)) z := by have h := ((hP'.fun_pow 2).const_mul (6 : ℂ)).sub_const (L.g₂ / 2) - simpa using h + simpa only [hasDerivAt_sub_const_iff, Nat.cast_ofNat, Nat.add_one_sub_one, pow_one] using h rw [h2.deriv] ring @@ -2218,9 +2220,9 @@ theorem Fm_two {z : ℂ} (hz : z ∉ L.lattice) : (mul_ne_zero (pow_ne_zero 2 hσz) (pow_ne_zero 2 hσz)) have hψ : HasDerivAt (fun v => (z - v) * H v) (-H z) z := by have h1 : HasDerivAt (fun v : ℂ => z - v) (-1) z := by - simpa using (hasDerivAt_id z).const_sub z + simpa only [id_eq] using (hasDerivAt_id z).const_sub z have h := h1.fun_mul hHdiff.hasDerivAt - simpa using h + simpa only [neg_mul, one_mul, sub_self, zero_mul, add_zero] using h have hA : HasDerivAt (fun v => L.weierstrassP v - L.weierstrassP z) (L.derivWeierstrassP z) z := (L.hasDerivAt_weierstrassP hz).sub_const _ have hev : (fun v => L.weierstrassP v - L.weierstrassP z) =ᶠ[𝓝 z] @@ -2235,7 +2237,7 @@ theorem Fm_two {z : ℂ} (hz : z ∉ L.lattice) : simp only [hHdef] rw [hQ0, mul_one, ← two_mul] simp only [Fm] - norm_num + norm_num1 ring_nf rw [← hHz] linear_combination hval @@ -2264,18 +2266,18 @@ private theorem wp2_eq_zeta {z : ℂ} (hz : z ∉ L.lattice) (h2z : 2 * z ∉ L. filter_upwards [L.isClosed_lattice.isOpen_compl.mem_nhds hz] with w hw have h := L.Fm_two hw simp only [Fm] at h - rw [show ((2 : ℕ) : ℂ) = (2 : ℂ) by norm_num, show (2 : ℕ) ^ 2 = 4 from rfl] at h + rw [show ((2 : ℕ) : ℂ) = (2 : ℂ) by norm_num1, show (2 : ℕ) ^ 2 = 4 from rfl] at h exact h have hlin : HasDerivAt (fun w : ℂ => 2 * w) 2 z := by - simpa using (hasDerivAt_id z).const_mul (2 : ℂ) + simpa only [id_eq, mul_one] using (hasDerivAt_id z).const_mul (2 : ℂ) have hnum : HasDerivAt (fun w => L.weierstrassSigma (2 * w)) (L.weierstrassZeta (2 * z) * L.weierstrassSigma (2 * z) * 2) z := by have h := (L.hasDerivAt_sigma h2z).comp z hlin - simpa [Function.comp_def] using h + simpa only [Function.comp_def] using h have hden : HasDerivAt (fun w => L.weierstrassSigma w ^ 4) (4 * L.weierstrassSigma z ^ 3 * (L.weierstrassZeta z * L.weierstrassSigma z)) z := by - simpa using (L.hasDerivAt_sigma hz).fun_pow 4 + simpa only [Nat.cast_ofNat, Nat.add_one_sub_one] using (L.hasDerivAt_sigma hz).fun_pow 4 have hdiv := hnum.fun_div hden (pow_ne_zero 4 hσz) have hneg : HasDerivAt (fun w => -L.derivWeierstrassP w) (-deriv L.derivWeierstrassP z) z := (L.hasDerivAt_derivWeierstrassP hz).fun_neg @@ -2285,7 +2287,7 @@ private theorem wp2_eq_zeta {z : ℂ} (hz : z ∉ L.lattice) (h2z : 2 * z ∉ L. -- substitute `σ(2z) = −℘′·σ(z)⁴` (that is, `F₂ = −℘′`) have hF2 := L.Fm_two hz simp only [Fm] at hF2 - rw [show ((2 : ℕ) : ℂ) = (2 : ℂ) by norm_num, show (2 : ℕ) ^ 2 = 4 from rfl, + rw [show ((2 : ℕ) : ℂ) = (2 : ℂ) by norm_num1, show (2 : ℕ) ^ 2 = 4 from rfl, div_eq_iff (pow_ne_zero 4 hσz)] at hF2 rw [hF2] at hEq have hgoal : (L.weierstrassSigma z ^ 4) ^ 2 * deriv L.derivWeierstrassP z @@ -2318,11 +2320,11 @@ private theorem wp_dup {z : ℂ} (hz : z ∉ L.lattice) (h2z : 2 * z ∉ L.latti have hEq := hev.deriv_eq rw [L.wp_third_deriv hz] at hEq have hlin : HasDerivAt (fun w : ℂ => 2 * w) 2 z := by - simpa using (hasDerivAt_id z).const_mul (2 : ℂ) + simpa only [id_eq, mul_one] using (hasDerivAt_id z).const_mul (2 : ℂ) have hζ2 : HasDerivAt (fun w => L.weierstrassZeta (2 * w)) (-L.weierstrassP (2 * z) * 2) z := by have h := (L.hasDerivAt_zeta h2z).comp z hlin - simpa [Function.comp_def] using h + simpa only [neg_mul, Function.comp_def] using h have hG : HasDerivAt (fun w => 2 * (L.weierstrassZeta (2 * w) - 2 * L.weierstrassZeta w)) (2 * (-L.weierstrassP (2 * z) * 2 - 2 * -L.weierstrassP z)) z := @@ -2351,16 +2353,16 @@ private theorem wpp_dup {z : ℂ} (hz : z ∉ L.lattice) (h2z : 2 * z ∉ L.latt exact L.wp_dup hw.1 hw.2 have hEq := hev.deriv_eq have hlin : HasDerivAt (fun w : ℂ => 2 * w) 2 z := by - simpa using (hasDerivAt_id z).const_mul (2 : ℂ) + simpa only [id_eq, mul_one] using (hasDerivAt_id z).const_mul (2 : ℂ) have hP2 : HasDerivAt (fun w => L.weierstrassP (2 * w)) (L.derivWeierstrassP (2 * z) * 2) z := by have h := (L.hasDerivAt_weierstrassP h2z).comp z hlin - simpa [Function.comp_def] using h + simpa only [Function.comp_def] using h have hP' := L.hasDerivAt_weierstrassP hz have hP'' := L.hasDerivAt_derivWeierstrassP hz have hP'sq : HasDerivAt (fun w => L.derivWeierstrassP w ^ 2) (2 * L.derivWeierstrassP z * deriv L.derivWeierstrassP z) z := by - simpa using hP''.fun_pow 2 + simpa only [Nat.cast_ofNat, Nat.add_one_sub_one, pow_one] using hP''.fun_pow 2 have hL : HasDerivAt (fun w => 4 * L.weierstrassP (2 * w) * L.derivWeierstrassP w ^ 2) (4 * (L.derivWeierstrassP (2 * z) * 2) * L.derivWeierstrassP z ^ 2 @@ -2372,7 +2374,7 @@ private theorem wpp_dup {z : ℂ} (hz : z ∉ L.lattice) (h2z : 2 * z ∉ L.latt (((L.analyticOnNhd_derivWeierstrassP z hz).deriv).differentiableAt).hasDerivAt have hdd2 : HasDerivAt (fun w => (deriv L.derivWeierstrassP w) ^ 2) (2 * deriv L.derivWeierstrassP z * deriv (deriv L.derivWeierstrassP) z) z := by - simpa using hdd.fun_pow 2 + simpa only [Nat.cast_ofNat, Nat.add_one_sub_one, pow_one] using hdd.fun_pow 2 have hR : HasDerivAt (fun w => (deriv L.derivWeierstrassP w) ^ 2 - 8 * L.weierstrassP w * L.derivWeierstrassP w ^ 2) @@ -2421,7 +2423,7 @@ private lemma Fm_zero (z : ℂ) : L.Fm 0 z = 0 := by /-- `F₁ = 1` off the lattice. -/ private lemma Fm_one {z : ℂ} (hz : z ∉ L.lattice) : L.Fm 1 z = 1 := by have hσ := L.weierstrassSigma_ne_zero hz - simp [Fm, div_self hσ] + simp only [Fm, Nat.cast_one, one_mul, one_pow, pow_one, div_self hσ] /-- `F_k(z) ≠ 0` when `z, kz ∉ L`. -/ private lemma Fm_ne_zero {k : ℕ} {z : ℂ} (hz : z ∉ L.lattice) @@ -2551,9 +2553,9 @@ private lemma coeffToC_h2 : L.coeffToC Milla.h2 = L.g₂ / 4 := by private lemma coeffToC_h3 : L.coeffToC Milla.h3 = L.g₃ / 4 := by simp [coeffToC, Milla.h3] -private lemma Pc_one : L.Pc 1 = 1 := by simp [Pc] +private lemma Pc_one : L.Pc 1 = 1 := by simp only [Pc, Milla.P_one, Polynomial.map_one] -private lemma Pc_two : L.Pc 2 = 1 := by simp [Pc] +private lemma Pc_two : L.Pc 2 = 1 := by simp only [Pc, Milla.P_two, Polynomial.map_one] private lemma eval_Pc_three (x : ℂ) : (L.Pc 3).eval x @@ -2902,7 +2904,8 @@ private lemma coeffToC_eq_comp : L.coeffToR := by apply MvPolynomial.ringHom_ext · intro r - simp [coeffToC, coeffToR] + simp only [coeffToC, Nat.succ_eq_add_one, Nat.reduceAdd, AlgHom.toRingHom_eq_coe, eq_intCast, + map_intCast, coeffToR] · intro i fin_cases i <;> simp [coeffToC, coeffToR] @@ -2961,15 +2964,17 @@ private lemma isIntegral_of_cubic_root {x : ℂ} (hx : 4 * (x ^ 3 - L.g₂ / 4 * x - L.g₃ / 4) = 0) : IsIntegral (Algebra.adjoin ℤ ({L.g₂ / 4, L.g₃ / 4} : Set ℂ)) x := by let R := Algebra.adjoin ℤ ({L.g₂ / 4, L.g₃ / 4} : Set ℂ) - let a : R := ⟨L.g₂ / 4, Algebra.subset_adjoin (by simp)⟩ - let b : R := ⟨L.g₃ / 4, Algebra.subset_adjoin (by simp)⟩ + let a : R := ⟨L.g₂ / 4, Algebra.subset_adjoin (by simp only [Set.mem_insert_iff, + Set.mem_singleton_iff, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, div_left_inj', true_or])⟩ + let b : R := ⟨L.g₃ / 4, Algebra.subset_adjoin (by simp only [Set.mem_insert_iff, ne_eq, + OfNat.ofNat_ne_zero, not_false_eq_true, div_left_inj', Set.mem_singleton_iff, or_true])⟩ refine ⟨Polynomial.X ^ 3 - (Polynomial.C a * Polynomial.X + Polynomial.C b), ?_, ?_⟩ · exact Polynomial.monic_X_pow_sub - (Polynomial.degree_linear_le.trans_lt (by norm_num)) + (Polynomial.degree_linear_le.trans_lt (by norm_num1)) · simp only [Polynomial.eval₂_sub, Polynomial.eval₂_add, Polynomial.eval₂_mul, Polynomial.eval₂_pow, Polynomial.eval₂_X, Polynomial.eval₂_C] change x ^ 3 - (L.g₂ / 4 * x + L.g₃ / 4) = 0 - have hzero := (mul_eq_zero.mp hx).resolve_left (by norm_num : (4 : ℂ) ≠ 0) + have hzero := (mul_eq_zero.mp hx).resolve_left (by norm_num1 : (4 : ℂ) ≠ 0) simpa only [sub_sub] using hzero /-- The evaluation of the Baker product at a division value vanishes. -/ diff --git a/LeanPool/Chudnovsky/Estimates.lean b/LeanPool/Chudnovsky/Estimates.lean index 69ef4c254b..123420d5c7 100644 --- a/LeanPool/Chudnovsky/Estimates.lean +++ b/LeanPool/Chudnovsky/Estimates.lean @@ -84,9 +84,9 @@ lemma mul_Jtilde_eq (τ : ℍ) : (1 + 240 * (q τ + 9 * q τ ^ 2)) ^ 3 / (q τ * (1 - q τ - q τ ^ 2) ^ 24) := by simp only [Jtilde] rw [show (1728 : ℂ) * q τ * (1 - q τ - q τ ^ 2) ^ 24 - = 1728 * (q τ * (1 - q τ - q τ ^ 2) ^ 24) by ring, + = 1728 * (q τ * (1 - q τ - q τ ^ 2) ^ 24) by ac_rfl, ← div_div, mul_div_assoc', mul_div_assoc', - mul_div_cancel_left₀ _ (by norm_num : (1728 : ℂ) ≠ 0)] + mul_div_cancel_left₀ _ (by norm_num1 : (1728 : ℂ) ≠ 0)] /-- The approximation `stilde₂` of Ramanujan's `s₂` from Theorem `theonaehers2` of the paper: `stilde₂(τ) = (1 + 240(q + 9q²))/(1 - 504(q + 33q²)) · (1 - 24(q + 3q²) - 3/(π·Im τ))`. -/ @@ -118,7 +118,7 @@ lemma norm_q_lt_of_mem_Region {τ : ℍ} (hτ : τ ∈ Region) : rw [norm_q, Real.exp_lt_exp, neg_lt_neg_iff] have hπ : (3.1408 : ℝ) < π := by linarith [Real.pi_gt_d4] have him : (5 / 4 : ℝ) < τ.im := hτ - nlinarith [mul_pos (sub_pos.2 hπ) (sub_pos.2 him)] + linarith [mul_pos (sub_pos.2 hπ) (sub_pos.2 him)] /-! ### `q`-expansions of the Eisenstein series (paper Prop. `sigmaeisen`) @@ -157,11 +157,11 @@ lemma E₄_eq_tsum (τ : ℍ) : /-- Paper Prop. `sigmaeisen`: `E₆(τ) = 1 - 504·∑_{n≥1} σ₅(n)·qⁿ`. -/ lemma E₆_eq_tsum (τ : ℍ) : E₆ τ = 1 - 504 * ∑' n : ℕ, (ArithmeticFunction.sigma 5 (n + 1) : ℂ) * q τ ^ (n + 1) := by - have h := EisensteinSeries.q_expansion_bernoulli (k := 6) (by norm_num) (by decide) τ + have h := EisensteinSeries.q_expansion_bernoulli (k := 6) (by norm_num only) (by decide) τ rw [show bernoulli 6 = 1 / 42 by as_aux_lemma => exact bernoulli_six_value, ← q_eq] at h simp only [zpow_natCast] at h rw [tsum_pnat_eq_tsum_succ (f := fun n ↦ (ArithmeticFunction.sigma 5 n : ℂ) * q τ ^ n)] at h - rw [h]; norm_num + rw [h]; norm_num only /-- Paper Prop. `sigmaeisen`: `E₂(τ) = 1 - 24·∑_{n≥1} σ₁(n)·qⁿ`. -/ lemma E2_eq_tsum (τ : ℍ) : @@ -313,14 +313,14 @@ theorem norm_eisensteinTail_sigma₁ {τ : ℍ} (hτ : τ ∈ Region) : set Q := ‖q τ‖ with hQdef have hQpos : 0 < Q := norm_q_pos τ have hQ : Q < 0.000389 := lt_trans (norm_q_lt_of_mem_Region hτ) exp_neg_bound - have hs : (1 + 1 / (4 : ℝ)) ^ (1 + 1) * Q < 1 := by norm_num; linarith - have htail := norm_eisensteinTail_le 1 4 (by norm_num) τ hs - norm_num at htail + have hs : (1 + 1 / (4 : ℝ)) ^ (1 + 1) * Q < 1 := by norm_num1; linarith + have htail := norm_eisensteinTail_le 1 4 (by norm_num1) τ hs + norm_num1 at htail rw [eisensteinTail_succ 1 3 τ] refine le_trans (norm_add_le _ _) ?_ rw [norm_mul, norm_pow, Complex.norm_natCast, show (ArithmeticFunction.sigma 1 3 : ℕ) = 4 from by decide] - have hD : (0 : ℝ) < 1 - 25 / 16 * Q := by linarith + have hD : (0 : ℝ) < 1 - 25 / 16 * Q := by linarith only [hQ] have hdiv : 16 * Q ^ 4 / (1 - 25 / 16 * Q) ≤ 0.007 * Q ^ 3 := by rw [div_le_iff₀ hD]; linarith [pow_succ_le_of_lt 3 hQpos hQ, pow_pos hQpos 3] push_cast @@ -332,14 +332,14 @@ theorem norm_eisensteinTail_sigma₃ {τ : ℍ} (hτ : τ ∈ Region) : set Q := ‖q τ‖ with hQdef have hQpos : 0 < Q := norm_q_pos τ have hQ : Q < 0.000389 := lt_trans (norm_q_lt_of_mem_Region hτ) exp_neg_bound - have hs : (1 + 1 / (4 : ℝ)) ^ (3 + 1) * Q < 1 := by norm_num; linarith - have htail := norm_eisensteinTail_le 3 4 (by norm_num) τ hs - norm_num at htail + have hs : (1 + 1 / (4 : ℝ)) ^ (3 + 1) * Q < 1 := by norm_num1; linarith + have htail := norm_eisensteinTail_le 3 4 (by norm_num1) τ hs + norm_num1 at htail rw [eisensteinTail_succ 3 3 τ] refine le_trans (norm_add_le _ _) ?_ rw [norm_mul, norm_pow, Complex.norm_natCast, show (ArithmeticFunction.sigma 3 3 : ℕ) = 28 from by decide] - have hD : (0 : ℝ) < 1 - 625 / 256 * Q := by linarith + have hD : (0 : ℝ) < 1 - 625 / 256 * Q := by linarith only [hQ] have hdiv : 256 * Q ^ 4 / (1 - 625 / 256 * Q) ≤ 0.1 * Q ^ 3 := by rw [div_le_iff₀ hD]; linarith [pow_succ_le_of_lt 3 hQpos hQ, pow_pos hQpos 3] push_cast @@ -351,14 +351,14 @@ theorem norm_eisensteinTail_sigma₅ {τ : ℍ} (hτ : τ ∈ Region) : set Q := ‖q τ‖ with hQdef have hQpos : 0 < Q := norm_q_pos τ have hQ : Q < 0.000389 := lt_trans (norm_q_lt_of_mem_Region hτ) exp_neg_bound - have hs : (1 + 1 / (4 : ℝ)) ^ (5 + 1) * Q < 1 := by norm_num; linarith - have htail := norm_eisensteinTail_le 5 4 (by norm_num) τ hs - norm_num at htail + have hs : (1 + 1 / (4 : ℝ)) ^ (5 + 1) * Q < 1 := by norm_num1; linarith + have htail := norm_eisensteinTail_le 5 4 (by norm_num1) τ hs + norm_num1 at htail rw [eisensteinTail_succ 5 3 τ] refine le_trans (norm_add_le _ _) ?_ rw [norm_mul, norm_pow, Complex.norm_natCast, show (ArithmeticFunction.sigma 5 3 : ℕ) = 244 from by decide] - have hD : (0 : ℝ) < 1 - 15625 / 4096 * Q := by linarith + have hD : (0 : ℝ) < 1 - 15625 / 4096 * Q := by linarith only [hQ] have hdiv : 4096 * Q ^ 4 / (1 - 15625 / 4096 * Q) ≤ 1.6 * Q ^ 3 := by rw [div_le_iff₀ hD]; linarith [pow_succ_le_of_lt 3 hQpos hQ, pow_pos hQpos 3] push_cast @@ -675,7 +675,7 @@ lemma horner_norm_bound (p : ℂ) {ρ : ℝ} (hp : ‖p‖ ≤ ρ) (hρ : 0 ≤ ≤ l.foldr (fun (a : ℤ) (acc : ℝ) => |(a : ℝ)| + ρ * acc) 0 := by intro l induction l with - | nil => simp + | nil => simp only [List.foldr_nil, norm_zero, Std.le_refl] | cons a t ih => rw [List.foldr_cons, List.foldr_cons] refine (norm_add_le _ _).trans ?_ @@ -880,7 +880,7 @@ theorem theonaeherJ_approx {τ : ℍ} (hτ : τ ∈ Region) : have heq : 1728 * J τ - 1728 * Jtilde τ = (1728 * q τ * J τ - 1728 * q τ * Jtilde τ) / q τ := by rw [eq_div_iff hq]; ring rw [heq, norm_div, div_lt_iff₀ hQpos] - nlinarith [lem3 hτ, pow_pos hQpos 2, hQpos] + linarith [lem3 hτ, pow_pos hQpos 2, hQpos] /-- Paper Theorem `theonaeherJ`, headline approximation bound: `|1728·J(τ) - 1728·Jtilde(τ)| < 0.2` for `Im τ > 5/4`. -/ diff --git a/LeanPool/Chudnovsky/Fourier.lean b/LeanPool/Chudnovsky/Fourier.lean index 4e824984d5..921fbd9509 100644 --- a/LeanPool/Chudnovsky/Fourier.lean +++ b/LeanPool/Chudnovsky/Fourier.lean @@ -62,7 +62,8 @@ private lemma G_Lτ_eq (τ : ℍ) {k : ℕ} (hk : 3 ≤ k) : have hbase : (((Lτ τ).latticeEquivProd.symm.toEquiv x : (Lτ τ).lattice) : ℂ) = (x.1 : ℂ) + (x.2 : ℂ) * (τ : ℂ) := by have h := (Lτ τ).latticeEquiv_symm_apply x - simpa using h + simpa only [LinearEquiv.toEquiv_symm, LinearEquiv.coe_symm_toEquiv, Lτ_ω₁, mul_one, + Lτ_ω₂] using h rw [hbase, eisSummand, pairArrowEquiv_apply] simp only [Matrix.cons_val_zero, Matrix.cons_val_one] rw [zpow_neg, zpow_natCast, add_comm] @@ -76,8 +77,8 @@ private lemma eisensteinSeries_eq_two_E (τ : ℍ) {k : ℕ} (hk : 3 ≤ k) : /-- `ζ(6) = π⁶/945`. -/ private lemma riemannZeta_six : riemannZeta 6 = (π : ℂ) ^ 6 / 945 := by - have h := riemannZeta_two_mul_nat (k := 3) (by norm_num) - norm_num [show bernoulli 6 = 1 / 42 by as_aux_lemma => exact bernoulli_six_value] at h + have h := riemannZeta_two_mul_nat (k := 3) (by norm_num1) + norm_num only [show bernoulli 6 = 1 / 42 by as_aux_lemma => exact bernoulli_six_value] at h rw [h]; ring private lemma pi_C_ne_zero : (π : ℂ) ≠ 0 := by exact_mod_cast Real.pi_ne_zero @@ -147,10 +148,11 @@ private lemma weierstrassSigma_add_period (L : PeriodPair) (ω : ℂ) (hωlat : set S : Set ℂ := (↑L.lattice)ᶜ with hSdef have hSopen : IsOpen S := L.isClosed_lattice.isOpen_compl have hSconn : IsPreconnected S := - ((countable_lattice L).isConnected_compl_of_one_lt_rank (by simp)).isPreconnected + ((countable_lattice L).isConnected_compl_of_one_lt_rank (by simp only [rank_real_complex, + Nat.one_lt_ofNat])).isPreconnected have hσdiff : Differentiable ℂ sig := L.differentiable_weierstrassSigma have hmem : ∀ {x : ℂ}, x ∉ L.lattice → x + ω ∉ L.lattice := by - intro x hx hc; exact hx (by simpa using sub_mem hc hωlat) + intro x hx hc; exact hx (by simpa only [add_sub_cancel_right] using sub_mem hc hωlat) have hσne : ∀ {x : ℂ}, x ∉ L.lattice → sig x ≠ 0 := by intro x hx; rw [hsig]; exact fun h => hx ((L.weierstrassSigma_eq_zero_iff x).mp h) set E : ℂ → ℂ := fun z => Complex.exp (μ * (z + ω / 2)) with hE @@ -159,8 +161,8 @@ private lemma weierstrassSigma_add_period (L : PeriodPair) (ω : ℂ) (hωlat : have hEderiv : ∀ z, HasDerivAt E (μ * E z) z := by intro z have hlin : HasDerivAt (fun z : ℂ => μ * (z + ω / 2)) μ z := by - simpa using ((hasDerivAt_id z).add_const (ω / 2)).const_mul μ - simpa [hE, mul_comm] using hlin.cexp + simpa only [id_eq, mul_one] using ((hasDerivAt_id z).add_const (ω / 2)).const_mul μ + simpa only [hE, mul_comm] using hlin.cexp have hf : ∀ z, HasDerivAt (fun z => sig (z + ω)) (deriv sig (z + ω)) z := by intro z have h := (hσdiff (z + ω)).hasDerivAt.comp z ((hasDerivAt_id z).add_const ω) @@ -205,7 +207,7 @@ private lemma weierstrassSigma_add_period (L : PeriodPair) (ω : ℂ) (hωlat : -- Hence `m = -1` on `S`. have hmconst : Set.EqOn m (fun _ => (-1 : ℂ)) S := by have hx0mem : -(ω / 2) ∈ S := by - change -(ω / 2) ∉ L.lattice; intro hc; exact hω2 (by simpa using neg_mem hc) + change -(ω / 2) ∉ L.lattice; intro hc; exact hω2 (by simpa only [neg_neg] using neg_mem hc) have hval0 : m (-(ω / 2)) = -1 := by have e1 : -(ω / 2) + ω = ω / 2 := by ring have hEval : E (-(ω / 2)) = 1 := by @@ -216,7 +218,7 @@ private lemma weierstrassSigma_add_period (L : PeriodPair) (ω : ℂ) (hωlat : rw [inv_neg, mul_neg, mul_inv_cancel₀ hsne] refine hSopen.eqOn_of_deriv_eq hSconn ?_ (differentiableOn_const _) ?_ hx0mem ?_ · exact fun z hz => (hmderiv z hz).differentiableAt.differentiableWithinAt - · intro z hz; rw [(hmderiv z hz).deriv]; simp + · intro z hz; rw [(hmderiv z hz).deriv]; simp only [deriv_const'] · simpa using hval0 -- Turn the constancy into the pointwise relation on `S`, then extend by density. have hkey : Set.EqOn (fun z => sig (z + ω)) (fun z => -E z * sig z) S := by @@ -228,13 +230,13 @@ private lemma weierstrassSigma_add_period (L : PeriodPair) (ω : ℂ) (hωlat : change sig (z + ω) = -E z * sig z rw [this, hg]; ring have hcontf : Continuous (fun z => sig (z + ω)) := - hσdiff.continuous.comp (by fun_prop) + hσdiff.continuous.comp SeparatelyContinuousAdd.continuous_add_const have hcontg : Continuous (fun z => -E z * sig z) := by have hcE : Continuous E := by simp only [hE]; fun_prop exact (hcE.neg).mul hσdiff.continuous have heq := Continuous.ext_on (dense_compl_lattice L) hcontf hcontg hkey have := congrFun heq z - simpa [hsig, hE] using this + simpa only [hsig, neg_mul, hE] using this /-- σ transformation law for `L_τ` in the `ω₁ = 1` direction: `σ(z+1) = -exp(η₁·(z+1/2))·σ(z)`. -/ @@ -310,7 +312,8 @@ private lemma qProd_ne_zero {q : ℂ} (hq : ‖q‖ < 1) {v : ℂ} refine tprod_one_add_ne_zero_of_summable (fun k => ?_) ?_ · rw [show (1 : ℂ) + -(q ^ (k + 1) * v) = 1 - q ^ (k + 1) * v by ring, sub_ne_zero] exact fun h => hv k h.symm - · simpa [norm_neg] using summable_norm_iff.mpr (summable_qpow_mul hq v) + · simpa only [norm_neg, Complex.norm_mul, + norm_pow] using summable_norm_iff.mpr (summable_qpow_mul hq v) have hcongr : (∏' k : ℕ, (1 + -(q ^ (k + 1) * v))) = qProd q v := by simp only [qProd]; exact tprod_congr (fun k => by ring) rwa [hcongr] at key @@ -326,7 +329,7 @@ private lemma differentiable_qProd {q : ℂ} (hq : ‖q‖ < 1) : apply hasProdLocallyUniformlyOn_of_forall_compact isOpen_univ intro K _ hcK rcases K.eq_empty_or_nonempty with hN | hN - · simpa [hasProdUniformlyOn_iff_tendstoUniformlyOn, hN] using tendstoUniformlyOn_empty + · simpa only [hN, hasProdUniformlyOn_iff_tendstoUniformlyOn] using tendstoUniformlyOn_empty · obtain ⟨v₀, _, _, HB⟩ := hcK.exists_sSup_image_eq_and_ge hN (show ContinuousOn (fun v : ℂ => ‖v‖) K by fun_prop) refine (((summable_nat_add_iff 1).mpr @@ -336,7 +339,7 @@ private lemma differentiable_qProd {q : ℂ} (hq : ‖q‖ < 1) : rw [norm_neg, norm_mul, norm_pow] exact mul_le_mul_of_nonneg_left (HB x hx) (by positivity) have := hLU.hasProdLocallyUniformlyOn.differentiableOn - (.of_forall fun _ => by simpa [Finset.prod_fn] using + (.of_forall fun _ => by simpa only [Finset.prod_fn] using DifferentiableOn.finsetProd (fun i _ => by fun_prop)) isOpen_univ exact this @@ -592,7 +595,7 @@ private lemma deriv_weierstrassSigma_zero (L : PeriodPair) : deriv L.weierstrass rw [← differentiableOn_univ] refine (L.hasProdLocallyUniformly_weierstrassSigmaTerm.hasProdLocallyUniformlyOn |>.differentiableOn) (.of_forall fun _ => ?_) isOpen_univ - simpa [Finset.prod_fn] using DifferentiableOn.finsetProd (fun i _ => + simpa only [ne_eq, Finset.prod_fn] using DifferentiableOn.finsetProd (fun i _ => (by unfold PeriodPair.weierstrassSigmaTerm; fun_prop : DifferentiableOn ℂ (fun z => PeriodPair.weierstrassSigmaTerm z (i.1 : ℂ)) _)) have hP0 : (∏' l : {l : L.lattice // l ≠ 0}, @@ -617,15 +620,15 @@ private lemma gfun_hasDerivAt_zero (τ : ℍ) : HasDerivAt (gfun τ) 1 0 := by have h1 : HasDerivAt (fun z : ℂ => exp (2 * (π : ℂ) * I * z)) (exp (2 * (π : ℂ) * I * 0) * (2 * (π : ℂ) * I)) 0 := by have hlin : HasDerivAt (fun z : ℂ => 2 * (π : ℂ) * I * z) (2 * (π : ℂ) * I) 0 := by - simpa using (hasDerivAt_id (0 : ℂ)).const_mul (2 * (π : ℂ) * I) - simpa [mul_comm] using hlin.cexp + simpa only [id_eq, mul_one] using (hasDerivAt_id (0 : ℂ)).const_mul (2 * (π : ℂ) * I) + simpa only [mul_comm, zero_mul, exp_zero, one_mul] using hlin.cexp have hA : HasDerivAt (fun z : ℂ => (exp (2 * (π : ℂ) * I * z) - 1) / (2 * (π : ℂ) * I)) 1 0 := by have := (h1.sub_const 1).div_const (2 * (π : ℂ) * I) rwa [mul_zero, Complex.exp_zero, one_mul, div_self h2pi] at this have hmul := hA.mul (differentiable_Gfun τ 0).hasDerivAt have hval : (1 : ℂ) * Gfun τ 0 + (exp (2 * (π : ℂ) * I * 0) - 1) / (2 * (π : ℂ) * I) * deriv (Gfun τ) 0 = 1 := by - rw [Gfun_zero]; simp + rw [Gfun_zero]; simp only [mul_one, mul_zero, exp_zero, sub_self, zero_div, zero_mul, add_zero] rw [hval] at hmul exact hmul @@ -651,7 +654,7 @@ private lemma phi_order (τ : ℍ) (z : ℂ) : rfl rw [heq, meromorphicOrderAt_mul hexpan.meromorphicAt hσ, hexpan.meromorphicOrderAt_eq, hexpan.analyticOrderAt_eq_zero.mpr (Complex.exp_ne_zero _)] - simp + simp only [ENat.map_zero, CharP.cast_eq_zero, WithTop.coe_zero, zero_add] /-- `H := φ/g` is periodic under the lattice `L_τ`. -/ private lemma hfun_add_lattice (τ : ℍ) (l : ℂ) (hl : l ∈ (Lτ τ).lattice) (z : ℂ) : @@ -699,7 +702,8 @@ theorem weierstrassSigma_Lτ (τ : ℍ) (z : ℂ) : have hHord0 : meromorphicOrderAt H 0 = 0 := by rw [hH, meromorphicOrderAt_div (hφmero 0) (hgmero 0), phi_order τ 0, (Lτ τ).meromorphicOrderAt_weierstrassSigma 0 (Lτ τ).lattice.zero_mem, gfun_order_zero] - simp + simp only [LinearOrderedAddCommGroupWithTop.sub_self_eq_zero_iff_ne_top, ne_eq, + WithTop.one_ne_top, not_false_eq_true] have hHordAll : ∀ w, meromorphicOrderAt H w = 0 := by intro w by_cases hw : w ∈ (Lτ τ).lattice @@ -707,7 +711,7 @@ theorem weierstrassSigma_Lτ (τ : ℍ) (z : ℂ) : have hcomp : (H ∘ fun x => x + w) = H := by funext x have := hfun_add_lattice τ w hw x - simpa [hH, Pi.div_apply] using this + simpa only [hH, Function.comp_apply, Pi.div_apply] using this have hg : AnalyticAt ℂ (fun x : ℂ => x + w) 0 := by fun_prop have hg' : deriv (fun x : ℂ => x + w) 0 ≠ 0 := by rw [deriv_add_const, deriv_id'']; exact one_ne_zero @@ -726,7 +730,7 @@ theorem weierstrassSigma_Lτ (τ : ℍ) (z : ℂ) : have han : AnalyticAt ℂ (gfun τ) w := (differentiable_gfun τ).analyticAt w rw [han.meromorphicOrderAt_eq, han.analyticOrderAt_eq_zero.mpr (gfun_ne_zero τ hw)] rfl - rw [hσw, hgw]; simp + rw [hσw, hgw]; simp only [sub_zero] -- Apply the workhorse against the constant `1`. have hone : (Lτ τ).IsEllipticWith (fun _ : ℂ => (1 : ℂ)) := ⟨fun w => analyticAt_const.meromorphicAt, fun w l => rfl⟩ @@ -739,7 +743,7 @@ theorem weierstrassSigma_Lτ (τ : ℍ) (z : ℂ) : -- Turn the codiscrete equality into `φ = c·g` everywhere. have hcodis' : {w : ℂ | H w = c} ∈ Filter.codiscrete ℂ := by have h : {w : ℂ | H w = (fun _ => c * (1 : ℂ)) w} ∈ Filter.codiscrete ℂ := hcodis - simpa using h + simpa only [mul_one] using h have hsub : {w : ℂ | H w = c} ⊆ {w : ℂ | φfun τ w = c * gfun τ w} := by intro w hw simp only [Set.mem_ofPred_eq, hH, Pi.div_apply] at hw ⊢ @@ -770,9 +774,10 @@ theorem weierstrassSigma_Lτ (τ : ℍ) (z : ℂ) : have hvlin : HasDerivAt (fun z : ℂ => -(Lτ τ).eta₁ / 2 * z ^ 2 + (π : ℂ) * I * z) ((π : ℂ) * I) 0 := by have h1 : HasDerivAt (fun z : ℂ => -(Lτ τ).eta₁ / 2 * z ^ 2) 0 0 := by - simpa using (hasDerivAt_pow 2 (0 : ℂ)).const_mul (-(Lτ τ).eta₁ / 2) + simpa only [Nat.cast_ofNat, Nat.add_one_sub_one, pow_one, + mul_zero] using (hasDerivAt_pow 2 (0 : ℂ)).const_mul (-(Lτ τ).eta₁ / 2) have h2 : HasDerivAt (fun z : ℂ => (π : ℂ) * I * z) ((π : ℂ) * I) 0 := by - simpa using (hasDerivAt_id (0 : ℂ)).const_mul ((π : ℂ) * I) + simpa only [id_eq, mul_one] using (hasDerivAt_id (0 : ℂ)).const_mul ((π : ℂ) * I) have h3 := h1.add h2 rw [zero_add] at h3 exact h3 diff --git a/LeanPool/Chudnovsky/Imports.lean b/LeanPool/Chudnovsky/Imports.lean index 5c5c773e2d..2410b26dea 100644 --- a/LeanPool/Chudnovsky/Imports.lean +++ b/LeanPool/Chudnovsky/Imports.lean @@ -20,6 +20,7 @@ public import LeanPool.Chudnovsky.Kummer public import LeanPool.Chudnovsky.Lattices public import LeanPool.Chudnovsky.Liouville public import LeanPool.Chudnovsky.MainTheorem +public import LeanPool.Chudnovsky.NumericalBounds public import LeanPool.Chudnovsky.Numerics public import LeanPool.Chudnovsky.Periodicity public import LeanPool.Chudnovsky.PicardFuchs diff --git a/LeanPool/Chudnovsky/Kummer.lean b/LeanPool/Chudnovsky/Kummer.lean index 7330a5b174..5ad75d8db6 100644 --- a/LeanPool/Chudnovsky/Kummer.lean +++ b/LeanPool/Chudnovsky/Kummer.lean @@ -395,7 +395,7 @@ private lemma hasDerivAt_YhC (τ : ℍ) (h4 : E₄ τ ≠ 0) (h6 : E₆ τ ≠ 0 + 1 / 12 * (5 / 12) * hyp2F1 (J τ)⁻¹) / ((J τ)⁻¹ * ((J τ)⁻¹ - 1)) := by rw [eq_div_iff hden] linear_combination hODE - convert h using 1 + refine h.congr_deriv (Eq.symm ?_) rw [XhC_apply, YhC_apply, hF2] simp only [m22] rw [inv_J_sub_one h4, inv_J_eq] @@ -465,12 +465,12 @@ All limits are soft consequences of `E₂, E₄, E₆ → 1` except `Ytilde → cusp-function factorization of `D E₄` and `kfun → 1`. -/ private lemma tendsto_q_zero : Tendsto (fun τ : ℍ => q τ) atImInfty (𝓝 0) := by - simpa [q] using qParam_tendsto_atImInfty one_pos + simpa only [q] using qParam_tendsto_atImInfty one_pos private lemma tendsto_invJ : Tendsto (fun τ : ℍ => (J τ)⁻¹) atImInfty (𝓝 0) := by have h := ((tendsto_E₄_atImInfty.pow 3).sub (tendsto_E₆_atImInfty.pow 2)).div - (tendsto_E₄_atImInfty.pow 3) (by norm_num) - norm_num at h + (tendsto_E₄_atImInfty.pow 3) (by norm_num only) + norm_num only at h exact h.congr fun τ => (inv_J_eq τ).symm private lemma tendsto_XhC : Tendsto (fun τ : ℍ => XhC ↑τ) atImInfty (𝓝 1) := by @@ -534,14 +534,15 @@ private lemma YtC_eq (τ : ℍ) : field_simp rcases eq_or_ne (E₆ τ) 0 with h6 | h6 · rw [YtC_apply, h6] - simp + simp only [one_div, sub_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, mul_zero, + div_zero] · have hk : kfun τ ≠ 0 := - div_ne_zero (E₄_cube_sub_E₆_sq_ne_zero τ) (mul_ne_zero (by norm_num) hq) + div_ne_zero (E₄_cube_sub_E₆_sq_ne_zero τ) (mul_ne_zero (by norm_num only) hq) have hd1 : (12 : ℂ) * (1728 * q τ * kfun τ) * E₆ τ ≠ 0 := - mul_ne_zero (mul_ne_zero (by norm_num) - (mul_ne_zero (mul_ne_zero (by norm_num) hq) hk)) h6 + mul_ne_zero (mul_ne_zero (by norm_num only) + (mul_ne_zero (mul_ne_zero (by norm_num only) hq) hk)) h6 have hd2 : (6912 : ℂ) * kfun τ * E₆ τ ≠ 0 := - mul_ne_zero (mul_ne_zero (by norm_num) hk) h6 + mul_ne_zero (mul_ne_zero (by norm_num only) hk) h6 rw [YtC_apply, XtC_apply, hkey, hB, div_eq_div_iff hd1 hd2] ring @@ -550,15 +551,16 @@ private lemma tendsto_kfun : Tendsto kfun atImInfty (𝓝 1) := by have h1 : Tendsto (fun τ : ℍ => (1 : ℂ) - q τ - q τ ^ 2) atImInfty (𝓝 (1 - 0 - 0 ^ 2)) := (tendsto_const_nhds.sub tendsto_q_zero).sub (tendsto_q_zero.pow 2) have h2 := h1.pow 24 - norm_num at h2 + norm_num only at h2 exact h2.congr fun τ => by rw [ktilde] have hdiff : Tendsto (fun τ : ℍ => kfun τ - ktilde τ) atImInfty (𝓝 0) := by have hev : ∀ᶠ τ : ℍ in atImInfty, ‖kfun τ - ktilde τ‖ ≤ 365.6 * ‖q τ‖ ^ 2 := by rw [eventually_iff, atImInfty_mem] - exact ⟨2, fun τ hτ => lemk (lt_of_lt_of_le (by norm_num) hτ)⟩ + exact ⟨2, fun τ hτ => lemk (lt_of_lt_of_le (by norm_num only) hτ)⟩ have hg : Tendsto (fun τ : ℍ => 365.6 * ‖q τ‖ ^ 2) atImInfty (𝓝 0) := by have h := (tendsto_q_zero.norm.pow 2).const_mul (365.6 : ℝ) - simpa using h + simpa only [norm_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, + mul_zero] using h exact squeeze_zero_norm' hev hg have h := hkt.add hdiff rw [add_zero] at h @@ -571,21 +573,21 @@ private lemma tendsto_YtC : Tendsto (fun τ : ℍ => YtC ↑τ) atImInfty (𝓝 have hΦ0 : deriv (cuspFunction 1 ⇑E₄) 0 = 240 := by have h := ModularForm.E₄_qExpansion_coeff_one rw [qExpansion_coeff] at h - simpa [iteratedDeriv_one] using h + simpa only [Nat.factorial_one, Nat.cast_one, inv_one, iteratedDeriv_one, one_mul] using h have hΦ : Tendsto (fun τ : ℍ => deriv (cuspFunction 1 ⇑E₄) (q τ)) atImInfty (𝓝 240) := by have h := (hΦana.deriv.continuousAt.tendsto).comp tendsto_q_zero rwa [hΦ0] at h have hnum := (tendsto_XtC.mul (tendsto_E₄_atImInfty.pow 3)).mul hΦ have hden : Tendsto (fun τ : ℍ => 6912 * kfun τ * E₆ τ) atImInfty (𝓝 (6912 * 1 * 1)) := (tendsto_kfun.const_mul (6912 : ℂ)).mul tendsto_E₆_atImInfty - have h := hnum.div hden (by norm_num) - have hval : ((1 * 1 ^ 3 * 240 : ℂ)) / (6912 * 1 * 1) = 5 / 144 := by norm_num + have h := hnum.div hden (by norm_num only) + have hval : ((1 * 1 ^ 3 * 240 : ℂ)) / (6912 * 1 * 1) = 5 / 144 := by norm_num only rw [hval] at h exact h.congr fun τ => (YtC_eq τ).symm private lemma tendsto_WrC : Tendsto (fun τ : ℍ => WrC ↑τ) atImInfty (𝓝 0) := by have h := (tendsto_XhC.mul tendsto_YtC).sub (tendsto_YhC.mul tendsto_XtC) - norm_num at h + norm_num only at h exact h.congr fun τ => by rw [WrC_apply] private lemma tendsto_m22 : Tendsto (fun τ : ℍ => m22 τ) atImInfty (𝓝 (-1)) := by @@ -625,20 +627,20 @@ private lemma eventually_good : ∀ᶠ τ : ℍ in atImInfty, E₄ τ ∈ Complex.slitPlane ∧ E₆ τ ≠ 0 ∧ J τ ≠ 0 ∧ ‖(J τ)⁻¹‖ < 1 ∧ XhC ↑τ ≠ 0 ∧ (m22 τ).re ≤ -(1 / 2) := by have h₁ : ∀ᶠ τ : ℍ in atImInfty, ‖E₄ τ - 1‖ < 1 / 2 := by - have h := Metric.tendsto_nhds.mp tendsto_E₄_atImInfty (1 / 2) (by norm_num) - simpa [dist_eq_norm] using h + have h := Metric.tendsto_nhds.mp tendsto_E₄_atImInfty (1 / 2) (by norm_num only) + simpa only [one_div, dist_eq_norm] using h have h₂ : ∀ᶠ τ : ℍ in atImInfty, ‖E₆ τ - 1‖ < 1 / 2 := by - have h := Metric.tendsto_nhds.mp tendsto_E₆_atImInfty (1 / 2) (by norm_num) - simpa [dist_eq_norm] using h + have h := Metric.tendsto_nhds.mp tendsto_E₆_atImInfty (1 / 2) (by norm_num only) + simpa only [one_div, dist_eq_norm] using h have h₃ : ∀ᶠ τ : ℍ in atImInfty, ‖(J τ)⁻¹‖ < 1 := by have h := Metric.tendsto_nhds.mp tendsto_invJ 1 one_pos - simpa [dist_eq_norm] using h + simpa only [norm_inv, dist_eq_norm, sub_zero] using h have h₄ : ∀ᶠ τ : ℍ in atImInfty, ‖XhC ↑τ - 1‖ < 1 / 2 := by - have h := Metric.tendsto_nhds.mp tendsto_XhC (1 / 2) (by norm_num) - simpa [dist_eq_norm] using h + have h := Metric.tendsto_nhds.mp tendsto_XhC (1 / 2) (by norm_num only) + simpa only [one_div, dist_eq_norm] using h have h₅ : ∀ᶠ τ : ℍ in atImInfty, ‖m22 τ + 1‖ < 1 / 2 := by - have h := Metric.tendsto_nhds.mp tendsto_m22 (1 / 2) (by norm_num) - simpa [dist_eq_norm, sub_neg_eq_add] using h + have h := Metric.tendsto_nhds.mp tendsto_m22 (1 / 2) (by norm_num only) + simpa only [one_div, dist_eq_norm, sub_neg_eq_add] using h filter_upwards [h₁, h₂, h₃, h₄, h₅] with τ k₁ k₂ k₃ k₄ k₅ exact ⟨near_one_slitPlane k₁, near_one_ne_zero k₂, J_ne_zero (near_one_ne_zero k₁), k₃, near_one_ne_zero k₄, re_le_neg_half k₅⟩ @@ -659,7 +661,7 @@ private lemma E₄_ne_zero_of_mem_Region {τ : ℍ} (hτ : τ ∈ Region) : E₄ have hq3 : ‖q τ‖ ^ 3 ≤ (0.000389 : ℝ) ^ 3 := pow_le_pow_left₀ hqpos.le hq.le 3 intro h0 rw [h0, zero_sub, norm_neg] at h2 - nlinarith [hq3] + linarith [hq3] private lemma im_add_vert (z₀ : ℂ) (t : ℝ) : (z₀ + ↑t * Complex.I).im = z₀.im + t := by simp [Complex.add_im, Complex.mul_im] @@ -712,7 +714,8 @@ private lemma WrC_eq_zero {A : ℝ} (hA : 2 ≤ A) exact coe_ofComplex (him t ht) rw [hcoe] at hW have hline : HasDerivAt (fun w : ℂ => z₀ + w * Complex.I) Complex.I ((t : ℝ) : ℂ) := by - simpa using ((hasDerivAt_id ((t : ℝ) : ℂ)).mul_const Complex.I).const_add z₀ + simpa only [hasDerivAt_const_add_iff, id_eq, + one_mul] using ((hasDerivAt_id ((t : ℝ) : ℂ)).mul_const Complex.I).const_add z₀ have hcc := hW.comp ((t : ℝ) : ℂ) hline have hcomp : HasDerivAt (fun s : ℝ => WrC (z₀ + ↑s * Complex.I)) (2 * ↑π * Complex.I * (m22 σ * WrC (z₀ + ↑t * Complex.I)) * Complex.I) t := @@ -731,43 +734,27 @@ private lemma WrC_eq_zero {A : ℝ} (hA : 2 ≤ A) rwa [show -(2 * ↑π) * (m22 (ofComplex (z₀ + ↑t * Complex.I)) * WrC (z₀ + ↑t * Complex.I)) = (-(2 * ↑π) * m22 (ofComplex (z₀ + ↑t * Complex.I))) * WrC (z₀ + ↑t * Complex.I) from (mul_assoc _ _ _).symm, real_inner_mul_self] at h - -- the weighted modulus `g(t) = r(t)·e^{-2πt}` and its monotonicity - have hgd : ∀ t : ℝ, 0 ≤ t → - HasDerivAt (fun s : ℝ => ‖WrC (z₀ + ↑s * Complex.I)‖ ^ 2 * Real.exp (-(2 * π) * s)) - (2 * ((-(2 * ↑π) * m22 (ofComplex (z₀ + ↑t * Complex.I))).re - * ‖WrC (z₀ + ↑t * Complex.I)‖ ^ 2) * Real.exp (-(2 * π) * t) - + ‖WrC (z₀ + ↑t * Complex.I)‖ ^ 2 * (-(2 * π) * Real.exp (-(2 * π) * t))) t := by - intro t ht - have hexp : HasDerivAt (fun s : ℝ => Real.exp (-(2 * π) * s)) - (-(2 * π) * Real.exp (-(2 * π) * t)) t := by - have h1 : HasDerivAt (fun s : ℝ => -(2 * π) * s) (-(2 * π)) t := by - simpa using (hasDerivAt_id t).const_mul (-(2 * π)) - have h2 := (Real.hasDerivAt_exp (-(2 * π) * t)).comp t h1 - rw [show Real.exp (-(2 * π) * t) * (-(2 * π)) - = -(2 * π) * Real.exp (-(2 * π) * t) from mul_comm _ _] at h2 - exact h2 - exact (hrd t ht).mul hexp - have hmono : MonotoneOn (fun s : ℝ => ‖WrC (z₀ + ↑s * Complex.I)‖ ^ 2 - * Real.exp (-(2 * π) * s)) (Set.Ici (0 : ℝ)) := by + -- The squared modulus is nondecreasing along the vertical ray. + have hmono : MonotoneOn (fun s : ℝ => ‖WrC (z₀ + ↑s * Complex.I)‖ ^ 2) + (Set.Ici (0 : ℝ)) := by apply monotoneOn_of_deriv_nonneg (convex_Ici 0) - · exact fun s hs => ((hgd s hs).continuousAt).continuousWithinAt + · exact fun s hs => ((hrd s hs).continuousAt).continuousWithinAt · rw [interior_Ici] - exact fun s hs => (hgd s (le_of_lt hs)).differentiableAt.differentiableWithinAt + exact fun s hs => (hrd s (le_of_lt hs)).differentiableAt.differentiableWithinAt · rw [interior_Ici] intro s hs - rw [(hgd s (le_of_lt hs)).deriv] + rw [(hrd s (le_of_lt hs)).deriv] obtain ⟨_, _, _, _, _, hre⟩ := hgood (ofComplex (z₀ + ↑s * Complex.I)) (himA s (le_of_lt hs)) - have h1 : (0 : ℝ) ≤ ‖WrC (z₀ + ↑s * Complex.I)‖ ^ 2 := by positivity - have h2 : (0 : ℝ) < Real.exp (-(2 * π) * s) := Real.exp_pos _ - have h3 : (-(2 * ↑π) * m22 (ofComplex (z₀ + ↑s * Complex.I))).re + have hreal : (-(2 * ↑π) * m22 (ofComplex (z₀ + ↑s * Complex.I))).re = -(2 * π) * (m22 (ofComplex (z₀ + ↑s * Complex.I))).re := by rw [show (-(2 * ↑π) : ℂ) = ((-(2 * π) : ℝ) : ℂ) from by push_cast; ring, Complex.re_ofReal_mul] - rw [h3] - have key : (0 : ℝ) ≤ -(4 * π * (m22 (ofComplex (z₀ + ↑s * Complex.I))).re) - 2 * π := by - nlinarith only [hre, Real.pi_pos] - linear_combination mul_nonneg (mul_nonneg h1 h2.le) key + rw [hreal] + have hnonneg : 0 ≤ -(2 * π) * (m22 (ofComplex (z₀ + ↑s * Complex.I))).re := + mul_nonneg_of_nonpos_of_nonpos (neg_nonpos.mpr (by positivity)) + (hre.trans (by norm_num only)) + exact mul_nonneg (by norm_num only) (mul_nonneg hnonneg (sq_nonneg _)) -- `ψ → 0` along the ray, so `r → 0` have hψ0 : Tendsto (fun t : ℝ => WrC (z₀ + ↑t * Complex.I)) atTop (𝓝 0) := by have h := tendsto_WrC.comp (tendsto_vertical hz₀im) @@ -777,21 +764,14 @@ private lemma WrC_eq_zero {A : ℝ} (hA : 2 ≤ A) rw [coe_ofComplex (him t ht)] have hr0 : Tendsto (fun t : ℝ => ‖WrC (z₀ + ↑t * Complex.I)‖ ^ 2) atTop (𝓝 0) := by have h := (hψ0.norm).pow 2 - simpa using h - -- squeeze: `g 0 ≤ g t ≤ r t → 0` - have hg0 : ‖WrC (z₀ + ↑(0 : ℝ) * Complex.I)‖ ^ 2 * Real.exp (-(2 * π) * 0) ≤ 0 := by - have hle : ∀ᶠ t : ℝ in atTop, - ‖WrC (z₀ + ↑(0 : ℝ) * Complex.I)‖ ^ 2 * Real.exp (-(2 * π) * 0) - ≤ ‖WrC (z₀ + ↑t * Complex.I)‖ ^ 2 := by - filter_upwards [eventually_ge_atTop (0 : ℝ)] with t ht - have hmt := hmono Set.self_mem_Ici (Set.mem_Ici.mpr ht) ht - have hexp1 : Real.exp (-(2 * π) * t) ≤ 1 := by - apply Real.exp_le_one_iff.mpr - exact mul_nonpos_of_nonpos_of_nonneg (neg_nonpos.mpr (by positivity)) ht - exact hmt.trans (mul_le_of_le_one_right (sq_nonneg _) hexp1) - exact ge_of_tendsto hr0 hle + simpa only [norm_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow] using h + -- A nondecreasing nonnegative function tending to zero vanishes at the origin. + have hg0 : ‖WrC (z₀ + ↑(0 : ℝ) * Complex.I)‖ ^ 2 ≤ 0 := by + apply ge_of_tendsto hr0 + filter_upwards [eventually_ge_atTop (0 : ℝ)] with t ht + exact hmono Set.self_mem_Ici (Set.mem_Ici.mpr ht) ht have hz : WrC (z₀ + ↑(0 : ℝ) * Complex.I) = WrC z₀ := by norm_num - rw [hz, mul_zero, Real.exp_zero, mul_one] at hg0 + rw [hz] at hg0 have hnorm : ‖WrC z₀‖ = 0 := sq_eq_zero_iff.mp (le_antisymm hg0 (sq_nonneg _)) exact norm_eq_zero.mp hnorm @@ -846,7 +826,7 @@ private lemma XtC_eq_XhC {A : ℝ} (hA : 2 ≤ A) have hray : Tendsto (fun t : ℝ => XtC (z + ↑t * Complex.I) / XhC (z + ↑t * Complex.I)) atTop (𝓝 1) := by have h := (tendsto_XtC.div tendsto_XhC one_ne_zero).comp (tendsto_vertical hz0) - norm_num at h + norm_num only at h refine h.congr' ?_ filter_upwards [eventually_ge_atTop (0 : ℝ)] with t ht have him : 0 < (z + ↑t * Complex.I).im := by diff --git a/LeanPool/Chudnovsky/Liouville.lean b/LeanPool/Chudnovsky/Liouville.lean index 9d882110fa..ac2e4c5c89 100644 --- a/LeanPool/Chudnovsky/Liouville.lean +++ b/LeanPool/Chudnovsky/Liouville.lean @@ -283,7 +283,7 @@ private lemma finite_fundamentalParallelogram_inter {L : PeriodPair} {S : Set ≤ ‖s • L.ω₁‖ + ‖t • L.ω₂‖ := norm_add_le _ _ _ = |s| * ‖L.ω₁‖ + |t| * ‖L.ω₂‖ := by rw [norm_smul, norm_smul, Real.norm_eq_abs, Real.norm_eq_abs] - _ ≤ ‖L.ω₁‖ + ‖L.ω₂‖ := by nlinarith [norm_nonneg L.ω₁, norm_nonneg L.ω₂] + _ ≤ ‖L.ω₁‖ + ‖L.ω₂‖ := by nlinarith only [hs1, ht1, norm_nonneg L.ω₁, norm_nonneg L.ω₂] exact (Metric.finite_isBounded_inter_isClosed hdisc Metric.isBounded_closedBall hclosed).subset (Set.inter_subset_inter_left S hPsub) @@ -303,7 +303,7 @@ theorem IsEllipticWith.exists_eq_const_of_differentiable (hf : L.IsEllipticWith L.exists_sub_mem_lattice_of_mem_fundamentalParallelogram z have h := hf.2 (s • L.ω₁ + t • L.ω₂) ⟨z - (s • L.ω₁ + t • L.ω₂), hl⟩ rw [show (s • L.ω₁ + t • L.ω₂) + ((⟨z - (s • L.ω₁ + t • L.ω₂), hl⟩ : L.lattice) : ℂ) = z - from by simp] at h + from by simp only [Complex.real_smul, add_sub_cancel]] at h rw [h] exact hM (Set.mem_image_of_mem f ⟨(s, t), ⟨⟨hs.1, hs.2.le⟩, ⟨ht.1, ht.2.le⟩⟩, rfl⟩) @@ -372,7 +372,8 @@ private lemma integral_edge_eq_sub {f F : ℂ → ℂ} {p ω : ℂ} ∫ t in (0 : ℝ)..1, f (p + (t : ℂ) * ω) * ω = F (p + ω) - F p := by have hγ : ∀ t : ℝ, HasDerivAt (fun s : ℝ ↦ p + (s : ℂ) * ω) ω t := by intro t - simpa using ((Complex.ofRealCLM.hasDerivAt (x := t)).mul_const ω).const_add p + simpa only [hasDerivAt_const_add_iff, Complex.ofRealCLM_apply, Complex.ofReal_one, + one_mul] using ((Complex.ofRealCLM.hasDerivAt (x := t)).mul_const ω).const_add p have key : ∀ t ∈ Set.uIcc (0 : ℝ) 1, HasDerivAt (fun s : ℝ ↦ F (p + (s : ℂ) * ω)) (f (p + (t : ℂ) * ω) * ω) t := by intro t ht @@ -633,7 +634,8 @@ private lemma coord_eq_zero_of_eq_zero {L : PeriodPair} {r s : ℝ} have hli := Fintype.linearIndependent_iff.mp L.indep ![r, s] have hsum : ∑ i, (![r, s] i) • (![L.ω₁, L.ω₂] i) = 0 := by rw [Fin.sum_univ_two] - simpa [Complex.real_smul] using h + simpa only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, Matrix.cons_val_zero, + Complex.real_smul, Matrix.cons_val_one, Matrix.cons_val_fin_one] using h have hall := hli hsum exact ⟨hall 0, hall 1⟩ @@ -1255,7 +1257,7 @@ private lemma boundaryIntegral_principalPart {L : PeriodPair} {v c : ℂ} (a : intro k _ apply continuousOn_const.mul refine (continuousOn_id.sub continuousOn_const).zpow₀ _ (fun z hz => ?_) - exact Or.inl (by simpa using sub_ne_zero.2 (hbne z hz)) + exact Or.inl (by simpa only [Pi.sub_apply, id_eq, ne_eq] using sub_ne_zero.2 (hbne z hz)) rw [boundaryIntegral_finsetSum hterm] apply Finset.sum_eq_zero intro k _ @@ -1762,7 +1764,7 @@ theorem IsEllipticWith.sum_meromorphicOrderAt_eq_zero (hf : L.IsEllipticWith f) Chudnovsky.residue_eq_zero_of_analyticAt hana rw [hres z] at hz0 have huntop : (meromorphicOrderAt f z).untop₀ ≠ 0 := fun h => - hzord (by rw [← WithTop.coe_untop₀_of_ne_top (hforall z), h]; simp) + hzord (by rw [← WithTop.coe_untop₀_of_ne_top (hforall z), h]; simp only [WithTop.coe_zero]) exact huntop (by exact_mod_cast hz0) -- At the extra non-analyticity points the order (and hence the residue) is `0`. have hzero : ∀ z ∈ hg.finite_nonAnalytic.toFinset, @@ -1772,7 +1774,7 @@ theorem IsEllipticWith.sum_meromorphicOrderAt_eq_zero (hf : L.IsEllipticWith f) have hord0 : meromorphicOrderAt f z = 0 := by by_contra hne exact hznotin ⟨hz.1, hne⟩ - rw [hres z, hord0]; simp + rw [hres z, hord0]; simp only [WithTop.untop₀_zero, Int.cast_zero] have key : ∑ z ∈ (hf.finite_order_ne_zero h0).toFinset, Chudnovsky.residue (logDeriv f) z = 0 := by rw [Finset.sum_subset hsub hzero]; exact hsum0 @@ -1798,7 +1800,7 @@ private lemma codiscrete_add_preimage {S : Set ℂ} (l : ℂ) simp only [Set.mem_preimage, Set.mem_image] constructor · intro hz; exact ⟨z + l, hz, by ring⟩ - · rintro ⟨w, hw, rfl⟩; simpa using hw + · rintro ⟨w, hw, rfl⟩; simpa only [neg_add_cancel_right] using hw rw [hEq]; exact key /-- **Workhorse lemma** (used throughout the paper, e.g. in `pstrichprod`, diff --git a/LeanPool/Chudnovsky/MainTheorem.lean b/LeanPool/Chudnovsky/MainTheorem.lean index 895ac8ef45..754f82098e 100644 --- a/LeanPool/Chudnovsky/MainTheorem.lean +++ b/LeanPool/Chudnovsky/MainTheorem.lean @@ -117,9 +117,9 @@ theorem summable_mainSummand {τ : ℍ} (hτ : τ ∈ Region) : have hqb : ‖q τ‖ < 0.000389 := lt_trans (norm_q_lt_of_mem_Region hτ) exp_neg_bound have hM : (1728 : ℝ) < M := by have h1 : (1728 : ℝ) < 0.737 / ‖q τ‖ := by - rw [lt_div_iff₀ hqpos]; nlinarith [hqb, hqpos] + rw [lt_div_iff₀ hqpos]; linarith [hqb, hqpos] exact lt_trans h1 (theonaeherJ_lower hτ) - have hMpos : 0 < M := lt_trans (by norm_num) hM + have hMpos : 0 < M := lt_trans (by norm_num1) hM set r : ℝ := 1728 / M with hrdef have hr0 : 0 ≤ r := by rw [hrdef]; positivity have hr1 : r < 1 := by rw [hrdef, div_lt_one hMpos]; exact hM @@ -130,7 +130,7 @@ theorem summable_mainSummand {τ : ℍ} (hτ : τ ∈ Region) : have hgeom1 : Summable (fun n : ℕ => (n : ℝ) * r ^ n) := by have h := summable_pow_mul_geometric_of_norm_lt_one 1 (r := r) (by rw [Real.norm_eq_abs, abs_of_nonneg hr0]; exact hr1) - simpa using h + simpa only [pow_one] using h have hg : Summable (fun n : ℕ => (C + n) * r ^ n) := by have he : (fun n : ℕ => (C + (n : ℝ)) * r ^ n) = fun n : ℕ => C * r ^ n + (n : ℝ) * r ^ n := by ext n; ring @@ -143,7 +143,7 @@ theorem summable_mainSummand {τ : ℍ} (hτ : τ ∈ Region) : Complex.norm_natCast, div_le_iff₀ hden_pos] calc ((6 * n)! : ℝ) ≤ ((1728 ^ n * ((3 * n)! * (n !) ^ 3) : ℕ) : ℝ) := by exact_mod_cast factorial_ratio_le n - _ = 1728 ^ n * (((3 * n)! : ℝ) * ((n ! : ℝ)) ^ 3) := by push_cast; ring + _ = 1728 ^ n * (((3 * n)! : ℝ) * ((n ! : ℝ)) ^ 3) := by push_cast; ac_rfl have hA : ‖(1 - s₂ τ) / 6 + (n : ℂ)‖ ≤ C + n := by calc ‖(1 - s₂ τ) / 6 + (n : ℂ)‖ ≤ ‖(1 - s₂ τ) / 6‖ + ‖(n : ℂ)‖ := norm_add_le _ _ _ = C + n := by rw [Complex.norm_natCast, hCdef] @@ -175,7 +175,7 @@ theorem sq_eq_on_preconnected_eq {X : Type*} [TopologicalSpace X] {s : Set X} have h : IsClosed {x : s | (fun x : s => f x + g x) x = 0} := isClosed_eq (hfc.add hgc) continuous_const convert h using 2 with x - simp [eq_neg_iff_add_eq_zero] + simp only [eq_neg_iff_add_eq_zero] -- `A ∪ B = univ` since `(f - g)(f + g) = f² - g² = 0`. have hcover : A ∪ B = Set.univ := by ext x @@ -205,7 +205,7 @@ theorem sq_eq_on_preconnected_eq {X : Type*} [TopologicalSpace X] {s : Set X} hAclopen.eq_univ ⟨⟨x₀, hx₀⟩, h₀⟩ intro x hx have : (⟨x, hx⟩ : s) ∈ A := hAuniv ▸ Set.mem_univ _ - simpa [hA] using this + simpa only [hA, Set.mem_ofPred_eq] using this /-- The region `Im τ > 1.25` is preconnected. -/ theorem isPreconnected_Region : IsPreconnected (Region : Set ℍ) := by @@ -264,10 +264,10 @@ private lemma hasDerivAt_tsum_mainCoeff {z : ℂ} (hz : ‖z‖ < 1) : have h : Summable fun n : ℕ => (n : ℝ) * ρ ^ n := by have := summable_pow_mul_geometric_of_norm_lt_one (R := ℝ) 1 (r := ρ) (by rw [Real.norm_eq_abs, abs_of_nonneg hρpos.le]; exact hρ1) - simpa using this + simpa only [pow_one] using this refine (h.mul_left ρ⁻¹).congr fun n => ?_ rcases n with _ | k - · simp + · simp only [CharP.cast_eq_zero, pow_zero, mul_one, mul_zero, zero_tsub] · rw [Nat.succ_sub_one, pow_succ] push_cast field_simp @@ -429,7 +429,7 @@ private lemma norm_E₆_sub_one_le {τ : ℍ} (hτ : τ ∈ Region) : ‖E₆ τ rw [heq] refine le_trans (norm_sub_le _ _) ?_ rw [norm_neg, norm_mul, norm_mul, Complex.norm_ofNat] - nlinarith [norm_nonneg (eisensteinTail 5 3 τ), pow_pos hQpos 2, pow_pos hQpos 3] + nlinarith only [hQ, htail, hqq, pow_pos hQpos 3] /-- If `a` is closer to `b` than `b` is to `0`, then `a/b` lies in the right half-plane. -/ private lemma re_div_pos_of_norm_sub_lt {a b : ℂ} (hb : ‖a - b‖ < ‖b‖) : 0 < (a / b).re := by @@ -439,7 +439,7 @@ private lemma re_div_pos_of_norm_sub_lt {a b : ℂ} (hb : ‖a - b‖ < ‖b‖) have h2 : ‖a / b - 1‖ < 1 := by rw [h1, norm_div, div_lt_one hbn]; exact hb have h3 : |(a / b - 1).re| ≤ ‖a / b - 1‖ := Complex.abs_re_le_norm _ - have h4 : (a / b - 1).re = (a / b).re - 1 := by simp + have h4 : (a / b - 1).re = (a / b).re - 1 := by simp only [sub_re, one_re] have h5 := (abs_le.mp h3).1 linarith @@ -585,13 +585,13 @@ theorem thm42 {τ : ℍ} (hτ : τ ∈ Region) : -- basic non-vanishing facts have hJnorm : (1.096 : ℝ) < ‖J τ‖ := theonaeherJ_norm_J hτ have hJ0 : J τ ≠ 0 := by - intro h; rw [h, norm_zero] at hJnorm; norm_num at hJnorm + intro h; rw [h, norm_zero] at hJnorm; norm_num only at hJnorm have hden : E₄ τ ^ 3 - E₆ τ ^ 2 ≠ 0 := E₄_cube_sub_E₆_sq_ne_zero τ have hE₄0 : E₄ τ ≠ 0 := by intro h apply hJ0 rw [J, h] - simp + simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, zero_sub, zero_div] have hE₆0 : E₆ τ ≠ 0 := E₆_ne_zero_of_mem_Region hτ have hπ0 : (π : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr Real.pi_ne_zero have him0 : ((τ.im : ℝ) : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr (ne_of_gt τ.im_pos) @@ -613,17 +613,13 @@ theorem thm42 {τ : ℍ} (hτ : τ ∈ Region) : rw [hone] have hG : HasDerivAt hyp2F1 (deriv hyp2F1 (J τ)⁻¹) (J τ)⁻¹ := (hyp2F1_analyticAt hu).differentiableAt.hasDerivAt - have h2 : deriv (fun w => hyp2F1 w ^ 2) (J τ)⁻¹ = - (2 : ℕ) * hyp2F1 (J τ)⁻¹ ^ (2 - 1) * deriv hyp2F1 (J τ)⁻¹ := (hG.pow 2).deriv - rw [h2] - norm_num + simpa only [Nat.cast_ofNat, Nat.reduceSub, pow_one] using (hG.fun_pow 2).deriv -- `J/(J−1)` is the square of `G⁶/E₆` have hsq : J τ / (J τ - 1) = (hyp2F1 (J τ)⁻¹ ^ 6 / E₆ τ) ^ 2 := by have hJ1 : J τ - 1 ≠ 0 := by intro h - have h2 : (J τ - 1) * (E₄ τ ^ 3 - E₆ τ ^ 2) = E₆ τ ^ 2 := by linear_combination hJmul - rw [h, zero_mul] at h2 - exact hE₆0 (pow_eq_zero_iff (n := 2) (by norm_num) |>.mp h2.symm) + rw [sub_eq_zero.mp h, norm_one] at hJnorm + norm_num1 at hJnorm have hJmul' := hJmul rw [hE₄] at hJmul' rw [div_pow, div_eq_div_iff hJ1 (pow_ne_zero 2 hE₆0)] @@ -631,8 +627,8 @@ theorem thm42 {τ : ℍ} (hτ : τ ∈ Region) : -- positivity of `Re(G⁶/E₆)`: quantitative bounds have hznorm : ‖(J τ)⁻¹‖ ≤ 0.9125 := by rw [norm_inv] - have h2 : (1.096 : ℝ)⁻¹ ≤ 0.9125 := by norm_num - exact le_trans (inv_anti₀ (by norm_num) hJnorm.le) h2 + have h2 : (1.096 : ℝ)⁻¹ ≤ 0.9125 := by norm_num only + exact le_trans (inv_anti₀ (by norm_num only) hJnorm.le) h2 have hb2 : ‖hyp2F1 (J τ)⁻¹ ^ 2 - 1‖ ≤ 0.15 := norm_Gsq_sub_one_le hznorm have hb6 : ‖hyp2F1 (J τ)⁻¹ ^ 6 - 1‖ ≤ 0.520875 := by have hexp : hyp2F1 (J τ)⁻¹ ^ 6 - 1 = @@ -642,7 +638,7 @@ theorem thm42 {τ : ℍ} (hτ : τ ∈ Region) : refine le_trans (norm_add_le _ _) (le_trans (add_le_add (norm_add_le _ _) le_rfl) ?_) rw [norm_pow, norm_mul, norm_mul, Complex.norm_ofNat, norm_pow] have h0 : (0 : ℝ) ≤ ‖hyp2F1 (J τ)⁻¹ ^ 2 - 1‖ := norm_nonneg _ - nlinarith [hb2] + nlinarith only [hb2, h0] have hE₆b : ‖E₆ τ - 1‖ ≤ 0.199 := norm_E₆_sub_one_le hτ have hE₆big : (0.8 : ℝ) < ‖E₆ τ‖ := lemE6 hτ have hsub : ‖hyp2F1 (J τ)⁻¹ ^ 6 - E₆ τ‖ < ‖E₆ τ‖ := by @@ -652,25 +648,21 @@ theorem thm42 {τ : ℍ} (hτ : τ ∈ Region) : calc ‖(hyp2F1 (J τ)⁻¹ ^ 6 - 1) - (E₆ τ - 1)‖ ≤ ‖hyp2F1 (J τ)⁻¹ ^ 6 - 1‖ + ‖E₆ τ - 1‖ := norm_sub_le _ _ _ ≤ 0.520875 + 0.199 := add_le_add hb6 hE₆b - _ < 0.8 := by norm_num + _ < 0.8 := by norm_num only _ < ‖E₆ τ‖ := hE₆big have hre : 0 < (hyp2F1 (J τ)⁻¹ ^ 6 / E₆ τ).re := re_div_pos_of_norm_sub_lt hsub -- resolve the branch of the square root have hbranch : (J τ / (J τ - 1)) ^ (1 / 2 : ℂ) = hyp2F1 (J τ)⁻¹ ^ 6 / E₆ τ := by - rw [hsq, show (1 / 2 : ℂ) = ((2 : ℂ)⁻¹ : ℂ) by norm_num] + rw [hsq, show (1 / 2 : ℂ) = ((2 : ℂ)⁻¹ : ℂ) by norm_num only] exact Complex.sq_cpow_two_inv hre - -- solve the E₂ identity for `E2 τ` and substitute everything - have hE2' : E2 τ = (E₆ τ * (E₄ τ * J τ) + - 12 * hyp2F1 (J τ)⁻¹ ^ 3 * deriv hyp2F1 (J τ)⁻¹ * E₆ τ) / (E₄ τ ^ 2 * J τ) := by - rw [eq_div_iff (mul_ne_zero (pow_ne_zero 2 hE₄0) hJ0)] - exact hE2 rw [hbranch, hderivsq, hone] simp only [s₂, E₂star] - rw [hE2', hE₄] - set g : ℂ := hyp2F1 (J τ)⁻¹ with hgdef - set g' : ℂ := deriv hyp2F1 (J τ)⁻¹ with hg'def - field_simp - ring + rw [hE₄] at hE2 ⊢ + -- Multiply by the square so the differential identity applies directly. + apply mul_left_cancel₀ (pow_ne_zero 2 hG0) + field_simp (disch := first | assumption | norm_num1 | positivity) + simp only [one_div] + linear_combination (2 * (π : ℂ) * (τ.im : ℂ)) * hE2 /-- **The Main Theorem** (Milla, Thm. `hauptformel`; Chudnovsky–Chudnovsky 1988, Eq. (1.4)): for all `τ` with `Im τ > 1.25`, @@ -683,7 +675,7 @@ theorem hauptformel {τ : ℍ} (hτ : τ ∈ Region) : have hJ0 : J τ ≠ 0 := by intro h rw [h, norm_zero] at hJ - exact absurd hJ (by norm_num) + exact absurd hJ (by norm_num1) have hw : ‖1 / J τ‖ < 1 := by rw [norm_div, norm_one, div_lt_one (lt_trans one_pos hJ)] exact hJ @@ -701,12 +693,12 @@ theorem hauptformel {τ : ℍ} (hτ : τ ∈ Region) : refine Summable.of_norm_bounded (g := fun n : ℕ => (n : ℝ) * ‖w‖ ^ n) ?_ fun n => ?_ · have := summable_pow_mul_geometric_of_norm_lt_one (R := ℝ) 1 (r := ‖w‖) (by rw [Real.norm_eq_abs, abs_of_nonneg (norm_nonneg w)]; exact hw) - simpa using this + simpa only [pow_one] using this · rw [norm_mul, norm_mul, norm_pow, Complex.norm_natCast] calc (n : ℝ) * (‖mainCoeff n‖ * ‖w‖ ^ n) ≤ (n : ℝ) * (1 * ‖w‖ ^ n) := by gcongr exact norm_mainCoeff_le_one n - _ = (n : ℝ) * ‖w‖ ^ n := by ring + _ = (n : ℝ) * ‖w‖ ^ n := by ac_rfl rw [thm42 hτ, Gsq_eq_tsum hw, deriv_Gsq_eq hw, ← hwdef] -- Push the constants into the sums. rw [← tsum_mul_left, ← tsum_mul_left] @@ -714,10 +706,10 @@ theorem hauptformel {τ : ℍ} (hτ : τ ∈ Region) : = fun n : ℕ => (n : ℂ) * (mainCoeff n * w ^ n) := by ext n rcases n with _ | k - · simp + · simp only [CharP.cast_eq_zero, zero_tsub, pow_zero, mul_one, mul_zero, zero_mul] · rw [Nat.succ_sub_one, pow_succ] push_cast - ring + ac_rfl rw [hstep] rw [← (hS0.mul_left ((1 - s₂ τ) / 6)).tsum_add hS1] refine tsum_congr fun n => ?_ diff --git a/LeanPool/Chudnovsky/NumericalBounds.lean b/LeanPool/Chudnovsky/NumericalBounds.lean new file mode 100644 index 0000000000..478937a6cd --- /dev/null +++ b/LeanPool/Chudnovsky/NumericalBounds.lean @@ -0,0 +1,171 @@ +/- +Copyright (c) 2026 Xuanji Li and Lean Pool contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Xuanji Li, Lean Pool contributors +-/ +module + +public import Mathlib.Basic.Real.Basic +import Mathlib.Data.Rat.Cast.Order +import Mathlib.Tactic.Linarith.Frontend +import Mathlib.Tactic.NormNum.Abs +import Mathlib.Tactic.NormNum.DivMod +import Mathlib.Tactic.NormNum.OfScientific +import Mathlib.Tactic.Ring.RingNF + +/-! +# Real interval certificates for the Chudnovsky coefficients + +Prove the numeric enclosures independently of the modular-form and lattice developments. +Rounded coefficient and factor intervals keep the arithmetic certificates small. +-/ + +public section + +namespace Chudnovsky.NumericalBounds + +/-- Enclose the real approximation to the singular j-value within half a unit. -/ +theorem jwert_real_bound {e : ℝ} + (hL : (3.80898093700765233822623151647e-18 : ℝ) < e) + (hU : e < (3.80898093700765233822623151648e-18 : ℝ)) : + |(1 - 240 * e + 2160 * e ^ 2) ^ 3 / (e * (1 + e - e ^ 2) ^ 24) - 640320 ^ 3| < 1 / 2 := by + -- The final tolerance is one half, so coarse rational enclosures suffice. + have hL : (3.808980937007652338e-18 : ℝ) < e := lt_trans (by norm_num1) hL + have hU : e < (3.808980937007652339e-18 : ℝ) := lt_trans hU (by norm_num1) + have hepos : 0 < e := lt_trans (by norm_num1) hL + have he2U : e ^ 2 ≤ (3.808980937007652339e-18 : ℝ) ^ 2 := + pow_le_pow_left₀ hepos.le hU.le 2 + have he2nn : 0 ≤ e ^ 2 := sq_nonneg e + -- enclosures for `g = 1 - 240e + 2160e²` + have hGLg : (1 - 240 * 3.808980937007652339e-18 : ℝ) + ≤ 1 - 240 * e + 2160 * e ^ 2 := by linarith only [hU, he2nn] + have hgGH : 1 - 240 * e + 2160 * e ^ 2 ≤ + (1 - 240 * 3.808980937007652338e-18 + + 2160 * (3.808980937007652339e-18) ^ 2 : ℝ) := by linarith only [hL, he2U] + have hGLpos : (0 : ℝ) < 1 - 240 * 3.808980937007652339e-18 := by norm_num1 + have hgpos : 0 < 1 - 240 * e + 2160 * e ^ 2 := lt_of_lt_of_le hGLpos hGLg + -- enclosures for `h = 1 + e - e²` + have hHLh : (1 + 3.808980937007652338e-18 + - (3.808980937007652339e-18) ^ 2 : ℝ) ≤ 1 + e - e ^ 2 := by + linarith only [hL, he2U] + have hhHH : 1 + e - e ^ 2 ≤ (1 + 3.808980937007652339e-18 : ℝ) := by + linarith only [hU, he2nn] + have hHLpos : (0 : ℝ) < 1 + 3.808980937007652338e-18 + - (3.808980937007652339e-18) ^ 2 := by norm_num1 + have hhpos : 0 < 1 + e - e ^ 2 := lt_of_lt_of_le hHLpos hHLh + -- cube / 24-th power the enclosures + have hN_hi : (1 - 240 * e + 2160 * e ^ 2) ^ 3 ≤ + (1 - 240 * 3.808980937007652338e-18 + + 2160 * (3.808980937007652339e-18) ^ 2) ^ 3 := + pow_le_pow_left₀ hgpos.le hgGH 3 + have hN_lo : (1 - 240 * 3.808980937007652339e-18) ^ 3 + ≤ (1 - 240 * e + 2160 * e ^ 2) ^ 3 := pow_le_pow_left₀ hGLpos.le hGLg 3 + have hW_hi : (1 + e - e ^ 2) ^ 24 ≤ (1 + 3.808980937007652339e-18) ^ 24 := + pow_le_pow_left₀ hhpos.le hhHH 24 + have hW_lo : (1 + 3.808980937007652338e-18 + - (3.808980937007652339e-18) ^ 2) ^ 24 ≤ (1 + e - e ^ 2) ^ 24 := + pow_le_pow_left₀ hHLpos.le hHLh 24 + -- the two division enclosures of `S` + have hden_pos : 0 < e * (1 + e - e ^ 2) ^ 24 := mul_pos hepos (pow_pos hhpos 24) + have hSupper : (1 - 240 * e + 2160 * e ^ 2) ^ 3 / (e * (1 + e - e ^ 2) ^ 24) ≤ + (1 - 240 * 3.808980937007652338e-18 + + 2160 * (3.808980937007652339e-18) ^ 2) ^ 3 / + (3.808980937007652338e-18 * + (1 + 3.808980937007652338e-18 + - (3.808980937007652339e-18) ^ 2) ^ 24) := by + apply div_le_div₀ (by positivity) hN_hi + (mul_pos (by norm_num1) (pow_pos hHLpos 24)) + exact mul_le_mul hL.le hW_lo (pow_nonneg hHLpos.le 24) hepos.le + have hSlower : (1 - 240 * 3.808980937007652339e-18) ^ 3 / + (3.808980937007652339e-18 * + (1 + 3.808980937007652339e-18) ^ 24) ≤ + (1 - 240 * e + 2160 * e ^ 2) ^ 3 / (e * (1 + e - e ^ 2) ^ 24) := by + apply div_le_div₀ (by positivity) hN_lo hden_pos + exact mul_le_mul hU.le hW_hi (pow_nonneg hhpos.le 24) (by norm_num1) + -- the two heavy rational inequalities + have hUpNum : (1 - 240 * 3.808980937007652338e-18 + + 2160 * (3.808980937007652339e-18) ^ 2) ^ 3 / + (3.808980937007652338e-18 * + (1 + 3.808980937007652338e-18 + - (3.808980937007652339e-18) ^ 2) ^ 24) < (640320 : ℝ) ^ 3 + 1 / 2 := by + norm_num1 + have hLoNum : (640320 : ℝ) ^ 3 - 1 / 2 < + (1 - 240 * 3.808980937007652339e-18) ^ 3 / + (3.808980937007652339e-18 * + (1 + 3.808980937007652339e-18) ^ 24) := by + norm_num1 + rw [abs_lt] + exact ⟨by linarith only [hLoNum.trans_le hSlower], + by linarith only [hSupper.trans_lt hUpNum]⟩ + +/-- Enclose the scaled real approximation to `s₂` within half a unit. -/ +theorem s2tilde_real_bound {e pv sv : ℝ} + (heL : (3.80898093700765233822623151647e-18 : ℝ) < e) + (heU : e < (3.80898093700765233822623151648e-18 : ℝ)) + (hpL : (3.14159265358979323846 : ℝ) < pv) (hpU : pv < (3.14159265358979323847 : ℝ)) + (hsL : (12.7671453348037046617 : ℝ) < sv) (hsU : sv < (12.7671453348037046618 : ℝ)) : + |(1 - 240 * e + 2160 * e ^ 2) / (1 + 504 * e - 16632 * e ^ 2) + * (1 + 24 * e - 72 * e ^ 2 - 3 / (pv * (sv / 2))) * 10996566783048 + - 9351571368960| < 1 / 2 := by + have heL : (3e-18 : ℝ) < e := lt_trans (by norm_num1) heL + have heU : e < (4e-18 : ℝ) := lt_trans heU (by norm_num1) + have hpL : (3.14159265358979 : ℝ) < pv := lt_trans (by norm_num1) hpL + have hpU : pv < (3.14159265358980 : ℝ) := lt_trans hpU (by norm_num1) + have hsL : (12.7671453348037 : ℝ) < sv := lt_trans (by norm_num1) hsL + have hsU : sv < (12.7671453348038 : ℝ) := lt_trans hsU (by norm_num1) + have hepos : 0 < e := lt_trans (by norm_num1) heL + have hp_pos : 0 < pv := lt_trans (by norm_num1) hpL + have hs_pos : 0 < sv := lt_trans (by norm_num1) hsL + have he2U : e ^ 2 ≤ (4e-18 : ℝ) ^ 2 := pow_le_pow_left₀ hepos.le heU.le 2 + have he2nn : 0 ≤ e ^ 2 := sq_nonneg e + have hdenpos : 0 < 1 + 504 * e - 16632 * e ^ 2 := by linarith only [heL, he2U] + let R := (1 - 240 * e + 2160 * e ^ 2) / (1 + 504 * e - 16632 * e ^ 2) + let Z := 1 + 24 * e - 72 * e ^ 2 - 3 / (pv * (sv / 2)) + change |R * Z * 10996566783048 - 9351571368960| < 1 / 2 + -- Round the first factor near one before combining the interval estimates. + have hRL : (1 - 1e-14 : ℝ) ≤ R := by + apply (le_div_iff₀ hdenpos).mpr + linarith only [heU, he2nn] + have hRH : R ≤ (1 : ℝ) := by + apply (div_le_iff₀ hdenpos).mpr + linarith only [heL, he2U] + have hdivision : 3 / (pv * (sv / 2)) = 6 / (pv * sv) := by ring + have hwH : 6 / (pv * sv) ≤ (6 / (3.14159265358979 * 12.7671453348037) : ℝ) := + div_le_div_of_nonneg_left (by norm_num1) (by norm_num1) + (mul_le_mul hpL.le hsL.le (by norm_num1) hp_pos.le) + have hwL : (6 / (3.14159265358980 * 12.7671453348038) : ℝ) ≤ 6 / (pv * sv) := + div_le_div_of_nonneg_left (by norm_num1) (mul_pos hp_pos hs_pos) + (mul_le_mul hpU.le hsU.le hs_pos.le (by norm_num1)) + -- Enclose the second factor directly around the final rational value. + have hZL : (9351571368960 / 10996566783048 - 1e-14 : ℝ) ≤ Z := by + have hnumeric : (9351571368960 / 10996566783048 - 1e-14 : ℝ) + ≤ 1 + 24 * 3e-18 - 72 * (4e-18) ^ 2 + - 6 / (3.14159265358979 * 12.7671453348037) := by norm_num1 + dsimp [Z] + rw [hdivision] + linarith only [hnumeric, heL, he2U, hwH] + have hZH : Z ≤ (9351571368960 / 10996566783048 + 1e-14 : ℝ) := by + have hnumeric : (1 + 24 * 4e-18 + - 6 / (3.14159265358980 * 12.7671453348038) : ℝ) + ≤ 9351571368960 / 10996566783048 + 1e-14 := by norm_num1 + dsimp [Z] + rw [hdivision] + linarith only [hnumeric, heU, he2nn, hwL] + have hRnonneg : 0 ≤ R := le_trans (by norm_num1) hRL + have hZnonneg : 0 ≤ Z := le_trans (by norm_num1) hZL + have hlo := mul_le_mul_of_nonneg_right + (mul_le_mul hRL hZL (by norm_num1) hRnonneg) + (by norm_num1 : (0 : ℝ) ≤ 10996566783048) + have hhi := mul_le_mul_of_nonneg_right + (mul_le_mul hRH hZH hZnonneg (by norm_num1)) + (by norm_num1 : (0 : ℝ) ≤ 10996566783048) + have hlow : (9351571368960 : ℝ) - 1 / 2 + < (1 - 1e-14) * (9351571368960 / 10996566783048 - 1e-14) * 10996566783048 := by + norm_num1 + have hhigh : (1 : ℝ) * (9351571368960 / 10996566783048 + 1e-14) * 10996566783048 + < 9351571368960 + 1 / 2 := by norm_num1 + rw [abs_lt] + exact ⟨by linarith only [hlo, hlow], by linarith only [hhi, hhigh]⟩ + + +end Chudnovsky.NumericalBounds diff --git a/LeanPool/Chudnovsky/Periodicity.lean b/LeanPool/Chudnovsky/Periodicity.lean index 604b0f2f50..b4427398e9 100644 --- a/LeanPool/Chudnovsky/Periodicity.lean +++ b/LeanPool/Chudnovsky/Periodicity.lean @@ -25,13 +25,13 @@ lemma periodic_comp_ofComplex_of_vadd {f : ℍ → ℂ} (hf : ∀ τ : ℍ, f (( Periodic (f ∘ ofComplex) 1 := by intro w rcases lt_or_ge 0 w.im with hw | hw - · have hw1 : 0 < (w + 1).im := by simpa using hw + · have hw1 : 0 < (w + 1).im := by simpa only [add_im, one_im, add_zero] using hw simp only [comp_apply, ofComplex_apply_of_im_pos hw1, ofComplex_apply_of_im_pos hw] have h := hf ⟨w, hw⟩ convert h using 2 ext - simp [add_comm] - · have hw1 : (w + 1).im ≤ 0 := by simpa using hw + simp only [coe_vadd, ofReal_one, add_comm] + · have hw1 : (w + 1).im ≤ 0 := by simpa only [add_im, one_im, add_zero] using hw simp only [comp_apply] rw [ofComplex_apply_eq_of_im_nonpos hw1 (by simpa using hw)] diff --git a/LeanPool/Chudnovsky/Quasiperiods.lean b/LeanPool/Chudnovsky/Quasiperiods.lean index 5893642b2f..49c5850e75 100644 --- a/LeanPool/Chudnovsky/Quasiperiods.lean +++ b/LeanPool/Chudnovsky/Quasiperiods.lean @@ -58,10 +58,11 @@ private theorem weierstrassZeta_add_period (ω : ℂ) (hω : ω ∈ L.lattice) L.weierstrassZeta (z + ω) = L.weierstrassZeta z + 2 * L.weierstrassZeta (ω / 2) := by have hopen : IsOpen ((↑L.lattice : Set ℂ)ᶜ) := L.isClosed_lattice.isOpen_compl have hconn : IsPreconnected ((↑L.lattice : Set ℂ)ᶜ) := - (L.countable_lattice.isConnected_compl_of_one_lt_rank (by simp)).isPreconnected + (L.countable_lattice.isConnected_compl_of_one_lt_rank (by simp only [Complex.rank_real_complex, + Nat.one_lt_ofNat])).isPreconnected have hmem : ∀ {x : ℂ}, x ∉ L.lattice → x + ω ∉ L.lattice := by intro x hx hc - exact hx (by simpa using sub_mem hc hω) + exact hx (by simpa only [add_sub_cancel_right] using sub_mem hc hω) have hfdiff : DifferentiableOn ℂ (fun z ↦ L.weierstrassZeta (z + ω)) (↑L.lattice)ᶜ := L.differentiableOn_weierstrassZeta.comp (by fun_prop) (fun x hx ↦ hmem hx) have hgdiff : DifferentiableOn ℂ @@ -80,7 +81,7 @@ private theorem weierstrassZeta_add_period (ω : ℂ) (hω : ω ∈ L.lattice) have hx₀ : -(ω / 2) ∈ (↑L.lattice : Set ℂ)ᶜ := by change -(ω / 2) ∉ L.lattice intro hc - exact hω2 (by simpa using neg_mem hc) + exact hω2 (by simpa only [neg_neg] using neg_mem hc) have hval : L.weierstrassZeta (-(ω / 2) + ω) = L.weierstrassZeta (-(ω / 2)) + 2 * L.weierstrassZeta (ω / 2) := by rw [show -(ω / 2) + ω = ω / 2 by ring, L.weierstrassZeta_neg] @@ -248,7 +249,7 @@ private lemma hasSum_symmetricIco_D (τ : ℍ) (z : ℂ) (m : ℤ) : refine (tendsto_congr hpart).mpr ?_ have h1 := tendsto_zero_inv_linear C 1 have h2 := tendsto_zero_inv_linear_sub C 1 - simpa using h1.sub h2 + simpa only [one_mul, one_div, Int.cast_one, sub_self] using h1.sub h2 /-- The reindexing equivalence `ℤ × ℤ ≃ (L_τ).lattice`, `(m,n) ↦ m·τ + n`. -/ private def bridgeEqv (τ : ℍ) : ℤ × ℤ ≃ (Lτ τ).lattice := @@ -480,7 +481,8 @@ oriented basis (`0 < Im(ω₂/ω₁)`; for the opposite orientation the right-ha `-2πi`). -/ theorem legendre_relation (h : 0 < (L.ω₂ / L.ω₁).im) : L.eta₁ * L.ω₂ - L.eta₂ * L.ω₁ = 2 * (Real.pi : ℂ) * Complex.I := by - have hω₁ : L.ω₁ ≠ 0 := by simpa using L.indep.ne_zero 0 + have hω₁ : L.ω₁ ≠ 0 := by simpa only [ne_eq, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, + Matrix.cons_val_zero] using L.indep.ne_zero 0 set τ : ℍ := ⟨L.ω₂ / L.ω₁, h⟩ with hτdef set u : ℂˣ := Units.mk0 L.ω₁ hω₁ with hudef have huval : (u : ℂ) = L.ω₁ := Units.val_mk0 _ @@ -489,7 +491,7 @@ theorem legendre_relation (h : 0 < (L.ω₂ / L.ω₁).im) : apply PeriodPair.periodPair_eq · rw [PeriodPair.smulPP_ω₁, Chudnovsky.Lτ_ω₁, huval, mul_one] · rw [PeriodPair.smulPP_ω₂, Chudnovsky.Lτ_ω₂, huval, hτc] - field_simp + field_simp (disch := first | assumption | norm_num1 | positivity) have he1 : L.eta₁ = (u : ℂ)⁻¹ * (Chudnovsky.Lτ τ).eta₁ := by rw [hLeq]; exact PeriodPair.eta₁_smulPP u (Chudnovsky.Lτ τ) have he2 : L.eta₂ = (u : ℂ)⁻¹ * (Chudnovsky.Lτ τ).eta₂ := by @@ -500,7 +502,7 @@ theorem legendre_relation (h : 0 < (L.ω₂ / L.ω₁).im) : - (u : ℂ)⁻¹ * (Chudnovsky.Lτ τ).eta₂ * (u : ℂ) = (Chudnovsky.Lτ τ).eta₁ * (τ : ℂ) - (Chudnovsky.Lτ τ).eta₂ := by have hune : (u : ℂ) ≠ 0 := u.ne_zero - field_simp + field_simp (disch := first | assumption | norm_num1 | positivity) rw [he1, he2, hω2, ← huval, hrw] exact hlτ @@ -516,8 +518,8 @@ open scoped Real (paper `legendre` with `ω₁ = 1`, `ω₂ = τ`). -/ theorem legendre_Lτ (τ : ℍ) : (Lτ τ).eta₁ * τ - (Lτ τ).eta₂ = 2 * (π : ℂ) * Complex.I := by - have h := (Lτ τ).legendre_relation (by simpa using τ.im_pos) - simpa using h + have h := (Lτ τ).legendre_relation (by simpa only [Lτ_ω₂, Lτ_ω₁, div_one, coe_im] using τ.im_pos) + simpa only [Lτ_ω₂, Lτ_ω₁, mul_one] using h /-- The first quasiperiod of `L_τ` is the weight-2 Eisenstein series `G₂` in its Eisenstein summation order (Mathlib's `EisensteinSeries.G2`, summed over symmetric diff --git a/LeanPool/Chudnovsky/Ramanujan.lean b/LeanPool/Chudnovsky/Ramanujan.lean index 8858eee587..e23e39af6a 100644 --- a/LeanPool/Chudnovsky/Ramanujan.lean +++ b/LeanPool/Chudnovsky/Ramanujan.lean @@ -74,7 +74,7 @@ lemma deriv_eqOn_upperHalfPlaneSet {F G : ℂ → ℂ} (h : Set.EqOn F G upperHa /-! ### Transformation behaviour of `E₂` and of level-one modular forms under `T` and `S` -/ lemma E2_slash_T : E2 ∣[(2 : ℤ)] ModularGroup.T = E2 := by - simp [E2_slash_action, D2_T] + simp only [E2_slash_action, one_div, mul_inv_rev, D2_T, smul_zero, sub_zero] private lemma denom_T (τ : ℍ) : denom ModularGroup.T τ = 1 := by simp [ModularGroup.denom_apply, ModularGroup.coe_T] @@ -165,7 +165,7 @@ lemma tendsto_E2_atImInfty : Tendsto E2 atImInfty (𝓝 1) := by have hx0 : (0 : ℝ) ≤ ‖q τ‖ := norm_nonneg _ have hxr : ‖q τ‖ ≤ r := by rw [norm_q, hrdef, Real.exp_le_exp] - have := Real.pi_pos; nlinarith + have := Real.pi_pos; nlinarith only [him, this] have hE : E2 τ - 1 = -(24 * ∑' n : ℕ, (ArithmeticFunction.sigma 1 (n + 1) : ℂ) * q τ ^ (n + 1)) := by rw [E2_eq_one_sub_tsum τ]; ring @@ -301,7 +301,7 @@ lemma isZeroAtImInfty_normalizedDeriv (hper : Periodic (f ∘ ofComplex) 1) analyticAt_cuspFunction_zero one_pos hper hhol hbdd have hc : ContinuousAt (deriv (cuspFunction 1 f)) 0 := hana.deriv.continuousAt have hq0 : Tendsto (fun τ : ℍ ↦ q τ) atImInfty (𝓝 0) := by - simpa [q] using qParam_tendsto_atImInfty one_pos + simpa only [q] using qParam_tendsto_atImInfty one_pos have h : Tendsto (fun τ : ℍ ↦ q τ * deriv (cuspFunction 1 f) (q τ)) atImInfty (𝓝 (0 * deriv (cuspFunction 1 f) 0)) := hq0.mul ((hc.tendsto).comp hq0) @@ -375,7 +375,8 @@ lemma normalizedDeriv_S_smul_of_weight (hhol : MDiff f) {m : ℕ} have hd := deriv_comp_ofComplex_S hhol heq τ -- compute the derivative of the right-hand side have hp : HasDerivAt (fun w : ℂ ↦ w ^ (m + 1)) ((((m + 1) : ℕ) : ℂ) * (↑τ : ℂ) ^ m) ↑τ := by - simpa using hasDerivAt_pow (m + 1) (↑τ : ℂ) + simpa only [Nat.cast_add, Nat.cast_one, + add_tsub_cancel_right] using hasDerivAt_pow (m + 1) (↑τ : ℂ) have hΦ : HasDerivAt (fun w : ℂ ↦ w ^ (m + 1) * (f ∘ ofComplex) w) ((((m + 1) : ℕ) : ℂ) * (↑τ : ℂ) ^ m * (f ∘ ofComplex) ↑τ + (↑τ : ℂ) ^ (m + 1) * deriv (f ∘ ofComplex) ↑τ) ↑τ := @@ -412,7 +413,7 @@ lemma normalizedDeriv_E2_S_smul (τ : ℍ) : simp only [comp_apply, hofS, E2_S_smul ⟨w, hw⟩, ofComplex_apply_of_im_pos hw] have hd := deriv_comp_ofComplex_S E2_mdifferentiable heq τ have hp : HasDerivAt (fun w : ℂ ↦ w ^ 2) (2 * (↑τ : ℂ)) ↑τ := by - simpa using hasDerivAt_pow 2 (↑τ : ℂ) + simpa only [Nat.cast_ofNat, Nat.add_one_sub_one, pow_one] using hasDerivAt_pow 2 (↑τ : ℂ) have hlin : HasDerivAt (fun w : ℂ ↦ 6 / (π * I) * w) (6 / (π * I) * 1) ↑τ := (hasDerivAt_id (↑τ : ℂ)).const_mul (6 / (π * I) : ℂ) have hΦ : HasDerivAt (fun w : ℂ ↦ w ^ 2 * (E2 ∘ ofComplex) w + 6 / (π * I) * w) @@ -444,7 +445,7 @@ private lemma serreDerivative_slash_T {kc : ℂ} {f : ℍ → ℂ} {w : ℤ} rw [SL_slash_apply, denom_T, modular_T_smul] simp only [serreDerivative_apply] rw [normalizedDeriv_vadd_one (periodic_comp_ofComplex_of_vadd hf) τ, E2_vadd_one, hf] - simp + simp only [zpow_neg, one_zpow, inv_one, mul_one] /-- Boundedness at `i∞` of a Serre derivative. -/ private lemma isBoundedAtImInfty_serre {kc : ℂ} {f : ℍ → ℂ} @@ -475,7 +476,7 @@ private lemma tendsto_serre_atImInfty {kc : ℂ} {f : ℍ → ℂ} {a : ℂ} ((tendsto_const_nhds.mul tendsto_E2_atImInfty).mul hlim) have h := hD.sub h2 rw [serreDerivative_eq] - simpa using h + simpa only [mul_one, zero_sub] using h /-- Slash-invariance under `S` of `∂₄E₄` (weight 6). -/ private lemma serre_E₄_slash_S : @@ -604,16 +605,17 @@ private lemma E₄sq_ne_zero : E₄sq ≠ 0 := by rw [E₄sq_coe]; rfl rw [hcoe, qExpansion_mul_coeff_zero hana.continuousAt hana.continuousAt, h4, mul_one] rw [(ModularForm.qExpansion_eq_zero_iff one_pos one_mem_strictPeriods_SL E₄sq).mpr h] at h0 - simp at h0 + simp only [PowerSeries.coeff_zero_eq_constantCoeff, PowerSeries.constantCoeff_zero, + zero_ne_one] at h0 private lemma tendsto_E₄sq_atImInfty : Tendsto (⇑E₄sq) atImInfty (𝓝 1) := by rw [E₄sq_coe] - simpa using tendsto_E₄_atImInfty.mul tendsto_E₄_atImInfty + simpa only [mul_one] using tendsto_E₄_atImInfty.mul tendsto_E₄_atImInfty private lemma rank_eight : Module.rank ℂ (ModularForm 𝒮ℒ (8 : ℤ)) = 1 := by have h := ModularForm.dimension_level_one 8 (by decide) rw [ite_eq_right (by decide)] at h - simpa using h + simpa only [Nat.cast_ofNat, Nat.reduceDiv, zero_add, Nat.cast_one] using h /-- Extract the scalar from a rank-one comparison by taking limits at `i∞`. -/ private lemma smul_const_of_tendsto {k : ℤ} {e : ModularForm 𝒮ℒ k} {g : ℍ → ℂ} {c a b : ℂ} @@ -640,10 +642,10 @@ theorem serreDerivative_E₄_eq : serreDerivative 4 (⇑E₄) = fun τ : ℍ ↦ (ModularFormClass.bdd_at_infty E₄) tendsto_E₄_atImInfty) have hcval : c = -(3⁻¹) := by rw [mul_one] at hval - rw [hval]; norm_num + rw [hval]; norm_num1 funext τ rw [← hfun, hcval] - simp + simp only [_root_.neg_smul, neg_apply, smul_apply, smul_eq_mul, neg_mul] /-- The Serre-derivative form of Ramanujan's identity for `E₆`: `D E₆ - (1/2)·E₂·E₆ = -(1/2)·E₄²`. -/ @@ -659,11 +661,11 @@ theorem serreDerivative_E₆_eq : (ModularFormClass.bdd_at_infty E₆) tendsto_E₆_atImInfty) have hcval : c = -(2⁻¹) := by rw [mul_one] at hval - rw [hval]; norm_num + rw [hval]; norm_num1 funext τ have h := congr_fun hfun τ rw [← h, hcval] - simp [E₄sq_coe] + simp only [_root_.neg_smul, neg_apply, smul_apply, E₄sq_coe, smul_eq_mul, neg_mul] /-- The Serre-derivative form of Ramanujan's identity for `E₂`: `D E₂ - (1/12)·E₂² = -(1/12)·E₄`. -/ @@ -678,10 +680,10 @@ theorem serreDerivative_E2_eq : serreDerivative 1 E2 = fun τ : ℍ ↦ -(12⁻ tendsto_E2_atImInfty) have hcval : c = -(12⁻¹) := by rw [mul_one] at hval - rw [hval]; norm_num + rw [hval]; norm_num1 funext τ rw [← hfun, hcval] - simp + simp only [_root_.neg_smul, neg_apply, smul_apply, smul_eq_mul, neg_mul] end RankOne diff --git a/LeanPool/Chudnovsky/SigmaZeta.lean b/LeanPool/Chudnovsky/SigmaZeta.lean index 6c10326c7d..6301736f2f 100644 --- a/LeanPool/Chudnovsky/SigmaZeta.lean +++ b/LeanPool/Chudnovsky/SigmaZeta.lean @@ -64,7 +64,8 @@ private def negNonzero : {l : L.lattice // l ≠ 0} ≃ {l : L.lattice // l ≠ @[simp] private lemma negNonzero_coe (l : {l : L.lattice // l ≠ 0}) : ((L.negNonzero l).1 : ℂ) = -(l.1 : ℂ) := by - simp [negNonzero, Equiv.subtypeEquiv] + simp only [ne_eq, negNonzero, Equiv.subtypeEquiv, Equiv.neg_apply, Equiv.neg_symm, + Equiv.coe_fn_mk, NegMemClass.coe_neg] private lemma weierstrassSigmaTerm_neg_neg (z w : ℂ) : weierstrassSigmaTerm (-z) (-w) = weierstrassSigmaTerm z w := by @@ -120,7 +121,7 @@ private lemma norm_weierstrassZetaTerm_le (z w : ℂ) (hw : w ≠ 0) (h : 2 * linear_combination mul_le_mul_of_nonneg_left h1 (by positivity : (0 : ℝ) ≤ 2 * ‖z‖ ^ 2 * ‖w‖ ^ 2) refine hbound.trans_eq ?_ - rw [show (-3 : ℝ) = -(3 : ℕ) by norm_num, Real.rpow_neg hwpos.le, Real.rpow_natCast] + rw [show (-3 : ℝ) = -(3 : ℕ) by norm_num1, Real.rpow_neg hwpos.le, Real.rpow_natCast] ring /-- The pointwise bound `‖σ-factor − 1‖ ≤ (4/3)‖z‖³‖ω‖⁻³` for `‖ω‖ ≥ 2‖z‖`. -/ @@ -131,12 +132,12 @@ private lemma norm_weierstrassSigmaTerm_sub_one_le (z w : ℂ) (hw : w ≠ 0) (h rw [norm_div, div_le_iff₀ hwpos]; linarith only [h] have hlt1 : ‖-(z / w)‖ < 1 := by rw [norm_neg] - exact hnorm.trans_lt (by norm_num) + exact hnorm.trans_lt (by norm_num1) have h1a : (1 : ℂ) - z / w ≠ 0 := by intro H rw [sub_eq_zero] at H rw [← H, norm_one] at hnorm - norm_num at hnorm + norm_num1 at hnorm have hexp : weierstrassSigmaTerm z w = Complex.exp (Complex.log (1 + -(z / w)) - logTaylor 3 (-(z / w))) := by have h1 : (1 : ℂ) + -(z / w) = 1 - z / w := by ring @@ -148,24 +149,24 @@ private lemma norm_weierstrassSigmaTerm_sub_one_le (z w : ℂ) (hw : w ≠ 0) (h rw [hexp] have hubound : ‖Complex.log (1 + -(z / w)) - logTaylor 3 (-(z / w))‖ ≤ 2 / 3 * ‖z / w‖ ^ 3 := by have hinv : (1 - ‖z / w‖)⁻¹ ≤ 2 := by - rw [inv_le_comm₀ (by linarith only [hnorm]) (by norm_num)] + rw [inv_le_comm₀ (by linarith only [hnorm]) (by norm_num1)] rw [inv_eq_one_div]; linarith only [hnorm] calc ‖Complex.log (1 + -(z / w)) - logTaylor 3 (-(z / w))‖ ≤ ‖-(z / w)‖ ^ (2 + 1) * (1 - ‖-(z / w)‖)⁻¹ / (2 + 1) := norm_log_sub_logTaylor_le 2 hlt1 - _ = ‖z / w‖ ^ 3 * (1 - ‖z / w‖)⁻¹ / 3 := by rw [norm_neg]; norm_num + _ = ‖z / w‖ ^ 3 * (1 - ‖z / w‖)⁻¹ / 3 := by rw [norm_neg]; norm_num only _ ≤ ‖z / w‖ ^ 3 * 2 / 3 := by gcongr _ = 2 / 3 * ‖z / w‖ ^ 3 := by ring have hule1 : ‖Complex.log (1 + -(z / w)) - logTaylor 3 (-(z / w))‖ ≤ 1 := by refine hubound.trans ?_ calc 2 / 3 * ‖z / w‖ ^ 3 ≤ 2 / 3 * (1 / 2 : ℝ) ^ 3 := by gcongr - _ ≤ 1 := by norm_num + _ ≤ 1 := by norm_num1 calc ‖Complex.exp (Complex.log (1 + -(z / w)) - logTaylor 3 (-(z / w))) - 1‖ ≤ 2 * ‖Complex.log (1 + -(z / w)) - logTaylor 3 (-(z / w))‖ := norm_exp_sub_one_le hule1 _ ≤ 2 * (2 / 3 * ‖z / w‖ ^ 3) := by gcongr _ = 4 / 3 * ‖z / w‖ ^ 3 := by ring _ = 4 / 3 * ‖z‖ ^ 3 * ‖w‖ ^ (-3 : ℝ) := by - rw [norm_div, div_pow, show (-3 : ℝ) = -(3 : ℕ) by norm_num, + rw [norm_div, div_pow, show (-3 : ℝ) = -(3 : ℕ) by norm_num1, Real.rpow_neg hwpos.le, Real.rpow_natCast] ring @@ -185,7 +186,8 @@ private lemma hasDerivAt_weierstrassSigmaTerm (z w : ℂ) : * (1 / w + z / w ^ 2))) z := by have hquad : HasDerivAt (fun z : ℂ ↦ z ^ 2 / (2 * w ^ 2)) (z / w ^ 2) z := by have h : HasDerivAt (fun z : ℂ ↦ z ^ 2 / (2 * w ^ 2)) ((2 * z) / (2 * w ^ 2)) z := by - simpa using (hasDerivAt_pow 2 z).div_const (2 * w ^ 2) + simpa only [Nat.cast_ofNat, Nat.add_one_sub_one, + pow_one] using (hasDerivAt_pow 2 z).div_const (2 * w ^ 2) rwa [mul_div_mul_left _ _ two_ne_zero] at h exact (((hasDerivAt_id z).div_const w).const_sub 1).mul (((hasDerivAt_id z).div_const w).add hquad).cexp @@ -213,7 +215,7 @@ private lemma deriv_weierstrassZetaTerm {z w : ℂ} (_hw : w ≠ 0) (hzw : z ≠ exact ((hasDerivAt_id z).sub_const w).inv hzw' have h2 : HasDerivAt (fun _ : ℂ ↦ 1 / w) (0 : ℂ) z := hasDerivAt_const z _ have h3 : HasDerivAt (fun z : ℂ ↦ z / w ^ 2) (1 / w ^ 2) z := by - simpa using (hasDerivAt_id z).div_const (w ^ 2) + simpa only [one_div, id_eq] using (hasDerivAt_id z).div_const (w ^ 2) exact (h1.add h2).add h3 rw [hd.deriv]; ring @@ -224,14 +226,14 @@ private lemma summable_norm_sigma_sub_one (z : ℂ) : ((L.summable_norm_rpow_neg_three).mul_left (4 / 3 * ‖z‖ ^ 3)) ?_ filter_upwards [L.cofinite_norm_ge (2 * ‖z‖)] with l hl rw [norm_norm] - have hw : (l.1 : ℂ) ≠ 0 := by simpa using l.2 + have hw : (l.1 : ℂ) ≠ 0 := by simpa only [ne_eq, ZeroMemClass.coe_eq_zero] using l.2 exact norm_weierstrassSigmaTerm_sub_one_le z (l.1 : ℂ) hw hl /-- On a compact set the norm is bounded by a positive constant. -/ private lemma exists_norm_bound_on_compact {K : Set ℂ} (hK : IsCompact K) : ∃ r : ℝ, 0 < r ∧ ∀ x ∈ K, ‖x‖ ≤ r := by rcases K.eq_empty_or_nonempty with rfl | hne - · exact ⟨1, one_pos, by simp⟩ + · exact ⟨1, one_pos, by simp only [Set.mem_empty_iff_false, IsEmpty.forall_iff, implies_true]⟩ · obtain ⟨r, hr⟩ := hK.isBounded.subset_closedBall (0 : ℂ) refine ⟨max r 1, lt_of_lt_of_le one_pos (le_max_right _ _), fun x hx => ?_⟩ have := hr hx @@ -248,7 +250,7 @@ theorem multipliable_weierstrassSigmaTerm (z : ℂ) : refine Summable.of_norm_bounded_eventually ((L.summable_norm_rpow_neg_three).mul_left (4 / 3 * ‖z‖ ^ 3)) ?_ filter_upwards [L.cofinite_norm_ge (2 * ‖z‖)] with l hl - have hw : (l.1 : ℂ) ≠ 0 := by simpa using l.2 + have hw : (l.1 : ℂ) ≠ 0 := by simpa only [ne_eq, ZeroMemClass.coe_eq_zero] using l.2 exact norm_weierstrassSigmaTerm_sub_one_le z (l.1 : ℂ) hw hl exact (Complex.multipliable_one_add_of_summable hsummable).congr fun l ↦ by ring @@ -268,7 +270,7 @@ theorem hasProdLocallyUniformly_weierstrassSigmaTerm : · exact Filter.Eventually.of_forall fun n x _ ↦ Finset.prod_congr rfl fun i _ ↦ by ring · exact fun x _ ↦ tprod_congr fun l ↦ by ring · filter_upwards [L.cofinite_norm_ge (2 * r)] with l hl x hx - have hw : (l.1 : ℂ) ≠ 0 := by simpa using l.2 + have hw : (l.1 : ℂ) ≠ 0 := by simpa only [ne_eq, ZeroMemClass.coe_eq_zero] using l.2 have hx' : ‖x‖ ≤ r := hKr x hx have h2 : 2 * ‖x‖ ≤ ‖(l.1 : ℂ)‖ := le_trans (by linarith) hl calc ‖weierstrassSigmaTerm x (l.1 : ℂ) - 1‖ @@ -286,7 +288,7 @@ theorem summable_weierstrassZetaTerm (z : ℂ) (_hz : z ∉ L.lattice) : refine Summable.of_norm_bounded_eventually ((L.summable_norm_rpow_neg_three).mul_left (2 * ‖z‖ ^ 2)) ?_ filter_upwards [L.cofinite_norm_ge (2 * ‖z‖)] with l hl - have hw : (l.1 : ℂ) ≠ 0 := by simpa using l.2 + have hw : (l.1 : ℂ) ≠ 0 := by simpa only [ne_eq, ZeroMemClass.coe_eq_zero] using l.2 exact norm_weierstrassZetaTerm_le z (l.1 : ℂ) hw hl /-- The ζ-series converges locally uniformly away from the lattice. -/ @@ -302,7 +304,7 @@ theorem hasSumLocallyUniformlyOn_weierstrassZetaTerm : apply tendstoUniformlyOn_tsum_of_cofinite_eventually ((L.summable_norm_rpow_neg_three).mul_left (2 * r ^ 2)) filter_upwards [L.cofinite_norm_ge (2 * r)] with l hl x hx - have hw : (l.1 : ℂ) ≠ 0 := by simpa using l.2 + have hw : (l.1 : ℂ) ≠ 0 := by simpa only [ne_eq, ZeroMemClass.coe_eq_zero] using l.2 have hx' : ‖x‖ ≤ r := hKr x hx have h2 : 2 * ‖x‖ ≤ ‖(l.1 : ℂ)‖ := le_trans (by linarith) hl calc ‖weierstrassZetaTerm x (l.1 : ℂ)‖ @@ -324,7 +326,7 @@ private lemma differentiable_tprod_weierstrassSigmaTerm : refine (L.hasProdLocallyUniformly_weierstrassSigmaTerm.hasProdLocallyUniformlyOn).differentiableOn (.of_forall fun _ ↦ ?_) isOpen_univ - simpa [Finset.prod_fn] using + simpa only [ne_eq, Finset.prod_fn] using DifferentiableOn.finsetProd fun i _ ↦ (differentiable_weierstrassSigmaTerm (i.1 : ℂ)).differentiableOn @@ -346,7 +348,7 @@ theorem differentiableOn_weierstrassZeta : hopen ?_ intro l r hr have hrne : r ≠ (l.1 : ℂ) := by rintro rfl; exact hr l.1.2 - have hw : (l.1 : ℂ) ≠ 0 := by simpa using l.2 + have hw : (l.1 : ℂ) ≠ 0 := by simpa only [ne_eq, ZeroMemClass.coe_eq_zero] using l.2 have hrw : r - (l.1 : ℂ) ≠ 0 := sub_ne_zero.mpr hrne unfold weierstrassZetaTerm fun_prop (disch := assumption) @@ -440,7 +442,7 @@ private lemma differentiable_tprod_family {ι : Type*} (g : ι → ℂ → ℂ) exact hi x (hKr x hx) · exact fun i ↦ ((hdiff i).continuous.sub continuous_const).continuousOn refine hLU.hasProdLocallyUniformlyOn.differentiableOn (.of_forall fun _ ↦ ?_) isOpen_univ - simpa [Finset.prod_fn] using DifferentiableOn.finsetProd fun i _ ↦ (hdiff i).differentiableOn + simpa only [Finset.prod_fn] using DifferentiableOn.finsetProd fun i _ ↦ (hdiff i).differentiableOn /-- At a nonzero lattice point `ω`, the derivative of `σ` is nonzero: split the factor at `ω` out of the product, `σ z = (z · Q z) · (σ-factor at ω)`, where the factor vanishes simply and @@ -449,7 +451,7 @@ private lemma deriv_weierstrassSigma_ne_zero_at (i₀ : {l : L.lattice // l ≠ deriv L.weierstrassSigma (i₀.1 : ℂ) ≠ 0 := by classical set w : ℂ := (i₀.1 : ℂ) with hw - have hwne : w ≠ 0 := by rw [hw]; simpa using i₀.2 + have hwne : w ≠ 0 := by rw [hw]; simpa only [ne_eq, ZeroMemClass.coe_eq_zero] using i₀.2 -- the σ-product with the factor at `i₀` replaced by `1` set g : {l : L.lattice // l ≠ 0} → ℂ → ℂ := fun n z ↦ if n = i₀ then 1 else weierstrassSigmaTerm z (n.1 : ℂ) with hg @@ -471,7 +473,7 @@ private lemma deriv_weierstrassSigma_ne_zero_at (i₀ : {l : L.lattice // l ≠ · simp only [ite_eq_left h, sub_self, norm_zero] positivity · simp only [ite_eq_right h] - have hwn : (n.1 : ℂ) ≠ 0 := by simpa using n.2 + have hwn : (n.1 : ℂ) ≠ 0 := by simpa only [ne_eq, ZeroMemClass.coe_eq_zero] using n.2 have h2 : 2 * ‖x‖ ≤ ‖(n.1 : ℂ)‖ := le_trans (by linarith) hn calc ‖weierstrassSigmaTerm x (n.1 : ℂ) - 1‖ ≤ 4 / 3 * ‖x‖ ^ 3 * ‖(n.1 : ℂ)‖ ^ (-3 : ℝ) := @@ -506,7 +508,8 @@ private lemma deriv_weierstrassSigma_ne_zero_at (i₀ : {l : L.lattice // l ≠ by_cases h : n = i₀ · simp only [ite_eq_left h]; exact one_ne_zero · simp only [ite_eq_right h] - refine weierstrassSigmaTerm_ne_zero (by simpa using n.2) (fun hcontra ↦ ?_) + refine weierstrassSigmaTerm_ne_zero (by simpa only [ne_eq, + ZeroMemClass.coe_eq_zero] using n.2) (fun hcontra ↦ ?_) exact h (Subtype.ext (Subtype.ext hcontra.symm)) have hsummable : Summable (fun n ↦ ‖g n w - 1‖) := Summable.of_nonneg_of_le (fun n ↦ norm_nonneg _) hle (L.summable_norm_sigma_sub_one w) @@ -519,7 +522,7 @@ private lemma deriv_weierstrassSigma_ne_zero_at (i₀ : {l : L.lattice // l ≠ simpa only [div_self hwne, sub_self, zero_mul, add_zero] using hasDerivAt_weierstrassSigmaTerm w w have hBw : weierstrassSigmaTerm w w = 0 := by - rw [weierstrassSigmaTerm, div_self hwne]; simp + rw [weierstrassSigmaTerm, div_self hwne]; simp only [sub_self, zero_mul] have hdB_ne : (-(1 / w) * Complex.exp (w / w + w ^ 2 / (2 * w ^ 2))) ≠ 0 := mul_ne_zero (neg_ne_zero.mpr (one_div_ne_zero hwne)) (Complex.exp_ne_zero _) have hσeq : L.weierstrassSigma = fun z ↦ (z * Q z) * weierstrassSigmaTerm z w := by @@ -566,7 +569,7 @@ theorem meromorphicOrderAt_weierstrassSigma (l : ℂ) (hl : l ∈ L.lattice) : simpa only [hP0, id_eq, one_mul, zero_mul, add_zero] using (one_ne_zero : (1 : ℂ) ≠ 0) · -- `l ≠ 0`: reduce to the split-factor lemma at the lattice point `l`. have hmem : (⟨l, hl⟩ : L.lattice) ≠ 0 := - fun H ↦ hl0 (by simpa using congrArg Subtype.val H) + fun H ↦ hl0 (by simpa only [ZeroMemClass.coe_zero] using congrArg Subtype.val H) exact L.deriv_weierstrassSigma_ne_zero_at ⟨⟨l, hl⟩, hmem⟩ have hord : analyticOrderAt L.weierstrassSigma l = 1 := hAn.analyticOrderAt_eq_one_of_zero_deriv_ne_zero hzero hderiv @@ -582,7 +585,8 @@ theorem logDeriv_weierstrassSigma (z : ℂ) (hz : z ∉ L.lattice) : have hopen : IsOpen ((↑L.lattice : Set ℂ)ᶜ) := L.isClosed_lattice.isOpen_compl have hzne : ∀ l : {l : L.lattice // l ≠ 0}, z ≠ (l.1 : ℂ) := by intro l; rintro rfl; exact hz l.1.2 - have hwne : ∀ l : {l : L.lattice // l ≠ 0}, (l.1 : ℂ) ≠ 0 := fun l ↦ by simpa using l.2 + have hwne : ∀ l : {l : L.lattice // l ≠ 0}, (l.1 : ℂ) ≠ 0 := fun l ↦ by simpa only [ne_eq, + ZeroMemClass.coe_eq_zero] using l.2 have hfacne : ∀ l : {l : L.lattice // l ≠ 0}, weierstrassSigmaTerm z (l.1 : ℂ) ≠ 0 := fun l ↦ weierstrassSigmaTerm_ne_zero (hwne l) (hzne l) have hlogterm : ∀ l : {l : L.lattice // l ≠ 0}, @@ -624,7 +628,7 @@ private lemma differentiableOn_weierstrassZetaTerm (l : {l : L.lattice // l ≠ DifferentiableOn ℂ (fun z ↦ weierstrassZetaTerm z (l.1 : ℂ)) (↑L.lattice)ᶜ := by intro r hr have hrne : r ≠ (l.1 : ℂ) := by rintro rfl; exact hr l.1.2 - have hw : (l.1 : ℂ) ≠ 0 := by simpa using l.2 + have hw : (l.1 : ℂ) ≠ 0 := by simpa only [ne_eq, ZeroMemClass.coe_eq_zero] using l.2 have hrw : r - (l.1 : ℂ) ≠ 0 := sub_ne_zero.mpr hrne unfold weierstrassZetaTerm refine DifferentiableAt.differentiableWithinAt (((?_ : DifferentiableAt ℂ @@ -659,7 +663,8 @@ private lemma hasSum_deriv_zetaTerm {z : ℂ} (hz : z ∉ L.lattice) : have hzc : z ∈ (↑L.lattice : Set ℂ)ᶜ := hz have hzne : ∀ l : {l : L.lattice // l ≠ 0}, z ≠ (l.1 : ℂ) := by intro l; rintro rfl; exact hz l.1.2 - have hwne : ∀ l : {l : L.lattice // l ≠ 0}, (l.1 : ℂ) ≠ 0 := fun l ↦ by simpa using l.2 + have hwne : ∀ l : {l : L.lattice // l ≠ 0}, (l.1 : ℂ) ≠ 0 := fun l ↦ by simpa only [ne_eq, + ZeroMemClass.coe_eq_zero] using l.2 have hderivS : HasSum (fun l : {l : L.lattice // l ≠ 0} ↦ deriv (fun z ↦ weierstrassZetaTerm z (l.1 : ℂ)) z) (deriv (fun z ↦ ∑' l : {l : L.lattice // l ≠ 0}, weierstrassZetaTerm z (l.1 : ℂ)) z) := by diff --git a/LeanPool/Chudnovsky/SingularModuli/CosetOrbit.lean b/LeanPool/Chudnovsky/SingularModuli/CosetOrbit.lean index 32c324c0fc..5717e730f5 100644 --- a/LeanPool/Chudnovsky/SingularModuli/CosetOrbit.lean +++ b/LeanPool/Chudnovsky/SingularModuli/CosetOrbit.lean @@ -84,11 +84,13 @@ def Acol (m : ℕ) [NeZero m] (b : ℤ) : GL (Fin 2) ℝ := lemma det_AInf_pos [NeZero m] : 0 < (AInf m).det.val := by rw [Matrix.GeneralLinearGroup.val_det_apply, val_AInf, Matrix.det_fin_two_of] - simpa using (Nat.cast_pos.mpr (Nat.pos_of_ne_zero (NeZero.ne m)) : (0 : ℝ) < m) + simpa only [mul_one, mul_zero, sub_zero, + Nat.cast_pos] using (Nat.cast_pos.mpr (Nat.pos_of_ne_zero (NeZero.ne m)) : (0 : ℝ) < m) lemma det_Acol_pos [NeZero m] (b : ℤ) : 0 < (Acol m b).det.val := by rw [Matrix.GeneralLinearGroup.val_det_apply, val_Acol, Matrix.det_fin_two_of] - simpa using (Nat.cast_pos.mpr (Nat.pos_of_ne_zero (NeZero.ne m)) : (0 : ℝ) < m) + simpa only [one_mul, mul_zero, sub_zero, + Nat.cast_pos] using (Nat.cast_pos.mpr (Nat.pos_of_ne_zero (NeZero.ne m)) : (0 : ℝ) < m) /-- The `∞`-coset point: `AInf m • τ = m·τ`. -/ lemma coe_AInf_smul [NeZero m] (τ : ℍ) : (↑(AInf m • τ) : ℂ) = m * τ := by @@ -171,17 +173,18 @@ lemma f_T_smul [NeZero m] (i : Option (ZMod m)) (τ : ℍ) : simp only [coe_AInf_smul, UpperHalfPlane.coe_vadd] push_cast; ring rw [hpt] - simpa using j_vadd_int (m : ℤ) (AInf m • τ) + simpa only [j_def, mul_eq_mul_left_iff, OfNat.ofNat_ne_zero, or_false, + Int.cast_natCast] using j_vadd_int (m : ℤ) (AInf m • τ) | some b => simp only [f_some, σT_some] -- first move the `+1` inside the coset offset: point equality have hpt : Acol m b.val • ((1 : ℝ) +ᵥ τ) = Acol m (b.val + 1) • τ := by apply UpperHalfPlane.ext simp only [coe_Acol_smul, UpperHalfPlane.coe_vadd] - push_cast; ring + push_cast; ac_rfl rw [hpt] -- then reduce `(b.val + 1)` to `(b+1).val` mod m - exact j_Acol_smul_congr (by simpa using dvd_val_add b 1) τ + exact j_Acol_smul_congr (by simpa only [ZMod.natCast_val, Int.cast_one] using dvd_val_add b 1) τ /-! ## The `S`-permutation diff --git a/LeanPool/Chudnovsky/SingularModuli/FormReduction.lean b/LeanPool/Chudnovsky/SingularModuli/FormReduction.lean index 94e7f848ec..8f6f29696a 100644 --- a/LeanPool/Chudnovsky/SingularModuli/FormReduction.lean +++ b/LeanPool/Chudnovsky/SingularModuli/FormReduction.lean @@ -45,7 +45,7 @@ open UpperHalfPlane def Equiv (f g : BQF) : Prop := ∃ p q r s : ℤ, p * s - q * r = 1 ∧ act f p q r s = g -@[refl] theorem Equiv.refl (f : BQF) : Equiv f f := ⟨1, 0, 0, 1, by ring, act_one f⟩ +@[refl] theorem Equiv.refl (f : BQF) : Equiv f f := ⟨1, 0, 0, 1, by ac_rfl, act_one f⟩ theorem Equiv.symm {f g : BQF} (h : Equiv f g) : Equiv g f := by obtain ⟨p, q, r, s, hdet, hfg⟩ := h @@ -71,7 +71,7 @@ lemma act_T_c (f : BQF) (n : ℤ) : (act f 1 n 0 1).c = f.a * n ^ 2 + f.b * n + simp only [act_c]; ring /-- The `S`-generator: swap `(a, b, c) ↦ (c, −b, a)`. -/ -theorem Equiv.S (f : BQF) : Equiv f (act f 0 (-1) 1 0) := ⟨0, -1, 1, 0, by ring, rfl⟩ +theorem Equiv.S (f : BQF) : Equiv f (act f 0 (-1) 1 0) := ⟨0, -1, 1, 0, by ac_rfl, rfl⟩ lemma act_S_a (f : BQF) : (act f 0 (-1) 1 0).a = f.c := by simp lemma act_S_b (f : BQF) : (act f 0 (-1) 1 0).b = -f.b := by simp only [act_b]; ring @@ -80,7 +80,7 @@ lemma act_S_c (f : BQF) : (act f 0 (-1) 1 0).c = f.a := by simp only [act_c]; ri /-- Equivalent forms have equal discriminant. -/ theorem Equiv.disc_eq {f g : BQF} (h : Equiv f g) : disc f = disc g := by obtain ⟨p, q, r, s, hdet, rfl⟩ := h - rw [disc_act, hdet]; ring + rw [disc_act, hdet]; ac_rfl /-- Equivalence preserves primitivity. -/ theorem Equiv.isPrimitive {f g : BQF} (h : Equiv f g) (hf : IsPrimitive f) : IsPrimitive g := by @@ -284,8 +284,8 @@ theorem disc_of_three_relations {D0 : ℤ} (hD3 : D0 ≤ -3) have e1 := reprN_of_relation (m := 41) (by norm_num) hD3 hl1 (by exact_mod_cast h1) have e2 := reprN_of_relation (m := 43) (by norm_num) hD3 hl2 (by exact_mod_cast h2) have e3 := reprN_of_relation (m := 61) (by norm_num) hD3 hl3 (by exact_mod_cast h3) - have hl1sq : (1 : ℤ) ≤ l1 ^ 2 := by rcases lt_or_gt_of_ne hl1 with h' | h' <;> nlinarith - have hub : (-D0) ≤ 164 := by nlinarith [h1, hl1sq, sq_nonneg t1] + have hl1sq : (1 : ℤ) ≤ l1 ^ 2 := by rcases lt_or_gt_of_ne hl1 with h' | h' <;> nlinarith only [h'] + have hub : (-D0) ≤ 164 := by nlinarith only [h1, hl1sq] have hmem : (-D0).toNat ∈ Finset.Icc 1 244 := by rw [Finset.mem_Icc]; omega have := three_prime_N (-D0).toNat hmem e1 e2 e3 diff --git a/LeanPool/Chudnovsky/SingularModuli/JFunction.lean b/LeanPool/Chudnovsky/SingularModuli/JFunction.lean index 09fc5a2c21..a1ef51ba48 100644 --- a/LeanPool/Chudnovsky/SingularModuli/JFunction.lean +++ b/LeanPool/Chudnovsky/SingularModuli/JFunction.lean @@ -138,15 +138,15 @@ coefficients. These feed the ℤ-refinement `ModularPolynomialZ.lean` downstream /-- Every q-expansion coefficient of `E₄` is an integer (`1` at `n = 0`, `240·σ₃(n)` else). -/ lemma E₄_qExpansion_coeff_int (n : ℕ) : ∃ c : ℤ, (qExpansion 1 E₄).coeff n = (c : ℂ) := by - have h := EisensteinSeries.E_qExpansion_coeff (k := 4) (by norm_num) (by decide) n + have h := EisensteinSeries.E_qExpansion_coeff (k := 4) (by norm_num only) (by decide) n have hb : bernoulli 4 = -1 / 30 := bernoulli_four_value rw [hb, show (4 : ℕ) - 1 = 3 from rfl] at h by_cases hn : n = 0 - · exact ⟨1, by rw [h, ite_eq_left hn]; norm_num⟩ + · exact ⟨1, by rw [h, ite_eq_left hn]; norm_num only⟩ · refine ⟨240 * ArithmeticFunction.sigma 3 n, ?_⟩ rw [h, ite_eq_right hn] push_cast - norm_num + norm_num only /-- Every q-expansion coefficient of the cube `(qExpansion E₄)³` — i.e. of `E₄³` — is an integer. This is the numerator side of `j = E₄³/Δ`. -/ @@ -155,7 +155,7 @@ lemma E₄_qExpansion_pow_three_coeff_int (n : ℕ) : choose c hc using E₄_qExpansion_coeff_int have hmap : qExpansion 1 E₄ = (PowerSeries.mk c).map (Int.castRingHom ℂ) := by ext m - simp [PowerSeries.coeff_map, PowerSeries.coeff_mk, hc m] + simp only [hc m, PowerSeries.coeff_map, PowerSeries.coeff_mk, eq_intCast] refine ⟨((PowerSeries.mk c) ^ 3).coeff n, ?_⟩ rw [hmap, ← map_pow, PowerSeries.coeff_map] rfl @@ -252,10 +252,10 @@ private lemma dvd_1728_coeff (m : ℕ) : have h24 : (24 : ℤ) ∣ PowerSeries.coeff m (sigmaPS 5 - sigmaPS 3) := by rw [map_sub, sigmaPS, sigmaPS, PowerSeries.coeff_mk, PowerSeries.coeff_mk] split_ifs - · simp + · simp only [sub_self, dvd_zero] · exact dvd_sigma_sub m obtain ⟨c, hc⟩ := h24 - exact ⟨14 * c, by rw [hc]; ring⟩ + exact ⟨14 * c, by rw [hc]; ac_rfl⟩ private lemma exists_delta_coeff (m : ℕ) : ∃ t : ℤ, PowerSeries.coeff m (E4Z ^ 3 - E6Z ^ 2) = 1728 * t := dvd_1728_coeff m @@ -390,12 +390,12 @@ private lemma cuspFunction_qfun_eqOn : intro z hz by_cases hz0 : z = 0 · subst hz0 - simpa using isZeroAtImInfty_qfun.cuspFunction_apply_zero one_pos + simpa only [id_eq] using isZeroAtImInfty_qfun.cuspFunction_apply_zero one_pos · have him := Function.Periodic.im_invQParam_pos_of_norm_lt_one one_pos - (by simpa [dist_zero_right] using hz) hz0 - simp [cuspFunction, Function.Periodic.cuspFunction_eq_of_nonzero 1 _ hz0, - ofComplex_apply_of_im_pos him, q, - Function.Periodic.qParam_right_inv one_ne_zero hz0] + (by simpa only [Metric.mem_ball, dist_zero_right] using hz) hz0 + simp only [cuspFunction, q, Function.Periodic.cuspFunction_eq_of_nonzero 1 _ hz0, + Function.comp_apply, ofComplex_apply_of_im_pos him, + Function.Periodic.qParam_right_inv one_ne_zero hz0, id_eq] /-- The q-expansion of the nome itself is the series `X`. -/ private lemma qExpansion_qfun_eq : qExpansion 1 (fun τ : ℍ ↦ q τ) = PowerSeries.X := by @@ -404,14 +404,16 @@ private lemma qExpansion_qfun_eq : qExpansion 1 (fun τ : ℍ ↦ q τ) = PowerS ext m rw [qExpansion_coeff, PowerSeries.coeff_X, Filter.EventuallyEq.iteratedDeriv_eq m heq] match m with - | 0 => simp - | 1 => simp + | 0 => simp only [Nat.factorial_zero, Nat.cast_one, inv_one, iteratedDeriv_zero, id_eq, mul_zero, + zero_ne_one, ↓reduceIte] + | 1 => simp only [Nat.factorial_one, Nat.cast_one, inv_one, iteratedDeriv_one, deriv_id', mul_one, + ↓reduceIte] | (k + 2) => have hconst : iteratedDeriv (k + 2) (id : ℂ → ℂ) 0 = 0 := by rw [iteratedDeriv_succ', deriv_id'] - simp [iteratedDeriv_const] + simp only [iteratedDeriv_const, Nat.add_eq_zero_iff, one_ne_zero, and_false, ↓reduceIte] rw [hconst] - simp + simp only [mul_zero, Nat.reduceEqDiff, ↓reduceIte] /-- `j·q` is invariant under `τ ↦ τ + 1`. -/ private lemma jq_vadd_one (τ : ℍ) : j ((1 : ℝ) +ᵥ τ) * q ((1 : ℝ) +ᵥ τ) = j τ * q τ := by @@ -446,7 +448,7 @@ private lemma isBoundedAtImInfty_jq : IsBoundedAtImInfty (fun τ : ℍ ↦ j τ have hE : IsBoundedAtImInfty ⇑E₄ := ModularFormClass.bdd_at_infty E₄ have hPinv : Filter.Tendsto (fun τ : ℍ ↦ (∏' n : ℕ, (1 - eta_q n ↑τ) ^ 24)⁻¹) atImInfty (nhds 1) := by - simpa using tendsto_atImInfty_tprod_one_sub_eta_q_pow.inv₀ one_ne_zero + simpa only [inv_one] using tendsto_atImInfty_tprod_one_sub_eta_q_pow.inv₀ one_ne_zero have hPb : IsBoundedAtImInfty (fun τ : ℍ ↦ (∏' n : ℕ, (1 - eta_q n ↑τ) ^ 24)⁻¹) := hPinv.isBigO_one ℝ exact Filter.BoundedAtFilter.mul hE (Filter.BoundedAtFilter.mul hE @@ -530,7 +532,7 @@ theorem j_mul_q_qExpansion_coeff_zero : PowerSeries.coeff 0 (qExpansion 1 (fun τ : ℍ ↦ j τ * q τ)) = 1 := by rw [qExpansion_j_mul_q, PowerSeries.coeff_map, PowerSeries.coeff_zero_eq_constantCoeff_apply, constantCoeff_jqInt] - simp + simp only [eq_intCast, Int.cast_one] /-- **(B1) headline, existential packaging**: `j·q ∈ 1 + q·ℤ⟦q⟧` — there are integers `c 0 = 1, c 1 = 744, c 2 = 196884, …` with `j τ · q τ = ∑ c n · q τ ^ n` for all `τ : ℍ`. -/ diff --git a/LeanPool/Chudnovsky/SingularModuli/Kronecker.lean b/LeanPool/Chudnovsky/SingularModuli/Kronecker.lean index 0f2260eb38..4577ddb95b 100644 --- a/LeanPool/Chudnovsky/SingularModuli/Kronecker.lean +++ b/LeanPool/Chudnovsky/SingularModuli/Kronecker.lean @@ -60,7 +60,7 @@ variable {m : ℕ} /-- `q τ → 0` as `Im τ → ∞`. -/ lemma q_tendsto_zero : Tendsto (fun τ : ℍ ↦ q τ) atImInfty (nhds 0) := by - simpa [q] using qParam_tendsto_atImInfty one_pos + simpa only [q] using qParam_tendsto_atImInfty one_pos /-- `j·q` is bounded at the cusp (it tends to `1`); reconstructed from `discriminant = q · ∏ (1 − qⁿ)²⁴` and `j·Δ = E₄³`. -/ @@ -79,7 +79,7 @@ lemma isBoundedAtImInfty_jq' : IsBoundedAtImInfty (fun τ : ℍ ↦ j τ * q τ) rw [hrec] have hE : IsBoundedAtImInfty ⇑E₄ := ModularFormClass.bdd_at_infty E₄ have hPinv : Tendsto (fun τ : ℍ ↦ (∏' n : ℕ, (1 - eta_q n ↑τ) ^ 24)⁻¹) atImInfty (nhds 1) := by - simpa using tendsto_atImInfty_tprod_one_sub_eta_q_pow.inv₀ one_ne_zero + simpa only [inv_one] using tendsto_atImInfty_tprod_one_sub_eta_q_pow.inv₀ one_ne_zero have hPb : IsBoundedAtImInfty (fun τ : ℍ ↦ (∏' n : ℕ, (1 - eta_q n ↑τ) ^ 24)⁻¹) := hPinv.isBigO_one ℝ exact Filter.BoundedAtFilter.mul hE (Filter.BoundedAtFilter.mul hE @@ -96,7 +96,8 @@ lemma jq_tendsto_one : Tendsto (fun τ : ℍ ↦ j τ * q τ) atImInfty (nhds 1) have hcusp0 : cuspFunction 1 (fun τ : ℍ ↦ j τ * q τ) 0 = 1 := by have h := j_mul_q_qExpansion_coeff_zero rw [qExpansion_coeff] at h - simpa using h + simpa only [j_def, Nat.factorial_zero, Nat.cast_one, inv_one, iteratedDeriv_zero, + one_mul] using h have hcomp : Tendsto (fun τ : ℍ ↦ cuspFunction 1 (fun ρ : ℍ ↦ j ρ * q ρ) (q τ)) atImInfty (nhds (cuspFunction 1 (fun τ : ℍ ↦ j τ * q τ) 0)) := hcts.tendsto.comp q_tendsto_zero rw [hcusp0] at hcomp @@ -113,9 +114,11 @@ lemma jq_comp_tendsto_one {A : GL (Fin 2) ℝ} (hA : (A : Matrix (Fin 2) (Fin 2) lemma wParam_tendsto_zero [NeZero m] : Tendsto (fun τ : ℍ ↦ wParam m τ) atImInfty (nhds 0) := by have h : Tendsto (fun τ : ℍ ↦ q (Acol m (0 : ℤ) • τ)) atImInfty (nhds 0) := - q_tendsto_zero.comp (tendsto_smul_atImInfty (g := Acol m (0 : ℤ)) (by simp [val_Acol])) + q_tendsto_zero.comp (tendsto_smul_atImInfty (g := Acol m (0 : ℤ)) (by simp only [Fin.isValue, + val_Acol, Int.cast_zero, Matrix.of_apply, Matrix.cons_val', Matrix.cons_val_zero, + Matrix.cons_val_fin_one, Matrix.cons_val_one])) refine h.congr (fun τ ↦ ?_) - rw [q_Acol_smul]; simp + rw [q_Acol_smul]; simp only [zpow_ofNat, pow_zero, one_mul] /-! ### Per-factor limits of the orbit product -/ @@ -139,18 +142,18 @@ lemma some_factor_tendsto_one [Fact m.Prime] (b : ZMod m) : rw [show (j (Acol m (b.val : ℤ) • τ) * (zetaM m ^ (b.val : ℤ) * wParam m τ)) * (zetaM m ^ (-(b.val : ℤ)) * wParam m τ ^ (m - 1)) = j (Acol m (b.val : ℤ) • τ) * (zetaM m ^ (b.val : ℤ) * zetaM m ^ (-(b.val : ℤ))) - * (wParam m τ * wParam m τ ^ (m - 1)) from by ring, hzz, hww, mul_one] + * (wParam m τ * wParam m τ ^ (m - 1)) from by ac_rfl, hzz, hww, mul_one] have hA : Tendsto (fun τ : ℍ ↦ j (Acol m (b.val : ℤ) • τ) * q (Acol m (b.val : ℤ) • τ)) atImInfty (nhds 1) := jq_comp_tendsto_one (A := Acol m (b.val : ℤ)) (by simp [val_Acol]) have hB : Tendsto (fun τ : ℍ ↦ zetaM m ^ (-(b.val : ℤ)) * wParam m τ ^ (m - 1)) atImInfty (nhds 0) := by have hw : Tendsto (fun τ : ℍ ↦ wParam m τ ^ (m - 1)) atImInfty (nhds 0) := by - simpa [zero_pow (show m - 1 ≠ 0 by omega)] using wParam_tendsto_zero.pow (m - 1) - simpa using tendsto_const_nhds.mul hw + simpa only [zero_pow (show m - 1 ≠ 0 by omega)] using wParam_tendsto_zero.pow (m - 1) + simpa only [ZMod.natCast_val, zpow_neg, mul_zero] using tendsto_const_nhds.mul hw have hmul : Tendsto (fun τ : ℍ ↦ (j (Acol m (b.val : ℤ) • τ) * q (Acol m (b.val : ℤ) • τ)) * (zetaM m ^ (-(b.val : ℤ)) * wParam m τ ^ (m - 1))) atImInfty (nhds 0) := by - simpa using hA.mul hB + simpa only [ZMod.natCast_val, j_def, zpow_neg, mul_zero] using hA.mul hB exact hmul.congr (fun τ ↦ (hkey τ).symm) have hsub : Tendsto (fun τ : ℍ ↦ j τ * q τ - f m (some b) τ * q τ) atImInfty (nhds (1 - 0)) := jq_tendsto_one.sub hfac @@ -166,14 +169,15 @@ lemma none_factor_tendsto_neg_one [Fact m.Prime] : have hjqm : Tendsto (fun τ : ℍ ↦ j τ * q τ ^ m) atImInfty (nhds 0) := by have h1 : Tendsto (fun τ : ℍ ↦ (j τ * q τ) * q τ ^ (m - 1)) atImInfty (nhds (1 * 0)) := jq_tendsto_one.mul (by - simpa [zero_pow (show m - 1 ≠ 0 by omega)] using q_tendsto_zero.pow (m - 1)) + simpa only [zero_pow (show m - 1 ≠ 0 by omega)] using q_tendsto_zero.pow (m - 1)) rw [mul_zero] at h1 refine h1.congr (fun τ ↦ ?_) rw [mul_assoc, ← pow_succ', Nat.sub_add_cancel (show 1 ≤ m by omega)] -- `f_∞ · qᵐ = j(m·τ) · q(m·τ) → 1` have hfnone : Tendsto (fun τ : ℍ ↦ f m none τ * q τ ^ m) atImInfty (nhds 1) := by have hAI : Tendsto (fun τ : ℍ ↦ j (AInf m • τ) * q (AInf m • τ)) atImInfty (nhds 1) := - jq_comp_tendsto_one (A := AInf m) (by simp [val_AInf]) + jq_comp_tendsto_one (A := AInf m) (by simp only [Fin.isValue, val_AInf, Matrix.of_apply, + Matrix.cons_val', Matrix.cons_val_zero, Matrix.cons_val_fin_one, Matrix.cons_val_one]) refine hAI.congr (fun τ ↦ ?_) rw [f_none, q_AInf_smul (m := m), ← wParam_pow_m (m := m) τ, ← pow_mul, pow_two] have hsub : Tendsto (fun τ : ℍ ↦ j τ * q τ ^ m - f m none τ * q τ ^ m) atImInfty (nhds (0 - 1)) := @@ -191,14 +195,15 @@ lemma orbit_prod_tendsto_neg_one [Fact m.Prime] : have h := tendsto_finsetProd (Finset.univ : Finset (ZMod m)) (f := fun b (τ : ℍ) ↦ (j τ - f m (some b) τ) * q τ) (a := fun _ ↦ (1 : ℂ)) (fun b _ ↦ some_factor_tendsto_one b) - simpa using h + simpa only [j_def, f_some, ZMod.natCast_val, prod_const_one] using h have hcombined : Tendsto (fun τ : ℍ ↦ ((j τ - f m none τ) * q τ ^ m) * ∏ b : ZMod m, ((j τ - f m (some b) τ) * q τ)) atImInfty (nhds (-1)) := by - simpa using none_factor_tendsto_neg_one.mul hprod + simpa only [j_def, f_none, f_some, ZMod.natCast_val, + mul_one] using none_factor_tendsto_neg_one.mul hprod refine hcombined.congr (fun τ ↦ ?_) rw [Fintype.prod_option, Finset.prod_mul_distrib, Finset.prod_const, Finset.card_univ, ZMod.card, show 2 * m = m + m from two_mul m, pow_add] - ring + ac_rfl /-! ### The polynomial side -/ @@ -210,18 +215,18 @@ lemma term_tendsto (c : ℂ) (r d : ℕ) (hrd : r ≤ d) : intro τ have hq : q τ ^ d = q τ ^ r * q τ ^ (d - r) := by rw [← pow_add, Nat.add_sub_cancel' hrd] - rw [hq, mul_pow]; ring + rw [hq, mul_pow]; ac_rfl simp_rw [hfun] by_cases h : r = d · subst h simp only [Nat.sub_self, pow_zero, mul_one, ite_true] - simpa using tendsto_const_nhds.mul (jq_tendsto_one.pow r) + simpa only [j_def, one_pow, mul_one] using tendsto_const_nhds.mul (jq_tendsto_one.pow r) · rw [ite_eq_right h] have hqdr : Tendsto (fun τ : ℍ ↦ q τ ^ (d - r)) atImInfty (nhds 0) := by - simpa [zero_pow (show d - r ≠ 0 by omega)] using q_tendsto_zero.pow (d - r) + simpa only [zero_pow (show d - r ≠ 0 by omega)] using q_tendsto_zero.pow (d - r) have h2 : Tendsto (fun τ : ℍ ↦ c * (j τ * q τ) ^ r) atImInfty (nhds c) := by - simpa using tendsto_const_nhds.mul (jq_tendsto_one.pow r) - simpa using h2.mul hqdr + simpa only [j_def, one_pow, mul_one] using tendsto_const_nhds.mul (jq_tendsto_one.pow r) + simpa only [j_def, mul_zero] using h2.mul hqdr /-- `G(j τ)·q^{natDegree G} → (leadingCoeff G : ℂ)`: matching the polynomial against its top `q`-power isolates the leading coefficient. -/ @@ -275,13 +280,13 @@ theorem diagPhiZ_natDegree_and_leadingCoeff [Fact m.Prime] have hshift : Tendsto (fun τ : ℍ ↦ (G.eval₂ (Int.castRingHom ℂ) (j τ) * q τ ^ G.natDegree) * q τ ^ (2 * m - G.natDegree)) atImInfty (nhds (((G.leadingCoeff : ℤ) : ℂ) * 0)) := hB.mul (by - simpa [zero_pow (show 2 * m - G.natDegree ≠ 0 by omega)] + simpa only [zero_pow (show 2 * m - G.natDegree ≠ 0 by omega)] using q_tendsto_zero.pow (2 * m - G.natDegree)) rw [mul_zero] at hshift have h0 : Tendsto (fun τ : ℍ ↦ G.eval₂ (Int.castRingHom ℂ) (j τ) * q τ ^ (2 * m)) atImInfty (nhds 0) := hshift.congr (fun τ ↦ by rw [mul_assoc, ← pow_add, Nat.add_sub_cancel' hlt.le]) - exact absurd (tendsto_nhds_unique h0 hA) (by norm_num) + exact absurd (tendsto_nhds_unique h0 hA) (by norm_num1) · -- `natDegree = 2m` : the two limits agree, so `leadingCoeff = −1` have hBeq : Tendsto (fun τ : ℍ ↦ G.eval₂ (Int.castRingHom ℂ) (j τ) * q τ ^ (2 * m)) atImInfty (nhds ((G.leadingCoeff : ℤ) : ℂ)) := by rw [← heq]; exact hB @@ -291,7 +296,7 @@ theorem diagPhiZ_natDegree_and_leadingCoeff [Fact m.Prime] have hshift : Tendsto (fun τ : ℍ ↦ (G.eval₂ (Int.castRingHom ℂ) (j τ) * q τ ^ (2 * m)) * q τ ^ (G.natDegree - 2 * m)) atImInfty (nhds ((-1 : ℂ) * 0)) := hA.mul (by - simpa [zero_pow (show G.natDegree - 2 * m ≠ 0 by omega)] + simpa only [zero_pow (show G.natDegree - 2 * m ≠ 0 by omega)] using q_tendsto_zero.pow (G.natDegree - 2 * m)) rw [mul_zero] at hshift have h0 : Tendsto (fun τ : ℍ ↦ G.eval₂ (Int.castRingHom ℂ) (j τ) * q τ ^ G.natDegree) atImInfty @@ -304,9 +309,9 @@ theorem diagPhiZ_natDegree_and_leadingCoeff [Fact m.Prime] have hA0 : Tendsto (fun τ : ℍ ↦ G.eval₂ (Int.castRingHom ℂ) (j τ) * q τ ^ (2 * m)) atImInfty (nhds 0) := by have hz : (fun τ : ℍ ↦ G.eval₂ (Int.castRingHom ℂ) (j τ) * q τ ^ (2 * m)) - = fun _ ↦ (0 : ℂ) := by funext τ; rw [hlcZ]; simp + = fun _ ↦ (0 : ℂ) := by funext τ; rw [hlcZ]; simp only [j_def, eval₂_zero, zero_mul] rw [hz]; exact tendsto_const_nhds - exact absurd (tendsto_nhds_unique hA0 hA) (by norm_num) + exact absurd (tendsto_nhds_unique hA0 hA) (by norm_num1) /-- **`natDegree (diagPhiZ PhiZ) = 2·m`.** -/ theorem diagPhiZ_natDegree_eq [Fact m.Prime] {PhiZ : Polynomial (Polynomial ℤ)} diff --git a/LeanPool/Chudnovsky/SingularModuli/MasserA1.lean b/LeanPool/Chudnovsky/SingularModuli/MasserA1.lean index 9facfd96b3..357777d415 100644 --- a/LeanPool/Chudnovsky/SingularModuli/MasserA1.lean +++ b/LeanPool/Chudnovsky/SingularModuli/MasserA1.lean @@ -150,10 +150,10 @@ lemma j₀_ne_zero : (1728 : ℂ) * J τ₁₆₃ ≠ 0 := lemma j₀_ne_1728 : (1728 : ℂ) * J τ₁₆₃ ≠ 1728 := by intro hc have hJ1 : J τ₁₆₃ = 1 := - mul_left_cancel₀ (show (1728 : ℂ) ≠ 0 by norm_num) (by rw [hc]; ring) + mul_left_cancel₀ (show (1728 : ℂ) ≠ 0 by norm_num1) (by rw [hc]; ac_rfl) have h := one_lt_norm_J τ₁₆₃_mem_Region rw [hJ1, norm_one] at h - linarith + linarith only [h] /-- `E₆(τ₁₆₃) ≠ 0` (Estimates `E₆_ne_zero_of_mem_Region`). -/ lemma E₆_τ₁₆₃_ne_zero : E₆ τ₁₆₃ ≠ 0 := @@ -277,7 +277,7 @@ private lemma two_mul_sub_one_ne_zero {z : ℂ} (hz : 0 < z.im) : 2 * z - 1 ≠ have him := congrArg Complex.im h simp only [Complex.sub_im, Complex.mul_im, Complex.one_im, Complex.zero_im] at him norm_num at him - nlinarith [him, hz] + linarith [him, hz] /-- `λ` matches the `GL₂`-action: `↑(Λ • ofComplex z) = λ z` for `z` in the upper half-plane. -/ private lemma coe_LamGL_smul_ofComplex {z : ℂ} (hz : 0 < z.im) : @@ -425,7 +425,7 @@ Masser's proof) used below. -/ private lemma hasDerivAt_poly_comp {P : Polynomial ℂ} {v : ℂ → ℂ} {v' z : ℂ} (hv : HasDerivAt v v' z) : HasDerivAt (fun y ↦ P.eval (v y)) ((P.derivative).eval (v z) * v') z := by - simpa [Function.comp_def] using (P.hasDerivAt (v z)).comp z hv + simpa only [Function.comp_def] using (P.hasDerivAt (v z)).comp z hv private lemma masser_bivariate_derivs (s : Finset ℕ) (p : ℕ → Polynomial ℂ) (u v u' v' : ℂ → ℂ) (t u'' v'' : ℂ) @@ -715,9 +715,9 @@ private lemma masser_norm_form_solve {p k : ℤ} (h : p * p - p * k + 41 * (k * (p = 1 ∧ k = 2) ∨ (p = -1 ∧ k = -2) := by -- Completing the square in each variable bounds the finite search. have hk : |k| ≤ 2 := abs_le_of_sq_le_sq - (by nlinarith only [h, sq_nonneg (2 * p - k)]) (by norm_num) + (by linarith only [h, sq_nonneg (2 * p - k)]) (by norm_num1) have hp : |p| ≤ 13 := abs_le_of_sq_le_sq - (by nlinarith only [h, sq_nonneg (p - 82 * k)]) (by norm_num) + (by linarith only [h, sq_nonneg (p - 82 * k)]) (by norm_num1) have hfinite : ∀ p ∈ Finset.Icc (-13 : ℤ) 13, ∀ k ∈ Finset.Icc (-2 : ℤ) 2, p * p - p * k + 41 * (k * k) = 163 → (p = 1 ∧ k = 2) ∨ (p = -1 ∧ k = -2) := by decide +kernel @@ -744,7 +744,7 @@ private lemma masser_fixes_of_coset {e f g : ℤ} (γ : SL(2, ℤ)) {Aτ τ' : push_cast at h0 obtain ⟨hc0, hd0⟩ := QF.int_lin_eq_zero Aτ h0 rw [hc0, hd0] at hdet - simp at hdet + simp only [Fin.isValue, mul_zero, sub_self, zero_ne_one] at hdet rw [eq_div_iff hden, hW] at hco simp only [eq_intCast] at hco simp only [QF.Fixes] @@ -763,7 +763,7 @@ private lemma masser_fixes_pm {p q r s : ℤ} (hfix : QF.Fixes p q r s τ₁₆ push_cast linear_combination τ₁₆₃_sq have hprim : QF.IsPrimitive ⟨1, -1, 41⟩ := fun d hd _ _ ↦ isUnit_of_dvd_one hd - have hpd : QF.IsPosDef ⟨1, -1, 41⟩ := ⟨one_pos, by norm_num [QF.disc]⟩ + have hpd : QF.IsPosDef ⟨1, -1, 41⟩ := ⟨one_pos, by norm_num only [QF.disc]⟩ obtain ⟨k, hr, hsp, hq⟩ := QF.fixes_classification hprim hpd hroot hfix dsimp only at hr hsp hq have heq : p * p - p * k + 41 * (k * k) = 163 := by diff --git a/LeanPool/Chudnovsky/SingularModuli/ModularPolynomialQ.lean b/LeanPool/Chudnovsky/SingularModuli/ModularPolynomialQ.lean index aa5dc30ae2..859d64e70f 100644 --- a/LeanPool/Chudnovsky/SingularModuli/ModularPolynomialQ.lean +++ b/LeanPool/Chudnovsky/SingularModuli/ModularPolynomialQ.lean @@ -125,7 +125,7 @@ lemma sum_zetaM_zpow_mul [NeZero m] (n : ℤ) : rw [sum_zmod_eq_range m (fun k ↦ (zetaM m ^ n) ^ k)] by_cases hdvd : (m : ℤ) ∣ n · rw [ite_eq_left hdvd, (zetaM_zpow_eq_one_iff n).mpr hdvd] - simp + simp only [one_pow, sum_const, card_range, nsmul_eq_mul, mul_one] · rw [ite_eq_right hdvd] have hx1 : zetaM m ^ n ≠ 1 := fun h ↦ hdvd ((zetaM_zpow_eq_one_iff n).mp h) rw [geom_sum_eq hx1] @@ -191,7 +191,8 @@ lemma powerSum_smul [Fact m.Prime] (k : ℕ) (γ : SL(2, ℤ)) (τ : ℍ) : /-- Each power sum is holomorphic on `ℍ`. -/ lemma mdifferentiable_powerSum [NeZero m] (k : ℕ) : MDiff (powerSum m k) := by have heq : powerSum m k = ∑ i : Option (ZMod m), (fun τ : ℍ ↦ (f m i τ) ^ k) := by - funext τ; simp [powerSum, Finset.sum_apply] + funext τ; simp only [powerSum, Fintype.sum_option, f_none, j_def, f_some, ZMod.natCast_val, + Finset.sum_apply] rw [heq] exact MDifferentiable.sum (fun i _ ↦ (mdifferentiable_f i).pow k) @@ -246,7 +247,7 @@ lemma mdifferentiable_coeff_prod_X_sub_C {ι : Type*} (a : ι → ℍ → ℂ) intro n have hconst : (fun τ : ℍ ↦ ((∏ i ∈ (∅ : Finset ι), (X - C (a i τ))).coeff n : ℂ)) = fun _ : ℍ ↦ (if n = 0 then (1 : ℂ) else 0) := by - funext τ; simp [coeff_one] + funext τ; simp only [prod_empty, coeff_one] rw [hconst] exact mdifferentiable_const | insert j s hj ih => @@ -590,15 +591,17 @@ lemma qExpansion_coeff_unique_raw {F : ℍ → ℂ} {c : ℕ → ℂ} have hball2 := hasFPowerSeriesOnBall_cuspFunction one_pos hFan hsum2 have heq := hball1.hasFPowerSeriesAt.eq_formalMultilinearSeries hball2.hasFPowerSeriesAt have hcoeff := congr_arg (fun p : FormalMultilinearSeries ℂ ℂ ℂ ↦ p.coeff n) heq - simpa [FormalMultilinearSeries.coeff_ofScalars] using hcoeff + simpa only [FormalMultilinearSeries.coeff_ofScalars] using hcoeff /-- The cusp function of the constant function `1` is the constant function `1`. -/ lemma cuspFunction_one_eq : cuspFunction 1 (1 : ℍ → ℂ) = 1 := by ext w rcases eq_or_ne w 0 with rfl | hw - · simpa [cuspFunction, Function.Periodic.cuspFunction] + · simpa only [cuspFunction, Function.Periodic.cuspFunction, Pi.one_comp, Function.update_self, + Pi.one_apply] using! tendsto_const_nhds.limUnder_eq - · simp [cuspFunction, Function.Periodic.cuspFunction_eq_of_nonzero 1 _ hw] + · simp only [cuspFunction, Pi.one_comp, Function.Periodic.cuspFunction_eq_of_nonzero 1 _ hw, + Pi.one_apply] /-- Powers preserve cusp-analyticity, and the `q`-expansion of a power is the power of the `q`-expansion. -/ @@ -662,7 +665,8 @@ lemma divByQ {F G : ℍ → ℂ} intro τ have h1 : HasSum (fun k ↦ (qExpansion 1 F).coeff (k + 1) • q τ ^ (k + 1)) (F τ) := by have hraw := (hasSum_nat_add_iff' 1).mpr (hFsum τ) - simpa [Finset.sum_range_one, hF0] using hraw + simpa only [smul_eq_mul, range_one, sum_singleton, hF0, pow_zero, mul_one, + sub_zero] using hraw have h2 := h1.mul_right (q τ)⁻¹ have hsimp : (fun k ↦ ((qExpansion 1 F).coeff (k + 1) • q τ ^ (k + 1)) * (q τ)⁻¹) = fun k ↦ (qExpansion 1 F).coeff (k + 1) • q τ ^ k := by @@ -696,7 +700,7 @@ private lemma isBoundedAtImInfty_jq_recon : IsBoundedAtImInfty (fun τ : ℍ ↦ have hE : IsBoundedAtImInfty ⇑E₄ := ModularFormClass.bdd_at_infty E₄ have hPinv : Filter.Tendsto (fun τ : ℍ ↦ (∏' n : ℕ, (1 - eta_q n ↑τ) ^ 24)⁻¹) atImInfty (nhds 1) := by - simpa using tendsto_atImInfty_tprod_one_sub_eta_q_pow.inv₀ one_ne_zero + simpa only [inv_one] using tendsto_atImInfty_tprod_one_sub_eta_q_pow.inv₀ one_ne_zero have hPb : IsBoundedAtImInfty (fun τ : ℍ ↦ (∏' n : ℕ, (1 - eta_q n ↑τ) ^ 24)⁻¹) := hPinv.isBigO_one ℝ exact Filter.BoundedAtFilter.mul hE (Filter.BoundedAtFilter.mul hE @@ -917,7 +921,7 @@ lemma Fi_some_eq [NeZero m] (k : ℕ) (b : ZMod m) (τ : ℍ) : /-- A function bounded by `1` in norm is bounded at `i∞`. -/ lemma isBoundedAtImInfty_of_norm_le_one {g : ℍ → ℂ} (hg : ∀ τ, ‖g τ‖ ≤ 1) : IsBoundedAtImInfty g := - Asymptotics.isBigO_of_le atImInfty (fun τ ↦ by simpa using hg τ) + Asymptotics.isBigO_of_le atImInfty (fun τ ↦ by simpa only [Pi.one_apply, norm_one] using hg τ) /-- `(j·q)ᵏ` composed with an upper-triangular isogeny `A` (lower-left entry `0`) is bounded at `i∞`, since the isogeny pushes towards the cusp. -/ @@ -943,7 +947,8 @@ lemma isBoundedAtImInfty_powerSum_mul_qpow [Fact m.Prime] (k : ℕ) : | none => change IsBoundedAtImInfty (fun τ : ℍ ↦ (f m none τ) ^ k * q τ ^ (m * k)) rw [funext (fun τ ↦ Fi_none_eq k τ)] - have hAI : (AInf m) 1 0 = 0 := by simp [val_AInf] + have hAI : (AInf m) 1 0 = 0 := by simp only [Fin.isValue, val_AInf, Matrix.of_apply, + Matrix.cons_val', Matrix.cons_val_zero, Matrix.cons_val_fin_one, Matrix.cons_val_one] exact isBoundedAtImInfty_jqPow_comp k (AInf m) hAI | some b => change IsBoundedAtImInfty (fun τ : ℍ ↦ (f m (some b) τ) ^ k * q τ ^ (m * k)) @@ -1039,7 +1044,7 @@ lemma cast_c [NeZero m] (k : ℕ) : (((m ^ 2 - 1) * k : ℕ) : ℤ) = (m : ℤ) ^ 2 * (k : ℤ) - (k : ℤ) := by have hkle : k ≤ m ^ 2 * k := Nat.le_mul_of_pos_left k (pow_pos (Nat.pos_of_ne_zero (NeZero.ne m)) 2) - rw [Nat.sub_one_mul, Nat.cast_sub hkle]; push_cast; ring + rw [Nat.sub_one_mul, Nat.cast_sub hkle]; push_cast; ac_rfl /-- **`q`-expansion of the averaged coset contribution `∑_b (f_b)ᵏ·q^{mk}`.** The root-of-unity average `sum_zetaM_zpow_mul` collapses the `b`-dependence, leaving an honest `q`-series with @@ -1180,7 +1185,7 @@ def polyJ : Subalgebra ℚ (ℍ → ℂ) := (Polynomial.aeval (fun τ : ℍ ↦ lemma aeval_j_apply (Q : Polynomial ℚ) (τ : ℍ) : (Polynomial.aeval (fun τ : ℍ ↦ j τ) Q) τ = Polynomial.aeval (j τ) Q := by have := Polynomial.aeval_algHom_apply (Pi.evalAlgHom ℚ (fun _ : ℍ ↦ ℂ) τ) (fun τ : ℍ ↦ j τ) Q - simpa using this.symm + simpa only [j_def, Pi.evalAlgHom_apply] using this.symm lemma mem_polyJ_iff {g : ℍ → ℂ} : g ∈ polyJ ↔ ∃ Q : Polynomial ℚ, ∀ τ, g τ = Polynomial.aeval (j τ) Q := by diff --git a/LeanPool/Chudnovsky/SingularModuli/ModularPolynomialZ.lean b/LeanPool/Chudnovsky/SingularModuli/ModularPolynomialZ.lean index 42f0e178c4..cfad28d837 100644 --- a/LeanPool/Chudnovsky/SingularModuli/ModularPolynomialZ.lean +++ b/LeanPool/Chudnovsky/SingularModuli/ModularPolynomialZ.lean @@ -329,7 +329,8 @@ lemma GoodQ.ana {h : ℝ} (hh : 0 < h) {R : Subring ℂ} {g : ℍ → ℂ} (hg : lemma GoodQ.add {h : ℝ} (hh : 0 < h) {R : Subring ℂ} {g₁ g₂ : ℍ → ℂ} (h₁ : GoodQ h R g₁) (h₂ : GoodQ h R g₂) : GoodQ h R (fun τ ↦ g₁ τ + g₂ τ) where per := by - have := h₁.per.add h₂.per; simpa [Function.comp_def] using this + have := h₁.per.add h₂.per; simpa only [Function.Periodic, Function.comp_apply, + Function.comp_def, Pi.add_apply] using this holo := h₁.holo.add h₂.holo bdd := h₁.bdd.add h₂.bdd mem n := by @@ -340,7 +341,8 @@ lemma GoodQ.add {h : ℝ} (hh : 0 < h) {R : Subring ℂ} {g₁ g₂ : ℍ → lemma GoodQ.mul {h : ℝ} (hh : 0 < h) {R : Subring ℂ} {g₁ g₂ : ℍ → ℂ} (h₁ : GoodQ h R g₁) (h₂ : GoodQ h R g₂) : GoodQ h R (fun τ ↦ g₁ τ * g₂ τ) where per := by - have := h₁.per.mul h₂.per; simpa [Function.comp_def] using this + have := h₁.per.mul h₂.per; simpa only [Function.Periodic, Function.comp_apply, + Function.comp_def, Pi.mul_apply] using this holo := h₁.holo.mul h₂.holo bdd := h₁.bdd.mul h₂.bdd mem n := by @@ -349,14 +351,14 @@ lemma GoodQ.mul {h : ℝ} (hh : 0 < h) {R : Subring ℂ} {g₁ g₂ : ℍ → exact R.sum_mem (fun p _ ↦ R.mul_mem (h₁.mem p.1) (h₂.mem p.2)) lemma goodQ_one {h : ℝ} (_hh : 0 < h) {R : Subring ℂ} : GoodQ h R (fun _ : ℍ ↦ (1:ℂ)) where - per := by simp + per := by simp only [Function.Periodic, Function.comp_apply, implies_true] holo := mdifferentiable_const bdd := Filter.const_boundedAtFilter atImInfty (1 : ℂ) mem n := by have h1 : (fun _ : ℍ ↦ (1:ℂ)) = (1 : ℍ → ℂ) := rfl rw [h1, qExpansion_one] rcases eq_or_ne n 0 with rfl | hn - · simp + · simp only [PowerSeries.coeff_one, ↓reduceIte, one_mem] · rw [PowerSeries.coeff_one, ite_eq_right hn]; exact R.zero_mem lemma goodQ_smul {h : ℝ} (hh : 0 < h) {R : Subring ℂ} {g : ℍ → ℂ} (hg : GoodQ h R g) @@ -384,13 +386,13 @@ lemma GoodQ.neg {h : ℝ} (hh : 0 < h) {R : Subring ℂ} {g : ℍ → ℂ} (hg : lemma GoodQ.sub {h : ℝ} (hh : 0 < h) {R : Subring ℂ} {g₁ g₂ : ℍ → ℂ} (h₁ : GoodQ h R g₁) (h₂ : GoodQ h R g₂) : GoodQ h R (fun τ ↦ g₁ τ - g₂ τ) := by have := h₁.add hh (h₂.neg hh) - simpa [sub_eq_add_neg] using this + simpa only [sub_eq_add_neg] using this /-- `wParam` is holomorphic. -/ lemma mdifferentiable_wParam : MDiff (fun τ : ℍ ↦ wParam m τ) := by have heq : (fun τ : ℍ ↦ wParam m τ) = (fun z : ℂ ↦ Complex.exp (2 * ↑π * Complex.I * z / m)) ∘ (fun τ : ℍ ↦ (τ : ℂ)) := by - funext τ; simp [wParam, Function.comp] + funext τ; simp only [wParam, Function.comp] rw [heq] exact Differentiable.comp_mdifferentiable (by fun_prop) mdifferentiable_coe @@ -398,7 +400,8 @@ lemma mdifferentiable_wParam : MDiff (fun τ : ℍ ↦ wParam m τ) := by lemma isBoundedAtImInfty_jqPow (k : ℕ) : IsBoundedAtImInfty (fun τ : ℍ ↦ (j τ * q τ) ^ k) := by have hA : (1 : GL (Fin 2) ℝ) 1 0 = 0 := by - simp [Matrix.one_apply_ne] + simp only [Fin.isValue, Units.val_one, ne_eq, one_ne_zero, not_false_eq_true, + Matrix.one_apply_ne] have h := isBoundedAtImInfty_jqPow_comp k 1 hA simpa only [one_smul] using h @@ -451,7 +454,7 @@ lemma goodQ_sum {h : ℝ} (hh : 0 < h) {R : Subring ℂ} {ι : Type*} (s : Finse (hg : ∀ i ∈ s, GoodQ h R (g i)) : GoodQ h R (fun τ ↦ ∑ i ∈ s, g i τ) := by classical induction s using Finset.induction with - | empty => simpa using goodQ_const hh (R := R) R.zero_mem + | empty => simpa only [sum_empty] using goodQ_const hh (R := R) R.zero_mem | @insert a s ha ih => have hrw : (fun τ ↦ ∑ i ∈ insert a s, g i τ) = (fun τ ↦ g a τ + ∑ i ∈ s, g i τ) := by @@ -477,7 +480,7 @@ lemma orbitPoly_coeff_isCuspMeroR_RQ [NeZero m] (n : ℕ) (P : Polynomial ℚ) Finset.sum_mul] refine Finset.sum_congr rfl (fun k hk ↦ ?_) have hk' : k ≤ N := Nat.lt_succ_iff.mp (Finset.mem_range.mp hk) - have hcast : algebraMap ℚ ℂ (P.coeff k) = ((P.coeff k : ℚ) : ℂ) := by simp + have hcast : algebraMap ℚ ℂ (P.coeff k) = ((P.coeff k : ℚ) : ℂ) := by simp only [eq_ratCast] have hdist : (j τ) ^ k * q τ ^ N = (j τ * q τ) ^ k * q τ ^ (N - k) := by rw [mul_pow, mul_assoc, ← pow_add, Nat.add_sub_cancel' hk'] rw [hcast, mul_assoc, hdist] @@ -505,7 +508,7 @@ lemma wExpansion_coeff_unique_raw [NeZero m] {F : ℍ → ℂ} {c : ℕ → ℂ} have hball2 := hasFPowerSeriesOnBall_cuspFunction hm hFan hsum2 have heq := hball1.hasFPowerSeriesAt.eq_formalMultilinearSeries hball2.hasFPowerSeriesAt have hcoeff := congr_arg (fun p : FormalMultilinearSeries ℂ ℂ ℂ ↦ p.coeff n) heq - simpa [FormalMultilinearSeries.coeff_ofScalars] using hcoeff + simpa only [FormalMultilinearSeries.coeff_ofScalars] using hcoeff /-! ## Width-`m` machinery: algebraic integrality of the `w`-expansion -/ @@ -521,15 +524,17 @@ lemma intCast_mem_RI (n : ℤ) : (n : ℂ) ∈ RI := intCast_mem RI n lemma zetaM_mem_RI [NeZero m] : zetaM m ∈ RI := by rw [mem_RI_iff] refine ⟨X ^ m - C 1, monic_X_pow_sub_C 1 (NeZero.ne m), ?_⟩ - simp [zetaM_pow_m] + simp only [algebraMap_int_eq, eq_intCast, Int.cast_one, eval₂_sub, eval₂_X_pow, zetaM_pow_m, + eval₂_one, sub_self] lemma zetaM_zpow_mem_RI [NeZero m] (n : ℤ) : zetaM m ^ n ∈ RI := by rw [mem_RI_iff] refine ⟨X ^ m - C 1, monic_X_pow_sub_C 1 (NeZero.ne m), ?_⟩ have hpow : (zetaM m ^ n) ^ m = 1 := by rw [← zpow_natCast (zetaM m ^ n) m, ← zpow_mul] - exact (zetaM_zpow_eq_one_iff (n * (m : ℤ))).mpr ⟨n, by ring⟩ - simp [hpow] + exact (zetaM_zpow_eq_one_iff (n * (m : ℤ))).mpr ⟨n, by ac_rfl⟩ + simp only [algebraMap_int_eq, eq_intCast, Int.cast_one, eval₂_sub, eval₂_X_pow, hpow, eval₂_one, + sub_self] /-- General period-`p` version of `periodic_comp_ofComplex_of_vadd`. -/ lemma periodic_comp_ofComplex_of_vadd_gen {f : ℍ → ℂ} {p : ℝ} (_hp : 0 < p) @@ -624,7 +629,8 @@ lemma goodQ_G_none [NeZero m] : rw [mul_one] at h rw [show wParam m τ ^ (m ^ 2) = q τ ^ m by have := wParam_pow_mk (m := m) 1 τ; rwa [mul_one, mul_one] at this] - simpa using h + simpa only [f_none, j_def, pow_one, mul_eq_mul_left_iff, mul_eq_zero, OfNat.ofNat_ne_zero, + false_or] using h have hpe : Function.Periodic ((fun τ : ℍ ↦ f m none τ * wParam m τ ^ (m ^ 2)) ∘ ofComplex) (m : ℝ) := periodic_comp_ofComplex_of_vadd_gen hm (fun τ ↦ by rw [f_vadd_m, wParam_vadd_m]) @@ -632,7 +638,9 @@ lemma goodQ_G_none [NeZero m] : (mdifferentiable_f none).mul (mdifferentiable_wParam.pow (m ^ 2)) have hbd : IsBoundedAtImInfty (fun τ : ℍ ↦ f m none τ * wParam m τ ^ (m ^ 2)) := by rw [funext hval] - exact isBoundedAtImInfty_jqPow_comp 1 (AInf m) (by simp [val_AInf]) + exact isBoundedAtImInfty_jqPow_comp 1 (AInf m) (by simp only [Fin.isValue, val_AInf, + Matrix.of_apply, Matrix.cons_val', Matrix.cons_val_zero, Matrix.cons_val_fin_one, + Matrix.cons_val_one]) refine goodQ_of_wHasSum hpe hho hbd (e := fun n ↦ m ^ 2 * n) (a := fun n ↦ ((PowerSeries.coeff n jqInt : ℤ) : ℂ)) (fun a b hab ↦ Nat.eq_of_mul_eq_mul_left (pow_pos (Nat.pos_of_ne_zero (NeZero.ne m)) 2) hab) @@ -706,7 +714,8 @@ lemma goodQ_G [NeZero m] (i : Option (ZMod m)) : lemma coeff_linMul_zero (α β : ℂ) (Q : Polynomial ℂ) : ((C α * X - C β) * Q).coeff 0 = -(β * Q.coeff 0) := by - rw [sub_mul, coeff_sub, mul_assoc, coeff_C_mul, coeff_C_mul, coeff_zero_eq_eval_zero]; simp + rw [sub_mul, coeff_sub, mul_assoc, coeff_C_mul, coeff_C_mul, coeff_zero_eq_eval_zero]; simp only [ + eval_mul, eval_X, zero_mul, mul_zero, zero_sub] lemma coeff_linMul_succ (α β : ℂ) (Q : Polynomial ℂ) (k : ℕ) : ((C α * X - C β) * Q).coeff (k + 1) = α * Q.coeff k - β * Q.coeff (k + 1) := by @@ -727,9 +736,9 @@ lemma goodQ_prod_coeff [NeZero m] (s : Finset (Option (ZMod m))) : intro n by_cases hn : n = 0 · refine (goodQ_const hm (show (1:ℂ) ∈ RI from RI.one_mem)).of_eq (fun τ ↦ ?_) - simp [hn] + simp only [map_pow, map_mul, prod_empty, hn, coeff_one_zero] · refine (goodQ_const hm RI.zero_mem).of_eq (fun τ ↦ ?_) - simp [Finset.prod_empty, coeff_one, hn] + simp only [map_pow, map_mul, prod_empty, coeff_one, hn, ↓reduceIte] | @insert a s ha ih => intro n cases n with diff --git a/LeanPool/Chudnovsky/SingularModuli/QuadraticPoints.lean b/LeanPool/Chudnovsky/SingularModuli/QuadraticPoints.lean index 0217c0375e..2a2aa1054e 100644 --- a/LeanPool/Chudnovsky/SingularModuli/QuadraticPoints.lean +++ b/LeanPool/Chudnovsky/SingularModuli/QuadraticPoints.lean @@ -153,7 +153,7 @@ lemma int_lin_eq_zero (τ : ℍ) {α β : ℤ} (h : (α : ℂ) * (τ : ℂ) + ( lemma IsPosDef.c_pos {f : BQF} (hf : IsPosDef f) : 0 < f.c := by obtain ⟨ha, hd⟩ := hf simp only [disc] at hd - nlinarith [sq_nonneg f.b, hd, ha] + nlinarith only [ha, hd] /-- The square-completion identity `(2aτ + b)² = disc f` for a root `τ` of `f`. -/ lemma sq_two_a_root {f : BQF} {τ : ℍ} (h : IsRoot f τ) : diff --git a/LeanPool/Chudnovsky/SingularModuli/Rationality.lean b/LeanPool/Chudnovsky/SingularModuli/Rationality.lean index 2532c520a1..af212f8bfd 100644 --- a/LeanPool/Chudnovsky/SingularModuli/Rationality.lean +++ b/LeanPool/Chudnovsky/SingularModuli/Rationality.lean @@ -112,7 +112,7 @@ def cmGL (n : ℤ) : GL (Fin 2) ℝ := lemma cmGL_det_pos (n : ℤ) : 0 < (cmGL n).det.val := by rw [Matrix.GeneralLinearGroup.val_det_apply, val_cmGL, Matrix.det_fin_two_of] - nlinarith [sq_nonneg (2 * (n : ℝ) + 1)] + linarith [sq_nonneg (2 * (n : ℝ) + 1)] /-- **`M_n` fixes `τ₁₆₃`** as a Möbius transformation. -/ lemma cmGL_smul_eq (n : ℤ) : cmGL n • τ₁₆₃ = τ₁₆₃ := by @@ -313,7 +313,7 @@ lemma fixes_of_coset {e f g : ℤ} (γ : SL(2, ℤ)) {Aτ τ' : ℍ} simp only [eq_intCast] at h0 push_cast at h0 obtain ⟨hc0, hd0⟩ := QF.int_lin_eq_zero Aτ h0 - rw [hc0, hd0] at hdet; simp at hdet + rw [hc0, hd0] at hdet; simp only [Fin.isValue, mul_zero, sub_self, zero_ne_one] at hdet rw [eq_div_iff hden, hW] at hco simp only [eq_intCast] at hco simp only [QF.Fixes] @@ -335,14 +335,14 @@ lemma exists_fixes_of_coincidence [Fact m.Prime] {τ' : ℍ} {i : Option (ZMod m obtain ⟨γ, hγ⟩ := j_injective_mod_Γ hj obtain ⟨p, q, r, s, hfix, hdet⟩ := fixes_of_coset (e := (m : ℤ)) (f := 0) (g := 1) γ - (by rw [coe_AInf_smul]; push_cast; ring) (by norm_num) hγ.symm + (by rw [coe_AInf_smul]; push_cast; ring) (by norm_num only) hγ.symm exact ⟨p, q, r, s, hfix, by rw [hdet]; ring⟩ | some b => have hj : j (Acol m (b.val : ℤ) • τ') = j τ' := by rw [← f_some]; exact h obtain ⟨γ, hγ⟩ := j_injective_mod_Γ hj obtain ⟨p, q, r, s, hfix, hdet⟩ := fixes_of_coset (e := 1) (f := (b.val : ℤ)) (g := (m : ℤ)) γ - (by rw [coe_Acol_smul]; push_cast; ring) (by exact_mod_cast hmpos.ne') hγ.symm + (by rw [coe_Acol_smul]; push_cast; ring) (by exact Nat.cast_ne_zero.mpr hmpos.ne') hγ.symm exact ⟨p, q, r, s, hfix, by rw [hdet]; ring⟩ /-- **(C4), packaged.** A coset coincidence at `τ′` produces a positive-definite integer form diff --git a/LeanPool/Chudnovsky/SingularModuli/Valence.lean b/LeanPool/Chudnovsky/SingularModuli/Valence.lean index f087862e34..8464ba36c9 100644 --- a/LeanPool/Chudnovsky/SingularModuli/Valence.lean +++ b/LeanPool/Chudnovsky/SingularModuli/Valence.lean @@ -140,8 +140,8 @@ theorem exists_units_smul_g₂_g₃ (L₁ L₂ : PeriodPair) suffices h : ∃ α : ℂ, α ≠ 0 ∧ (α ^ 4)⁻¹ * L₂.g₂ = L₁.g₂ ∧ (α ^ 6)⁻¹ * L₂.g₃ = L₁.g₃ by obtain ⟨α, hα, h2, h3⟩ := h refine ⟨Units.mk0 α hα, ?_, ?_⟩ - · rw [PeriodPair.g₂_smul]; simpa using h2 - · rw [PeriodPair.g₃_smul]; simpa using h3 + · rw [PeriodPair.g₂_smul]; simpa only [Units.val_mk0] using h2 + · rw [PeriodPair.g₃_smul]; simpa only [Units.val_mk0] using h3 by_cases ha2 : L₁.g₂ = 0 · -- `J₁ = 0`, so `L₂.g₂ = 0`; match the `g₃`'s by a 6th root. have ha3 : L₁.g₃ ≠ 0 := fun h ↦ hd₁ (by simp [PeriodPair.discr, ha2, h]) @@ -150,12 +150,12 @@ theorem exists_units_smul_g₂_g₃ (L₁ L₂ : PeriodPair) have : L₂.g₂ ^ 3 = 0 := by rcases mul_eq_zero.mp hz with h | h · exact h - · exact absurd (pow_eq_zero_iff (by norm_num) |>.mp h) ha3 - exact pow_eq_zero_iff (by norm_num) |>.mp this + · exact absurd (pow_eq_zero_iff (by norm_num1) |>.mp h) ha3 + exact pow_eq_zero_iff (by norm_num1) |>.mp this have hb3 : L₂.g₃ ≠ 0 := fun h ↦ hd₂ (by simp [PeriodPair.discr, hb2, h]) - obtain ⟨α, hα6⟩ := IsAlgClosed.exists_pow_nat_eq (L₂.g₃ / L₁.g₃) (n := 6) (by norm_num) + obtain ⟨α, hα6⟩ := IsAlgClosed.exists_pow_nat_eq (L₂.g₃ / L₁.g₃) (n := 6) (by norm_num1) have hαne : α ≠ 0 := by - rintro rfl; rw [zero_pow (by norm_num)] at hα6 + rintro rfl; rw [zero_pow (by norm_num1)] at hα6 exact (div_ne_zero hb3 ha3) hα6.symm refine ⟨α, hαne, ?_, ?_⟩ · rw [ha2, hb2]; ring @@ -166,13 +166,13 @@ theorem exists_units_smul_g₂_g₃ (L₁ L₂ : PeriodPair) have hz : L₁.g₂ ^ 3 * L₂.g₃ ^ 2 = 0 := by rw [hR, ha3]; ring have : L₂.g₃ ^ 2 = 0 := by rcases mul_eq_zero.mp hz with h | h - · exact absurd (pow_eq_zero_iff (by norm_num) |>.mp h) ha2 + · exact absurd (pow_eq_zero_iff (by norm_num1) |>.mp h) ha2 · exact h - exact pow_eq_zero_iff (by norm_num) |>.mp this + exact pow_eq_zero_iff (by norm_num1) |>.mp this have hb2 : L₂.g₂ ≠ 0 := fun h ↦ hd₂ (by simp [PeriodPair.discr, h, hb3]) - obtain ⟨α, hα4⟩ := IsAlgClosed.exists_pow_nat_eq (L₂.g₂ / L₁.g₂) (n := 4) (by norm_num) + obtain ⟨α, hα4⟩ := IsAlgClosed.exists_pow_nat_eq (L₂.g₂ / L₁.g₂) (n := 4) (by norm_num1) have hαne : α ≠ 0 := by - rintro rfl; rw [zero_pow (by norm_num)] at hα4 + rintro rfl; rw [zero_pow (by norm_num1)] at hα4 exact (div_ne_zero hb2 ha2) hα4.symm refine ⟨α, hαne, ?_, ?_⟩ · rw [hα4, inv_div, div_mul_cancel₀ _ hb2] @@ -184,9 +184,9 @@ theorem exists_units_smul_g₂_g₃ (L₁ L₂ : PeriodPair) have hz : L₁.g₂ ^ 3 * L₂.g₃ ^ 2 = 0 := by rw [hR, h]; ring have : L₂.g₃ ^ 2 = 0 := by rcases mul_eq_zero.mp hz with h' | h' - · exact absurd (pow_eq_zero_iff (by norm_num) |>.mp h') ha2 + · exact absurd (pow_eq_zero_iff (by norm_num1) |>.mp h') ha2 · exact h' - exact pow_eq_zero_iff (by norm_num) |>.mp this + exact pow_eq_zero_iff (by norm_num1) |>.mp this exact hd₂ (by simp [PeriodPair.discr, h, hb3z]) have hb3 : L₂.g₃ ≠ 0 := by intro h @@ -194,28 +194,28 @@ theorem exists_units_smul_g₂_g₃ (L₁ L₂ : PeriodPair) have : L₂.g₂ ^ 3 = 0 := by rcases mul_eq_zero.mp hz with h' | h' · exact h' - · exact absurd (pow_eq_zero_iff (by norm_num) |>.mp h') ha3 - exact hb2 (pow_eq_zero_iff (by norm_num) |>.mp this) + · exact absurd (pow_eq_zero_iff (by norm_num1) |>.mp h') ha3 + exact hb2 (pow_eq_zero_iff (by norm_num1) |>.mp this) -- `u = g₂₂/g₂₁`, `v = g₃₂/g₃₁`, and `u³ = v²`; pick `α` with `α² = v/u`. have hcube : (L₂.g₂ / L₁.g₂) ^ 3 = (L₂.g₃ / L₁.g₃) ^ 2 := by - field_simp + field_simp (disch := first | assumption | norm_num1 | positivity) linear_combination -hR obtain ⟨α, hα2⟩ := - IsAlgClosed.exists_pow_nat_eq ((L₂.g₃ / L₁.g₃) / (L₂.g₂ / L₁.g₂)) (n := 2) (by norm_num) + IsAlgClosed.exists_pow_nat_eq ((L₂.g₃ / L₁.g₃) / (L₂.g₂ / L₁.g₂)) (n := 2) (by norm_num1) have hu : L₂.g₂ / L₁.g₂ ≠ 0 := div_ne_zero hb2 ha2 have hv : L₂.g₃ / L₁.g₃ ≠ 0 := div_ne_zero hb3 ha3 have hαne : α ≠ 0 := by - rintro rfl; rw [zero_pow (by norm_num)] at hα2 + rintro rfl; rw [zero_pow (by norm_num1)] at hα2 exact (div_ne_zero hv hu) hα2.symm -- `α⁴ = (v/u)² = u` and `α⁶ = (v/u)³ = v`. have h4 : α ^ 4 = L₂.g₂ / L₁.g₂ := by have : α ^ 4 = (α ^ 2) ^ 2 := by ring rw [this, hα2, div_pow, ← hcube] - field_simp + field_simp (disch := first | assumption | norm_num1 | positivity) have h6 : α ^ 6 = L₂.g₃ / L₁.g₃ := by have : α ^ 6 = (α ^ 2) ^ 3 := by ring rw [this, hα2, div_pow, hcube] - field_simp + field_simp (disch := first | assumption | norm_num1 | positivity) refine ⟨α, hαne, ?_, ?_⟩ · rw [h4, inv_div, div_mul_cancel₀ _ hb2] · rw [h6, inv_div, div_mul_cancel₀ _ hb3] @@ -547,7 +547,7 @@ theorem lattice_eq_of_weierstrassP_eventuallyEq (L₁ L₂ : PeriodPair) have hScount : S.Countable := (lattice_countable L₁).union (lattice_countable L₂) have hUconn : IsPreconnected Sᶜ := (hScount.isConnected_compl_of_one_lt_rank - (by rw [Complex.rank_real_complex]; norm_num)).isPreconnected + (by rw [Complex.rank_real_complex]; norm_num1)).isPreconnected have hUdense : Dense Sᶜ := hScount.dense_compl ℝ have ha1 : AnalyticOnNhd ℂ L₁.weierstrassP Sᶜ := (L₁.analyticOnNhd_weierstrassP).mono @@ -586,7 +586,7 @@ lemma orient_eq {b s t : ℂ} {m₁ n₁ m₂ n₂ : ℤ} have e : starRingEnd ℂ b * (b * t) = ↑(Complex.normSq b) * t := by rw [← mul_assoc, ← Complex.normSq_eq_conj_mul_self] have hcb : starRingEnd ℂ b = ↑m₁ + ↑n₁ * starRingEnd ℂ s := by - rw [h1]; simp + rw [h1]; simp only [map_add, map_intCast, map_mul] rw [hcb, h2] at e have him := congrArg Complex.im e simp only [Complex.mul_im, Complex.add_im, Complex.add_re, Complex.intCast_im, @@ -873,7 +873,7 @@ theorem isClosed_range_j : IsClosed (Set.range (j : ℍ → ℂ)) := by have him2 : z.im ≤ M := hz.2.2.2 have habs : ‖z‖ ≤ |z.re| + |z.im| := Complex.norm_le_abs_re_add_abs_im z have himabs : |z.im| ≤ |M| := by - rw [abs_of_nonneg (le_trans (by norm_num) him1)] + rw [abs_of_nonneg (le_trans (by norm_num1) him1)] exact him2.trans (le_abs_self M) exact habs.trans (add_le_add hre himabs) have hKc_compact : IsCompact Kc := @@ -885,12 +885,12 @@ theorem isClosed_range_j : IsClosed (Set.range (j : ℍ → ℂ)) := by · rw [UpperHalfPlane.coe_im]; exact him_ge n · rw [UpperHalfPlane.coe_im]; exact him_le n obtain ⟨a, haKc, φ, hφmono, hφlim⟩ := hKc_compact.tendsto_subseq hmem - have haim : (0 : ℝ) < a.im := lt_of_lt_of_le (by norm_num) haKc.2.2.1 + have haim : (0 : ℝ) < a.im := lt_of_lt_of_le (by norm_num1) haKc.2.2.1 set τstar : ℍ := UpperHalfPlane.mk a haim with hτstar have hcoe : (τstar : ℂ) = a := rfl have htend : Filter.Tendsto (fun k => τ (φ k)) Filter.atTop (𝓝 τstar) := by rw [UpperHalfPlane.isEmbedding_coe.tendsto_nhds_iff] - simpa [Function.comp_def, hcoe] using hφlim + simpa only [Function.comp_def, hcoe] using hφlim have hjcont : Continuous (j : ℍ → ℂ) := mdifferentiable_j.continuous have htendj : Filter.Tendsto (fun k => j (τ (φ k))) Filter.atTop (𝓝 (j τstar)) := (hjcont.tendsto τstar).comp htend diff --git a/LeanPool/Chudnovsky/WeierstrassMore.lean b/LeanPool/Chudnovsky/WeierstrassMore.lean index 12e7b92aa2..1a477c5b6b 100644 --- a/LeanPool/Chudnovsky/WeierstrassMore.lean +++ b/LeanPool/Chudnovsky/WeierstrassMore.lean @@ -113,7 +113,7 @@ theorem meromorphicOrderAt_weierstrassP_sub {c : ℂ} {l₀ : ℂ} (h : l₀ ∈ /-- `℘ - c` is an elliptic function. -/ theorem isEllipticWith_weierstrassP_sub (c : ℂ) : L.IsEllipticWith (fun z => ℘[L] z - c) := - ⟨by fun_prop, fun z l => by simp⟩ + ⟨by fun_prop, fun z l => by simp only [weierstrassP_add_coe]⟩ /-- **Counting bound** from the third Liouville theorem: the elliptic function `℘ - c` has, counted with multiplicity, at most `2` zeros in the fundamental parallelogram, since @@ -220,7 +220,7 @@ theorem half_ne_half {a b a' b' : ℝ} (h : ¬ (a = a' ∧ b = b')) : a • L.ω₁ + b • L.ω₂ ≠ a' • L.ω₁ + b' • L.ω₂ := by intro he have he' : (a : ℂ) * L.ω₁ + (b : ℂ) * L.ω₂ = (a' : ℂ) * L.ω₁ + (b' : ℂ) * L.ω₂ := by - simpa [Complex.real_smul] using he + simpa only [Complex.real_smul] using he have key : (a - a') • L.ω₁ + (b - b') • L.ω₂ = 0 := by simp only [sub_smul, Complex.real_smul]; linear_combination he' obtain ⟨h1, h2⟩ := LinearIndependent.pair_iff.mp L.indep _ _ key @@ -256,37 +256,43 @@ theorem weierstrassP_ne_of_half {p q : ℂ} /-- Membership of `ω₁/2` in the fundamental parallelogram. -/ private theorem mem_fund_ω₁_div_two : L.ω₁ / 2 ∈ L.fundamentalParallelogram := - ⟨1 / 2, ⟨by norm_num, by norm_num⟩, 0, ⟨le_refl 0, zero_lt_one⟩, by - simp [Complex.real_smul]; ring⟩ + ⟨1 / 2, ⟨by norm_num1, by norm_num1⟩, 0, ⟨le_refl 0, zero_lt_one⟩, by + simp only [one_div, Complex.real_smul, Complex.ofReal_inv, Complex.ofReal_ofNat, zero_smul, + add_zero]; ac_rfl⟩ private theorem mem_fund_ω₂_div_two : L.ω₂ / 2 ∈ L.fundamentalParallelogram := - ⟨0, ⟨le_refl 0, zero_lt_one⟩, 1 / 2, ⟨by norm_num, by norm_num⟩, by - simp [Complex.real_smul]; ring⟩ + ⟨0, ⟨le_refl 0, zero_lt_one⟩, 1 / 2, ⟨by norm_num1, by norm_num1⟩, by + simp only [zero_smul, one_div, Complex.real_smul, Complex.ofReal_inv, Complex.ofReal_ofNat, + zero_add]; ac_rfl⟩ private theorem mem_fund_add_div_two : (L.ω₁ + L.ω₂) / 2 ∈ L.fundamentalParallelogram := - ⟨1 / 2, ⟨by norm_num, by norm_num⟩, 1 / 2, ⟨by norm_num, by norm_num⟩, by - simp [Complex.real_smul]; ring⟩ + ⟨1 / 2, ⟨by norm_num1, by norm_num1⟩, 1 / 2, ⟨by norm_num1, by norm_num1⟩, by + simp only [one_div, Complex.real_smul, Complex.ofReal_inv, Complex.ofReal_ofNat]; ring⟩ private theorem ω₁_div_two_ne_ω₂_div_two : L.ω₁ / 2 ≠ L.ω₂ / 2 := by have h := L.half_ne_half (a := 1 / 2) (b := 0) (a' := 0) (b' := 1 / 2) (by norm_num) rwa [show (1 / 2 : ℝ) • L.ω₁ + (0 : ℝ) • L.ω₂ = L.ω₁ / 2 by - simp [Complex.real_smul]; ring, + simp only [one_div, Complex.real_smul, Complex.ofReal_inv, Complex.ofReal_ofNat, zero_smul, + add_zero]; ac_rfl, show (0 : ℝ) • L.ω₁ + (1 / 2 : ℝ) • L.ω₂ = L.ω₂ / 2 by - simp [Complex.real_smul]; ring] at h + simp only [zero_smul, one_div, Complex.real_smul, Complex.ofReal_inv, Complex.ofReal_ofNat, + zero_add]; ac_rfl] at h private theorem ω₁_div_two_ne_add_div_two : L.ω₁ / 2 ≠ (L.ω₁ + L.ω₂) / 2 := by have h := L.half_ne_half (a := 1 / 2) (b := 0) (a' := 1 / 2) (b' := 1 / 2) (by norm_num) rwa [show (1 / 2 : ℝ) • L.ω₁ + (0 : ℝ) • L.ω₂ = L.ω₁ / 2 by - simp [Complex.real_smul]; ring, + simp only [one_div, Complex.real_smul, Complex.ofReal_inv, Complex.ofReal_ofNat, zero_smul, + add_zero]; ac_rfl, show (1 / 2 : ℝ) • L.ω₁ + (1 / 2 : ℝ) • L.ω₂ = (L.ω₁ + L.ω₂) / 2 by - simp [Complex.real_smul]; ring] at h + simp only [one_div, Complex.real_smul, Complex.ofReal_inv, Complex.ofReal_ofNat]; ring] at h private theorem ω₂_div_two_ne_add_div_two : L.ω₂ / 2 ≠ (L.ω₁ + L.ω₂) / 2 := by have h := L.half_ne_half (a := 0) (b := 1 / 2) (a' := 1 / 2) (b' := 1 / 2) (by norm_num) rwa [show (0 : ℝ) • L.ω₁ + (1 / 2 : ℝ) • L.ω₂ = L.ω₂ / 2 by - simp [Complex.real_smul]; ring, + simp only [zero_smul, one_div, Complex.real_smul, Complex.ofReal_inv, Complex.ofReal_ofNat, + zero_add]; ac_rfl, show (1 / 2 : ℝ) • L.ω₁ + (1 / 2 : ℝ) • L.ω₂ = (L.ω₁ + L.ω₂) / 2 by - simp [Complex.real_smul]; ring] at h + simp only [one_div, Complex.real_smul, Complex.ofReal_inv, Complex.ofReal_ofNat]; ring] at h /-- The half-lattice values are pairwise distinct: `e₁ ≠ e₂`. -/ theorem e₁_ne_e₂ : L.e₁ ≠ L.e₂ :=