From f22c3485e96799d37643ffc19953442d0ba9c970 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Tue, 3 Nov 2026 16:24:36 +0000 Subject: [PATCH] Optimize Chudnovsky proof elaboration and build dependencies --- LeanPool/Chudnovsky/BernoulliValues.lean | 39 +++ LeanPool/Chudnovsky/Clausen.lean | 66 +--- LeanPool/Chudnovsky/Coefficients.lean | 150 +++++---- LeanPool/Chudnovsky/DivisionValues.lean | 55 ++-- LeanPool/Chudnovsky/Estimates.lean | 11 +- LeanPool/Chudnovsky/Fourier.lean | 3 +- LeanPool/Chudnovsky/Imports.lean | 2 + LeanPool/Chudnovsky/Liouville.lean | 308 ++++++------------ LeanPool/Chudnovsky/Periodicity.lean | 38 +++ LeanPool/Chudnovsky/PicardFuchs.lean | 7 +- LeanPool/Chudnovsky/Ramanujan.lean | 16 +- LeanPool/Chudnovsky/SigmaZeta.lean | 6 - .../SingularModuli/FormReduction.lean | 23 +- .../Chudnovsky/SingularModuli/JFunction.lean | 20 +- .../Chudnovsky/SingularModuli/Kronecker.lean | 2 +- .../SingularModuli/ModularPolynomialQ.lean | 2 +- .../SingularModuli/ModularPolynomialZ.lean | 2 +- LeanPool/Chudnovsky/WeierstrassMore.lean | 6 - 18 files changed, 336 insertions(+), 420 deletions(-) create mode 100644 LeanPool/Chudnovsky/BernoulliValues.lean create mode 100644 LeanPool/Chudnovsky/Periodicity.lean diff --git a/LeanPool/Chudnovsky/BernoulliValues.lean b/LeanPool/Chudnovsky/BernoulliValues.lean new file mode 100644 index 0000000000..f7c86a2229 --- /dev/null +++ b/LeanPool/Chudnovsky/BernoulliValues.lean @@ -0,0 +1,39 @@ +/- +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.NumberTheory.Bernoulli + +/-! +# Bernoulli values used in the Chudnovsky formula + +Evaluate the two small Bernoulli numbers once, without unfolding their recursive definitions +inside the analytic developments that use them. +-/ + +public section + +namespace Chudnovsky + +/-- The fourth Bernoulli number, using the known value of `bernoulli'`. -/ +lemma bernoulli_four_value : bernoulli 4 = -1 / 30 := by + rw [bernoulli, bernoulli'_four] + norm_num + +/-- 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 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] + rw [bernoulli, h6] + norm_num + +end Chudnovsky diff --git a/LeanPool/Chudnovsky/Clausen.lean b/LeanPool/Chudnovsky/Clausen.lean index 6e00c842ae..1318e54138 100644 --- a/LeanPool/Chudnovsky/Clausen.lean +++ b/LeanPool/Chudnovsky/Clausen.lean @@ -9,13 +9,9 @@ public import Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric public import Mathlib.Analysis.CStarAlgebra.Classes public import Mathlib.Analysis.Calculus.Deriv.Basic import Mathlib.Algebra.Order.Ring.Star +import Mathlib.Analysis.Calculus.Deriv.Pow import Mathlib.Analysis.Calculus.SmoothSeries -import Mathlib.Analysis.Complex.UpperHalfPlane.Basic -import Mathlib.Analysis.SpecialFunctions.Bernstein -import Mathlib.Analysis.SpecialFunctions.Gamma.Basic -import Mathlib.Combinatorics.Matroid.Init -import Mathlib.Data.Nat.Choose.Multinomial -import Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt +import Mathlib.Topology.Algebra.Module.ModuleTopology -- shake: keep /-! # Clausen's formula and the hypergeometric differential equations @@ -1079,8 +1075,7 @@ theorem clausen_coeff_identity (n : ℕ) : /-- Clausen's formula specialized to `a = 1/12`, `b = 5/12` (paper Thm. `satzclausen`): `(₂F₁(1/12, 5/12; 1; z))² = ₃F₂(1/6, 5/6, 1/2; 1, 1; z)` for `‖z‖ < 1`. -The analytic reduction (Cauchy product of the square, coefficient comparison) is carried out -here; the remaining arithmetic core is `clausen_coeff_identity`. -/ +This follows directly from the general formula, with both lower parameters equal to `1`. -/ theorem hyp2F1_sq_eq_hyp3F2 {z : ℂ} (hz : ‖z‖ < 1) : hyp2F1 z ^ 2 = hyp3F2 z := by -- Non-degeneracy of the lower parameter `c = 1` (and of `a = 1/12`, `b = 5/12`). have hnd : ∀ kn : ℕ, (kn : ℂ) ≠ -(1 / 12) ∧ (kn : ℂ) ≠ -(5 / 12) ∧ (kn : ℂ) ≠ -1 := by @@ -1092,55 +1087,12 @@ theorem hyp2F1_sq_eq_hyp3F2 {z : ℂ} (hz : ‖z‖ < 1) : hyp2F1 z ^ 2 = hyp3F2 rw [Nat.cast_eq_zero] at h0; omega · have h0 : ((kn + 1 : ℕ) : ℂ) = 0 := by push_cast; linear_combination h rw [Nat.cast_eq_zero] at h0; omega - -- Absolute convergence of the `₂F₁` series, needed for the Cauchy product. - have hfsum : Summable fun n : ℕ => - ‖ordinaryHypergeometricCoefficient (1 / 12 : ℂ) (5 / 12) 1 n * z ^ n‖ := - ordinaryHypergeometric_norm_summable (1 / 12) (5 / 12) 1 hnd hz - -- `hyp2F1 z` as a `tsum` of `cₖ zᵏ`. - have hL : hyp2F1 z = - ∑' n : ℕ, ordinaryHypergeometricCoefficient (1 / 12 : ℂ) (5 / 12) 1 n * z ^ n := by - rw [hyp2F1, ordinaryHypergeometric, ordinaryHypergeometric_sum_eq] - exact tsum_congr fun n => smul_eq_mul _ _ - -- `hyp3F2 z` as a `tsum` of `dₙ zⁿ`. - have hR : hyp3F2 z = - ∑' n : ℕ, generalizedHypergeometricCoefficient (1 / 6 : ℂ) (5 / 6) (1 / 2) 1 1 n * z ^ n := by - rw [hyp3F2, generalizedHypergeometric, generalizedHypergeometric_sum_eq] - exact tsum_congr fun n => smul_eq_mul _ _ - -- The square is the Cauchy product; compare coefficients. - rw [sq, hL, hR, tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm hfsum hfsum] - refine tsum_congr fun n => ?_ - -- Pull `zⁿ` out of the finite convolution sum. - have hz_pow : ∀ k ∈ Finset.range (n + 1), - ordinaryHypergeometricCoefficient (1 / 12 : ℂ) (5 / 12) 1 k * z ^ k * - (ordinaryHypergeometricCoefficient (1 / 12 : ℂ) (5 / 12) 1 (n - k) * z ^ (n - k)) - = ordinaryHypergeometricCoefficient (1 / 12 : ℂ) (5 / 12) 1 k * - ordinaryHypergeometricCoefficient (1 / 12 : ℂ) (5 / 12) 1 (n - k) * z ^ n := by - intro k hk - rw [Finset.mem_range, Nat.lt_succ_iff] at hk - have hpow : z ^ k * z ^ (n - k) = z ^ n := by rw [← pow_add, Nat.add_sub_cancel' hk] - linear_combination (ordinaryHypergeometricCoefficient (1 / 12 : ℂ) (5 / 12) 1 k * - ordinaryHypergeometricCoefficient (1 / 12 : ℂ) (5 / 12) 1 (n - k)) * hpow - rw [Finset.sum_congr rfl hz_pow, ← Finset.sum_mul] - -- Reduce the complex coefficient identity to the rational one. - congr 1 - have hq := clausen_coeff_identity n - have hsumcast : (∑ k ∈ Finset.range (n + 1), - ordinaryHypergeometricCoefficient (1 / 12 : ℂ) (5 / 12) 1 k * - ordinaryHypergeometricCoefficient (1 / 12 : ℂ) (5 / 12) 1 (n - k)) - = ((∑ k ∈ Finset.range (n + 1), - ordinaryHypergeometricCoefficient (1 / 12 : ℚ) (5 / 12) 1 k * - ordinaryHypergeometricCoefficient (1 / 12 : ℚ) (5 / 12) 1 (n - k) : ℚ) : ℂ) := by - rw [Rat.cast_sum] - refine Finset.sum_congr rfl fun k _ => ?_ - rw [Rat.cast_mul, ordinaryHypergeometricCoefficient_ratCast, - ordinaryHypergeometricCoefficient_ratCast] - norm_num - have hgencast : - generalizedHypergeometricCoefficient (1 / 6 : ℂ) (5 / 6) (1 / 2) 1 1 n - = ((generalizedHypergeometricCoefficient (1 / 6 : ℚ) (5 / 6) (1 / 2) 1 1 n : ℚ) : ℂ) := by - rw [generalizedHypergeometricCoefficient_ratCast] - norm_num - rw [hsumcast, hgencast, hq] + have hc : (1 / 12 : ℂ) + 5 / 12 + 1 / 2 = 1 := by norm_num + have hc' : 2 * (1 / 12 : ℂ) + 2 * (5 / 12) = 1 := by norm_num + have h := clausen_formula (1 / 12 : ℂ) (5 / 12) + (fun k => by rw [hc]; exact (hnd k).2.2) + (fun k => by rw [hc']; exact (hnd k).2.2) hz + convert h using 1 <;> norm_num [hyp2F1, hyp3F2] /-- The Pochhammer/factorial identity from the proof of paper Thm. `darst`: `(1/6)ₙ · (1/2)ₙ · (5/6)ₙ = (6n)! / ((3n)! · 12^(3n))`, stated over `ℚ`. -/ diff --git a/LeanPool/Chudnovsky/Coefficients.lean b/LeanPool/Chudnovsky/Coefficients.lean index 1ee0329cd4..5b8b1adb55 100644 --- a/LeanPool/Chudnovsky/Coefficients.lean +++ b/LeanPool/Chudnovsky/Coefficients.lean @@ -50,72 +50,75 @@ open scoped Real Proved by monotone rational enclosures of the numerator `(1-240e+2160e²)³` and the `24`-th power `(1+e-e²)²⁴`, followed by `norm_num` on the two resulting rational -inequalities (whose `24`-th powers of the ~47-digit endpoints have ~4500 digits). -/ +inequalities, using rounded endpoints sufficient for the `1/2` tolerance. -/ 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.80898093700765233822623151648e-18 : ℝ) ^ 2 := + 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.80898093700765233822623151648e-18 : ℝ) + 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.80898093700765233822623151647e-18 - + 2160 * (3.80898093700765233822623151648e-18) ^ 2 : ℝ) := by linarith only [hL, he2U] - have hGLpos : (0 : ℝ) < 1 - 240 * 3.80898093700765233822623151648e-18 := by norm_num + (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.80898093700765233822623151647e-18 - - (3.80898093700765233822623151648e-18) ^ 2 : ℝ) ≤ 1 + e - e ^ 2 := by + 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.80898093700765233822623151648e-18 : ℝ) := by + have hhHH : 1 + e - e ^ 2 ≤ (1 + 3.808980937007652339e-18 : ℝ) := by linarith only [hU, he2nn] - have hHLpos : (0 : ℝ) < 1 + 3.80898093700765233822623151647e-18 - - (3.80898093700765233822623151648e-18) ^ 2 := by norm_num + 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.80898093700765233822623151647e-18 - + 2160 * (3.80898093700765233822623151648e-18) ^ 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.80898093700765233822623151648e-18) ^ 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.80898093700765233822623151648e-18) ^ 24 := + 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.80898093700765233822623151647e-18 - - (3.80898093700765233822623151648e-18) ^ 2) ^ 24 ≤ (1 + e - e ^ 2) ^ 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.80898093700765233822623151647e-18 - + 2160 * (3.80898093700765233822623151648e-18) ^ 2) ^ 3 / - (3.80898093700765233822623151647e-18 * - (1 + 3.80898093700765233822623151647e-18 - - (3.80898093700765233822623151648e-18) ^ 2) ^ 24) := by + (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.80898093700765233822623151648e-18) ^ 3 / - (3.80898093700765233822623151648e-18 * - (1 + 3.80898093700765233822623151648e-18) ^ 24) ≤ + 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.80898093700765233822623151647e-18 - + 2160 * (3.80898093700765233822623151648e-18) ^ 2) ^ 3 / - (3.80898093700765233822623151647e-18 * - (1 + 3.80898093700765233822623151647e-18 - - (3.80898093700765233822623151648e-18) ^ 2) ^ 24) < (640320 : ℝ) ^ 3 + 1 / 2 := by + 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.80898093700765233822623151648e-18) ^ 3 / - (3.80898093700765233822623151648e-18 * - (1 + 3.80898093700765233822623151648e-18) ^ 24) := by + (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], @@ -199,65 +202,72 @@ 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 ≤ (3.80898093700765233822623151648e-18 : ℝ) ^ 2 := + have he2U : e ^ 2 ≤ (4e-18 : ℝ) ^ 2 := pow_le_pow_left₀ hepos.le heU.le 2 - have he2L : (3.80898093700765233822623151647e-18 : ℝ) ^ 2 ≤ e ^ 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 * 3.80898093700765233822623151648e-18 : ℝ) + 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 * 3.80898093700765233822623151647e-18 - + 2160 * (3.80898093700765233822623151648e-18) ^ 2 : ℝ) := by linarith only [heL, he2U] + (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 * 3.80898093700765233822623151647e-18 - - 16632 * (3.80898093700765233822623151648e-18) ^ 2 : ℝ) + 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 * 3.80898093700765233822623151648e-18 : ℝ) := by + 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.14159265358979323846 * (12.7671453348037046617 / 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.14159265358979323847 * (12.7671453348037046618 / 2)) : ℝ) + 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 * 3.80898093700765233822623151647e-18 - - 72 * (3.80898093700765233822623151648e-18) ^ 2 - - 3 / (3.14159265358979323846 * (12.7671453348037046617 / 2)) : ℝ) + 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 * 3.80898093700765233822623151648e-18 - - 72 * (3.80898093700765233822623151647e-18) ^ 2 - - 3 / (3.14159265358979323847 * (12.7671453348037046618 / 2)) : ℝ) := by + (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 * 3.80898093700765233822623151648e-18) - * (1 + 24 * 3.80898093700765233822623151647e-18 - - 72 * (3.80898093700765233822623151648e-18) ^ 2 - - 3 / (3.14159265358979323846 * (12.7671453348037046617 / 2))) + 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 * 3.80898093700765233822623151647e-18 - + 2160 * (3.80898093700765233822623151648e-18) ^ 2) - * (1 + 24 * 3.80898093700765233822623151648e-18 - - 72 * (3.80898093700765233822623151647e-18) ^ 2 - - 3 / (3.14159265358979323847 * (12.7671453348037046618 / 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) @@ -271,11 +281,11 @@ private lemma s2tilde_real_bound {e pv sv : ℝ} 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 * 3.80898093700765233822623151648e-18) - < (1 - 240 * 3.80898093700765233822623151648e-18) - * (1 + 24 * 3.80898093700765233822623151647e-18 - - 72 * (3.80898093700765233822623151648e-18) ^ 2 - - 3 / (3.14159265358979323846 * (12.7671453348037046617 / 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))) @@ -284,14 +294,14 @@ private lemma s2tilde_real_bound {e pv sv : ℝ} 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 * 3.80898093700765233822623151647e-18 - + 2160 * (3.80898093700765233822623151648e-18) ^ 2) - * (1 + 24 * 3.80898093700765233822623151648e-18 - - 72 * (3.80898093700765233822623151647e-18) ^ 2 - - 3 / (3.14159265358979323847 * (12.7671453348037046618 / 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 * 3.80898093700765233822623151647e-18 - - 16632 * (3.80898093700765233822623151648e-18) ^ 2) := by norm_num + < (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]⟩ diff --git a/LeanPool/Chudnovsky/DivisionValues.lean b/LeanPool/Chudnovsky/DivisionValues.lean index 69302f7362..b91c18a632 100644 --- a/LeanPool/Chudnovsky/DivisionValues.lean +++ b/LeanPool/Chudnovsky/DivisionValues.lean @@ -1736,11 +1736,9 @@ private lemma E_natDegree : E.natDegree = 6 := by private lemma E_leadingCoeff : E.leadingCoeff = 16 := by have hq : (X ^ 3 - C h2 * X - C h3 : Coeff[X]).Monic := by - have h : (X ^ 3 - C h2 * X - C h3 : Coeff[X]) - = X ^ (2 + 1) - (C h2 * X + C h3) := by ring - rw [h] - refine Polynomial.monic_X_pow_sub ?_ - compute_degree! + rw [sub_sub] + exact Polynomial.monic_X_pow_sub + (Polynomial.degree_linear_le.trans_lt (by norm_num)) rw [E, Polynomial.leadingCoeff_mul, Polynomial.leadingCoeff_pow, hq.leadingCoeff, one_pow, mul_one] rw [show (16 : Coeff[X]) = Polynomial.C (16 : Coeff) from (map_ofNat Polynomial.C 16).symm, @@ -2208,10 +2206,13 @@ theorem Fm_two {z : ℂ} (hz : z ∉ L.lattice) : ring have hσdiff : Differentiable ℂ L.weierstrassSigma := L.differentiable_weierstrassSigma have hHdiff : DifferentiableAt ℂ H z := by - have h1 : DifferentiableAt ℂ (fun v : ℂ => L.weierstrassSigma (z + v)) z := by fun_prop - have h2 : DifferentiableAt ℂ (fun v : ℂ => Q (z - v)) z := by fun_prop + have h1 : DifferentiableAt ℂ (fun v : ℂ => L.weierstrassSigma (z + v)) z := + (hσdiff.comp ((differentiable_const _).add differentiable_id)).differentiableAt + have h2 : DifferentiableAt ℂ (fun v : ℂ => Q (z - v)) z := + (hQdiff.comp ((differentiable_const _).sub differentiable_id)).differentiableAt have h3 : DifferentiableAt ℂ - (fun v : ℂ => L.weierstrassSigma z ^ 2 * L.weierstrassSigma v ^ 2) z := by fun_prop + (fun v : ℂ => L.weierstrassSigma z ^ 2 * L.weierstrassSigma v ^ 2) z := + ((differentiable_const _).mul (hσdiff.pow 2)).differentiableAt exact (h1.mul h2).div h3 (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 @@ -2958,33 +2959,17 @@ private lemma isIntegral_of_Pc_root (m l : ℕ) (hl : l ≠ 0) 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 - refine ⟨Polynomial.X ^ 3 - - Polynomial.C (⟨L.g₂ / 4, Algebra.subset_adjoin (by simp)⟩ : - (Algebra.adjoin ℤ ({L.g₂ / 4, L.g₃ / 4} : Set ℂ))) * Polynomial.X - - Polynomial.C (⟨L.g₃ / 4, Algebra.subset_adjoin (by simp)⟩ : - (Algebra.adjoin ℤ ({L.g₂ / 4, L.g₃ / 4} : Set ℂ))), ?_, ?_⟩ - · have h : (Polynomial.X ^ 3 - - Polynomial.C (⟨L.g₂ / 4, Algebra.subset_adjoin (by simp)⟩ : - (Algebra.adjoin ℤ ({L.g₂ / 4, L.g₃ / 4} : Set ℂ))) * Polynomial.X - - Polynomial.C (⟨L.g₃ / 4, Algebra.subset_adjoin (by simp)⟩ : - (Algebra.adjoin ℤ ({L.g₂ / 4, L.g₃ / 4} : Set ℂ)))) - = Polynomial.X ^ (2 + 1) - - (Polynomial.C (⟨L.g₂ / 4, Algebra.subset_adjoin (by simp)⟩ : - (Algebra.adjoin ℤ ({L.g₂ / 4, L.g₃ / 4} : Set ℂ))) * Polynomial.X - + Polynomial.C (⟨L.g₃ / 4, Algebra.subset_adjoin (by simp)⟩ : - (Algebra.adjoin ℤ ({L.g₂ / 4, L.g₃ / 4} : Set ℂ)))) := by - ring - rw [h] - refine Polynomial.monic_X_pow_sub ?_ - compute_degree! - · simp only [Polynomial.eval₂_sub, Polynomial.eval₂_mul, Polynomial.eval₂_pow, - Polynomial.eval₂_X, Polynomial.eval₂_C] - have hc2 : algebraMap (Algebra.adjoin ℤ ({L.g₂ / 4, L.g₃ / 4} : Set ℂ)) ℂ - ⟨L.g₂ / 4, Algebra.subset_adjoin (by simp)⟩ = L.g₂ / 4 := rfl - have hc3 : algebraMap (Algebra.adjoin ℤ ({L.g₂ / 4, L.g₃ / 4} : Set ℂ)) ℂ - ⟨L.g₃ / 4, Algebra.subset_adjoin (by simp)⟩ = L.g₃ / 4 := rfl - rw [hc2, hc3] - linear_combination hx / 4 + 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)⟩ + 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)) + · 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) + simpa only [sub_sub] using hzero /-- The evaluation of the Baker product at a division value vanishes. -/ private lemma eval_baker_zero (m : ℕ) [NeZero m] {v : Fin m × Fin m} (hv : v ≠ 0) : diff --git a/LeanPool/Chudnovsky/Estimates.lean b/LeanPool/Chudnovsky/Estimates.lean index 1bd3df6e09..69ef4c254b 100644 --- a/LeanPool/Chudnovsky/Estimates.lean +++ b/LeanPool/Chudnovsky/Estimates.lean @@ -6,6 +6,7 @@ Authors: Xuanji Li module public import LeanPool.Chudnovsky.Basic +import LeanPool.Chudnovsky.BernoulliValues import Mathlib.Analysis.Complex.ExponentialBounds import Mathlib.Analysis.Real.Pi.Bounds @@ -148,7 +149,7 @@ lemma summable_norm_sigma_q (k : ℕ) (τ : ℍ) : lemma E₄_eq_tsum (τ : ℍ) : E₄ τ = 1 + 240 * ∑' n : ℕ, (ArithmeticFunction.sigma 3 (n + 1) : ℂ) * q τ ^ (n + 1) := by have h := EisensteinSeries.q_expansion_bernoulli (k := 4) (by norm_num) (by decide) τ - rw [show bernoulli 4 = -1 / 30 by decide +kernel, ← q_eq] at h + rw [show bernoulli 4 = -1 / 30 by as_aux_lemma => exact bernoulli_four_value, ← q_eq] at h simp only [zpow_natCast] at h rw [tsum_pnat_eq_tsum_succ (f := fun n ↦ (ArithmeticFunction.sigma 3 n : ℂ) * q τ ^ n)] at h rw [h]; norm_num @@ -157,7 +158,7 @@ lemma E₄_eq_tsum (τ : ℍ) : 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) τ - rw [show bernoulli 6 = 1 / 42 by decide +kernel, ← q_eq] at h + 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 @@ -507,14 +508,14 @@ lemma norm_sub_E₄trunc_le {τ : ℍ} (hτ : τ ∈ Region) : ‖E₄ τ - E₄trunc τ‖ ≤ 6744 * ‖q τ‖ ^ 3 := by have heq : E₄ τ - E₄trunc τ = 240 * eisensteinTail 3 3 τ := by rw [E₄_eq_trunc τ]; ring rw [heq, norm_mul, Complex.norm_ofNat] - nlinarith [norm_eisensteinTail_sigma₃ hτ, norm_nonneg (eisensteinTail 3 3 τ)] + linarith only [norm_eisensteinTail_sigma₃ hτ, pow_nonneg (norm_nonneg (q τ)) 3] /-- `|δY| = |E₆ - Y| ≤ 123783·|q|³`. -/ lemma norm_sub_E₆trunc_le {τ : ℍ} (hτ : τ ∈ Region) : ‖E₆ τ - E₆trunc τ‖ ≤ 123783 * ‖q τ‖ ^ 3 := by have heq : E₆ τ - E₆trunc τ = -(504 * eisensteinTail 5 3 τ) := by rw [E₆_eq_trunc τ]; ring rw [heq, norm_neg, norm_mul, Complex.norm_ofNat] - nlinarith [norm_eisensteinTail_sigma₅ hτ, norm_nonneg (eisensteinTail 5 3 τ)] + linarith only [norm_eisensteinTail_sigma₅ hτ, pow_nonneg (norm_nonneg (q τ)) 3] /-- `|δZ| = |E₂* - Z| ≤ 96.2·|q|³`. -/ lemma norm_sub_E₂starTrunc_le {τ : ℍ} (hτ : τ ∈ Region) : @@ -522,7 +523,7 @@ lemma norm_sub_E₂starTrunc_le {τ : ℍ} (hτ : τ ∈ Region) : have heq : E₂star τ - E₂starTrunc τ = -(24 * eisensteinTail 1 3 τ) := by rw [E₂star_eq_trunc τ]; ring rw [heq, norm_neg, norm_mul, Complex.norm_ofNat] - nlinarith [norm_eisensteinTail_sigma₁ hτ, norm_nonneg (eisensteinTail 1 3 τ)] + linarith only [norm_eisensteinTail_sigma₁ hτ, pow_nonneg (norm_nonneg (q τ)) 3] /-! ### Klein's `k` and its truncation `ktilde` (paper Lemma `lemk`) -/ diff --git a/LeanPool/Chudnovsky/Fourier.lean b/LeanPool/Chudnovsky/Fourier.lean index 27a1ac1adb..c7fdc7af5f 100644 --- a/LeanPool/Chudnovsky/Fourier.lean +++ b/LeanPool/Chudnovsky/Fourier.lean @@ -6,6 +6,7 @@ Authors: Xuanji Li module public import LeanPool.Chudnovsky.Lattices +import LeanPool.Chudnovsky.BernoulliValues import LeanPool.Chudnovsky.Liouville /-! @@ -75,7 +76,7 @@ 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 decide +kernel] at h + norm_num [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 diff --git a/LeanPool/Chudnovsky/Imports.lean b/LeanPool/Chudnovsky/Imports.lean index 2709d8d647..5c5c773e2d 100644 --- a/LeanPool/Chudnovsky/Imports.lean +++ b/LeanPool/Chudnovsky/Imports.lean @@ -8,6 +8,7 @@ module -- shake: keep-all --deprecated_module: ignore -- Generated project imports; run `lake exe mk_all`. public import LeanPool.Chudnovsky public import LeanPool.Chudnovsky.Basic +public import LeanPool.Chudnovsky.BernoulliValues public import LeanPool.Chudnovsky.Chudnovsky public import LeanPool.Chudnovsky.Clausen public import LeanPool.Chudnovsky.Coefficients @@ -20,6 +21,7 @@ public import LeanPool.Chudnovsky.Lattices public import LeanPool.Chudnovsky.Liouville public import LeanPool.Chudnovsky.MainTheorem public import LeanPool.Chudnovsky.Numerics +public import LeanPool.Chudnovsky.Periodicity public import LeanPool.Chudnovsky.PicardFuchs public import LeanPool.Chudnovsky.Quasiperiods public import LeanPool.Chudnovsky.Ramanujan diff --git a/LeanPool/Chudnovsky/Liouville.lean b/LeanPool/Chudnovsky/Liouville.lean index ff877306f8..ac244cd7f7 100644 --- a/LeanPool/Chudnovsky/Liouville.lean +++ b/LeanPool/Chudnovsky/Liouville.lean @@ -7,13 +7,7 @@ module public import Mathlib.Analysis.CStarAlgebra.Classes public import Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass -import Mathlib.Analysis.Complex.UpperHalfPlane.Basic import Mathlib.Analysis.Meromorphic.NormalForm -import Mathlib.Analysis.SpecialFunctions.Bernstein -import Mathlib.Analysis.SpecialFunctions.Gamma.Basic -import Mathlib.Combinatorics.Matroid.Init -import Mathlib.Data.Nat.Choose.Multinomial -import Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt /-! # Elliptic functions and the Liouville theorems @@ -31,8 +25,8 @@ Statements from chapter 1 of Milla (arXiv:1809.00533v6, file `060_ElliptFunct.te agree up to a nonzero constant factor. All statements in this file are fully proved (no `sorry`s). The second Liouville theorem is -proved via a self-contained parallelogram residue theorem built from Mathlib's rectangle -Cauchy--Goursat primitives. +proved via a self-contained parallelogram residue theorem using the fundamental theorem of +calculus and Fubini's theorem. -/ @[expose] public section @@ -207,7 +201,7 @@ lemma residue_logDeriv_eq_order {f : ℂ → ℂ} {c : ℂ} (hf : MeromorphicAt rw [hstep] have hmul : (fun z ↦ (z - c) ^ n • g z) = fun z ↦ (z - c) ^ n * g z := by ext z; rw [smul_eq_mul] - have hbase : DifferentiableAt ℂ (fun z : ℂ ↦ z - c) z := by fun_prop + have hbase : DifferentiableAt ℂ (fun z : ℂ ↦ z - c) z := differentiableAt_id.sub_const c have hmulLog : logDeriv (fun z ↦ (z - c) ^ n * g z) z = logDeriv (fun z ↦ (z - c) ^ n) z + logDeriv g z := logDeriv_mul (f := fun z ↦ (z - c) ^ n) (g := g) z (zpow_ne_zero n hzc') hgz @@ -407,6 +401,10 @@ private lemma mem_boundarySet_of_edge {L : PeriodPair} {v : ℂ} : fun t ht => Or.inl (Or.inr ⟨t, ht, rfl⟩), fun t ht => Or.inr ⟨t, ht, rfl⟩⟩ +private lemma continuous_edge (p ω : ℂ) : + Continuous (fun t : ℝ ↦ p + (t : ℂ) * ω) := + continuous_const.add (Complex.continuous_ofReal.mul continuous_const) + /-- **Loop integral of a derivative vanishes**: if `F` is a primitive of `f` on the boundary of the parallelogram, then the boundary integral of `f` is zero (fundamental theorem of calculus along each edge, then telescoping around the closed loop). -/ @@ -418,8 +416,7 @@ private lemma boundaryIntegral_eq_zero_of_primitive {L : PeriodPair} {f F : ℂ have hcont : ∀ (p ω : ℂ), (∀ t ∈ Set.Icc (0 : ℝ) 1, p + (t : ℂ) * ω ∈ L.boundarySet v) → ContinuousOn (fun t : ℝ ↦ f (p + (t : ℂ) * ω)) (Set.Icc 0 1) := by intro p ω hmem - apply hc.comp _ hmem - fun_prop + exact hc.comp (continuous_edge p ω).continuousOn hmem have E1 := integral_edge_eq_sub (fun t ht => hF _ (he₁ t ht)) (hcont _ _ he₁) have E2 := integral_edge_eq_sub (fun t ht => hF _ (he₂ t ht)) (hcont _ _ he₂) have E3 := integral_edge_eq_sub (fun t ht => hF _ (he₃ t ht)) (hcont _ _ he₃) @@ -479,12 +476,12 @@ private lemma boundaryIntegral_add {L : PeriodPair} {f g : ℂ → ℂ} {v : ℂ MeasureTheory.volume 0 1 := by apply ContinuousOn.intervalIntegrable rw [Set.uIcc_of_le zero_le_one] - exact (hf.comp (by fun_prop) hmem).mul continuousOn_const + exact (hf.comp (continuous_edge p ω).continuousOn hmem).mul continuousOn_const have hig : IntervalIntegrable (fun t : ℝ ↦ g (p + (t : ℂ) * ω) * ω) MeasureTheory.volume 0 1 := by apply ContinuousOn.intervalIntegrable rw [Set.uIcc_of_le zero_le_one] - exact (hg.comp (by fun_prop) hmem).mul continuousOn_const + exact (hg.comp (continuous_edge p ω).continuousOn hmem).mul continuousOn_const rw [← intervalIntegral.integral_add hif hig] apply intervalIntegral.integral_congr intro t _ @@ -722,7 +719,7 @@ private lemma edge_inv_im {c p ω : ℂ} (hne : ∀ t ∈ Set.Icc (0 : ℝ) 1, p * ∫ t in (0 : ℝ)..1, (Complex.normSq (p + (t : ℂ) * ω - c))⁻¹ := by have hcont : ContinuousOn (fun t : ℝ ↦ (p + (t : ℂ) * ω - c)⁻¹ * ω) (Set.Icc 0 1) := by apply ContinuousOn.mul _ continuousOn_const - exact ContinuousOn.inv₀ (by fun_prop) hne + exact ContinuousOn.inv₀ ((continuous_edge p ω).sub continuous_const).continuousOn hne have hint : IntervalIntegrable (fun t : ℝ ↦ (p + (t : ℂ) * ω - c)⁻¹ * ω) MeasureTheory.volume 0 1 := by apply ContinuousOn.intervalIntegrable @@ -790,7 +787,8 @@ private lemma boundaryIntegral_sub_inv_ne_zero {L : PeriodPair} {v c : ℂ} {a b apply intervalIntegral.intervalIntegral_pos_of_pos_on · apply ContinuousOn.intervalIntegrable rw [Set.uIcc_of_le zero_le_one] - apply ContinuousOn.inv₀ (by fun_prop) + apply ContinuousOn.inv₀ (Complex.continuous_normSq.comp + ((continuous_edge p ω).sub continuous_const)).continuousOn intro t ht exact Complex.normSq_pos.mpr (hne t ht) |>.ne' · intro t ht @@ -928,199 +926,107 @@ private lemma intervalIntegral_conj_comp {g gc : ℂ → ℂ} intervalIntegral.integral_congr (fun x _ => hgc (p x)) rw [hc, intervalIntegral_conj, h] +/-- Fubini's theorem for a continuous function on the closed unit square. -/ +private lemma integral_unitSquare_swap {d : ℝ × ℝ → ℂ} + (hd : ContinuousOn d (Set.Icc (0 : ℝ) 1 ×ˢ Set.Icc (0 : ℝ) 1)) : + (∫ s in (0 : ℝ)..1, ∫ t in (0 : ℝ)..1, d (s, t)) = + ∫ t in (0 : ℝ)..1, ∫ s in (0 : ℝ)..1, d (s, t) := by + simp only [intervalIntegral.integral_of_le zero_le_one] + apply MeasureTheory.integral_integral_swap + rw [MeasureTheory.Measure.prod_restrict, ← MeasureTheory.Measure.volume_eq_prod] + exact (hd.integrableOn_compact (isCompact_Icc.prod isCompact_Icc)).mono_set + (fun p hp => ⟨⟨hp.1.1.le, hp.1.2⟩, ⟨hp.2.1.le, hp.2.2⟩⟩) + /-- **Cauchy's theorem for a parallelogram.** If `f` is holomorphic on an open set containing the closed parallelogram, its boundary integral vanishes. -Mathlib only has the Cauchy–Goursat theorem for axis-parallel rectangles; we pull the -parallelogram back to the unit square along the real-affine map -`T u = v + u.re·ω₁ + u.im·ω₂` and apply Mathlib's *real* rectangle formula -(`Complex.integral_boundary_rect_of_hasFDerivAt_real_off_countable`, which computes the boundary -integral as the area integral of the `∂/∂zbar`-term) to both `f ∘ T` and `conj ∘ f ∘ T`. Since -`T` is not holomorphic the individual `∂/∂zbar`-terms do not vanish, but both are constant complex -multiples of the single area integral `M = ∫∫ f'(T u)`, and the parallelogram boundary integral -is the linear combination of the two identities in which `M` cancels. -/ +The fundamental theorem of calculus expresses the differences between opposite edge integrals +as iterated integrals of `f'`. Fubini identifies these area integrals, and their contributions +to the oriented boundary cancel. -/ private lemma boundaryIntegral_eq_zero_of_differentiableOn {L : PeriodPair} {f : ℂ → ℂ} {v : ℂ} {U : Set ℂ} (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) (hsub : ∀ s ∈ Set.Icc (0 : ℝ) 1, ∀ t ∈ Set.Icc (0 : ℝ) 1, v + (s : ℂ) * L.ω₁ + (t : ℂ) * L.ω₂ ∈ U) : L.boundaryIntegral f v = 0 := by - have hfa : AnalyticOnNhd ℂ f U := hf.analyticOnNhd hU - have hd_cont : ContinuousOn (deriv f) U := hfa.deriv.continuousOn - -- the affine pullback map and its (constant) real derivative - set Tlin : ℂ →L[ℝ] ℂ := Complex.reCLM.smulRight L.ω₁ + Complex.imCLM.smulRight L.ω₂ - with hTlin - have hTlin_apply : ∀ u : ℂ, Tlin u = (u.re : ℂ) * L.ω₁ + (u.im : ℂ) * L.ω₂ := by - intro u - simp [hTlin, Complex.real_smul] - set T : ℂ → ℂ := fun u ↦ v + (u.re : ℂ) * L.ω₁ + (u.im : ℂ) * L.ω₂ with hT - have hTcont : Continuous T := by fun_prop - have hTFDeriv : ∀ u : ℂ, HasFDerivAt T Tlin u := by - intro u - have heq : T = fun u ↦ v + Tlin u := by - funext w - rw [hTlin_apply] - simp [hT] - ring - rw [heq] - exact Tlin.hasFDerivAt.const_add v - set g : ℂ → ℂ := fun u ↦ f (T u) with hg - set d : ℂ → ℂ := fun u ↦ deriv f (T u) with hd - set g' : ℂ → ℂ →L[ℝ] ℂ := - fun u ↦ ((ContinuousLinearMap.toSpanSingleton ℂ (d u)).restrictScalars ℝ).comp Tlin with hg' - have hg'1 : ∀ u : ℂ, g' u 1 = L.ω₁ * d u := by - intro u - simp [hg', hTlin_apply, ContinuousLinearMap.toSpanSingleton_apply, smul_eq_mul, mul_comm] - have hg'I : ∀ u : ℂ, g' u Complex.I = L.ω₂ * d u := by - intro u - simp [hg', hTlin_apply, ContinuousLinearMap.toSpanSingleton_apply, smul_eq_mul, mul_comm] - -- membership of the closed square image - have hmemT : ∀ u : ℂ, u.re ∈ Set.Icc (0 : ℝ) 1 → u.im ∈ Set.Icc (0 : ℝ) 1 → T u ∈ U := - fun u h1 h2 => hsub u.re h1 u.im h2 - -- differentiability of the pullback - have hgFDeriv : ∀ u : ℂ, u.re ∈ Set.Icc (0 : ℝ) 1 → u.im ∈ Set.Icc (0 : ℝ) 1 → - HasFDerivAt g (g' u) u := by - intro u h1 h2 - have hmem : T u ∈ U := hmemT u h1 h2 - have hdf : HasDerivAt f (d u) (T u) := - (hf.differentiableAt (hU.mem_nhds hmem)).hasDerivAt - have hdF := (hdf.hasFDerivAt.restrictScalars ℝ).comp u (hTFDeriv u) - have hcomp : (f ∘ T) = g := rfl - rw [hcomp] at hdF - exact hdF - -- continuity of the pullback and of the area integrand - have hgc : ∀ u : ℂ, u.re ∈ Set.Icc (0 : ℝ) 1 → u.im ∈ Set.Icc (0 : ℝ) 1 → - ContinuousWithinAt g (Set.Icc (0:ℝ) 1 ×ℂ Set.Icc (0:ℝ) 1) u := by - intro u h1 h2 - have : ContinuousAt f (T u) := - (hfa (T u) (hmemT u h1 h2)).continuousAt - exact (this.comp hTcont.continuousAt).continuousWithinAt - -- endpoints of the unit square as a "rectangle" in Mathlib's sense - have hre0 : (0 : ℂ).re = 0 := rfl - have him0 : (0 : ℂ).im = 0 := rfl - have hre1 : (1 + Complex.I).re = 1 := by simp - have him1 : (1 + Complex.I).im = 1 := by simp - have hsq : Set.uIcc ((0 : ℂ).re) ((1 + Complex.I).re) ×ℂ - Set.uIcc ((0 : ℂ).im) ((1 + Complex.I).im) - = Set.Icc (0 : ℝ) 1 ×ℂ Set.Icc (0 : ℝ) 1 := by - rw [hre0, him0, hre1, him1, Set.uIcc_of_le zero_le_one] - have hIoo : Set.Ioo (min (0 : ℂ).re (1 + Complex.I).re) (max (0 : ℂ).re (1 + Complex.I).re) ×ℂ - Set.Ioo (min (0 : ℂ).im (1 + Complex.I).im) (max (0 : ℂ).im (1 + Complex.I).im) - = Set.Ioo (0 : ℝ) 1 ×ℂ Set.Ioo (0 : ℝ) 1 := by - rw [hre0, him0, hre1, him1, min_eq_left zero_le_one, max_eq_right zero_le_one] - -- hypotheses of the rectangle formula, for `g` - have Hc₁ : ContinuousOn g (Set.Icc (0 : ℝ) 1 ×ℂ Set.Icc (0 : ℝ) 1) := by - intro u hu - rw [Complex.mem_reProdIm] at hu - exact hgc u hu.1 hu.2 - have Hd₁ : ∀ u ∈ (Set.Ioo (0 : ℝ) 1 ×ℂ Set.Ioo (0 : ℝ) 1) \ (∅ : Set ℂ), - HasFDerivAt g (g' u) u := by - intro u hu - rw [Set.sdiff_empty, Complex.mem_reProdIm] at hu - exact hgFDeriv u (Set.mem_Icc_of_Ioo hu.1) (Set.mem_Icc_of_Ioo hu.2) - have hd_contSq : ContinuousOn d (Set.Icc (0 : ℝ) 1 ×ℂ Set.Icc (0 : ℝ) 1) := by - intro u hu - rw [Complex.mem_reProdIm] at hu - exact ((hd_cont (T u) (hmemT u hu.1 hu.2)).continuousAt - (hU.mem_nhds (hmemT u hu.1 hu.2))).comp hTcont.continuousAt |>.continuousWithinAt - have Hi₁ : MeasureTheory.IntegrableOn (fun u ↦ Complex.I • g' u 1 - g' u Complex.I) - (Set.Icc (0 : ℝ) 1 ×ℂ Set.Icc (0 : ℝ) 1) := - integrableOn_diff_apply hg'1 hg'I hd_contSq - -- hypotheses for the conjugated pullback - set gc : ℂ → ℂ := fun u ↦ (starRingEnd ℂ) (g u) with hgcdef - set gc' : ℂ → ℂ →L[ℝ] ℂ := - fun u ↦ (Complex.conjCLE.toContinuousLinearMap).comp (g' u) with hgc' - have hgc'1 : ∀ u : ℂ, gc' u 1 = (starRingEnd ℂ) (L.ω₁ * d u) := by - intro u - simp [hgc', hg'1] - have hgc'I : ∀ u : ℂ, gc' u Complex.I = (starRingEnd ℂ) (L.ω₂ * d u) := by - intro u - simp [hgc', hg'I] - have Hc₂ : ContinuousOn gc (Set.Icc (0 : ℝ) 1 ×ℂ Set.Icc (0 : ℝ) 1) := - Complex.continuous_conj.comp_continuousOn Hc₁ - have Hd₂ : ∀ u ∈ (Set.Ioo (0 : ℝ) 1 ×ℂ Set.Ioo (0 : ℝ) 1) \ (∅ : Set ℂ), - HasFDerivAt gc (gc' u) u := by - intro u hu - exact (Complex.conjCLE.toContinuousLinearMap.hasFDerivAt).comp u (Hd₁ u hu) - have Hi₂ : MeasureTheory.IntegrableOn (fun u ↦ Complex.I • gc' u 1 - gc' u Complex.I) - (Set.Icc (0 : ℝ) 1 ×ℂ Set.Icc (0 : ℝ) 1) := - integrableOn_diff_apply (c₁ := (starRingEnd ℂ) L.ω₁) (c₂ := (starRingEnd ℂ) L.ω₂) - (d := fun u ↦ (starRingEnd ℂ) (d u)) - (fun u => by rw [hgc'1]; exact map_mul _ _ _) - (fun u => by rw [hgc'I]; exact map_mul _ _ _) - (Complex.continuous_conj.comp_continuousOn hd_contSq) - -- the two rectangle identities - have Heq₁ := Complex.integral_boundary_rect_of_hasFDerivAt_real_off_countable g g' - 0 (1 + Complex.I) ∅ Set.countable_empty - (by rw [hsq]; exact Hc₁) (by rw [hIoo]; exact Hd₁) (by rw [hsq]; exact Hi₁) - have Heq₂ := Complex.integral_boundary_rect_of_hasFDerivAt_real_off_countable gc gc' - 0 (1 + Complex.I) ∅ Set.countable_empty - (by rw [hsq]; exact Hc₂) (by rw [hIoo]; exact Hd₂) (by rw [hsq]; exact Hi₂) - simp only [hre0, him0, hre1, him1, Complex.ofReal_zero, Complex.ofReal_one, zero_mul, - one_mul, add_zero, zero_add, smul_eq_mul] at Heq₁ Heq₂ - -- convert the pullback edge integrals to parallelogram edge integrals - set M : ℂ := ∫ x in (0 : ℝ)..1, ∫ y in (0 : ℝ)..1, d (↑x + ↑y * Complex.I) with hM - have hsimp : ∀ (x : ℝ) (w : ℂ), g (↑x + w) = f (v + (↑x + w.re) * L.ω₁ + ↑w.im * L.ω₂) := by - intro x w - simp [hg, hT] - have hB : (∫ x in (0 : ℝ)..1, g ↑x) = ∫ t in (0 : ℝ)..1, f (v + ↑t * L.ω₁) := by - apply intervalIntegral.integral_congr - intro t _ - change g ↑t = f (v + ↑t * L.ω₁) - simp [hg, hT] - have hTop : (∫ x in (0 : ℝ)..1, g (↑x + Complex.I)) - = ∫ t in (0 : ℝ)..1, f (v + L.ω₂ + ↑t * L.ω₁) := by - apply intervalIntegral.integral_congr - intro t _ - change g (↑t + Complex.I) = f (v + L.ω₂ + ↑t * L.ω₁) - simp [hg, hT] - congr 1 - ring - have hR : (∫ y in (0 : ℝ)..1, g (1 + ↑y * Complex.I)) - = ∫ t in (0 : ℝ)..1, f (v + L.ω₁ + ↑t * L.ω₂) := by - apply intervalIntegral.integral_congr - intro t _ - change g (1 + ↑t * Complex.I) = f (v + L.ω₁ + ↑t * L.ω₂) - simp [hg, hT] - have hL : (∫ y in (0 : ℝ)..1, g (↑y * Complex.I)) - = ∫ t in (0 : ℝ)..1, f (v + ↑t * L.ω₂) := by + have hd : ContinuousOn (deriv f) U := (hf.analyticOnNhd hU).deriv.continuousOn + let D (s t : ℝ) := deriv f (v + (s : ℂ) * L.ω₁ + (t : ℂ) * L.ω₂) + have rows (g : ℂ → ℂ) (hg : ContinuousOn g U) (t : ℝ) (ht : t ∈ Set.Icc (0 : ℝ) 1) : + ContinuousOn (fun s : ℝ => g (v + (s : ℂ) * L.ω₁ + (t : ℂ) * L.ω₂)) + (Set.Icc (0 : ℝ) 1) := + hg.comp ((PeriodPair.continuous_edge v L.ω₁).add continuous_const).continuousOn + (fun s hs => hsub s hs t ht) + have columns (g : ℂ → ℂ) (hg : ContinuousOn g U) (s : ℝ) + (hs : s ∈ Set.Icc (0 : ℝ) 1) : + ContinuousOn (fun t : ℝ => g (v + (s : ℂ) * L.ω₁ + (t : ℂ) * L.ω₂)) + (Set.Icc (0 : ℝ) 1) := + hg.comp (PeriodPair.continuous_edge (v + (s : ℂ) * L.ω₁) L.ω₂).continuousOn + (fun t ht => hsub s hs t ht) + have hD : ContinuousOn (fun p : ℝ × ℝ => D p.1 p.2) + (Set.Icc (0 : ℝ) 1 ×ˢ Set.Icc (0 : ℝ) 1) := + hd.comp ((continuous_const.add + ((Complex.continuous_ofReal.comp continuous_fst).mul continuous_const)).add + ((Complex.continuous_ofReal.comp continuous_snd).mul continuous_const)).continuousOn + (fun p hp => hsub p.1 hp.1 p.2 hp.2) + have rowIntegrable (t : ℝ) (ht : t ∈ Set.Icc (0 : ℝ) 1) : + IntervalIntegrable (fun s : ℝ => f (v + (s : ℂ) * L.ω₁ + (t : ℂ) * L.ω₂)) + MeasureTheory.volume 0 1 := by + apply ContinuousOn.intervalIntegrable + rw [Set.uIcc_of_le zero_le_one] + exact rows f hf.continuousOn t ht + have columnIntegrable (s : ℝ) (hs : s ∈ Set.Icc (0 : ℝ) 1) : + IntervalIntegrable (fun t : ℝ => f (v + (s : ℂ) * L.ω₁ + (t : ℂ) * L.ω₂)) + MeasureTheory.volume 0 1 := by + apply ContinuousOn.intervalIntegrable + rw [Set.uIcc_of_le zero_le_one] + exact columns f hf.continuousOn s hs + have h0 : (0 : ℝ) ∈ Set.Icc (0 : ℝ) 1 := ⟨le_rfl, zero_le_one⟩ + have h1 : (1 : ℝ) ∈ Set.Icc (0 : ℝ) 1 := ⟨zero_le_one, le_rfl⟩ + have hr0 := rowIntegrable 0 h0 + have hr1 := rowIntegrable 1 h1 + have hc0 := columnIntegrable 0 h0 + have hc1 := columnIntegrable 1 h1 + simp only [Complex.ofReal_zero, Complex.ofReal_one, zero_mul, one_mul, add_zero] + at hr0 hr1 hc0 hc1 + have vertical : ((∫ s in (0 : ℝ)..1, f (v + (s : ℂ) * L.ω₁ + L.ω₂)) + - (∫ s in (0 : ℝ)..1, f (v + (s : ℂ) * L.ω₁))) = + (∫ s in (0 : ℝ)..1, ∫ t in (0 : ℝ)..1, D s t) * L.ω₂ := by + rw [← intervalIntegral.integral_sub hr1 hr0] + calc + _ = ∫ s in (0 : ℝ)..1, ∫ t in (0 : ℝ)..1, D s t * L.ω₂ := by + apply intervalIntegral.integral_congr + intro s hs + rw [Set.uIcc_of_le zero_le_one] at hs + exact (PeriodPair.integral_edge_eq_sub + (fun t ht => (hf.differentiableAt (hU.mem_nhds (hsub s hs t ht))).hasDerivAt) + (columns (deriv f) hd s hs)).symm + _ = _ := by simp only [intervalIntegral.integral_mul_const] + have horizontal : ((∫ t in (0 : ℝ)..1, f (v + L.ω₁ + (t : ℂ) * L.ω₂)) + - (∫ t in (0 : ℝ)..1, f (v + (t : ℂ) * L.ω₂))) = + (∫ s in (0 : ℝ)..1, ∫ t in (0 : ℝ)..1, D s t) * L.ω₁ := by + rw [← intervalIntegral.integral_sub hc1 hc0] + calc + _ = ∫ t in (0 : ℝ)..1, ∫ s in (0 : ℝ)..1, D s t * L.ω₁ := by + apply intervalIntegral.integral_congr + intro t ht + rw [Set.uIcc_of_le zero_le_one] at ht + have edge := PeriodPair.integral_edge_eq_sub (p := v + (t : ℂ) * L.ω₂) (ω := L.ω₁) + (fun s hs => (hf.differentiableAt (hU.mem_nhds (by + simpa only [add_right_comm v] using hsub s hs t ht))).hasDerivAt) + (by simpa only [add_right_comm v] using rows (deriv f) hd t ht) + simpa only [D, add_right_comm v] using edge.symm + _ = (∫ t in (0 : ℝ)..1, ∫ s in (0 : ℝ)..1, D s t) * L.ω₁ := by + simp only [intervalIntegral.integral_mul_const] + _ = _ := by rw [← integral_unitSquare_swap hD] + have top : (∫ s in (0 : ℝ)..1, f (v + L.ω₂ + (s : ℂ) * L.ω₁)) = + ∫ s in (0 : ℝ)..1, f (v + (s : ℂ) * L.ω₁ + L.ω₂) := by apply intervalIntegral.integral_congr - intro t _ - change g (↑t * Complex.I) = f (v + ↑t * L.ω₂) - simp [hg, hT] - have hRHS₁ : (∫ x in (0 : ℝ)..1, ∫ y in (0 : ℝ)..1, - Complex.I * g' (↑x + ↑y * Complex.I) 1 - g' (↑x + ↑y * Complex.I) Complex.I) - = (Complex.I * L.ω₁ - L.ω₂) * M := by - rw [hM]; exact double_integral_diff_apply hg'1 hg'I - have hRHS₂ : (∫ x in (0 : ℝ)..1, ∫ y in (0 : ℝ)..1, - Complex.I * gc' (↑x + ↑y * Complex.I) 1 - gc' (↑x + ↑y * Complex.I) Complex.I) - = (starRingEnd ℂ) ((-(Complex.I * L.ω₁) - L.ω₂) * M) := - double_integral_conj_apply hM hgc'1 hgc'I - -- conjugated edge conversions - have hgcpt : ∀ z, gc z = (starRingEnd ℂ) (g z) := fun z => congrFun hgcdef z - have hBc : (∫ x in (0 : ℝ)..1, gc ↑x) - = (starRingEnd ℂ) (∫ t in (0 : ℝ)..1, f (v + ↑t * L.ω₁)) := - intervalIntegral_conj_comp hgcpt hB - have hTopc : (∫ x in (0 : ℝ)..1, gc (↑x + Complex.I)) - = (starRingEnd ℂ) (∫ t in (0 : ℝ)..1, f (v + L.ω₂ + ↑t * L.ω₁)) := - intervalIntegral_conj_comp hgcpt hTop - have hRc : (∫ y in (0 : ℝ)..1, gc (1 + ↑y * Complex.I)) - = (starRingEnd ℂ) (∫ t in (0 : ℝ)..1, f (v + L.ω₁ + ↑t * L.ω₂)) := - intervalIntegral_conj_comp hgcpt hR - have hLc : (∫ y in (0 : ℝ)..1, gc (↑y * Complex.I)) - = (starRingEnd ℂ) (∫ t in (0 : ℝ)..1, f (v + ↑t * L.ω₂)) := - intervalIntegral_conj_comp hgcpt hL - rw [hB, hTop, hR, hL, hRHS₁] at Heq₁ - rw [hBc, hTopc, hRc, hLc, hRHS₂] at Heq₂ - have Heq₂' := congrArg (starRingEnd ℂ) Heq₂ - simp only [map_sub, map_add, map_mul, Complex.conj_conj, Complex.conj_I] at Heq₂' - -- assemble the boundary integral and eliminate the area term - rw [boundaryIntegral, intervalIntegral.integral_mul_const, intervalIntegral.integral_mul_const, - intervalIntegral.integral_mul_const, intervalIntegral.integral_mul_const] - linear_combination ((L.ω₁ - Complex.I * L.ω₂) / 2) * Heq₁ - + ((L.ω₁ + Complex.I * L.ω₂) / 2) * Heq₂' - + ((∫ t in (0 : ℝ)..1, f (v + L.ω₁ + ↑t * L.ω₂)) * L.ω₂ - - (∫ t in (0 : ℝ)..1, f (v + ↑t * L.ω₂)) * L.ω₂ - - L.ω₁ * L.ω₂ * M) * Complex.I_mul_I + intro s _ + exact congrArg f (add_right_comm v L.ω₂ ((s : ℂ) * L.ω₁)) + rw [PeriodPair.boundaryIntegral, intervalIntegral.integral_mul_const, + intervalIntegral.integral_mul_const, intervalIntegral.integral_mul_const, + intervalIntegral.integral_mul_const, top] + linear_combination -L.ω₁ * vertical + L.ω₂ * horizontal + /-- `dslope` of a function analytic at a point is analytic there. -/ private lemma analyticAt_dslope_self {g : ℂ → ℂ} {c : ℂ} (hg : AnalyticAt ℂ g c) : @@ -1301,7 +1207,7 @@ private lemma analyticAt_sub_zpow (c : ℂ) (n : ℤ) {z : ℂ} (hzc : z ≠ c) have hd : DifferentiableOn ℂ (fun w ↦ (w - c) ^ n) {c}ᶜ := by intro w hw apply DifferentiableAt.differentiableWithinAt - have hbase : DifferentiableAt ℂ (fun w : ℂ ↦ w - c) w := by fun_prop + have hbase : DifferentiableAt ℂ (fun w : ℂ ↦ w - c) w := differentiableAt_id.sub_const c exact hbase.zpow (Or.inl (sub_ne_zero.2 (by simpa using hw))) exact hd.analyticOnNhd isOpen_compl_singleton z (by simpa using hzc) @@ -1311,7 +1217,7 @@ private lemma analyticAt_sub_inv (c : ℂ) {z : ℂ} (hzc : z ≠ c) : have hd : DifferentiableOn ℂ (fun w ↦ (w - c)⁻¹) {c}ᶜ := by intro w hw apply DifferentiableAt.differentiableWithinAt - have hbase : DifferentiableAt ℂ (fun w : ℂ ↦ w - c) w := by fun_prop + have hbase : DifferentiableAt ℂ (fun w : ℂ ↦ w - c) w := differentiableAt_id.sub_const c exact hbase.inv (sub_ne_zero.2 (by simpa using hw)) exact hd.analyticOnNhd isOpen_compl_singleton z (by simpa using hzc) diff --git a/LeanPool/Chudnovsky/Periodicity.lean b/LeanPool/Chudnovsky/Periodicity.lean new file mode 100644 index 0000000000..604b0f2f50 --- /dev/null +++ b/LeanPool/Chudnovsky/Periodicity.lean @@ -0,0 +1,38 @@ +/- +Copyright (c) 2026 Xuanji Li. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Xuanji Li +-/ +module + +public import Mathlib.Analysis.Complex.UpperHalfPlane.Topology + +/-! +# Periodicity after extension from the upper half-plane + +This elementary bridge is shared by the modular-function and derivative developments. +Keeping it separate lets the modular-function modules build without the derivative theory. +-/ + +@[expose] public section + +namespace Chudnovsky + +open UpperHalfPlane Complex Function + +/-- A `1`-translation-invariant function on `ℍ` extends to a `1`-periodic function on `ℂ`. -/ +lemma periodic_comp_ofComplex_of_vadd {f : ℍ → ℂ} (hf : ∀ τ : ℍ, f ((1 : ℝ) +ᵥ τ) = 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 + 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 [comp_apply] + rw [ofComplex_apply_eq_of_im_nonpos hw1 (by simpa using hw)] + +end Chudnovsky diff --git a/LeanPool/Chudnovsky/PicardFuchs.lean b/LeanPool/Chudnovsky/PicardFuchs.lean index e64a73e59e..d02ddf64bf 100644 --- a/LeanPool/Chudnovsky/PicardFuchs.lean +++ b/LeanPool/Chudnovsky/PicardFuchs.lean @@ -7,12 +7,7 @@ module public import Mathlib.Analysis.CStarAlgebra.Classes public import Mathlib.Analysis.Calculus.Deriv.Basic -import Mathlib.Analysis.Complex.UpperHalfPlane.Basic -import Mathlib.Analysis.SpecialFunctions.Bernstein -import Mathlib.Analysis.SpecialFunctions.Gamma.Basic -import Mathlib.Combinatorics.Matroid.Init -import Mathlib.Data.Nat.Choose.Multinomial -import Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt +import Mathlib.Analysis.Complex.UpperHalfPlane.Basic -- shake: keep /-! # The Picard–Fuchs differential equation diff --git a/LeanPool/Chudnovsky/Ramanujan.lean b/LeanPool/Chudnovsky/Ramanujan.lean index 3811caaf4e..8858eee587 100644 --- a/LeanPool/Chudnovsky/Ramanujan.lean +++ b/LeanPool/Chudnovsky/Ramanujan.lean @@ -6,6 +6,7 @@ Authors: Xuanji Li module public import LeanPool.Chudnovsky.Basic +public import LeanPool.Chudnovsky.Periodicity public import Mathlib.NumberTheory.ModularForms.Derivative import Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula @@ -70,21 +71,6 @@ lemma deriv_eqOn_upperHalfPlaneSet {F G : ℂ → ℂ} (h : Set.EqOn F G upperHa {z : ℂ} (hz : 0 < z.im) : deriv F z = deriv G z := (Filter.eventuallyEq_of_mem (isOpen_upperHalfPlaneSet.mem_nhds hz) h).deriv_eq -/-- A `1`-translation-invariant function on `ℍ` extends to a `1`-periodic function on `ℂ`. -/ -lemma periodic_comp_ofComplex_of_vadd {f : ℍ → ℂ} (hf : ∀ τ : ℍ, f ((1 : ℝ) +ᵥ τ) = 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 - 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 [comp_apply] - rw [ofComplex_apply_eq_of_im_nonpos hw1 (by simpa using hw)] - /-! ### Transformation behaviour of `E₂` and of level-one modular forms under `T` and `S` -/ lemma E2_slash_T : E2 ∣[(2 : ℤ)] ModularGroup.T = E2 := by diff --git a/LeanPool/Chudnovsky/SigmaZeta.lean b/LeanPool/Chudnovsky/SigmaZeta.lean index b8a8726cb5..6c10326c7d 100644 --- a/LeanPool/Chudnovsky/SigmaZeta.lean +++ b/LeanPool/Chudnovsky/SigmaZeta.lean @@ -9,13 +9,7 @@ public import Mathlib.Analysis.CStarAlgebra.Classes public import Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass import Mathlib.Analysis.Calculus.LogDerivUniformlyOn import Mathlib.Analysis.Complex.SummableUniformlyOn -import Mathlib.Analysis.Complex.UpperHalfPlane.Basic import Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn -import Mathlib.Analysis.SpecialFunctions.Bernstein -import Mathlib.Analysis.SpecialFunctions.Gamma.Basic -import Mathlib.Combinatorics.Matroid.Init -import Mathlib.Data.Nat.Choose.Multinomial -import Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt /-! # The Weierstrass σ- and ζ-functions diff --git a/LeanPool/Chudnovsky/SingularModuli/FormReduction.lean b/LeanPool/Chudnovsky/SingularModuli/FormReduction.lean index 46d996acde..94e7f848ec 100644 --- a/LeanPool/Chudnovsky/SingularModuli/FormReduction.lean +++ b/LeanPool/Chudnovsky/SingularModuli/FormReduction.lean @@ -56,7 +56,9 @@ theorem Equiv.trans {f g h : BQF} (hfg : Equiv f g) (hgh : Equiv g h) : Equiv f obtain ⟨p', q', r', s', hdet', rfl⟩ := hgh refine ⟨p * p' + q * r', p * q' + q * s', r * p' + s * r', r * q' + s * s', ?_, (act_act f p q r s p' q' r' s').symm⟩ - nlinarith [hdet, hdet'] + calc + _ = (p * s - q * r) * (p' * s' - q' * r') := by ring + _ = 1 := by rw [hdet, hdet', one_mul] /-- The `T`-generator: shift `(a, b, c) ↦ (a, b + 2an, a n² + b n + c)`; preserves the form class and (obviously) the discriminant. -/ @@ -196,6 +198,25 @@ private lemma reprN_eq_reprB (m d : ℕ) : reprN m d = reprB m d := by · rintro ⟨t, ht, h2, l, ⟨hl1, hl9⟩, h1⟩ exact ⟨t, ht, l, ⟨hl1, by omega⟩, h1, h2⟩ +/-- The Boolean sieve for the three-prime test retains only `163`. -/ +private lemma three_prime_candidates : + (List.range 245).filter (fun d => reprB 41 d && reprB 43 d && reprB 61 d) = [163] := by + decide +kernel + +/-- Membership in the Boolean sieve gives the bounded discriminant test. -/ +private lemma three_prime_bound : + ∀ d < 245, reprB 41 d = true → reprB 43 d = true → reprB 61 d = true → d = 163 := by + intro d hd h41 h43 h61 + have hmem : d ∈ (List.range 245).filter + (fun d => reprB 41 d && reprB 43 d && reprB 61 d) := + List.mem_filter.mpr ⟨List.mem_range.mpr hd, by simp only [h41, h43, h61, Bool.and_self]⟩ + simpa only [three_prime_candidates, List.mem_singleton] using hmem + +-- Keep the original decision bridge and its generated declarations while reusing the sieve proof. +private local instance three_prime_decidable : Decidable + (∀ d < 245, reprB 41 d = true → reprB 43 d = true → reprB 61 d = true → d = 163) := + isTrue three_prime_bound + /-- **(C5), computational core.** The only `d ∈ [1, 244]` simultaneously representable at `m = 41, 43, 61` is `d = 163` (i.e. `D₀ = −163`). The `{41,43,47}` trap of §6.6 is exactly that `d = 43` would also survive there; here it does not. Decided by the kernel on the diff --git a/LeanPool/Chudnovsky/SingularModuli/JFunction.lean b/LeanPool/Chudnovsky/SingularModuli/JFunction.lean index 17f083616d..09fc5a2c21 100644 --- a/LeanPool/Chudnovsky/SingularModuli/JFunction.lean +++ b/LeanPool/Chudnovsky/SingularModuli/JFunction.lean @@ -6,7 +6,8 @@ Authors: Xuanji Li module public import LeanPool.Chudnovsky.Basic -import LeanPool.Chudnovsky.Ramanujan +import LeanPool.Chudnovsky.BernoulliValues +import LeanPool.Chudnovsky.Periodicity import Mathlib.Geometry.Manifold.MFDeriv.NormedSpace /-! @@ -138,7 +139,7 @@ coefficients. These feed the ℤ-refinement `ModularPolynomialZ.lean` downstream 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 hb : bernoulli 4 = -1 / 30 := by rw [bernoulli, bernoulli'_four]; norm_num + 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⟩ @@ -196,24 +197,15 @@ private lemma coeff_E6Z (n : ℕ) : split <;> ring /-- The Bernoulli number `B₆ = 1/42` (not in Mathlib as a literal). -/ -private lemma bernoulli_six : bernoulli 6 = 1 / 42 := by - have h5 : bernoulli' 5 = 0 := bernoulli'_eq_zero_of_odd ⟨2, rfl⟩ (by norm_num) - 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] - rw [bernoulli, h6] - norm_num +private lemma bernoulli_six : bernoulli 6 = 1 / 42 := + bernoulli_six_value /-- Analytic identification: Mathlib's q-expansion of `E₄` is the formal series `E4Z`. -/ private lemma qExpansion_E₄_eq : qExpansion 1 ⇑E₄ = PowerSeries.map (Int.castRingHom ℂ) E4Z := by ext n have h := EisensteinSeries.E_qExpansion_coeff (k := 4) (by norm_num) (by decide) n - have hb : bernoulli 4 = -1 / 30 := by rw [bernoulli, bernoulli'_four]; norm_num + have hb : bernoulli 4 = -1 / 30 := bernoulli_four_value rw [hb, show (4 : ℕ) - 1 = 3 from rfl] at h rw [PowerSeries.coeff_map, coeff_E4Z, h] split_ifs diff --git a/LeanPool/Chudnovsky/SingularModuli/Kronecker.lean b/LeanPool/Chudnovsky/SingularModuli/Kronecker.lean index 548b17a931..0f2260eb38 100644 --- a/LeanPool/Chudnovsky/SingularModuli/Kronecker.lean +++ b/LeanPool/Chudnovsky/SingularModuli/Kronecker.lean @@ -6,7 +6,7 @@ Authors: Xuanji Li module public import LeanPool.Chudnovsky.SingularModuli.ModularPolynomialZ -import LeanPool.Chudnovsky.Ramanujan +import LeanPool.Chudnovsky.Periodicity /-! # Kronecker's unit-leading-coefficient lemma for the diagonal modular polynomial (Phase C, B7) diff --git a/LeanPool/Chudnovsky/SingularModuli/ModularPolynomialQ.lean b/LeanPool/Chudnovsky/SingularModuli/ModularPolynomialQ.lean index 1ed5bc48ad..73bb315e13 100644 --- a/LeanPool/Chudnovsky/SingularModuli/ModularPolynomialQ.lean +++ b/LeanPool/Chudnovsky/SingularModuli/ModularPolynomialQ.lean @@ -6,7 +6,7 @@ Authors: Xuanji Li module public import LeanPool.Chudnovsky.SingularModuli.CosetOrbit -import LeanPool.Chudnovsky.Ramanujan +import LeanPool.Chudnovsky.Periodicity import Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities /-! diff --git a/LeanPool/Chudnovsky/SingularModuli/ModularPolynomialZ.lean b/LeanPool/Chudnovsky/SingularModuli/ModularPolynomialZ.lean index 4130a59f26..42f0e178c4 100644 --- a/LeanPool/Chudnovsky/SingularModuli/ModularPolynomialZ.lean +++ b/LeanPool/Chudnovsky/SingularModuli/ModularPolynomialZ.lean @@ -6,7 +6,7 @@ Authors: Xuanji Li module public import LeanPool.Chudnovsky.SingularModuli.ModularPolynomialQ -import LeanPool.Chudnovsky.Ramanujan +import LeanPool.Chudnovsky.Periodicity import Mathlib.Algebra.GCDMonoid.IntegrallyClosed import Mathlib.Geometry.Manifold.MFDeriv.NormedSpace diff --git a/LeanPool/Chudnovsky/WeierstrassMore.lean b/LeanPool/Chudnovsky/WeierstrassMore.lean index 7017b10afc..12e7b92aa2 100644 --- a/LeanPool/Chudnovsky/WeierstrassMore.lean +++ b/LeanPool/Chudnovsky/WeierstrassMore.lean @@ -6,12 +6,6 @@ Authors: Xuanji Li module public import LeanPool.Chudnovsky.Liouville -import Mathlib.Analysis.Complex.UpperHalfPlane.Basic -import Mathlib.Analysis.SpecialFunctions.Bernstein -import Mathlib.Analysis.SpecialFunctions.Gamma.Basic -import Mathlib.Combinatorics.Matroid.Init -import Mathlib.Data.Nat.Choose.Multinomial -import Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt /-! # The zeros of ℘′ and the factorization of ℘′²