← Session 24 — ii′-2…4: swaps, (4.10) design, contour + website roadmap fixes
thinking (8878 chars)
`HasDerivAt.const_cpow (hf : HasDerivAt f f' x) (h0 : c ≠ 0 ∨ f x ≠ 0) : HasDerivAt (fun x => c ^ f x) (c ^ f x * Complex.log c * f') x` ✓ — side condition: c ≠ 0 ∨ f x ≠ 0. For c = (x:ℂ) (x > 1): c ≠ 0 ✓ left.
Now write §3. The structure (cloned from Zeta23 with my modifications):
```lean
/-! ## 3. Analyticity of the B̃₂ parameter integral -/
/-- The B̃₂ parameter integral is differentiable on re s > −1, with the
log-weighted derivative. (Clone of Zeta23's `hasDerivAt_Zeta0Integral`
with one more power of decay, D-067 §2.) -/
theorem hasDerivAt_b2Integral {s : ℂ} (hs : -1 < s.re) :
HasDerivAt (fun z : ℂ => ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-z - 2))
(∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * ((x : ℂ) ^ (-s - 2) * (-Real.log x))) s := by
set f : ℝ → ℂ := fun x ↦ (b2Fun x : ℂ)
set F : ℂ → ℝ → ℂ := fun z x ↦ (x : ℂ) ^ (-z - 2) * f x
set F' : ℂ → ℝ → ℂ := fun z x ↦ (x : ℂ) ^ (-z - 2) * (-Real.log x) * f x
set ε := (s.re + 1) / 2
have ε_pos : 0 < ε := by linarith
set bound : ℝ → ℝ := fun x ↦ |x ^ (-(s.re + 3) / 2)| * |Real.log x|
let μ : Measure ℝ := volume.restrict (Set.Ioi (1:ℝ))
have hF_meas : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) μ := by
have hU : {z : ℂ | -1 < z.re} ∈ 𝓝 s := by
rw [mem_nhds_iff]
exact ⟨{z | -1 < z.re}, fun _ a ↦ a, isOpen_lt continuous_const Complex.continuous_re, hs⟩
filter_upwards [hU] with z hz
have h := (integrableOn_b2_cpow hz).aestronglyMeasurable
-- F z x = x^(−z−2) * f x vs their form: f x * x^(−z−2): comm
exact h.congr (Filter.Eventually.of_forall fun x => by
simp only [F, f]
ring)
have hF_int : Integrable (F s) μ := by
apply Integrable.congr ((integrableOn_b2_cpow hs) : Integrable _ μ) -- IntegrableOn = Integrable on restrict — defeq
filter_upwards with x
simp only [F, f]
ring
have hF'_meas : AEStronglyMeasurable (F' s) μ := by
have h := (integrableOn_b2_cpow_log hs).aestronglyMeasurable
exact h.congr (Filter.Eventually.of_forall fun x => by
simp only [F', f]
ring)
have h_bound : ∀ᵐ x ∂μ, ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x := by
filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx
have hx1 : (1:ℝ) < x := Set.mem_Ioi.mp hx
intro z hz
have hzre : (s.re - 1) / 2 < z.re := by
rw [Metric.mem_ball, Complex.dist_eq] at hz
have := abs_re_le_norm (z - s)
have : |z.re - s.re| ≤ ‖z - s‖ := this
have h2 : z.re - s.re > -ε := by linarith [abs_lt.mp (lt_of_le_of_lt this hz)] -- hmm
...
```
Hmm let me be careful: z ∈ ball s ε ⟹ dist z s < ε ⟹ |z.re − s.re| ≤ ‖z − s‖ = dist < ε ⟹ z.re > s.re − ε = σ − (σ+1)/2 = (σ−1)/2 ✓. Then −z.re − 2 < −(σ−1)/2 − 2 = (−σ−3)/2 ✓. Then x^(−z.re−2) ≤ x^((−σ−3)/2) for x ≥ 1 (rpow monotone in exponent for x ≥ 1: `Real.rpow_le_rpow_of_exponent_le (hx : 1 ≤ x) (h : a ≤ b)`? — name: Real.rpow_le_rpow_of_exponent_le ✓ (from their proof)). With ≤ vs < : use .le.
Then:
‖F' z x‖ = ‖x^(−z−2)‖·‖−log x‖·‖f x‖ = x^(−z.re−2)·|log x|·|b2Fun x| ≤ x^((−σ−3)/2)·|log x|·(1/8) ≤ x^((−σ−3)/2)·|log x| = |x^((−σ−3)/2)|·|log x| = bound x ✓ (x^... ≥ 0).
The norm computation: ‖(x:ℂ)^(−z−2)‖ = x^(re(−z−2)) = x^(−z.re−2) (norm_cpow_eq_rpow_re_of_pos ✓ x > 1). ‖−Real.log x‖ as ℂ = |log x| ✓ (norm_neg + norm_real + norm_eq_abs). ‖f x‖ = |b2Fun x| ≤ 1/8 ✓.
have bound_integrable : Integrable bound μ := by
have h := integrable_log_over_pow (r := -(s.re + 1)/2) (by linarith) (N := 1) (by norm_num)
rw [Nat.cast_one] at h
-- their form: IntegrableOn (fun x => ‖x^(r−1)‖·‖log x‖) (Ioi 1): r−1 = (−σ−3)/2 ✓
refine h.congr_fun ?_ measurableSet_Ioi -- hmm Integrable bound μ vs IntegrableOn — defeq
intro x hx
have hx1 : (1:ℝ) < x := Set.mem_Ioi.mp hx
show ‖x ^ (-(s.re + 1)/2 - 1)‖ * ‖Real.log x‖ = |x ^ (-(s.re + 3)/2)| * |Real.log x|
rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_nonneg (Real.rpow_nonneg (by linarith) _),
Real.abs_rpow_of_nonneg (by linarith)] -- |x^...| = x^... ✓ both
congr 2
ring
have h_diff : ∀ᵐ x ∂μ, ∀ z ∈ Metric.ball s ε, HasDerivAt (fun w ↦ F w x) (F' z x) z := by
filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx
have hx1 : (1:ℝ) < x := Set.mem_Ioi.mp hx
intro z hz
-- F w x = x^(−w−2)·f x: derivative = x^(−z−2)·log x·(−1)·f x — via const_cpow with f w = −w−2:
have h1 : HasDerivAt (fun w : ℂ => (x : ℂ) ^ (-w - 2)) ((x : ℂ) ^ (-z - 2) * Complex.log x * (-1)) z := by
have := HasDerivAt.const_cpow (c := (x : ℂ)) (f := fun w : ℂ => -w - 2) (f' := -1) (x := z)
?_ ?_
· -- match derivative form: const_cpow gives c^(f z)·log c·f' = x^(−z−2)·log x·(−1) ✓
convert this using 2 -- f z = −z−2 ✓ rfl; the log of ofReal: Complex.log ↑x = ↑(Real.log x) ✓ (Complex.ofReal_log (x ≥ 0))
...
· left -- c ≠ 0: ↑x ≠ 0 (x > 1)
exact_mod_cast ne_of_gt (lt_trans zero_lt_one hx1)...
-- then times f x (const):
have h2 := h1.mul_const (f x) -- HasDerivAt (fun w => x^(−w−2)·f x) (x^(−z−2)·log x·(−1)·f x)
convert h2 using 1
· ext w; simp only [F]; ring -- F w x = x^(−w−2)·f x ✓
· simp only [F', f] -- F' z x = x^(−z−2)·(−log x)·f x vs x^(−z−2)·log x·(−1)·f x
rw [Complex.ofReal_log (by linarith)] -- if needed
ring
-- the final assembly
have key := (hasDerivAt_integral_of_dominated_loc_of_deriv_le (F := F) (F' := F') (x₀ := s)
(s := Metric.ball s ε) (bound := bound) (μ := μ) (Metric.ball_mem_nhds s ε_pos)
hF_meas hF_int hF'_meas h_bound bound_integrable h_diff).2
-- key : HasDerivAt (fun z => ∫ x, F z x ∂μ) (∫ x, F' s x ∂μ) s; match forms:
convert key using 1
· ext z; simp only [F, f] -- ∫ x, x^(−z−2)·↑b2Fun x = ∫ x, ↑b2Fun x·x^(−z−2): integral_congr? ext on the function z ↦ ∫ — the integrals: ∫ ∂μ vs ∫ Ioi: ∫ x, F z x ∂μ = ∫ x in Ioi 1, ...: μ = volume.restrict (Ioi 1): `integral_restrict`? hmm — the ∫ a, F n a ∂μ with μ = restrict: `MeasureTheory.integral_restrict`? there's integral over restrict = set integral: `integral_restrict (hs : MeasurableSet s) : ∫ x, f x ∂(μ.restrict s) = ∫ x in s, f x ∂μ`? I believe ∫ over restrict is by def `∫ x in s, f x ∂μ = ∫ x, f x ∂(μ.restrict s)` — so convert: the goals match after rewriting set integral ↔ restrict integral (defeq? set integral is DEFINED as restrict integral ✓ rfl-level). And the integrand order: F z x = x^· * f vs goal's ↑b2Fun·x^·: ext z; apply integral_congr_ae; filter_upwards; ring.
· simp only [F', f]; apply integral_congr_ae; filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx; ring — hmm my goal form: ↑b2Fun x * (↑x^(−s−2) * (−↑(Real.log x))) vs F' form ↑x^(−s−2) * (−↑log x) * ↑b2Fun x: ring ✓ but need the log-cast aligned: −Real.log x cast — both sides ↑(-Real.log x)?? the goal's written as (-Real.log x) inside ℂ mult — elaborates as ↑(−Real.log x)? or −↑(Real.log x)? Both defeq via push_cast; ring handles if atoms match... to be safe use `push_cast; ring`.
```
Let me check HasDerivAt.const_cpow's application shape: (hf : HasDerivAt f f' x) (h0 : c ≠ 0 ∨ f x ≠ 0) : HasDerivAt (fun x => c ^ f x) (c ^ f x * Complex.log c * f') x. So:
```lean
have h1 : HasDerivAt (fun w : ℂ => (x : ℂ) ^ (-w - 2))
((x : ℂ) ^ (-z - 2) * Complex.log (x : ℂ) * (-1)) z :=
HasDerivAt.const_cpow (c := (x : ℂ)) (f := fun w : ℂ => -w - 2) (f' := -1) (x := z)
((hasDerivAt_id z).neg.sub_const 2) (Or.inl (by norm_cast; linarith))
```
Hmm — (hasDerivAt_id z).neg : HasDerivAt (fun w => -w) (-1) z ✓; .sub_const 2: fun w => −w − 2, derivative −1 − 0 = −1 ✓ (maybe displays −1 directly; or needs sub_zero simp). And f z = −z−2 ✓ the c^(f z) = x^(−z−2) ✓. c ≠ 0: (x:ℂ) ≠ 0 from x > 1: `(by norm_cast; linarith)`? norm_cast: (↑x : ℂ) ≠ 0 ↔ x ≠ 0: `Complex.ofReal_ne_zero.mpr (by linarith)` ✓ cleaner.
Then the derivative value: x^(−z−2)·log(↑x)·(−1) — Complex.log (↑x) = ↑(Real.log x) for x ≥ 0: `Complex.ofReal_log (hx : 0 ≤ x) : Complex.log ↑x = ↑(Real.log x)` ✓.
Then h2 := h1.mul_const (f x): HasDerivAt.mul_const? `HasDerivAt.mul_const (h : HasDerivAt f f' x) (c) : HasDerivAt (fun x => f x * c) (f' * c)` ✓. Gives derivative (x^(−z−2)·↑log x·(−1))·f x — want F' z x = x^(−z−2)·(−↑log x)·f x: equal by ring ✓.
The HasDerivAt.const_cpow — wait — one nuance: `HasDerivAt.const_cpow (hf : HasDerivAt f f' x) (h0 : c ≠ 0 ∨ f x ≠ 0)` — h0 : c ≠ 0 ∨ f x ≠ 0 — I pass Or.inl (ofReal_ne_zero...) ✓ (f x ≠ 0 unnecessary).
Also `hasDerivAt_integral_of_dominated_loc_of_deriv_le` — check arg order: (hs : s ∈ 𝓝 x₀) (hF_meas) (hF_int) {F'} (hF'_meas) (h_bound) (bound_integrable) (h_diff) : Integrable (F' x₀) ∧ HasDerivAt (fun n ↦ ∫ a, F n a ∂μ) (∫ a, F' x₀ a ∂μ) x₀ — the μ and F are implicit/explicit? Variables from the section: F, μ probably explicit-ish. The Zeta23 usage passed (F := F) (F' := F') (x₀ := s) (s := ...) (bound := ...) (μ := μ) explicitly ✓ copy.
Alright — write §3 now.
Writing §3 — the parameter-integral derivative (cloning Zeta23's proof with the extra decay power).
tool: Edit ok
input
{
"replace_all": false,
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiRBound.lean",
"old_string": "end NguyenRH1\n\nend",
"new_string": "/-! ## 3. Analyticity of the B\u0303\u2082 parameter integral -/\n\n/-- The B\u0303\u2082 parameter integral is differentiable on re s > \u22121, with the\nlog-weighted derivative. (Clone of Zeta23's `hasDerivAt_Zeta0Integral`\nwith one more power of decay, per D-067 \u00a72.) -/\ntheorem hasDerivAt_b2Integral {s : \u2102} (hs : -1 < s.re) :\n HasDerivAt (fun z : \u2102 => \u222b x in Set.Ioi (1:\u211d), (b2Fun x : \u2102) * (x : \u2102) ^ (-z - 2))\n (\u222b x in Set.Ioi (1:\u211d), (b2Fun x : \u2102) * ((x : \u2102) ^ (-s - 2) * (-Real.log x))) s := by\n set f : \u211d \u2192 \u2102 := fun x \u21a6 (b2Fun x : \u2102)\n set F : \u2102 \u2192 \u211d \u2192 \u2102 := fun z x \u21a6 (x : \u2102) ^ (-z - 2) * f x\n set F' : \u2102 \u2192 \u211d \u2192 \u2102 := fun z x \u21a6 (x : \u2102) ^ (-z - 2) * (-Real.log x) * f x\n set \u03b5 := (s.re + 1) / 2\n have \u03b5_pos : 0 < \u03b5 := by linarith\n set bound : \u211d \u2192 \u211d := fun x \u21a6 |x ^ (-(s.re + 3) / 2)| * |Real.log x|\n let \u03bc : Measure \u211d := volume.restrict (Set.Ioi (1:\u211d))\n have hF_meas : \u2200\u1da0 (z : \u2102) in \ud835\udcdd s, AEStronglyMeasurable (F z) \u03bc := by\n have hU : {z : \u2102 | -1 < z.re} \u2208 \ud835\udcdd s := by\n rw [mem_nhds_iff]\n exact \u27e8{z | -1 < z.re}, fun _ a \u21a6 a, isOpen_lt continuous_const Complex.continuous_re, hs\u27e9\n filter_upwards [hU] with z hz\n have h := (integrableOn_b2_cpow hz).aestronglyMeasurable\n exact h.congr (Filter.Eventually.of_forall fun x => by simp only [F, f]; ring)\n have hF_int : Integrable (F s) \u03bc := by\n apply Integrable.congr (integrableOn_b2_cpow hs)\n filter_upwards with x\n simp only [F, f]\n ring\n have hF'_meas : AEStronglyMeasurable (F' s) \u03bc := by\n have h := (integrableOn_b2_cpow_log hs).aestronglyMeasurable\n exact h.congr (Filter.Eventually.of_forall fun x => by simp only [F', f]; ring)\n have h_bound : \u2200\u1d50 x \u2202\u03bc, \u2200 z \u2208 Metric.ball s \u03b5, \u2016F' z x\u2016 \u2264 bound x := by\n filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx\n have hx1 : (1:\u211d) < x := Set.mem_Ioi.mp hx\n intro z hz\n have hzre : (s.re - 1) / 2 < z.re := by\n rw [Metric.mem_ball, Complex.dist_eq] at hz\n have h1 : |z.re - s.re| \u2264 \u2016z - s\u2016 := abs_re_le_norm (z - s)\n have h2 : z.re - s.re > -\u03b5 := by\n have h3 : |z.re - s.re| < \u03b5 := lt_of_le_of_lt h1 hz\n linarith [abs_lt.mp h3]\n linarith [h2]\n have hpow : \u2016(x : \u2102) ^ (-z - 2)\u2016 \u2264 x ^ (-(s.re + 3) / 2) := by\n rw [norm_cpow_eq_rpow_re_of_pos (by linarith)]\n have h3 : (-z - 2).re = -z.re - 2 := by simp\n rw [h3]\n apply Real.rpow_le_rpow_of_exponent_le (by linarith)\n linarith [hzre]\n calc \u2016F' z x\u2016 = \u2016(x : \u2102) ^ (-z - 2)\u2016 * |Real.log x| * |b2Fun x| := by\n simp only [F', f, norm_mul, norm_neg, Complex.norm_real, Real.norm_eq_abs]\n ring\n _ \u2264 x ^ (-(s.re + 3) / 2) * |Real.log x| * (1 / 8) := by\n apply mul_le_mul_of_nonneg_right _ (by norm_num)\n apply mul_le_mul_of_nonneg_right hpow (abs_nonneg _)\n _ \u2264 x ^ (-(s.re + 3) / 2) * |Real.log x| * 1 := by\n apply mul_le_mul_of_nonneg_left _ (by positivity)\n exact (abs_b2Fun_le x).trans (by norm_num)\n _ = bound x := by\n simp only [bound]\n rw [Real.abs_rpow_of_nonneg (by linarith)]\n ring\n have bound_integrable : Integrable bound \u03bc := by\n have h := integrable_log_over_pow (r := -(s.re + 1) / 2) (by linarith) (N := 1) (by norm_num)\n rw [Nat.cast_one] at h\n refine h.congr_fun ?_ measurableSet_Ioi\n intro x hx\n have hx1 : (1:\u211d) < x := Set.mem_Ioi.mp hx\n show \u2016x ^ (-(s.re + 1) / 2 - 1)\u2016 * \u2016Real.log x\u2016 = |x ^ (-(s.re + 3) / 2)| * |Real.log x|\n rw [Real.norm_eq_abs, Real.norm_eq_abs, Real.abs_rpow_of_nonneg (by linarith),\n Real.abs_rpow_of_nonneg (by linarith)]\n congr 2\n ring\n have h_diff : \u2200\u1d50 x \u2202\u03bc, \u2200 z \u2208 Metric.ball s \u03b5, HasDerivAt (fun w \u21a6 F w x) (F' z x) z := by\n filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx\n have hx1 : (1:\u211d) < x := Set.mem_Ioi.mp hx\n intro z hz\n have h1 : HasDerivAt (fun w : \u2102 => (x : \u2102) ^ (-w - 2))\n ((x : \u2102) ^ (-z - 2) * Complex.log (x : \u2102) * (-1)) z :=\n HasDerivAt.const_cpow (c := (x : \u2102)) (f := fun w : \u2102 => -w - 2) (f' := -1) (x := z)\n ((hasDerivAt_id z).neg.sub_const 2)\n (Or.inl (Complex.ofReal_ne_zero.mpr (by linarith)))\n have h2 := h1.mul_const (f x)\n convert h2 using 1\n \u00b7 ext w\n simp only [F]\n ring\n \u00b7 simp only [F', f]\n rw [Complex.ofReal_log (by linarith : (0:\u211d) \u2264 x)]\n push_cast\n ring\n have key := (hasDerivAt_integral_of_dominated_loc_of_deriv_le (F := F) (F' := F') (x\u2080 := s)\n (s := Metric.ball s \u03b5) (bound := bound) (\u03bc := \u03bc) (Metric.ball_mem_nhds s \u03b5_pos)\n hF_meas hF_int hF'_meas h_bound bound_integrable h_diff).2\n convert key using 1\n \u00b7 ext z\n apply integral_congr_ae\n filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx\n simp only [F, f]\n ring\n \u00b7 apply integral_congr_ae\n filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx\n simp only [F', f]\n push_cast\n ring\n\nend NguyenRH1\n\nend"
}
result 2026-08-22 18:10:00Z → 2026-08-25 05:44:53Z
{
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiContour.lean",
"oldString": " have hu1 := Finset.sum_union_inter (s := (zeroWindow_finite (a - 1)).toFinset)\n (t := (zeroWindow_finite a).toFinset \u222a (zeroWindow_finite (a + 1)).toFinset)\n (f := fun \u03c1 => (zeroMult \u03c1 : \u211d))\n have hnn : (0 : \u211d) \u2264 \u2211 \u03c1 \u2208 (zeroWindow_finite (a - 1)).toFinset \u2229\n ((zeroWindow_finite a).toFinset \u222a (zeroWindow_finite (a + 1)).toFinset),\n (zeroMult \u03c1 : \u211d) :=\n Finset.sum_nonneg (fun \u03c1 _ => Nat.cast_nonneg _)\n have hu2 := Finset.sum_union_inter (s := (zeroWindow_finite a).toFinset)\n (t := (zeroWindow_finite (a + 1)).toFinset) (f := fun \u03c1 => (zeroMult \u03c1 : \u211d))\n have hnn2 : (0 : \u211d) \u2264 \u2211 \u03c1 \u2208 (zeroWindow_finite a).toFinset \u2229\n (zeroWindow_finite (a + 1)).toFinset, (zeroMult \u03c1 : \u211d) :=\n Finset.sum_nonneg (fun \u03c1 _ => Nat.cast_nonneg _)\n linarith\n have h1 := hZC (a - 1) (by linarith)\n have h2 := hZC a (by linarith)\n have h3 := hZC (a + 1) (by linarith)\n have hmono1 : C0hat a \u2264 C0hat (a + 2) := C0hat_mono (by linarith) (by linarith)\n have hmono2 : C0hat (a + 1) \u2264 C0hat (a + 2) := C0hat_mono (by linarith) (by linarith)",
"newString": " have hu1 := Finset.sum_union_inter (s\u2081 := (zeroWindow_finite (a - 1)).toFinset)\n (s\u2082 := (zeroWindow_finite a).toFinset \u222a (zeroWindow_finite (a + 1)).toFinset)\n (f := fun \u03c1 => (zeroMult \u03c1 : \u211d))\n have hnn : (0 : \u211d) \u2264 \u2211 \u03c1 \u2208 (zeroWindow_finite (a - 1)).toFinset \u2229\n ((zeroWindow_finite a).toFinset \u222a (zeroWindow_finite (a + 1)).toFinset),\n (zeroMult \u03c1 : \u211d) :=\n Finset.sum_nonneg (fun \u03c1 _ => Nat.cast_nonneg _)\n have hu2 := Finset.sum_union_inter (s\u2081 := (zeroWindow_finite a).toFinset)\n (s\u2082 := (zeroWindow_finite (a + 1)).toFinset) (f := fun \u03c1 => (zeroMult \u03c1 : \u211d))\n have hnn2 : (0 : \u211d) \u2264 \u2211 \u03c1 \u2208 (zeroWindow_finite a).toFinset \u2229\n (zeroWindow_finite (a + 1)).toFinset, (zeroMult \u03c1 : \u211d) :=\n Finset.sum_nonneg (fun \u03c1 _ => Nat.cast_nonneg _)\n linarith\n have h1 : (\u2211 \u03c1 \u2208 (zeroWindow_finite (a - 1)).toFinset, (zeroMult \u03c1 : \u211d)) \u2264\n C0hat a := by\n have h := hZC (a - 1) (by linarith)\n rwa [show a - 1 + 1 = a from by ring] at h\n have h2 := hZC a (by linarith)\n have h3 : (\u2211 \u03c1 \u2208 (zeroWindow_finite (a + 1)).toFinset, (zeroMult \u03c1 : \u211d)) \u2264\n C0hat (a + 2) := by\n have h := hZC (a + 1) (by linarith)\n rwa [show a + 1 + 1 = a + 2 from by ring] at h\n have hlog1 : Real.log (a + 2) \u2264 Real.log (a + 2 + 2) :=\n Real.log_le_log (by positivity) (by linarith)\n have hlog2 : Real.log (Real.log (a + 2)) \u2264 Real.log (Real.log (a + 2 + 2)) :=\n Real.log_le_log (Real.log_pos (by linarith)) hlog1\n have hmono1 : C0hat a \u2264 C0hat (a + 2) := by\n unfold C0hat\n linarith [hlog1, hlog2]\n have hmono2 : C0hat (a + 1) \u2264 C0hat (a + 2) := by\n unfold C0hat\n have h1' : Real.log (a + 1 + 2) \u2264 Real.log (a + 2 + 2) :=\n Real.log_le_log (by positivity) (by linarith)\n have h2' : Real.log (Real.log (a + 1 + 2)) \u2264 Real.log (Real.log (a + 2 + 2)) :=\n Real.log_le_log (Real.log_pos (by linarith)) h1'\n linarith [h1', h2']",
"originalFile": "/-\nNguyenRH1/LiContour.lean \u2014 tier ii\u2032 sub-stage ii\u2032-4 (D-064 \u00a75 graph L3+L1,\nD-036 \u00a72\u20133): the zero-avoiding ordinate T (pigeonhole on the perimeter\nunit-window count bound) and the Lagarias-kernel norm bounds.\n\nL3 (D-036 \u00a72): in a unit ordinate window [a, a+1] (a \u2265 2) with at most\n\u0108\u2080(a+1) zero ordinates, one of the k+1 equally spaced midpoints\nT_j = a + (2j+1)/(2(k+1)) has distance \u2265 1/(2(k+1)) \u2265 1/(3\u00b7\u0108\u2080(a+1)) from\nevery zero ordinate in the window (each zero lies within < 1/(2(k+1)) of\nat most one midpoint \u2014 adjacent midpoints are 1/(k+1) apart \u2014 so at most\nk of the k+1 midpoints are blocked). The count input is the perimeter\nhypothesis `ZeroCountProp` (Trudgian 2014 N(T)/S(T), D-062 \u00a74; \u0108\u2080 =\n`C0hat` is D-056 \u00a72's majorant, already in LiSkeleton). [Session-035\nerratum: ZeroCountProp strengthened to the mult-weighted form \u2014 see the\ndef's docstring; `one_le_zeroMult` gives card \u2264 \u03a3 mult.]\n\nL1 (D-036 \u00a73): the kernel kFun n s = (s/(s\u22121))\u207f \u2212 1 satisfies\n * \u2016kFun n s\u2016 \u2264 2 (re s \u2264 1/2: here |s/(s\u22121)| \u2264 1)\n * \u2016kFun n (s+1)\u2016 \u2264 e\u2074 + 1 (re s \u2264 3, n \u2264 (im s)\u00b2: the\n horizontals, |1+1/s| \u2264 1 + (\u03c3+1)/(\u03c3\u00b2+T\u00b2) \u2264 1 + 4/n)\n * \u2016kFun n (s+1)\u2016 \u2264 e^{\u221an/2} + 1 (2\u221an \u2264 re s: the right vertical,\n |1+1/s| \u2264 1 + 1/|s| \u2264 1 + 1/(2\u221an))\n * kFun n (\u22122) = (2/3)\u207f \u2212 1, hence \u2016kFun n (\u22122)\u2016 \u2264 1 (trivial-zero term).\n\nAlso the deferred trivial-zero simplicity (ii\u2032-1b(iii) NOTE): zeroMult(\u22122) = 1,\nvia \u03b6(s) = (s+2)\u00b7G(s) near \u22122 with G(s) = \u039b(s)/H(s),\nH(s) = 4\u00b7\u03c0^{\u2212s/2}\u00b7\u0393(s/2+2)/s (= (s+2)\u00b7\u0393R(s) off s \u2208 {\u22122, 0}), H(\u22122) = \u22122\u03c0 \u2260 0,\n\u039b(\u22122) = \u039b(3) = \u0393R(3)\u00b7\u03b6(3) \u2260 0.\n\nArchive references: D-036 \u00a72\u20133, D-056 \u00a72, D-064 \u00a75 (L3/L1), D-066 \u00a76.\n-/\nimport Mathlib\nimport Zeta23.Statement\nimport Zeta23.RvM.CountByIntegral\nimport NguyenRH1.LiSides\nimport NguyenRH1.LiSkeleton\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The unit ordinate window and the perimeter count hypothesis -/\n\n/-- The nontrivial zeros with ordinate in the unit window [a, a+1]. -/\ndef zeroWindow (a : \u211d) : Set \u2102 :=\n {\u03c1 | IsNontrivialZero \u03c1 \u2227 a \u2264 \u03c1.im \u2227 \u03c1.im \u2264 a + 1}\n\n/-- Finiteness of the unit ordinate window (via Zeta23 `zerosIn_finite`). -/\ntheorem zeroWindow_finite (a : \u211d) : (zeroWindow a).Finite := by\n apply Set.Finite.subset (zerosIn_finite (a - 1) (a + 1))\n intro \u03c1 h\u03c1\n refine \u27e8h\u03c1.1, ?_, h\u03c1.2.2\u27e9\n linarith [h\u03c1.2.1]\n\n/-- A nontrivial zero has multiplicity \u2265 1 (zeroMult is the analytic\norder). Bridges the mult-weighted perimeter count to the plain window\ncardinality (card \u2264 \u03a3 mult). -/\ntheorem one_le_zeroMult {\u03c1 : \u2102} (h\u03c1 : IsNontrivialZero \u03c1) : 1 \u2264 zeroMult \u03c1 := by\n have h\u03c11 : \u03c1 \u2260 1 := by\n rintro rfl\n have h := h\u03c1.2.2\n rw [Complex.one_re] at h\n exact (lt_irrefl (1 : \u211d)) h\n have htop := zeta_order_ne_top_of_ne h\u03c11\n have hne : analyticOrderAt riemannZeta \u03c1 \u2260 0 :=\n (analyticAt_riemannZeta h\u03c11).analyticOrderAt_ne_zero.mpr h\u03c1.1\n exact ENat.toNat_pos hne htop\n\n/-- [PERIMETER \u2014 Trudgian 2014 N(T)/S(T), D-062 \u00a74] The unit-window\nzero-count bound: the multiplicity-weighted count of nontrivial zeros\nwith ordinates in [t, t+1] is at most \u0108\u2080(t+1) (t \u2265 2). Declared\ncounting input for the L3 pigeonhole and the tight R-bound; \u0108\u2080 =\n`C0hat` is D-056 \u00a72's honest majorant (LiSkeleton).\n[Erratum 2026-08-23 (session 035): strengthened from the unweighted\nset-card form `(Nat.card (zeroWindow t) : \u211d) \u2264 \u0108\u2080(t+1)` to the\nmult-weighted form \u2014 Trudgian's N(T) counts zeros with multiplicity,\nand the mult-weighted form is what the 5f/ii\u2032-6 near sums\n(zeroMult-weighted, from `seriesFun`) consume; the set-card encoding\nunder-captured the declared source (a second ii\u2032-1a-class encoding\ndefect, found at the point of consumption). The set-card bound follows\nfrom this form via `one_le_zeroMult` (card \u2264 \u03a3 mult); the two\nconsumers (exists_zero_avoiding_T, exists_gapCircle_radius) adapted.] -/\ndef ZeroCountProp : Prop :=\n \u2200 t : \u211d, 2 \u2264 t \u2192\n (((zeroWindow_finite t).toFinset.sum fun \u03c1 => zeroMult \u03c1) : \u211d) \u2264 C0hat (t + 1)\n\n/-- The two-unit ordinate window: nontrivial zeros with |\u03b3 \u2212 t| \u2264 1. -/\ndef zeroAbsWindow (t : \u211d) : Set \u2102 :=\n {\u03c1 | IsNontrivialZero \u03c1 \u2227 |\u03c1.im - t| \u2264 1}\n\n/-- Finiteness of the two-unit ordinate window (via Zeta23\n`zerosIn_finite`). -/\ntheorem zeroAbsWindow_finite (t : \u211d) : (zeroAbsWindow t).Finite := by\n apply Set.Finite.subset (zerosIn_finite (t - 2) (t + 1))\n intro \u03c1 h\u03c1\n refine \u27e8h\u03c1.1, ?_, ?_\u27e9\n \u00b7 have := h\u03c1.2; linarith [abs_le.mp this]\n \u00b7 have := h\u03c1.2; linarith [abs_le.mp this]\n\n/-- [PERIMETER \u2014 Trudgian 2014 N(T)/S(T), the two-unit specialization,\nD-069 \u00a72] The two-unit window count: the multiplicity-weighted count of\nnontrivial zeros with |\u03b3 \u2212 t| \u2264 1 is at most 0.6\u00b7log(t+2) +\n0.886\u00b7log log(t+2) + 2.7 (t \u2265 10). This is N(t+1) \u2212 N(t\u22121) bounded by\nthe F-difference + S_b-pair: F(t+1)\u2212F(t\u22121) \u2264 (1/\u03c0)\u00b7log((t+1)/2\u03c0) \u2264\n0.31831\u00b7log(t+2) \u2212 0.585 and S_b(t+1)+S_b(t\u22121) \u2264 0.274\u00b7log(t+2) +\n0.886\u00b7log log(t+2) + 3.176, totaling 0.59231\u00b7log(t+2) +\n0.886\u00b7log log(t+2) + 2.591 \u2014 the closed form has 0.008\u00b7log(t+2) + 0.11\nslack. NOT derivable from the per-unit `ZeroCountProp` (the crude double\n2\u00b7\u0108\u2080 has log-coefficient 0.866 > 0.6); declared under the same\nTrudgian-2014 source (D-062 \u00a74 class). [Added session 035 \u2014 5f's piece 2\nconsumes exactly this form; D-069 Finding 1.] -/\ndef ZeroCountProp2 : Prop :=\n \u2200 t : \u211d, 10 \u2264 t \u2192\n (((zeroAbsWindow_finite t).toFinset.sum fun \u03c1 => zeroMult \u03c1) : \u211d) \u2264\n 0.6 * Real.log (t + 2) + 0.886 * Real.log (Real.log (t + 2)) + 2.7\n\n/-- [PERIMETER \u2014 Platt-class zero-location certificate, D-069 \u00a72] There\nare no nontrivial zeros with |\u03b3| \u2264 14: the first nontrivial zero is at\n\u03b3 = 14.134725\u2026. This is the zero-LOCATION content of the\nPlatt\u2013Trudgian-class Turing-method certificate (the same computation\nthat verifies RH to height 3\u00d710\u00b9\u00b2 locates the zeros); it is not implied\nby `RHUpTo` (an on-line statement) nor by the Trudgian count bounds\n(the S_b slack is too large at low height). Declared in the\nPlatt\u2013Trudgian trust class. [Added session 035 \u2014 5f's piece 3\n(far-difference sum) consumes this for the intervals below height 14;\nD-069 Finding/need (P2).] -/\ndef NoLowZeros : Prop :=\n \u2200 \u03c1 : \u2102, IsNontrivialZero \u03c1 \u2192 14 \u2264 |\u03c1.im|\n\n/-- The global ordinate window: nontrivial zeros with 0 < \u03b3 \u2264 T. -/\ndef zeroGlobalWindow (T : \u211d) : Set \u2102 :=\n {\u03c1 | IsNontrivialZero \u03c1 \u2227 0 < \u03c1.im \u2227 \u03c1.im \u2264 T}\n\n/-- Finiteness of the global ordinate window (via Zeta23\n`zerosIn_finite`). -/\ntheorem zeroGlobalWindow_finite (T : \u211d) : (zeroGlobalWindow T).Finite := by\n apply Set.Finite.subset (zerosIn_finite 0 T)\n intro \u03c1 h\u03c1\n refine \u27e8h\u03c1.1, by linarith [h\u03c1.2.1], h\u03c1.2.2\u27e9\n\n/-- [PERIMETER \u2014 Trudgian 2014 N(T) GLOBAL form, D-062 \u00a74 / D-071 \u00a73,\nuser-approved session 038] The global zero-count bound: the\nmultiplicity-weighted count of nontrivial zeros with 0 < \u03b3 \u2264 T is at\nmost FAlt T (T \u2265 2). This is the un-specialized form of the declared\nTrudgian source (`ZeroCountProp` is its unit-window corollary); the\nunit form does NOT imply the global form at the FAlt level (summing\nunit windows gives 0.433\u00b7T\u00b7log T > (1/2\u03c0)\u00b7T\u00b7log T). Used by the ii\u2032-6\nbridge (the both-signs count is 2\u00d7 the one-sign count by conj\nsymmetry, `isNontrivialZero_conj` + `zeroMult_conj`). -/\ndef ZeroCountGlobalProp : Prop :=\n \u2200 T : \u211d, 2 \u2264 T \u2192\n (((zeroGlobalWindow_finite T).toFinset.sum fun \u03c1 => zeroMult \u03c1) : \u211d) \u2264 FAlt T\n\n/-- [PERIMETER \u2014 M\u2080 interval certificate, D-062 \u00a74 L6 / D-071 \u00a73,\nuser-approved session 038] \u2016\u03b6\u2032/\u03b6(\u22125/2 + it)\u2016 \u2264 1.3352 for |t| \u2264 10\n(E-023 grid + sampled-Lipschitz \u00d72 safety; E-023b acb box-cover upgrade\noptional). The same trust class as the Platt\u2013Trudgian certificate\n(interval-arithmetic computation). Used by the I_III short piece\n(|t| \u2264 10 of the left vertical). -/\ndef MZeroProp : Prop :=\n \u2200 t : \u211d, |t| \u2264 10 \u2192\n \u2016logDeriv riemannZeta ((-5 / 2 : \u2102) + (t : \u211d) * Complex.I)\u2016 \u2264 1.3352\n\n/-- \u0108\u2080(t) \u2265 2 for t \u2265 1 (indeed \u2265 3.33: log(t+2) \u2265 1 as t + 2 \u2265 3 > e,\nso log log(t+2) \u2265 0 and the constant 2.9 remains). -/\ntheorem two_le_C0hat {t : \u211d} (ht : 1 \u2264 t) : 2 \u2264 C0hat t := by\n have h3 : (3 : \u211d) \u2264 t + 2 := by linarith\n have hlog : 1 \u2264 Real.log (t + 2) := by\n rw [Real.le_log_iff_exp_le (by positivity : (0:\u211d) < t + 2)]\n have he := Real.exp_one_lt_d9.le\n linarith\n have hloglog : 0 \u2264 Real.log (Real.log (t + 2)) := Real.log_nonneg hlog\n have h1 : (0:\u211d) \u2264 0.433 * Real.log (t + 2) := by positivity\n have h2 : (0:\u211d) \u2264 0.886 * Real.log (Real.log (t + 2)) := by positivity\n unfold C0hat\n linarith\n\n/-! ## 2. The midpoint pigeonhole (pure combinatorics) -/\n\n/-- **Midpoint pigeonhole**: a finset S of reals with card S \u2264 k admits one\nof the k+1 midpoints a + (2j+1)/(2(k+1)) (j < k+1) at distance\n\u2265 1/(2(k+1)) from every point of S. (Each x \u2208 S lies within < 1/(2(k+1))\nof at most one midpoint \u2014 adjacent midpoints are 1/(k+1) apart \u2014 so at\nmost card S \u2264 k of the k+1 midpoints are blocked.) -/\ntheorem exists_avoiding_midpoint {k : \u2115} (a : \u211d) (S : Finset \u211d)\n (hcard : S.card \u2264 k) :\n \u2203 T : \u211d, a \u2264 T \u2227 T \u2264 a + 1 \u2227\n \u2200 x \u2208 S, 1 / (2 * ((k : \u211d) + 1)) \u2264 |x - T| := by\n classical\n set w : \u211d := 1 / (2 * ((k : \u211d) + 1)) with hw_def\n have hk1 : (0:\u211d) < 2 * ((k : \u211d) + 1) := by positivity\n have hw : 0 < w := one_div_pos.mpr hk1\n set c : \u2115 \u2192 \u211d := fun j => a + (2 * (j : \u211d) + 1) * w with hc_def\n -- candidate spread: c i \u2212 c j = 2(i \u2212 j)\u00b7w\n have hcd : \u2200 i j : \u2115, c i - c j = 2 * ((i : \u211d) - (j : \u211d)) * w := fun i j => by\n simp only [hc_def]; ring\n -- each candidate lies in [a, a+1]\n have hc_mem : \u2200 j < k + 1, a \u2264 c j \u2227 c j \u2264 a + 1 := by\n intro j hj\n have hjl : (0:\u211d) \u2264 2 * (j : \u211d) + 1 := by positivity\n have hju : 2 * (j : \u211d) + 1 \u2264 2 * ((k : \u211d) + 1) := by\n have hjk : j \u2264 k := Nat.lt_succ_iff.mp hj\n have : (j : \u211d) \u2264 k := by exact_mod_cast hjk\n linarith\n have h1 : (0:\u211d) \u2264 (2 * (j : \u211d) + 1) * w := mul_nonneg hjl hw.le\n have h2 : (2 * (j : \u211d) + 1) * w \u2264 1 := by\n rw [hw_def, mul_one_div, div_le_one hk1]\n exact hju\n constructor <;> simp only [hc_def] <;> linarith\n -- the bad candidates: those within < w of some point of S\n set Bad : Finset \u2115 := (Finset.range (k + 1)).filter\n (fun j => \u2203 x \u2208 S, |x - c j| < w) with hBad_def\n have hbad_wit : \u2200 j \u2208 Bad, \u2203 x \u2208 S, |x - c j| < w := fun j hj =>\n (Finset.mem_filter.mp hj).2\n choose! f hfS hfw using hbad_wit\n -- distinct bad candidates need distinct witnesses: f is injective on Bad\n have hinj : Set.InjOn f Bad := by\n intro i hi j hj hij\n by_contra hne\n have h1 : |f i - c i| < w := hfw i hi\n have h2 : |f j - c j| < w := hfw j hj\n have hlt : |c i - c j| < 2 * w := by\n have h3 : |c i - c j| \u2264 |c i - f i| + |f i - c j| :=\n abs_sub_le (c i) (f i) (c j)\n rw [abs_sub_comm (c i) (f i)] at h3\n rw [hij] at h1 h3\n linarith\n rw [hcd i j] at hlt\n have hne1 : (1:\u211d) \u2264 |(i : \u211d) - (j : \u211d)| := by\n rcases lt_or_gt_of_ne hne with h | h\n \u00b7 have h4 : (i : \u211d) + 1 \u2264 j := by\n exact_mod_cast Nat.add_one_le_of_lt h\n rw [abs_of_nonpos (by linarith)]\n linarith\n \u00b7 have h4 : (j : \u211d) + 1 \u2264 i := by\n exact_mod_cast Nat.add_one_le_of_lt h\n rw [abs_of_nonneg (by linarith)]\n linarith\n have hge : 2 * w \u2264 |2 * ((i : \u211d) - (j : \u211d)) * w| := by\n rw [abs_mul, abs_mul, abs_of_pos hw, abs_of_pos (by norm_num : (0:\u211d) < 2)]\n nlinarith [hne1, hw]\n linarith\n have hcardBad : Bad.card \u2264 S.card :=\n Finset.card_le_card_of_injOn f (fun j hj => hfS j hj) hinj\n -- some candidate is not bad\n have hlt2 : Bad.card < (Finset.range (k + 1)).card := by\n rw [Finset.card_range]\n exact Nat.lt_succ_of_le (hcardBad.trans hcard)\n obtain \u27e8j, hj, hjB\u27e9 : \u2203 j \u2208 Finset.range (k + 1), j \u2209 Bad := by\n by_contra hcon\n push Not at hcon\n have hsub : Finset.range (k + 1) \u2286 Bad := fun x hx => hcon x hx\n have := Finset.card_le_card hsub\n omega\n have hjk : j < k + 1 := Finset.mem_range.mp hj\n refine \u27e8c j, (hc_mem j hjk).1, (hc_mem j hjk).2, fun x hx => ?_\u27e9\n have hnot : \u00ac |x - c j| < w := by\n intro hlt\n exact hjB (Finset.mem_filter.mpr \u27e8hj, \u27e8x, hx, hlt\u27e9\u27e9)\n have : w \u2264 |x - c j| := not_lt.mp hnot\n rwa [hw_def] at this\n\n/-! ## 3. L3: the zero-avoiding ordinate -/\n\n/-- **L3** (D-036 \u00a72): given the perimeter count bound `ZeroCountProp`,\nevery unit window [a, a+1] with a \u2265 2 contains an ordinate T at distance\n\u2265 1/(3\u00b7\u0108\u2080(a+1)) from every zero ordinate in the window. -/\ntheorem exists_zero_avoiding_T (hZC : ZeroCountProp) {a : \u211d} (ha : 2 \u2264 a) :\n \u2203 T : \u211d, a \u2264 T \u2227 T \u2264 a + 1 \u2227\n \u2200 \u03c1 : \u2102, IsNontrivialZero \u03c1 \u2192 a \u2264 \u03c1.im \u2192 \u03c1.im \u2264 a + 1 \u2192\n 1 / (3 * C0hat (a + 1)) \u2264 |\u03c1.im - T| := by\n classical\n have hfin := zeroWindow_finite a\n set WF : Finset \u2102 := hfin.toFinset with hWF_def\n have hWFmem : \u2200 \u03c1 : \u2102, \u03c1 \u2208 WF \u2194 \u03c1 \u2208 zeroWindow a :=\n fun \u03c1 => Set.Finite.mem_toFinset hfin\n set S : Finset \u211d := WF.image Complex.im with hS_def\n have hScard : S.card \u2264 WF.card := Finset.card_image_le\n have hWFcard : (WF.card : \u211d) \u2264 C0hat (a + 1) := by\n have h1 := hZC a ha\n -- h1 : (\u2211 \u03c1 \u2208 WF, (zeroMult \u03c1 : \u211d)) \u2264 C0hat (a + 1); card \u2264 \u03a3 mult\n have h2 : (WF.card : \u211d) \u2264 \u2211 \u03c1 \u2208 WF, (zeroMult \u03c1 : \u211d) := by\n rw [show (WF.card : \u211d) = \u2211 _\u03c1 \u2208 WF, (1 : \u211d) by simp]\n apply Finset.sum_le_sum\n intro \u03c1 h\u03c1\n exact_mod_cast one_le_zeroMult ((hWFmem \u03c1).mp h\u03c1).1\n exact h2.trans h1\n obtain \u27e8T, hT1, hT2, hT3\u27e9 := exists_avoiding_midpoint a S hScard\n refine \u27e8T, hT1, hT2, fun \u03c1 h\u03c1 h\u03c1a h\u03c1a1 => ?_\u27e9\n have h\u03c1mem : \u03c1 \u2208 WF := (hWFmem \u03c1).mpr \u27e8h\u03c1, h\u03c1a, h\u03c1a1\u27e9\n have himmem : \u03c1.im \u2208 S := Finset.mem_image.mpr \u27e8\u03c1, h\u03c1mem, rfl\u27e9\n have h1 := hT3 \u03c1.im himmem\n have hC : 2 \u2264 C0hat (a + 1) := two_le_C0hat (by linarith)\n have hpos : (0:\u211d) < 2 * ((WF.card : \u211d) + 1) := by positivity\n have hle : 2 * ((WF.card : \u211d) + 1) \u2264 3 * C0hat (a + 1) := by\n linarith [hWFcard]\n exact le_trans (one_div_le_one_div_of_le hpos hle) h1\n\n/-! ## 3b. The wide zero-avoiding ordinate (D-071 Finding-2 repair) -/\n\n/-- The wide ordinate window: nontrivial zeros with ordinate in\n[a\u22121, a+2] (the 3-unit window for the Finding-2-extended pigeonhole \u2014\nzeros just outside [a, a+1] can sit at distance < 1/(3\u0108\u2080) from T). -/\ndef zeroWindowWide (a : \u211d) : Set \u2102 :=\n {\u03c1 | IsNontrivialZero \u03c1 \u2227 a - 1 \u2264 \u03c1.im \u2227 \u03c1.im \u2264 a + 2}\n\n/-- Finiteness of the wide window (union of the three unit windows). -/\ntheorem zeroWindowWide_finite (a : \u211d) : (zeroWindowWide a).Finite := by\n apply Set.Finite.subset ((zeroWindow_finite (a - 1)).union\n ((zeroWindow_finite a).union (zeroWindow_finite (a + 1))))\n intro \u03c1 h\u03c1\n obtain \u27e8hz, hlo, hhi\u27e9 := h\u03c1\n by_cases h1 : \u03c1.im \u2264 a\n \u00b7 exact Or.inl \u27e8hz, hlo, by linarith\u27e9\n \u00b7 by_cases h2 : \u03c1.im \u2264 a + 1\n \u00b7 exact Or.inr (Or.inl \u27e8hz, by linarith, h2\u27e9)\n \u00b7 exact Or.inr (Or.inr \u27e8hz, by linarith, by linarith\u27e9)\n\n/-- The wide window's cardinality \u2264 3\u00b7\u0108\u2080(a+2) (three unit windows via\nthe perimeter + `C0hat_mono`). -/\ntheorem zeroWindowWide_card_le (hZC : ZeroCountProp) {a : \u211d} (ha : 3 \u2264 a) :\n ((zeroWindowWide_finite a).toFinset.card : \u211d) \u2264 3 * C0hat (a + 2) := by\n have hsub : (zeroWindowWide_finite a).toFinset \u2286\n (zeroWindow_finite (a - 1)).toFinset \u222a\n ((zeroWindow_finite a).toFinset \u222a (zeroWindow_finite (a + 1)).toFinset) := by\n intro \u03c1 h\u03c1\n have hmem : \u03c1 \u2208 zeroWindowWide a := (zeroWindowWide_finite a).mem_toFinset.mp h\u03c1\n obtain \u27e8hz, hlo, hhi\u27e9 := hmem\n by_cases h1 : \u03c1.im \u2264 a\n \u00b7 exact Finset.mem_union.mpr (Or.inl\n ((zeroWindow_finite (a - 1)).mem_toFinset.mpr \u27e8hz, hlo, by linarith\u27e9))\n \u00b7 by_cases h2 : \u03c1.im \u2264 a + 1\n \u00b7 exact Finset.mem_union.mpr (Or.inr (Finset.mem_union.mpr (Or.inl\n ((zeroWindow_finite a).mem_toFinset.mpr \u27e8hz, by linarith, h2\u27e9))))\n \u00b7 exact Finset.mem_union.mpr (Or.inr (Finset.mem_union.mpr (Or.inr\n ((zeroWindow_finite (a + 1)).mem_toFinset.mpr \u27e8hz, by linarith, by linarith\u27e9))))\n have hsum1 : (\u2211 \u03c1 \u2208 (zeroWindowWide_finite a).toFinset, (zeroMult \u03c1 : \u211d)) \u2264\n \u2211 \u03c1 \u2208 ((zeroWindow_finite (a - 1)).toFinset \u222a\n ((zeroWindow_finite a).toFinset \u222a (zeroWindow_finite (a + 1)).toFinset)),\n (zeroMult \u03c1 : \u211d) :=\n Finset.sum_le_sum_of_subset_of_nonneg hsub (fun \u03c1 _ _ => Nat.cast_nonneg _)\n have hsum2 : (\u2211 \u03c1 \u2208 ((zeroWindow_finite (a - 1)).toFinset \u222a\n ((zeroWindow_finite a).toFinset \u222a (zeroWindow_finite (a + 1)).toFinset)),\n (zeroMult \u03c1 : \u211d)) \u2264\n (\u2211 \u03c1 \u2208 (zeroWindow_finite (a - 1)).toFinset, (zeroMult \u03c1 : \u211d)) +\n ((\u2211 \u03c1 \u2208 (zeroWindow_finite a).toFinset, (zeroMult \u03c1 : \u211d)) +\n (\u2211 \u03c1 \u2208 (zeroWindow_finite (a + 1)).toFinset, (zeroMult \u03c1 : \u211d))) := by\n have hu1 := Finset.sum_union_inter (s := (zeroWindow_finite (a - 1)).toFinset)\n (t := (zeroWindow_finite a).toFinset \u222a (zeroWindow_finite (a + 1)).toFinset)\n (f := fun \u03c1 => (zeroMult \u03c1 : \u211d))\n have hnn : (0 : \u211d) \u2264 \u2211 \u03c1 \u2208 (zeroWindow_finite (a - 1)).toFinset \u2229\n ((zeroWindow_finite a).toFinset \u222a (zeroWindow_finite (a + 1)).toFinset),\n (zeroMult \u03c1 : \u211d) :=\n Finset.sum_nonneg (fun \u03c1 _ => Nat.cast_nonneg _)\n have hu2 := Finset.sum_union_inter (s := (zeroWindow_finite a).toFinset)\n (t := (zeroWindow_finite (a + 1)).toFinset) (f := fun \u03c1 => (zeroMult \u03c1 : \u211d))\n have hnn2 : (0 : \u211d) \u2264 \u2211 \u03c1 \u2208 (zeroWindow_finite a).toFinset \u2229\n (zeroWindow_finite (a + 1)).toFinset, (zeroMult \u03c1 : \u211d) :=\n Finset.sum_nonneg (fun \u03c1 _ => Nat.cast_nonneg _)\n linarith\n have h1 := hZC (a - 1) (by linarith)\n have h2 := hZC a (by linarith)\n have h3 := hZC (a + 1) (by linarith)\n have hmono1 : C0hat a \u2264 C0hat (a + 2) := C0hat_mono (by linarith) (by linarith)\n have hmono2 : C0hat (a + 1) \u2264 C0hat (a + 2) := C0hat_mono (by linarith) (by linarith)\n have hcard_le_sum : ((zeroWindowWide_finite a).toFinset.card : \u211d) \u2264\n \u2211 \u03c1 \u2208 (zeroWindowWide_finite a).toFinset, (zeroMult \u03c1 : \u211d) := by\n rw [show ((zeroWindowWide_finite a).toFinset.card : \u211d) =\n \u2211 _\u03c1 \u2208 (zeroWindowWide_finite a).toFinset, (1 : \u211d) by simp]\n apply Finset.sum_le_sum\n intro \u03c1 h\u03c1\n exact_mod_cast one_le_zeroMult (((zeroWindowWide_finite a).mem_toFinset.mp h\u03c1).1)\n calc ((zeroWindowWide_finite a).toFinset.card : \u211d)\n \u2264 \u2211 \u03c1 \u2208 (zeroWindowWide_finite a).toFinset, (zeroMult \u03c1 : \u211d) := hcard_le_sum\n _ \u2264 C0hat a + C0hat (a + 1) + C0hat (a + 2) := by linarith [hsum1, hsum2, h1, h2, h3]\n _ \u2264 3 * C0hat (a + 2) := by linarith [hmono1, hmono2]\n\n/-- **L3-wide** (D-071 Finding-2 repair): given the perimeter count\nbound, every unit window [a, a+1] with a \u2265 3 contains an ordinate T at\ndistance \u2265 1/(9\u00b7\u0108\u2080(a+2)) from EVERY zero ordinate in the 3-unit window\n(a\u22121, a+2) \u2014 covering the zeros just outside [a, a+1] that the plain\nL3 clearance misses. -/\ntheorem exists_zero_avoiding_T_wide (hZC : ZeroCountProp) {a : \u211d} (ha : 3 \u2264 a) :\n \u2203 T : \u211d, a \u2264 T \u2227 T \u2264 a + 1 \u2227\n \u2200 \u03c1 : \u2102, IsNontrivialZero \u03c1 \u2192 a - 1 < \u03c1.im \u2192 \u03c1.im < a + 2 \u2192\n 1 / (9 * C0hat (a + 2)) \u2264 |\u03c1.im - T| := by\n classical\n have hfin := zeroWindowWide_finite a\n set WF : Finset \u2102 := hfin.toFinset with hWF_def\n have hWFmem : \u2200 \u03c1 : \u2102, \u03c1 \u2208 WF \u2194 \u03c1 \u2208 zeroWindowWide a :=\n fun \u03c1 => Set.Finite.mem_toFinset hfin\n set S : Finset \u211d := WF.image Complex.im with hS_def\n have hScard : S.card \u2264 WF.card := Finset.card_image_le\n have hWFcard : (WF.card : \u211d) \u2264 3 * C0hat (a + 2) := zeroWindowWide_card_le hZC ha\n obtain \u27e8T, hT1, hT2, hT3\u27e9 := exists_avoiding_midpoint a S hScard\n refine \u27e8T, hT1, hT2, fun \u03c1 h\u03c1 h\u03c1lo h\u03c1hi => ?_\u27e9\n have h\u03c1mem : \u03c1 \u2208 WF := (hWFmem \u03c1).mpr \u27e8h\u03c1, by linarith, by linarith\u27e9\n have himmem : \u03c1.im \u2208 S := Finset.mem_image.mpr \u27e8\u03c1, h\u03c1mem, rfl\u27e9\n have h1 := hT3 \u03c1.im himmem\n have hC : 2 \u2264 C0hat (a + 2) := two_le_C0hat (by linarith)\n have hpos : (0:\u211d) < 2 * ((WF.card : \u211d) + 1) := by positivity\n have hle : 2 * ((WF.card : \u211d) + 1) \u2264 9 * C0hat (a + 2) := by\n linarith [hWFcard, hC]\n exact le_trans (one_div_le_one_div_of_le hpos hle) h1\n\n/-! ## 4. L1: kernel norm bounds (D-036 \u00a73) -/\n\n/-- On re s \u2264 1/2 the ratio satisfies \u2016s/(s\u22121)\u2016 \u2264 1 (i.e. \u2016s\u2016 \u2264 \u2016s\u22121\u2016:\nre s \u2264 1/2 \u27fa 0 \u2264 1 \u2212 2\u00b7re s \u27fa re s\u00b2 + im s\u00b2 \u2264 (re s \u2212 1)\u00b2 + im s\u00b2). -/\ntheorem norm_div_sub_one_le_one {s : \u2102} (hs : s.re \u2264 1 / 2) : \u2016s / (s - 1)\u2016 \u2264 1 := by\n have hs1 : s \u2260 1 := by\n rintro h\n rw [h] at hs\n simp only [Complex.one_re] at hs\n norm_num at hs\n have hnorm : \u2016s\u2016 \u2264 \u2016s - 1\u2016 := by\n have h : \u2016s\u2016 ^ 2 \u2264 \u2016s - 1\u2016 ^ 2 := by\n rw [\u2190 Complex.normSq_eq_norm_sq, \u2190 Complex.normSq_eq_norm_sq]\n rw [Complex.normSq_apply s, Complex.normSq_apply (s - 1)]\n simp only [sub_re, one_re, sub_im, one_im, sub_zero]\n nlinarith [hs]\n exact (sq_le_sq\u2080 (norm_nonneg _) (norm_nonneg _)).mp h\n have hpos : (0:\u211d) < \u2016s - 1\u2016 := norm_pos_iff.mpr (sub_ne_zero.mpr hs1)\n rw [norm_div]\n exact (div_le_one hpos).mpr hnorm\n\n/-- **L1 (left side)**: \u2016kFun n s\u2016 \u2264 2 for re s \u2264 1/2 (D-036 \u00a73 (III)). -/\ntheorem kFun_norm_le_two {n : \u2115} {s : \u2102} (hs : s.re \u2264 1 / 2) : \u2016kFun n s\u2016 \u2264 2 := by\n have h1 := norm_div_sub_one_le_one hs\n have h2 : \u2016(s / (s - 1)) ^ n\u2016 \u2264 1 := by\n rw [norm_pow]\n exact pow_le_one\u2080 (norm_nonneg _) h1\n calc \u2016kFun n s\u2016 = \u2016(s / (s - 1)) ^ n - 1\u2016 := rfl\n _ \u2264 \u2016(s / (s - 1)) ^ n\u2016 + \u2016(1 : \u2102)\u2016 := norm_sub_le _ _\n _ \u2264 1 + 1 := by rw [norm_one]; linarith [h2]\n _ = 2 := by norm_num\n\n/-- kFun at the shifted point: kFun n (s+1) = (1 + 1/s)\u207f \u2212 1 (s \u2260 0). -/\ntheorem kFun_add_one {n : \u2115} {s : \u2102} (hs : s \u2260 0) :\n kFun n (s + 1) = (1 + 1 / s) ^ n - 1 := by\n have e : (s + 1) / (s + 1 - 1) = 1 + 1 / s := by\n rw [show s + 1 - 1 = s by ring]\n field_simp\n unfold kFun\n rw [e]\n\n/-- The horizontal core estimate: \u20161 + 1/s\u2016 \u2264 1 + (re s + 1)/normSq s.\nFrom \u20161+1/s\u2016\u00b2 = 1 + (2\u03c3+1)/D \u2264 (1+(\u03c3+1)/D)\u00b2 with D = normSq s = \u03c3\u00b2 + T\u00b2. -/\ntheorem norm_one_add_one_div_le {s : \u2102} (hs : s \u2260 0) :\n \u20161 + 1 / s\u2016 \u2264 1 + (s.re + 1) / Complex.normSq s := by\n set D := Complex.normSq s with hD_def\n have hD : (0:\u211d) < D := Complex.normSq_pos.mpr hs\n have hD_rel : D = s.re * s.re + s.im * s.im := by rw [hD_def, Complex.normSq_apply s]\n have h1 : (1 + 1 / s).re = 1 + s.re / D := by\n simp [Complex.add_re, Complex.one_re, hD_def]\n have h2 : (1 + 1 / s).im = -s.im / D := by\n simp [Complex.add_im, Complex.one_im, hD_def]\n have hsq : Complex.normSq (1 + 1 / s) = 1 + (2 * s.re + 1) / D := by\n rw [Complex.normSq_apply (1 + 1 / s), h1, h2]\n field_simp [hD.ne']\n nlinarith [hD_rel]\n have hRHS : (0:\u211d) \u2264 1 + (s.re + 1) / D := by\n have hsum : (0:\u211d) < D + (s.re + 1) := by\n nlinarith [sq_nonneg (s.re + 1 / 2), sq_nonneg s.im, hD_rel]\n have e : 1 + (s.re + 1) / D = (D + (s.re + 1)) / D := by field_simp [hD.ne']\n rw [e]\n exact div_nonneg hsum.le hD.le\n have hcmp : \u20161 + 1 / s\u2016 ^ 2 \u2264 (1 + (s.re + 1) / D) ^ 2 := by\n rw [\u2190 Complex.normSq_eq_norm_sq, hsq]\n have e : (1 + (s.re + 1) / D) ^ 2\n = 1 + (2 * s.re + 1) / D + (1 / D + ((s.re + 1) / D) ^ 2) := by\n field_simp [hD.ne']\n ring\n rw [e]\n have hpos : (0:\u211d) \u2264 1 / D + ((s.re + 1) / D) ^ 2 := by positivity\n linarith\n exact (sq_le_sq\u2080 (norm_nonneg _) hRHS).mp hcmp\n\n/-- **L1 (horizontals)**: \u2016kFun n (s+1)\u2016 \u2264 e\u2074 + 1 for re s \u2264 3 and\nn \u2264 (im s)\u00b2 (D-036 \u00a73 (II),(IV)): then |1+1/s| \u2264 1 + 4/n, and\n(1 + 4/n)\u207f \u2264 (e^{4/n})\u207f = e\u2074. -/\ntheorem kFun_shift_norm_le_exp_four_add_one {n : \u2115} {s : \u2102}\n (h\u03c3 : s.re \u2264 3) (hT : (n : \u211d) \u2264 s.im ^ 2) :\n \u2016kFun n (s + 1)\u2016 \u2264 Real.exp 4 + 1 := by\n rcases Nat.eq_zero_or_pos n with hn | hn\n \u00b7 subst hn\n simp only [kFun, pow_zero, sub_self, norm_zero]\n positivity\n \u00b7 have hnR : (1:\u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have hTim : 0 < s.im ^ 2 := by nlinarith [hT, hnR]\n have hs0 : s \u2260 0 := by\n rintro h\n rw [h, Complex.zero_im] at hTim\n norm_num at hTim\n have hD : (0:\u211d) < Complex.normSq s := Complex.normSq_pos.mpr hs0\n have hDn : (n:\u211d) \u2264 Complex.normSq s := by\n rw [Complex.normSq_apply s]\n nlinarith [hT, sq_nonneg s.re]\n have hle : \u20161 + 1 / s\u2016 \u2264 1 + 4 / (n : \u211d) := by\n refine (norm_one_add_one_div_le hs0).trans ?_\n have h\u03c34 : s.re + 1 \u2264 4 := by linarith\n have h4 : (s.re + 1) / Complex.normSq s \u2264 4 / (n : \u211d) := by\n by_cases h\u03c3p : 0 \u2264 s.re + 1\n \u00b7 calc (s.re + 1) / Complex.normSq s \u2264 4 / Complex.normSq s :=\n (div_le_div_iff_of_pos_right hD).mpr h\u03c34\n _ \u2264 4 / (n : \u211d) :=\n (div_le_div_iff_of_pos_left (by norm_num) hD (by positivity)).mpr hDn\n \u00b7 have hneg : (s.re + 1) / Complex.normSq s \u2264 0 :=\n div_nonpos_of_nonpos_of_nonneg (not_le.mp h\u03c3p).le hD.le\n have hpos4 : (0:\u211d) \u2264 4 / (n : \u211d) := by positivity\n linarith\n linarith [h4]\n have hpow : \u20161 + 1 / s\u2016 ^ n \u2264 Real.exp 4 := by\n calc \u20161 + 1 / s\u2016 ^ n \u2264 (1 + 4 / (n : \u211d)) ^ n :=\n pow_le_pow_left\u2080 (norm_nonneg _) hle n\n _ \u2264 (Real.exp (4 / (n : \u211d))) ^ n := by\n have h := Real.add_one_le_exp (4 / (n : \u211d))\n exact pow_le_pow_left\u2080 (by positivity) (by linarith) n\n _ = Real.exp 4 := by\n rw [\u2190 Real.exp_nat_mul]\n congr 1\n have hn0 : (n : \u211d) \u2260 0 := by exact_mod_cast hn.ne'\n field_simp [hn0]\n rw [kFun_add_one hs0]\n calc \u2016(1 + 1 / s) ^ n - 1\u2016 \u2264 \u2016(1 + 1 / s) ^ n\u2016 + \u2016(1 : \u2102)\u2016 := norm_sub_le _ _\n _ = \u20161 + 1 / s\u2016 ^ n + 1 := by rw [norm_pow, norm_one]\n _ \u2264 Real.exp 4 + 1 := by linarith [hpow]\n\n/-- **L1 (right vertical)**: \u2016kFun n (s+1)\u2016 \u2264 e^{\u221an/2} + 1 for 0 < n and\n2\u221an \u2264 re s (D-036 \u00a73 (I)): then |1+1/s| \u2264 1 + 1/(2\u221an), whose n-th power\nis \u2264 e^{n/(2\u221an)} = e^{\u221an/2}. -/\ntheorem kFun_shift_norm_le_exp_sqrt_half_add_one {n : \u2115} {s : \u2102}\n (hn : 0 < n) (h\u03c3 : 2 * Real.sqrt (n : \u211d) \u2264 s.re) :\n \u2016kFun n (s + 1)\u2016 \u2264 Real.exp (Real.sqrt (n : \u211d) / 2) + 1 := by\n have hnR : (0:\u211d) < (n : \u211d) := by exact_mod_cast hn\n have hsqrt : 0 < Real.sqrt (n : \u211d) := Real.sqrt_pos.mpr hnR\n have hre0 : (0:\u211d) \u2264 s.re := by linarith [hsqrt.le]\n have hnorm_s : 2 * Real.sqrt (n : \u211d) \u2264 \u2016s\u2016 :=\n h\u03c3.trans (abs_of_nonneg hre0 \u25b8 Complex.abs_re_le_norm s)\n have hs0 : s \u2260 0 := by\n rintro h\n rw [h, norm_zero] at hnorm_s\n linarith [hsqrt]\n have hnorm_pos : (0:\u211d) < \u2016s\u2016 := by linarith [hsqrt]\n have h1 : \u20161 + 1 / s\u2016 \u2264 1 + 1 / (2 * Real.sqrt (n : \u211d)) := by\n calc \u20161 + 1 / s\u2016 \u2264 \u2016(1 : \u2102)\u2016 + \u20161 / s\u2016 := norm_add_le _ _\n _ = 1 + 1 / \u2016s\u2016 := by rw [norm_one, norm_div, norm_one]\n _ \u2264 1 + 1 / (2 * Real.sqrt (n : \u211d)) := by\n have h := (div_le_div_iff_of_pos_left one_pos hnorm_pos\n (by positivity : (0:\u211d) < 2 * Real.sqrt (n : \u211d))).mpr hnorm_s\n linarith [h]\n have hpow : \u20161 + 1 / s\u2016 ^ n \u2264 Real.exp (Real.sqrt (n : \u211d) / 2) := by\n calc \u20161 + 1 / s\u2016 ^ n \u2264 (1 + 1 / (2 * Real.sqrt (n : \u211d))) ^ n :=\n pow_le_pow_left\u2080 (norm_nonneg _) h1 n\n _ \u2264 (Real.exp (1 / (2 * Real.sqrt (n : \u211d)))) ^ n := by\n have h := Real.add_one_le_exp (1 / (2 * Real.sqrt (n : \u211d)))\n exact pow_le_pow_left\u2080 (by positivity) (by linarith) n\n _ = Real.exp (Real.sqrt (n : \u211d) / 2) := by\n rw [\u2190 Real.exp_nat_mul]\n congr 1\n rw [mul_one_div, div_eq_div_iff (by positivity : (2 * Real.sqrt (n : \u211d)) \u2260 0)\n (by norm_num : (2 : \u211d) \u2260 0)]\n nlinarith [Real.mul_self_sqrt hnR.le]\n rw [kFun_add_one hs0]\n calc \u2016(1 + 1 / s) ^ n - 1\u2016 \u2264 \u2016(1 + 1 / s) ^ n\u2016 + \u2016(1 : \u2102)\u2016 := norm_sub_le _ _\n _ = \u20161 + 1 / s\u2016 ^ n + 1 := by rw [norm_pow, norm_one]\n _ \u2264 Real.exp (Real.sqrt (n : \u211d) / 2) + 1 := by linarith [hpow]\n\n/-- **L1 (trivial-zero term)**: kFun n (\u22122) = (2/3)\u207f \u2212 1. -/\ntheorem kFun_neg_two (n : \u2115) : kFun n (-2) = (2 / 3 : \u2102) ^ n - 1 := by\n unfold kFun\n norm_num\n\n/-- The trivial-zero contribution is harmless: \u2016kFun n (\u22122)\u2016 \u2264 1\n(it equals 1 \u2212 (2/3)\u207f as a real absolute value). -/\ntheorem norm_kFun_neg_two_le_one (n : \u2115) : \u2016kFun n (-2)\u2016 \u2264 1 := by\n rw [kFun_neg_two]\n have h23 : (2 / 3 : \u2102) = ((2 / 3 : \u211d) : \u2102) := by norm_num\n rw [h23]\n have h : (((2 / 3 : \u211d) : \u2102) ^ n - 1) = (((2 / 3 : \u211d) ^ n - 1 : \u211d) : \u2102) := by\n push_cast\n ring\n rw [h, Complex.norm_real, Real.norm_eq_abs]\n have h01 : (0:\u211d) \u2264 (2 / 3 : \u211d) ^ n := by positivity\n have h1le : (2 / 3 : \u211d) ^ n \u2264 1 := pow_le_one\u2080 (by norm_num) (by norm_num)\n rw [abs_of_nonpos (by linarith)]\n linarith\n\n/-! ## 5. Trivial-zero simplicity: zeroMult (\u22122) = 1 -/\n\n/-- The local factor of \u0393R at \u22122: Hfun s = 4\u00b7\u03c0^{\u2212s/2}\u00b7\u0393(s/2+2)/s. Equals\n(s+2)\u00b7\u0393R(s) off {\u22122, 0} (by `Gamma_add_one` twice); analytic at \u22122 with\nHfun(\u22122) = \u22122\u03c0 \u2260 0. This is the nonvanishing cofactor in the local\nfactorization \u03b6(s) = (s+2)\u00b7(\u039b(s)/Hfun(s)) proving zeroMult(\u22122) = 1. -/\ndef Hfun (s : \u2102) : \u2102 := 4 * (Real.pi : \u2102) ^ (-s / 2) * Complex.Gamma (s / 2 + 2) / s\n\n/-- Hfun is analytic at \u22122: on ball(\u22122, 1) the point s/2+2 avoids the\nGamma poles {0, \u22121, \u22122, \u2026} (it lies in ball(1, 1/2)). -/\ntheorem Hfun_analyticAt_neg_two : AnalyticAt \u2102 Hfun (-2) := by\n have hcpi : AnalyticAt \u2102 (fun s : \u2102 => (Real.pi : \u2102) ^ (-s / 2)) (-2) := by\n have hexp : AnalyticAt \u2102\n (fun s : \u2102 => Complex.exp ((Complex.log (Real.pi : \u2102) * (-1 / 2)) * s)) (-2) :=\n (analyticAt_const.mul analyticAt_id).cexp\n apply hexp.congr\n filter_upwards with s\n rw [Complex.cpow_def_of_ne_zero (by norm_num : (Real.pi : \u2102) \u2260 0)]\n ring_nf\n have hGamma : AnalyticAt \u2102 (fun s : \u2102 => Complex.Gamma (s / 2 + 2)) (-2) := by\n have hd : DifferentiableOn \u2102 (fun s : \u2102 => Complex.Gamma (s / 2 + 2))\n (Metric.ball (-2 : \u2102) (1 : \u211d)) := by\n intro s hs\n have hg : DifferentiableAt \u2102 Complex.Gamma (s / 2 + 2) := by\n apply Complex.differentiableAt_Gamma\n intro m hm\n have hs_eq : s = -2 * (m : \u2102) - 4 := by linear_combination 2 * hm\n rw [hs_eq, Metric.mem_ball, dist_eq_norm] at hs\n have h1 : ((-2 : \u2102) * (m : \u2102) - 4) - -2\n = -(((2 : \u211d) * m + 2 : \u211d) : \u2102) := by push_cast; ring\n rw [h1, norm_neg, Complex.norm_real, Real.norm_eq_abs] at hs\n rw [abs_of_nonneg (by positivity : (0:\u211d) \u2264 2 * (m : \u211d) + 2)] at hs\n have hge : (2:\u211d) \u2264 2 * (m : \u211d) + 2 := by\n have hm0 : (0:\u211d) \u2264 (m : \u211d) := by positivity\n linarith\n linarith\n exact (hg.comp s\n (show DifferentiableAt \u2102 (fun s : \u2102 => s / 2 + 2) s from by fun_prop)).differentiableWithinAt\n have hball : (-2 : \u2102) \u2208 Metric.ball (-2 : \u2102) (1 : \u211d) :=\n Metric.mem_ball_self (zero_lt_one : (0:\u211d) < 1)\n exact (hd.analyticOnNhd Metric.isOpen_ball) _ hball\n show AnalyticAt \u2102 (fun s : \u2102 => 4 * (Real.pi : \u2102) ^ (-s / 2) *\n Complex.Gamma (s / 2 + 2) / s) (-2)\n exact ((analyticAt_const.mul hcpi).mul hGamma).div analyticAt_id (by norm_num)\n\n/-- Hfun(\u22122) = \u22122\u03c0 (via \u0393(1) = 1 and \u03c0^1 = \u03c0). -/\ntheorem Hfun_neg_two : Hfun (-2) = -2 * (Real.pi : \u2102) := by\n unfold Hfun\n rw [show (-(-2 : \u2102) / 2) = 1 by norm_num, Complex.cpow_one,\n show ((-2 : \u2102) / 2 + 2) = 1 by norm_num, Complex.Gamma_one, mul_one]\n field_simp\n ring\n\n/-- Hfun(\u22122) \u2260 0. -/\ntheorem Hfun_neg_two_ne_zero : Hfun (-2) \u2260 0 := by\n rw [Hfun_neg_two]\n norm_num [Real.pi_ne_zero]\n\n/-- The punctured identity: (s+2)\u00b7\u0393R(s) = Hfun s for s \u2209 {\u22122, 0}\n(Gamma_add_one applied twice: \u0393(s/2) = \u0393(s/2+2)/((s/2)(s/2+1))). -/\ntheorem Hfun_eq (s : \u2102) (hs2 : s \u2260 -2) (hs0 : s \u2260 0) :\n (s + 2) * Complex.Gamma\u211d s = Hfun s := by\n have h2ne : s / 2 \u2260 0 := div_ne_zero hs0 (by norm_num)\n have h21ne : s / 2 + 1 \u2260 0 := by\n intro h\n apply hs2\n linear_combination 2 * h\n have h1 := Complex.Gamma_add_one (s / 2) h2ne\n have h2 : Complex.Gamma (s / 2 + 2) = (s / 2 + 1) * Complex.Gamma (s / 2 + 1) := by\n rw [show s / 2 + 2 = (s / 2 + 1) + 1 by ring]\n exact Complex.Gamma_add_one _ h21ne\n have hG : Complex.Gamma (s / 2)\n = Complex.Gamma (s / 2 + 2) / ((s / 2) * (s / 2 + 1)) := by\n have h12 : Complex.Gamma (s / 2 + 2)\n = (s / 2 + 1) * (s / 2) * Complex.Gamma (s / 2) := by\n rw [h2, h1]; ring\n rw [h12, mul_comm (s / 2 + 1) (s / 2)]\n exact (mul_div_cancel_left\u2080 _ (mul_ne_zero h2ne h21ne)).symm\n rw [Complex.Gamma\u211d_def, hG]\n unfold Hfun\n have hs2' : s + 2 \u2260 0 := by\n rw [ne_eq, add_eq_zero_iff_eq_neg]\n exact hs2\n field_simp [hs0, hs2', mul_ne_zero h2ne h21ne]\n ring\n\n/-- **Trivial-zero simplicity** (deferred from ii\u2032-1b(iii), route D-066 \u00a76):\nzeroMult(\u22122) = 1. The local factorization \u03b6(s) = (s+2)\u00b7G(s) holds near \u22122\nwith G(s) = \u039b(s)/Hfun(s) analytic and G(\u22122) = \u039b(\u22122)/(\u22122\u03c0) \u2260 0, since\n\u039b(\u22122) = \u039b(3) = \u0393R(3)\u00b7\u03b6(3) \u2260 0 (functional equation + \u0393R(3) \u2260 0 via\n`Gamma\u211d_eq_zero_iff` + `riemannZeta_ne_zero_of_one_lt_re`). -/\ntheorem zeroMult_neg_two : zeroMult (-2) = 1 := by\n have hHfun_an : AnalyticAt \u2102 Hfun (-2) := Hfun_analyticAt_neg_two\n have hHfun_ne : Hfun (-2) \u2260 0 := Hfun_neg_two_ne_zero\n have h\u039b_an : AnalyticAt \u2102 completedRiemannZeta (-2) := by\n have hd : DifferentiableOn \u2102 completedRiemannZeta (Metric.ball (-2) 1) := by\n intro s hs\n have hs0 : s \u2260 0 := by\n rintro h\n rw [h, Metric.mem_ball, dist_eq_norm] at hs\n have e : ((0 : \u2102) - -2) = ((2 : \u211d) : \u2102) := by norm_num\n rw [e, Complex.norm_real, Real.norm_eq_abs] at hs\n norm_num at hs\n have hs1 : s \u2260 1 := by\n rintro h\n rw [h, Metric.mem_ball, dist_eq_norm] at hs\n have e : ((1 : \u2102) - -2) = ((3 : \u211d) : \u2102) := by norm_num\n rw [e, Complex.norm_real, Real.norm_eq_abs] at hs\n norm_num at hs\n exact (differentiableAt_completedZeta hs0 hs1).differentiableWithinAt\n exact (hd.analyticOnNhd Metric.isOpen_ball) (-2) (Metric.mem_ball_self zero_lt_one)\n have h\u039b_ne : completedRiemannZeta (-2) \u2260 0 := by\n have h\u0393R3 : Complex.Gamma\u211d 3 \u2260 0 := by\n rw [ne_eq, Complex.Gamma\u211d_eq_zero_iff]\n rintro \u27e8m, hm\u27e9\n have hre := congrArg Complex.re hm\n norm_num [Complex.neg_re, Complex.mul_re] at hre\n have hm0 : (0:\u211d) \u2264 (m : \u211d) := by positivity\n linarith\n have h\u03b63 : riemannZeta 3 \u2260 0 :=\n riemannZeta_ne_zero_of_one_lt_re (by norm_num)\n have h\u039b3 : completedRiemannZeta 3 \u2260 0 := by\n rw [RvM.completedRiemannZeta_eq_Gamma\u211d_mul (by norm_num) h\u0393R3]\n exact mul_ne_zero h\u0393R3 h\u03b63\n have hfe : completedRiemannZeta (-2) = completedRiemannZeta 3 := by\n have h := completedRiemannZeta_one_sub (-2 : \u2102)\n norm_num at h\n exact h.symm\n rw [hfe]\n exact h\u039b3\n have hG_an : AnalyticAt \u2102 (fun s => completedRiemannZeta s / Hfun s) (-2) :=\n h\u039b_an.div hHfun_an hHfun_ne\n have hG_ne : completedRiemannZeta (-2) / Hfun (-2) \u2260 0 :=\n div_ne_zero h\u039b_ne hHfun_ne\n have hEv : \u2200\u1da0 s in \ud835\udcdd (-2 : \u2102),\n riemannZeta s = (s - -2) ^ 1 \u2022 (completedRiemannZeta s / Hfun s) := by\n have hHne_ev : \u2200\u1da0 s in \ud835\udcdd (-2 : \u2102), Hfun s \u2260 0 :=\n hHfun_an.continuousAt.eventually_ne hHfun_ne\n filter_upwards [Metric.ball_mem_nhds (-2) (zero_lt_one : (0:\u211d) < 1), hHne_ev]\n with s hs1 hHne\n by_cases hs : s = -2\n \u00b7 subst hs\n have hz0 : riemannZeta (-2) = 0 := by\n have h := riemannZeta_neg_two_mul_nat_add_one 0\n norm_num at h\n exact h\n rw [hz0]\n simp\n \u00b7 have hs0 : s \u2260 0 := by\n rintro h\n rw [h, Metric.mem_ball, dist_eq_norm] at hs1\n have e : ((0 : \u2102) - -2) = ((2 : \u211d) : \u2102) := by norm_num\n rw [e, Complex.norm_real, Real.norm_eq_abs] at hs1\n norm_num at hs1\n have h\u0393R : Complex.Gamma\u211d s \u2260 0 := by\n rw [ne_eq, Complex.Gamma\u211d_eq_zero_iff]\n rintro \u27e8m, hm\u27e9\n rcases Nat.eq_zero_or_pos m with hm0 | hmpos\n \u00b7 subst hm0\n norm_num at hm\n exact hs0 hm\n \u00b7 rcases eq_or_ne m 1 with hm1 | hm1\n \u00b7 subst hm1\n norm_num at hm\n exact hs hm\n \u00b7 have hm2 : 2 \u2264 m := by omega\n rw [hm, Metric.mem_ball, dist_eq_norm] at hs1\n have h1 : (-(2 * (m : \u2102))) - -2 = (((2 : \u211d) - 2 * m : \u211d) : \u2102) := by\n push_cast\n ring\n rw [h1, Complex.norm_real, Real.norm_eq_abs] at hs1\n have hle : (2:\u211d) - 2 * (m : \u211d) \u2264 0 := by\n have hmR : (2:\u211d) \u2264 (m : \u211d) := by exact_mod_cast hm2\n linarith\n rw [abs_of_nonpos hle] at hs1\n have hmR : (2:\u211d) \u2264 (m : \u211d) := by exact_mod_cast hm2\n nlinarith\n have h\u039b := RvM.completedRiemannZeta_eq_Gamma\u211d_mul hs0 h\u0393R\n have hH : (s + 2) * Complex.Gamma\u211d s = Hfun s := Hfun_eq s hs hs0\n rw [pow_one, smul_eq_mul, show s - -2 = s + 2 by ring]\n have hz : riemannZeta s = completedRiemannZeta s / Complex.Gamma\u211d s := by\n rw [h\u039b, mul_div_cancel_left\u2080 _ h\u0393R]\n rw [hz, \u2190 mul_div_assoc, div_eq_div_iff h\u0393R hHne, \u2190 hH]\n ring\n have hRHS_an : AnalyticAt \u2102\n (fun s => (s - -2) ^ 1 \u2022 (completedRiemannZeta s / Hfun s)) (-2) :=\n ((analyticAt_id.sub analyticAt_const).pow 1).smul hG_an\n have hzeta_an : AnalyticAt \u2102 riemannZeta (-2) := hRHS_an.congr (EventuallyEq.symm hEv)\n have horder : analyticOrderAt riemannZeta (-2) = 1 :=\n (hzeta_an.analyticOrderAt_eq_natCast).mpr\n \u27e8fun s => completedRiemannZeta s / Hfun s, hG_an, hG_ne, hEv\u27e9\n rw [zeroMult, horder]\n exact ENat.toNat_one\n\nend NguyenRH1\n\nend\n",
"structuredPatch": [
{
"oldStart": 348,
"oldLines": 24,
"newStart": 348,
"newLines": 42,
"lines": [
" (\u2211 \u03c1 \u2208 (zeroWindow_finite (a - 1)).toFinset, (zeroMult \u03c1 : \u211d)) +",
" ((\u2211 \u03c1 \u2208 (zeroWindow_finite a).toFinset, (zeroMult \u03c1 : \u211d)) +",
" (\u2211 \u03c1 \u2208 (zeroWindow_finite (a + 1)).toFinset, (zeroMult \u03c1 : \u211d))) := by",
"- have hu1 := Finset.sum_union_inter (s := (zeroWindow_finite (a - 1)).toFinset)",
"- (t := (zeroWindow_finite a).toFinset \u222a (zeroWindow_finite (a + 1)).toFinset)",
"+ have hu1 := Finset.sum_union_inter (s\u2081 := (zeroWindow_finite (a - 1)).toFinset)",
"+ (s\u2082 := (zeroWindow_finite a).toFinset \u222a (zeroWindow_finite (a + 1)).toFinset)",
" (f := fun \u03c1 => (zeroMult \u03c1 : \u211d))",
" have hnn : (0 : \u211d) \u2264 \u2211 \u03c1 \u2208 (zeroWindow_finite (a - 1)).toFinset \u2229",
" ((zeroWindow_finite a).toFinset \u222a (zeroWindow_finite (a + 1)).toFinset),",
" (zeroMult \u03c1 : \u211d) :=",
" Finset.sum_nonneg (fun \u03c1 _ => Nat.cast_nonneg _)",
"- have hu2 := Finset.sum_union_inter (s := (zeroWindow_finite a).toFinset)",
"- (t := (zeroWindow_finite (a + 1)).toFinset) (f := fun \u03c1 => (zeroMult \u03c1 : \u211d))",
"+ have hu2 := Finset.sum_union_inter (s\u2081 := (zeroWindow_finite a).toFinset)",
"+ (s\u2082 := (zeroWindow_finite (a + 1)).toFinset) (f := fun \u03c1 => (zeroMult \u03c1 : \u211d))",
" have hnn2 : (0 : \u211d) \u2264 \u2211 \u03c1 \u2208 (zeroWindow_finite a).toFinset \u2229",
" (zeroWindow_finite (a + 1)).toFinset, (zeroMult \u03c1 : \u211d) :=",
" Finset.sum_nonneg (fun \u03c1 _ => Nat.cast_nonneg _)",
" linarith",
"- have h1 := hZC (a - 1) (by linarith)",
"+ have h1 : (\u2211 \u03c1 \u2208 (zeroWindow_finite (a - 1)).toFinset, (zeroMult \u03c1 : \u211d)) \u2264",
"+ C0hat a := by",
"+ have h := hZC (a - 1) (by linarith)",
"+ rwa [show a - 1 + 1 = a from by ring] at h",
" have h2 := hZC a (by linarith)",
"- have h3 := hZC (a + 1) (by linarith)",
"- have hmono1 : C0hat a \u2264 C0hat (a + 2) := C0hat_mono (by linarith) (by linarith)",
"- have hmono2 : C0hat (a + 1) \u2264 C0hat (a + 2) := C0hat_mono (by linarith) (by linarith)",
"+ have h3 : (\u2211 \u03c1 \u2208 (zeroWindow_finite (a + 1)).toFinset, (zeroMult \u03c1 : \u211d)) \u2264",
"+ C0hat (a + 2) := by",
"+ have h := hZC (a + 1) (by linarith)",
"+ rwa [show a + 1 + 1 = a + 2 from by ring] at h",
"+ have hlog1 : Real.log (a + 2) \u2264 Real.log (a + 2 + 2) :=",
"+ Real.log_le_log (by positivity) (by linarith)",
"+ have hlog2 : Real.log (Real.log (a + 2)) \u2264 Real.log (Real.log (a + 2 + 2)) :=",
"+ Real.log_le_log (Real.log_pos (by linarith)) hlog1",
"+ have hmono1 : C0hat a \u2264 C0hat (a + 2) := by",
"+ unfold C0hat",
"+ linarith [hlog1, hlog2]",
"+ have hmono2 : C0hat (a + 1) \u2264 C0hat (a + 2) := by",
"+ unfold C0hat",
"+ have h1' : Real.log (a + 1 + 2) \u2264 Real.log (a + 2 + 2) :=",
"+ Real.log_le_log (by positivity) (by linarith)",
"+ have h2' : Real.log (Real.log (a + 1 + 2)) \u2264 Real.log (Real.log (a + 2 + 2)) :=",
"+ Real.log_le_log (Real.log_pos (by linarith)) h1'",
"+ linarith [h1', h2']",
" have hcard_le_sum : ((zeroWindowWide_finite a).toFinset.card : \u211d) \u2264",
" \u2211 \u03c1 \u2208 (zeroWindowWide_finite a).toFinset, (zeroMult \u03c1 : \u211d) := by",
" rw [show ((zeroWindowWide_finite a).toFinset.card : \u211d) ="
]
}
],
"userModified": false,
"replaceAll": false
}
raw content_json (database row)
[{"type":"thinking","thinking":"`HasDerivAt.const_cpow (hf : HasDerivAt f f' x) (h0 : c ≠ 0 ∨ f x ≠ 0) : HasDerivAt (fun x => c ^ f x) (c ^ f x * Complex.log c * f') x` ✓ — side condition: c ≠ 0 ∨ f x ≠ 0. For c = (x:ℂ) (x > 1): c ≠ 0 ✓ left.\n\nNow write §3. The structure (cloned from Zeta23 with my modifications):\n\n```lean\n/-! ## 3. Analyticity of the B̃₂ parameter integral -/\n\n/-- The B̃₂ parameter integral is differentiable on re s > −1, with the\nlog-weighted derivative. (Clone of Zeta23's `hasDerivAt_Zeta0Integral`\nwith one more power of decay, D-067 §2.) -/\ntheorem hasDerivAt_b2Integral {s : ℂ} (hs : -1 < s.re) :\n HasDerivAt (fun z : ℂ => ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-z - 2))\n (∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * ((x : ℂ) ^ (-s - 2) * (-Real.log x))) s := by\n set f : ℝ → ℂ := fun x ↦ (b2Fun x : ℂ)\n set F : ℂ → ℝ → ℂ := fun z x ↦ (x : ℂ) ^ (-z - 2) * f x\n set F' : ℂ → ℝ → ℂ := fun z x ↦ (x : ℂ) ^ (-z - 2) * (-Real.log x) * f x\n set ε := (s.re + 1) / 2\n have ε_pos : 0 < ε := by linarith\n set bound : ℝ → ℝ := fun x ↦ |x ^ (-(s.re + 3) / 2)| * |Real.log x|\n let μ : Measure ℝ := volume.restrict (Set.Ioi (1:ℝ))\n have hF_meas : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) μ := by\n have hU : {z : ℂ | -1 < z.re} ∈ 𝓝 s := by\n rw [mem_nhds_iff]\n exact ⟨{z | -1 < z.re}, fun _ a ↦ a, isOpen_lt continuous_const Complex.continuous_re, hs⟩\n filter_upwards [hU] with z hz\n have h := (integrableOn_b2_cpow hz).aestronglyMeasurable\n -- F z x = x^(−z−2) * f x vs their form: f x * x^(−z−2): comm\n exact h.congr (Filter.Eventually.of_forall fun x => by\n simp only [F, f]\n ring)\n have hF_int : Integrable (F s) μ := by\n apply Integrable.congr ((integrableOn_b2_cpow hs) : Integrable _ μ) -- IntegrableOn = Integrable on restrict — defeq\n filter_upwards with x\n simp only [F, f]\n ring\n have hF'_meas : AEStronglyMeasurable (F' s) μ := by\n have h := (integrableOn_b2_cpow_log hs).aestronglyMeasurable\n exact h.congr (Filter.Eventually.of_forall fun x => by\n simp only [F', f]\n ring)\n have h_bound : ∀ᵐ x ∂μ, ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x := by\n filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx\n have hx1 : (1:ℝ) < x := Set.mem_Ioi.mp hx\n intro z hz\n have hzre : (s.re - 1) / 2 < z.re := by\n rw [Metric.mem_ball, Complex.dist_eq] at hz\n have := abs_re_le_norm (z - s)\n have : |z.re - s.re| ≤ ‖z - s‖ := this\n have h2 : z.re - s.re > -ε := by linarith [abs_lt.mp (lt_of_le_of_lt this hz)] -- hmm\n ... \n```\nHmm let me be careful: z ∈ ball s ε ⟹ dist z s < ε ⟹ |z.re − s.re| ≤ ‖z − s‖ = dist < ε ⟹ z.re > s.re − ε = σ − (σ+1)/2 = (σ−1)/2 ✓. Then −z.re − 2 < −(σ−1)/2 − 2 = (−σ−3)/2 ✓. Then x^(−z.re−2) ≤ x^((−σ−3)/2) for x ≥ 1 (rpow monotone in exponent for x ≥ 1: `Real.rpow_le_rpow_of_exponent_le (hx : 1 ≤ x) (h : a ≤ b)`? — name: Real.rpow_le_rpow_of_exponent_le ✓ (from their proof)). With ≤ vs < : use .le.\nThen:\n‖F' z x‖ = ‖x^(−z−2)‖·‖−log x‖·‖f x‖ = x^(−z.re−2)·|log x|·|b2Fun x| ≤ x^((−σ−3)/2)·|log x|·(1/8) ≤ x^((−σ−3)/2)·|log x| = |x^((−σ−3)/2)|·|log x| = bound x ✓ (x^... ≥ 0).\n\nThe norm computation: ‖(x:ℂ)^(−z−2)‖ = x^(re(−z−2)) = x^(−z.re−2) (norm_cpow_eq_rpow_re_of_pos ✓ x > 1). ‖−Real.log x‖ as ℂ = |log x| ✓ (norm_neg + norm_real + norm_eq_abs). ‖f x‖ = |b2Fun x| ≤ 1/8 ✓.\n\n have bound_integrable : Integrable bound μ := by\n have h := integrable_log_over_pow (r := -(s.re + 1)/2) (by linarith) (N := 1) (by norm_num)\n rw [Nat.cast_one] at h\n -- their form: IntegrableOn (fun x => ‖x^(r−1)‖·‖log x‖) (Ioi 1): r−1 = (−σ−3)/2 ✓\n refine h.congr_fun ?_ measurableSet_Ioi -- hmm Integrable bound μ vs IntegrableOn — defeq\n intro x hx\n have hx1 : (1:ℝ) < x := Set.mem_Ioi.mp hx\n show ‖x ^ (-(s.re + 1)/2 - 1)‖ * ‖Real.log x‖ = |x ^ (-(s.re + 3)/2)| * |Real.log x|\n rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_nonneg (Real.rpow_nonneg (by linarith) _),\n Real.abs_rpow_of_nonneg (by linarith)] -- |x^...| = x^... ✓ both\n congr 2\n ring\n have h_diff : ∀ᵐ x ∂μ, ∀ z ∈ Metric.ball s ε, HasDerivAt (fun w ↦ F w x) (F' z x) z := by\n filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx\n have hx1 : (1:ℝ) < x := Set.mem_Ioi.mp hx\n intro z hz\n -- F w x = x^(−w−2)·f x: derivative = x^(−z−2)·log x·(−1)·f x — via const_cpow with f w = −w−2:\n have h1 : HasDerivAt (fun w : ℂ => (x : ℂ) ^ (-w - 2)) ((x : ℂ) ^ (-z - 2) * Complex.log x * (-1)) z := by\n have := HasDerivAt.const_cpow (c := (x : ℂ)) (f := fun w : ℂ => -w - 2) (f' := -1) (x := z)\n ?_ ?_\n · -- match derivative form: const_cpow gives c^(f z)·log c·f' = x^(−z−2)·log x·(−1) ✓\n convert this using 2 -- f z = −z−2 ✓ rfl; the log of ofReal: Complex.log ↑x = ↑(Real.log x) ✓ (Complex.ofReal_log (x ≥ 0))\n ...\n · left -- c ≠ 0: ↑x ≠ 0 (x > 1)\n exact_mod_cast ne_of_gt (lt_trans zero_lt_one hx1)...\n -- then times f x (const):\n have h2 := h1.mul_const (f x) -- HasDerivAt (fun w => x^(−w−2)·f x) (x^(−z−2)·log x·(−1)·f x)\n convert h2 using 1\n · ext w; simp only [F]; ring -- F w x = x^(−w−2)·f x ✓\n · simp only [F', f] -- F' z x = x^(−z−2)·(−log x)·f x vs x^(−z−2)·log x·(−1)·f x\n rw [Complex.ofReal_log (by linarith)] -- if needed\n ring\n -- the final assembly\n have key := (hasDerivAt_integral_of_dominated_loc_of_deriv_le (F := F) (F' := F') (x₀ := s)\n (s := Metric.ball s ε) (bound := bound) (μ := μ) (Metric.ball_mem_nhds s ε_pos)\n hF_meas hF_int hF'_meas h_bound bound_integrable h_diff).2\n -- key : HasDerivAt (fun z => ∫ x, F z x ∂μ) (∫ x, F' s x ∂μ) s; match forms:\n convert key using 1\n · ext z; simp only [F, f] -- ∫ x, x^(−z−2)·↑b2Fun x = ∫ x, ↑b2Fun x·x^(−z−2): integral_congr? ext on the function z ↦ ∫ — the integrals: ∫ ∂μ vs ∫ Ioi: ∫ x, F z x ∂μ = ∫ x in Ioi 1, ...: μ = volume.restrict (Ioi 1): `integral_restrict`? hmm — the ∫ a, F n a ∂μ with μ = restrict: `MeasureTheory.integral_restrict`? there's integral over restrict = set integral: `integral_restrict (hs : MeasurableSet s) : ∫ x, f x ∂(μ.restrict s) = ∫ x in s, f x ∂μ`? I believe ∫ over restrict is by def `∫ x in s, f x ∂μ = ∫ x, f x ∂(μ.restrict s)` — so convert: the goals match after rewriting set integral ↔ restrict integral (defeq? set integral is DEFINED as restrict integral ✓ rfl-level). And the integrand order: F z x = x^· * f vs goal's ↑b2Fun·x^·: ext z; apply integral_congr_ae; filter_upwards; ring.\n · simp only [F', f]; apply integral_congr_ae; filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx; ring — hmm my goal form: ↑b2Fun x * (↑x^(−s−2) * (−↑(Real.log x))) vs F' form ↑x^(−s−2) * (−↑log x) * ↑b2Fun x: ring ✓ but need the log-cast aligned: −Real.log x cast — both sides ↑(-Real.log x)?? the goal's written as (-Real.log x) inside ℂ mult — elaborates as ↑(−Real.log x)? or −↑(Real.log x)? Both defeq via push_cast; ring handles if atoms match... to be safe use `push_cast; ring`.\n```\n\nLet me check HasDerivAt.const_cpow's application shape: (hf : HasDerivAt f f' x) (h0 : c ≠ 0 ∨ f x ≠ 0) : HasDerivAt (fun x => c ^ f x) (c ^ f x * Complex.log c * f') x. So:\n```lean\n have h1 : HasDerivAt (fun w : ℂ => (x : ℂ) ^ (-w - 2))\n ((x : ℂ) ^ (-z - 2) * Complex.log (x : ℂ) * (-1)) z :=\n HasDerivAt.const_cpow (c := (x : ℂ)) (f := fun w : ℂ => -w - 2) (f' := -1) (x := z)\n ((hasDerivAt_id z).neg.sub_const 2) (Or.inl (by norm_cast; linarith))\n```\nHmm — (hasDerivAt_id z).neg : HasDerivAt (fun w => -w) (-1) z ✓; .sub_const 2: fun w => −w − 2, derivative −1 − 0 = −1 ✓ (maybe displays −1 directly; or needs sub_zero simp). And f z = −z−2 ✓ the c^(f z) = x^(−z−2) ✓. c ≠ 0: (x:ℂ) ≠ 0 from x > 1: `(by norm_cast; linarith)`? norm_cast: (↑x : ℂ) ≠ 0 ↔ x ≠ 0: `Complex.ofReal_ne_zero.mpr (by linarith)` ✓ cleaner.\n\nThen the derivative value: x^(−z−2)·log(↑x)·(−1) — Complex.log (↑x) = ↑(Real.log x) for x ≥ 0: `Complex.ofReal_log (hx : 0 ≤ x) : Complex.log ↑x = ↑(Real.log x)` ✓.\n\nThen h2 := h1.mul_const (f x): HasDerivAt.mul_const? `HasDerivAt.mul_const (h : HasDerivAt f f' x) (c) : HasDerivAt (fun x => f x * c) (f' * c)` ✓. Gives derivative (x^(−z−2)·↑log x·(−1))·f x — want F' z x = x^(−z−2)·(−↑log x)·f x: equal by ring ✓.\n\nThe HasDerivAt.const_cpow — wait — one nuance: `HasDerivAt.const_cpow (hf : HasDerivAt f f' x) (h0 : c ≠ 0 ∨ f x ≠ 0)` — h0 : c ≠ 0 ∨ f x ≠ 0 — I pass Or.inl (ofReal_ne_zero...) ✓ (f x ≠ 0 unnecessary).\n\nAlso `hasDerivAt_integral_of_dominated_loc_of_deriv_le` — check arg order: (hs : s ∈ 𝓝 x₀) (hF_meas) (hF_int) {F'} (hF'_meas) (h_bound) (bound_integrable) (h_diff) : Integrable (F' x₀) ∧ HasDerivAt (fun n ↦ ∫ a, F n a ∂μ) (∫ a, F' x₀ a ∂μ) x₀ — the μ and F are implicit/explicit? Variables from the section: F, μ probably explicit-ish. The Zeta23 usage passed (F := F) (F' := F') (x₀ := s) (s := ...) (bound := ...) (μ := μ) explicitly ✓ copy.\n\nAlright — write §3 now.","signature":""},{"type":"text","text":"Writing §3 — the parameter-integral derivative (cloning Zeta23's proof with the extra decay power)."},{"type":"tool_use","id":"Edit_260","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiRBound.lean","old_string":"end NguyenRH1\n\nend","new_string":"/-! ## 3. Analyticity of the B̃₂ parameter integral -/\n\n/-- The B̃₂ parameter integral is differentiable on re s > −1, with the\nlog-weighted derivative. (Clone of Zeta23's `hasDerivAt_Zeta0Integral`\nwith one more power of decay, per D-067 §2.) -/\ntheorem hasDerivAt_b2Integral {s : ℂ} (hs : -1 < s.re) :\n HasDerivAt (fun z : ℂ => ∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * (x : ℂ) ^ (-z - 2))\n (∫ x in Set.Ioi (1:ℝ), (b2Fun x : ℂ) * ((x : ℂ) ^ (-s - 2) * (-Real.log x))) s := by\n set f : ℝ → ℂ := fun x ↦ (b2Fun x : ℂ)\n set F : ℂ → ℝ → ℂ := fun z x ↦ (x : ℂ) ^ (-z - 2) * f x\n set F' : ℂ → ℝ → ℂ := fun z x ↦ (x : ℂ) ^ (-z - 2) * (-Real.log x) * f x\n set ε := (s.re + 1) / 2\n have ε_pos : 0 < ε := by linarith\n set bound : ℝ → ℝ := fun x ↦ |x ^ (-(s.re + 3) / 2)| * |Real.log x|\n let μ : Measure ℝ := volume.restrict (Set.Ioi (1:ℝ))\n have hF_meas : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) μ := by\n have hU : {z : ℂ | -1 < z.re} ∈ 𝓝 s := by\n rw [mem_nhds_iff]\n exact ⟨{z | -1 < z.re}, fun _ a ↦ a, isOpen_lt continuous_const Complex.continuous_re, hs⟩\n filter_upwards [hU] with z hz\n have h := (integrableOn_b2_cpow hz).aestronglyMeasurable\n exact h.congr (Filter.Eventually.of_forall fun x => by simp only [F, f]; ring)\n have hF_int : Integrable (F s) μ := by\n apply Integrable.congr (integrableOn_b2_cpow hs)\n filter_upwards with x\n simp only [F, f]\n ring\n have hF'_meas : AEStronglyMeasurable (F' s) μ := by\n have h := (integrableOn_b2_cpow_log hs).aestronglyMeasurable\n exact h.congr (Filter.Eventually.of_forall fun x => by simp only [F', f]; ring)\n have h_bound : ∀ᵐ x ∂μ, ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x := by\n filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx\n have hx1 : (1:ℝ) < x := Set.mem_Ioi.mp hx\n intro z hz\n have hzre : (s.re - 1) / 2 < z.re := by\n rw [Metric.mem_ball, Complex.dist_eq] at hz\n have h1 : |z.re - s.re| ≤ ‖z - s‖ := abs_re_le_norm (z - s)\n have h2 : z.re - s.re > -ε := by\n have h3 : |z.re - s.re| < ε := lt_of_le_of_lt h1 hz\n linarith [abs_lt.mp h3]\n linarith [h2]\n have hpow : ‖(x : ℂ) ^ (-z - 2)‖ ≤ x ^ (-(s.re + 3) / 2) := by\n rw [norm_cpow_eq_rpow_re_of_pos (by linarith)]\n have h3 : (-z - 2).re = -z.re - 2 := by simp\n rw [h3]\n apply Real.rpow_le_rpow_of_exponent_le (by linarith)\n linarith [hzre]\n calc ‖F' z x‖ = ‖(x : ℂ) ^ (-z - 2)‖ * |Real.log x| * |b2Fun x| := by\n simp only [F', f, norm_mul, norm_neg, Complex.norm_real, Real.norm_eq_abs]\n ring\n _ ≤ x ^ (-(s.re + 3) / 2) * |Real.log x| * (1 / 8) := by\n apply mul_le_mul_of_nonneg_right _ (by norm_num)\n apply mul_le_mul_of_nonneg_right hpow (abs_nonneg _)\n _ ≤ x ^ (-(s.re + 3) / 2) * |Real.log x| * 1 := by\n apply mul_le_mul_of_nonneg_left _ (by positivity)\n exact (abs_b2Fun_le x).trans (by norm_num)\n _ = bound x := by\n simp only [bound]\n rw [Real.abs_rpow_of_nonneg (by linarith)]\n ring\n have bound_integrable : Integrable bound μ := by\n have h := integrable_log_over_pow (r := -(s.re + 1) / 2) (by linarith) (N := 1) (by norm_num)\n rw [Nat.cast_one] at h\n refine h.congr_fun ?_ measurableSet_Ioi\n intro x hx\n have hx1 : (1:ℝ) < x := Set.mem_Ioi.mp hx\n show ‖x ^ (-(s.re + 1) / 2 - 1)‖ * ‖Real.log x‖ = |x ^ (-(s.re + 3) / 2)| * |Real.log x|\n rw [Real.norm_eq_abs, Real.norm_eq_abs, Real.abs_rpow_of_nonneg (by linarith),\n Real.abs_rpow_of_nonneg (by linarith)]\n congr 2\n ring\n have h_diff : ∀ᵐ x ∂μ, ∀ z ∈ Metric.ball s ε, HasDerivAt (fun w ↦ F w x) (F' z x) z := by\n filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx\n have hx1 : (1:ℝ) < x := Set.mem_Ioi.mp hx\n intro z hz\n have h1 : HasDerivAt (fun w : ℂ => (x : ℂ) ^ (-w - 2))\n ((x : ℂ) ^ (-z - 2) * Complex.log (x : ℂ) * (-1)) z :=\n HasDerivAt.const_cpow (c := (x : ℂ)) (f := fun w : ℂ => -w - 2) (f' := -1) (x := z)\n ((hasDerivAt_id z).neg.sub_const 2)\n (Or.inl (Complex.ofReal_ne_zero.mpr (by linarith)))\n have h2 := h1.mul_const (f x)\n convert h2 using 1\n · ext w\n simp only [F]\n ring\n · simp only [F', f]\n rw [Complex.ofReal_log (by linarith : (0:ℝ) ≤ x)]\n push_cast\n ring\n have key := (hasDerivAt_integral_of_dominated_loc_of_deriv_le (F := F) (F' := F') (x₀ := s)\n (s := Metric.ball s ε) (bound := bound) (μ := μ) (Metric.ball_mem_nhds s ε_pos)\n hF_meas hF_int hF'_meas h_bound bound_integrable h_diff).2\n convert key using 1\n · ext z\n apply integral_congr_ae\n filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx\n simp only [F, f]\n ring\n · apply integral_congr_ae\n filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with x hx\n simp only [F', f]\n push_cast\n ring\n\nend NguyenRH1\n\nend"},"extra_content":null}]