[{"type":"thinking","thinking":"Signatures:\n- `AntitoneOn.tsum_comp_add_le_integral (N : ℕ) (anti : AntitoneOn f (Ici (N:ℝ))) (integrable : IntegrableOn f (Ioi (N:ℝ))) (nonneg : ∀ t ∈ Ioi (N:ℝ), 0 ≤ f t) : ∑' n, f (n + N + 1 : ℕ) ≤ ∫ x in Ioi (N:ℝ), f x`.\n- `AntitoneOn.summable_of_integrableOn_Ioi {N : ℕ} (anti) (integrable) (nonneg : ∀ t ∈ Ioi (N:ℝ), 0 ≤ f t) : Summable (fun n => f n)` — f n with the NAT CAST (n : ℝ)... \"Summable (fun (n : ℕ) ↦ f n)\" — f applied to ↑n presumably.\n\nNote: `integrableOn_Ioi_deriv_of_nonneg'` — let me check its signature too (used in this file at integrableOn_log_div_sq). It was used as: `integrableOn_Ioi_deriv_of_nonneg' (fun x hx => hasDerivAt...) (nonneg) (tendsto)`. I'll mirror the existing working code.\n\nNow write §11. The pattern from tsum_log_div_sq_tail_le:\n```\nhave hle := antitoneOn_log_div_sq.tsum_comp_add_le_integral 3\n  integrableOn_log_div_sq (fun t ht => by\n    have ht3 : (3 : ℝ) < t := ht\n    have hlog : (0 : ℝ) ≤ Real.log t := Real.log_nonneg (by linarith)\n    positivity)\n```\nSo the nonneg arg: (fun t ht => ...) with ht : t ∈ Ioi N and ht3 : N < t := ht ✓.\n\nAlso for RW₁: the shift from Ici 3 to Ici 10: `antitoneOn_log_div_sq.mono (Set.Ici_subset_Ici.mpr (by norm_num : (3:ℝ) ≤ 10))`? AntitoneOn.mono : AntitoneOn f t → s ⊆ t → AntitoneOn f s. Ici 10 ⊆ Ici 3: `Set.Ici_subset_Ici.mpr (by norm_num : (3:ℝ) ≤ 10)` — Ici_subset_Ici : a ≤ b → Ici b ⊆ Ici a ✓.\nAnd integrable: `integrableOn_log_div_sq.mono (Set.Ioi_subset_Ioi (by norm_num : (3:ℝ) ≤ 10))`? IntegrableOn.mono_set : IntegrableOn f t → s ⊆ t → IntegrableOn f s: Ioi 10 ⊆ Ioi 3: Ioi_subset_Ioi (3 ≤ 10) ✓ — `Set.Ioi_subset_Ioi : a ≤ b → Ioi b ⊆ Ioi a`.\n\nFor the integral at 10: mirror integral_log_div_sq_Ioi_three:\n```\nlemma integral_log_div_sq_Ioi_ten :\n    ∫ x in Set.Ioi (10 : ℝ), Real.log x / x ^ 2 = (Real.log 10 + 1) / 10 := by\n  have h := integral_Ioi_of_hasDerivAt_of_tendsto'\n    (fun x hx => hasDerivAt_neg_log_add_one_div (by\n      have h := (Set.mem_Ici.mp hx); linarith))\n    integrableOn_log_div_sq_ten tendsto_neg_log_add_one_div\n  rw [h]\n  show (0 : ℝ) - -((Real.log 10 + 1) / 10) = (Real.log 10 + 1) / 10\n  ring\n```\nwith integrableOn_log_div_sq_ten := the mono'd one. Wait — the hderiv's hx: x ∈ Ici 10 (integral_Ioi_of_hasDerivAt_of_tendsto' wants HasDerivAt on Ici a) — the existing code used `Set.mem_Ici.mp hx` then linarith ✓ clone.\n\nLet me now write the whole §11 chunk. Also expose summables:\n- tail11_log_div_sq_summable := (antitoneOn_log_div_sq.mono ...).summable_of_integrableOn_Ioi integrableOn_log_div_sq_ten (nonneg on Ioi 10) : Summable (fun n => log ↑n/↑n²) — then shifted by 11 via summable_nat_add_iff (like summable_log_div_sq_tail did).\n  Actually for RW₂ I need Summable (fun k => log(k+11)/(k+11)²): mirror summable_log_div_sq_tail:\n  ```\n  lemma tail11_log_div_sq_summable : Summable (fun k : ℕ => Real.log ((k:ℝ)+11) / ((k:ℝ)+11)^2) := by\n    have h := (antitoneOn_log_div_sq.mono (Set.Ici_subset_Ici.mpr (by norm_num : (3:ℝ) ≤ 10))).summable_of_integrableOn_Ioi\n      integrableOn_log_div_sq_ten (fun t ht => by\n        have ht10 : (10:ℝ) < t := ht\n        have hlog : (0:ℝ) ≤ Real.log t := Real.log_nonneg (by linarith)\n        positivity)\n    -- h : Summable (fun n ↦ (fun x => log x / x²) ↑n); shift by 11\n    have h2 := (summable_nat_add_iff (f := fun n : ℕ => Real.log (n:ℝ) / (n:ℝ)^2) 11).mpr h\n    refine h2.congr fun n => ?_\n    push_cast\n    ring_nf\n  ```\n  mirroring summable_log_div_sq_tail ✓ (which used 4-shift and ring_nf).\n  \nSimilarly LA₁'s summable for LA₂: \n```\nlemma tail14_log_div_add_sq_summable : Summable (fun j : ℕ => Real.log ((j:ℝ)+14) / (((j:ℝ)+14)+10)^2)\n```\nvia antitoneOn_log_div_add_sq.summable_of_integrableOn_Ioi (integrable at 13) + 14-shift.\n\nFor RW₀'s tail: I need the tsum bound directly (no separate summable needed for tsum_le_tsum since tsum_comp_add_le_integral gives it). But tail11_inv_sq_le uses the tsum form 1/((k:ℝ)+11)^2 vs the machine's f ↑(n+10+1) with f = (fun x => 1/x^2): f ↑(...) = 1/(↑(n+10+1))^2 — the hcongr bridge ✓ as I sketched.\n\nNow, the antiderivative HasDerivAts for LA₀/LA₁ and RW₀ — write them carefully with simpa-normalization.\n\nLet me also double check integrableOn_Ioi_deriv_of_nonneg's signature from the existing use in this file (integrableOn_log_div_sq):\n```\napply integrableOn_Ioi_deriv_of_nonneg' (fun x hx =>\n  hasDerivAt_neg_log_add_one_div (by\n    have h := (Set.mem_Ici.mp hx); linarith))\n· intro x hx\n  have hx3 : (3 : ℝ) < x := hx\n  have hlog : (0 : ℝ) ≤ Real.log x := Real.log_nonneg (by linarith)\n  positivity\n· exact tendsto_neg_log_add_one_div\n```\nSo: integrableOn_Ioi_deriv_of_nonneg' (hderiv : ∀ x ∈ Ici a, HasDerivAt F f' x) (hnonneg : ∀ x ∈ Ioi a, 0 ≤ f' x) (htendsto : Tendsto F atTop (𝓝 0)) — the first arg's hx : x ∈ Ici a (Set.mem_Ici.mp). ✓\n\nFor LA₁'s F = −log x/(x+10) + (1/10)·log(x/(x+10)): build the HasDerivAt — the messy one. Plan:\n```\nhave hF1 : HasDerivAt (fun y : ℝ => -Real.log y / (y + 10))\n    (-(1 / (x * (x + 10))) + Real.log x / (x + 10) ^ 2) x := by\n  have hx0 : x ≠ 0 := by linarith [hx_Ici]\n  have hx10 : x + 10 ≠ 0 := by linarith\n  have h1 := ((Real.hasDerivAt_log hx0).div ((hasDerivAt_id' x).const_add 10) hx10).neg\n  -- h1 : HasDerivAt (-(log · / (·+10))) (-((x⁻¹·(x+10) − log x·1)/(x+10)²)) x\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```\nThe div-derivative raw form: HasDerivAt.div (hf : HasDerivAt f f' x) (hg : HasDerivAt g g' x) (hc : g x ≠ 0) : HasDerivAt (f/g) ((f'·g x − f x·g')/(g x)^2)?? hmm — in this Mathlib the form was seen earlier: from hasDerivAt_neg_log_add_one_div: ((Real.hasDerivAt_log hx0).add_const 1).div (hasDerivAt_id' x) hx0 — and the file normalized via a show-rw: `rw [show Real.log x / x ^ 2 = -((x⁻¹ * x - (Real.log x + 1) * 1) / x ^ 2) from by ...]` — so the raw form is (f' * g − f * g') / g^2?? The file's raw was `(x⁻¹ * x - (Real.log x + 1) * 1) / x ^ 2` — i.e. (f'·g(x) − f(x)·g')/g(x)² with f' = x⁻¹, g(x) = x, g' = 1 ✓. So for F1: raw = (x⁻¹·(x+10) − log x·1)/(x+10)², negated. Then the show-rw: −(x⁻¹(x+10) − log x)/(x+10)² = −(1/(x(x+10))) + log x/(x+10)²: check: x⁻¹(x+10)/(x+10)² = (x+10)/(x(x+10)²) = 1/(x(x+10)) ✓. field_simp + ring should handle.\n\nF2:\n```\nhave hF2 : HasDerivAt (fun y : ℝ => (1 / 10) * Real.log (y / (y + 10)))\n    (1 / (x * (x + 10))) x := by\n  have hx0 : x ≠ 0 := ...\n  have hx10 : x + 10 ≠ 0 := ...\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    -- raw: (1·(x+10) − x·1)/(x+10)² = 10/(x+10)²\n    rw [show (1 * (x + 10) - x * 1) / (x + 10) ^ 2 = 10 / (x + 10) ^ 2 from by\n      field_simp [hx10]; ring] at h\n    exact h\n  have hxr : x / (x + 10) ≠ 0 := by positivity\n  have h2 := (Real.hasDerivAt_log hxr).comp x hratio\n  -- raw: (x/(x+10))⁻¹ * (10/(x+10)²)\n  have h3 := h2.const_mul (1 / 10 : ℝ)\n  rw [show (1 / 10 : ℝ) • ...] -- the const_mul derivative form: (1/10) • deriv\n  ...\n```\nconst_mul: HasDerivAt.const_mul (c) : HasDerivAt (fun x => c * f x) (c • f')... or (c * f')? For ℝ it's (c * f')? The smul form might appear: normalize via show-rw/simpa.\nThe value: (x/(x+10))⁻¹ · (10/(x+10)²) = ((x+10)/x)·(10/(x+10)²) = 10/(x(x+10)) — times 1/10 = 1/(x(x+10)) ✓.\n\nThen hF := hF1.add hF2 : derivative −1/(x(x+10)) + log x/(x+10)² + 1/(x(x+10)) = log x/(x+10)² — normalize via show-rw: the sum form: (−(1/(x(x+10))) + log x/(x+10)²) + 1/(x(x+10)) = log x/(x+10)² by ring? The raw sum: (−A + B) + A with A = 1/(x(x+10)), B = log x/(x+10)²: = B ✓ ring (field atoms: ring handles with the divisions as atoms? A and B are different atoms — (−A+B)+A = B ✓ ring ✓).\n\nAnd the function form: (fun y => −log y/(y+10)) + (fun y => (1/10)·log(y/(y+10))) = fun y => −log y/(y+10) + (1/10)·log(y/(y+10)) — HasDerivAt.add gives the Pi.add form — show-bridge: 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 [Pi.add_apply]] at hF — or just state hF's target function as the sum-of-lambdas form from the start. Simplest: ascribe hF's type with the lambda form and use the Pi.add_apply show-rw.\n\nTendsto F → 0:\n```\nhave 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 h2 : 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 : Filter.Tendsto (fun x : ℝ => 1 / (1 + (10 : ℝ) / x)) Filter.atTop (𝓝 (1 / (1 + 0))) :=\n      h22.div tendsto_const_nhds (by norm_num : (1 : ℝ) + 0 ≠ 0)\n    have h24 : (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    rw [h24]\n    simpa using h23\n  have h3 : (fun x : ℝ => Real.log x / (x + 10)) = (fun x : ℝ => (Real.log x / x) * (x / (x + 10))) := by\n    funext x\n    by_cases hx : x = 0\n    · rw [hx]\n      simp\n    · field_simp [hx]\n      ring\n  rw [h3]\n  have h4 := h1.mul h2\n  rwa [mul_zero, mul_one] at h4\n```\nhmm — h1.mul h2 : Tendsto ((log x/x)·(x/(x+10))) (𝓝 (0·1)) = 𝓝 0 ✓ (0·1 = 0 via zero_mul — the value: 0·1 — `mul_zero`? 0·1: zero_mul. rwa [zero_mul] at h4). Careful with forms; use: have h4 := h1.mul h2; simp only [zero_mul] at h4; exact h4? Tendsto ... (𝓝 (0*1)): 0*1 = 0 by norm_num/simp. Then F1 = −(log x/(x+10)) → −0 = 0: hT1.neg; F2 = (1/10)·log(x/(x+10)) → (1/10)·log 1 = 0: \n```\nhave hT2 : Filter.Tendsto (fun x : ℝ => (1/10) * Real.log (x / (x + 10))) Filter.atTop (𝓝 0) := by\n  have h1 : Filter.Tendsto (fun x : ℝ => Real.log (x / (x + 10))) Filter.atTop (𝓝 (Real.log 1)) := by\n    have h2 : ContinuousAt Real.log 1 := Real.continuousAt_log (by norm_num : (1:ℝ) ≠ 0)\n    exact h2.tendsto.comp h2ratio  -- h2ratio : the x/(x+10) → 1 from above\n  have h3 := h1.const_mul (1 / 10 : ℝ)\n  rw [Real.log_one, mul_zero] at h3\n  exact h3\n```\nThen hT := hT1.neg.add hT2 : Tendsto (F1+F2) (𝓝 (−0+0)) → 0: simpa.\n\nHmm — hT1 is for −log x/(x+10): hT1.neg gives −(log x/(x+10)) → −0: the F function is fun y => −log y/(y+10) + (1/10)·log(y/(y+10)) — the sum: hT1.neg.add hT2 : Tendsto (fun y => (−(log y/(y+10))) + (1/10)·log(y/(y+10))) (𝓝 (−0 + 0)) — then show the function matches F's lambda via funext/simpa.\n\nThis is getting long but mechanical. Similarly the LA₁ integrableOn via integrableOn_Ioi_deriv_of_nonneg' with this F, nonneg: log x/(x+10)² ≥ 0 for x > 13 ✓, tendsto → 0 ✓.\n\nLet me write the whole §11 now — it's ~600 lines of mechanical code. I'll write it in two edits: (11a) RW bricks; (11b) LA bricks. Write 11a first.","signature":""},{"type":"text","text":"Signatures confirmed. Writing §11 (the six tail bricks) — part 11a (the k ≥ 11 right-tail bricks) first."},{"type":"tool_use","id":"Edit_96","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiTightR.lean","old_string":"end NguyenRH1\n\nend","new_string":"/-! ## 11. Piece 3c: the right-tail weight bricks (Σ over k ≥ 11) -/\n\n/-- 1/x² is antitone on Ici 10. -/\nlemma antitoneOn_one_div_sq : AntitoneOn (fun x : ℝ => 1 / x ^ 2) (Set.Ici (10 : ℝ)) := by\n  intro a ha b hb hab\n  rw [Set.mem_Ici] at ha hb\n  have ha0 : (0 : ℝ) < a := by linarith\n  exact one_div_le_one_div_of_le (pow_pos ha0 2)\n    (pow_le_pow_left₀ ha0.le hab 2)\n\n/-- −x⁻¹ has derivative 1/x² (x ≠ 0). -/\nlemma hasDerivAt_neg_inv (x : ℝ) (hx0 : x ≠ 0) :\n    HasDerivAt (fun y : ℝ => -y⁻¹) (1 / x ^ 2) x := by\n  have h2 := (hasDerivAt_id' x).inv hx0\n  have h3 := h2.neg\n  simpa [one_div, inv_pow, mul_neg, neg_neg, Pi.neg_apply, Function.comp_def] using h3\n\n/-- 1/x² is integrable on Ioi 10. -/\nlemma integrableOn_one_div_sq :\n    IntegrableOn (fun x : ℝ => 1 / x ^ 2) (Set.Ioi (10 : ℝ)) volume := by\n  apply integrableOn_Ioi_deriv_of_nonneg' (fun x hx =>\n    hasDerivAt_neg_inv x (by\n      have h := (Set.mem_Ici.mp hx); linarith))\n  · intro x hx\n    have hx10 : (10 : ℝ) < x := hx\n    positivity\n  · simpa using tendsto_inv_atTop_zero.neg\n\n/-- The integral of 1/x² over Ioi 10 is 1/10. -/\nlemma integral_one_div_sq_Ioi_ten :\n    ∫ x in Set.Ioi (10 : ℝ), 1 / x ^ 2 = 1 / 10 := by\n  have h := integral_Ioi_of_hasDerivAt_of_tendsto'\n    (fun x hx => hasDerivAt_neg_inv x (by\n      have h := (Set.mem_Ici.mp hx); linarith))\n    integrableOn_one_div_sq (by simpa using tendsto_inv_atTop_zero.neg)\n  rw [h]\n  show (0 : ℝ) - -((10 : ℝ)⁻¹) = 1 / 10\n  norm_num\n\n/-- **RW₀**: Σ_{k≥11} 1/k² ≤ 0.1. -/\nlemma tail11_inv_sq_le : (∑' k : ℕ, (1 : ℝ) / ((k : ℝ) + 11) ^ 2) ≤ 0.1 := by\n  have hle := antitoneOn_one_div_sq.tsum_comp_add_le_integral 10\n    integrableOn_one_div_sq (fun t ht => by\n      have ht10 : (10 : ℝ) < t := ht\n      positivity)\n  rw [integral_one_div_sq_Ioi_ten] at hle\n  have hcongr : (∑' n : ℕ, 1 / ((↑(n + 10 + 1) : ℕ) : ℝ) ^ 2)\n      = ∑' n : ℕ, (1 : ℝ) / ((n : ℝ) + 11) ^ 2 := by\n    refine tsum_congr fun n => ?_\n    have h1 : ((↑(n + 10 + 1) : ℕ) : ℝ) = (n : ℝ) + 11 := by push_cast; ring\n    rw [h1]\n  rw [hcongr] at hle\n  have h2 : (1 : ℝ) / 10 = 0.1 := by norm_num\n  rw [h2] at hle\n  exact hle\n\n/-- log x/x² is integrable on Ioi 10 (restricting the Ioi 3 instance). -/\nlemma integrableOn_log_div_sq_ten :\n    IntegrableOn (fun x : ℝ => Real.log x / x ^ 2) (Set.Ioi (10 : ℝ)) volume :=\n  integrableOn_log_div_sq.mono_set (Set.Ioi_subset_Ioi (by norm_num : (3 : ℝ) ≤ 10))\n\n/-- log x/x² is antitone on Ici 10 (restricting the Ici 3 instance). -/\nlemma antitoneOn_log_div_sq_ten :\n    AntitoneOn (fun x : ℝ => Real.log x / x ^ 2) (Set.Ici (10 : ℝ)) :=\n  antitoneOn_log_div_sq.mono (Set.Ici_subset_Ici.mpr (by norm_num : (3 : ℝ) ≤ 10))\n\n/-- The integral of log x/x² over Ioi 10 is (log 10 + 1)/10. -/\nlemma integral_log_div_sq_Ioi_ten :\n    ∫ x in Set.Ioi (10 : ℝ), Real.log x / x ^ 2 = (Real.log 10 + 1) / 10 := by\n  have h := integral_Ioi_of_hasDerivAt_of_tendsto'\n    (fun x hx => hasDerivAt_neg_log_add_one_div (by\n      have h := (Set.mem_Ici.mp hx); linarith))\n    integrableOn_log_div_sq_ten tendsto_neg_log_add_one_div\n  rw [h]\n  show (0 : ℝ) - -((Real.log 10 + 1) / 10) = (Real.log 10 + 1) / 10\n  ring\n\n/-- The shifted log-family is summable. -/\nlemma tail11_log_div_sq_summable :\n    Summable (fun k : ℕ => Real.log ((k : ℝ) + 11) / ((k : ℝ) + 11) ^ 2) := by\n  have h := antitoneOn_log_div_sq_ten.summable_of_integrableOn_Ioi\n    integrableOn_log_div_sq_ten (fun t ht => by\n      have ht10 : (10 : ℝ) < 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 : ℝ) ^ 2) 11).mpr h\n  refine h2.congr fun n => ?_\n  push_cast\n  ring_nf\n\n/-- **RW₁**: Σ_{k≥11} log k/k² ≤ 0.3303. -/\nlemma tail11_log_div_sq_le :\n    (∑' k : ℕ, Real.log ((k : ℝ) + 11) / ((k : ℝ) + 11) ^ 2) ≤ 0.3303 := by\n  have hle := antitoneOn_log_div_sq_ten.tsum_comp_add_le_integral 10\n    integrableOn_log_div_sq_ten (fun t ht => by\n      have ht10 : (10 : ℝ) < t := ht\n      have hlog : (0 : ℝ) ≤ Real.log t := Real.log_nonneg (by linarith)\n      positivity)\n  rw [integral_log_div_sq_Ioi_ten] at hle\n  have hcongr : (∑' n : ℕ, Real.log (↑(n + 10 + 1) : ℕ) / ((↑(n + 10 + 1) : ℕ) : ℝ) ^ 2)\n      = ∑' n : ℕ, Real.log ((n : ℝ) + 11) / ((n : ℝ) + 11) ^ 2 := by\n    refine tsum_congr fun n => ?_\n    have h1 : ((↑(n + 10 + 1) : ℕ) : ℝ) = (n : ℝ) + 11 := by push_cast; ring\n    rw [h1]\n  rw [hcongr] at hle\n  have h1 := log_ten_le\n  linarith [hle, h1]\n\n/-- **RW₂**: Σ_{k≥11} log log k/k² ≤ 0.1216 (via log log k ≤ (1/e)·log k). -/\nlemma tail11_loglog_div_sq_le :\n    (∑' k : ℕ, Real.log (Real.log ((k : ℝ) + 11)) / ((k : ℝ) + 11) ^ 2) ≤ 0.1216 := by\n  have hpt : ∀ k : ℕ, Real.log (Real.log ((k : ℝ) + 11)) / ((k : ℝ) + 11) ^ 2\n      ≤ (1 / Real.exp 1) * (Real.log ((k : ℝ) + 11) / ((k : ℝ) + 11) ^ 2) := by\n    intro k\n    have hk1 : (1 : ℝ) < (k : ℝ) + 11 := by\n      have h := Nat.cast_nonneg k\n      linarith\n    have h2 := log_log_le_div_exp hk1\n    have h3 : (0 : ℝ) ≤ ((k : ℝ) + 11) ^ 2 := by positivity\n    have h4 := div_le_div_of_nonneg_right h2 h3\n    rw [mul_div_assoc] at h4\n    exact h4\n  have hsumm2 : Summable (fun k : ℕ =>\n      (1 / Real.exp 1) * (Real.log ((k : ℝ) + 11) / ((k : ℝ) + 11) ^ 2)) :=\n    tail11_log_div_sq_summable.mul_left _\n  have hsumm : Summable (fun k : ℕ =>\n      Real.log (Real.log ((k : ℝ) + 11)) / ((k : ℝ) + 11) ^ 2) := by\n    apply Summable.of_norm_bounded hsumm2\n    intro k\n    rw [Real.norm_eq_abs]\n    rw [abs_of_nonneg (by\n      have hk1 : (1 : ℝ) ≤ Real.log ((k : ℝ) + 11) := by\n        have h1 := log_eleven_ge\n        have h2 : Real.log 11 ≤ Real.log ((k : ℝ) + 11) :=\n          Real.log_le_log (by norm_num : (0 : ℝ) < 11) (by\n            have h := Nat.cast_nonneg k\n            linarith)\n        linarith [h1, h2]\n      have h3 : (0 : ℝ) ≤ Real.log (Real.log ((k : ℝ) + 11)) := Real.log_nonneg hk1\n      positivity : (0 : ℝ) ≤ Real.log (Real.log ((k : ℝ) + 11)) / ((k : ℝ) + 11) ^ 2)]\n    exact hpt k\n  have hle := Summable.tsum_le_tsum hpt hsumm hsumm2\n  rw [tsum_mul_left] at hle\n  have h1 := tail11_log_div_sq_le\n  have h2 := one_div_exp_one_le\n  have h4 : (1 / Real.exp 1) * (∑' k : ℕ, Real.log ((k : ℝ) + 11) / ((k : ℝ) + 11) ^ 2)\n      ≤ (1 / Real.exp 1) * 0.3303 :=\n    mul_le_mul_of_nonneg_left h1 (by positivity : (0 : ℝ) ≤ 1 / Real.exp 1)\n  have h3 : (1 / Real.exp 1) * 0.3303 ≤ 0.1216 := by\n    calc (1 / Real.exp 1) * 0.3303 ≤ 0.3679 * 0.3303 :=\n        mul_le_mul_of_nonneg_right h2 (by norm_num)\n      _ ≤ 0.1216 := by norm_num\n  linarith [hle, h4, h3]\n\nend NguyenRH1\n\nend"},"extra_content":null}]