← Session 29 — ii′-5e-v: circle bound (far-tail + series bounds)
thinking (9963 chars)
3c-i committed (d2bfde6). Now 3c-ii: the three dyadic shells (inlo, inhi, up).
Let me write shell_inlo fully as the template:
```lean
/-- **The inner-low shell** (3 < ‖ρ‖ ≤ R/2): at most 60·A₀·(log R)². -/
lemma shell_inlo {s : ℂ} {R : ℝ} (hs : ‖s‖ = R) (hsz : ¬ IsNontrivialZero s)
(hR : (16002 : ℝ) ≤ R) :
∑ ρ ∈ (circleZeros R).filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>
¬ ‖(ρ : ℂ)‖ ≤ 3 ∧ ‖(ρ : ℂ)‖ ≤ R / 2), ‖seriesTerm s ρ‖
≤ 60 * A0count * (Real.log R) ^ 2 := by
have hRpos : (0 : ℝ) < R := by linarith [hR]
have hlogR : (9 : ℝ) ≤ Real.log R := nine_le_log_of_16002_le hR
set J := Nat.log 2 ⌊R⌋₊ with hJ
have hJle : (J : ℝ) ≤ 2 * Real.log R := Nat.log_floor_two_le hR
set FS := (circleZeros R).filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>
¬ ‖(ρ : ℂ)‖ ≤ 3 ∧ ‖(ρ : ℂ)‖ ≤ R / 2) with hFS
-- the per-element dyadic-class range
have hdj : ∀ ρ ∈ FS, 1 ≤ Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊ ∧ Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊ ≤ J := by
intro ρ hρ
rw [hFS, Finset.mem_filter] at hρ
obtain ⟨-, hρ3, hρR2⟩ := hρ
have hρ3' : (3 : ℝ) < ‖(ρ : ℂ)‖ := lt_of_not_le hρ3
have hfl3 : (3 : ℕ) ≤ ⌊‖(ρ : ℂ)‖⌋₊ := by
rw [Nat.le_floor_iff (by linarith : (0 : ℝ) ≤ 3)]
exact hρ3'.le -- hmm Nat.le_floor_iff : n ≤ ⌊x⌋₊ ↔ (n:ℝ) ≤ x: 3 ≤ ⌊‖ρ‖⌋₊ ⟺ (3:ℝ) ≤ ‖ρ‖ ✓ (hρ3'.le : 3 ≤ ‖ρ‖)
have h1 : (1 : ℕ) ≤ Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊ := by
have h2 := Nat.log_mono_right (b := 2) hfl3 -- Nat.log 2 3 ≤ Nat.log 2 ⌊‖ρ‖⌋₊
have h3 : Nat.log 2 3 = 1 := by norm_num -- log₂3 = 1
rw [h3] at h2
exact h2
have h2 : Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊ ≤ J := by
apply Nat.log_mono_right (b := 2)
apply Nat.floor_mono -- ⌊‖ρ‖⌋₊ ≤ ⌊R⌋₊: ‖ρ‖ ≤ R/2 ≤ R ✓
linarith [hρR2, hR]
exact ⟨h1, h2⟩
...
```
Hmm wait — Nat.log_mono_right : n ≤ m → Nat.log b n ≤ Nat.log b m ✓. Nat.log 2 3 = 1: log₂3: 2^1 = 2 ≤ 3 < 4 = 2^2 ✓ = 1: by decide or norm_num ✓. Nat.floor_mono : x ≤ y → ⌊x⌋₊ ≤ ⌊y⌋₊ ✓.
- the term bound:
```
have hterm : ∀ ρ ∈ FS, ‖seriesTerm s ρ‖
≤ 2 * (zeroMult (ρ : ℂ) : ℝ) / (2 : ℝ) ^ (Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊) := by
intro ρ hρ
rw [hFS, Finset.mem_filter] at hρ
obtain ⟨-, hρ3, hρR2⟩ := hρ
have hρ3' : (3 : ℝ) < ‖(ρ : ℂ)‖ := lt_of_not_le hρ3
-- 2^{jf} ≤ ‖ρ‖
have hpowle : (2 : ℝ) ^ (Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊) ≤ ‖(ρ : ℂ)‖ := by
have hfl : ⌊‖(ρ : ℂ)‖⌋₊ ≠ 0 := by
rw [Ne, Nat.floor_eq_zero]; push Not; linarith [hρ3']
have h1 := Nat.pow_log_le_self 2 hfl
have h2 : ((2 ^ Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊ : ℕ) : ℝ) ≤ (⌊‖(ρ : ℂ)‖⌋₊ : ℝ) := by exact_mod_cast h1
have h3 : ((2 ^ Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊ : ℕ) : ℝ)
= (2 : ℝ) ^ (Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊) := by push_cast; ring
rw [h3] at h2
have h4 : (⌊‖(ρ : ℂ)‖⌋₊ : ℝ) ≤ ‖(ρ : ℂ)‖ := Nat.floor_le (norm_nonneg _)
linarith [h2, h4]
-- ‖s−ρ‖ ≥ R/2
have hsr : R / 2 ≤ ‖s - (ρ : ℂ)‖ := by
have h := abs_norm_sub_norm_le s (ρ : ℂ)
rw [hs, abs_of_nonneg (by linarith [hR, hρR2] : (0 : ℝ) ≤ R - ‖(ρ : ℂ)‖)] at h
linarith [h, hρR2]
have hρpos : (0 : ℝ) < ‖(ρ : ℂ)‖ := by linarith [hρ3']
have hsrpos : (0 : ℝ) < ‖s - (ρ : ℂ)‖ := by linarith [hsr, hR]
have hid := seriesTerm_norm_eq_div hs hsz ρ
rw [hid]
have hm : (0 : ℝ) ≤ (zeroMult (ρ : ℂ) : ℝ) := Nat.cast_nonneg _
-- m·R/(‖ρ‖‖s−ρ‖) ≤ m·R/(‖ρ‖·(R/2)) = 2m/‖ρ‖ ≤ 2m/2^{jf}
have h1 : R / (‖(ρ : ℂ)‖ * ‖s - (ρ : ℂ)‖) ≤ R / (‖(ρ : ℂ)‖ * (R / 2)) := by
apply div_le_div_of_nonneg_left hRpos.le (mul_pos hρpos (by linarith [hR]))
exact mul_le_mul_of_nonneg_left hsr hρpos.le
have h2 : R / (‖(ρ : ℂ)‖ * (R / 2)) = 2 / ‖(ρ : ℂ)‖ := by
field_simp
ring
have h3 : 2 / ‖(ρ : ℂ)‖ ≤ 2 / (2 : ℝ) ^ (Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊) := by
apply div_le_div_of_nonneg_left (by norm_num : (0 : ℝ) ≤ 2)
(by positivity)
exact hpowle
calc (zeroMult (ρ : ℂ) : ℝ) * (R / (‖(ρ : ℂ)‖ * ‖s - (ρ : ℂ)‖))
≤ (zeroMult (ρ : ℂ) : ℝ) * (R / (‖(ρ : ℂ)‖ * (R / 2))) :=
mul_le_mul_of_nonneg_left h1 hm
_ = (zeroMult (ρ : ℂ) : ℝ) * (2 / ‖(ρ : ℂ)‖) := by rw [h2]
_ ≤ (zeroMult (ρ : ℂ) : ℝ) * (2 / (2 : ℝ) ^ (Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊)) :=
mul_le_mul_of_nonneg_left h3 hm
_ = 2 * (zeroMult (ρ : ℂ) : ℝ) / (2 : ℝ) ^ (Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊) := by ring
```
Careful with h2: R/(‖ρ‖·(R/2)): field_simp gives 2/(‖ρ‖)·... R/(‖ρ‖·(R/2)) = R·2/(‖ρ‖·R) = 2/‖ρ‖ — field_simp; ring. ✓
- the count:
```
have hcount : ∀ j : ℕ, ∑ ρ ∈ FS.filter (fun ρ => Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊ = j),
(zeroMult (ρ : ℂ) : ℝ)
≤ 3 * A0count * ((2 : ℝ) ^ j + 3) * Real.log (3 * max |(2 : ℝ) ^ j - 1| |(2 : ℝ) ^ (j + 1)| + 5) := by
intro j
by_cases hj : j ∈ Finset.Ico 1 (J + 1)
· rw [Finset.mem_Ico] at hj
have hj1 : (1 : ℝ) ≤ (2 : ℝ) ^ j := by
exact_mod_cast Nat.one_le_two_pow
have hj2 : (2 : ℝ) ≤ (2 : ℝ) ^ j := by
have h1 : (2 : ℝ) ^ 1 ≤ (2 : ℝ) ^ j := pow_le_pow_right₀ (by norm_num) (by omega : 1 ≤ j)
linarith [h1]
apply sum_zeroMult_le_of_im_band
...
```
Wait — hcount's statement in dyadic_family_le has the filter lambda `fun ρ => Nat.log 2 ⌊d ρ⌋₊ = j` — with d := fun ρ => ‖(ρ:ℂ)‖ — the lambda there: `fun ρ => Nat.log 2 ⌊‖(ρ:ℂ)‖⌋₊ = j` — the coercion again!! Banked gotcha: pin the binder: `fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => ...`. Hmm — but in dyadic_family_le the filter lambdas are `fun ρ => Nat.log 2 ⌊d ρ⌋₊ = j` — d application pins ρ to the subtype ✓ no coercion issue THERE. But when I INSTANTIATE d := fun ρ => ‖(ρ:ℂ)‖ and write hcount's filter as `FS.filter (fun ρ => Nat.log 2 ⌊‖(ρ:ℂ)‖⌋₊ = j)`, the elaborator must see the filter lambdas as SYNTACTICALLY equal: dyadic_family_le's internal filter is on `fun ρ => Nat.log 2 ⌊d ρ⌋₊ = j` with d substituted — `⌊d ρ⌋₊` = `⌊(fun ρ => ‖(ρ:ℂ)‖) ρ⌋₊` = beta `⌊‖(ρ:ℂ)‖⌋₊` — should be defeq, but for the hcount hypothesis application the elaborator needs to unify the filter sets — with `classical` and defeq it should work if I state hcount's lambda identically: `fun ρ => Nat.log 2 ⌊(fun ρ => ‖(ρ:ℂ)‖) ρ⌋₊ = j`... The application `dyadic_family_le FS (fun ρ => ‖(ρ:ℂ)‖) J _ 2 cnt hC1 hdj hterm hcount` — the hcount's expected type: ∀ j, ∑ ρ ∈ FS.filter (fun ρ => Nat.log 2 ⌊(d) ρ⌋₊ = j), ... ≤ cnt j with d := the lambda — beta-reduced during unification ✓ my stated hcount uses ⌊‖(ρ:ℂ)‖⌋₊ directly — defeq ✓. BUT the lambda binder ambiguity strikes again: in MY hcount statement `fun ρ => Nat.log 2 ⌊‖(ρ:ℂ)‖⌋₊ = j` — the coercion ‖(ρ:ℂ)‖ — the expected type from dyadic_family_le's unification pins ρ : subtype ✓ — since hcount is APPLIED to a known expected type, elaboration is fine. But if hcount is a standalone `have` with ascribed type, I must pin the binder: `fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => ...` — then unification with the expected type needs defeq between `fun ρ : ST => Nat.log 2 ⌊‖(ρ:ℂ)‖⌋₊ = j` and `fun ρ => Nat.log 2 ⌊d ρ⌋₊ = j` — beta + coe ✓ fine.
The brick application per j (with hj : j ∈ Ico): a := 2^j−1, b := 2^{j+1}, c := 2^j−1:
- hM1 : 1 ≤ max (2^j−1) (2^j−1) = 2^j−1 ⟺ 2 ≤ 2^j ⟺ j ≥ 1 ✓.
- hMb : max ... = 2^j−1 ≤ 2^{j+1} ✓.
- hsub : ∀ ρ ∈ FS.filter (jf · = j), a ≤ |γ| ∧ |γ| ≤ b ∧ c ≤ |γ|:
per element: jf ρ = j ⟹ 2^j ≤ ‖ρ‖ (as before) and ‖ρ‖ < 2^{j+1} (Nat.lt_pow_succ_log_self + floor+1):
```
have hup : ‖(ρ:ℂ)‖ < (2:ℝ)^(j+1) := by
have h1 : ⌊‖(ρ:ℂ)‖⌋₊ < 2 ^ (Nat.log 2 ⌊‖(ρ:ℂ)‖⌋₊ + 1) := Nat.lt_pow_succ_log_self (by norm_num) _
rw [hρj] at h1 -- hρj : Nat.log 2 ⌊‖ρ‖⌋₊ = j
have h2 : ⌊‖(ρ:ℂ)‖⌋₊ + 1 ≤ 2 ^ (j + 1) := h1
have h3 : ‖(ρ:ℂ)‖ < (⌊‖(ρ:ℂ)‖⌋₊ : ℝ) + 1 := Nat.lt_floor_add_one _
have h4 : ((⌊‖(ρ:ℂ)‖⌋₊ + 1 : ℕ) : ℝ) ≤ ((2 ^ (j + 1) : ℕ) : ℝ) := by exact_mod_cast h2
push_cast at h4
-- h4 : (⌊‖ρ‖⌋₊ : ℝ) + 1 ≤ (2:ℝ)^(j+1)
linarith [h3, h4]
```
hmm h4's cast: ((2^(j+1) : ℕ) : ℝ) = (2:ℝ)^(j+1): push_cast at h4 gives (⌊‖ρ‖⌋₊:ℝ)+1 ≤ (2:ℝ)^(j+1) ✓.
Then: |γ| ≥ ‖ρ‖−1 ≥ 2^j−1 = a ✓ (abs_im_ge_norm_sub_one); |γ| ≤ ‖ρ‖ ≤ ... ‖ρ‖ < 2^{j+1} ⟹ ‖ρ‖ ≤ 2^{j+1} = b: |γ| ≤ ‖ρ‖ — wait |γ| = |im ρ| ≤ ‖ρ‖ (abs_im_le_norm) ✓ then ≤ b via hup.le.
- The brick then gives ≤ 3·A₀·(b−a+2)·log(3·max|a||b|+5): b−a+2 = 2^{j+1}−(2^j−1)+2 = 2^j+3: need a ring identity with the pow: 2^{j+1} = 2·2^j (pow_succ'). max|a||b| = max|2^j−1||2^{j+1}|: |2^j−1| = 2^j−1 (≥ 1 > 0: j ≥ 1 hmm 2^j−1 ≥ 1 ✓); |2^{j+1}| = 2^{j+1}: max = 2^{j+1} (2^j−1 ≤ 2^{j+1} ✓).
So cnt j := 3 * A0count * ((2:ℝ)^j + 3) * Real.log (3 * (2:ℝ)^(j+1) + 5).
Then per-j uniform bound: (C₁/2^j)·cnt j = (2/2^j)·3A₀(2^j+3)·log(3·2^{j+1}+5) ≤ 30·A₀·L:
- log(3·2^{j+1}+5) ≤ 2L: via log_three_le_two_log with x := 2^{j+1}: 0 ≤ x ✓; x ≤ 3R: 2^{j+1} ≤ 2R (j ≤ J: 2^j ≤ 2^J ≤ R ⟹ 2^{j+1} ≤ 2R ≤ 3R ✓ — 2^j ≤ 2^J: pow_le_pow_right₀ (1≤2) (j ≤ J); 2^J ≤ R from Nat.log_floor_two_le's internals — hmm I need (2:ℝ)^J ≤ R as a standalone. Nat.log_floor_two_le gives J ≤ 2L but not 2^J ≤ R. Add a tiny lemma or inline: (2:ℝ)^J ≤ R: Nat.pow_log_le_self + floor_le as in the term bound. Make a lemma `two_pow_log_floor_le (hR : 16002 ≤ R) : (2:ℝ)^(Nat.log 2 ⌊R⌋₊) ≤ R`.)
- (2/2^j)·3A₀(2^j+3)·2L = 12·A₀·L·(2^j+3)/2^j = 12A₀L(1 + 3/2^j) ≤ 12A₀L(1+3/2) = 30A₀L (2^j ≥ 2 ⟹ 3/2^j ≤ 3/2: div_le_div_of_nonneg_left... (3:ℝ)/2^j ≤ 3/2 ⟸ 2^j ≥ 2, via div_le_div_of_nonneg_left (3≥0) (0<2) (2 ≤ 2^j): gives 3/2^j ≤ 3/2 ✓).
- Σ_{j∈Ico 1 (J+1)} 30A₀L = J·30A₀L (sum_const, card Ico = J) ≤ 2L·30A₀L = 60A₀L² ✓.
Final: shell_inlo ≤ 60·A₀·L².
Structure per shell lemma ~150 lines. Three of them + crit + assembly — the remaining big push. Let me write shell_inlo now and compile before cloning the pattern.
Also — for the final assembly I need the shell bounds in terms of the filter-normal forms from the iterated split: the assembly's second shell is (F.filter ¬P1).filter P2 = F.filter (¬P1 ∧ P2) via Finset.filter_filter. I'll state shell_inlo's finset as F.filter (fun ρ => ¬‖ρ‖ ≤ 3 ∧ ‖ρ‖ ≤ R/2) — and in the assembly use filter_filter to match. ✓ (P1 := ‖ρ‖ ≤ 3, ¬P1 = ¬‖ρ‖ ≤ 3 ✓.)
Let me write shell_inlo.
3c-i committed. Now shell_inlo (the template for the dyadic shells).
tool: Edit
input
{
"replace_all": false,
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiCircleBound.lean",
"old_string": "end NguyenRH1\n\nend",
"new_string": "/-! ## 8. The three dyadic shells (5e-v-b chunk 3c-ii)\n\n`two_pow_log_floor_le`: (2:\u211d)^J \u2264 R. `shell_inlo` (3 < \u2016\u03c1\u2016 \u2264 R/2),\n`shell_inhi` (R/2 < \u2016\u03c1\u2016 \u2264 R\u22122), `shell_up` (R+2 \u2264 \u2016\u03c1\u2016 within the\nfinite part): dyadic in \u2016\u03c1\u2016 / R\u2212\u2016\u03c1\u2016 / \u2016\u03c1\u2016\u2212R respectively, per-fiber\ncount via the brick, uniform log bound \u2264 2\u00b7log R. Each \u2264\n60/60/30\u00b7A\u2080\u00b7(log R)\u00b2. -/\n\n/-- (2:\u211d)^J \u2264 R for J = Nat.log 2 \u230aR\u230b\u208a, R \u2265 16002. -/\nlemma two_pow_log_floor_le {R : \u211d} (hR : (16002 : \u211d) \u2264 R) :\n (2 : \u211d) ^ (Nat.log 2 \u230aR\u230b\u208a) \u2264 R := by\n have hfl : \u230aR\u230b\u208a \u2260 0 := by\n rw [Ne, Nat.floor_eq_zero]\n push Not\n linarith\n have h2 := Nat.pow_log_le_self 2 hfl\n have h3 : ((2 ^ Nat.log 2 \u230aR\u230b\u208a : \u2115) : \u211d) \u2264 (\u230aR\u230b\u208a : \u211d) := by exact_mod_cast h2\n have h4 : (\u230aR\u230b\u208a : \u211d) \u2264 R := Nat.floor_le (by linarith [hR])\n have h5 : ((2 ^ Nat.log 2 \u230aR\u230b\u208a : \u2115) : \u211d) = (2 : \u211d) ^ Nat.log 2 \u230aR\u230b\u208a := by\n push_cast\n ring\n rw [h5] at h3\n linarith [h3, h4]\n\n/-- **The inner-low shell** (3 < \u2016\u03c1\u2016 \u2264 R/2): \u2264 60\u00b7A\u2080\u00b7(log R)\u00b2. -/\nlemma shell_inlo {s : \u2102} {R : \u211d} (hs : \u2016s\u2016 = R) (hsz : \u00ac IsNontrivialZero s)\n (hR : (16002 : \u211d) \u2264 R) :\n \u2211 \u03c1 \u2208 (circleZeros R).filter (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} =>\n \u00ac \u2016(\u03c1 : \u2102)\u2016 \u2264 3 \u2227 \u2016(\u03c1 : \u2102)\u2016 \u2264 R / 2), \u2016seriesTerm s \u03c1\u2016\n \u2264 60 * A0count * (Real.log R) ^ 2 := by\n classical\n have hRpos : (0 : \u211d) < R := by linarith [hR]\n have hlogR : (9 : \u211d) \u2264 Real.log R := nine_le_log_of_16002_le hR\n have hlogRnn : (0 : \u211d) \u2264 Real.log R := by linarith [hlogR]\n set J := Nat.log 2 \u230aR\u230b\u208a with hJ\n have hJle : (J : \u211d) \u2264 2 * Real.log R := Nat.log_floor_two_le hR\n have h2JR : (2 : \u211d) ^ J \u2264 R := two_pow_log_floor_le hR\n set FS := (circleZeros R).filter (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} =>\n \u00ac \u2016(\u03c1 : \u2102)\u2016 \u2264 3 \u2227 \u2016(\u03c1 : \u2102)\u2016 \u2264 R / 2) with hFS\n have hdj : \u2200 \u03c1 \u2208 FS, 1 \u2264 Nat.log 2 \u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a \u2227 Nat.log 2 \u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a \u2264 J := by\n intro \u03c1 h\u03c1\n rw [hFS, Finset.mem_filter] at h\u03c1\n obtain \u27e8-, h\u03c13, h\u03c1R2\u27e9 := h\u03c1\n have h\u03c13' : (3 : \u211d) < \u2016(\u03c1 : \u2102)\u2016 := lt_of_not_le h\u03c13\n have hfl3 : (3 : \u2115) \u2264 \u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a := by\n rw [Nat.le_floor_iff (by norm_num : (0 : \u211d) \u2264 3)]\n exact h\u03c13'.le\n have h1 : (1 : \u2115) \u2264 Nat.log 2 \u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a := by\n have h2 := Nat.log_mono_right (b := 2) hfl3\n have h3 : Nat.log 2 3 = 1 := by decide\n rw [h3] at h2\n exact h2\n have h2 : Nat.log 2 \u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a \u2264 J := by\n apply Nat.log_mono_right (b := 2)\n apply Nat.floor_mono\n linarith [h\u03c1R2, hR]\n exact \u27e8h1, h2\u27e9\n have hterm : \u2200 \u03c1 \u2208 FS, \u2016seriesTerm s \u03c1\u2016\n \u2264 2 * (zeroMult (\u03c1 : \u2102) : \u211d) / (2 : \u211d) ^ (Nat.log 2 \u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a) := by\n intro \u03c1 h\u03c1\n rw [hFS, Finset.mem_filter] at h\u03c1\n obtain \u27e8-, h\u03c13, h\u03c1R2\u27e9 := h\u03c1\n have h\u03c13' : (3 : \u211d) < \u2016(\u03c1 : \u2102)\u2016 := lt_of_not_le h\u03c13\n have hpowle : (2 : \u211d) ^ (Nat.log 2 \u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a) \u2264 \u2016(\u03c1 : \u2102)\u2016 := by\n have hfl : \u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a \u2260 0 := by\n rw [Ne, Nat.floor_eq_zero]\n push Not\n linarith [h\u03c13']\n have h1 := Nat.pow_log_le_self 2 hfl\n have h2 : ((2 ^ Nat.log 2 \u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a : \u2115) : \u211d) \u2264 (\u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a : \u211d) := by\n exact_mod_cast h1\n have h3 : ((2 ^ Nat.log 2 \u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a : \u2115) : \u211d)\n = (2 : \u211d) ^ (Nat.log 2 \u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a) := by\n push_cast\n ring\n rw [h3] at h2\n have h4 : (\u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a : \u211d) \u2264 \u2016(\u03c1 : \u2102)\u2016 := Nat.floor_le (norm_nonneg _)\n linarith [h2, h4]\n have hsr : R / 2 \u2264 \u2016s - (\u03c1 : \u2102)\u2016 := by\n have h := abs_norm_sub_norm_le s (\u03c1 : \u2102)\n rw [hs, abs_of_nonneg (by linarith [hR, h\u03c1R2] : (0 : \u211d) \u2264 R - \u2016(\u03c1 : \u2102)\u2016)] at h\n linarith [h, h\u03c1R2]\n have h\u03c1pos : (0 : \u211d) < \u2016(\u03c1 : \u2102)\u2016 := by linarith [h\u03c13']\n have hsrpos : (0 : \u211d) < \u2016s - (\u03c1 : \u2102)\u2016 := by linarith [hsr, hR]\n have hid := seriesTerm_norm_eq_div hs hsz \u03c1\n rw [hid]\n have hm : (0 : \u211d) \u2264 (zeroMult (\u03c1 : \u2102) : \u211d) := Nat.cast_nonneg _\n have h1 : R / (\u2016(\u03c1 : \u2102)\u2016 * \u2016s - (\u03c1 : \u2102)\u2016) \u2264 R / (\u2016(\u03c1 : \u2102)\u2016 * (R / 2)) := by\n apply div_le_div_of_nonneg_left hRpos.le (mul_pos h\u03c1pos (by linarith [hR]))\n exact mul_le_mul_of_nonneg_left hsr h\u03c1pos.le\n have h2 : R / (\u2016(\u03c1 : \u2102)\u2016 * (R / 2)) = 2 / \u2016(\u03c1 : \u2102)\u2016 := by\n field_simp\n ring\n have h3 : (2 : \u211d) / \u2016(\u03c1 : \u2102)\u2016 \u2264 2 / (2 : \u211d) ^ (Nat.log 2 \u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a) := by\n apply div_le_div_of_nonneg_left (by norm_num : (0 : \u211d) \u2264 2) (by positivity)\n exact hpowle\n calc (zeroMult (\u03c1 : \u2102) : \u211d) * (R / (\u2016(\u03c1 : \u2102)\u2016 * \u2016s - (\u03c1 : \u2102)\u2016))\n \u2264 (zeroMult (\u03c1 : \u2102) : \u211d) * (R / (\u2016(\u03c1 : \u2102)\u2016 * (R / 2))) :=\n mul_le_mul_of_nonneg_left h1 hm\n _ = (zeroMult (\u03c1 : \u2102) : \u211d) * (2 / \u2016(\u03c1 : \u2102)\u2016) := by rw [h2]\n _ \u2264 (zeroMult (\u03c1 : \u2102) : \u211d) * (2 / (2 : \u211d) ^ (Nat.log 2 \u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a)) :=\n mul_le_mul_of_nonneg_left h3 hm\n _ = 2 * (zeroMult (\u03c1 : \u2102) : \u211d) / (2 : \u211d) ^ (Nat.log 2 \u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a) := by ring\n have hcount : \u2200 j : \u2115,\n \u2211 \u03c1 \u2208 FS.filter (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} =>\n Nat.log 2 \u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a = j), (zeroMult (\u03c1 : \u2102) : \u211d)\n \u2264 3 * A0count * ((2 : \u211d) ^ j + 3) * Real.log (3 * (2 : \u211d) ^ (j + 1) + 5) := by\n intro j\n by_cases hj : j \u2208 Finset.Ico 1 (J + 1)\n \u00b7 rw [Finset.mem_Ico] at hj\n have hj2 : (2 : \u211d) \u2264 (2 : \u211d) ^ j := by\n have h1 : (2 : \u211d) ^ 1 \u2264 (2 : \u211d) ^ j :=\n pow_le_pow_right\u2080 (by norm_num) (by omega : 1 \u2264 j)\n linarith [h1]\n have hM1 : (1 : \u211d) \u2264 max ((2 : \u211d) ^ j - 1) ((2 : \u211d) ^ j - 1) := by\n rw [max_self]\n linarith [hj2]\n have hMb : max ((2 : \u211d) ^ j - 1) ((2 : \u211d) ^ j - 1) \u2264 (2 : \u211d) ^ (j + 1) := by\n rw [max_self]\n have h1 : (2 : \u211d) ^ (j + 1) = 2 * (2 : \u211d) ^ j := by rw [pow_succ']\n linarith [hj2]\n have hsub : \u2200 \u03c1 \u2208 FS.filter (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} =>\n Nat.log 2 \u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a = j),\n (2 : \u211d) ^ j - 1 \u2264 |(\u03c1 : \u2102).im| \u2227 |(\u03c1 : \u2102).im| \u2264 (2 : \u211d) ^ (j + 1) \u2227\n (2 : \u211d) ^ j - 1 \u2264 |(\u03c1 : \u2102).im| := by\n intro \u03c1 h\u03c1\n rw [Finset.mem_filter] at h\u03c1\n obtain \u27e8h\u03c1F, h\u03c1j\u27e9 := h\u03c1\n have hpowle : (2 : \u211d) ^ j \u2264 \u2016(\u03c1 : \u2102)\u2016 := by\n have hfl : \u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a \u2260 0 := by\n rw [Ne, Nat.floor_eq_zero]\n push Not\n rw [hFS, Finset.mem_filter] at h\u03c1F\n have h\u03c13' : (3 : \u211d) < \u2016(\u03c1 : \u2102)\u2016 := lt_of_not_le h\u03c1F.2.1\n linarith [h\u03c13']\n have h1 := Nat.pow_log_le_self 2 hfl\n rw [\u2190 h\u03c1j] at h1\n have h2 : ((2 ^ j : \u2115) : \u211d) \u2264 (\u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a : \u211d) := by exact_mod_cast h1\n have h3 : ((2 ^ j : \u2115) : \u211d) = (2 : \u211d) ^ j := by push_cast; ring\n rw [h3] at h2\n have h4 : (\u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a : \u211d) \u2264 \u2016(\u03c1 : \u2102)\u2016 := Nat.floor_le (norm_nonneg _)\n linarith [h2, h4]\n have hpowup : \u2016(\u03c1 : \u2102)\u2016 < (2 : \u211d) ^ (j + 1) := by\n have h1 : \u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a < 2 ^ (Nat.log 2 \u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a + 1) :=\n Nat.lt_pow_succ_log_self (by norm_num) _\n rw [h\u03c1j] at h1\n have h2 : \u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a + 1 \u2264 2 ^ (j + 1) := h1\n have h3 : \u2016(\u03c1 : \u2102)\u2016 < (\u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a : \u211d) + 1 := Nat.lt_floor_add_one _\n have h4 : ((\u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a + 1 : \u2115) : \u211d) \u2264 ((2 ^ (j + 1) : \u2115) : \u211d) := by\n exact_mod_cast h2\n have h5 : ((2 ^ (j + 1) : \u2115) : \u211d) = (2 : \u211d) ^ (j + 1) := by push_cast; ring\n rw [h5] at h4\n push_cast at h4\n linarith [h3, h4]\n have him1 := abs_im_ge_norm_sub_one \u03c1\n have him2 : |(\u03c1 : \u2102).im| \u2264 \u2016(\u03c1 : \u2102)\u2016 := abs_im_le_norm _\n exact \u27e8by linarith [him1, hpowle], by linarith [him2, hpowup],\n by linarith [him1, hpowle]\u27e9\n have hbrick := sum_zeroMult_le_of_im_band\n (FS.filter (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => Nat.log 2 \u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a = j))\n hM1 hMb hsub\n have hab : (2 : \u211d) ^ (j + 1) - ((2 : \u211d) ^ j - 1) + 2 = (2 : \u211d) ^ j + 3 := by\n have h1 : (2 : \u211d) ^ (j + 1) = 2 * (2 : \u211d) ^ j := by rw [pow_succ']\n linarith [h1]\n have hmax : max |(2 : \u211d) ^ j - 1| |(2 : \u211d) ^ (j + 1)| = (2 : \u211d) ^ (j + 1) := by\n have h1 : |(2 : \u211d) ^ (j + 1)| = (2 : \u211d) ^ (j + 1) := abs_of_nonneg (by positivity)\n have h2 : |(2 : \u211d) ^ j - 1| = (2 : \u211d) ^ j - 1 := abs_of_nonneg (by linarith [hj2])\n rw [h1, h2]\n have h3 : (2 : \u211d) ^ (j + 1) = 2 * (2 : \u211d) ^ j := by rw [pow_succ']\n have h4 : (0 : \u211d) < (2 : \u211d) ^ j := by positivity\n nlinarith [h3, h4]\n rw [hab, hmax] at hbrick\n exact hbrick\n \u00b7 have hempty : FS.filter (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} =>\n Nat.log 2 \u230a\u2016(\u03c1 : \u2102)\u2016\u230b\u208a = j) = \u2205 := by\n apply Finset.eq_empty_iff_forall_not_mem.mpr\n intro \u03c1 h\u03c1\n rw [Finset.mem_filter] at h\u03c1\n obtain \u27e8h\u03c1F, h\u03c1j\u27e9 := h\u03c1\n have hdj\u03c1 := hdj \u03c1 h\u03c1F\n rw [h\u03c1j] at hdj\u03c1\n rw [Finset.mem_Ico] at hj\n omega\n rw [hempty, Finset.sum_empty]\n have h1 : (0 : \u211d) \u2264 Real.log (3 * (2 : \u211d) ^ (j + 1) + 5) := by\n apply Real.log_nonneg\n have h2 : (0 : \u211d) < (2 : \u211d) ^ (j + 1) := by positivity\n linarith [h2]\n exact mul_nonneg (mul_nonneg (by norm_num) A0count_pos.le (by positivity)) h1\n -- the closed-form per-shell bound\n have hper : \u2200 j \u2208 Finset.Ico 1 (J + 1),\n (2 / (2 : \u211d) ^ j) * (3 * A0count * ((2 : \u211d) ^ j + 3) *\n Real.log (3 * (2 : \u211d) ^ (j + 1) + 5))\n \u2264 30 * A0count * Real.log R := by\n intro j hj\n rw [Finset.mem_Ico] at hj\n have h2j0 : (0 : \u211d) < (2 : \u211d) ^ j := by positivity\n have hj2 : (2 : \u211d) \u2264 (2 : \u211d) ^ j := by\n have h1 : (2 : \u211d) ^ 1 \u2264 (2 : \u211d) ^ j :=\n pow_le_pow_right\u2080 (by norm_num) (by omega : 1 \u2264 j)\n linarith [h1]\n have hlogle : Real.log (3 * (2 : \u211d) ^ (j + 1) + 5) \u2264 2 * Real.log R := by\n apply log_three_le_two_log hR (by positivity)\n have h1 : (2 : \u211d) ^ (j + 1) = 2 * (2 : \u211d) ^ j := by rw [pow_succ']\n have h2 : (2 : \u211d) ^ j \u2264 (2 : \u211d) ^ J := pow_le_pow_right\u2080 (by norm_num) (by omega : j \u2264 J)\n nlinarith [h1, h2, h2JR, hR]\n have hA0 := A0count_pos.le\n have h1 : (2 / (2 : \u211d) ^ j) * (3 * A0count * ((2 : \u211d) ^ j + 3) *\n Real.log (3 * (2 : \u211d) ^ (j + 1) + 5))\n = 6 * A0count * Real.log (3 * (2 : \u211d) ^ (j + 1) + 5) * (1 + 3 / (2 : \u211d) ^ j) := by\n field_simp\n ring\n rw [h1]\n have h2 : 3 / (2 : \u211d) ^ j \u2264 3 / 2 := by\n apply div_le_div_of_nonneg_left (by norm_num : (0 : \u211d) \u2264 3) (by norm_num) hj2\n have hlognn : (0 : \u211d) \u2264 Real.log (3 * (2 : \u211d) ^ (j + 1) + 5) := by\n apply Real.log_nonneg\n have h3 : (0 : \u211d) < (2 : \u211d) ^ (j + 1) := by positivity\n linarith [h3]\n nlinarith [hlogle, h2, hlognn, hA0, hlogRnn]\n -- assembly via dyadic_family_le\n have hmain := dyadic_family_le FS (fun \u03c1 => \u2016(\u03c1 : \u2102)\u2016) J\n (fun \u03c1 => \u2016seriesTerm s \u03c1\u2016) 2\n (fun j => 3 * A0count * ((2 : \u211d) ^ j + 3) * Real.log (3 * (2 : \u211d) ^ (j + 1) + 5))\n (by norm_num) hdj hterm hcount\n calc \u2211 \u03c1 \u2208 FS, \u2016seriesTerm s \u03c1\u2016\n \u2264 \u2211 j \u2208 Finset.Ico 1 (J + 1), (2 / (2 : \u211d) ^ j) *\n (3 * A0count * ((2 : \u211d) ^ j + 3) * Real.log (3 * (2 : \u211d) ^ (j + 1) + 5)) := hmain\n _ \u2264 \u2211 j \u2208 Finset.Ico 1 (J + 1), 30 * A0count * Real.log R := Finset.sum_le_sum hper\n _ = (J : \u211d) * (30 * A0count * Real.log R) := by\n rw [Finset.sum_const, Nat.card_Ico, Nat.add_sub_cancel, nsmul_eq_mul]\n _ \u2264 60 * A0count * (Real.log R) ^ 2 := by\n have hA0 := A0count_pos.le\n nlinarith [hJle, hA0, hlogRnn]\n\nend NguyenRH1\n\nend"
}
raw content_json (database row)
[{"type":"thinking","thinking":"3c-i committed (d2bfde6). Now 3c-ii: the three dyadic shells (inlo, inhi, up).\n\nLet me write shell_inlo fully as the template:\n\n```lean\n/-- **The inner-low shell** (3 < ‖ρ‖ ≤ R/2): at most 60·A₀·(log R)². -/\nlemma shell_inlo {s : ℂ} {R : ℝ} (hs : ‖s‖ = R) (hsz : ¬ IsNontrivialZero s)\n (hR : (16002 : ℝ) ≤ R) :\n ∑ ρ ∈ (circleZeros R).filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n ¬ ‖(ρ : ℂ)‖ ≤ 3 ∧ ‖(ρ : ℂ)‖ ≤ R / 2), ‖seriesTerm s ρ‖\n ≤ 60 * A0count * (Real.log R) ^ 2 := by\n have hRpos : (0 : ℝ) < R := by linarith [hR]\n have hlogR : (9 : ℝ) ≤ Real.log R := nine_le_log_of_16002_le hR\n set J := Nat.log 2 ⌊R⌋₊ with hJ\n have hJle : (J : ℝ) ≤ 2 * Real.log R := Nat.log_floor_two_le hR\n set FS := (circleZeros R).filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n ¬ ‖(ρ : ℂ)‖ ≤ 3 ∧ ‖(ρ : ℂ)‖ ≤ R / 2) with hFS\n -- the per-element dyadic-class range\n have hdj : ∀ ρ ∈ FS, 1 ≤ Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊ ∧ Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊ ≤ J := by\n intro ρ hρ\n rw [hFS, Finset.mem_filter] at hρ\n obtain ⟨-, hρ3, hρR2⟩ := hρ\n have hρ3' : (3 : ℝ) < ‖(ρ : ℂ)‖ := lt_of_not_le hρ3\n have hfl3 : (3 : ℕ) ≤ ⌊‖(ρ : ℂ)‖⌋₊ := by\n rw [Nat.le_floor_iff (by linarith : (0 : ℝ) ≤ 3)]\n exact hρ3'.le -- hmm Nat.le_floor_iff : n ≤ ⌊x⌋₊ ↔ (n:ℝ) ≤ x: 3 ≤ ⌊‖ρ‖⌋₊ ⟺ (3:ℝ) ≤ ‖ρ‖ ✓ (hρ3'.le : 3 ≤ ‖ρ‖)\n have h1 : (1 : ℕ) ≤ Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊ := by\n have h2 := Nat.log_mono_right (b := 2) hfl3 -- Nat.log 2 3 ≤ Nat.log 2 ⌊‖ρ‖⌋₊\n have h3 : Nat.log 2 3 = 1 := by norm_num -- log₂3 = 1\n rw [h3] at h2\n exact h2\n have h2 : Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊ ≤ J := by\n apply Nat.log_mono_right (b := 2)\n apply Nat.floor_mono -- ⌊‖ρ‖⌋₊ ≤ ⌊R⌋₊: ‖ρ‖ ≤ R/2 ≤ R ✓\n linarith [hρR2, hR]\n exact ⟨h1, h2⟩\n ...\n```\n\nHmm wait — Nat.log_mono_right : n ≤ m → Nat.log b n ≤ Nat.log b m ✓. Nat.log 2 3 = 1: log₂3: 2^1 = 2 ≤ 3 < 4 = 2^2 ✓ = 1: by decide or norm_num ✓. Nat.floor_mono : x ≤ y → ⌊x⌋₊ ≤ ⌊y⌋₊ ✓.\n\n- the term bound:\n```\n have hterm : ∀ ρ ∈ FS, ‖seriesTerm s ρ‖\n ≤ 2 * (zeroMult (ρ : ℂ) : ℝ) / (2 : ℝ) ^ (Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊) := by\n intro ρ hρ\n rw [hFS, Finset.mem_filter] at hρ\n obtain ⟨-, hρ3, hρR2⟩ := hρ\n have hρ3' : (3 : ℝ) < ‖(ρ : ℂ)‖ := lt_of_not_le hρ3\n -- 2^{jf} ≤ ‖ρ‖\n have hpowle : (2 : ℝ) ^ (Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊) ≤ ‖(ρ : ℂ)‖ := by\n have hfl : ⌊‖(ρ : ℂ)‖⌋₊ ≠ 0 := by\n rw [Ne, Nat.floor_eq_zero]; push Not; linarith [hρ3']\n have h1 := Nat.pow_log_le_self 2 hfl\n have h2 : ((2 ^ Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊ : ℕ) : ℝ) ≤ (⌊‖(ρ : ℂ)‖⌋₊ : ℝ) := by exact_mod_cast h1\n have h3 : ((2 ^ Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊ : ℕ) : ℝ)\n = (2 : ℝ) ^ (Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊) := by push_cast; ring\n rw [h3] at h2\n have h4 : (⌊‖(ρ : ℂ)‖⌋₊ : ℝ) ≤ ‖(ρ : ℂ)‖ := Nat.floor_le (norm_nonneg _)\n linarith [h2, h4]\n -- ‖s−ρ‖ ≥ R/2\n have hsr : R / 2 ≤ ‖s - (ρ : ℂ)‖ := by\n have h := abs_norm_sub_norm_le s (ρ : ℂ)\n rw [hs, abs_of_nonneg (by linarith [hR, hρR2] : (0 : ℝ) ≤ R - ‖(ρ : ℂ)‖)] at h\n linarith [h, hρR2]\n have hρpos : (0 : ℝ) < ‖(ρ : ℂ)‖ := by linarith [hρ3']\n have hsrpos : (0 : ℝ) < ‖s - (ρ : ℂ)‖ := by linarith [hsr, hR]\n have hid := seriesTerm_norm_eq_div hs hsz ρ\n rw [hid]\n have hm : (0 : ℝ) ≤ (zeroMult (ρ : ℂ) : ℝ) := Nat.cast_nonneg _\n -- m·R/(‖ρ‖‖s−ρ‖) ≤ m·R/(‖ρ‖·(R/2)) = 2m/‖ρ‖ ≤ 2m/2^{jf}\n have h1 : R / (‖(ρ : ℂ)‖ * ‖s - (ρ : ℂ)‖) ≤ R / (‖(ρ : ℂ)‖ * (R / 2)) := by\n apply div_le_div_of_nonneg_left hRpos.le (mul_pos hρpos (by linarith [hR]))\n exact mul_le_mul_of_nonneg_left hsr hρpos.le\n have h2 : R / (‖(ρ : ℂ)‖ * (R / 2)) = 2 / ‖(ρ : ℂ)‖ := by\n field_simp\n ring\n have h3 : 2 / ‖(ρ : ℂ)‖ ≤ 2 / (2 : ℝ) ^ (Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊) := by\n apply div_le_div_of_nonneg_left (by norm_num : (0 : ℝ) ≤ 2)\n (by positivity)\n exact hpowle\n calc (zeroMult (ρ : ℂ) : ℝ) * (R / (‖(ρ : ℂ)‖ * ‖s - (ρ : ℂ)‖))\n ≤ (zeroMult (ρ : ℂ) : ℝ) * (R / (‖(ρ : ℂ)‖ * (R / 2))) :=\n mul_le_mul_of_nonneg_left h1 hm\n _ = (zeroMult (ρ : ℂ) : ℝ) * (2 / ‖(ρ : ℂ)‖) := by rw [h2]\n _ ≤ (zeroMult (ρ : ℂ) : ℝ) * (2 / (2 : ℝ) ^ (Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊)) :=\n mul_le_mul_of_nonneg_left h3 hm\n _ = 2 * (zeroMult (ρ : ℂ) : ℝ) / (2 : ℝ) ^ (Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊) := by ring\n```\nCareful with h2: R/(‖ρ‖·(R/2)): field_simp gives 2/(‖ρ‖)·... R/(‖ρ‖·(R/2)) = R·2/(‖ρ‖·R) = 2/‖ρ‖ — field_simp; ring. ✓\n\n- the count:\n```\n have hcount : ∀ j : ℕ, ∑ ρ ∈ FS.filter (fun ρ => Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊ = j),\n (zeroMult (ρ : ℂ) : ℝ)\n ≤ 3 * A0count * ((2 : ℝ) ^ j + 3) * Real.log (3 * max |(2 : ℝ) ^ j - 1| |(2 : ℝ) ^ (j + 1)| + 5) := by\n intro j\n by_cases hj : j ∈ Finset.Ico 1 (J + 1)\n · rw [Finset.mem_Ico] at hj\n have hj1 : (1 : ℝ) ≤ (2 : ℝ) ^ j := by\n exact_mod_cast Nat.one_le_two_pow\n have hj2 : (2 : ℝ) ≤ (2 : ℝ) ^ j := by\n have h1 : (2 : ℝ) ^ 1 ≤ (2 : ℝ) ^ j := pow_le_pow_right₀ (by norm_num) (by omega : 1 ≤ j)\n linarith [h1]\n apply sum_zeroMult_le_of_im_band\n ...\n```\nWait — hcount's statement in dyadic_family_le has the filter lambda `fun ρ => Nat.log 2 ⌊d ρ⌋₊ = j` — with d := fun ρ => ‖(ρ:ℂ)‖ — the lambda there: `fun ρ => Nat.log 2 ⌊‖(ρ:ℂ)‖⌋₊ = j` — the coercion again!! Banked gotcha: pin the binder: `fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => ...`. Hmm — but in dyadic_family_le the filter lambdas are `fun ρ => Nat.log 2 ⌊d ρ⌋₊ = j` — d application pins ρ to the subtype ✓ no coercion issue THERE. But when I INSTANTIATE d := fun ρ => ‖(ρ:ℂ)‖ and write hcount's filter as `FS.filter (fun ρ => Nat.log 2 ⌊‖(ρ:ℂ)‖⌋₊ = j)`, the elaborator must see the filter lambdas as SYNTACTICALLY equal: dyadic_family_le's internal filter is on `fun ρ => Nat.log 2 ⌊d ρ⌋₊ = j` with d substituted — `⌊d ρ⌋₊` = `⌊(fun ρ => ‖(ρ:ℂ)‖) ρ⌋₊` = beta `⌊‖(ρ:ℂ)‖⌋₊` — should be defeq, but for the hcount hypothesis application the elaborator needs to unify the filter sets — with `classical` and defeq it should work if I state hcount's lambda identically: `fun ρ => Nat.log 2 ⌊(fun ρ => ‖(ρ:ℂ)‖) ρ⌋₊ = j`... The application `dyadic_family_le FS (fun ρ => ‖(ρ:ℂ)‖) J _ 2 cnt hC1 hdj hterm hcount` — the hcount's expected type: ∀ j, ∑ ρ ∈ FS.filter (fun ρ => Nat.log 2 ⌊(d) ρ⌋₊ = j), ... ≤ cnt j with d := the lambda — beta-reduced during unification ✓ my stated hcount uses ⌊‖(ρ:ℂ)‖⌋₊ directly — defeq ✓. BUT the lambda binder ambiguity strikes again: in MY hcount statement `fun ρ => Nat.log 2 ⌊‖(ρ:ℂ)‖⌋₊ = j` — the coercion ‖(ρ:ℂ)‖ — the expected type from dyadic_family_le's unification pins ρ : subtype ✓ — since hcount is APPLIED to a known expected type, elaboration is fine. But if hcount is a standalone `have` with ascribed type, I must pin the binder: `fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => ...` — then unification with the expected type needs defeq between `fun ρ : ST => Nat.log 2 ⌊‖(ρ:ℂ)‖⌋₊ = j` and `fun ρ => Nat.log 2 ⌊d ρ⌋₊ = j` — beta + coe ✓ fine.\n\nThe brick application per j (with hj : j ∈ Ico): a := 2^j−1, b := 2^{j+1}, c := 2^j−1:\n- hM1 : 1 ≤ max (2^j−1) (2^j−1) = 2^j−1 ⟺ 2 ≤ 2^j ⟺ j ≥ 1 ✓.\n- hMb : max ... = 2^j−1 ≤ 2^{j+1} ✓.\n- hsub : ∀ ρ ∈ FS.filter (jf · = j), a ≤ |γ| ∧ |γ| ≤ b ∧ c ≤ |γ|:\n per element: jf ρ = j ⟹ 2^j ≤ ‖ρ‖ (as before) and ‖ρ‖ < 2^{j+1} (Nat.lt_pow_succ_log_self + floor+1): \n ```\n have hup : ‖(ρ:ℂ)‖ < (2:ℝ)^(j+1) := by\n have h1 : ⌊‖(ρ:ℂ)‖⌋₊ < 2 ^ (Nat.log 2 ⌊‖(ρ:ℂ)‖⌋₊ + 1) := Nat.lt_pow_succ_log_self (by norm_num) _\n rw [hρj] at h1 -- hρj : Nat.log 2 ⌊‖ρ‖⌋₊ = j\n have h2 : ⌊‖(ρ:ℂ)‖⌋₊ + 1 ≤ 2 ^ (j + 1) := h1\n have h3 : ‖(ρ:ℂ)‖ < (⌊‖(ρ:ℂ)‖⌋₊ : ℝ) + 1 := Nat.lt_floor_add_one _\n have h4 : ((⌊‖(ρ:ℂ)‖⌋₊ + 1 : ℕ) : ℝ) ≤ ((2 ^ (j + 1) : ℕ) : ℝ) := by exact_mod_cast h2\n push_cast at h4\n -- h4 : (⌊‖ρ‖⌋₊ : ℝ) + 1 ≤ (2:ℝ)^(j+1)\n linarith [h3, h4]\n ```\n hmm h4's cast: ((2^(j+1) : ℕ) : ℝ) = (2:ℝ)^(j+1): push_cast at h4 gives (⌊‖ρ‖⌋₊:ℝ)+1 ≤ (2:ℝ)^(j+1) ✓.\n Then: |γ| ≥ ‖ρ‖−1 ≥ 2^j−1 = a ✓ (abs_im_ge_norm_sub_one); |γ| ≤ ‖ρ‖ ≤ ... ‖ρ‖ < 2^{j+1} ⟹ ‖ρ‖ ≤ 2^{j+1} = b: |γ| ≤ ‖ρ‖ — wait |γ| = |im ρ| ≤ ‖ρ‖ (abs_im_le_norm) ✓ then ≤ b via hup.le.\n- The brick then gives ≤ 3·A₀·(b−a+2)·log(3·max|a||b|+5): b−a+2 = 2^{j+1}−(2^j−1)+2 = 2^j+3: need a ring identity with the pow: 2^{j+1} = 2·2^j (pow_succ'). max|a||b| = max|2^j−1||2^{j+1}|: |2^j−1| = 2^j−1 (≥ 1 > 0: j ≥ 1 hmm 2^j−1 ≥ 1 ✓); |2^{j+1}| = 2^{j+1}: max = 2^{j+1} (2^j−1 ≤ 2^{j+1} ✓).\n\nSo cnt j := 3 * A0count * ((2:ℝ)^j + 3) * Real.log (3 * (2:ℝ)^(j+1) + 5).\n\nThen per-j uniform bound: (C₁/2^j)·cnt j = (2/2^j)·3A₀(2^j+3)·log(3·2^{j+1}+5) ≤ 30·A₀·L:\n- log(3·2^{j+1}+5) ≤ 2L: via log_three_le_two_log with x := 2^{j+1}: 0 ≤ x ✓; x ≤ 3R: 2^{j+1} ≤ 2R (j ≤ J: 2^j ≤ 2^J ≤ R ⟹ 2^{j+1} ≤ 2R ≤ 3R ✓ — 2^j ≤ 2^J: pow_le_pow_right₀ (1≤2) (j ≤ J); 2^J ≤ R from Nat.log_floor_two_le's internals — hmm I need (2:ℝ)^J ≤ R as a standalone. Nat.log_floor_two_le gives J ≤ 2L but not 2^J ≤ R. Add a tiny lemma or inline: (2:ℝ)^J ≤ R: Nat.pow_log_le_self + floor_le as in the term bound. Make a lemma `two_pow_log_floor_le (hR : 16002 ≤ R) : (2:ℝ)^(Nat.log 2 ⌊R⌋₊) ≤ R`.)\n- (2/2^j)·3A₀(2^j+3)·2L = 12·A₀·L·(2^j+3)/2^j = 12A₀L(1 + 3/2^j) ≤ 12A₀L(1+3/2) = 30A₀L (2^j ≥ 2 ⟹ 3/2^j ≤ 3/2: div_le_div_of_nonneg_left... (3:ℝ)/2^j ≤ 3/2 ⟸ 2^j ≥ 2, via div_le_div_of_nonneg_left (3≥0) (0<2) (2 ≤ 2^j): gives 3/2^j ≤ 3/2 ✓).\n- Σ_{j∈Ico 1 (J+1)} 30A₀L = J·30A₀L (sum_const, card Ico = J) ≤ 2L·30A₀L = 60A₀L² ✓.\n\nFinal: shell_inlo ≤ 60·A₀·L².\n\nStructure per shell lemma ~150 lines. Three of them + crit + assembly — the remaining big push. Let me write shell_inlo now and compile before cloning the pattern.\n\nAlso — for the final assembly I need the shell bounds in terms of the filter-normal forms from the iterated split: the assembly's second shell is (F.filter ¬P1).filter P2 = F.filter (¬P1 ∧ P2) via Finset.filter_filter. I'll state shell_inlo's finset as F.filter (fun ρ => ¬‖ρ‖ ≤ 3 ∧ ‖ρ‖ ≤ R/2) — and in the assembly use filter_filter to match. ✓ (P1 := ‖ρ‖ ≤ 3, ¬P1 = ¬‖ρ‖ ≤ 3 ✓.)\n\nLet me write shell_inlo.","signature":""},{"type":"text","text":"3c-i committed. Now shell_inlo (the template for the dyadic shells)."},{"type":"tool_use","id":"Edit_79","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiCircleBound.lean","old_string":"end NguyenRH1\n\nend","new_string":"/-! ## 8. The three dyadic shells (5e-v-b chunk 3c-ii)\n\n`two_pow_log_floor_le`: (2:ℝ)^J ≤ R. `shell_inlo` (3 < ‖ρ‖ ≤ R/2),\n`shell_inhi` (R/2 < ‖ρ‖ ≤ R−2), `shell_up` (R+2 ≤ ‖ρ‖ within the\nfinite part): dyadic in ‖ρ‖ / R−‖ρ‖ / ‖ρ‖−R respectively, per-fiber\ncount via the brick, uniform log bound ≤ 2·log R. Each ≤\n60/60/30·A₀·(log R)². -/\n\n/-- (2:ℝ)^J ≤ R for J = Nat.log 2 ⌊R⌋₊, R ≥ 16002. -/\nlemma two_pow_log_floor_le {R : ℝ} (hR : (16002 : ℝ) ≤ R) :\n (2 : ℝ) ^ (Nat.log 2 ⌊R⌋₊) ≤ R := by\n have hfl : ⌊R⌋₊ ≠ 0 := by\n rw [Ne, Nat.floor_eq_zero]\n push Not\n linarith\n have h2 := Nat.pow_log_le_self 2 hfl\n have h3 : ((2 ^ Nat.log 2 ⌊R⌋₊ : ℕ) : ℝ) ≤ (⌊R⌋₊ : ℝ) := by exact_mod_cast h2\n have h4 : (⌊R⌋₊ : ℝ) ≤ R := Nat.floor_le (by linarith [hR])\n have h5 : ((2 ^ Nat.log 2 ⌊R⌋₊ : ℕ) : ℝ) = (2 : ℝ) ^ Nat.log 2 ⌊R⌋₊ := by\n push_cast\n ring\n rw [h5] at h3\n linarith [h3, h4]\n\n/-- **The inner-low shell** (3 < ‖ρ‖ ≤ R/2): ≤ 60·A₀·(log R)². -/\nlemma shell_inlo {s : ℂ} {R : ℝ} (hs : ‖s‖ = R) (hsz : ¬ IsNontrivialZero s)\n (hR : (16002 : ℝ) ≤ R) :\n ∑ ρ ∈ (circleZeros R).filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n ¬ ‖(ρ : ℂ)‖ ≤ 3 ∧ ‖(ρ : ℂ)‖ ≤ R / 2), ‖seriesTerm s ρ‖\n ≤ 60 * A0count * (Real.log R) ^ 2 := by\n classical\n have hRpos : (0 : ℝ) < R := by linarith [hR]\n have hlogR : (9 : ℝ) ≤ Real.log R := nine_le_log_of_16002_le hR\n have hlogRnn : (0 : ℝ) ≤ Real.log R := by linarith [hlogR]\n set J := Nat.log 2 ⌊R⌋₊ with hJ\n have hJle : (J : ℝ) ≤ 2 * Real.log R := Nat.log_floor_two_le hR\n have h2JR : (2 : ℝ) ^ J ≤ R := two_pow_log_floor_le hR\n set FS := (circleZeros R).filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n ¬ ‖(ρ : ℂ)‖ ≤ 3 ∧ ‖(ρ : ℂ)‖ ≤ R / 2) with hFS\n have hdj : ∀ ρ ∈ FS, 1 ≤ Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊ ∧ Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊ ≤ J := by\n intro ρ hρ\n rw [hFS, Finset.mem_filter] at hρ\n obtain ⟨-, hρ3, hρR2⟩ := hρ\n have hρ3' : (3 : ℝ) < ‖(ρ : ℂ)‖ := lt_of_not_le hρ3\n have hfl3 : (3 : ℕ) ≤ ⌊‖(ρ : ℂ)‖⌋₊ := by\n rw [Nat.le_floor_iff (by norm_num : (0 : ℝ) ≤ 3)]\n exact hρ3'.le\n have h1 : (1 : ℕ) ≤ Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊ := by\n have h2 := Nat.log_mono_right (b := 2) hfl3\n have h3 : Nat.log 2 3 = 1 := by decide\n rw [h3] at h2\n exact h2\n have h2 : Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊ ≤ J := by\n apply Nat.log_mono_right (b := 2)\n apply Nat.floor_mono\n linarith [hρR2, hR]\n exact ⟨h1, h2⟩\n have hterm : ∀ ρ ∈ FS, ‖seriesTerm s ρ‖\n ≤ 2 * (zeroMult (ρ : ℂ) : ℝ) / (2 : ℝ) ^ (Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊) := by\n intro ρ hρ\n rw [hFS, Finset.mem_filter] at hρ\n obtain ⟨-, hρ3, hρR2⟩ := hρ\n have hρ3' : (3 : ℝ) < ‖(ρ : ℂ)‖ := lt_of_not_le hρ3\n have hpowle : (2 : ℝ) ^ (Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊) ≤ ‖(ρ : ℂ)‖ := by\n have hfl : ⌊‖(ρ : ℂ)‖⌋₊ ≠ 0 := by\n rw [Ne, Nat.floor_eq_zero]\n push Not\n linarith [hρ3']\n have h1 := Nat.pow_log_le_self 2 hfl\n have h2 : ((2 ^ Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊ : ℕ) : ℝ) ≤ (⌊‖(ρ : ℂ)‖⌋₊ : ℝ) := by\n exact_mod_cast h1\n have h3 : ((2 ^ Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊ : ℕ) : ℝ)\n = (2 : ℝ) ^ (Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊) := by\n push_cast\n ring\n rw [h3] at h2\n have h4 : (⌊‖(ρ : ℂ)‖⌋₊ : ℝ) ≤ ‖(ρ : ℂ)‖ := Nat.floor_le (norm_nonneg _)\n linarith [h2, h4]\n have hsr : R / 2 ≤ ‖s - (ρ : ℂ)‖ := by\n have h := abs_norm_sub_norm_le s (ρ : ℂ)\n rw [hs, abs_of_nonneg (by linarith [hR, hρR2] : (0 : ℝ) ≤ R - ‖(ρ : ℂ)‖)] at h\n linarith [h, hρR2]\n have hρpos : (0 : ℝ) < ‖(ρ : ℂ)‖ := by linarith [hρ3']\n have hsrpos : (0 : ℝ) < ‖s - (ρ : ℂ)‖ := by linarith [hsr, hR]\n have hid := seriesTerm_norm_eq_div hs hsz ρ\n rw [hid]\n have hm : (0 : ℝ) ≤ (zeroMult (ρ : ℂ) : ℝ) := Nat.cast_nonneg _\n have h1 : R / (‖(ρ : ℂ)‖ * ‖s - (ρ : ℂ)‖) ≤ R / (‖(ρ : ℂ)‖ * (R / 2)) := by\n apply div_le_div_of_nonneg_left hRpos.le (mul_pos hρpos (by linarith [hR]))\n exact mul_le_mul_of_nonneg_left hsr hρpos.le\n have h2 : R / (‖(ρ : ℂ)‖ * (R / 2)) = 2 / ‖(ρ : ℂ)‖ := by\n field_simp\n ring\n have h3 : (2 : ℝ) / ‖(ρ : ℂ)‖ ≤ 2 / (2 : ℝ) ^ (Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊) := by\n apply div_le_div_of_nonneg_left (by norm_num : (0 : ℝ) ≤ 2) (by positivity)\n exact hpowle\n calc (zeroMult (ρ : ℂ) : ℝ) * (R / (‖(ρ : ℂ)‖ * ‖s - (ρ : ℂ)‖))\n ≤ (zeroMult (ρ : ℂ) : ℝ) * (R / (‖(ρ : ℂ)‖ * (R / 2))) :=\n mul_le_mul_of_nonneg_left h1 hm\n _ = (zeroMult (ρ : ℂ) : ℝ) * (2 / ‖(ρ : ℂ)‖) := by rw [h2]\n _ ≤ (zeroMult (ρ : ℂ) : ℝ) * (2 / (2 : ℝ) ^ (Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊)) :=\n mul_le_mul_of_nonneg_left h3 hm\n _ = 2 * (zeroMult (ρ : ℂ) : ℝ) / (2 : ℝ) ^ (Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊) := by ring\n have hcount : ∀ j : ℕ,\n ∑ ρ ∈ FS.filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊ = j), (zeroMult (ρ : ℂ) : ℝ)\n ≤ 3 * A0count * ((2 : ℝ) ^ j + 3) * Real.log (3 * (2 : ℝ) ^ (j + 1) + 5) := by\n intro j\n by_cases hj : j ∈ Finset.Ico 1 (J + 1)\n · rw [Finset.mem_Ico] at hj\n have hj2 : (2 : ℝ) ≤ (2 : ℝ) ^ j := by\n have h1 : (2 : ℝ) ^ 1 ≤ (2 : ℝ) ^ j :=\n pow_le_pow_right₀ (by norm_num) (by omega : 1 ≤ j)\n linarith [h1]\n have hM1 : (1 : ℝ) ≤ max ((2 : ℝ) ^ j - 1) ((2 : ℝ) ^ j - 1) := by\n rw [max_self]\n linarith [hj2]\n have hMb : max ((2 : ℝ) ^ j - 1) ((2 : ℝ) ^ j - 1) ≤ (2 : ℝ) ^ (j + 1) := by\n rw [max_self]\n have h1 : (2 : ℝ) ^ (j + 1) = 2 * (2 : ℝ) ^ j := by rw [pow_succ']\n linarith [hj2]\n have hsub : ∀ ρ ∈ FS.filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊ = j),\n (2 : ℝ) ^ j - 1 ≤ |(ρ : ℂ).im| ∧ |(ρ : ℂ).im| ≤ (2 : ℝ) ^ (j + 1) ∧\n (2 : ℝ) ^ j - 1 ≤ |(ρ : ℂ).im| := by\n intro ρ hρ\n rw [Finset.mem_filter] at hρ\n obtain ⟨hρF, hρj⟩ := hρ\n have hpowle : (2 : ℝ) ^ j ≤ ‖(ρ : ℂ)‖ := by\n have hfl : ⌊‖(ρ : ℂ)‖⌋₊ ≠ 0 := by\n rw [Ne, Nat.floor_eq_zero]\n push Not\n rw [hFS, Finset.mem_filter] at hρF\n have hρ3' : (3 : ℝ) < ‖(ρ : ℂ)‖ := lt_of_not_le hρF.2.1\n linarith [hρ3']\n have h1 := Nat.pow_log_le_self 2 hfl\n rw [← hρj] at h1\n have h2 : ((2 ^ j : ℕ) : ℝ) ≤ (⌊‖(ρ : ℂ)‖⌋₊ : ℝ) := by exact_mod_cast h1\n have h3 : ((2 ^ j : ℕ) : ℝ) = (2 : ℝ) ^ j := by push_cast; ring\n rw [h3] at h2\n have h4 : (⌊‖(ρ : ℂ)‖⌋₊ : ℝ) ≤ ‖(ρ : ℂ)‖ := Nat.floor_le (norm_nonneg _)\n linarith [h2, h4]\n have hpowup : ‖(ρ : ℂ)‖ < (2 : ℝ) ^ (j + 1) := by\n have h1 : ⌊‖(ρ : ℂ)‖⌋₊ < 2 ^ (Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊ + 1) :=\n Nat.lt_pow_succ_log_self (by norm_num) _\n rw [hρj] at h1\n have h2 : ⌊‖(ρ : ℂ)‖⌋₊ + 1 ≤ 2 ^ (j + 1) := h1\n have h3 : ‖(ρ : ℂ)‖ < (⌊‖(ρ : ℂ)‖⌋₊ : ℝ) + 1 := Nat.lt_floor_add_one _\n have h4 : ((⌊‖(ρ : ℂ)‖⌋₊ + 1 : ℕ) : ℝ) ≤ ((2 ^ (j + 1) : ℕ) : ℝ) := by\n exact_mod_cast h2\n have h5 : ((2 ^ (j + 1) : ℕ) : ℝ) = (2 : ℝ) ^ (j + 1) := by push_cast; ring\n rw [h5] at h4\n push_cast at h4\n linarith [h3, h4]\n have him1 := abs_im_ge_norm_sub_one ρ\n have him2 : |(ρ : ℂ).im| ≤ ‖(ρ : ℂ)‖ := abs_im_le_norm _\n exact ⟨by linarith [him1, hpowle], by linarith [him2, hpowup],\n by linarith [him1, hpowle]⟩\n have hbrick := sum_zeroMult_le_of_im_band\n (FS.filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊ = j))\n hM1 hMb hsub\n have hab : (2 : ℝ) ^ (j + 1) - ((2 : ℝ) ^ j - 1) + 2 = (2 : ℝ) ^ j + 3 := by\n have h1 : (2 : ℝ) ^ (j + 1) = 2 * (2 : ℝ) ^ j := by rw [pow_succ']\n linarith [h1]\n have hmax : max |(2 : ℝ) ^ j - 1| |(2 : ℝ) ^ (j + 1)| = (2 : ℝ) ^ (j + 1) := by\n have h1 : |(2 : ℝ) ^ (j + 1)| = (2 : ℝ) ^ (j + 1) := abs_of_nonneg (by positivity)\n have h2 : |(2 : ℝ) ^ j - 1| = (2 : ℝ) ^ j - 1 := abs_of_nonneg (by linarith [hj2])\n rw [h1, h2]\n have h3 : (2 : ℝ) ^ (j + 1) = 2 * (2 : ℝ) ^ j := by rw [pow_succ']\n have h4 : (0 : ℝ) < (2 : ℝ) ^ j := by positivity\n nlinarith [h3, h4]\n rw [hab, hmax] at hbrick\n exact hbrick\n · have hempty : FS.filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n Nat.log 2 ⌊‖(ρ : ℂ)‖⌋₊ = j) = ∅ := by\n apply Finset.eq_empty_iff_forall_not_mem.mpr\n intro ρ hρ\n rw [Finset.mem_filter] at hρ\n obtain ⟨hρF, hρj⟩ := hρ\n have hdjρ := hdj ρ hρF\n rw [hρj] at hdjρ\n rw [Finset.mem_Ico] at hj\n omega\n rw [hempty, Finset.sum_empty]\n have h1 : (0 : ℝ) ≤ Real.log (3 * (2 : ℝ) ^ (j + 1) + 5) := by\n apply Real.log_nonneg\n have h2 : (0 : ℝ) < (2 : ℝ) ^ (j + 1) := by positivity\n linarith [h2]\n exact mul_nonneg (mul_nonneg (by norm_num) A0count_pos.le (by positivity)) h1\n -- the closed-form per-shell bound\n have hper : ∀ j ∈ Finset.Ico 1 (J + 1),\n (2 / (2 : ℝ) ^ j) * (3 * A0count * ((2 : ℝ) ^ j + 3) *\n Real.log (3 * (2 : ℝ) ^ (j + 1) + 5))\n ≤ 30 * A0count * Real.log R := by\n intro j hj\n rw [Finset.mem_Ico] at hj\n have h2j0 : (0 : ℝ) < (2 : ℝ) ^ j := by positivity\n have hj2 : (2 : ℝ) ≤ (2 : ℝ) ^ j := by\n have h1 : (2 : ℝ) ^ 1 ≤ (2 : ℝ) ^ j :=\n pow_le_pow_right₀ (by norm_num) (by omega : 1 ≤ j)\n linarith [h1]\n have hlogle : Real.log (3 * (2 : ℝ) ^ (j + 1) + 5) ≤ 2 * Real.log R := by\n apply log_three_le_two_log hR (by positivity)\n have h1 : (2 : ℝ) ^ (j + 1) = 2 * (2 : ℝ) ^ j := by rw [pow_succ']\n have h2 : (2 : ℝ) ^ j ≤ (2 : ℝ) ^ J := pow_le_pow_right₀ (by norm_num) (by omega : j ≤ J)\n nlinarith [h1, h2, h2JR, hR]\n have hA0 := A0count_pos.le\n have h1 : (2 / (2 : ℝ) ^ j) * (3 * A0count * ((2 : ℝ) ^ j + 3) *\n Real.log (3 * (2 : ℝ) ^ (j + 1) + 5))\n = 6 * A0count * Real.log (3 * (2 : ℝ) ^ (j + 1) + 5) * (1 + 3 / (2 : ℝ) ^ j) := by\n field_simp\n ring\n rw [h1]\n have h2 : 3 / (2 : ℝ) ^ j ≤ 3 / 2 := by\n apply div_le_div_of_nonneg_left (by norm_num : (0 : ℝ) ≤ 3) (by norm_num) hj2\n have hlognn : (0 : ℝ) ≤ Real.log (3 * (2 : ℝ) ^ (j + 1) + 5) := by\n apply Real.log_nonneg\n have h3 : (0 : ℝ) < (2 : ℝ) ^ (j + 1) := by positivity\n linarith [h3]\n nlinarith [hlogle, h2, hlognn, hA0, hlogRnn]\n -- assembly via dyadic_family_le\n have hmain := dyadic_family_le FS (fun ρ => ‖(ρ : ℂ)‖) J\n (fun ρ => ‖seriesTerm s ρ‖) 2\n (fun j => 3 * A0count * ((2 : ℝ) ^ j + 3) * Real.log (3 * (2 : ℝ) ^ (j + 1) + 5))\n (by norm_num) hdj hterm hcount\n calc ∑ ρ ∈ FS, ‖seriesTerm s ρ‖\n ≤ ∑ j ∈ Finset.Ico 1 (J + 1), (2 / (2 : ℝ) ^ j) *\n (3 * A0count * ((2 : ℝ) ^ j + 3) * Real.log (3 * (2 : ℝ) ^ (j + 1) + 5)) := hmain\n _ ≤ ∑ j ∈ Finset.Ico 1 (J + 1), 30 * A0count * Real.log R := Finset.sum_le_sum hper\n _ = (J : ℝ) * (30 * A0count * Real.log R) := by\n rw [Finset.sum_const, Nat.card_Ico, Nat.add_sub_cancel, nsmul_eq_mul]\n _ ≤ 60 * A0count * (Real.log R) ^ 2 := by\n have hA0 := A0count_pos.le\n nlinarith [hJle, hA0, hlogRnn]\n\nend NguyenRH1\n\nend"},"extra_content":null}]