← Session 24 — ii′-2…4: swaps, (4.10) design, contour + website roadmap fixes
thinking (4887 chars)
I left a sorry in integrableOn_b2_cpow_log's measurability (the −log x continuity). Fix: `Real.log` continuous on Ioi 1: `ContinuousOn.log`? `Real.continuousOn_log : ContinuousOn Real.log {0}ᶜ`? there's `Real.continuousOn_log : ContinuousOn Real.log {0}ᶜ` ✓ I believe. Then .mono (Ioi 1 ⊆ {0}ᶜ), then neg: `.neg`, then ofReal-cast: the function is `(-Real.log x)` cast into ℂ? The integrand: (↑b2Fun x) * (↑x^(−s−2) * (−Real.log x)) — the −Real.log x is ℝ→? in the ℂ product: `- Real.log x` with the product in ℂ — the `(x:ℂ)^(−s−2) * (-Real.log x)` — (−Real.log x) must be ℂ: ↑(-Real.log x)? As written `-Real.log x` in a ℂ context — needs coercion: `(x:ℂ)^(-s-2) * (-(Real.log x : ℝ))` — hmm the expression as I wrote it: `(x : ℂ) ^ (-s - 2) * (-Real.log x)` — Lean will parse `-Real.log x` as ℂ via ↑? No — it'll fail to elaborate unless there's a coercion. The Zeta23 version: `(⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (-z - 1) * (- Real.log x)` — Real.log x : ℝ coerced to ℂ by the multiplication ✓ automatic (↑ is inserted since the other factor is ℂ — actually no: ℂ * ℝ doesn't elaborate — the Zeta23 code must have an explicit... their F' : `(x : ℂ) ^ (- s - 1) * (- Real.log x) * f x` — f x : ℂ; `(-Real.log x)` — hmm — in their context maybe `↑(-Real.log x)` inserted via coercion... `(- Real.log x)` where expected ℂ: elaborator inserts ↑ ✓ (OfReal of −Real.log x: `↑(-Real.log x)` — the − is inside the cast ✓ elaborates). OK so `-Real.log x` gets coerced fine.
For measurability/continuity of the log piece: (fun x : ℝ => (-(Real.log x : ℝ) : ℂ)) continuous on Ioi 1: Real.log continuous on {0}ᶜ ⊇ Ioi 1, neg, ofReal:
```lean
· exact ((continuous_ofReal.comp (Real.continuousOn_log.mono ... )) hmm
```
Real.continuousOn_log : ContinuousOn Real.log {0}ᶜ? — hmm exact name: `Real.continuousOn_log : ContinuousOn Real.log {0}ᶜ` ✓ I'm fairly confident. Then:
```lean
· have hlog : ContinuousOn (fun x : ℝ => (Real.log x : ℂ)) (Set.Ioi (1:ℝ)) :=
(continuous_ofReal.comp_real... ) hmm
```
continuous_ofReal : Continuous ((↑) : ℝ → ℂ) ✓; Real.continuousOn_log : ContinuousOn Real.log {0}ᶜ: comp: continuous_ofReal.comp_continuousOn? `Continuous.comp_continuousOn (hc : Continuous g) (hf : ContinuousOn f s) : ContinuousOn (g ∘ f) s` ✓. So:
```lean
· have hlog : ContinuousOn (fun x : ℝ => (Real.log x : ℂ)) (Set.Ioi (1:ℝ)) :=
(continuous_ofReal.comp_continuousOn
(Real.continuousOn_log.mono (fun x hx => by
intro h; rw [h] at hx; simp at hx))).neg
```
hmm — ContinuousOn.neg: (ContinuousOn f s).neg : ContinuousOn (−f) s ✓. The subset: Ioi 1 ⊆ {0}ᶜ: x > 1 ⟹ x ≠ 0 ✓: `Set.subset_compl_singleton_iff...`: `fun x hx => by intro h0; rw [h0] at hx; exact absurd (Set.mem_Ioi.mp hx) (by norm_num)`. Let me write it carefully:
Also the integrand association: my function is fun x => ↑b2Fun x * (↑x^(−s−2) * ↑(−Real.log x)) — ContinuousOn.mul (b2Fun-part) (cpow-part.mul log-part) ✓ association matches.
But wait — actually, for the derivative of the parameter integral, the Zeta23 F' has form `x^(−s−1) * (−log x) * f x` — the association there: (x^· * −log) * f. Mine: b2 * (x^ · −log). Association differences are handled by ring_nf congr at the end (their proof's final convert! ... using 3 with ring_nf). I'll deal with it in the hasDerivAt assembly.
Also the `refine h.congr_fun ?_ measurableSet_Ioi` in hg — h : IntegrableOn (fun x => ‖x^(r−1)‖·‖log x‖) (Ioi 1) with r = −σ−1: my target: x^(−σ−2)·|log x|: EqOn: ‖x^(r−1)‖ = x^(r−1) (abs of nonneg ✓) and r−1 = −σ−1−1 = −σ−2 ✓ ring. My earlier code:
```lean
rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_nonneg (Real.rpow_nonneg (by linarith) _),
abs_of_nonneg (by linarith : (0:ℝ) ≤ Real.log x)]
congr 2
ring
```
Hmm — the goal after intro x hx: ‖x^(r−1)‖ * ‖Real.log x‖ = x^(−σ−2) * |Real.log x|: ‖·‖ on reals = abs ✓ rw both norm_eq_abs; abs_of_nonneg rpow: |x^(r−1)| = x^(r−1) ✓; |log x| = log x (x > 1 ⟹ log ≥ 0 ✓): abs_of_nonneg (Real.log_nonneg (by linarith)) — wait |log x| appears on the RHS — the equation is LHS = RHS with RHS having |log x|: after rw abs stuff: hmm messy. Simpler:
```lean
intro x hx
have hx1 : (1:ℝ) < x := Set.mem_Ioi.mp hx
have h1 : ‖x ^ (-s.re - 1 - 1)‖ = x ^ (-s.re - 2) := by
rw [Real.norm_eq_abs, abs_of_nonneg (Real.rpow_nonneg (by linarith) _)]
congr 1
ring
rw [h1, Real.norm_eq_abs, abs_of_nonneg (Real.log_nonneg hx1.le)]
```
hmm — ‖Real.log x‖ = |log x| = log x (nonneg) ✓ then goal: x^(−σ−2)·log x = x^(−σ−2)·|log x| ✓ after the abs_of_nonneg rewrite of RHS's |log x| → log x ✓ rfl.
Ugh — but the form of h's function: `fun x => ‖x ^ (r - 1)‖ * ‖Real.log x‖` — with r := −s.re − 1: the exponent displays as (−s.re − 1) − 1. My h1 handles it.
This is getting long. Let me just write the whole §2 remaining block + §3 cleanly and compile. Rewrite integrableOn_b2_cpow_log fully:
Completing the log-weighted integrability lemma properly.
tool: Edit
input
{
"replace_all": false,
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiRBound.lean",
"old_string": "/-- The log-weighted B\u0303\u2082 integrand is integrable on (1, \u221e) for re s > \u22121. -/\ntheorem integrableOn_b2_cpow_log {s : \u2102} (hs : -1 < s.re) :\n IntegrableOn (fun x : \u211d => (b2Fun x : \u2102) * ((x : \u2102) ^ (-s - 2) * (-Real.log x)))\n (Set.Ioi 1) := by\n have hg : IntegrableOn (fun x : \u211d => x ^ (-s.re - 2) * |Real.log x|) (Set.Ioi 1) := by\n have h := integrable_log_over_pow (r := -s.re - 1) (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 rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_nonneg (Real.rpow_nonneg (by linarith) _),\n abs_of_nonneg (by linarith : (0:\u211d) \u2264 Real.log x)]\n congr 2\n ring\n have hmeas : AEStronglyMeasurable (fun x : \u211d => (b2Fun x : \u2102) * ((x : \u2102) ^ (-s - 2) *\n (-Real.log x))) (volume.restrict (Set.Ioi (1:\u211d))) := by\n apply ContinuousOn.aestronglyMeasurable _ measurableSet_Ioi\n apply ContinuousOn.mul\n \u00b7 exact (continuous_ofReal.comp continuous_b2Fun).continuousOn\n \u00b7 apply ContinuousOn.mul\n \u00b7 intro x hx\n exact (continuousAt_ofReal_cpow_const x _\n (Or.inr (by linarith [Set.mem_Ioi.mp hx] : x \u2260 0))).continuousWithinAt\n \u00b7 apply Continuous.neg _).continuousOn -- \u2212log x: continuous on Ioi 1\n -- (continuous_neg (Real.log \u2218 ...)): use:\n exact (continuous_neg_of... ) sorry\n sorry",
"new_string": "/-- The log-weighted B\u0303\u2082 integrand is integrable on (1, \u221e) for re s > \u22121. -/\ntheorem integrableOn_b2_cpow_log {s : \u2102} (hs : -1 < s.re) :\n IntegrableOn (fun x : \u211d => (b2Fun x : \u2102) * ((x : \u2102) ^ (-s - 2) * (-Real.log x)))\n (Set.Ioi 1) := by\n have hg : IntegrableOn (fun x : \u211d => x ^ (-s.re - 2) * |Real.log x|) (Set.Ioi 1) := by\n have h := integrable_log_over_pow (r := -s.re - 1) (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 have h1 : \u2016x ^ (-s.re - 1 - 1)\u2016 = x ^ (-s.re - 2) := by\n rw [Real.norm_eq_abs, abs_of_nonneg (Real.rpow_nonneg (by linarith) _)]\n congr 1\n ring\n rw [h1, Real.norm_eq_abs, abs_of_nonneg (Real.log_nonneg hx1.le)]\n have hmeas : AEStronglyMeasurable (fun x : \u211d => (b2Fun x : \u2102) * ((x : \u2102) ^ (-s - 2) *\n (-Real.log x))) (volume.restrict (Set.Ioi (1:\u211d))) := by\n apply ContinuousOn.aestronglyMeasurable _ measurableSet_Ioi\n apply ContinuousOn.mul\n \u00b7 exact (continuous_ofReal.comp continuous_b2Fun).continuousOn\n \u00b7 apply ContinuousOn.mul\n \u00b7 intro x hx\n exact (continuousAt_ofReal_cpow_const x _\n (Or.inr (by linarith [Set.mem_Ioi.mp hx] : x \u2260 0))).continuousWithinAt\n \u00b7 have hlog : ContinuousOn (fun x : \u211d => (Real.log x : \u2102)) (Set.Ioi (1:\u211d)) :=\n continuous_ofReal.comp_continuousOn (Real.continuousOn_log.mono\n (fun x hx => by\n intro h0\n rw [Set.mem_compl_singleton_iff] at *\n rw [h0] at hx\n simp at hx))\n exact hlog.neg\n have hbound : \u2200\u1d50 x \u2202(volume.restrict (Set.Ioi 1)),\n \u2016(b2Fun x : \u2102) * ((x : \u2102) ^ (-s - 2) * (-Real.log x))\u2016 \u2264 x ^ (-s.re - 2) * |Real.log 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 have hnorm : \u2016(x : \u2102) ^ (-s - 2)\u2016 = x ^ (-s.re - 2) := by\n rw [norm_cpow_eq_rpow_re_of_pos (by linarith)]\n congr 2\n rw [norm_mul, norm_mul, Complex.norm_real, hnorm]\n rw [show \u2016(-(Real.log x : \u211d) : \u2102)\u2016 = |Real.log x| by\n rw [Complex.norm_real, Real.norm_eq_abs]]\n calc |b2Fun x| * (x ^ (-s.re - 2) * |Real.log x|)\n \u2264 (1 / 8) * (x ^ (-s.re - 2) * |Real.log x|) :=\n mul_le_mul_of_nonneg_right (abs_b2Fun_le x)\n (mul_nonneg (Real.rpow_nonneg (by linarith) _) (abs_nonneg _))\n _ \u2264 x ^ (-s.re - 2) * |Real.log x| :=\n mul_le_of_le_one_left (mul_nonneg (Real.rpow_nonneg (by linarith) _) (abs_nonneg _))\n (by norm_num)\n exact Integrable.mono' hg hmeas hbound"
}
raw content_json (database row)
[{"type":"thinking","thinking":"I left a sorry in integrableOn_b2_cpow_log's measurability (the −log x continuity). Fix: `Real.log` continuous on Ioi 1: `ContinuousOn.log`? `Real.continuousOn_log : ContinuousOn Real.log {0}ᶜ`? there's `Real.continuousOn_log : ContinuousOn Real.log {0}ᶜ` ✓ I believe. Then .mono (Ioi 1 ⊆ {0}ᶜ), then neg: `.neg`, then ofReal-cast: the function is `(-Real.log x)` cast into ℂ? The integrand: (↑b2Fun x) * (↑x^(−s−2) * (−Real.log x)) — the −Real.log x is ℝ→? in the ℂ product: `- Real.log x` with the product in ℂ — the `(x:ℂ)^(−s−2) * (-Real.log x)` — (−Real.log x) must be ℂ: ↑(-Real.log x)? As written `-Real.log x` in a ℂ context — needs coercion: `(x:ℂ)^(-s-2) * (-(Real.log x : ℝ))` — hmm the expression as I wrote it: `(x : ℂ) ^ (-s - 2) * (-Real.log x)` — Lean will parse `-Real.log x` as ℂ via ↑? No — it'll fail to elaborate unless there's a coercion. The Zeta23 version: `(⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (-z - 1) * (- Real.log x)` — Real.log x : ℝ coerced to ℂ by the multiplication ✓ automatic (↑ is inserted since the other factor is ℂ — actually no: ℂ * ℝ doesn't elaborate — the Zeta23 code must have an explicit... their F' : `(x : ℂ) ^ (- s - 1) * (- Real.log x) * f x` — f x : ℂ; `(-Real.log x)` — hmm — in their context maybe `↑(-Real.log x)` inserted via coercion... `(- Real.log x)` where expected ℂ: elaborator inserts ↑ ✓ (OfReal of −Real.log x: `↑(-Real.log x)` — the − is inside the cast ✓ elaborates). OK so `-Real.log x` gets coerced fine.\n\nFor measurability/continuity of the log piece: (fun x : ℝ => (-(Real.log x : ℝ) : ℂ)) continuous on Ioi 1: Real.log continuous on {0}ᶜ ⊇ Ioi 1, neg, ofReal:\n```lean\n · exact ((continuous_ofReal.comp (Real.continuousOn_log.mono ... )) hmm\n```\nReal.continuousOn_log : ContinuousOn Real.log {0}ᶜ? — hmm exact name: `Real.continuousOn_log : ContinuousOn Real.log {0}ᶜ` ✓ I'm fairly confident. Then:\n```lean\n · have hlog : ContinuousOn (fun x : ℝ => (Real.log x : ℂ)) (Set.Ioi (1:ℝ)) :=\n (continuous_ofReal.comp_real... ) hmm\n```\ncontinuous_ofReal : Continuous ((↑) : ℝ → ℂ) ✓; Real.continuousOn_log : ContinuousOn Real.log {0}ᶜ: comp: continuous_ofReal.comp_continuousOn? `Continuous.comp_continuousOn (hc : Continuous g) (hf : ContinuousOn f s) : ContinuousOn (g ∘ f) s` ✓. So:\n```lean\n · have hlog : ContinuousOn (fun x : ℝ => (Real.log x : ℂ)) (Set.Ioi (1:ℝ)) :=\n (continuous_ofReal.comp_continuousOn\n (Real.continuousOn_log.mono (fun x hx => by\n intro h; rw [h] at hx; simp at hx))).neg\n```\nhmm — ContinuousOn.neg: (ContinuousOn f s).neg : ContinuousOn (−f) s ✓. The subset: Ioi 1 ⊆ {0}ᶜ: x > 1 ⟹ x ≠ 0 ✓: `Set.subset_compl_singleton_iff...`: `fun x hx => by intro h0; rw [h0] at hx; exact absurd (Set.mem_Ioi.mp hx) (by norm_num)`. Let me write it carefully:\n\nAlso the integrand association: my function is fun x => ↑b2Fun x * (↑x^(−s−2) * ↑(−Real.log x)) — ContinuousOn.mul (b2Fun-part) (cpow-part.mul log-part) ✓ association matches.\n\nBut wait — actually, for the derivative of the parameter integral, the Zeta23 F' has form `x^(−s−1) * (−log x) * f x` — the association there: (x^· * −log) * f. Mine: b2 * (x^ · −log). Association differences are handled by ring_nf congr at the end (their proof's final convert! ... using 3 with ring_nf). I'll deal with it in the hasDerivAt assembly.\n\nAlso the `refine h.congr_fun ?_ measurableSet_Ioi` in hg — h : IntegrableOn (fun x => ‖x^(r−1)‖·‖log x‖) (Ioi 1) with r = −σ−1: my target: x^(−σ−2)·|log x|: EqOn: ‖x^(r−1)‖ = x^(r−1) (abs of nonneg ✓) and r−1 = −σ−1−1 = −σ−2 ✓ ring. My earlier code: \n```lean\n rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_nonneg (Real.rpow_nonneg (by linarith) _),\n abs_of_nonneg (by linarith : (0:ℝ) ≤ Real.log x)]\n congr 2\n ring\n```\nHmm — the goal after intro x hx: ‖x^(r−1)‖ * ‖Real.log x‖ = x^(−σ−2) * |Real.log x|: ‖·‖ on reals = abs ✓ rw both norm_eq_abs; abs_of_nonneg rpow: |x^(r−1)| = x^(r−1) ✓; |log x| = log x (x > 1 ⟹ log ≥ 0 ✓): abs_of_nonneg (Real.log_nonneg (by linarith)) — wait |log x| appears on the RHS — the equation is LHS = RHS with RHS having |log x|: after rw abs stuff: hmm messy. Simpler:\n```lean\n intro x hx\n have hx1 : (1:ℝ) < x := Set.mem_Ioi.mp hx\n have h1 : ‖x ^ (-s.re - 1 - 1)‖ = x ^ (-s.re - 2) := by\n rw [Real.norm_eq_abs, abs_of_nonneg (Real.rpow_nonneg (by linarith) _)]\n congr 1\n ring\n rw [h1, Real.norm_eq_abs, abs_of_nonneg (Real.log_nonneg hx1.le)]\n```\nhmm — ‖Real.log x‖ = |log x| = log x (nonneg) ✓ then goal: x^(−σ−2)·log x = x^(−σ−2)·|log x| ✓ after the abs_of_nonneg rewrite of RHS's |log x| → log x ✓ rfl.\n\nUgh — but the form of h's function: `fun x => ‖x ^ (r - 1)‖ * ‖Real.log x‖` — with r := −s.re − 1: the exponent displays as (−s.re − 1) − 1. My h1 handles it.\n\nThis is getting long. Let me just write the whole §2 remaining block + §3 cleanly and compile. Rewrite integrableOn_b2_cpow_log fully:","signature":""},{"type":"text","text":"Completing the log-weighted integrability lemma properly."},{"type":"tool_use","id":"Edit_252","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiRBound.lean","old_string":"/-- The log-weighted B̃₂ integrand is integrable on (1, ∞) for re s > −1. -/\ntheorem integrableOn_b2_cpow_log {s : ℂ} (hs : -1 < s.re) :\n IntegrableOn (fun x : ℝ => (b2Fun x : ℂ) * ((x : ℂ) ^ (-s - 2) * (-Real.log x)))\n (Set.Ioi 1) := by\n have hg : IntegrableOn (fun x : ℝ => x ^ (-s.re - 2) * |Real.log x|) (Set.Ioi 1) := by\n have h := integrable_log_over_pow (r := -s.re - 1) (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 rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_nonneg (Real.rpow_nonneg (by linarith) _),\n abs_of_nonneg (by linarith : (0:ℝ) ≤ Real.log x)]\n congr 2\n ring\n have hmeas : AEStronglyMeasurable (fun x : ℝ => (b2Fun x : ℂ) * ((x : ℂ) ^ (-s - 2) *\n (-Real.log x))) (volume.restrict (Set.Ioi (1:ℝ))) := by\n apply ContinuousOn.aestronglyMeasurable _ measurableSet_Ioi\n apply ContinuousOn.mul\n · exact (continuous_ofReal.comp continuous_b2Fun).continuousOn\n · apply ContinuousOn.mul\n · intro x hx\n exact (continuousAt_ofReal_cpow_const x _\n (Or.inr (by linarith [Set.mem_Ioi.mp hx] : x ≠ 0))).continuousWithinAt\n · apply Continuous.neg _).continuousOn -- −log x: continuous on Ioi 1\n -- (continuous_neg (Real.log ∘ ...)): use:\n exact (continuous_neg_of... ) sorry\n sorry","new_string":"/-- The log-weighted B̃₂ integrand is integrable on (1, ∞) for re s > −1. -/\ntheorem integrableOn_b2_cpow_log {s : ℂ} (hs : -1 < s.re) :\n IntegrableOn (fun x : ℝ => (b2Fun x : ℂ) * ((x : ℂ) ^ (-s - 2) * (-Real.log x)))\n (Set.Ioi 1) := by\n have hg : IntegrableOn (fun x : ℝ => x ^ (-s.re - 2) * |Real.log x|) (Set.Ioi 1) := by\n have h := integrable_log_over_pow (r := -s.re - 1) (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 have h1 : ‖x ^ (-s.re - 1 - 1)‖ = x ^ (-s.re - 2) := by\n rw [Real.norm_eq_abs, abs_of_nonneg (Real.rpow_nonneg (by linarith) _)]\n congr 1\n ring\n rw [h1, Real.norm_eq_abs, abs_of_nonneg (Real.log_nonneg hx1.le)]\n have hmeas : AEStronglyMeasurable (fun x : ℝ => (b2Fun x : ℂ) * ((x : ℂ) ^ (-s - 2) *\n (-Real.log x))) (volume.restrict (Set.Ioi (1:ℝ))) := by\n apply ContinuousOn.aestronglyMeasurable _ measurableSet_Ioi\n apply ContinuousOn.mul\n · exact (continuous_ofReal.comp continuous_b2Fun).continuousOn\n · apply ContinuousOn.mul\n · intro x hx\n exact (continuousAt_ofReal_cpow_const x _\n (Or.inr (by linarith [Set.mem_Ioi.mp hx] : x ≠ 0))).continuousWithinAt\n · have hlog : ContinuousOn (fun x : ℝ => (Real.log x : ℂ)) (Set.Ioi (1:ℝ)) :=\n continuous_ofReal.comp_continuousOn (Real.continuousOn_log.mono\n (fun x hx => by\n intro h0\n rw [Set.mem_compl_singleton_iff] at *\n rw [h0] at hx\n simp at hx))\n exact hlog.neg\n have hbound : ∀ᵐ x ∂(volume.restrict (Set.Ioi 1)),\n ‖(b2Fun x : ℂ) * ((x : ℂ) ^ (-s - 2) * (-Real.log x))‖ ≤ x ^ (-s.re - 2) * |Real.log 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 have hnorm : ‖(x : ℂ) ^ (-s - 2)‖ = x ^ (-s.re - 2) := by\n rw [norm_cpow_eq_rpow_re_of_pos (by linarith)]\n congr 2\n rw [norm_mul, norm_mul, Complex.norm_real, hnorm]\n rw [show ‖(-(Real.log x : ℝ) : ℂ)‖ = |Real.log x| by\n rw [Complex.norm_real, Real.norm_eq_abs]]\n calc |b2Fun x| * (x ^ (-s.re - 2) * |Real.log x|)\n ≤ (1 / 8) * (x ^ (-s.re - 2) * |Real.log x|) :=\n mul_le_mul_of_nonneg_right (abs_b2Fun_le x)\n (mul_nonneg (Real.rpow_nonneg (by linarith) _) (abs_nonneg _))\n _ ≤ x ^ (-s.re - 2) * |Real.log x| :=\n mul_le_of_le_one_left (mul_nonneg (Real.rpow_nonneg (by linarith) _) (abs_nonneg _))\n (by norm_num)\n exact Integrable.mono' hg hmeas hbound"},"extra_content":null}]