← Session 21 — Tier ii′ planning + launch: close SfBoundProp in Lean (D-064)
thinking (9154 chars)
`mul_geom_sum (x : R) (n : ℕ) : (x - 1) * ∑ i ∈ range n, x ^ i = x ^ n - 1` — exactly the direction I wanted.
Now for the star/conj bridge: `star (z : ℂ)` vs `conj z`. conj IS `starRingEnd ℂ` (defined that way), and `star` on ℂ goes through the StarMul instance whose star function is conj. So `star z` should be defeq to `conj z`. In proofs, use `star_div₀`-style lemmas for the star manipulation, then convert to conj by `show` (defeq) or `Complex.star_def` if it exists. Let me test defeq conversion via `show` — I'll write the code and iterate.
Let me now rewrite Scratch.lean with all fixes:
1. summand_star: use star_sub, star_one, star_pow, star_div₀.
2. liSummand_eq: convert star to conj (defeq — try `show ... conj ...` or simp [star] — hmm; the term in liSummand's def uses `star (ρ:ℂ)`. After summand_star rewrites `1 - (1 - 1/(star z))^n` to `star (1 - (1 - 1/z)^n)`, the goal has `star (1 - ...)`; then `Complex.re_eq_add_conj : (z.re : ℂ) = (z + conj z)/2` — rewrite RHS: goal: (mult/2)·(f + star f) = mult·(re f : ℂ). If star f is defeq conj f, `show (zeroMult : ℂ)/2 * (f + conj f) = _` might work directly since star and conj are defeq. Let me structure:
```
lemma liSummand_eq ... := by
rw [liSummand, summand_star]
have h : (1 - (1 - 1 / (ρ:ℂ)) ^ n) + star (1 - (1 - 1 / (ρ:ℂ)) ^ n)
= 2 * (((1 - (1 - 1 / (ρ:ℂ)) ^ n).re) : ℂ) := by
rw [Complex.add_conj] -- if star ≟ conj defeq, this rw works? add_conj is about conj
```
Hmm — Complex.add_conj's LHS is `z + conj z`; our term is `f + star f`. rw with add_conj: pattern `?z + conj ?z` — `conj ?z` is `(starRingEnd ℂ) ?z` — the term `star f` where star = Star.star — different head constants (Star.star vs starRingEnd application). rw may fail. Solution: change liSummand's def to use `conj` instead of `star`:
`(zeroMult ρ : ℂ) / 2 * ((1 - (1 - 1/(ρ:ℂ))^n) + (1 - (1 - 1/(conj (ρ:ℂ)))^n))`
conj = starRingEnd ℂ — map_ lemmas apply directly (map_sub, map_one, map_pow, map_div₀). And Complex.add_conj matches.
So summand_conj:
```
lemma summand_conj (n : ℕ) (z : ℂ) :
(1 : ℂ) - (1 - 1 / (conj z)) ^ n = conj ((1 - (1 - 1 / z) ^ n)) := by
rw [map_sub, map_one, map_pow, map_sub, map_one, map_div₀, map_one]
```
conj z = (starRingEnd ℂ) z — map_sub etc. should match with ?f := starRingEnd ℂ ✓ (this failed for star but should work for conj since conj IS the bundled hom).
Hmm wait — conj (1/z): map_div₀ (starRingEnd ℂ) 1 z = conj 1 / conj z ✓ = 1/conj z after map_one.
3. pow_one_add_inv_two_mul_le — rewrite cleanly:
```
lemma pow_one_add_inv_two_mul_le (n : ℕ) (hn : 1 ≤ n) :
((1 : ℝ) + 1 / (2 * n)) ^ n ≤ 2 := by
have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
have h1 : ((1 : ℝ) + 1 / (2 * n)) ^ n ≤ Real.exp (1 / 2) := by
have hbase : (1 : ℝ) + 1 / (2 * n) ≤ Real.exp (1 / (2 * n)) :=
Real.add_one_le_exp _
calc ((1 : ℝ) + 1 / (2 * n)) ^ n
≤ (Real.exp (1 / (2 * n))) ^ n := by
apply pow_le_pow_left₀ (by positivity) hbase
_ = Real.exp (↑n * (1 / (2 * n))) := by
rw [Real.exp_nat_mul]
_ = Real.exp (1 / 2) := by
congr 1; field_simp
have h2 : Real.exp (1 / 2 : ℝ) ≤ 2 := by
have h3 : Real.log 2 ≥ 1 / 2 := by
have h := Real.log_two_gt_d9
linarith [h]
calc Real.exp (1 / 2 : ℝ) ≤ Real.exp (Real.log 2) := Real.exp_le_exp.mpr h3
_ = 2 := Real.exp_log (by norm_num)
exact h1.trans h2
```
pow_le_pow_left₀ signature: `pow_le_pow_left₀ (ha : 0 ≤ a) (hab : a ≤ b) (n : ℕ) : a^n ≤ b^n`? I believe `pow_le_pow_left₀ (ha : 0 ≤ a) (hab : a ≤ b) (n : ℕ) : a ^ n ≤ b ^ n` ✓.
Real.exp_nat_mul : `Real.exp_nat_mul (x : ℝ) (n : ℕ) : Real.exp (n * x) = (Real.exp x) ^ n` — so `rw [Real.exp_nat_mul]` on goal `(exp x)^n = exp(n*x)`?? My calc step is `_ = Real.exp (↑n * (1/(2*n)))` — I'm proving `(Real.exp (1/(2n)))^n = Real.exp (↑n * (1/(2*n)))` — that's `Real.exp_nat_mul` REVERSED: `(exp x)^n = exp (n*x)` — so the proof is `rw [Real.exp_nat_mul]` — rewrites RHS `exp (↑n * x)` to `(exp x)^n` making both sides equal ✓. Hmm, wait: exp_nat_mul states exp (n*x) = (exp x)^n; rw [Real.exp_nat_mul] rewrites instances of `exp (n * x)` → `(exp x)^n`. Goal: `(exp x)^n = exp (↑n * x)` → after rw: `(exp x)^n = (exp x)^n` ✓ closed by rfl automatically (rw closes goals that become rfl). But careful: the cast ↑n vs n in exp_nat_mul — exp_nat_mul has (n : ℕ) and the term is `↑n * x` where ↑ is Nat→ℝ cast ✓ matches.
`Real.log_two_gt_d9 : 0.6931471803 < Real.log 2` ✓ exists (used in D-062's plan).
4. re_li_summand_le — full rewrite with mul_geom_sum and fixes. Let me also double check `Finset.sum_range_id_mul_two : (∑ i ∈ range n, i) * 2 = n * (n - 1)` — for ℕ. ✓ exists I believe.
`norm_sum_le : ‖∑ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖` ✓.
`norm_inv : ‖z⁻¹‖ = ‖z‖⁻¹` ✓.
`norm_div : ‖a / b‖ = ‖a‖ / ‖b‖` ✓.
`Complex.abs_re_le_norm : |z.re| ≤ ‖z‖` ✓ (from the grep: abs_re_le_norm exists ✓).
`Complex.inv_re : z⁻¹.re = z.re / normSq z` ✓ (grep found it). Need normSq z = ‖z‖² bridge: `Complex.normSq_eq_norm_sq`? Let me just use normSq form in the final bound instead of ‖z‖²? The final inequality is stated with ‖z‖^2 — conversion: normSq z = ‖z‖^2 — `Complex.normSq_eq_norm_sq (z : ℂ) : normSq z = ‖z‖ ^ 2`? I think there is `Complex.normSq_eq_norm_sq`. If not: normSq z = (Complex.abs z)^2 via `Complex.normSq_eq_abs` and `Complex.norm_eq_abs`. I'll write: `have hnsq : Complex.normSq z = ‖z‖ ^ 2 := by rw [Complex.normSq_eq_abs, Complex.norm_eq_abs]`.
For hre1: ((n : ℂ) * (1 / z)).re = n * z.re / ‖z‖ ^ 2:
(n·(1/z)).re = n·(1/z).re (n real: (a·b).re with a = n ∈ ℝ — `Complex.re_ofReal_mul`? simpler: (n : ℂ) = (n : ℝ) cast; (x * y).re = x.re*y.re − x.im*y.im; (n:ℂ).im = 0, (n:ℂ).re = n ✓ so (n·w).re = n·w.re: `Complex.natCast_re`? simp handles: simp [Complex.mul_re, Complex.natCast_re, Complex.natCast_im]. Then (1/z).re = z.re/normSq z (inv_re with one_div). So:
```
have hre1 : ((n : ℂ) * (1 / z)).re = n * z.re / ‖z‖ ^ 2 := by
have hinv : ((1 : ℂ) / z).re = z.re / ‖z‖ ^ 2 := by
rw [one_div, Complex.inv_re, hnsq]
rw [show (n : ℂ) * (1 / z) = (n : ℝ) * (1 / z) by simp]
simp [Complex.mul_re, hinv]
```
Hmm — (n:ℂ)·w: mul_re: (a*b).re = a.re*b.re − a.im*b.im; with a = (n:ℂ): a.re = n, a.im = 0: = n·b.re. simp [Complex.mul_re, Complex.natCast_re, Complex.natCast_im, hinv] should give n·(z.re/‖z‖²) = n·z.re/‖z‖² — need ring_nf maybe. I'll use: `rw [Complex.mul_re]; simp [hinv]; ring`. Might need fiddling; iterate.
Actually cleaner: avoid hre1 entirely — restructure hfre to keep (1/z)·n as n·(1/z).re... Alternatively: bind everything through the real identity Re(a·b)... Let me simplify the whole hfre step:
f = (1/z)·S = (1/z)·n + (1/z)·(S−n). f.re = ((1/z)·n).re + ((1/z)·(S−n)).re.
((1/z)·n).re = n·(1/z).re since n is a nonnegative real (as a complex scalar with 0 imag part).
(1/z).re = z.re/normSq z.
So f.re = n·z.re/normSq z + ((S−n)/z).re. Then:
|f.re| ≤ n·|z.re|/normSq z + ‖(S−n)/z‖ ≤ n/normSq z + (n²/‖z‖)/‖z‖ = n/‖z‖² + n²/‖z‖².
Wait — (S−n)/z: note (1/z)·(S−n) = (S−n)/z ✓ same norm.
n·z.re/normSq z: |n·z.re/normSq z| = n·|z.re|/normSq z ≤ n·1/normSq z (|z.re| ≤ 1). And normSq z = ‖z‖² ✓.
OK let me write the final file now, carefully. Also drop the unused hre1-Complex.add_re bits.
One more possible issue: `Finset.sum_range_id_mul_two n : (∑ i ∈ range n, i) * 2 = n * (n - 1)` — this is for ℕ. In the real context I cast. Fine.
And in hbound: I have extra parens and the max handling; hwmax : max 1 ‖w‖ ≤ 1 + 1/(2n): from hwnorm : ‖w‖ ≤ 1 + 1/‖z‖ and 1/‖z‖ ≤ 1/(2n): max_le (by positivity?) hmm max 1 ‖w‖ ≤ 1 + 1/(2n) ⟸ 1 ≤ 1+1/(2n) ✓ and ‖w‖ ≤ 1+1/(2n) ✓ via hwnorm.trans (add_le_add_left ...). Fine.
pow bound: ‖w^i‖ = ‖w‖^i ≤ (1+1/(2n))^i ≤ (1+1/(2n))^{n-1} for i ≤ n−1: `pow_le_pow_left₀ (h : 0 ≤ a) (hab : a ≤ b) (n)` then `pow_le_pow_right₀ (hb : 1 ≤ b) (h : m ≤ n)`: chain: ‖w‖^i ≤ (1+1/(2n))^i ≤ (1+1/(2n))^{n-1}:
step1: pow_le_pow_left₀ (norm_nonneg _) (le_trans (le_max_right 1 ‖w‖) hwmax) i
step2: pow_le_pow_right₀ (by positivity? need 1 ≤ 1+1/(2n)) (i ≤ n−1)
— pow_le_pow_right₀ signature check: `pow_le_pow_right₀ (hb : 1 ≤ b) (h : m ≤ n) : b ^ m ≤ b ^ n`? Hmm — actual name/signature in current Mathlib: `pow_le_pow_right₀ (ha : 1 ≤ a) (hmn : m ≤ n) : a ^ m ≤ a ^ n` — I believe so (there was a rename from pow_le_pow_of_le_one... no that's different). Try it.
The earlier gcongr "no goals" issue: gcongr closed the side goals automatically; I restructured to explicit apply.
Let me also reconsider the hsumj: `Finset.sum_range_id_mul_two (n : ℕ) : (∑ i ∈ range n, i) * 2 = n * (n - 1)` ✓.
OK writing the final version now. Also fix the earlier `Finset.mul_sum` step:
∑_{j<n} (1/‖z‖)·(j·M) = (1/‖z‖)·M·∑_{j<n} j:
conv: each term (1/‖z‖)*(j*M) = ((1/‖z‖)*M)*j → Finset.mul_sum: ∑ (c·j) = c·∑ j:
rw [Finset.mul_sum] turns ∑ ((1/‖z‖)*j*M)?? Let me set c := (1/‖z‖)*M and show each summand = c*j by ring, then `rw [← Finset.mul_sum]`? Finset.mul_sum : c * ∑ f = ∑ c·f — direction: `← Finset.mul_sum` rewrites ∑ (c·f) → c·∑f ✓. So:
have : ∀ j ∈ range n, (1/‖z‖)*(j*M) = ((1/‖z‖)*M)*j := fun j _ => by ring
rw [Finset.sum_congr rfl this, ← Finset.mul_sum]
Let me write the complete fixed file.
All names confirmed: `mul_geom_sum` (right direction), `Complex.inv_re`, `star_div₀`, and conj = the bundled hom (so `map_` lemmas apply). Rewriting with fixes.
tool: Write ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\Scratch.lean",
"content": "/- Session 015 scratch: ii\u2032-1a \u2014 paired liSummand + summability (D-064 \u00a71).\n When green, merge into LiSkeleton.lean \u00a71 replacing the defective liCoeff. -/\nimport Mathlib\nimport Zeta23.WeilEF.ZeroSummability\nimport Zeta23.Statement.SeamClosed\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-- The paired (symmetrized) Li summand: \u00bd\u00b7mult\u00b7(f \u03c1 + f \u03c1\u0304),\nf \u03c1 = 1 \u2212 (1\u22121/\u03c1)\u207f. Manifestly real-valued (`liSummand_eq`), absolutely\nsummable (`liSummable`) \u2014 the correct Keiper\u2013Li coefficient (D-064 \u00a71:\nthe plain unordered sum of f over the zeros is not absolutely\nsummable; the pairing is the classical Bombieri\u2013Lagarias convention). -/\ndef liSummand (n : \u2115) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) : \u2102 :=\n (zeroMult \u03c1 : \u2102) / 2 * ((1 - (1 - 1 / (\u03c1 : \u2102)) ^ n) + (1 - (1 - 1 / (conj (\u03c1 : \u2102))) ^ n))\n\nlemma summand_conj (n : \u2115) (z : \u2102) :\n (1 : \u2102) - (1 - 1 / (conj z)) ^ n = conj ((1 - (1 - 1 / z) ^ n)) := by\n rw [map_sub, map_one, map_pow, map_sub, map_one, map_div\u2080, map_one]\n\nlemma liSummand_eq (n : \u2115) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) :\n liSummand n \u03c1 = (zeroMult \u03c1 : \u2102) * (((1 - (1 - 1 / (\u03c1 : \u2102)) ^ n).re) : \u2102) := by\n rw [liSummand, summand_conj, Complex.add_conj]\n ring\n\n/-! ### The geometric-sum estimate: |Re(1 \u2212 w\u207f)| \u2264 2n\u00b2/\u2016z\u2016\u00b2 for w = 1\u22121/z -/\n\n/-- (1 + 1/(2n))\u207f \u2264 2 for n \u2265 1. Via (1+x)\u207f \u2264 exp(nx) and exp(1/2) \u2264 2. -/\nlemma pow_one_add_inv_two_mul_le (n : \u2115) (hn : 1 \u2264 n) :\n ((1 : \u211d) + 1 / (2 * n)) ^ n \u2264 2 := by\n have hn0 : (0 : \u211d) < n := by exact_mod_cast hn\n have hbase : (1 : \u211d) + 1 / (2 * n) \u2264 Real.exp (1 / (2 * n)) :=\n Real.add_one_le_exp _\n have h1 : ((1 : \u211d) + 1 / (2 * n)) ^ n \u2264 Real.exp (1 / 2) := by\n calc ((1 : \u211d) + 1 / (2 * n)) ^ n\n \u2264 (Real.exp (1 / (2 * n))) ^ n := pow_le_pow_left\u2080 (by positivity) hbase n\n _ = Real.exp (\u2191n * (1 / (2 * n))) := by rw [Real.exp_nat_mul]\n _ = Real.exp (1 / 2) := by congr 1; field_simp\n have h2 : Real.exp (1 / 2 : \u211d) \u2264 2 := by\n have h3 : (1 : \u211d) / 2 \u2264 Real.log 2 := by\n have h := Real.log_two_gt_d9\n linarith\n calc Real.exp (1 / 2 : \u211d) \u2264 Real.exp (Real.log 2) := Real.exp_le_exp.mpr h3\n _ = 2 := Real.exp_log (by norm_num)\n exact h1.trans h2\n\n/-- Key estimate: for n \u2265 1, z with re z \u2208 [0,1], 2n \u2264 \u2016z\u2016:\n|Re(1 \u2212 (1\u22121/z)\u207f)| \u2264 2n\u00b2/\u2016z\u2016\u00b2. -/\nlemma re_li_summand_le {n : \u2115} (hn : 1 \u2264 n) {z : \u2102}\n (hzre0 : 0 \u2264 z.re) (hzre1 : z.re \u2264 1) (hz : 2 * n \u2264 \u2016z\u2016) :\n |(1 - (1 - 1 / z) ^ n).re| \u2264 2 * n ^ 2 / \u2016z\u2016 ^ 2 := by\n have hn0 : (0 : \u211d) < n := by exact_mod_cast hn\n have hz0 : z \u2260 0 := by\n intro h; rw [h, norm_zero] at hz; linarith\n have hzn : (0 : \u211d) < \u2016z\u2016 := norm_pos_iff.mpr hz0\n have hnsq : Complex.normSq z = \u2016z\u2016 ^ 2 := by\n rw [Complex.normSq_eq_abs, Complex.norm_eq_abs]\n set w : \u2102 := 1 - 1 / z with hw\n -- kernel identity: 1 \u2212 w\u207f = (1/z)\u00b7S, S = \u03a3_{j<n} w^j\n have hgeom : (w - 1) * \u2211 j \u2208 Finset.range n, w ^ j = w ^ n - 1 := mul_geom_sum w n\n have hw1 : w - 1 = -(1 / z) := by rw [hw]; ring\n have hf : (1 : \u2102) - w ^ n = (1 / z) * \u2211 j \u2208 Finset.range n, w ^ j := by\n have h := hgeom\n rw [hw1] at h\n have e := congr_arg Neg.neg h\n simp only [neg_sub, sub_eq_add_neg] at e \u22a2\n have e2 : (1 : \u2102) - w ^ n = -(w ^ n - 1) := by ring\n rw [e2, h]; ring\n set S : \u2102 := \u2211 j \u2208 Finset.range n, w ^ j\n have hS : S = (n : \u2102) + (S - n) := by ring\n -- \u2016w\u2016 \u2264 1 + 1/\u2016z\u2016\n have hwnorm : \u2016w\u2016 \u2264 1 + 1 / \u2016z\u2016 := by\n have e : w = 1 - z\u207b\u00b9 := by rw [hw, div_eq_mul_inv, one_mul]\n rw [e]\n calc \u2016(1 : \u2102) - z\u207b\u00b9\u2016 \u2264 \u2016(1 : \u2102)\u2016 + \u2016z\u207b\u00b9\u2016 := norm_sub_le _ _\n _ = 1 + 1 / \u2016z\u2016 := by rw [norm_one, norm_inv, inv_eq_one_div]\n have h1z : 1 / \u2016z\u2016 \u2264 1 / (2 * n) :=\n one_div_le_one_div_of_le (by positivity) (by exact_mod_cast hz)\n have hwmax : max 1 \u2016w\u2016 \u2264 1 + 1 / (2 * n) := by\n apply max_le (by positivity)\n exact hwnorm.trans (by linarith)\n -- |S \u2212 n| \u2264 n\u00b2/\u2016z\u2016\n have hSn : \u2016S - n\u2016 \u2264 n ^ 2 / \u2016z\u2016 := by\n have hSn1 : S - n = \u2211 j \u2208 Finset.range n, (w ^ j - 1) := by\n rw [Finset.sum_sub_distrib]\n simp [Finset.sum_const, Finset.card_range]\n have hbound : \u2200 j \u2208 Finset.range n,\n \u2016w ^ j - 1\u2016 \u2264 (1 / \u2016z\u2016) * (j * (1 + 1 / (2 * n)) ^ (n - 1)) := by\n intro j hj\n have hgeomj : (w - 1) * \u2211 i \u2208 Finset.range j, w ^ i = w ^ j - 1 := mul_geom_sum w j\n have hjn : j \u2264 n := le_of_lt (Finset.mem_range.mp hj)\n have h2 : w ^ j - 1 = -(1 / z) * \u2211 i \u2208 Finset.range j, w ^ i := by\n have h := hgeomj; rw [hw1] at h\n rw [\u2190 h]; ring\n rw [h2, norm_mul, norm_neg, norm_div, norm_one]\n have hsum : \u2016\u2211 i \u2208 Finset.range j, w ^ i\u2016 \u2264 j * (1 + 1 / (2 * n)) ^ (n - 1) := by\n calc \u2016\u2211 i \u2208 Finset.range j, w ^ i\u2016\n \u2264 \u2211 i \u2208 Finset.range j, \u2016w ^ i\u2016 := norm_sum_le _ _\n _ \u2264 \u2211 i \u2208 Finset.range j, (1 + 1 / (2 * n)) ^ (n - 1) := by\n apply Finset.sum_le_sum\n intro i hi\n rw [norm_pow]\n have hij : i < j := Finset.mem_range.mp hi\n have h1 : \u2016w\u2016 ^ i \u2264 (1 + 1 / (2 * n)) ^ i :=\n pow_le_pow_left\u2080 (norm_nonneg _)\n (le_trans (le_max_right 1 \u2016w\u2016) hwmax) i\n have h2 : (1 + 1 / (2 * n)) ^ i \u2264 (1 + 1 / (2 * n)) ^ (n - 1) := by\n apply pow_le_pow_right\u2080 (by positivity)\n omega\n exact h1.trans h2\n _ = j * (1 + 1 / (2 * n)) ^ (n - 1) := by\n rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul]\n exact mul_le_mul_of_nonneg_left hsum (by positivity)\n calc \u2016\u2211 j \u2208 Finset.range n, (w ^ j - 1)\u2016\n \u2264 \u2211 j \u2208 Finset.range n, \u2016w ^ j - 1\u2016 := norm_sum_le _ _\n _ \u2264 \u2211 j \u2208 Finset.range n, (1 / \u2016z\u2016) * (j * (1 + 1 / (2 * n)) ^ (n - 1)) :=\n Finset.sum_le_sum hbound\n _ = ((1 / \u2016z\u2016) * (1 + 1 / (2 * n)) ^ (n - 1)) * \u2211 j \u2208 Finset.range n, j := by\n rw [\u2190 Finset.mul_sum]\n apply Finset.sum_congr rfl\n intro j _; ring\n _ \u2264 n ^ 2 / \u2016z\u2016 := by\n have hsumj : (\u2211 j \u2208 Finset.range n, j : \u211d) = n * (n - 1) / 2 := by\n have h := Finset.sum_range_id_mul_two n\n have h2 : ((\u2211 j \u2208 Finset.range n, j : \u2115) : \u211d) * 2 = n * (n - 1) := by\n exact_mod_cast h\n linarith\n rw [hsumj]\n have hpow : (1 + 1 / (2 * n : \u211d)) ^ (n - 1) \u2264 2 :=\n le_trans (pow_le_pow_right\u2080 (by positivity) (Nat.sub_le n 1))\n (pow_one_add_inv_two_mul_le n hn)\n have hb1 : (n : \u211d) * (n - 1) / 2 \u2264 n ^ 2 / 2 := by nlinarith [hn0]\n have hb2 : (1 + 1 / (2 * n : \u211d)) ^ (n - 1) * (n * (n - 1) / 2)\n \u2264 2 * (n ^ 2 / 2) :=\n mul_le_mul_of_nonneg hpow hb1 (by positivity) (by positivity)\n have hb3 : ((1 : \u211d) / \u2016z\u2016) * (1 + 1 / (2 * n)) ^ (n - 1) * (n * (n - 1) / 2)\n \u2264 (1 / \u2016z\u2016) * (2 * (n ^ 2 / 2)) :=\n mul_le_mul_of_nonneg_left hb2 (by positivity)\n exact hb3.trans (by ring_nf)\n -- Re(f) = n\u00b7z.re/\u2016z\u2016\u00b2 + ((S\u2212n)/z).re\n have hre1 : ((n : \u2102) * (1 / z)).re = n * z.re / \u2016z\u2016 ^ 2 := by\n have hinv : ((1 : \u2102) / z).re = z.re / \u2016z\u2016 ^ 2 := by\n rw [one_div, Complex.inv_re, hnsq]\n rw [Complex.mul_re]\n simp [hinv]\n have hfre : (1 - w ^ n).re = n * z.re / \u2016z\u2016 ^ 2 + ((S - n) / z).re := by\n rw [hf, hS, Complex.add_re]\n congr 1\n rw [mul_comm, div_eq_mul_inv]\n exact hre1\n rw [hfre]\n have hA : |n * z.re / \u2016z\u2016 ^ 2| \u2264 n / \u2016z\u2016 ^ 2 := by\n rw [abs_div, abs_mul, abs_of_nonneg hn0.le,\n abs_of_nonneg (sq_nonneg \u2016z\u2016)]\n apply (div_le_div_right (by positivity)).mpr\n apply mul_le_mul_of_nonneg_left _ hn0.le\n exact abs_le.mpr \u27e8hzre0, hzre1\u27e9\n have hB : |((S - n) / z).re| \u2264 n ^ 2 / \u2016z\u2016 ^ 2 := by\n have h1 : |((S - n) / z).re| \u2264 \u2016(S - n) / z\u2016 := Complex.abs_re_le_norm _\n have h2 : \u2016(S - n) / z\u2016 \u2264 (n ^ 2 / \u2016z\u2016) / \u2016z\u2016 := by\n rw [norm_div]\n exact (div_le_div_right hzn).mpr hSn\n exact h1.trans (h2.trans (by rw [div_div, \u2190 pow_two]))\n have hnn : (n : \u211d) \u2264 n ^ 2 := by\n have h : (1 : \u211d) \u2264 n := by exact_mod_cast hn\n nlinarith\n calc |n * z.re / \u2016z\u2016 ^ 2 + ((S - n) / z).re|\n \u2264 n / \u2016z\u2016 ^ 2 + n ^ 2 / \u2016z\u2016 ^ 2 := (abs_add _ _).trans (add_le_add hA hB)\n _ = (n + n ^ 2) / \u2016z\u2016 ^ 2 := by ring\n _ \u2264 2 * n ^ 2 / \u2016z\u2016 ^ 2 := by\n apply (div_le_div_right (by positivity)).mpr\n linarith\n\nend NguyenRH1\n"
}
result 2026-08-21 19:21:56Z → 2026-08-21 19:21:56Z
{
"type": "update",
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\Scratch.lean",
"content": "/- Session 015 scratch: ii\u2032-1a \u2014 paired liSummand + summability (D-064 \u00a71).\n When green, merge into LiSkeleton.lean \u00a71 replacing the defective liCoeff. -/\nimport Mathlib\nimport Zeta23.WeilEF.ZeroSummability\nimport Zeta23.Statement.SeamClosed\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-- The paired (symmetrized) Li summand: \u00bd\u00b7mult\u00b7(f \u03c1 + f \u03c1\u0304),\nf \u03c1 = 1 \u2212 (1\u22121/\u03c1)\u207f. Manifestly real-valued (`liSummand_eq`), absolutely\nsummable (`liSummable`) \u2014 the correct Keiper\u2013Li coefficient (D-064 \u00a71:\nthe plain unordered sum of f over the zeros is not absolutely\nsummable; the pairing is the classical Bombieri\u2013Lagarias convention). -/\ndef liSummand (n : \u2115) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) : \u2102 :=\n (zeroMult \u03c1 : \u2102) / 2 * ((1 - (1 - 1 / (\u03c1 : \u2102)) ^ n) + (1 - (1 - 1 / (conj (\u03c1 : \u2102))) ^ n))\n\nlemma summand_conj (n : \u2115) (z : \u2102) :\n (1 : \u2102) - (1 - 1 / (conj z)) ^ n = conj ((1 - (1 - 1 / z) ^ n)) := by\n rw [map_sub, map_one, map_pow, map_sub, map_one, map_div\u2080, map_one]\n\nlemma liSummand_eq (n : \u2115) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) :\n liSummand n \u03c1 = (zeroMult \u03c1 : \u2102) * (((1 - (1 - 1 / (\u03c1 : \u2102)) ^ n).re) : \u2102) := by\n rw [liSummand, summand_conj, Complex.add_conj]\n ring\n\n/-! ### The geometric-sum estimate: |Re(1 \u2212 w\u207f)| \u2264 2n\u00b2/\u2016z\u2016\u00b2 for w = 1\u22121/z -/\n\n/-- (1 + 1/(2n))\u207f \u2264 2 for n \u2265 1. Via (1+x)\u207f \u2264 exp(nx) and exp(1/2) \u2264 2. -/\nlemma pow_one_add_inv_two_mul_le (n : \u2115) (hn : 1 \u2264 n) :\n ((1 : \u211d) + 1 / (2 * n)) ^ n \u2264 2 := by\n have hn0 : (0 : \u211d) < n := by exact_mod_cast hn\n have hbase : (1 : \u211d) + 1 / (2 * n) \u2264 Real.exp (1 / (2 * n)) :=\n Real.add_one_le_exp _\n have h1 : ((1 : \u211d) + 1 / (2 * n)) ^ n \u2264 Real.exp (1 / 2) := by\n calc ((1 : \u211d) + 1 / (2 * n)) ^ n\n \u2264 (Real.exp (1 / (2 * n))) ^ n := pow_le_pow_left\u2080 (by positivity) hbase n\n _ = Real.exp (\u2191n * (1 / (2 * n))) := by rw [Real.exp_nat_mul]\n _ = Real.exp (1 / 2) := by congr 1; field_simp\n have h2 : Real.exp (1 / 2 : \u211d) \u2264 2 := by\n have h3 : (1 : \u211d) / 2 \u2264 Real.log 2 := by\n have h := Real.log_two_gt_d9\n linarith\n calc Real.exp (1 / 2 : \u211d) \u2264 Real.exp (Real.log 2) := Real.exp_le_exp.mpr h3\n _ = 2 := Real.exp_log (by norm_num)\n exact h1.trans h2\n\n/-- Key estimate: for n \u2265 1, z with re z \u2208 [0,1], 2n \u2264 \u2016z\u2016:\n|Re(1 \u2212 (1\u22121/z)\u207f)| \u2264 2n\u00b2/\u2016z\u2016\u00b2. -/\nlemma re_li_summand_le {n : \u2115} (hn : 1 \u2264 n) {z : \u2102}\n (hzre0 : 0 \u2264 z.re) (hzre1 : z.re \u2264 1) (hz : 2 * n \u2264 \u2016z\u2016) :\n |(1 - (1 - 1 / z) ^ n).re| \u2264 2 * n ^ 2 / \u2016z\u2016 ^ 2 := by\n have hn0 : (0 : \u211d) < n := by exact_mod_cast hn\n have hz0 : z \u2260 0 := by\n intro h; rw [h, norm_zero] at hz; linarith\n have hzn : (0 : \u211d) < \u2016z\u2016 := norm_pos_iff.mpr hz0\n have hnsq : Complex.normSq z = \u2016z\u2016 ^ 2 := by\n rw [Complex.normSq_eq_abs, Complex.norm_eq_abs]\n set w : \u2102 := 1 - 1 / z with hw\n -- kernel identity: 1 \u2212 w\u207f = (1/z)\u00b7S, S = \u03a3_{j<n} w^j\n have hgeom : (w - 1) * \u2211 j \u2208 Finset.range n, w ^ j = w ^ n - 1 := mul_geom_sum w n\n have hw1 : w - 1 = -(1 / z) := by rw [hw]; ring\n have hf : (1 : \u2102) - w ^ n = (1 / z) * \u2211 j \u2208 Finset.range n, w ^ j := by\n have h := hgeom\n rw [hw1] at h\n have e := congr_arg Neg.neg h\n simp only [neg_sub, sub_eq_add_neg] at e \u22a2\n have e2 : (1 : \u2102) - w ^ n = -(w ^ n - 1) := by ring\n rw [e2, h]; ring\n set S : \u2102 := \u2211 j \u2208 Finset.range n, w ^ j\n have hS : S = (n : \u2102) + (S - n) := by ring\n -- \u2016w\u2016 \u2264 1 + 1/\u2016z\u2016\n have hwnorm : \u2016w\u2016 \u2264 1 + 1 / \u2016z\u2016 := by\n have e : w = 1 - z\u207b\u00b9 := by rw [hw, div_eq_mul_inv, one_mul]\n rw [e]\n calc \u2016(1 : \u2102) - z\u207b\u00b9\u2016 \u2264 \u2016(1 : \u2102)\u2016 + \u2016z\u207b\u00b9\u2016 := norm_sub_le _ _\n _ = 1 + 1 / \u2016z\u2016 := by rw [norm_one, norm_inv, inv_eq_one_div]\n have h1z : 1 / \u2016z\u2016 \u2264 1 / (2 * n) :=\n one_div_le_one_div_of_le (by positivity) (by exact_mod_cast hz)\n have hwmax : max 1 \u2016w\u2016 \u2264 1 + 1 / (2 * n) := by\n apply max_le (by positivity)\n exact hwnorm.trans (by linarith)\n -- |S \u2212 n| \u2264 n\u00b2/\u2016z\u2016\n have hSn : \u2016S - n\u2016 \u2264 n ^ 2 / \u2016z\u2016 := by\n have hSn1 : S - n = \u2211 j \u2208 Finset.range n, (w ^ j - 1) := by\n rw [Finset.sum_sub_distrib]\n simp [Finset.sum_const, Finset.card_range]\n have hbound : \u2200 j \u2208 Finset.range n,\n \u2016w ^ j - 1\u2016 \u2264 (1 / \u2016z\u2016) * (j * (1 + 1 / (2 * n)) ^ (n - 1)) := by\n intro j hj\n have hgeomj : (w - 1) * \u2211 i \u2208 Finset.range j, w ^ i = w ^ j - 1 := mul_geom_sum w j\n have hjn : j \u2264 n := le_of_lt (Finset.mem_range.mp hj)\n have h2 : w ^ j - 1 = -(1 / z) * \u2211 i \u2208 Finset.range j, w ^ i := by\n have h := hgeomj; rw [hw1] at h\n rw [\u2190 h]; ring\n rw [h2, norm_mul, norm_neg, norm_div, norm_one]\n have hsum : \u2016\u2211 i \u2208 Finset.range j, w ^ i\u2016 \u2264 j * (1 + 1 / (2 * n)) ^ (n - 1) := by\n calc \u2016\u2211 i \u2208 Finset.range j, w ^ i\u2016\n \u2264 \u2211 i \u2208 Finset.range j, \u2016w ^ i\u2016 := norm_sum_le _ _\n _ \u2264 \u2211 i \u2208 Finset.range j, (1 + 1 / (2 * n)) ^ (n - 1) := by\n apply Finset.sum_le_sum\n intro i hi\n rw [norm_pow]\n have hij : i < j := Finset.mem_range.mp hi\n have h1 : \u2016w\u2016 ^ i \u2264 (1 + 1 / (2 * n)) ^ i :=\n pow_le_pow_left\u2080 (norm_nonneg _)\n (le_trans (le_max_right 1 \u2016w\u2016) hwmax) i\n have h2 : (1 + 1 / (2 * n)) ^ i \u2264 (1 + 1 / (2 * n)) ^ (n - 1) := by\n apply pow_le_pow_right\u2080 (by positivity)\n omega\n exact h1.trans h2\n _ = j * (1 + 1 / (2 * n)) ^ (n - 1) := by\n rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul]\n exact mul_le_mul_of_nonneg_left hsum (by positivity)\n calc \u2016\u2211 j \u2208 Finset.range n, (w ^ j - 1)\u2016\n \u2264 \u2211 j \u2208 Finset.range n, \u2016w ^ j - 1\u2016 := norm_sum_le _ _\n _ \u2264 \u2211 j \u2208 Finset.range n, (1 / \u2016z\u2016) * (j * (1 + 1 / (2 * n)) ^ (n - 1)) :=\n Finset.sum_le_sum hbound\n _ = ((1 / \u2016z\u2016) * (1 + 1 / (2 * n)) ^ (n - 1)) * \u2211 j \u2208 Finset.range n, j := by\n rw [\u2190 Finset.mul_sum]\n apply Finset.sum_congr rfl\n intro j _; ring\n _ \u2264 n ^ 2 / \u2016z\u2016 := by\n have hsumj : (\u2211 j \u2208 Finset.range n, j : \u211d) = n * (n - 1) / 2 := by\n have h := Finset.sum_range_id_mul_two n\n have h2 : ((\u2211 j \u2208 Finset.range n, j : \u2115) : \u211d) * 2 = n * (n - 1) := by\n exact_mod_cast h\n linarith\n rw [hsumj]\n have hpow : (1 + 1 / (2 * n : \u211d)) ^ (n - 1) \u2264 2 :=\n le_trans (pow_le_pow_right\u2080 (by positivity) (Nat.sub_le n 1))\n (pow_one_add_inv_two_mul_le n hn)\n have hb1 : (n : \u211d) * (n - 1) / 2 \u2264 n ^ 2 / 2 := by nlinarith [hn0]\n have hb2 : (1 + 1 / (2 * n : \u211d)) ^ (n - 1) * (n * (n - 1) / 2)\n \u2264 2 * (n ^ 2 / 2) :=\n mul_le_mul_of_nonneg hpow hb1 (by positivity) (by positivity)\n have hb3 : ((1 : \u211d) / \u2016z\u2016) * (1 + 1 / (2 * n)) ^ (n - 1) * (n * (n - 1) / 2)\n \u2264 (1 / \u2016z\u2016) * (2 * (n ^ 2 / 2)) :=\n mul_le_mul_of_nonneg_left hb2 (by positivity)\n exact hb3.trans (by ring_nf)\n -- Re(f) = n\u00b7z.re/\u2016z\u2016\u00b2 + ((S\u2212n)/z).re\n have hre1 : ((n : \u2102) * (1 / z)).re = n * z.re / \u2016z\u2016 ^ 2 := by\n have hinv : ((1 : \u2102) / z).re = z.re / \u2016z\u2016 ^ 2 := by\n rw [one_div, Complex.inv_re, hnsq]\n rw [Complex.mul_re]\n simp [hinv]\n have hfre : (1 - w ^ n).re = n * z.re / \u2016z\u2016 ^ 2 + ((S - n) / z).re := by\n rw [hf, hS, Complex.add_re]\n congr 1\n rw [mul_comm, div_eq_mul_inv]\n exact hre1\n rw [hfre]\n have hA : |n * z.re / \u2016z\u2016 ^ 2| \u2264 n / \u2016z\u2016 ^ 2 := by\n rw [abs_div, abs_mul, abs_of_nonneg hn0.le,\n abs_of_nonneg (sq_nonneg \u2016z\u2016)]\n apply (div_le_div_right (by positivity)).mpr\n apply mul_le_mul_of_nonneg_left _ hn0.le\n exact abs_le.mpr \u27e8hzre0, hzre1\u27e9\n have hB : |((S - n) / z).re| \u2264 n ^ 2 / \u2016z\u2016 ^ 2 := by\n have h1 : |((S - n) / z).re| \u2264 \u2016(S - n) / z\u2016 := Complex.abs_re_le_norm _\n have h2 : \u2016(S - n) / z\u2016 \u2264 (n ^ 2 / \u2016z\u2016) / \u2016z\u2016 := by\n rw [norm_div]\n exact (div_le_div_right hzn).mpr hSn\n exact h1.trans (h2.trans (by rw [div_div, \u2190 pow_two]))\n have hnn : (n : \u211d) \u2264 n ^ 2 := by\n have h : (1 : \u211d) \u2264 n := by exact_mod_cast hn\n nlinarith\n calc |n * z.re / \u2016z\u2016 ^ 2 + ((S - n) / z).re|\n \u2264 n / \u2016z\u2016 ^ 2 + n ^ 2 / \u2016z\u2016 ^ 2 := (abs_add _ _).trans (add_le_add hA hB)\n _ = (n + n ^ 2) / \u2016z\u2016 ^ 2 := by ring\n _ \u2264 2 * n ^ 2 / \u2016z\u2016 ^ 2 := by\n apply (div_le_div_right (by positivity)).mpr\n linarith\n\nend NguyenRH1\n",
"structuredPatch": [
{
"oldStart": 16,
"oldLines": 15,
"newStart": 16,
"newLines": 15,
"lines": [
" the plain unordered sum of f over the zeros is not absolutely",
" summable; the pairing is the classical Bombieri\u2013Lagarias convention). -/",
" def liSummand (n : \u2115) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) : \u2102 :=",
"- (zeroMult \u03c1 : \u2102) / 2 * ((1 - (1 - 1 / (\u03c1 : \u2102)) ^ n) + (1 - (1 - 1 / (star (\u03c1 : \u2102))) ^ n))",
"+ (zeroMult \u03c1 : \u2102) / 2 * ((1 - (1 - 1 / (\u03c1 : \u2102)) ^ n) + (1 - (1 - 1 / (conj (\u03c1 : \u2102))) ^ n))",
" ",
"-lemma summand_star (n : \u2115) (z : \u2102) :",
"- (1 : \u2102) - (1 - 1 / (star z)) ^ n = star ((1 - (1 - 1 / z) ^ n)) := by",
"+lemma summand_conj (n : \u2115) (z : \u2102) :",
"+ (1 : \u2102) - (1 - 1 / (conj z)) ^ n = conj ((1 - (1 - 1 / z) ^ n)) := by",
" rw [map_sub, map_one, map_pow, map_sub, map_one, map_div\u2080, map_one]",
" ",
" lemma liSummand_eq (n : \u2115) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) :",
" liSummand n \u03c1 = (zeroMult \u03c1 : \u2102) * (((1 - (1 - 1 / (\u03c1 : \u2102)) ^ n).re) : \u2102) := by",
"- rw [liSummand, summand_star, Complex.add_conj]",
"+ rw [liSummand, summand_conj, Complex.add_conj]",
" ring",
" ",
" /-! ### The geometric-sum estimate: |Re(1 \u2212 w\u207f)| \u2264 2n\u00b2/\u2016z\u2016\u00b2 for w = 1\u22121/z -/"
]
},
{
"oldStart": 33,
"oldLines": 26,
"newStart": 33,
"newLines": 20,
"lines": [
" lemma pow_one_add_inv_two_mul_le (n : \u2115) (hn : 1 \u2264 n) :",
" ((1 : \u211d) + 1 / (2 * n)) ^ n \u2264 2 := by",
" have hn0 : (0 : \u211d) < n := by exact_mod_cast hn",
"- have h1 : ((1 : \u211d) + 1 / (2 * n)) ^ n \u2264 Real.exp (n * (1 / (2 * n))) := by",
"- have h := Real.add_one_le_exp (1 / (2 * (n : \u211d)))",
"+ have hbase : (1 : \u211d) + 1 / (2 * n) \u2264 Real.exp (1 / (2 * n)) :=",
"+ Real.add_one_le_exp _",
"+ have h1 : ((1 : \u211d) + 1 / (2 * n)) ^ n \u2264 Real.exp (1 / 2) := by",
" calc ((1 : \u211d) + 1 / (2 * n)) ^ n",
"- \u2264 (Real.exp (1 / (2 * n))) ^ n := by",
"- gcongr",
"- \u00b7 linarith",
"- \u00b7 exact h",
"- _ = Real.exp (n * (1 / (2 * n))) := by",
"- rw [\u2190 Real.exp_nat_mul]",
"- have h2 : (n : \u211d) * (1 / (2 * n)) = 1 / 2 := by field_simp",
"- rw [h2] at h1",
"- have h3 : Real.exp (1 / 2 : \u211d) \u2264 2 := by",
"- have hsq : (Real.exp (1 / 2 : \u211d)) ^ 2 \u2264 (2 : \u211d) ^ 2 := by",
"- rw [\u2190 Real.exp_nat_mul]",
"- have : Real.exp (2 * (1 / 2 : \u211d)) = Real.exp 1 := by ring_nf",
"- rw [this]",
"- have h := Real.exp_one_lt_d9",
"- norm_num at h \u22a2; linarith",
"- nlinarith [Real.exp_pos (1 / 2 : \u211d)]",
"- exact h1.trans h3",
"+ \u2264 (Real.exp (1 / (2 * n))) ^ n := pow_le_pow_left\u2080 (by positivity) hbase n",
"+ _ = Real.exp (\u2191n * (1 / (2 * n))) := by rw [Real.exp_nat_mul]",
"+ _ = Real.exp (1 / 2) := by congr 1; field_simp",
"+ have h2 : Real.exp (1 / 2 : \u211d) \u2264 2 := by",
"+ have h3 : (1 : \u211d) / 2 \u2264 Real.log 2 := by",
"+ have h := Real.log_two_gt_d9",
"+ linarith",
"+ calc Real.exp (1 / 2 : \u211d) \u2264 Real.exp (Real.log 2) := Real.exp_le_exp.mpr h3",
"+ _ = 2 := Real.exp_log (by norm_num)",
"+ exact h1.trans h2",
" ",
" /-- Key estimate: for n \u2265 1, z with re z \u2208 [0,1], 2n \u2264 \u2016z\u2016:",
" |Re(1 \u2212 (1\u22121/z)\u207f)| \u2264 2n\u00b2/\u2016z\u2016\u00b2. -/"
]
},
{
"oldStart": 63,
"oldLines": 41,
"newStart": 57,
"newLines": 46,
"lines": [
" have hz0 : z \u2260 0 := by",
" intro h; rw [h, norm_zero] at hz; linarith",
" have hzn : (0 : \u211d) < \u2016z\u2016 := norm_pos_iff.mpr hz0",
"+ have hnsq : Complex.normSq z = \u2016z\u2016 ^ 2 := by",
"+ rw [Complex.normSq_eq_abs, Complex.norm_eq_abs]",
" set w : \u2102 := 1 - 1 / z with hw",
" -- kernel identity: 1 \u2212 w\u207f = (1/z)\u00b7S, S = \u03a3_{j<n} w^j",
"- have hgeom : w ^ n - 1 = (w - 1) * \u2211 j \u2208 Finset.range n, w ^ j := geom_sum_mul w n",
"+ have hgeom : (w - 1) * \u2211 j \u2208 Finset.range n, w ^ j = w ^ n - 1 := mul_geom_sum w n",
" have hw1 : w - 1 = -(1 / z) := by rw [hw]; ring",
" have hf : (1 : \u2102) - w ^ n = (1 / z) * \u2211 j \u2208 Finset.range n, w ^ j := by",
"- have : (1 : \u2102) - w ^ n = -(w - 1) * \u2211 j \u2208 Finset.range n, w ^ j := by",
"- rw [\u2190 hgeom]; ring",
"- rw [this, hw1]; ring",
"+ have h := hgeom",
"+ rw [hw1] at h",
"+ have e := congr_arg Neg.neg h",
"+ simp only [neg_sub, sub_eq_add_neg] at e \u22a2",
"+ have e2 : (1 : \u2102) - w ^ n = -(w ^ n - 1) := by ring",
"+ rw [e2, h]; ring",
" set S : \u2102 := \u2211 j \u2208 Finset.range n, w ^ j",
"- -- S = n + (S \u2212 n); Re(f) = n\u00b7Re(1/z) + Re((S\u2212n)/z)",
" have hS : S = (n : \u2102) + (S - n) := by ring",
"+ -- \u2016w\u2016 \u2264 1 + 1/\u2016z\u2016",
"+ have hwnorm : \u2016w\u2016 \u2264 1 + 1 / \u2016z\u2016 := by",
"+ have e : w = 1 - z\u207b\u00b9 := by rw [hw, div_eq_mul_inv, one_mul]",
"+ rw [e]",
"+ calc \u2016(1 : \u2102) - z\u207b\u00b9\u2016 \u2264 \u2016(1 : \u2102)\u2016 + \u2016z\u207b\u00b9\u2016 := norm_sub_le _ _",
"+ _ = 1 + 1 / \u2016z\u2016 := by rw [norm_one, norm_inv, inv_eq_one_div]",
"+ have h1z : 1 / \u2016z\u2016 \u2264 1 / (2 * n) :=",
"+ one_div_le_one_div_of_le (by positivity) (by exact_mod_cast hz)",
"+ have hwmax : max 1 \u2016w\u2016 \u2264 1 + 1 / (2 * n) := by",
"+ apply max_le (by positivity)",
"+ exact hwnorm.trans (by linarith)",
" -- |S \u2212 n| \u2264 n\u00b2/\u2016z\u2016",
"- have hwnorm : \u2016w\u2016 \u2264 1 + 1 / \u2016z\u2016 := by",
"- have : w = 1 - z\u207b\u00b9 := by rw [hw, div_eq_mul_inv, one_mul]",
"- rw [this]",
"- calc \u2016(1 : \u2102) - z\u207b\u00b9\u2016 \u2264 \u2016(1 : \u2102)\u2016 + \u2016z\u207b\u00b9\u2016 := norm_sub_le _ _",
"- _ = 1 + 1 / \u2016z\u2016 := by rw [norm_one, norm_inv]",
"- have hwmax : max 1 \u2016w\u2016 \u2264 1 + 1 / (2 * n) := by",
"- have h1 : 1 / \u2016z\u2016 \u2264 1 / (2 * n) := by",
"- apply one_div_le_one_div_of_le (by positivity : (0:\u211d) < 2 * n)",
"- exact_mod_cast hz",
"- have h2 : \u2016w\u2016 \u2264 1 + 1 / (2 * n) := hwnorm.trans (by linarith)",
"- apply max_le",
"- \u00b7 linarith",
"- \u00b7 exact h2",
" have hSn : \u2016S - n\u2016 \u2264 n ^ 2 / \u2016z\u2016 := by",
" have hSn1 : S - n = \u2211 j \u2208 Finset.range n, (w ^ j - 1) := by",
" rw [Finset.sum_sub_distrib]",
" simp [Finset.sum_const, Finset.card_range]",
"- rw [hSn1]",
" have hbound : \u2200 j \u2208 Finset.range n,",
" \u2016w ^ j - 1\u2016 \u2264 (1 / \u2016z\u2016) * (j * (1 + 1 / (2 * n)) ^ (n - 1)) := by",
" intro j hj",
"- have hgeomj : w ^ j - 1 = (w - 1) * \u2211 i \u2208 Finset.range j, w ^ i := geom_sum_mul w j",
"- rw [hgeomj, norm_mul, hw1, norm_neg, norm_div, norm_one]",
"+ have hgeomj : (w - 1) * \u2211 i \u2208 Finset.range j, w ^ i = w ^ j - 1 := mul_geom_sum w j",
"+ have hjn : j \u2264 n := le_of_lt (Finset.mem_range.mp hj)",
"+ have h2 : w ^ j - 1 = -(1 / z) * \u2211 i \u2208 Finset.range j, w ^ i := by",
"+ have h := hgeomj; rw [hw1] at h",
"+ rw [\u2190 h]; ring",
"+ rw [h2, norm_mul, norm_neg, norm_div, norm_one]",
" have hsum : \u2016\u2211 i \u2208 Finset.range j, w ^ i\u2016 \u2264 j * (1 + 1 / (2 * n)) ^ (n - 1) := by",
" calc \u2016\u2211 i \u2208 Finset.range j, w ^ i\u2016",
" \u2264 \u2211 i \u2208 Finset.range j, \u2016w ^ i\u2016 := norm_sum_le _ _"
]
},
{
"oldStart": 105,
"oldLines": 22,
"newStart": 104,
"newLines": 25,
"lines": [
" apply Finset.sum_le_sum",
" intro i hi",
" rw [norm_pow]",
"- have hjn : i \u2264 n - 1 := by",
"- have hij : i < j := Finset.mem_range.mp hi",
"- have hjn' : j \u2264 n := le_of_lt (Finset.mem_range.mp hj)",
"+ have hij : i < j := Finset.mem_range.mp hi",
"+ have h1 : \u2016w\u2016 ^ i \u2264 (1 + 1 / (2 * n)) ^ i :=",
"+ pow_le_pow_left\u2080 (norm_nonneg _)",
"+ (le_trans (le_max_right 1 \u2016w\u2016) hwmax) i",
"+ have h2 : (1 + 1 / (2 * n)) ^ i \u2264 (1 + 1 / (2 * n)) ^ (n - 1) := by",
"+ apply pow_le_pow_right\u2080 (by positivity)",
" omega",
"- exact pow_le_pow_left\u2080 (by positivity)",
"- (le_trans (le_max_right 1 \u2016w\u2016) hwmax) i (by omega)",
"+ exact h1.trans h2",
" _ = j * (1 + 1 / (2 * n)) ^ (n - 1) := by",
" rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul]",
" exact mul_le_mul_of_nonneg_left hsum (by positivity)",
" calc \u2016\u2211 j \u2208 Finset.range n, (w ^ j - 1)\u2016",
" \u2264 \u2211 j \u2208 Finset.range n, \u2016w ^ j - 1\u2016 := norm_sum_le _ _",
"- _ \u2264 \u2211 j \u2208 Finset.range n, (1 / \u2016z\u2016) * (j * (1 + 1 / (2 * n)) ^ (n - 1)) := by",
"- exact Finset.sum_le_sum hbound",
"- _ = (1 / \u2016z\u2016) * (1 + 1 / (2 * n)) ^ (n - 1) * \u2211 j \u2208 Finset.range n, j := by",
"- rw [Finset.mul_sum]; congr 1; rw [Finset.mul_sum]",
"- apply Finset.sum_congr rfl; intro j _; ring",
"+ _ \u2264 \u2211 j \u2208 Finset.range n, (1 / \u2016z\u2016) * (j * (1 + 1 / (2 * n)) ^ (n - 1)) :=",
"+ Finset.sum_le_sum hbound",
"+ _ = ((1 / \u2016z\u2016) * (1 + 1 / (2 * n)) ^ (n - 1)) * \u2211 j \u2208 Finset.range n, j := by",
"+ rw [\u2190 Finset.mul_sum]",
"+ apply Finset.sum_congr rfl",
"+ intro j _; ring",
" _ \u2264 n ^ 2 / \u2016z\u2016 := by",
" have hsumj : (\u2211 j \u2208 Finset.range n, j : \u211d) = n * (n - 1) / 2 := by",
" have h := Finset.sum_range_id_mul_two n"
]
},
{
"oldStart": 128,
"oldLines": 63,
"newStart": 130,
"newLines": 50,
"lines": [
" exact_mod_cast h",
" linarith",
" rw [hsumj]",
"- have hpow : (1 + 1 / (2 * n : \u211d)) ^ (n - 1) \u2264 2 := by",
"- have h := pow_one_add_inv_two_mul_le n hn",
"- calc (1 + 1 / (2 * n : \u211d)) ^ (n - 1)",
"- \u2264 (1 + 1 / (2 * n : \u211d)) ^ n := by",
"- apply pow_le_pow_right\u2080 (by positivity)",
"- \u00b7 have : 1 \u2264 (1 : \u211d) + 1 / (2 * n) := by positivity",
"- exact this",
"- \u00b7 omega",
"- _ \u2264 2 := h",
"- have h3 : (1 / \u2016z\u2016) * (1 + 1 / (2 * n : \u211d)) ^ (n - 1) * (n * (n - 1) / 2)",
"- \u2264 (1 / \u2016z\u2016) * 2 * (n ^ 2 / 2) := by",
"- apply mul_le_mul_of_nonneg_left _ (by positivity)",
"- apply mul_le_mul_of_nonneg_left hpow (by positivity)",
"- \u00b7 have : (n : \u211d) * (n - 1) / 2 \u2264 n ^ 2 / 2 := by",
"- have hn1 : (1 : \u211d) \u2264 n := by exact_mod_cast hn",
"- nlinarith",
"- linarith",
"- calc (1 / \u2016z\u2016) * (1 + 1 / (2 * n : \u211d)) ^ (n - 1) * (n * (n - 1) / 2)",
"- \u2264 (1 / \u2016z\u2016) * 2 * (n ^ 2 / 2) := h3",
"- _ = n ^ 2 / \u2016z\u2016 := by ring",
"- -- assemble",
"- have hfre : (1 - w ^ n).re = n * z.re / \u2016z\u2016 ^ 2 + (((S - n) / z).re) := by",
"- rw [hf, hS]",
"- have h1 : ((1 / z) * ((n : \u2102) + (S - n))) = (n : \u2102) * (1 / z) + (S - n) / z := by",
"- field_simp; ring",
"- rw [h1]",
"- have hre1 : ((n : \u2102) * (1 / z)).re = n * z.re / \u2016z\u2016 ^ 2 := by",
"- have hinv : ((1 : \u2102) / z).re = z.re / \u2016z\u2016 ^ 2 := by",
"- rw [one_div, Complex.inv_def]",
"- simp [Complex.div_re, Complex.normSq_apply, Complex.norm_eq_abs,",
"- Complex.sq_abs]",
"- rw [Complex.add_re] at *",
"- simp [hinv]",
"- rw [Complex.add_re, hre1]",
"+ have hpow : (1 + 1 / (2 * n : \u211d)) ^ (n - 1) \u2264 2 :=",
"+ le_trans (pow_le_pow_right\u2080 (by positivity) (Nat.sub_le n 1))",
"+ (pow_one_add_inv_two_mul_le n hn)",
"+ have hb1 : (n : \u211d) * (n - 1) / 2 \u2264 n ^ 2 / 2 := by nlinarith [hn0]",
"+ have hb2 : (1 + 1 / (2 * n : \u211d)) ^ (n - 1) * (n * (n - 1) / 2)",
"+ \u2264 2 * (n ^ 2 / 2) :=",
"+ mul_le_mul_of_nonneg hpow hb1 (by positivity) (by positivity)",
"+ have hb3 : ((1 : \u211d) / \u2016z\u2016) * (1 + 1 / (2 * n)) ^ (n - 1) * (n * (n - 1) / 2)",
"+ \u2264 (1 / \u2016z\u2016) * (2 * (n ^ 2 / 2)) :=",
"+ mul_le_mul_of_nonneg_left hb2 (by positivity)",
"+ exact hb3.trans (by ring_nf)",
"+ -- Re(f) = n\u00b7z.re/\u2016z\u2016\u00b2 + ((S\u2212n)/z).re",
"+ have hre1 : ((n : \u2102) * (1 / z)).re = n * z.re / \u2016z\u2016 ^ 2 := by",
"+ have hinv : ((1 : \u2102) / z).re = z.re / \u2016z\u2016 ^ 2 := by",
"+ rw [one_div, Complex.inv_re, hnsq]",
"+ rw [Complex.mul_re]",
"+ simp [hinv]",
"+ have hfre : (1 - w ^ n).re = n * z.re / \u2016z\u2016 ^ 2 + ((S - n) / z).re := by",
"+ rw [hf, hS, Complex.add_re]",
"+ congr 1",
"+ rw [mul_comm, div_eq_mul_inv]",
"+ exact hre1",
" rw [hfre]",
" have hA : |n * z.re / \u2016z\u2016 ^ 2| \u2264 n / \u2016z\u2016 ^ 2 := by",
"- rw [abs_div, abs_mul, abs_of_nonneg hn0.le, abs_pow]",
"- apply div_le_div_of_nonneg_right (by positivity)",
"- calc |z.re| \u2264 1 := abs_le.mpr \u27e8by linarith, hzre1\u27e9",
"- _ \u2264 _ := by linarith",
"+ rw [abs_div, abs_mul, abs_of_nonneg hn0.le,",
"+ abs_of_nonneg (sq_nonneg \u2016z\u2016)]",
"+ apply (div_le_div_right (by positivity)).mpr",
"+ apply mul_le_mul_of_nonneg_left _ hn0.le",
"+ exact abs_le.mpr \u27e8hzre0, hzre1\u27e9",
" have hB : |((S - n) / z).re| \u2264 n ^ 2 / \u2016z\u2016 ^ 2 := by",
" have h1 : |((S - n) / z).re| \u2264 \u2016(S - n) / z\u2016 := Complex.abs_re_le_norm _",
" have h2 : \u2016(S - n) / z\u2016 \u2264 (n ^ 2 / \u2016z\u2016) / \u2016z\u2016 := by",
" rw [norm_div]",
"- apply div_le_div_of_nonneg_right hSn (by positivity)",
"- rw [div_pow] at *",
"- calc |((S - n) / z).re| \u2264 \u2016(S - n) / z\u2016 := h1",
"- _ \u2264 (n ^ 2 / \u2016z\u2016) / \u2016z\u2016 := h2",
"- _ = n ^ 2 / \u2016z\u2016 ^ 2 := by ring",
"+ exact (div_le_div_right hzn).mpr hSn",
"+ exact h1.trans (h2.trans (by rw [div_div, \u2190 pow_two]))",
"+ have hnn : (n : \u211d) \u2264 n ^ 2 := by",
"+ have h : (1 : \u211d) \u2264 n := by exact_mod_cast hn",
"+ nlinarith",
" calc |n * z.re / \u2016z\u2016 ^ 2 + ((S - n) / z).re|",
"- \u2264 n / \u2016z\u2016 ^ 2 + n ^ 2 / \u2016z\u2016 ^ 2 := abs_add _ _ |>.trans (add_le_add hA hB)",
"+ \u2264 n / \u2016z\u2016 ^ 2 + n ^ 2 / \u2016z\u2016 ^ 2 := (abs_add _ _).trans (add_le_add hA hB)",
"+ _ = (n + n ^ 2) / \u2016z\u2016 ^ 2 := by ring",
" _ \u2264 2 * n ^ 2 / \u2016z\u2016 ^ 2 := by",
"- have hn1 : (n : \u211d) \u2264 n ^ 2 := by",
"- have : (1 : \u211d) \u2264 n := by exact_mod_cast hn",
"- nlinarith",
"- field_simp at *",
"- nlinarith",
"+ apply (div_le_div_right (by positivity)).mpr",
"+ linarith",
" ",
" end NguyenRH1",
" "
]
}
],
"originalFile": "/- Session 015 scratch: ii\u2032-1a \u2014 paired liSummand + summability (D-064 \u00a71).\n When green, merge into LiSkeleton.lean \u00a71 replacing the defective liCoeff. -/\nimport Mathlib\nimport Zeta23.WeilEF.ZeroSummability\nimport Zeta23.Statement.SeamClosed\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-- The paired (symmetrized) Li summand: \u00bd\u00b7mult\u00b7(f \u03c1 + f \u03c1\u0304),\nf \u03c1 = 1 \u2212 (1\u22121/\u03c1)\u207f. Manifestly real-valued (`liSummand_eq`), absolutely\nsummable (`liSummable`) \u2014 the correct Keiper\u2013Li coefficient (D-064 \u00a71:\nthe plain unordered sum of f over the zeros is not absolutely\nsummable; the pairing is the classical Bombieri\u2013Lagarias convention). -/\ndef liSummand (n : \u2115) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) : \u2102 :=\n (zeroMult \u03c1 : \u2102) / 2 * ((1 - (1 - 1 / (\u03c1 : \u2102)) ^ n) + (1 - (1 - 1 / (star (\u03c1 : \u2102))) ^ n))\n\nlemma summand_star (n : \u2115) (z : \u2102) :\n (1 : \u2102) - (1 - 1 / (star z)) ^ n = star ((1 - (1 - 1 / z) ^ n)) := by\n rw [map_sub, map_one, map_pow, map_sub, map_one, map_div\u2080, map_one]\n\nlemma liSummand_eq (n : \u2115) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) :\n liSummand n \u03c1 = (zeroMult \u03c1 : \u2102) * (((1 - (1 - 1 / (\u03c1 : \u2102)) ^ n).re) : \u2102) := by\n rw [liSummand, summand_star, Complex.add_conj]\n ring\n\n/-! ### The geometric-sum estimate: |Re(1 \u2212 w\u207f)| \u2264 2n\u00b2/\u2016z\u2016\u00b2 for w = 1\u22121/z -/\n\n/-- (1 + 1/(2n))\u207f \u2264 2 for n \u2265 1. Via (1+x)\u207f \u2264 exp(nx) and exp(1/2) \u2264 2. -/\nlemma pow_one_add_inv_two_mul_le (n : \u2115) (hn : 1 \u2264 n) :\n ((1 : \u211d) + 1 / (2 * n)) ^ n \u2264 2 := by\n have hn0 : (0 : \u211d) < n := by exact_mod_cast hn\n have h1 : ((1 : \u211d) + 1 / (2 * n)) ^ n \u2264 Real.exp (n * (1 / (2 * n))) := by\n have h := Real.add_one_le_exp (1 / (2 * (n : \u211d)))\n calc ((1 : \u211d) + 1 / (2 * n)) ^ n\n \u2264 (Real.exp (1 / (2 * n))) ^ n := by\n gcongr\n \u00b7 linarith\n \u00b7 exact h\n _ = Real.exp (n * (1 / (2 * n))) := by\n rw [\u2190 Real.exp_nat_mul]\n have h2 : (n : \u211d) * (1 / (2 * n)) = 1 / 2 := by field_simp\n rw [h2] at h1\n have h3 : Real.exp (1 / 2 : \u211d) \u2264 2 := by\n have hsq : (Real.exp (1 / 2 : \u211d)) ^ 2 \u2264 (2 : \u211d) ^ 2 := by\n rw [\u2190 Real.exp_nat_mul]\n have : Real.exp (2 * (1 / 2 : \u211d)) = Real.exp 1 := by ring_nf\n rw [this]\n have h := Real.exp_one_lt_d9\n norm_num at h \u22a2; linarith\n nlinarith [Real.exp_pos (1 / 2 : \u211d)]\n exact h1.trans h3\n\n/-- Key estimate: for n \u2265 1, z with re z \u2208 [0,1], 2n \u2264 \u2016z\u2016:\n|Re(1 \u2212 (1\u22121/z)\u207f)| \u2264 2n\u00b2/\u2016z\u2016\u00b2. -/\nlemma re_li_summand_le {n : \u2115} (hn : 1 \u2264 n) {z : \u2102}\n (hzre0 : 0 \u2264 z.re) (hzre1 : z.re \u2264 1) (hz : 2 * n \u2264 \u2016z\u2016) :\n |(1 - (1 - 1 / z) ^ n).re| \u2264 2 * n ^ 2 / \u2016z\u2016 ^ 2 := by\n have hn0 : (0 : \u211d) < n := by exact_mod_cast hn\n have hz0 : z \u2260 0 := by\n intro h; rw [h, norm_zero] at hz; linarith\n have hzn : (0 : \u211d) < \u2016z\u2016 := norm_pos_iff.mpr hz0\n set w : \u2102 := 1 - 1 / z with hw\n -- kernel identity: 1 \u2212 w\u207f = (1/z)\u00b7S, S = \u03a3_{j<n} w^j\n have hgeom : w ^ n - 1 = (w - 1) * \u2211 j \u2208 Finset.range n, w ^ j := geom_sum_mul w n\n have hw1 : w - 1 = -(1 / z) := by rw [hw]; ring\n have hf : (1 : \u2102) - w ^ n = (1 / z) * \u2211 j \u2208 Finset.range n, w ^ j := by\n have : (1 : \u2102) - w ^ n = -(w - 1) * \u2211 j \u2208 Finset.range n, w ^ j := by\n rw [\u2190 hgeom]; ring\n rw [this, hw1]; ring\n set S : \u2102 := \u2211 j \u2208 Finset.range n, w ^ j\n -- S = n + (S \u2212 n); Re(f) = n\u00b7Re(1/z) + Re((S\u2212n)/z)\n have hS : S = (n : \u2102) + (S - n) := by ring\n -- |S \u2212 n| \u2264 n\u00b2/\u2016z\u2016\n have hwnorm : \u2016w\u2016 \u2264 1 + 1 / \u2016z\u2016 := by\n have : w = 1 - z\u207b\u00b9 := by rw [hw, div_eq_mul_inv, one_mul]\n rw [this]\n calc \u2016(1 : \u2102) - z\u207b\u00b9\u2016 \u2264 \u2016(1 : \u2102)\u2016 + \u2016z\u207b\u00b9\u2016 := norm_sub_le _ _\n _ = 1 + 1 / \u2016z\u2016 := by rw [norm_one, norm_inv]\n have hwmax : max 1 \u2016w\u2016 \u2264 1 + 1 / (2 * n) := by\n have h1 : 1 / \u2016z\u2016 \u2264 1 / (2 * n) := by\n apply one_div_le_one_div_of_le (by positivity : (0:\u211d) < 2 * n)\n exact_mod_cast hz\n have h2 : \u2016w\u2016 \u2264 1 + 1 / (2 * n) := hwnorm.trans (by linarith)\n apply max_le\n \u00b7 linarith\n \u00b7 exact h2\n have hSn : \u2016S - n\u2016 \u2264 n ^ 2 / \u2016z\u2016 := by\n have hSn1 : S - n = \u2211 j \u2208 Finset.range n, (w ^ j - 1) := by\n rw [Finset.sum_sub_distrib]\n simp [Finset.sum_const, Finset.card_range]\n rw [hSn1]\n have hbound : \u2200 j \u2208 Finset.range n,\n \u2016w ^ j - 1\u2016 \u2264 (1 / \u2016z\u2016) * (j * (1 + 1 / (2 * n)) ^ (n - 1)) := by\n intro j hj\n have hgeomj : w ^ j - 1 = (w - 1) * \u2211 i \u2208 Finset.range j, w ^ i := geom_sum_mul w j\n rw [hgeomj, norm_mul, hw1, norm_neg, norm_div, norm_one]\n have hsum : \u2016\u2211 i \u2208 Finset.range j, w ^ i\u2016 \u2264 j * (1 + 1 / (2 * n)) ^ (n - 1) := by\n calc \u2016\u2211 i \u2208 Finset.range j, w ^ i\u2016\n \u2264 \u2211 i \u2208 Finset.range j, \u2016w ^ i\u2016 := norm_sum_le _ _\n _ \u2264 \u2211 i \u2208 Finset.range j, (1 + 1 / (2 * n)) ^ (n - 1) := by\n apply Finset.sum_le_sum\n intro i hi\n rw [norm_pow]\n have hjn : i \u2264 n - 1 := by\n have hij : i < j := Finset.mem_range.mp hi\n have hjn' : j \u2264 n := le_of_lt (Finset.mem_range.mp hj)\n omega\n exact pow_le_pow_left\u2080 (by positivity)\n (le_trans (le_max_right 1 \u2016w\u2016) hwmax) i (by omega)\n _ = j * (1 + 1 / (2 * n)) ^ (n - 1) := by\n rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul]\n exact mul_le_mul_of_nonneg_left hsum (by positivity)\n calc \u2016\u2211 j \u2208 Finset.range n, (w ^ j - 1)\u2016\n \u2264 \u2211 j \u2208 Finset.range n, \u2016w ^ j - 1\u2016 := norm_sum_le _ _\n _ \u2264 \u2211 j \u2208 Finset.range n, (1 / \u2016z\u2016) * (j * (1 + 1 / (2 * n)) ^ (n - 1)) := by\n exact Finset.sum_le_sum hbound\n _ = (1 / \u2016z\u2016) * (1 + 1 / (2 * n)) ^ (n - 1) * \u2211 j \u2208 Finset.range n, j := by\n rw [Finset.mul_sum]; congr 1; rw [Finset.mul_sum]\n apply Finset.sum_congr rfl; intro j _; ring\n _ \u2264 n ^ 2 / \u2016z\u2016 := by\n have hsumj : (\u2211 j \u2208 Finset.range n, j : \u211d) = n * (n - 1) / 2 := by\n have h := Finset.sum_range_id_mul_two n\n have h2 : ((\u2211 j \u2208 Finset.range n, j : \u2115) : \u211d) * 2 = n * (n - 1) := by\n exact_mod_cast h\n linarith\n rw [hsumj]\n have hpow : (1 + 1 / (2 * n : \u211d)) ^ (n - 1) \u2264 2 := by\n have h := pow_one_add_inv_two_mul_le n hn\n calc (1 + 1 / (2 * n : \u211d)) ^ (n - 1)\n \u2264 (1 + 1 / (2 * n : \u211d)) ^ n := by\n apply pow_le_pow_right\u2080 (by positivity)\n \u00b7 have : 1 \u2264 (1 : \u211d) + 1 / (2 * n) := by positivity\n exact this\n \u00b7 omega\n _ \u2264 2 := h\n have h3 : (1 / \u2016z\u2016) * (1 + 1 / (2 * n : \u211d)) ^ (n - 1) * (n * (n - 1) / 2)\n \u2264 (1 / \u2016z\u2016) * 2 * (n ^ 2 / 2) := by\n apply mul_le_mul_of_nonneg_left _ (by positivity)\n apply mul_le_mul_of_nonneg_left hpow (by positivity)\n \u00b7 have : (n : \u211d) * (n - 1) / 2 \u2264 n ^ 2 / 2 := by\n have hn1 : (1 : \u211d) \u2264 n := by exact_mod_cast hn\n nlinarith\n linarith\n calc (1 / \u2016z\u2016) * (1 + 1 / (2 * n : \u211d)) ^ (n - 1) * (n * (n - 1) / 2)\n \u2264 (1 / \u2016z\u2016) * 2 * (n ^ 2 / 2) := h3\n _ = n ^ 2 / \u2016z\u2016 := by ring\n -- assemble\n have hfre : (1 - w ^ n).re = n * z.re / \u2016z\u2016 ^ 2 + (((S - n) / z).re) := by\n rw [hf, hS]\n have h1 : ((1 / z) * ((n : \u2102) + (S - n))) = (n : \u2102) * (1 / z) + (S - n) / z := by\n field_simp; ring\n rw [h1]\n have hre1 : ((n : \u2102) * (1 / z)).re = n * z.re / \u2016z\u2016 ^ 2 := by\n have hinv : ((1 : \u2102) / z).re = z.re / \u2016z\u2016 ^ 2 := by\n rw [one_div, Complex.inv_def]\n simp [Complex.div_re, Complex.normSq_apply, Complex.norm_eq_abs,\n Complex.sq_abs]\n rw [Complex.add_re] at *\n simp [hinv]\n rw [Complex.add_re, hre1]\n rw [hfre]\n have hA : |n * z.re / \u2016z\u2016 ^ 2| \u2264 n / \u2016z\u2016 ^ 2 := by\n rw [abs_div, abs_mul, abs_of_nonneg hn0.le, abs_pow]\n apply div_le_div_of_nonneg_right (by positivity)\n calc |z.re| \u2264 1 := abs_le.mpr \u27e8by linarith, hzre1\u27e9\n _ \u2264 _ := by linarith\n have hB : |((S - n) / z).re| \u2264 n ^ 2 / \u2016z\u2016 ^ 2 := by\n have h1 : |((S - n) / z).re| \u2264 \u2016(S - n) / z\u2016 := Complex.abs_re_le_norm _\n have h2 : \u2016(S - n) / z\u2016 \u2264 (n ^ 2 / \u2016z\u2016) / \u2016z\u2016 := by\n rw [norm_div]\n apply div_le_div_of_nonneg_right hSn (by positivity)\n rw [div_pow] at *\n calc |((S - n) / z).re| \u2264 \u2016(S - n) / z\u2016 := h1\n _ \u2264 (n ^ 2 / \u2016z\u2016) / \u2016z\u2016 := h2\n _ = n ^ 2 / \u2016z\u2016 ^ 2 := by ring\n calc |n * z.re / \u2016z\u2016 ^ 2 + ((S - n) / z).re|\n \u2264 n / \u2016z\u2016 ^ 2 + n ^ 2 / \u2016z\u2016 ^ 2 := abs_add _ _ |>.trans (add_le_add hA hB)\n _ \u2264 2 * n ^ 2 / \u2016z\u2016 ^ 2 := by\n have hn1 : (n : \u211d) \u2264 n ^ 2 := by\n have : (1 : \u211d) \u2264 n := by exact_mod_cast hn\n nlinarith\n field_simp at *\n nlinarith\n\nend NguyenRH1\n",
"autoRead": false
}
raw content_json (database row)
[{"type":"thinking","thinking":"`mul_geom_sum (x : R) (n : ℕ) : (x - 1) * ∑ i ∈ range n, x ^ i = x ^ n - 1` — exactly the direction I wanted. \n\nNow for the star/conj bridge: `star (z : ℂ)` vs `conj z`. conj IS `starRingEnd ℂ` (defined that way), and `star` on ℂ goes through the StarMul instance whose star function is conj. So `star z` should be defeq to `conj z`. In proofs, use `star_div₀`-style lemmas for the star manipulation, then convert to conj by `show` (defeq) or `Complex.star_def` if it exists. Let me test defeq conversion via `show` — I'll write the code and iterate.\n\nLet me now rewrite Scratch.lean with all fixes:\n\n1. summand_star: use star_sub, star_one, star_pow, star_div₀.\n2. liSummand_eq: convert star to conj (defeq — try `show ... conj ...` or simp [star] — hmm; the term in liSummand's def uses `star (ρ:ℂ)`. After summand_star rewrites `1 - (1 - 1/(star z))^n` to `star (1 - (1 - 1/z)^n)`, the goal has `star (1 - ...)`; then `Complex.re_eq_add_conj : (z.re : ℂ) = (z + conj z)/2` — rewrite RHS: goal: (mult/2)·(f + star f) = mult·(re f : ℂ). If star f is defeq conj f, `show (zeroMult : ℂ)/2 * (f + conj f) = _` might work directly since star and conj are defeq. Let me structure: \n```\nlemma liSummand_eq ... := by\n rw [liSummand, summand_star]\n have h : (1 - (1 - 1 / (ρ:ℂ)) ^ n) + star (1 - (1 - 1 / (ρ:ℂ)) ^ n)\n = 2 * (((1 - (1 - 1 / (ρ:ℂ)) ^ n).re) : ℂ) := by\n rw [Complex.add_conj] -- if star ≟ conj defeq, this rw works? add_conj is about conj\n```\nHmm — Complex.add_conj's LHS is `z + conj z`; our term is `f + star f`. rw with add_conj: pattern `?z + conj ?z` — `conj ?z` is `(starRingEnd ℂ) ?z` — the term `star f` where star = Star.star — different head constants (Star.star vs starRingEnd application). rw may fail. Solution: change liSummand's def to use `conj` instead of `star`:\n`(zeroMult ρ : ℂ) / 2 * ((1 - (1 - 1/(ρ:ℂ))^n) + (1 - (1 - 1/(conj (ρ:ℂ)))^n))`\nconj = starRingEnd ℂ — map_ lemmas apply directly (map_sub, map_one, map_pow, map_div₀). And Complex.add_conj matches. \n\nSo summand_conj:\n```\nlemma summand_conj (n : ℕ) (z : ℂ) :\n (1 : ℂ) - (1 - 1 / (conj z)) ^ n = conj ((1 - (1 - 1 / z) ^ n)) := by\n rw [map_sub, map_one, map_pow, map_sub, map_one, map_div₀, map_one]\n```\nconj z = (starRingEnd ℂ) z — map_sub etc. should match with ?f := starRingEnd ℂ ✓ (this failed for star but should work for conj since conj IS the bundled hom).\n\nHmm wait — conj (1/z): map_div₀ (starRingEnd ℂ) 1 z = conj 1 / conj z ✓ = 1/conj z after map_one.\n\n3. pow_one_add_inv_two_mul_le — rewrite cleanly:\n```\nlemma pow_one_add_inv_two_mul_le (n : ℕ) (hn : 1 ≤ n) :\n ((1 : ℝ) + 1 / (2 * n)) ^ n ≤ 2 := by\n have hn0 : (0 : ℝ) < n := by exact_mod_cast hn\n have h1 : ((1 : ℝ) + 1 / (2 * n)) ^ n ≤ Real.exp (1 / 2) := by\n have hbase : (1 : ℝ) + 1 / (2 * n) ≤ Real.exp (1 / (2 * n)) :=\n Real.add_one_le_exp _\n calc ((1 : ℝ) + 1 / (2 * n)) ^ n\n ≤ (Real.exp (1 / (2 * n))) ^ n := by\n apply pow_le_pow_left₀ (by positivity) hbase\n _ = Real.exp (↑n * (1 / (2 * n))) := by\n rw [Real.exp_nat_mul]\n _ = Real.exp (1 / 2) := by\n congr 1; field_simp\n have h2 : Real.exp (1 / 2 : ℝ) ≤ 2 := by\n have h3 : Real.log 2 ≥ 1 / 2 := by\n have h := Real.log_two_gt_d9\n linarith [h]\n calc Real.exp (1 / 2 : ℝ) ≤ Real.exp (Real.log 2) := Real.exp_le_exp.mpr h3\n _ = 2 := Real.exp_log (by norm_num)\n exact h1.trans h2\n```\npow_le_pow_left₀ signature: `pow_le_pow_left₀ (ha : 0 ≤ a) (hab : a ≤ b) (n : ℕ) : a^n ≤ b^n`? I believe `pow_le_pow_left₀ (ha : 0 ≤ a) (hab : a ≤ b) (n : ℕ) : a ^ n ≤ b ^ n` ✓.\n\nReal.exp_nat_mul : `Real.exp_nat_mul (x : ℝ) (n : ℕ) : Real.exp (n * x) = (Real.exp x) ^ n` — so `rw [Real.exp_nat_mul]` on goal `(exp x)^n = exp(n*x)`?? My calc step is `_ = Real.exp (↑n * (1/(2*n)))` — I'm proving `(Real.exp (1/(2n)))^n = Real.exp (↑n * (1/(2*n)))` — that's `Real.exp_nat_mul` REVERSED: `(exp x)^n = exp (n*x)` — so the proof is `rw [Real.exp_nat_mul]` — rewrites RHS `exp (↑n * x)` to `(exp x)^n` making both sides equal ✓. Hmm, wait: exp_nat_mul states exp (n*x) = (exp x)^n; rw [Real.exp_nat_mul] rewrites instances of `exp (n * x)` → `(exp x)^n`. Goal: `(exp x)^n = exp (↑n * x)` → after rw: `(exp x)^n = (exp x)^n` ✓ closed by rfl automatically (rw closes goals that become rfl). But careful: the cast ↑n vs n in exp_nat_mul — exp_nat_mul has (n : ℕ) and the term is `↑n * x` where ↑ is Nat→ℝ cast ✓ matches.\n\n`Real.log_two_gt_d9 : 0.6931471803 < Real.log 2` ✓ exists (used in D-062's plan).\n\n4. re_li_summand_le — full rewrite with mul_geom_sum and fixes. Let me also double check `Finset.sum_range_id_mul_two : (∑ i ∈ range n, i) * 2 = n * (n - 1)` — for ℕ. ✓ exists I believe.\n\n`norm_sum_le : ‖∑ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖` ✓.\n`norm_inv : ‖z⁻¹‖ = ‖z‖⁻¹` ✓.\n`norm_div : ‖a / b‖ = ‖a‖ / ‖b‖` ✓.\n`Complex.abs_re_le_norm : |z.re| ≤ ‖z‖` ✓ (from the grep: abs_re_le_norm exists ✓).\n`Complex.inv_re : z⁻¹.re = z.re / normSq z` ✓ (grep found it). Need normSq z = ‖z‖² bridge: `Complex.normSq_eq_norm_sq`? Let me just use normSq form in the final bound instead of ‖z‖²? The final inequality is stated with ‖z‖^2 — conversion: normSq z = ‖z‖^2 — `Complex.normSq_eq_norm_sq (z : ℂ) : normSq z = ‖z‖ ^ 2`? I think there is `Complex.normSq_eq_norm_sq`. If not: normSq z = (Complex.abs z)^2 via `Complex.normSq_eq_abs` and `Complex.norm_eq_abs`. I'll write: `have hnsq : Complex.normSq z = ‖z‖ ^ 2 := by rw [Complex.normSq_eq_abs, Complex.norm_eq_abs]`.\n\nFor hre1: ((n : ℂ) * (1 / z)).re = n * z.re / ‖z‖ ^ 2:\n (n·(1/z)).re = n·(1/z).re (n real: (a·b).re with a = n ∈ ℝ — `Complex.re_ofReal_mul`? simpler: (n : ℂ) = (n : ℝ) cast; (x * y).re = x.re*y.re − x.im*y.im; (n:ℂ).im = 0, (n:ℂ).re = n ✓ so (n·w).re = n·w.re: `Complex.natCast_re`? simp handles: simp [Complex.mul_re, Complex.natCast_re, Complex.natCast_im]. Then (1/z).re = z.re/normSq z (inv_re with one_div). So:\n```\nhave hre1 : ((n : ℂ) * (1 / z)).re = n * z.re / ‖z‖ ^ 2 := by\n have hinv : ((1 : ℂ) / z).re = z.re / ‖z‖ ^ 2 := by\n rw [one_div, Complex.inv_re, hnsq]\n rw [show (n : ℂ) * (1 / z) = (n : ℝ) * (1 / z) by simp]\n simp [Complex.mul_re, hinv]\n```\nHmm — (n:ℂ)·w: mul_re: (a*b).re = a.re*b.re − a.im*b.im; with a = (n:ℂ): a.re = n, a.im = 0: = n·b.re. simp [Complex.mul_re, Complex.natCast_re, Complex.natCast_im, hinv] should give n·(z.re/‖z‖²) = n·z.re/‖z‖² — need ring_nf maybe. I'll use: `rw [Complex.mul_re]; simp [hinv]; ring`. Might need fiddling; iterate.\n\nActually cleaner: avoid hre1 entirely — restructure hfre to keep (1/z)·n as n·(1/z).re... Alternatively: bind everything through the real identity Re(a·b)... Let me simplify the whole hfre step:\n\nf = (1/z)·S = (1/z)·n + (1/z)·(S−n). f.re = ((1/z)·n).re + ((1/z)·(S−n)).re.\n((1/z)·n).re = n·(1/z).re since n is a nonnegative real (as a complex scalar with 0 imag part).\n(1/z).re = z.re/normSq z.\n\nSo f.re = n·z.re/normSq z + ((S−n)/z).re. Then:\n|f.re| ≤ n·|z.re|/normSq z + ‖(S−n)/z‖ ≤ n/normSq z + (n²/‖z‖)/‖z‖ = n/‖z‖² + n²/‖z‖².\nWait — (S−n)/z: note (1/z)·(S−n) = (S−n)/z ✓ same norm.\nn·z.re/normSq z: |n·z.re/normSq z| = n·|z.re|/normSq z ≤ n·1/normSq z (|z.re| ≤ 1). And normSq z = ‖z‖² ✓.\n\nOK let me write the final file now, carefully. Also drop the unused hre1-Complex.add_re bits.\n\nOne more possible issue: `Finset.sum_range_id_mul_two n : (∑ i ∈ range n, i) * 2 = n * (n - 1)` — this is for ℕ. In the real context I cast. Fine.\n\nAnd in hbound: I have extra parens and the max handling; hwmax : max 1 ‖w‖ ≤ 1 + 1/(2n): from hwnorm : ‖w‖ ≤ 1 + 1/‖z‖ and 1/‖z‖ ≤ 1/(2n): max_le (by positivity?) hmm max 1 ‖w‖ ≤ 1 + 1/(2n) ⟸ 1 ≤ 1+1/(2n) ✓ and ‖w‖ ≤ 1+1/(2n) ✓ via hwnorm.trans (add_le_add_left ...). Fine.\n\npow bound: ‖w^i‖ = ‖w‖^i ≤ (1+1/(2n))^i ≤ (1+1/(2n))^{n-1} for i ≤ n−1: `pow_le_pow_left₀ (h : 0 ≤ a) (hab : a ≤ b) (n)` then `pow_le_pow_right₀ (hb : 1 ≤ b) (h : m ≤ n)`: chain: ‖w‖^i ≤ (1+1/(2n))^i ≤ (1+1/(2n))^{n-1}:\n step1: pow_le_pow_left₀ (norm_nonneg _) (le_trans (le_max_right 1 ‖w‖) hwmax) i\n step2: pow_le_pow_right₀ (by positivity? need 1 ≤ 1+1/(2n)) (i ≤ n−1)\n — pow_le_pow_right₀ signature check: `pow_le_pow_right₀ (hb : 1 ≤ b) (h : m ≤ n) : b ^ m ≤ b ^ n`? Hmm — actual name/signature in current Mathlib: `pow_le_pow_right₀ (ha : 1 ≤ a) (hmn : m ≤ n) : a ^ m ≤ a ^ n` — I believe so (there was a rename from pow_le_pow_of_le_one... no that's different). Try it.\n\nThe earlier gcongr \"no goals\" issue: gcongr closed the side goals automatically; I restructured to explicit apply.\n\nLet me also reconsider the hsumj: `Finset.sum_range_id_mul_two (n : ℕ) : (∑ i ∈ range n, i) * 2 = n * (n - 1)` ✓.\n\nOK writing the final version now. Also fix the earlier `Finset.mul_sum` step:\n∑_{j<n} (1/‖z‖)·(j·M) = (1/‖z‖)·M·∑_{j<n} j:\n conv: each term (1/‖z‖)*(j*M) = ((1/‖z‖)*M)*j → Finset.mul_sum: ∑ (c·j) = c·∑ j:\n rw [Finset.mul_sum] turns ∑ ((1/‖z‖)*j*M)?? Let me set c := (1/‖z‖)*M and show each summand = c*j by ring, then `rw [← Finset.mul_sum]`? Finset.mul_sum : c * ∑ f = ∑ c·f — direction: `← Finset.mul_sum` rewrites ∑ (c·f) → c·∑f ✓. So:\n have : ∀ j ∈ range n, (1/‖z‖)*(j*M) = ((1/‖z‖)*M)*j := fun j _ => by ring\n rw [Finset.sum_congr rfl this, ← Finset.mul_sum]\n\nLet me write the complete fixed file.","signature":""},{"type":"text","text":"All names confirmed: `mul_geom_sum` (right direction), `Complex.inv_re`, `star_div₀`, and conj = the bundled hom (so `map_` lemmas apply). Rewriting with fixes."},{"type":"tool_use","id":"Write_89","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\Scratch.lean","content":"/- Session 015 scratch: ii′-1a — paired liSummand + summability (D-064 §1).\n When green, merge into LiSkeleton.lean §1 replacing the defective liCoeff. -/\nimport Mathlib\nimport Zeta23.WeilEF.ZeroSummability\nimport Zeta23.Statement.SeamClosed\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-- The paired (symmetrized) Li summand: ½·mult·(f ρ + f ρ̄),\nf ρ = 1 − (1−1/ρ)ⁿ. Manifestly real-valued (`liSummand_eq`), absolutely\nsummable (`liSummable`) — the correct Keiper–Li coefficient (D-064 §1:\nthe plain unordered sum of f over the zeros is not absolutely\nsummable; the pairing is the classical Bombieri–Lagarias convention). -/\ndef liSummand (n : ℕ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ :=\n (zeroMult ρ : ℂ) / 2 * ((1 - (1 - 1 / (ρ : ℂ)) ^ n) + (1 - (1 - 1 / (conj (ρ : ℂ))) ^ n))\n\nlemma summand_conj (n : ℕ) (z : ℂ) :\n (1 : ℂ) - (1 - 1 / (conj z)) ^ n = conj ((1 - (1 - 1 / z) ^ n)) := by\n rw [map_sub, map_one, map_pow, map_sub, map_one, map_div₀, map_one]\n\nlemma liSummand_eq (n : ℕ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) :\n liSummand n ρ = (zeroMult ρ : ℂ) * (((1 - (1 - 1 / (ρ : ℂ)) ^ n).re) : ℂ) := by\n rw [liSummand, summand_conj, Complex.add_conj]\n ring\n\n/-! ### The geometric-sum estimate: |Re(1 − wⁿ)| ≤ 2n²/‖z‖² for w = 1−1/z -/\n\n/-- (1 + 1/(2n))ⁿ ≤ 2 for n ≥ 1. Via (1+x)ⁿ ≤ exp(nx) and exp(1/2) ≤ 2. -/\nlemma pow_one_add_inv_two_mul_le (n : ℕ) (hn : 1 ≤ n) :\n ((1 : ℝ) + 1 / (2 * n)) ^ n ≤ 2 := by\n have hn0 : (0 : ℝ) < n := by exact_mod_cast hn\n have hbase : (1 : ℝ) + 1 / (2 * n) ≤ Real.exp (1 / (2 * n)) :=\n Real.add_one_le_exp _\n have h1 : ((1 : ℝ) + 1 / (2 * n)) ^ n ≤ Real.exp (1 / 2) := by\n calc ((1 : ℝ) + 1 / (2 * n)) ^ n\n ≤ (Real.exp (1 / (2 * n))) ^ n := pow_le_pow_left₀ (by positivity) hbase n\n _ = Real.exp (↑n * (1 / (2 * n))) := by rw [Real.exp_nat_mul]\n _ = Real.exp (1 / 2) := by congr 1; field_simp\n have h2 : Real.exp (1 / 2 : ℝ) ≤ 2 := by\n have h3 : (1 : ℝ) / 2 ≤ Real.log 2 := by\n have h := Real.log_two_gt_d9\n linarith\n calc Real.exp (1 / 2 : ℝ) ≤ Real.exp (Real.log 2) := Real.exp_le_exp.mpr h3\n _ = 2 := Real.exp_log (by norm_num)\n exact h1.trans h2\n\n/-- Key estimate: for n ≥ 1, z with re z ∈ [0,1], 2n ≤ ‖z‖:\n|Re(1 − (1−1/z)ⁿ)| ≤ 2n²/‖z‖². -/\nlemma re_li_summand_le {n : ℕ} (hn : 1 ≤ n) {z : ℂ}\n (hzre0 : 0 ≤ z.re) (hzre1 : z.re ≤ 1) (hz : 2 * n ≤ ‖z‖) :\n |(1 - (1 - 1 / z) ^ n).re| ≤ 2 * n ^ 2 / ‖z‖ ^ 2 := by\n have hn0 : (0 : ℝ) < n := by exact_mod_cast hn\n have hz0 : z ≠ 0 := by\n intro h; rw [h, norm_zero] at hz; linarith\n have hzn : (0 : ℝ) < ‖z‖ := norm_pos_iff.mpr hz0\n have hnsq : Complex.normSq z = ‖z‖ ^ 2 := by\n rw [Complex.normSq_eq_abs, Complex.norm_eq_abs]\n set w : ℂ := 1 - 1 / z with hw\n -- kernel identity: 1 − wⁿ = (1/z)·S, S = Σ_{j<n} w^j\n have hgeom : (w - 1) * ∑ j ∈ Finset.range n, w ^ j = w ^ n - 1 := mul_geom_sum w n\n have hw1 : w - 1 = -(1 / z) := by rw [hw]; ring\n have hf : (1 : ℂ) - w ^ n = (1 / z) * ∑ j ∈ Finset.range n, w ^ j := by\n have h := hgeom\n rw [hw1] at h\n have e := congr_arg Neg.neg h\n simp only [neg_sub, sub_eq_add_neg] at e ⊢\n have e2 : (1 : ℂ) - w ^ n = -(w ^ n - 1) := by ring\n rw [e2, h]; ring\n set S : ℂ := ∑ j ∈ Finset.range n, w ^ j\n have hS : S = (n : ℂ) + (S - n) := by ring\n -- ‖w‖ ≤ 1 + 1/‖z‖\n have hwnorm : ‖w‖ ≤ 1 + 1 / ‖z‖ := by\n have e : w = 1 - z⁻¹ := by rw [hw, div_eq_mul_inv, one_mul]\n rw [e]\n calc ‖(1 : ℂ) - z⁻¹‖ ≤ ‖(1 : ℂ)‖ + ‖z⁻¹‖ := norm_sub_le _ _\n _ = 1 + 1 / ‖z‖ := by rw [norm_one, norm_inv, inv_eq_one_div]\n have h1z : 1 / ‖z‖ ≤ 1 / (2 * n) :=\n one_div_le_one_div_of_le (by positivity) (by exact_mod_cast hz)\n have hwmax : max 1 ‖w‖ ≤ 1 + 1 / (2 * n) := by\n apply max_le (by positivity)\n exact hwnorm.trans (by linarith)\n -- |S − n| ≤ n²/‖z‖\n have hSn : ‖S - n‖ ≤ n ^ 2 / ‖z‖ := by\n have hSn1 : S - n = ∑ j ∈ Finset.range n, (w ^ j - 1) := by\n rw [Finset.sum_sub_distrib]\n simp [Finset.sum_const, Finset.card_range]\n have hbound : ∀ j ∈ Finset.range n,\n ‖w ^ j - 1‖ ≤ (1 / ‖z‖) * (j * (1 + 1 / (2 * n)) ^ (n - 1)) := by\n intro j hj\n have hgeomj : (w - 1) * ∑ i ∈ Finset.range j, w ^ i = w ^ j - 1 := mul_geom_sum w j\n have hjn : j ≤ n := le_of_lt (Finset.mem_range.mp hj)\n have h2 : w ^ j - 1 = -(1 / z) * ∑ i ∈ Finset.range j, w ^ i := by\n have h := hgeomj; rw [hw1] at h\n rw [← h]; ring\n rw [h2, norm_mul, norm_neg, norm_div, norm_one]\n have hsum : ‖∑ i ∈ Finset.range j, w ^ i‖ ≤ j * (1 + 1 / (2 * n)) ^ (n - 1) := by\n calc ‖∑ i ∈ Finset.range j, w ^ i‖\n ≤ ∑ i ∈ Finset.range j, ‖w ^ i‖ := norm_sum_le _ _\n _ ≤ ∑ i ∈ Finset.range j, (1 + 1 / (2 * n)) ^ (n - 1) := by\n apply Finset.sum_le_sum\n intro i hi\n rw [norm_pow]\n have hij : i < j := Finset.mem_range.mp hi\n have h1 : ‖w‖ ^ i ≤ (1 + 1 / (2 * n)) ^ i :=\n pow_le_pow_left₀ (norm_nonneg _)\n (le_trans (le_max_right 1 ‖w‖) hwmax) i\n have h2 : (1 + 1 / (2 * n)) ^ i ≤ (1 + 1 / (2 * n)) ^ (n - 1) := by\n apply pow_le_pow_right₀ (by positivity)\n omega\n exact h1.trans h2\n _ = j * (1 + 1 / (2 * n)) ^ (n - 1) := by\n rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul]\n exact mul_le_mul_of_nonneg_left hsum (by positivity)\n calc ‖∑ j ∈ Finset.range n, (w ^ j - 1)‖\n ≤ ∑ j ∈ Finset.range n, ‖w ^ j - 1‖ := norm_sum_le _ _\n _ ≤ ∑ j ∈ Finset.range n, (1 / ‖z‖) * (j * (1 + 1 / (2 * n)) ^ (n - 1)) :=\n Finset.sum_le_sum hbound\n _ = ((1 / ‖z‖) * (1 + 1 / (2 * n)) ^ (n - 1)) * ∑ j ∈ Finset.range n, j := by\n rw [← Finset.mul_sum]\n apply Finset.sum_congr rfl\n intro j _; ring\n _ ≤ n ^ 2 / ‖z‖ := by\n have hsumj : (∑ j ∈ Finset.range n, j : ℝ) = n * (n - 1) / 2 := by\n have h := Finset.sum_range_id_mul_two n\n have h2 : ((∑ j ∈ Finset.range n, j : ℕ) : ℝ) * 2 = n * (n - 1) := by\n exact_mod_cast h\n linarith\n rw [hsumj]\n have hpow : (1 + 1 / (2 * n : ℝ)) ^ (n - 1) ≤ 2 :=\n le_trans (pow_le_pow_right₀ (by positivity) (Nat.sub_le n 1))\n (pow_one_add_inv_two_mul_le n hn)\n have hb1 : (n : ℝ) * (n - 1) / 2 ≤ n ^ 2 / 2 := by nlinarith [hn0]\n have hb2 : (1 + 1 / (2 * n : ℝ)) ^ (n - 1) * (n * (n - 1) / 2)\n ≤ 2 * (n ^ 2 / 2) :=\n mul_le_mul_of_nonneg hpow hb1 (by positivity) (by positivity)\n have hb3 : ((1 : ℝ) / ‖z‖) * (1 + 1 / (2 * n)) ^ (n - 1) * (n * (n - 1) / 2)\n ≤ (1 / ‖z‖) * (2 * (n ^ 2 / 2)) :=\n mul_le_mul_of_nonneg_left hb2 (by positivity)\n exact hb3.trans (by ring_nf)\n -- Re(f) = n·z.re/‖z‖² + ((S−n)/z).re\n have hre1 : ((n : ℂ) * (1 / z)).re = n * z.re / ‖z‖ ^ 2 := by\n have hinv : ((1 : ℂ) / z).re = z.re / ‖z‖ ^ 2 := by\n rw [one_div, Complex.inv_re, hnsq]\n rw [Complex.mul_re]\n simp [hinv]\n have hfre : (1 - w ^ n).re = n * z.re / ‖z‖ ^ 2 + ((S - n) / z).re := by\n rw [hf, hS, Complex.add_re]\n congr 1\n rw [mul_comm, div_eq_mul_inv]\n exact hre1\n rw [hfre]\n have hA : |n * z.re / ‖z‖ ^ 2| ≤ n / ‖z‖ ^ 2 := by\n rw [abs_div, abs_mul, abs_of_nonneg hn0.le,\n abs_of_nonneg (sq_nonneg ‖z‖)]\n apply (div_le_div_right (by positivity)).mpr\n apply mul_le_mul_of_nonneg_left _ hn0.le\n exact abs_le.mpr ⟨hzre0, hzre1⟩\n have hB : |((S - n) / z).re| ≤ n ^ 2 / ‖z‖ ^ 2 := by\n have h1 : |((S - n) / z).re| ≤ ‖(S - n) / z‖ := Complex.abs_re_le_norm _\n have h2 : ‖(S - n) / z‖ ≤ (n ^ 2 / ‖z‖) / ‖z‖ := by\n rw [norm_div]\n exact (div_le_div_right hzn).mpr hSn\n exact h1.trans (h2.trans (by rw [div_div, ← pow_two]))\n have hnn : (n : ℝ) ≤ n ^ 2 := by\n have h : (1 : ℝ) ≤ n := by exact_mod_cast hn\n nlinarith\n calc |n * z.re / ‖z‖ ^ 2 + ((S - n) / z).re|\n ≤ n / ‖z‖ ^ 2 + n ^ 2 / ‖z‖ ^ 2 := (abs_add _ _).trans (add_le_add hA hB)\n _ = (n + n ^ 2) / ‖z‖ ^ 2 := by ring\n _ ≤ 2 * n ^ 2 / ‖z‖ ^ 2 := by\n apply (div_le_div_right (by positivity)).mpr\n linarith\n\nend NguyenRH1\n"},"extra_content":null}]