← Session 31 — ii′-5f: tight R-bound 10.5/48 (piece 3 + pinch)
thinking (20543 chars)
Section 11a compiles clean. Now §11b: the LA bricks (left-tail, j ≥ 14, weight 1/(j+10)²). This includes the harder antiderivative for log x/(x+10)² and the antitone proof. Let me write it.
Plan recap:
- antitoneOn_one_div_add_sq (direct).
- hasDerivAt_neg_inv_add (F = −(x+10)⁻¹) + integrableOn_one_div_add_sq + integral = 1/23 + LA₀.
- antitoneOn_log_div_add_sq (calculus: deriv = ((x+10)/x − 2 log x)/(x+10)³ ≤ 0).
- The antiderivative F = −log x/(x+10) + (1/10)·log(x/(x+10)) with HasDerivAt = log x/(x+10)², Tendsto → 0; integrableOn_log_div_add_sq; integral = log 13/23 + log(23/13)/10; LA₁ ≤ 0.1687.
- LA₂ ≤ 0.0621 (pointwise trick).
For antitoneOn_log_div_add_sq — use antitoneOn_of_deriv_nonpos (convex_Ici 13) with continuity/differentiability/deriv-nonpos (the antitoneOn_log_div_sq pattern from this file, which used interior_Ici). The deriv computation:
deriv (fun y => log y/(y+10)²) x = ((x+10)/x − 2·log x)/(x+10)³.
Build the HasDerivAt:
h1 : HasDerivAt (fun y => (y+10)^2) (2*(x+10)) x:
((hasDerivAt_id' x).const_add 10) then .pow? HasDerivAt.pow? For h : HasDerivAt f f' x: h.pow 2? There is `HasDerivAt.pow (hf : HasDerivAt f f' x) : HasDerivAt (fun x => (f x)^n) (n * (f x)^(n-1) * f')`? hmm — earlier I used hasDerivAt_pow 2 (x+10) .comp: ((hasDerivAt_pow 2 (x+10)).comp x h1): derivative (2·(x+10)^1)·1 — normalize: 2(x+10).
h2 : HasDerivAt (fun y => Real.log y / (y+10)^2) (((1/x)·(x+10)^2 − log x·(2(x+10)))/((x+10)^2)^2) x := (Real.hasDerivAt_log hx0).div h1 (x+10)² ≠ 0.
Then deriv f x = that raw value via h2.deriv; normalize: ((1/x)(x+10)² − 2(x+10) log x)/(x+10)⁴ = ((x+10)/x − 2 log x)/(x+10)³: field_simp.
Then show ≤ 0: (x+10)/x − 2 log x ≤ 0: (x+10)/x = 1+10/x ≤ 1+10/13 = 23/13; 2 log x ≥ 2·1 = 2 ≥ 23/13 ✓ (log x ≥ 1 for x ≥ 13 ≥ e).
Let me write the deriv ≤ 0 part concretely:
```
lemma antitoneOn_log_div_add_sq :
AntitoneOn (fun x : ℝ => Real.log x / (x + 10) ^ 2) (Set.Ici (13 : ℝ)) := by
apply antitoneOn_of_deriv_nonpos (convex_Ici 13)
· intro x hx
have hx0 : x ≠ 0 := by have h := (Set.mem_Ici.mp hx); linarith
have hx10 : (x + 10) ^ 2 ≠ 0 := by
have h := (Set.mem_Ici.mp hx)
positivity
exact ((Real.differentiableAt_log hx0).div
(differentiableAt_const_add.pow 2) hx10).continuousAt.continuousWithinAt
· intro x hx
have hx0 : x ≠ 0 := by
have h : (13 : ℝ) < x := Set.mem_Ioi.mp (by rwa [interior_Ici] at hx)
linarith
have hx10 : (x + 10) ^ 2 ≠ 0 := by
have h : (13 : ℝ) < x := Set.mem_Ioi.mp (by rwa [interior_Ici] at hx)
positivity
exact ((Real.differentiableAt_log hx0).div
(differentiableAt_const_add.pow 2) hx10).differentiableWithinAt
· intro x hx
have hx13 : (13 : ℝ) < x := Set.mem_Ioi.mp (by rwa [interior_Ici] at hx)
have hx0 : x ≠ 0 := by linarith
have hx10 : (x + 10) ≠ 0 := by linarith
have hderiv : deriv (fun y => Real.log y / (y + 10) ^ 2) x
= ((x + 10) / x - 2 * Real.log x) / (x + 10) ^ 3 := by
have h1 : HasDerivAt (fun y : ℝ => (y + 10) ^ 2) (2 * (x + 10)) x := by
have h := (hasDerivAt_pow 2 (x + 10)).comp x ((hasDerivAt_id' x).const_add 10)
rw [show ((2 : ℕ) : ℝ) * (x + 10) ^ (2 - 1) * 1 = 2 * (x + 10) from by
rw [show (2 : ℕ) - 1 = 1 from rfl, pow_one]
push_cast
ring] at h
exact h
have h2 := (Real.hasDerivAt_log hx0).div h1 (by positivity : (x + 10) ^ 2 ≠ 0)
rw [h2.deriv]
field_simp [hx0, hx10]
ring
rw [hderiv]
have hlog1 : (1 : ℝ) ≤ Real.log x := by
have h1 : Real.exp 1 ≤ 13 := Real.exp_one_lt_d9.le.trans (by norm_num)
have h2 : (1 : ℝ) ≤ Real.log 13 := by
rw [Real.le_log_iff_exp_le (by norm_num : (0 : ℝ) < 13)]
exact h1
exact h2.trans (Real.log_le_log (by positivity : (0 : ℝ) < 13) hx13.le)
have hbound : (x + 10) / x ≤ 2 := by
rw [div_le_iff₀ (by linarith : (0 : ℝ) < x)]
linarith
have h3 : (x + 10) / x - 2 * Real.log x ≤ 0 := by linarith [hlog1, hbound]
exact div_nonpos_of_nonpos_of_nonneg h3 (by positivity)
```
Hmm — `differentiableAt_const_add.pow 2`: is there `differentiableAt_const_add (c) : DifferentiableAt f (x+c)??` — banked from this file: `differentiableAt_pow takes ONE arg (the exponent)` — differentiableAt_pow 2 : DifferentiableAt (fun x => x^2)?? no — differentiableAt_pow (n) : DifferentiableAt 𝕜 (fun x => x^n) x? It was used as `(differentiableAt_pow 2)` in antitoneOn_log_div_sq: `((Real.differentiableAt_log hx0).div (differentiableAt_pow 2) (pow_ne_zero 2 hx0))` — differentiableAt_pow 2 : DifferentiableAt ℝ (fun x => x^2) x?? with x implicit. For (x+10)^2: need DifferentiableAt (fun y => (y+10)^2) x: (differentiableAt_id.add_const 10).pow 2? `DifferentiableAt.add_const : DifferentiableAt f x → DifferentiableAt (fun x => f x + c) x`? For (y+10): differentiableAt_id.add_const 10?? `DifferentiableAt.add_const (hf : DifferentiableAt 𝕜 f x) (c : 𝕜) : DifferentiableAt 𝕜 (fun x => f x + c) x` — but fun y => y+10 = (· + 10) = id + const: differentiableAt_id.add_const 10 ✓. Then .pow 2: `DifferentiableAt.pow (hf : DifferentiableAt 𝕜 f x) : DifferentiableAt 𝕜 (fun x => (f x)^n) x`?? hmm — maybe `DifferentiableAt.pow (hf) (n)`? or `differentiableAt_pow.comp`... Use: (differentiableAt_id.add_const 10).pow 2 — check name `DifferentiableAt.pow` exists (it does: DifferentiableAt.pow : DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 (fun x => f x ^ n) x? actually I think it's `DifferentiableAt.pow (hf : DifferentiableAt 𝕜 f x) (n : ℕ)`?). Risky. Alternative: continuity of log/(x+10)² via ContinuousAt directly: (Real.continuousAt_log hx0).div (continuousAt... ) — for the continuity clause use ContinuousAt: `ContinuousAt.div (Real.continuousAt_log hx0) ((continuousAt_id.add_const 10).pow 2) hx10` — ContinuousAt.pow : ContinuousAt f x → ContinuousAt (f^n) x ✓ exists? `ContinuousAt.pow (hf : ContinuousAt f x) (n : ℕ) : ContinuousAt (fun x => (f x)^n) x` ✓ I'm fairly confident. And differentiability for the interior clause: ((Real.differentiableAt_log hx0).div ((differentiableAt_id.add_const 10).pow 2) hx10).differentiableWithinAt — DifferentiableAt.pow — hmm. Alternative for differentiability: DifferentiableAt.div with g = (y+10)^2: DifferentiableAt (fun y => (y+10)^2) x: via (differentiableAt_id.add_const 10): DifferentiableAt (fun y => y+10) x ✓ then .pow 2 — `DifferentiableAt.pow : DifferentiableAt 𝕜 f x → (n : ℕ) → DifferentiableAt 𝕜 (fun x => f x ^ n) x`? Hmm — actually I recall `DifferentiableAt.pow (hf : DifferentiableAt 𝕜 f x) : DifferentiableAt 𝕜 (fun x ↦ f x ^ n) x` with n implicit — mirroring HasDerivAt.pow? In this file earlier: `(differentiableAt_pow 2)` used directly as DifferentiableAt (fun y => y^2) — so `differentiableAt_pow (n) : DifferentiableAt 𝕜 (fun x => x^n) x`?? — that's for the identity-power, not the composed. For the composed (y+10)^2: ((differentiableAt_pow 2).comp x (differentiableAt_id.add_const 10))? DifferentiableAt.comp? — hmm: `DifferentiableAt.comp (hf : DifferentiableAt 𝕜 f (g x)) (hg : DifferentiableAt 𝕜 g x) : DifferentiableAt 𝕜 (f ∘ g) x` — the ∘ form; the eta might need show. Let me use:
```
have hg : DifferentiableAt ℝ (fun y : ℝ => (y + 10) ^ 2) x := by
exact (differentiableAt_id.add_const 10).pow 2
```
— and check if DifferentiableAt.pow exists with the right form; if not, fun_prop should handle: `(by fun_prop : DifferentiableAt ℝ (fun y : ℝ => (y + 10) ^ 2) x)` — fun_prop is available (used in this file: `by fun_prop` for continuity) ✓. Use fun_prop for both the continuity and differentiability clauses' pieces: continuity: (by fun_prop : ContinuousWithinAt (fun y => log y/(y+10)^2) (Ici 13) x)? — the pattern needs .continuousAt.continuousWithinAt from DifferentiableAt — use: ((Real.differentiableAt_log hx0).div (by fun_prop) hx10).continuousAt.continuousWithinAt with (by fun_prop : DifferentiableAt ℝ (fun y : ℝ => (y+10)^2) x) inline. Let me write it that way.
For the F antiderivative (LA₁ integrable + integral): the plan from my analysis. Let me write it:
```
lemma hasDerivAt_log_div_add_sq_antideriv (x : ℝ) (hx0 : x ≠ 0) (hx10 : x + 10 ≠ 0) :
HasDerivAt (fun y : ℝ => -Real.log y / (y + 10) + (1 / 10) * Real.log (y / (y + 10)))
(Real.log x / (x + 10) ^ 2) x := by
-- F1 = −log y/(y+10)
have hF1 : HasDerivAt (fun y : ℝ => -Real.log y / (y + 10))
(-(1 / (x * (x + 10))) + Real.log x / (x + 10) ^ 2) x := by
have h1 := ((Real.hasDerivAt_log hx0).div ((hasDerivAt_id' x).const_add 10) hx10).neg
rw [show (-(Real.log / fun y => y + 10)) = (fun y : ℝ => -Real.log y / (y + 10)) from by
ext y; simp only [Pi.neg_apply, Pi.div_apply]] at h1
rw [show (-(x⁻¹ * (x + 10) - Real.log x * 1) / (x + 10) ^ 2)
= -(1 / (x * (x + 10))) + Real.log x / (x + 10) ^ 2 from by
field_simp [hx0, hx10]
ring] at h1
exact h1
-- F2 = (1/10)·log(y/(y+10))
have hF2 : HasDerivAt (fun y : ℝ => (1 / 10) * Real.log (y / (y + 10)))
(1 / (x * (x + 10))) x := by
have hratio : HasDerivAt (fun y : ℝ => y / (y + 10)) (10 / (x + 10) ^ 2) x := by
have h := (hasDerivAt_id' x).div ((hasDerivAt_id' x).const_add 10) hx10
rw [show (1 * (x + 10) - x * 1) / (x + 10) ^ 2 = 10 / (x + 10) ^ 2 from by
field_simp [hx10]
ring] at h
exact h
have hxr : x / (x + 10) ≠ 0 := by
rw [div_ne_zero_iff]
exact ⟨hx0, hx10⟩
have h2 := (Real.hasDerivAt_log hxr).comp x hratio
have h3 := h2.const_mul (1 / 10 : ℝ)
rw [show (1 / 10 : ℝ) * ((x / (x + 10))⁻¹ * (10 / (x + 10) ^ 2))
= 1 / (x * (x + 10)) from by
field_simp [hx0, hx10]
ring] at h3
-- hmm — the comp derivative form might differ; normalize via this rw
exact h3
have hF := hF1.add hF2
rw [show (-(1 / (x * (x + 10))) + Real.log x / (x + 10) ^ 2) + 1 / (x * (x + 10))
= Real.log x / (x + 10) ^ 2 from by ring] at hF
rw [show (fun y : ℝ => -Real.log y / (y + 10)) + (fun y : ℝ => (1 / 10) * Real.log (y / (y + 10)))
= (fun y : ℝ => -Real.log y / (y + 10) + (1 / 10) * Real.log (y / (y + 10))) from by
ext y; simp only [Pi.add_apply]] at hF
exact hF
```
Concerns:
- The div derivative raw form: (f'·g − f·g')/g² — for F1: f = log, f' = x⁻¹, g = (·+10), g' = 1: raw = (x⁻¹·(x+10) − log x·1)/(x+10)² ✓ as I wrote.
- The .div's hypothesis: HasDerivAt.div (hf) (hg) (hc : g x ≠ 0)? — signature: HasDerivAt.div (hf : HasDerivAt f f' x) (hg : HasDerivAt g g' x) (hgx : g x ≠ 0) : HasDerivAt (f / g) ((f' * g x - f x * g') / (g x)^2) x? — earlier in hasDerivAt_neg_log_add_one_div they used `.div (hasDerivAt_id' x) hx0` where hx0 : x ≠ 0 — and the raw form was (x⁻¹ * x − (log x + 1) * 1) / x ^ 2 ✓ consistent.
- The hratio raw: (1·(x+10) − x·1)/(x+10)² ✓.
- h2.const_mul: `HasDerivAt.const_mul (c : ℝ) (hf : HasDerivAt f f' x) : HasDerivAt (fun x => c * f x) (c * f') x` — I think for ℝ it's c * f'. The show-rw at h3 normalizes the derivative product — if the actual form is smul (c • f'), adjust: use (c • f') form in the show. Let me hedge with a broader rw: first `rw [smul_eq_mul] at h3`? Hmm — const_mul for ℝ: `HasDerivAt.const_mul (c : 𝕜) : HasDerivAt 𝕜 f f' x → HasDerivAt 𝕜 (fun x => c * f x) (c * f') x`? I'll write the show with c * f' and if it's smul, fix at compile.
- Tendsto F → 0: write `tendsto_log_div_add_sq_antideriv`:
```
lemma tendsto_log_div_add_sq_antideriv :
Filter.Tendsto (fun y : ℝ => -Real.log y / (y + 10) + (1 / 10) * Real.log (y / (y + 10)))
Filter.atTop (𝓝 0) := by
have hratio : Filter.Tendsto (fun x : ℝ => x / (x + 10)) Filter.atTop (𝓝 1) := by
have h21 : Filter.Tendsto (fun x : ℝ => (10 : ℝ) / x) Filter.atTop (𝓝 0) := by
simpa [div_eq_mul_inv] using tendsto_inv_atTop_zero.const_mul 10
have h22 : Filter.Tendsto (fun x : ℝ => (1 : ℝ) + (10 : ℝ) / x) Filter.atTop (𝓝 (1 + 0)) :=
tendsto_const_nhds.add h21
have h23 : (fun x : ℝ => x / (x + 10)) = (fun x : ℝ => 1 / (1 + 10 / x)) := by
funext x
by_cases hx : x = 0
· rw [hx]
norm_num
· field_simp [hx]
ring
rw [h23]
have h24 : Filter.Tendsto (fun x : ℝ => 1 / (1 + (10 : ℝ) / x)) Filter.atTop (𝓝 (1 / (1 + 0))) := by
apply Filter.Tendsto.div tendsto_const_nhds h22
norm_num
simpa using h24
have hT1 : Filter.Tendsto (fun x : ℝ => Real.log x / (x + 10)) Filter.atTop (𝓝 0) := by
have h1 : Filter.Tendsto (fun x : ℝ => Real.log x / x) Filter.atTop (𝓝 0) := by
have h := Real.tendsto_pow_log_div_mul_add_atTop 1 0 1 one_ne_zero
simpa using h
have h3 : (fun x : ℝ => Real.log x / (x + 10))
= (fun x : ℝ => (Real.log x / x) * (x / (x + 10))) := by
funext x
by_cases hx : x = 0
· rw [hx]
norm_num
· field_simp [hx]
ring
rw [h3]
have h4 := h1.mul hratio
simp only [zero_mul, one_mul, mul_zero, mul_one] at h4
exact h4
have hT2 : Filter.Tendsto (fun x : ℝ => (1 / 10) * Real.log (x / (x + 10))) Filter.atTop (𝓝 0) := by
have h2 : ContinuousAt Real.log 1 := Real.continuousAt_log (by norm_num : (1 : ℝ) ≠ 0)
have h3 := (h2.tendsto.comp hratio).const_mul (1 / 10 : ℝ)
rw [Real.log_one] at h3
simpa using h3
have hT := hT1.neg.add hT2
have heq : (fun y : ℝ => -Real.log y / (y + 10) + (1 / 10) * Real.log (y / (y + 10)))
= (fun y : ℝ => -(Real.log y / (y + 10)) + (1 / 10) * Real.log (y / (y + 10))) := by
ext y
simp only [neg_div]
rw [heq]
simpa using hT
```
Concerns:
- Tendsto.div signature: `Filter.Tendsto.div (hf : Tendsto f l (𝓝 a)) (hg : Tendsto g l (𝓝 b)) (hb : b ≠ 0) : Tendsto (fun x => f x / g x) l (𝓝 (a / b))` ✓.
- h1.mul hratio: Tendsto (fun x => (log x/x)·(x/(x+10))) (𝓝 (0·1)) — 0·1: simp [zero_mul] at h4 — the 𝓝 (0*1): simp only [zero_mul] turns 0*1 → 0 ✓ but also mul_one could rewrite... I put both — careful that simp might rewrite inside the function too (log x/x — no literal products there; x/(x+10) fine). Use `simp only [zero_mul] at h4` — but the value is (0 * 1) — zero_mul ✓. Then exact h4.
- hT1.neg : Tendsto (−(log x/(x+10))) (𝓝 (−0)) — −0 = 0 by neg_zero — the .add hT2: value (−0) + 0 — simpa should normalize (neg_zero, add_zero).
- Real.continuousAt_log : (x ≠ 0) → ContinuousAt Real.log x ✓.
Then:
```
lemma integrableOn_log_div_add_sq :
IntegrableOn (fun x : ℝ => Real.log x / (x + 10) ^ 2) (Set.Ioi (13 : ℝ)) volume := by
apply integrableOn_Ioi_deriv_of_nonneg' (fun x hx =>
hasDerivAt_log_div_add_sq_antideriv x (by
have h := (Set.mem_Ici.mp hx); linarith) (by
have h := (Set.mem_Ici.mp hx); linarith))
· intro x hx
have hx13 : (13 : ℝ) < x := hx
have hlog : (0 : ℝ) ≤ Real.log x := Real.log_nonneg (by linarith)
positivity
· exact tendsto_log_div_add_sq_antideriv
```
Hmm — integrableOn_Ioi_deriv_of_nonneg's nonneg: 0 ≤ f x where f = the integrand — log x/(x+10)² ≥ 0 for x > 13 ✓.
```
lemma integral_log_div_add_sq_Ioi_thirteen :
∫ x in Set.Ioi (13 : ℝ), Real.log x / (x + 10) ^ 2
= Real.log 13 / 23 + Real.log (23 / 13) / 10 := by
have h := integral_Ioi_of_hasDerivAt_of_tendsto'
(fun x hx => hasDerivAt_log_div_add_sq_antideriv x (by
have h := (Set.mem_Ici.mp hx); linarith) (by
have h := (Set.mem_Ici.mp hx); linarith))
integrableOn_log_div_add_sq tendsto_log_div_add_sq_antideriv
rw [h]
have h1 : -Real.log 13 / (13 + 10) + (1 / 10) * Real.log (13 / (13 + 10))
= -(Real.log 13 / 23 + Real.log (23 / 13) / 10) := by
have h2 : Real.log (13 / (13 + 10)) = -Real.log (23 / 13) := by
rw [show (13 : ℝ) / (13 + 10) = (23 / 13)⁻¹ from by norm_num, Real.log_inv]
rw [h2]
ring
rw [h1]
show (-0 : ℝ) - -(Real.log 13 / 23 + Real.log (23 / 13) / 10)
= Real.log 13 / 23 + Real.log (23 / 13) / 10
ring
```
Wait — the integral value: 0 − F(13): F(13) = −log 13/23 + (1/10)·log(13/23): and log(13/23) = −log(23/13): F(13) = −log 13/23 − (1/10)log(23/13) = −(log 13/23 + log(23/13)/10) ✓. So integral = 0 − F(13) = log 13/23+log(23/13)/10 ✓. The tendsto value: −0 (from the antiderivative tendsto → 0 — integral_Ioi_of_hasDerivAt_of_tendsto' gives (0 − F a) where the 0 is the limit — the limit is exactly 0 here (my tendsto lemma concludes 𝓝 0) — so the form is `(0:ℝ) − F(13)`. My earlier RW₀ needed `-0` because the tendsto was .neg producing -0. Here the limit is stated 0 — the integral lemma's statement: integral_Ioi_of_hasDerivAt_of_tendsto' (hderiv)(hintegrable)(htendsto : Tendsto F atTop (𝓝 0)): ∫ = 0 − F a. So the rw [h] gives (0:ℝ) − F(13) — then rw [h1] (the F(13) form) then show 0 − −(...) = ... — use show (0:ℝ) - -(X) = X; ring. Let me write that.
LA₀ (1/(x+10)²):
```
lemma antitoneOn_one_div_add_sq : AntitoneOn (fun x : ℝ => 1 / (x + 10) ^ 2) (Set.Ici (13 : ℝ)) := by
intro a ha b hb hab
rw [Set.mem_Ici] at ha hb
have ha0 : (0 : ℝ) < a + 10 := by linarith
exact one_div_le_one_div_of_le (pow_pos ha0 2)
(pow_le_pow_left₀ ha0.le (by linarith : a + 10 ≤ b + 10) 2)
lemma hasDerivAt_neg_inv_add (x : ℝ) (hx10 : x + 10 ≠ 0) :
HasDerivAt (fun y : ℝ => -(y + 10)⁻¹) (1 / (x + 10) ^ 2) x := by
have h2 := ((hasDerivAt_id' x).const_add 10).inv hx10
have h3 := h2.neg
rw [show (-(fun y : ℝ => y + 10)⁻¹) = (fun y : ℝ => -(y + 10)⁻¹) from by
ext y; simp only [Pi.neg_apply, Pi.inv_apply]] at h3
rwa [show (-(-1 / (x + 10) ^ 2)) = 1 / (x + 10) ^ 2 from by ring] at h3
```
Wait — the inv derivative here: ((hasDerivAt_id' x).const_add 10).inv hx10 : HasDerivAt (fun y => (y+10)⁻¹) (-1/(x+10)^2)?? — the deriv form from HasDerivAt.inv: -(1/(g x)^2)·g' = -1/(x+10)²·1 — the display form might be -(1/(x+10)^2 * 1) or (-1/(x+10)^2)·... normalize: the .neg gives -(-1/(x+10)²·1)-ish: my show-rw assumes the form -(-1/(x+10)^2) — might need -(-(1/(x+10)^2 * 1)): hedge with a ring-normalizing rw: rwa [show (-(-1 / (x + 10) ^ 2 * 1)) = 1 / (x + 10) ^ 2 from by ring] — safer: convert h3 using 1 then ring_nf? NO convert on HasDerivAt (banked). Alternative: after the function rw, use `simpa [mul_one, neg_neg] using h3` for the derivative normalization:
```
rw [show (-(fun y : ℝ => y + 10)⁻¹) = (fun y : ℝ => -(y + 10)⁻¹) from by
ext y; simp only [Pi.neg_apply, Pi.inv_apply]] at h3
simpa [mul_one, neg_neg, one_div] using h3
```
- integrableOn_one_div_add_sq + integral = 1/23 + LA₀ brick (same pattern as RW₀).
LA₁'s summable for LA₂:
```
lemma tail14_log_div_add_sq_summable :
Summable (fun j : ℕ => Real.log ((j : ℝ) + 14) / (((j : ℝ) + 14) + 10) ^ 2) := by
have h := antitoneOn_log_div_add_sq.summable_of_integrableOn_Ioi
integrableOn_log_div_add_sq (fun t ht => by
have ht13 : (13 : ℝ) < t := ht
have hlog : (0 : ℝ) ≤ Real.log t := Real.log_nonneg (by linarith)
positivity)
have h2 := (summable_nat_add_iff (f := fun n : ℕ =>
Real.log (n : ℝ) / ((n : ℝ) + 10) ^ 2) 14).mpr h
refine h2.congr fun n => ?_
push_cast
ring_nf
```
Wait — h from summable_of_integrableOn_Ioi gives Summable (fun n => f ↑n) with f = (fun x => log x/(x+10)^2): f ↑n = log ↑n/(↑n+10)^2 — the summable_nat_add_iff shift: (fun n => log ↑n/(↑n+10)^2) at (n+14): log ↑(n+14)/(↑(n+14)+10)^2 — congr to log((n:ℝ)+14)/(((n:ℝ)+14)+10)^2 via push_cast/ring_nf ✓.
LA₁ brick:
```
lemma tail14_log_div_add_sq_le :
(∑' j : ℕ, Real.log ((j : ℝ) + 14) / (((j : ℝ) + 14) + 10) ^ 2) ≤ 0.1687 := by
have hle := antitoneOn_log_div_add_sq.tsum_comp_add_le_integral 13
integrableOn_log_div_add_sq (fun t ht => by
have ht13 : (13 : ℝ) < t := ht
have hlog : (0 : ℝ) ≤ Real.log t := Real.log_nonneg (by linarith)
positivity)
have hInt13 : (∫ x in Set.Ioi ((13 : ℕ) : ℝ), Real.log x / (x + 10) ^ 2)
= Real.log 13 / 23 + Real.log (23 / 13) / 10 := by
rw [show ((13 : ℕ) : ℝ) = (13 : ℝ) by norm_num]
exact integral_log_div_add_sq_Ioi_thirteen
rw [hInt13] at hle
have hcongr : (∑' n : ℕ, Real.log (↑(n + 13 + 1) : ℕ) / ((↑(n + 13 + 1) : ℕ) + 10) ^ 2)
= ∑' n : ℕ, Real.log ((n : ℝ) + 14) / (((n : ℝ) + 14) + 10) ^ 2 := by
refine tsum_congr fun n => ?_
have h1 : ((↑(n + 13 + 1) : ℕ) : ℝ) = (n : ℝ) + 14 := by push_cast; ring
rw [h1]
rw [hcongr] at hle
have h1 := log_thirteen_le
have h2 := log_23_13_le
linarith [hle, h1, h2]
```
2.565/23 + 0.571/10 = 0.111522+0.0571 = 0.168622 ≤ 0.1687 ✓ linarith ✓.
LA₂:
```
lemma tail14_loglog_div_add_sq_le :
(∑' j : ℕ, Real.log (Real.log ((j : ℝ) + 14)) / (((j : ℝ) + 14) + 10) ^ 2) ≤ 0.0621 := by
<same skeleton as RW₂ with the 0.3679·0.1687 = 0.06206623 ≤ 0.0621 fold>
```
nonneg for LA₂'s of_norm_bounded: loglog(j+14) ≥ loglog 14 ≥ 0 (log 14 ≥ 2.6388 ≥ 1 ✓).
Let me write §11b now.
Now §11b (the left-tail bricks). Writing the LA set.
tool: Edit
input
{
"replace_all": false,
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiTightR.lean",
"old_string": " linarith [hle, h4, h3]\n\nend NguyenRH1\n\nend",
"new_string": " linarith [hle, h4, h3]\n\n/-! ## 12. Piece 3d: the left-tail weight bricks (\u03a3 over j \u2265 14) -/\n\n/-- 1/(x+10)\u00b2 is antitone on Ici 13. -/\nlemma antitoneOn_one_div_add_sq :\n AntitoneOn (fun x : \u211d => 1 / (x + 10) ^ 2) (Set.Ici (13 : \u211d)) := by\n intro a ha b hb hab\n rw [Set.mem_Ici] at ha hb\n have ha0 : (0 : \u211d) < a + 10 := by linarith\n exact one_div_le_one_div_of_le (pow_pos ha0 2)\n (pow_le_pow_left\u2080 ha0.le (by linarith : a + 10 \u2264 b + 10) 2)\n\n/-- \u2212(x+10)\u207b\u00b9 has derivative 1/(x+10)\u00b2 (x + 10 \u2260 0). -/\nlemma hasDerivAt_neg_inv_add (x : \u211d) (hx10 : x + 10 \u2260 0) :\n HasDerivAt (fun y : \u211d => -(y + 10)\u207b\u00b9) (1 / (x + 10) ^ 2) x := by\n have h2 := ((hasDerivAt_id' x).const_add 10).inv hx10\n have h3 := h2.neg\n rw [show (-(fun y : \u211d => y + 10)\u207b\u00b9) = (fun y : \u211d => -(y + 10)\u207b\u00b9) from by\n ext y\n simp only [Pi.neg_apply, Pi.inv_apply]] at h3\n simpa [mul_one, neg_neg, one_div] using h3\n\n/-- 1/(x+10)\u00b2 is integrable on Ioi 13. -/\nlemma integrableOn_one_div_add_sq :\n IntegrableOn (fun x : \u211d => 1 / (x + 10) ^ 2) (Set.Ioi (13 : \u211d)) volume := by\n apply integrableOn_Ioi_deriv_of_nonneg' (fun x hx =>\n hasDerivAt_neg_inv_add x (by\n have h := (Set.mem_Ici.mp hx); linarith))\n \u00b7 intro x hx\n have hx13 : (13 : \u211d) < x := hx\n positivity\n \u00b7 simpa using tendsto_inv_atTop_zero.neg\n\n/-- The integral of 1/(x+10)\u00b2 over Ioi 13 is 1/23. -/\nlemma integral_one_div_add_sq_Ioi_thirteen :\n \u222b x in Set.Ioi (13 : \u211d), 1 / (x + 10) ^ 2 = 1 / 23 := by\n have h := integral_Ioi_of_hasDerivAt_of_tendsto'\n (fun x hx => hasDerivAt_neg_inv_add x (by\n have h := (Set.mem_Ici.mp hx); linarith))\n integrableOn_one_div_add_sq (by simpa using tendsto_inv_atTop_zero.neg)\n rw [h]\n show (-0 : \u211d) - -((13 + 10 : \u211d)\u207b\u00b9) = 1 / 23\n norm_num\n\n/-- **LA\u2080**: \u03a3_{j\u226514} 1/(j+10)\u00b2 \u2264 1/23. -/\nlemma tail14_inv_add_sq_le :\n (\u2211' j : \u2115, (1 : \u211d) / (((j : \u211d) + 14) + 10) ^ 2) \u2264 1 / 23 := by\n have hle := antitoneOn_one_div_add_sq.tsum_comp_add_le_integral 13\n integrableOn_one_div_add_sq (fun t ht => by\n have ht13 : (13 : \u211d) < t := ht\n positivity)\n have hInt13 : (\u222b x in Set.Ioi ((13 : \u2115) : \u211d), 1 / (x + 10) ^ 2) = 1 / 23 := by\n rw [show ((13 : \u2115) : \u211d) = (13 : \u211d) by norm_num]\n exact integral_one_div_add_sq_Ioi_thirteen\n rw [hInt13] at hle\n have hcongr : (\u2211' n : \u2115, 1 / ((\u2191(n + 13 + 1) : \u2115) + 10) ^ 2)\n = \u2211' n : \u2115, (1 : \u211d) / (((n : \u211d) + 14) + 10) ^ 2 := by\n refine tsum_congr fun n => ?_\n have h1 : ((\u2191(n + 13 + 1) : \u2115) : \u211d) = (n : \u211d) + 14 := by push_cast; ring\n rw [h1]\n rw [hcongr] at hle\n exact hle\n\n/-- log x/(x+10)\u00b2 is antitone on Ici 13 (derivative\n((x+10)/x \u2212 2 log x)/(x+10)\u00b3 \u2264 0 since (x+10)/x \u2264 2 \u2264 2 log x). -/\nlemma antitoneOn_log_div_add_sq :\n AntitoneOn (fun x : \u211d => Real.log x / (x + 10) ^ 2) (Set.Ici (13 : \u211d)) := by\n apply antitoneOn_of_deriv_nonpos (convex_Ici 13)\n \u00b7 intro x hx\n have hx0 : x \u2260 0 := by have h := (Set.mem_Ici.mp hx); linarith\n have hx10 : (x + 10) ^ 2 \u2260 0 := by\n have h := (Set.mem_Ici.mp hx)\n positivity\n exact ((Real.differentiableAt_log hx0).div (by\n fun_prop : DifferentiableAt \u211d (fun y : \u211d => (y + 10) ^ 2) x) hx10)\n |>.continuousAt.continuousWithinAt\n \u00b7 intro x hx\n have hx0 : x \u2260 0 := by\n have h : (13 : \u211d) < x := Set.mem_Ioi.mp (by rwa [interior_Ici] at hx)\n linarith\n have hx10 : (x + 10) ^ 2 \u2260 0 := by\n have h : (13 : \u211d) < x := Set.mem_Ioi.mp (by rwa [interior_Ici] at hx)\n positivity\n exact ((Real.differentiableAt_log hx0).div (by\n fun_prop : DifferentiableAt \u211d (fun y : \u211d => (y + 10) ^ 2) x) hx10)\n |>.differentiableWithinAt\n \u00b7 intro x hx\n have hx13 : (13 : \u211d) < x := Set.mem_Ioi.mp (by rwa [interior_Ici] at hx)\n have hx0 : x \u2260 0 := by linarith\n have hx10 : (x + 10) \u2260 0 := by linarith\n have hderiv : deriv (fun y => Real.log y / (y + 10) ^ 2) x\n = ((x + 10) / x - 2 * Real.log x) / (x + 10) ^ 3 := by\n have h1 : HasDerivAt (fun y : \u211d => (y + 10) ^ 2) (2 * (x + 10)) x := by\n have h := (hasDerivAt_pow 2 (x + 10)).comp x ((hasDerivAt_id' x).const_add 10)\n rw [show ((2 : \u2115) : \u211d) * (x + 10) ^ (2 - 1) * 1 = 2 * (x + 10) from by\n rw [show (2 : \u2115) - 1 = 1 from rfl, pow_one]\n push_cast\n ring] at h\n exact h\n have h2 := (Real.hasDerivAt_log hx0).div h1 (by positivity : (x + 10) ^ 2 \u2260 0)\n rw [h2.deriv]\n field_simp [hx0, hx10]\n ring\n rw [hderiv]\n have hlog1 : (1 : \u211d) \u2264 Real.log x := by\n have h1 : Real.exp 1 \u2264 13 := Real.exp_one_lt_d9.le.trans (by norm_num)\n have h2 : (1 : \u211d) \u2264 Real.log 13 := by\n rw [Real.le_log_iff_exp_le (by norm_num : (0 : \u211d) < 13)]\n exact h1\n exact h2.trans (Real.log_le_log (by positivity : (0 : \u211d) < 13) hx13.le)\n have hbound : (x + 10) / x \u2264 2 := by\n rw [div_le_iff\u2080 (by linarith : (0 : \u211d) < x)]\n linarith\n have h3 : (x + 10) / x - 2 * Real.log x \u2264 0 := by linarith [hlog1, hbound]\n exact div_nonpos_of_nonpos_of_nonneg h3 (by positivity)\n\n/-- The antiderivative of log x/(x+10)\u00b2:\nF(x) = \u2212log x/(x+10) + (1/10)\u00b7log(x/(x+10)). -/\nlemma hasDerivAt_log_div_add_sq_antideriv (x : \u211d) (hx0 : x \u2260 0) (hx10 : x + 10 \u2260 0) :\n HasDerivAt (fun y : \u211d => -Real.log y / (y + 10) + (1 / 10) * Real.log (y / (y + 10)))\n (Real.log x / (x + 10) ^ 2) x := by\n have hF1 : HasDerivAt (fun y : \u211d => -Real.log y / (y + 10))\n (-(1 / (x * (x + 10))) + Real.log x / (x + 10) ^ 2) x := by\n have h1 := ((Real.hasDerivAt_log hx0).div ((hasDerivAt_id' x).const_add 10) hx10).neg\n rw [show (-(Real.log / fun y => y + 10)) = (fun y : \u211d => -Real.log y / (y + 10)) from by\n ext y; simp only [Pi.neg_apply, Pi.div_apply]] at h1\n rw [show (-(x\u207b\u00b9 * (x + 10) - Real.log x * 1) / (x + 10) ^ 2)\n = -(1 / (x * (x + 10))) + Real.log x / (x + 10) ^ 2 from by\n field_simp [hx0, hx10]\n ring] at h1\n exact h1\n have hF2 : HasDerivAt (fun y : \u211d => (1 / 10) * Real.log (y / (y + 10)))\n (1 / (x * (x + 10))) x := by\n have hratio : HasDerivAt (fun y : \u211d => y / (y + 10)) (10 / (x + 10) ^ 2) x := by\n have h := (hasDerivAt_id' x).div ((hasDerivAt_id' x).const_add 10) hx10\n rw [show (1 * (x + 10) - x * 1) / (x + 10) ^ 2 = 10 / (x + 10) ^ 2 from by\n field_simp [hx10]\n ring] at h\n exact h\n have hxr : x / (x + 10) \u2260 0 := by\n rw [div_ne_zero_iff]\n exact \u27e8hx0, hx10\u27e9\n have h2 := (Real.hasDerivAt_log hxr).comp x hratio\n have h3 := h2.const_mul (1 / 10 : \u211d)\n rw [show (1 / 10 : \u211d) * ((x / (x + 10))\u207b\u00b9 * (10 / (x + 10) ^ 2))\n = 1 / (x * (x + 10)) from by\n field_simp [hx0, hx10]\n ring] at h3\n exact h3\n have hF := hF1.add hF2\n rw [show (-(1 / (x * (x + 10))) + Real.log x / (x + 10) ^ 2) + 1 / (x * (x + 10))\n = Real.log x / (x + 10) ^ 2 from by ring] at hF\n rw [show (fun y : \u211d => -Real.log y / (y + 10))\n + (fun y : \u211d => (1 / 10) * Real.log (y / (y + 10)))\n = (fun y : \u211d => -Real.log y / (y + 10) + (1 / 10) * Real.log (y / (y + 10))) from by\n ext y; simp only [Pi.add_apply]] at hF\n exact hF\n\n/-- The antiderivative tends to 0 at infinity. -/\nlemma tendsto_log_div_add_sq_antideriv :\n Filter.Tendsto (fun y : \u211d => -Real.log y / (y + 10) + (1 / 10) * Real.log (y / (y + 10)))\n Filter.atTop (\ud835\udcdd 0) := by\n have hratio : Filter.Tendsto (fun x : \u211d => x / (x + 10)) Filter.atTop (\ud835\udcdd 1) := by\n have h21 : Filter.Tendsto (fun x : \u211d => (10 : \u211d) / x) Filter.atTop (\ud835\udcdd 0) := by\n simpa [div_eq_mul_inv] using tendsto_inv_atTop_zero.const_mul 10\n have h22 : Filter.Tendsto (fun x : \u211d => (1 : \u211d) + (10 : \u211d) / x) Filter.atTop\n (\ud835\udcdd (1 + 0)) :=\n tendsto_const_nhds.add h21\n have h23 : (fun x : \u211d => x / (x + 10)) = (fun x : \u211d => 1 / (1 + 10 / x)) := by\n funext x\n by_cases hx : x = 0\n \u00b7 rw [hx]\n norm_num\n \u00b7 field_simp [hx]\n ring\n rw [h23]\n have h24 : Filter.Tendsto (fun x : \u211d => 1 / (1 + (10 : \u211d) / x)) Filter.atTop\n (\ud835\udcdd (1 / (1 + 0))) := by\n apply Filter.Tendsto.div tendsto_const_nhds h22\n norm_num\n simpa using h24\n have hT1 : Filter.Tendsto (fun x : \u211d => Real.log x / (x + 10)) Filter.atTop (\ud835\udcdd 0) := by\n have h1 : Filter.Tendsto (fun x : \u211d => Real.log x / x) Filter.atTop (\ud835\udcdd 0) := by\n have h := Real.tendsto_pow_log_div_mul_add_atTop 1 0 1 one_ne_zero\n simpa using h\n have h3 : (fun x : \u211d => Real.log x / (x + 10))\n = (fun x : \u211d => (Real.log x / x) * (x / (x + 10))) := by\n funext x\n by_cases hx : x = 0\n \u00b7 rw [hx]\n norm_num\n \u00b7 field_simp [hx]\n ring\n rw [h3]\n have h4 := h1.mul hratio\n simp only [zero_mul] at h4\n exact h4\n have hT2 : Filter.Tendsto (fun x : \u211d => (1 / 10) * Real.log (x / (x + 10))) Filter.atTop\n (\ud835\udcdd 0) := by\n have h2 : ContinuousAt Real.log 1 := Real.continuousAt_log (by norm_num : (1 : \u211d) \u2260 0)\n have h3 := (h2.tendsto.comp hratio).const_mul (1 / 10 : \u211d)\n rw [Real.log_one] at h3\n simpa using h3\n have hT := hT1.neg.add hT2\n have heq : (fun y : \u211d => -Real.log y / (y + 10) + (1 / 10) * Real.log (y / (y + 10)))\n = (fun y : \u211d => -(Real.log y / (y + 10)) + (1 / 10) * Real.log (y / (y + 10))) := by\n ext y\n simp only [neg_div]\n rw [heq]\n simpa using hT\n\n/-- log x/(x+10)\u00b2 is integrable on Ioi 13. -/\nlemma integrableOn_log_div_add_sq :\n IntegrableOn (fun x : \u211d => Real.log x / (x + 10) ^ 2) (Set.Ioi (13 : \u211d)) volume := by\n apply integrableOn_Ioi_deriv_of_nonneg' (fun x hx =>\n hasDerivAt_log_div_add_sq_antideriv x (by\n have h := (Set.mem_Ici.mp hx); linarith) (by\n have h := (Set.mem_Ici.mp hx); linarith))\n \u00b7 intro x hx\n have hx13 : (13 : \u211d) < x := hx\n have hlog : (0 : \u211d) \u2264 Real.log x := Real.log_nonneg (by linarith)\n positivity\n \u00b7 exact tendsto_log_div_add_sq_antideriv\n\n/-- The integral of log x/(x+10)\u00b2 over Ioi 13 is log 13/23 + log(23/13)/10. -/\nlemma integral_log_div_add_sq_Ioi_thirteen :\n \u222b x in Set.Ioi (13 : \u211d), Real.log x / (x + 10) ^ 2\n = Real.log 13 / 23 + Real.log (23 / 13) / 10 := by\n have h := integral_Ioi_of_hasDerivAt_of_tendsto'\n (fun x hx => hasDerivAt_log_div_add_sq_antideriv x (by\n have h := (Set.mem_Ici.mp hx); linarith) (by\n have h := (Set.mem_Ici.mp hx); linarith))\n integrableOn_log_div_add_sq tendsto_log_div_add_sq_antideriv\n rw [h]\n have h1 : -Real.log 13 / (13 + 10) + (1 / 10) * Real.log (13 / (13 + 10))\n = -(Real.log 13 / 23 + Real.log (23 / 13) / 10) := by\n have h2 : Real.log (13 / (13 + 10)) = -Real.log (23 / 13) := by\n rw [show (13 : \u211d) / (13 + 10) = (23 / 13)\u207b\u00b9 from by norm_num, Real.log_inv]\n rw [h2]\n ring\n rw [h1]\n show (0 : \u211d) - -(Real.log 13 / 23 + Real.log (23 / 13) / 10)\n = Real.log 13 / 23 + Real.log (23 / 13) / 10\n ring\n\n/-- The shifted log-family is summable. -/\nlemma tail14_log_div_add_sq_summable :\n Summable (fun j : \u2115 => Real.log ((j : \u211d) + 14) / (((j : \u211d) + 14) + 10) ^ 2) := by\n have h := antitoneOn_log_div_add_sq.summable_of_integrableOn_Ioi\n integrableOn_log_div_add_sq (fun t ht => by\n have ht13 : (13 : \u211d) < t := ht\n have hlog : (0 : \u211d) \u2264 Real.log t := Real.log_nonneg (by linarith)\n positivity)\n have h2 := (summable_nat_add_iff (f := fun n : \u2115 =>\n Real.log (n : \u211d) / ((n : \u211d) + 10) ^ 2) 14).mpr h\n refine h2.congr fun n => ?_\n push_cast\n ring_nf\n\n/-- **LA\u2081**: \u03a3_{j\u226514} log j/(j+10)\u00b2 \u2264 0.1687. -/\nlemma tail14_log_div_add_sq_le :\n (\u2211' j : \u2115, Real.log ((j : \u211d) + 14) / (((j : \u211d) + 14) + 10) ^ 2) \u2264 0.1687 := by\n have hle := antitoneOn_log_div_add_sq.tsum_comp_add_le_integral 13\n integrableOn_log_div_add_sq (fun t ht => by\n have ht13 : (13 : \u211d) < t := ht\n have hlog : (0 : \u211d) \u2264 Real.log t := Real.log_nonneg (by linarith)\n positivity)\n have hInt13 : (\u222b x in Set.Ioi ((13 : \u2115) : \u211d), Real.log x / (x + 10) ^ 2)\n = Real.log 13 / 23 + Real.log (23 / 13) / 10 := by\n rw [show ((13 : \u2115) : \u211d) = (13 : \u211d) by norm_num]\n exact integral_log_div_add_sq_Ioi_thirteen\n rw [hInt13] at hle\n have hcongr : (\u2211' n : \u2115, Real.log (\u2191(n + 13 + 1) : \u2115) / ((\u2191(n + 13 + 1) : \u2115) + 10) ^ 2)\n = \u2211' n : \u2115, Real.log ((n : \u211d) + 14) / (((n : \u211d) + 14) + 10) ^ 2 := by\n refine tsum_congr fun n => ?_\n have h1 : ((\u2191(n + 13 + 1) : \u2115) : \u211d) = (n : \u211d) + 14 := by push_cast; ring\n rw [h1]\n rw [hcongr] at hle\n have h1 := log_thirteen_le\n have h2 := log_23_13_le\n linarith [hle, h1, h2]\n\n/-- **LA\u2082**: \u03a3_{j\u226514} log log j/(j+10)\u00b2 \u2264 0.0621 (via log log j \u2264 (1/e)\u00b7log j). -/\nlemma tail14_loglog_div_add_sq_le :\n (\u2211' j : \u2115, Real.log (Real.log ((j : \u211d) + 14)) / (((j : \u211d) + 14) + 10) ^ 2) \u2264 0.0621 := by\n have hpt : \u2200 j : \u2115, Real.log (Real.log ((j : \u211d) + 14)) / (((j : \u211d) + 14) + 10) ^ 2\n \u2264 (1 / Real.exp 1) * (Real.log ((j : \u211d) + 14) / (((j : \u211d) + 14) + 10) ^ 2) := by\n intro j\n have hj1 : (1 : \u211d) < (j : \u211d) + 14 := by\n have h : (0 : \u211d) \u2264 (j : \u211d) := Nat.cast_nonneg j\n linarith\n have h2 := log_log_le_div_exp hj1\n have h3 : (0 : \u211d) \u2264 (((j : \u211d) + 14) + 10) ^ 2 := by positivity\n have h4 : Real.log (Real.log ((j : \u211d) + 14)) / (((j : \u211d) + 14) + 10) ^ 2\n \u2264 ((1 / Real.exp 1) * Real.log ((j : \u211d) + 14)) / (((j : \u211d) + 14) + 10) ^ 2 :=\n div_le_div_of_nonneg_right h2 h3\n rw [mul_div_assoc] at h4\n exact h4\n have hsumm2 : Summable (fun j : \u2115 =>\n (1 / Real.exp 1) * (Real.log ((j : \u211d) + 14) / (((j : \u211d) + 14) + 10) ^ 2)) :=\n tail14_log_div_add_sq_summable.mul_left _\n have hsumm : Summable (fun j : \u2115 =>\n Real.log (Real.log ((j : \u211d) + 14)) / (((j : \u211d) + 14) + 10) ^ 2) := by\n apply Summable.of_norm_bounded hsumm2\n intro j\n rw [Real.norm_eq_abs]\n rw [abs_of_nonneg (by\n have hj1 : (1 : \u211d) \u2264 Real.log ((j : \u211d) + 14) := by\n have h1 := log_fourteen_ge\n have h2 : Real.log 14 \u2264 Real.log ((j : \u211d) + 14) :=\n Real.log_le_log (by norm_num : (0 : \u211d) < 14) (by\n have h : (0 : \u211d) \u2264 (j : \u211d) := Nat.cast_nonneg j\n linarith)\n linarith [h1, h2]\n have h3 : (0 : \u211d) \u2264 Real.log (Real.log ((j : \u211d) + 14)) := Real.log_nonneg hj1\n positivity : (0 : \u211d) \u2264\n Real.log (Real.log ((j : \u211d) + 14)) / (((j : \u211d) + 14) + 10) ^ 2)]\n exact hpt j\n have hle := Summable.tsum_le_tsum hpt hsumm hsumm2\n rw [tsum_mul_left] at hle\n have h1 := tail14_log_div_add_sq_le\n have h2 := one_div_exp_one_le\n have h4 : (1 / Real.exp 1) * (\u2211' j : \u2115,\n Real.log ((j : \u211d) + 14) / (((j : \u211d) + 14) + 10) ^ 2)\n \u2264 (1 / Real.exp 1) * 0.1687 :=\n mul_le_mul_of_nonneg_left h1 (by positivity : (0 : \u211d) \u2264 1 / Real.exp 1)\n have h3 : (1 / Real.exp 1) * 0.1687 \u2264 0.0621 := by\n calc (1 / Real.exp 1) * 0.1687 \u2264 0.3679 * 0.1687 :=\n mul_le_mul_of_nonneg_right h2 (by norm_num)\n _ \u2264 0.0621 := by norm_num\n linarith [hle, h4, h3]\n\nend NguyenRH1\n\nend"
}
raw content_json (database row)
[{"type":"thinking","thinking":"Section 11a compiles clean. Now §11b: the LA bricks (left-tail, j ≥ 14, weight 1/(j+10)²). This includes the harder antiderivative for log x/(x+10)² and the antitone proof. Let me write it.\n\nPlan recap:\n- antitoneOn_one_div_add_sq (direct).\n- hasDerivAt_neg_inv_add (F = −(x+10)⁻¹) + integrableOn_one_div_add_sq + integral = 1/23 + LA₀.\n- antitoneOn_log_div_add_sq (calculus: deriv = ((x+10)/x − 2 log x)/(x+10)³ ≤ 0).\n- The antiderivative F = −log x/(x+10) + (1/10)·log(x/(x+10)) with HasDerivAt = log x/(x+10)², Tendsto → 0; integrableOn_log_div_add_sq; integral = log 13/23 + log(23/13)/10; LA₁ ≤ 0.1687.\n- LA₂ ≤ 0.0621 (pointwise trick).\n\nFor antitoneOn_log_div_add_sq — use antitoneOn_of_deriv_nonpos (convex_Ici 13) with continuity/differentiability/deriv-nonpos (the antitoneOn_log_div_sq pattern from this file, which used interior_Ici). The deriv computation:\nderiv (fun y => log y/(y+10)²) x = ((x+10)/x − 2·log x)/(x+10)³.\nBuild the HasDerivAt: \nh1 : HasDerivAt (fun y => (y+10)^2) (2*(x+10)) x:\n ((hasDerivAt_id' x).const_add 10) then .pow? HasDerivAt.pow? For h : HasDerivAt f f' x: h.pow 2? There is `HasDerivAt.pow (hf : HasDerivAt f f' x) : HasDerivAt (fun x => (f x)^n) (n * (f x)^(n-1) * f')`? hmm — earlier I used hasDerivAt_pow 2 (x+10) .comp: ((hasDerivAt_pow 2 (x+10)).comp x h1): derivative (2·(x+10)^1)·1 — normalize: 2(x+10).\nh2 : HasDerivAt (fun y => Real.log y / (y+10)^2) (((1/x)·(x+10)^2 − log x·(2(x+10)))/((x+10)^2)^2) x := (Real.hasDerivAt_log hx0).div h1 (x+10)² ≠ 0.\nThen deriv f x = that raw value via h2.deriv; normalize: ((1/x)(x+10)² − 2(x+10) log x)/(x+10)⁴ = ((x+10)/x − 2 log x)/(x+10)³: field_simp.\nThen show ≤ 0: (x+10)/x − 2 log x ≤ 0: (x+10)/x = 1+10/x ≤ 1+10/13 = 23/13; 2 log x ≥ 2·1 = 2 ≥ 23/13 ✓ (log x ≥ 1 for x ≥ 13 ≥ e).\n\nLet me write the deriv ≤ 0 part concretely:\n```\nlemma antitoneOn_log_div_add_sq :\n AntitoneOn (fun x : ℝ => Real.log x / (x + 10) ^ 2) (Set.Ici (13 : ℝ)) := by\n apply antitoneOn_of_deriv_nonpos (convex_Ici 13)\n · intro x hx\n have hx0 : x ≠ 0 := by have h := (Set.mem_Ici.mp hx); linarith\n have hx10 : (x + 10) ^ 2 ≠ 0 := by\n have h := (Set.mem_Ici.mp hx)\n positivity\n exact ((Real.differentiableAt_log hx0).div\n (differentiableAt_const_add.pow 2) hx10).continuousAt.continuousWithinAt\n · intro x hx\n have hx0 : x ≠ 0 := by\n have h : (13 : ℝ) < x := Set.mem_Ioi.mp (by rwa [interior_Ici] at hx)\n linarith\n have hx10 : (x + 10) ^ 2 ≠ 0 := by\n have h : (13 : ℝ) < x := Set.mem_Ioi.mp (by rwa [interior_Ici] at hx)\n positivity\n exact ((Real.differentiableAt_log hx0).div\n (differentiableAt_const_add.pow 2) hx10).differentiableWithinAt\n · intro x hx\n have hx13 : (13 : ℝ) < x := Set.mem_Ioi.mp (by rwa [interior_Ici] at hx)\n have hx0 : x ≠ 0 := by linarith\n have hx10 : (x + 10) ≠ 0 := by linarith\n have hderiv : deriv (fun y => Real.log y / (y + 10) ^ 2) x\n = ((x + 10) / x - 2 * Real.log x) / (x + 10) ^ 3 := by\n have h1 : HasDerivAt (fun y : ℝ => (y + 10) ^ 2) (2 * (x + 10)) x := by\n have h := (hasDerivAt_pow 2 (x + 10)).comp x ((hasDerivAt_id' x).const_add 10)\n rw [show ((2 : ℕ) : ℝ) * (x + 10) ^ (2 - 1) * 1 = 2 * (x + 10) from by\n rw [show (2 : ℕ) - 1 = 1 from rfl, pow_one]\n push_cast\n ring] at h\n exact h\n have h2 := (Real.hasDerivAt_log hx0).div h1 (by positivity : (x + 10) ^ 2 ≠ 0)\n rw [h2.deriv]\n field_simp [hx0, hx10]\n ring\n rw [hderiv]\n have hlog1 : (1 : ℝ) ≤ Real.log x := by\n have h1 : Real.exp 1 ≤ 13 := Real.exp_one_lt_d9.le.trans (by norm_num)\n have h2 : (1 : ℝ) ≤ Real.log 13 := by\n rw [Real.le_log_iff_exp_le (by norm_num : (0 : ℝ) < 13)]\n exact h1\n exact h2.trans (Real.log_le_log (by positivity : (0 : ℝ) < 13) hx13.le)\n have hbound : (x + 10) / x ≤ 2 := by\n rw [div_le_iff₀ (by linarith : (0 : ℝ) < x)]\n linarith\n have h3 : (x + 10) / x - 2 * Real.log x ≤ 0 := by linarith [hlog1, hbound]\n exact div_nonpos_of_nonpos_of_nonneg h3 (by positivity)\n```\nHmm — `differentiableAt_const_add.pow 2`: is there `differentiableAt_const_add (c) : DifferentiableAt f (x+c)??` — banked from this file: `differentiableAt_pow takes ONE arg (the exponent)` — differentiableAt_pow 2 : DifferentiableAt (fun x => x^2)?? no — differentiableAt_pow (n) : DifferentiableAt 𝕜 (fun x => x^n) x? It was used as `(differentiableAt_pow 2)` in antitoneOn_log_div_sq: `((Real.differentiableAt_log hx0).div (differentiableAt_pow 2) (pow_ne_zero 2 hx0))` — differentiableAt_pow 2 : DifferentiableAt ℝ (fun x => x^2) x?? with x implicit. For (x+10)^2: need DifferentiableAt (fun y => (y+10)^2) x: (differentiableAt_id.add_const 10).pow 2? `DifferentiableAt.add_const : DifferentiableAt f x → DifferentiableAt (fun x => f x + c) x`? For (y+10): differentiableAt_id.add_const 10?? `DifferentiableAt.add_const (hf : DifferentiableAt 𝕜 f x) (c : 𝕜) : DifferentiableAt 𝕜 (fun x => f x + c) x` — but fun y => y+10 = (· + 10) = id + const: differentiableAt_id.add_const 10 ✓. Then .pow 2: `DifferentiableAt.pow (hf : DifferentiableAt 𝕜 f x) : DifferentiableAt 𝕜 (fun x => (f x)^n) x`?? hmm — maybe `DifferentiableAt.pow (hf) (n)`? or `differentiableAt_pow.comp`... Use: (differentiableAt_id.add_const 10).pow 2 — check name `DifferentiableAt.pow` exists (it does: DifferentiableAt.pow : DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 (fun x => f x ^ n) x? actually I think it's `DifferentiableAt.pow (hf : DifferentiableAt 𝕜 f x) (n : ℕ)`?). Risky. Alternative: continuity of log/(x+10)² via ContinuousAt directly: (Real.continuousAt_log hx0).div (continuousAt... ) — for the continuity clause use ContinuousAt: `ContinuousAt.div (Real.continuousAt_log hx0) ((continuousAt_id.add_const 10).pow 2) hx10` — ContinuousAt.pow : ContinuousAt f x → ContinuousAt (f^n) x ✓ exists? `ContinuousAt.pow (hf : ContinuousAt f x) (n : ℕ) : ContinuousAt (fun x => (f x)^n) x` ✓ I'm fairly confident. And differentiability for the interior clause: ((Real.differentiableAt_log hx0).div ((differentiableAt_id.add_const 10).pow 2) hx10).differentiableWithinAt — DifferentiableAt.pow — hmm. Alternative for differentiability: DifferentiableAt.div with g = (y+10)^2: DifferentiableAt (fun y => (y+10)^2) x: via (differentiableAt_id.add_const 10): DifferentiableAt (fun y => y+10) x ✓ then .pow 2 — `DifferentiableAt.pow : DifferentiableAt 𝕜 f x → (n : ℕ) → DifferentiableAt 𝕜 (fun x => f x ^ n) x`? Hmm — actually I recall `DifferentiableAt.pow (hf : DifferentiableAt 𝕜 f x) : DifferentiableAt 𝕜 (fun x ↦ f x ^ n) x` with n implicit — mirroring HasDerivAt.pow? In this file earlier: `(differentiableAt_pow 2)` used directly as DifferentiableAt (fun y => y^2) — so `differentiableAt_pow (n) : DifferentiableAt 𝕜 (fun x => x^n) x`?? — that's for the identity-power, not the composed. For the composed (y+10)^2: ((differentiableAt_pow 2).comp x (differentiableAt_id.add_const 10))? DifferentiableAt.comp? — hmm: `DifferentiableAt.comp (hf : DifferentiableAt 𝕜 f (g x)) (hg : DifferentiableAt 𝕜 g x) : DifferentiableAt 𝕜 (f ∘ g) x` — the ∘ form; the eta might need show. Let me use: \n```\nhave hg : DifferentiableAt ℝ (fun y : ℝ => (y + 10) ^ 2) x := by\n exact (differentiableAt_id.add_const 10).pow 2\n```\n— and check if DifferentiableAt.pow exists with the right form; if not, fun_prop should handle: `(by fun_prop : DifferentiableAt ℝ (fun y : ℝ => (y + 10) ^ 2) x)` — fun_prop is available (used in this file: `by fun_prop` for continuity) ✓. Use fun_prop for both the continuity and differentiability clauses' pieces: continuity: (by fun_prop : ContinuousWithinAt (fun y => log y/(y+10)^2) (Ici 13) x)? — the pattern needs .continuousAt.continuousWithinAt from DifferentiableAt — use: ((Real.differentiableAt_log hx0).div (by fun_prop) hx10).continuousAt.continuousWithinAt with (by fun_prop : DifferentiableAt ℝ (fun y : ℝ => (y+10)^2) x) inline. Let me write it that way.\n\nFor the F antiderivative (LA₁ integrable + integral): the plan from my analysis. Let me write it:\n\n```\nlemma hasDerivAt_log_div_add_sq_antideriv (x : ℝ) (hx0 : x ≠ 0) (hx10 : x + 10 ≠ 0) :\n HasDerivAt (fun y : ℝ => -Real.log y / (y + 10) + (1 / 10) * Real.log (y / (y + 10)))\n (Real.log x / (x + 10) ^ 2) x := by\n -- F1 = −log y/(y+10)\n have hF1 : HasDerivAt (fun y : ℝ => -Real.log y / (y + 10))\n (-(1 / (x * (x + 10))) + Real.log x / (x + 10) ^ 2) x := by\n have h1 := ((Real.hasDerivAt_log hx0).div ((hasDerivAt_id' x).const_add 10) hx10).neg\n rw [show (-(Real.log / fun y => y + 10)) = (fun y : ℝ => -Real.log y / (y + 10)) from by\n ext y; simp only [Pi.neg_apply, Pi.div_apply]] at h1\n rw [show (-(x⁻¹ * (x + 10) - Real.log x * 1) / (x + 10) ^ 2)\n = -(1 / (x * (x + 10))) + Real.log x / (x + 10) ^ 2 from by\n field_simp [hx0, hx10]\n ring] at h1\n exact h1\n -- F2 = (1/10)·log(y/(y+10))\n have hF2 : HasDerivAt (fun y : ℝ => (1 / 10) * Real.log (y / (y + 10)))\n (1 / (x * (x + 10))) x := by\n have hratio : HasDerivAt (fun y : ℝ => y / (y + 10)) (10 / (x + 10) ^ 2) x := by\n have h := (hasDerivAt_id' x).div ((hasDerivAt_id' x).const_add 10) hx10\n rw [show (1 * (x + 10) - x * 1) / (x + 10) ^ 2 = 10 / (x + 10) ^ 2 from by\n field_simp [hx10]\n ring] at h\n exact h\n have hxr : x / (x + 10) ≠ 0 := by\n rw [div_ne_zero_iff]\n exact ⟨hx0, hx10⟩\n have h2 := (Real.hasDerivAt_log hxr).comp x hratio\n have h3 := h2.const_mul (1 / 10 : ℝ)\n rw [show (1 / 10 : ℝ) * ((x / (x + 10))⁻¹ * (10 / (x + 10) ^ 2))\n = 1 / (x * (x + 10)) from by\n field_simp [hx0, hx10]\n ring] at h3\n -- hmm — the comp derivative form might differ; normalize via this rw\n exact h3\n have hF := hF1.add hF2\n rw [show (-(1 / (x * (x + 10))) + Real.log x / (x + 10) ^ 2) + 1 / (x * (x + 10))\n = Real.log x / (x + 10) ^ 2 from by ring] at hF\n rw [show (fun y : ℝ => -Real.log y / (y + 10)) + (fun y : ℝ => (1 / 10) * Real.log (y / (y + 10)))\n = (fun y : ℝ => -Real.log y / (y + 10) + (1 / 10) * Real.log (y / (y + 10))) from by\n ext y; simp only [Pi.add_apply]] at hF\n exact hF\n```\nConcerns:\n- The div derivative raw form: (f'·g − f·g')/g² — for F1: f = log, f' = x⁻¹, g = (·+10), g' = 1: raw = (x⁻¹·(x+10) − log x·1)/(x+10)² ✓ as I wrote.\n- The .div's hypothesis: HasDerivAt.div (hf) (hg) (hc : g x ≠ 0)? — signature: HasDerivAt.div (hf : HasDerivAt f f' x) (hg : HasDerivAt g g' x) (hgx : g x ≠ 0) : HasDerivAt (f / g) ((f' * g x - f x * g') / (g x)^2) x? — earlier in hasDerivAt_neg_log_add_one_div they used `.div (hasDerivAt_id' x) hx0` where hx0 : x ≠ 0 — and the raw form was (x⁻¹ * x − (log x + 1) * 1) / x ^ 2 ✓ consistent.\n- The hratio raw: (1·(x+10) − x·1)/(x+10)² ✓.\n- h2.const_mul: `HasDerivAt.const_mul (c : ℝ) (hf : HasDerivAt f f' x) : HasDerivAt (fun x => c * f x) (c * f') x` — I think for ℝ it's c * f'. The show-rw at h3 normalizes the derivative product — if the actual form is smul (c • f'), adjust: use (c • f') form in the show. Let me hedge with a broader rw: first `rw [smul_eq_mul] at h3`? Hmm — const_mul for ℝ: `HasDerivAt.const_mul (c : 𝕜) : HasDerivAt 𝕜 f f' x → HasDerivAt 𝕜 (fun x => c * f x) (c * f') x`? I'll write the show with c * f' and if it's smul, fix at compile.\n\n- Tendsto F → 0: write `tendsto_log_div_add_sq_antideriv`:\n```\nlemma tendsto_log_div_add_sq_antideriv :\n Filter.Tendsto (fun y : ℝ => -Real.log y / (y + 10) + (1 / 10) * Real.log (y / (y + 10)))\n Filter.atTop (𝓝 0) := by\n have hratio : Filter.Tendsto (fun x : ℝ => x / (x + 10)) Filter.atTop (𝓝 1) := by\n have h21 : Filter.Tendsto (fun x : ℝ => (10 : ℝ) / x) Filter.atTop (𝓝 0) := by\n simpa [div_eq_mul_inv] using tendsto_inv_atTop_zero.const_mul 10\n have h22 : Filter.Tendsto (fun x : ℝ => (1 : ℝ) + (10 : ℝ) / x) Filter.atTop (𝓝 (1 + 0)) :=\n tendsto_const_nhds.add h21\n have h23 : (fun x : ℝ => x / (x + 10)) = (fun x : ℝ => 1 / (1 + 10 / x)) := by\n funext x\n by_cases hx : x = 0\n · rw [hx]\n norm_num\n · field_simp [hx]\n ring\n rw [h23]\n have h24 : Filter.Tendsto (fun x : ℝ => 1 / (1 + (10 : ℝ) / x)) Filter.atTop (𝓝 (1 / (1 + 0))) := by\n apply Filter.Tendsto.div tendsto_const_nhds h22\n norm_num\n simpa using h24\n have hT1 : Filter.Tendsto (fun x : ℝ => Real.log x / (x + 10)) Filter.atTop (𝓝 0) := by\n have h1 : Filter.Tendsto (fun x : ℝ => Real.log x / x) Filter.atTop (𝓝 0) := by\n have h := Real.tendsto_pow_log_div_mul_add_atTop 1 0 1 one_ne_zero\n simpa using h\n have h3 : (fun x : ℝ => Real.log x / (x + 10))\n = (fun x : ℝ => (Real.log x / x) * (x / (x + 10))) := by\n funext x\n by_cases hx : x = 0\n · rw [hx]\n norm_num\n · field_simp [hx]\n ring\n rw [h3]\n have h4 := h1.mul hratio\n simp only [zero_mul, one_mul, mul_zero, mul_one] at h4\n exact h4\n have hT2 : Filter.Tendsto (fun x : ℝ => (1 / 10) * Real.log (x / (x + 10))) Filter.atTop (𝓝 0) := by\n have h2 : ContinuousAt Real.log 1 := Real.continuousAt_log (by norm_num : (1 : ℝ) ≠ 0)\n have h3 := (h2.tendsto.comp hratio).const_mul (1 / 10 : ℝ)\n rw [Real.log_one] at h3\n simpa using h3\n have hT := hT1.neg.add hT2\n have heq : (fun y : ℝ => -Real.log y / (y + 10) + (1 / 10) * Real.log (y / (y + 10)))\n = (fun y : ℝ => -(Real.log y / (y + 10)) + (1 / 10) * Real.log (y / (y + 10))) := by\n ext y\n simp only [neg_div]\n rw [heq]\n simpa using hT\n```\nConcerns:\n- Tendsto.div signature: `Filter.Tendsto.div (hf : Tendsto f l (𝓝 a)) (hg : Tendsto g l (𝓝 b)) (hb : b ≠ 0) : Tendsto (fun x => f x / g x) l (𝓝 (a / b))` ✓.\n- h1.mul hratio: Tendsto (fun x => (log x/x)·(x/(x+10))) (𝓝 (0·1)) — 0·1: simp [zero_mul] at h4 — the 𝓝 (0*1): simp only [zero_mul] turns 0*1 → 0 ✓ but also mul_one could rewrite... I put both — careful that simp might rewrite inside the function too (log x/x — no literal products there; x/(x+10) fine). Use `simp only [zero_mul] at h4` — but the value is (0 * 1) — zero_mul ✓. Then exact h4.\n- hT1.neg : Tendsto (−(log x/(x+10))) (𝓝 (−0)) — −0 = 0 by neg_zero — the .add hT2: value (−0) + 0 — simpa should normalize (neg_zero, add_zero).\n- Real.continuousAt_log : (x ≠ 0) → ContinuousAt Real.log x ✓.\n\nThen:\n```\nlemma integrableOn_log_div_add_sq :\n IntegrableOn (fun x : ℝ => Real.log x / (x + 10) ^ 2) (Set.Ioi (13 : ℝ)) volume := by\n apply integrableOn_Ioi_deriv_of_nonneg' (fun x hx =>\n hasDerivAt_log_div_add_sq_antideriv x (by\n have h := (Set.mem_Ici.mp hx); linarith) (by\n have h := (Set.mem_Ici.mp hx); linarith))\n · intro x hx\n have hx13 : (13 : ℝ) < x := hx\n have hlog : (0 : ℝ) ≤ Real.log x := Real.log_nonneg (by linarith)\n positivity\n · exact tendsto_log_div_add_sq_antideriv\n```\nHmm — integrableOn_Ioi_deriv_of_nonneg's nonneg: 0 ≤ f x where f = the integrand — log x/(x+10)² ≥ 0 for x > 13 ✓.\n\n```\nlemma integral_log_div_add_sq_Ioi_thirteen :\n ∫ x in Set.Ioi (13 : ℝ), Real.log x / (x + 10) ^ 2\n = Real.log 13 / 23 + Real.log (23 / 13) / 10 := by\n have h := integral_Ioi_of_hasDerivAt_of_tendsto'\n (fun x hx => hasDerivAt_log_div_add_sq_antideriv x (by\n have h := (Set.mem_Ici.mp hx); linarith) (by\n have h := (Set.mem_Ici.mp hx); linarith))\n integrableOn_log_div_add_sq tendsto_log_div_add_sq_antideriv\n rw [h]\n have h1 : -Real.log 13 / (13 + 10) + (1 / 10) * Real.log (13 / (13 + 10))\n = -(Real.log 13 / 23 + Real.log (23 / 13) / 10) := by\n have h2 : Real.log (13 / (13 + 10)) = -Real.log (23 / 13) := by\n rw [show (13 : ℝ) / (13 + 10) = (23 / 13)⁻¹ from by norm_num, Real.log_inv]\n rw [h2]\n ring\n rw [h1]\n show (-0 : ℝ) - -(Real.log 13 / 23 + Real.log (23 / 13) / 10)\n = Real.log 13 / 23 + Real.log (23 / 13) / 10\n ring\n```\nWait — the integral value: 0 − F(13): F(13) = −log 13/23 + (1/10)·log(13/23): and log(13/23) = −log(23/13): F(13) = −log 13/23 − (1/10)log(23/13) = −(log 13/23 + log(23/13)/10) ✓. So integral = 0 − F(13) = log 13/23+log(23/13)/10 ✓. The tendsto value: −0 (from the antiderivative tendsto → 0 — integral_Ioi_of_hasDerivAt_of_tendsto' gives (0 − F a) where the 0 is the limit — the limit is exactly 0 here (my tendsto lemma concludes 𝓝 0) — so the form is `(0:ℝ) − F(13)`. My earlier RW₀ needed `-0` because the tendsto was .neg producing -0. Here the limit is stated 0 — the integral lemma's statement: integral_Ioi_of_hasDerivAt_of_tendsto' (hderiv)(hintegrable)(htendsto : Tendsto F atTop (𝓝 0)): ∫ = 0 − F a. So the rw [h] gives (0:ℝ) − F(13) — then rw [h1] (the F(13) form) then show 0 − −(...) = ... — use show (0:ℝ) - -(X) = X; ring. Let me write that.\n\nLA₀ (1/(x+10)²): \n```\nlemma antitoneOn_one_div_add_sq : AntitoneOn (fun x : ℝ => 1 / (x + 10) ^ 2) (Set.Ici (13 : ℝ)) := by\n intro a ha b hb hab\n rw [Set.mem_Ici] at ha hb\n have ha0 : (0 : ℝ) < a + 10 := by linarith\n exact one_div_le_one_div_of_le (pow_pos ha0 2)\n (pow_le_pow_left₀ ha0.le (by linarith : a + 10 ≤ b + 10) 2)\n\nlemma hasDerivAt_neg_inv_add (x : ℝ) (hx10 : x + 10 ≠ 0) :\n HasDerivAt (fun y : ℝ => -(y + 10)⁻¹) (1 / (x + 10) ^ 2) x := by\n have h2 := ((hasDerivAt_id' x).const_add 10).inv hx10\n have h3 := h2.neg\n rw [show (-(fun y : ℝ => y + 10)⁻¹) = (fun y : ℝ => -(y + 10)⁻¹) from by\n ext y; simp only [Pi.neg_apply, Pi.inv_apply]] at h3\n rwa [show (-(-1 / (x + 10) ^ 2)) = 1 / (x + 10) ^ 2 from by ring] at h3\n```\nWait — the inv derivative here: ((hasDerivAt_id' x).const_add 10).inv hx10 : HasDerivAt (fun y => (y+10)⁻¹) (-1/(x+10)^2)?? — the deriv form from HasDerivAt.inv: -(1/(g x)^2)·g' = -1/(x+10)²·1 — the display form might be -(1/(x+10)^2 * 1) or (-1/(x+10)^2)·... normalize: the .neg gives -(-1/(x+10)²·1)-ish: my show-rw assumes the form -(-1/(x+10)^2) — might need -(-(1/(x+10)^2 * 1)): hedge with a ring-normalizing rw: rwa [show (-(-1 / (x + 10) ^ 2 * 1)) = 1 / (x + 10) ^ 2 from by ring] — safer: convert h3 using 1 then ring_nf? NO convert on HasDerivAt (banked). Alternative: after the function rw, use `simpa [mul_one, neg_neg] using h3` for the derivative normalization:\n```\n rw [show (-(fun y : ℝ => y + 10)⁻¹) = (fun y : ℝ => -(y + 10)⁻¹) from by\n ext y; simp only [Pi.neg_apply, Pi.inv_apply]] at h3\n simpa [mul_one, neg_neg, one_div] using h3\n```\n- integrableOn_one_div_add_sq + integral = 1/23 + LA₀ brick (same pattern as RW₀).\n\nLA₁'s summable for LA₂:\n```\nlemma tail14_log_div_add_sq_summable :\n Summable (fun j : ℕ => Real.log ((j : ℝ) + 14) / (((j : ℝ) + 14) + 10) ^ 2) := by\n have h := antitoneOn_log_div_add_sq.summable_of_integrableOn_Ioi\n integrableOn_log_div_add_sq (fun t ht => by\n have ht13 : (13 : ℝ) < t := ht\n have hlog : (0 : ℝ) ≤ Real.log t := Real.log_nonneg (by linarith)\n positivity)\n have h2 := (summable_nat_add_iff (f := fun n : ℕ =>\n Real.log (n : ℝ) / ((n : ℝ) + 10) ^ 2) 14).mpr h\n refine h2.congr fun n => ?_\n push_cast\n ring_nf\n```\nWait — h from summable_of_integrableOn_Ioi gives Summable (fun n => f ↑n) with f = (fun x => log x/(x+10)^2): f ↑n = log ↑n/(↑n+10)^2 — the summable_nat_add_iff shift: (fun n => log ↑n/(↑n+10)^2) at (n+14): log ↑(n+14)/(↑(n+14)+10)^2 — congr to log((n:ℝ)+14)/(((n:ℝ)+14)+10)^2 via push_cast/ring_nf ✓.\n\nLA₁ brick:\n```\nlemma tail14_log_div_add_sq_le :\n (∑' j : ℕ, Real.log ((j : ℝ) + 14) / (((j : ℝ) + 14) + 10) ^ 2) ≤ 0.1687 := by\n have hle := antitoneOn_log_div_add_sq.tsum_comp_add_le_integral 13\n integrableOn_log_div_add_sq (fun t ht => by\n have ht13 : (13 : ℝ) < t := ht\n have hlog : (0 : ℝ) ≤ Real.log t := Real.log_nonneg (by linarith)\n positivity)\n have hInt13 : (∫ x in Set.Ioi ((13 : ℕ) : ℝ), Real.log x / (x + 10) ^ 2)\n = Real.log 13 / 23 + Real.log (23 / 13) / 10 := by\n rw [show ((13 : ℕ) : ℝ) = (13 : ℝ) by norm_num]\n exact integral_log_div_add_sq_Ioi_thirteen\n rw [hInt13] at hle\n have hcongr : (∑' n : ℕ, Real.log (↑(n + 13 + 1) : ℕ) / ((↑(n + 13 + 1) : ℕ) + 10) ^ 2)\n = ∑' n : ℕ, Real.log ((n : ℝ) + 14) / (((n : ℝ) + 14) + 10) ^ 2 := by\n refine tsum_congr fun n => ?_\n have h1 : ((↑(n + 13 + 1) : ℕ) : ℝ) = (n : ℝ) + 14 := by push_cast; ring\n rw [h1]\n rw [hcongr] at hle\n have h1 := log_thirteen_le\n have h2 := log_23_13_le\n linarith [hle, h1, h2]\n```\n2.565/23 + 0.571/10 = 0.111522+0.0571 = 0.168622 ≤ 0.1687 ✓ linarith ✓.\n\nLA₂:\n```\nlemma tail14_loglog_div_add_sq_le :\n (∑' j : ℕ, Real.log (Real.log ((j : ℝ) + 14)) / (((j : ℝ) + 14) + 10) ^ 2) ≤ 0.0621 := by\n <same skeleton as RW₂ with the 0.3679·0.1687 = 0.06206623 ≤ 0.0621 fold>\n```\nnonneg for LA₂'s of_norm_bounded: loglog(j+14) ≥ loglog 14 ≥ 0 (log 14 ≥ 2.6388 ≥ 1 ✓).\n\nLet me write §11b now.","signature":""},{"type":"text","text":"Now §11b (the left-tail bricks). Writing the LA set."},{"type":"tool_use","id":"Edit_106","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiTightR.lean","old_string":" linarith [hle, h4, h3]\n\nend NguyenRH1\n\nend","new_string":" linarith [hle, h4, h3]\n\n/-! ## 12. Piece 3d: the left-tail weight bricks (Σ over j ≥ 14) -/\n\n/-- 1/(x+10)² is antitone on Ici 13. -/\nlemma antitoneOn_one_div_add_sq :\n AntitoneOn (fun x : ℝ => 1 / (x + 10) ^ 2) (Set.Ici (13 : ℝ)) := by\n intro a ha b hb hab\n rw [Set.mem_Ici] at ha hb\n have ha0 : (0 : ℝ) < a + 10 := by linarith\n exact one_div_le_one_div_of_le (pow_pos ha0 2)\n (pow_le_pow_left₀ ha0.le (by linarith : a + 10 ≤ b + 10) 2)\n\n/-- −(x+10)⁻¹ has derivative 1/(x+10)² (x + 10 ≠ 0). -/\nlemma hasDerivAt_neg_inv_add (x : ℝ) (hx10 : x + 10 ≠ 0) :\n HasDerivAt (fun y : ℝ => -(y + 10)⁻¹) (1 / (x + 10) ^ 2) x := by\n have h2 := ((hasDerivAt_id' x).const_add 10).inv hx10\n have h3 := h2.neg\n rw [show (-(fun y : ℝ => y + 10)⁻¹) = (fun y : ℝ => -(y + 10)⁻¹) from by\n ext y\n simp only [Pi.neg_apply, Pi.inv_apply]] at h3\n simpa [mul_one, neg_neg, one_div] using h3\n\n/-- 1/(x+10)² is integrable on Ioi 13. -/\nlemma integrableOn_one_div_add_sq :\n IntegrableOn (fun x : ℝ => 1 / (x + 10) ^ 2) (Set.Ioi (13 : ℝ)) volume := by\n apply integrableOn_Ioi_deriv_of_nonneg' (fun x hx =>\n hasDerivAt_neg_inv_add x (by\n have h := (Set.mem_Ici.mp hx); linarith))\n · intro x hx\n have hx13 : (13 : ℝ) < x := hx\n positivity\n · simpa using tendsto_inv_atTop_zero.neg\n\n/-- The integral of 1/(x+10)² over Ioi 13 is 1/23. -/\nlemma integral_one_div_add_sq_Ioi_thirteen :\n ∫ x in Set.Ioi (13 : ℝ), 1 / (x + 10) ^ 2 = 1 / 23 := by\n have h := integral_Ioi_of_hasDerivAt_of_tendsto'\n (fun x hx => hasDerivAt_neg_inv_add x (by\n have h := (Set.mem_Ici.mp hx); linarith))\n integrableOn_one_div_add_sq (by simpa using tendsto_inv_atTop_zero.neg)\n rw [h]\n show (-0 : ℝ) - -((13 + 10 : ℝ)⁻¹) = 1 / 23\n norm_num\n\n/-- **LA₀**: Σ_{j≥14} 1/(j+10)² ≤ 1/23. -/\nlemma tail14_inv_add_sq_le :\n (∑' j : ℕ, (1 : ℝ) / (((j : ℝ) + 14) + 10) ^ 2) ≤ 1 / 23 := by\n have hle := antitoneOn_one_div_add_sq.tsum_comp_add_le_integral 13\n integrableOn_one_div_add_sq (fun t ht => by\n have ht13 : (13 : ℝ) < t := ht\n positivity)\n have hInt13 : (∫ x in Set.Ioi ((13 : ℕ) : ℝ), 1 / (x + 10) ^ 2) = 1 / 23 := by\n rw [show ((13 : ℕ) : ℝ) = (13 : ℝ) by norm_num]\n exact integral_one_div_add_sq_Ioi_thirteen\n rw [hInt13] at hle\n have hcongr : (∑' n : ℕ, 1 / ((↑(n + 13 + 1) : ℕ) + 10) ^ 2)\n = ∑' n : ℕ, (1 : ℝ) / (((n : ℝ) + 14) + 10) ^ 2 := by\n refine tsum_congr fun n => ?_\n have h1 : ((↑(n + 13 + 1) : ℕ) : ℝ) = (n : ℝ) + 14 := by push_cast; ring\n rw [h1]\n rw [hcongr] at hle\n exact hle\n\n/-- log x/(x+10)² is antitone on Ici 13 (derivative\n((x+10)/x − 2 log x)/(x+10)³ ≤ 0 since (x+10)/x ≤ 2 ≤ 2 log x). -/\nlemma antitoneOn_log_div_add_sq :\n AntitoneOn (fun x : ℝ => Real.log x / (x + 10) ^ 2) (Set.Ici (13 : ℝ)) := by\n apply antitoneOn_of_deriv_nonpos (convex_Ici 13)\n · intro x hx\n have hx0 : x ≠ 0 := by have h := (Set.mem_Ici.mp hx); linarith\n have hx10 : (x + 10) ^ 2 ≠ 0 := by\n have h := (Set.mem_Ici.mp hx)\n positivity\n exact ((Real.differentiableAt_log hx0).div (by\n fun_prop : DifferentiableAt ℝ (fun y : ℝ => (y + 10) ^ 2) x) hx10)\n |>.continuousAt.continuousWithinAt\n · intro x hx\n have hx0 : x ≠ 0 := by\n have h : (13 : ℝ) < x := Set.mem_Ioi.mp (by rwa [interior_Ici] at hx)\n linarith\n have hx10 : (x + 10) ^ 2 ≠ 0 := by\n have h : (13 : ℝ) < x := Set.mem_Ioi.mp (by rwa [interior_Ici] at hx)\n positivity\n exact ((Real.differentiableAt_log hx0).div (by\n fun_prop : DifferentiableAt ℝ (fun y : ℝ => (y + 10) ^ 2) x) hx10)\n |>.differentiableWithinAt\n · intro x hx\n have hx13 : (13 : ℝ) < x := Set.mem_Ioi.mp (by rwa [interior_Ici] at hx)\n have hx0 : x ≠ 0 := by linarith\n have hx10 : (x + 10) ≠ 0 := by linarith\n have hderiv : deriv (fun y => Real.log y / (y + 10) ^ 2) x\n = ((x + 10) / x - 2 * Real.log x) / (x + 10) ^ 3 := by\n have h1 : HasDerivAt (fun y : ℝ => (y + 10) ^ 2) (2 * (x + 10)) x := by\n have h := (hasDerivAt_pow 2 (x + 10)).comp x ((hasDerivAt_id' x).const_add 10)\n rw [show ((2 : ℕ) : ℝ) * (x + 10) ^ (2 - 1) * 1 = 2 * (x + 10) from by\n rw [show (2 : ℕ) - 1 = 1 from rfl, pow_one]\n push_cast\n ring] at h\n exact h\n have h2 := (Real.hasDerivAt_log hx0).div h1 (by positivity : (x + 10) ^ 2 ≠ 0)\n rw [h2.deriv]\n field_simp [hx0, hx10]\n ring\n rw [hderiv]\n have hlog1 : (1 : ℝ) ≤ Real.log x := by\n have h1 : Real.exp 1 ≤ 13 := Real.exp_one_lt_d9.le.trans (by norm_num)\n have h2 : (1 : ℝ) ≤ Real.log 13 := by\n rw [Real.le_log_iff_exp_le (by norm_num : (0 : ℝ) < 13)]\n exact h1\n exact h2.trans (Real.log_le_log (by positivity : (0 : ℝ) < 13) hx13.le)\n have hbound : (x + 10) / x ≤ 2 := by\n rw [div_le_iff₀ (by linarith : (0 : ℝ) < x)]\n linarith\n have h3 : (x + 10) / x - 2 * Real.log x ≤ 0 := by linarith [hlog1, hbound]\n exact div_nonpos_of_nonpos_of_nonneg h3 (by positivity)\n\n/-- The antiderivative of log x/(x+10)²:\nF(x) = −log x/(x+10) + (1/10)·log(x/(x+10)). -/\nlemma hasDerivAt_log_div_add_sq_antideriv (x : ℝ) (hx0 : x ≠ 0) (hx10 : x + 10 ≠ 0) :\n HasDerivAt (fun y : ℝ => -Real.log y / (y + 10) + (1 / 10) * Real.log (y / (y + 10)))\n (Real.log x / (x + 10) ^ 2) x := by\n have hF1 : HasDerivAt (fun y : ℝ => -Real.log y / (y + 10))\n (-(1 / (x * (x + 10))) + Real.log x / (x + 10) ^ 2) x := by\n have h1 := ((Real.hasDerivAt_log hx0).div ((hasDerivAt_id' x).const_add 10) hx10).neg\n rw [show (-(Real.log / fun y => y + 10)) = (fun y : ℝ => -Real.log y / (y + 10)) from by\n ext y; simp only [Pi.neg_apply, Pi.div_apply]] at h1\n rw [show (-(x⁻¹ * (x + 10) - Real.log x * 1) / (x + 10) ^ 2)\n = -(1 / (x * (x + 10))) + Real.log x / (x + 10) ^ 2 from by\n field_simp [hx0, hx10]\n ring] at h1\n exact h1\n have hF2 : HasDerivAt (fun y : ℝ => (1 / 10) * Real.log (y / (y + 10)))\n (1 / (x * (x + 10))) x := by\n have hratio : HasDerivAt (fun y : ℝ => y / (y + 10)) (10 / (x + 10) ^ 2) x := by\n have h := (hasDerivAt_id' x).div ((hasDerivAt_id' x).const_add 10) hx10\n rw [show (1 * (x + 10) - x * 1) / (x + 10) ^ 2 = 10 / (x + 10) ^ 2 from by\n field_simp [hx10]\n ring] at h\n exact h\n have hxr : x / (x + 10) ≠ 0 := by\n rw [div_ne_zero_iff]\n exact ⟨hx0, hx10⟩\n have h2 := (Real.hasDerivAt_log hxr).comp x hratio\n have h3 := h2.const_mul (1 / 10 : ℝ)\n rw [show (1 / 10 : ℝ) * ((x / (x + 10))⁻¹ * (10 / (x + 10) ^ 2))\n = 1 / (x * (x + 10)) from by\n field_simp [hx0, hx10]\n ring] at h3\n exact h3\n have hF := hF1.add hF2\n rw [show (-(1 / (x * (x + 10))) + Real.log x / (x + 10) ^ 2) + 1 / (x * (x + 10))\n = Real.log x / (x + 10) ^ 2 from by ring] at hF\n rw [show (fun y : ℝ => -Real.log y / (y + 10))\n + (fun y : ℝ => (1 / 10) * Real.log (y / (y + 10)))\n = (fun y : ℝ => -Real.log y / (y + 10) + (1 / 10) * Real.log (y / (y + 10))) from by\n ext y; simp only [Pi.add_apply]] at hF\n exact hF\n\n/-- The antiderivative tends to 0 at infinity. -/\nlemma tendsto_log_div_add_sq_antideriv :\n Filter.Tendsto (fun y : ℝ => -Real.log y / (y + 10) + (1 / 10) * Real.log (y / (y + 10)))\n Filter.atTop (𝓝 0) := by\n have hratio : Filter.Tendsto (fun x : ℝ => x / (x + 10)) Filter.atTop (𝓝 1) := by\n have h21 : Filter.Tendsto (fun x : ℝ => (10 : ℝ) / x) Filter.atTop (𝓝 0) := by\n simpa [div_eq_mul_inv] using tendsto_inv_atTop_zero.const_mul 10\n have h22 : Filter.Tendsto (fun x : ℝ => (1 : ℝ) + (10 : ℝ) / x) Filter.atTop\n (𝓝 (1 + 0)) :=\n tendsto_const_nhds.add h21\n have h23 : (fun x : ℝ => x / (x + 10)) = (fun x : ℝ => 1 / (1 + 10 / x)) := by\n funext x\n by_cases hx : x = 0\n · rw [hx]\n norm_num\n · field_simp [hx]\n ring\n rw [h23]\n have h24 : Filter.Tendsto (fun x : ℝ => 1 / (1 + (10 : ℝ) / x)) Filter.atTop\n (𝓝 (1 / (1 + 0))) := by\n apply Filter.Tendsto.div tendsto_const_nhds h22\n norm_num\n simpa using h24\n have hT1 : Filter.Tendsto (fun x : ℝ => Real.log x / (x + 10)) Filter.atTop (𝓝 0) := by\n have h1 : Filter.Tendsto (fun x : ℝ => Real.log x / x) Filter.atTop (𝓝 0) := by\n have h := Real.tendsto_pow_log_div_mul_add_atTop 1 0 1 one_ne_zero\n simpa using h\n have h3 : (fun x : ℝ => Real.log x / (x + 10))\n = (fun x : ℝ => (Real.log x / x) * (x / (x + 10))) := by\n funext x\n by_cases hx : x = 0\n · rw [hx]\n norm_num\n · field_simp [hx]\n ring\n rw [h3]\n have h4 := h1.mul hratio\n simp only [zero_mul] at h4\n exact h4\n have hT2 : Filter.Tendsto (fun x : ℝ => (1 / 10) * Real.log (x / (x + 10))) Filter.atTop\n (𝓝 0) := by\n have h2 : ContinuousAt Real.log 1 := Real.continuousAt_log (by norm_num : (1 : ℝ) ≠ 0)\n have h3 := (h2.tendsto.comp hratio).const_mul (1 / 10 : ℝ)\n rw [Real.log_one] at h3\n simpa using h3\n have hT := hT1.neg.add hT2\n have heq : (fun y : ℝ => -Real.log y / (y + 10) + (1 / 10) * Real.log (y / (y + 10)))\n = (fun y : ℝ => -(Real.log y / (y + 10)) + (1 / 10) * Real.log (y / (y + 10))) := by\n ext y\n simp only [neg_div]\n rw [heq]\n simpa using hT\n\n/-- log x/(x+10)² is integrable on Ioi 13. -/\nlemma integrableOn_log_div_add_sq :\n IntegrableOn (fun x : ℝ => Real.log x / (x + 10) ^ 2) (Set.Ioi (13 : ℝ)) volume := by\n apply integrableOn_Ioi_deriv_of_nonneg' (fun x hx =>\n hasDerivAt_log_div_add_sq_antideriv x (by\n have h := (Set.mem_Ici.mp hx); linarith) (by\n have h := (Set.mem_Ici.mp hx); linarith))\n · intro x hx\n have hx13 : (13 : ℝ) < x := hx\n have hlog : (0 : ℝ) ≤ Real.log x := Real.log_nonneg (by linarith)\n positivity\n · exact tendsto_log_div_add_sq_antideriv\n\n/-- The integral of log x/(x+10)² over Ioi 13 is log 13/23 + log(23/13)/10. -/\nlemma integral_log_div_add_sq_Ioi_thirteen :\n ∫ x in Set.Ioi (13 : ℝ), Real.log x / (x + 10) ^ 2\n = Real.log 13 / 23 + Real.log (23 / 13) / 10 := by\n have h := integral_Ioi_of_hasDerivAt_of_tendsto'\n (fun x hx => hasDerivAt_log_div_add_sq_antideriv x (by\n have h := (Set.mem_Ici.mp hx); linarith) (by\n have h := (Set.mem_Ici.mp hx); linarith))\n integrableOn_log_div_add_sq tendsto_log_div_add_sq_antideriv\n rw [h]\n have h1 : -Real.log 13 / (13 + 10) + (1 / 10) * Real.log (13 / (13 + 10))\n = -(Real.log 13 / 23 + Real.log (23 / 13) / 10) := by\n have h2 : Real.log (13 / (13 + 10)) = -Real.log (23 / 13) := by\n rw [show (13 : ℝ) / (13 + 10) = (23 / 13)⁻¹ from by norm_num, Real.log_inv]\n rw [h2]\n ring\n rw [h1]\n show (0 : ℝ) - -(Real.log 13 / 23 + Real.log (23 / 13) / 10)\n = Real.log 13 / 23 + Real.log (23 / 13) / 10\n ring\n\n/-- The shifted log-family is summable. -/\nlemma tail14_log_div_add_sq_summable :\n Summable (fun j : ℕ => Real.log ((j : ℝ) + 14) / (((j : ℝ) + 14) + 10) ^ 2) := by\n have h := antitoneOn_log_div_add_sq.summable_of_integrableOn_Ioi\n integrableOn_log_div_add_sq (fun t ht => by\n have ht13 : (13 : ℝ) < t := ht\n have hlog : (0 : ℝ) ≤ Real.log t := Real.log_nonneg (by linarith)\n positivity)\n have h2 := (summable_nat_add_iff (f := fun n : ℕ =>\n Real.log (n : ℝ) / ((n : ℝ) + 10) ^ 2) 14).mpr h\n refine h2.congr fun n => ?_\n push_cast\n ring_nf\n\n/-- **LA₁**: Σ_{j≥14} log j/(j+10)² ≤ 0.1687. -/\nlemma tail14_log_div_add_sq_le :\n (∑' j : ℕ, Real.log ((j : ℝ) + 14) / (((j : ℝ) + 14) + 10) ^ 2) ≤ 0.1687 := by\n have hle := antitoneOn_log_div_add_sq.tsum_comp_add_le_integral 13\n integrableOn_log_div_add_sq (fun t ht => by\n have ht13 : (13 : ℝ) < t := ht\n have hlog : (0 : ℝ) ≤ Real.log t := Real.log_nonneg (by linarith)\n positivity)\n have hInt13 : (∫ x in Set.Ioi ((13 : ℕ) : ℝ), Real.log x / (x + 10) ^ 2)\n = Real.log 13 / 23 + Real.log (23 / 13) / 10 := by\n rw [show ((13 : ℕ) : ℝ) = (13 : ℝ) by norm_num]\n exact integral_log_div_add_sq_Ioi_thirteen\n rw [hInt13] at hle\n have hcongr : (∑' n : ℕ, Real.log (↑(n + 13 + 1) : ℕ) / ((↑(n + 13 + 1) : ℕ) + 10) ^ 2)\n = ∑' n : ℕ, Real.log ((n : ℝ) + 14) / (((n : ℝ) + 14) + 10) ^ 2 := by\n refine tsum_congr fun n => ?_\n have h1 : ((↑(n + 13 + 1) : ℕ) : ℝ) = (n : ℝ) + 14 := by push_cast; ring\n rw [h1]\n rw [hcongr] at hle\n have h1 := log_thirteen_le\n have h2 := log_23_13_le\n linarith [hle, h1, h2]\n\n/-- **LA₂**: Σ_{j≥14} log log j/(j+10)² ≤ 0.0621 (via log log j ≤ (1/e)·log j). -/\nlemma tail14_loglog_div_add_sq_le :\n (∑' j : ℕ, Real.log (Real.log ((j : ℝ) + 14)) / (((j : ℝ) + 14) + 10) ^ 2) ≤ 0.0621 := by\n have hpt : ∀ j : ℕ, Real.log (Real.log ((j : ℝ) + 14)) / (((j : ℝ) + 14) + 10) ^ 2\n ≤ (1 / Real.exp 1) * (Real.log ((j : ℝ) + 14) / (((j : ℝ) + 14) + 10) ^ 2) := by\n intro j\n have hj1 : (1 : ℝ) < (j : ℝ) + 14 := by\n have h : (0 : ℝ) ≤ (j : ℝ) := Nat.cast_nonneg j\n linarith\n have h2 := log_log_le_div_exp hj1\n have h3 : (0 : ℝ) ≤ (((j : ℝ) + 14) + 10) ^ 2 := by positivity\n have h4 : Real.log (Real.log ((j : ℝ) + 14)) / (((j : ℝ) + 14) + 10) ^ 2\n ≤ ((1 / Real.exp 1) * Real.log ((j : ℝ) + 14)) / (((j : ℝ) + 14) + 10) ^ 2 :=\n div_le_div_of_nonneg_right h2 h3\n rw [mul_div_assoc] at h4\n exact h4\n have hsumm2 : Summable (fun j : ℕ =>\n (1 / Real.exp 1) * (Real.log ((j : ℝ) + 14) / (((j : ℝ) + 14) + 10) ^ 2)) :=\n tail14_log_div_add_sq_summable.mul_left _\n have hsumm : Summable (fun j : ℕ =>\n Real.log (Real.log ((j : ℝ) + 14)) / (((j : ℝ) + 14) + 10) ^ 2) := by\n apply Summable.of_norm_bounded hsumm2\n intro j\n rw [Real.norm_eq_abs]\n rw [abs_of_nonneg (by\n have hj1 : (1 : ℝ) ≤ Real.log ((j : ℝ) + 14) := by\n have h1 := log_fourteen_ge\n have h2 : Real.log 14 ≤ Real.log ((j : ℝ) + 14) :=\n Real.log_le_log (by norm_num : (0 : ℝ) < 14) (by\n have h : (0 : ℝ) ≤ (j : ℝ) := Nat.cast_nonneg j\n linarith)\n linarith [h1, h2]\n have h3 : (0 : ℝ) ≤ Real.log (Real.log ((j : ℝ) + 14)) := Real.log_nonneg hj1\n positivity : (0 : ℝ) ≤\n Real.log (Real.log ((j : ℝ) + 14)) / (((j : ℝ) + 14) + 10) ^ 2)]\n exact hpt j\n have hle := Summable.tsum_le_tsum hpt hsumm hsumm2\n rw [tsum_mul_left] at hle\n have h1 := tail14_log_div_add_sq_le\n have h2 := one_div_exp_one_le\n have h4 : (1 / Real.exp 1) * (∑' j : ℕ,\n Real.log ((j : ℝ) + 14) / (((j : ℝ) + 14) + 10) ^ 2)\n ≤ (1 / Real.exp 1) * 0.1687 :=\n mul_le_mul_of_nonneg_left h1 (by positivity : (0 : ℝ) ≤ 1 / Real.exp 1)\n have h3 : (1 / Real.exp 1) * 0.1687 ≤ 0.0621 := by\n calc (1 / Real.exp 1) * 0.1687 ≤ 0.3679 * 0.1687 :=\n mul_le_mul_of_nonneg_right h2 (by norm_num)\n _ ≤ 0.0621 := by norm_num\n linarith [hle, h4, h3]\n\nend NguyenRH1\n\nend"},"extra_content":null}]