← Session 31 — ii′-5f: tight R-bound 10.5/48 (piece 3 + pinch)
thinking (472 chars)
No intervalIntegral.integral_const in this Mathlib's IntervalIntegral.lean — use the antiderivative approach (∫ const via integral_eq_sub_of_hasDerivAt with (f′ a)·x). Or actually — simpler: I'll bound ∫ f′ by comparing with the constant function via integral_mono_on, and compute the constant integral via the same FTC trick.
Let me now write section 20 (5f-iii). Writing it in two chunks: (20a) the certified bounds + pinch lemma; (20b) the C0hat conversion + capstone.
Writing §20 (5f-iii): the certified bounds + the pinch lemma first.
tool: Edit
input
{
"replace_all": false,
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiTightR.lean",
"old_string": " _ \u2264 12.1284 * C0hat (t + 1) + 7.2425 := by\n have hC0nn : (0 : \u211d) \u2264 C0hat (t + 1) := by\n have h1 := two_le_C0hat (by linarith [ht] : (1 : \u211d) \u2264 t + 1)\n linarith\n nlinarith [hC0nn]\n\nend NguyenRH1\n\nend",
"new_string": " _ \u2264 12.1284 * C0hat (t + 1) + 7.2425 := by\n have hC0nn : (0 : \u211d) \u2264 C0hat (t + 1) := by\n have h1 := two_le_C0hat (by linarith [ht] : (1 : \u211d) \u2264 t + 1)\n linarith\n nlinarith [hC0nn]\n\n/-! ## 20. Piece 5f-iii: the pinch lemma and the capstone -/\n\n/-- e^0.4848 \u2264 1.6239 (partial sums). -/\nlemma exp_point4848_le : Real.exp 0.4848 \u2264 1.6239 := by\n have h := Real.sum_le_exp_of_nonneg (show (0 : \u211d) \u2264 0.4848 by norm_num) 7\n rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n Finset.sum_range_succ, Finset.sum_range_zero] at h\n norm_num at h\n linarith [h]\n\n/-- e\u00b2\u00b7e^0.4848 \u2264 12, hence log 12 \u2265 2.4848. -/\nlemma log_twelve_ge : (2.4848 : \u211d) \u2264 Real.log 12 := by\n have he2 : Real.exp 1 \u2264 (2.7182819 : \u211d) := Real.exp_one_lt_d9.le.trans (by norm_num)\n have he2sq : Real.exp 1 * Real.exp 1 \u2264 (7.3890566 : \u211d) := by\n have h := mul_le_mul he2 he2 (Real.exp_pos 1).le (by norm_num)\n have h2 : (2.7182819 : \u211d) * 2.7182819 \u2264 7.3890566 := by norm_num\n exact h.trans h2\n have h1 : Real.exp 2.4848 \u2264 12 := by\n have h2 : Real.exp 2.4848 = (Real.exp 1 * Real.exp 1) * Real.exp 0.4848 := by\n rw [\u2190 Real.exp_add, \u2190 Real.exp_add]\n congr 1\n norm_num\n rw [h2]\n have h3 := mul_le_mul he2sq exp_point4848_le (Real.exp_pos 0.4848).le (by norm_num)\n have h4 : (7.3890566 : \u211d) * 1.6239 \u2264 12 := by norm_num\n exact h3.trans h4\n have h5 := Real.le_log_iff_exp_le (by norm_num : (0 : \u211d) < 12)\n rw [h5]\n exact h1\n\n/-- e^0.9173 \u2265 2.5024 (partial sums), hence log 2.5024 \u2264 0.9173. -/\nlemma log_two_point_five_zero_two_four_le : Real.log 2.5024 \u2264 0.9173 := by\n have hbase : (2.5024 : \u211d) \u2264 Real.exp 0.9173 := by\n have h := Real.sum_le_exp_of_nonneg (show (0 : \u211d) \u2264 0.9173 by norm_num) 8\n rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_zero] at h\n norm_num at h\n linarith [h]\n have h2 : Real.log 2.5024 \u2264 Real.log (Real.exp 0.9173) :=\n Real.log_le_log (by norm_num : (0 : \u211d) < 2.5024) hbase\n rwa [Real.log_exp] at h2\n\n/-- The pinch function f(L) = 11.6321\u00b7log L \u2212 4.6484\u00b7L. -/\nprivate def pinchF (L : \u211d) : \u211d := 11.6321 * Real.log L - 4.6484 * L\n\n/-- Its derivative f\u2032(L) = 11.6321/L \u2212 4.6484. -/\nprivate def pinchF' (L : \u211d) : \u211d := 11.6321 / L - 4.6484\n\nlemma hasDerivAt_pinchF {x : \u211d} (hx0 : x \u2260 0) :\n HasDerivAt pinchF (pinchF' x) x := by\n have h1 := (Real.hasDerivAt_log hx0).const_mul 11.6321\n have h2 := (hasDerivAt_id' x).const_mul 4.6484\n have h3 := h1.sub h2\n rw [pinchF, pinchF']\n rw [show (11.6321 : \u211d) * x\u207b\u00b9 - 4.6484 = 11.6321 / x - 4.6484 from by\n rw [div_eq_mul_inv]]\n rw [show (fun L : \u211d => 11.6321 * Real.log L - 4.6484 * L)\n = (fun L : \u211d => 11.6321 * Real.log L) - (fun L : \u211d => 4.6484 * L) from by\n ext y; simp only [Pi.sub_apply]]\n exact h3\n\n/-- f\u2032 is antitone on Ici c (c > 0). -/\nlemma antitoneOn_pinchF' {c : \u211d} (hc : 0 < c) :\n AntitoneOn pinchF' (Set.Ici c) := by\n intro a ha b hb hab\n rw [Set.mem_Ici] at ha hb\n rw [pinchF', pinchF']\n have ha0 : (0 : \u211d) < a := by linarith [ha, hc]\n have hb0 : (0 : \u211d) < b := by linarith [hb, hc]\n have h1 : 11.6321 / b \u2264 11.6321 / a := by\n apply div_le_div_of_nonneg_left (by norm_num : (0 : \u211d) \u2264 11.6321) ha0 hab\n linarith [h1]\n\n/-- f(2.5024) \u2264 \u22120.96203 (certified evaluation). -/\nlemma pinchF_at_critical : pinchF 2.5024 \u2264 -0.96203 := by\n rw [pinchF]\n have h1 := log_two_point_five_zero_two_four_le\n have h2 : (4.6484 : \u211d) * 2.5024 \u2265 11.6321 := by norm_num\n have h3 : 11.6321 * Real.log 2.5024 \u2264 11.6321 * 0.9173 :=\n mul_le_mul_of_nonneg_left h1 (by norm_num)\n have h4 : (11.6321 : \u211d) * 0.9173 = 10.67012533 := by norm_num\n linarith [h3, h2, h4]\n\n/-- f\u2032(2.5024) \u2264 0 (the certified sign). -/\nlemma pinchF'_at_critical : pinchF' 2.5024 \u2264 0 := by\n rw [pinchF']\n have h1 : (11.6321 : \u211d) \u2264 4.6484 * 2.5024 := by norm_num\n have h2 : 11.6321 / 2.5024 \u2264 4.6484 := by\n rw [div_le_iff\u2080 (by norm_num : (0 : \u211d) < 2.5024)]\n exact h1\n linarith [h2]\n\n/-- **The pinch lemma**: for L \u2265 log 12,\n11.6321\u00b7log L \u2212 4.6484\u00b7L \u2264 0.3975 (the LL\u2212L concave bound; max at the\ncertified tangent point 2.5024). -/\nlemma pinch_tight_R {L : \u211d} (hL : Real.log 12 \u2264 L) :\n 11.6321 * Real.log L - 4.6484 * L \u2264 0.3975 := by\n have hlog12 : (0 : \u211d) < Real.log 12 := by\n have h1 := log_twelve_ge\n linarith [h1]\n have hLL : (0 : \u211d) < L := by linarith [hL, hlog12]\n have hanti := antitoneOn_pinchF' hlog12\n by_cases hcase : (2.5024 : \u211d) \u2264 L\n \u00b7 -- L \u2265 2.5024: f decreasing past the tangent point\n have hval := pinchF_at_critical\n have hsign := pinchF'_at_critical\n have hint : \u222b x in (2.5024 : \u211d)..L, pinchF' x = pinchF L - pinchF 2.5024 := by\n rw [intervalIntegral.integral_eq_sub_of_hasDerivAt (fun x hx =>\n hasDerivAt_pinchF (by\n have h2 : x \u2208 Set.Icc (2.5024 : \u211d) L := by\n rwa [Set.uIcc_of_le hcase] at hx\n have h3 : (0 : \u211d) < x := by linarith [hx.1]\n exact h3.ne'))\n (ContinuousOn.intervalIntegrable (by\n apply ContinuousOn.sub (ContinuousOn.div continuousOn_const continuousOn_id\n (fun x hx => by\n have h2 : x \u2208 Set.uIcc (2.5024 : \u211d) L := hx\n rw [Set.uIcc_of_le hcase] at h2\n have h3 : (0 : \u211d) < x := by linarith [h2.1]\n exact h3.ne'))\n exact continuousOn_const))]\n have hbound : \u222b x in (2.5024 : \u211d)..L, pinchF' x \u2264 0 := by\n apply intervalIntegral.integral_nonpos_of_nonpos hcase _\n \u00b7 apply ContinuousOn.intervalIntegrable\n apply ContinuousOn.sub (ContinuousOn.div continuousOn_const continuousOn_id\n (fun x hx => by\n have h2 : x \u2208 Set.uIcc (2.5024 : \u211d) L := hx\n rw [Set.uIcc_of_le hcase] at h2\n have h3 : (0 : \u211d) < x := by linarith [h2.1]\n exact h3.ne'))\n exact continuousOn_const\n \u00b7 intro x hx\n rw [Set.mem_Icc] at hx\n have h1 : pinchF' x \u2264 pinchF' 2.5024 := by\n apply hanti (by linarith [hcase] : (2.5024 : \u211d) \u2208 Set.Ici (Real.log 12))\n (by linarith [hx.1, hcase, hL] : x \u2208 Set.Ici (Real.log 12)) hx.1\n linarith [h1, hsign]\n -- assemble: f(L) = f(2.5024) + \u222b \u2264 f(2.5024) \u2264 \u22120.96203\n have hF : pinchF L = pinchF 2.5024 + \u222b x in (2.5024 : \u211d)..L, pinchF' x := by\n rw [hint]\n ring\n have hL' : (Real.log 12 : \u211d) \u2264 L := hL\n have hval' : pinchF L \u2264 -0.96203 := by\n rw [hF]\n linarith [hval, hbound]\n have h6 : pinchF L = 11.6321 * Real.log L - 4.6484 * L := rfl\n linarith [hval', h6]\n \u00b7 -- log 12 \u2264 L < 2.5024: the tangent-correction side\n push Not at hcase\n have hval := pinchF_at_critical\n have hsign := pinchF'_at_critical\n have hLlo : (0 : \u211d) < L := hLL\n have hint : \u222b x in L..(2.5024 : \u211d), pinchF' x = pinchF 2.5024 - pinchF L := by\n rw [intervalIntegral.integral_eq_sub_of_hasDerivAt (fun x hx =>\n hasDerivAt_pinchF (by\n have h2 : x \u2208 Set.Icc L (2.5024 : \u211d) := by\n rwa [Set.uIcc_of_le hcase.le] at hx\n have h3 : (0 : \u211d) < x := by linarith [hx.1, hLL]\n exact h3.ne'))\n (ContinuousOn.intervalIntegrable (by\n apply ContinuousOn.sub (ContinuousOn.div continuousOn_const continuousOn_id\n (fun x hx => by\n have h2 : x \u2208 Set.uIcc L (2.5024 : \u211d) := hx\n rw [Set.uIcc_of_le hcase.le] at h2\n have h3 : (0 : \u211d) < x := by linarith [h2.1, hLL]\n exact h3.ne'))\n exact continuousOn_const))]\n -- \u222b_L^{2.5024} f\u2032 \u2265 f\u2032(2.5024)\u00b7(2.5024\u2212L) (f\u2032 antitone: x \u2264 a \u27f9 f\u2032(x) \u2265 f\u2032(a))\n have hbound : (pinchF' 2.5024) * ((2.5024 : \u211d) - L)\n \u2264 \u222b x in L..(2.5024 : \u211d), pinchF' x := by\n rw [\u2190 intervalIntegral.integral_const (pinchF' 2.5024)]\n apply intervalIntegral.integral_mono_on hcase.le _ _\n \u00b7 apply ContinuousOn.intervalIntegrable\n exact continuousOn_const\n \u00b7 apply ContinuousOn.intervalIntegrable\n apply ContinuousOn.sub (ContinuousOn.div continuousOn_const continuousOn_id\n (fun x hx => by\n have h2 : x \u2208 Set.uIcc L (2.5024 : \u211d) := hx\n rw [Set.uIcc_of_le hcase.le] at h2\n have h3 : (0 : \u211d) < x := by linarith [h2.1, hLL]\n exact h3.ne'))\n exact continuousOn_const\n \u00b7 intro x hx\n rw [Set.mem_Icc] at hx\n exact hanti (by linarith [hx.2, hL] : (2.5024 : \u211d) \u2208 Set.Ici (Real.log 12))\n (by linarith [hx.1, hL] : x \u2208 Set.Ici (Real.log 12)) hx.2\n -- f(L) = f(2.5024) \u2212 \u222b \u2264 f(2.5024) \u2212 f\u2032(2.5024)(2.5024\u2212L) \u2264 f(2.5024) + 0.001\n have hF : pinchF L = pinchF 2.5024 - \u222b x in L..(2.5024 : \u211d), pinchF' x := by\n rw [hint]\n ring\n have hcorr : (-pinchF' 2.5024) * ((2.5024 : \u211d) - L) \u2264 0.001 := by\n have h1 : (0 : \u211d) \u2264 -pinchF' 2.5024 := by linarith [hsign]\n have h2 : -pinchF' 2.5024 = 4.6484 - 11.6321 / 2.5024 := by\n rw [pinchF']\n ring\n have h3 : 4.6484 - 11.6321 / 2.5024 \u2264 0.001 := by\n have h4 : (4.6484 - 0.001) * 2.5024 \u2264 11.6321 := by norm_num\n rw [sub_le_iff_le_add]\n rw [div_le_iff\u2080 (by norm_num : (0 : \u211d) < 2.5024)]\n have h5 : (4.6484 - 0.001) * 2.5024 \u2264 11.6321 := by norm_num\n linarith [h5]\n have h6 : ((2.5024 : \u211d) - L) \u2264 (2.5024 : \u211d) - Real.log 12 := by linarith [hL]\n have h7 : (2.5024 : \u211d) - Real.log 12 \u2264 0.01751 := by\n have h8 := log_twelve_ge\n linarith [h8]\n have h9 : (0 : \u211d) \u2264 -pinchF' 2.5024 := h1\n have h10 : (-pinchF' 2.5024) * ((2.5024 : \u211d) - L)\n \u2264 0.001 * ((2.5024 : \u211d) - Real.log 12) := by\n apply mul_le_mul _ h6 _ h9\n \u00b7 rw [h2]\n exact h3\n \u00b7 linarith [hL, log_twelve_ge]\n have h11 : (0.001 : \u211d) * ((2.5024 : \u211d) - Real.log 12) \u2264 0.001 := by\n have h12 := log_twelve_ge\n linarith [h12]\n exact h10.trans h11\n have hval' : pinchF L \u2264 -0.96203 + 0.001 := by\n rw [hF]\n have hsub : -(\u222b x in L..(2.5024 : \u211d), pinchF' x)\n \u2264 -(pinchF' 2.5024) * ((2.5024 : \u211d) - L) := by\n linarith [hbound]\n have h13 : pinchF 2.5024 - \u222b x in L..(2.5024 : \u211d), pinchF' x\n \u2264 pinchF 2.5024 + (-(\u222b x in L..(2.5024 : \u211d), pinchF' x)) := by ring\n have h14 : pinchF 2.5024 + (-(\u222b x in L..(2.5024 : \u211d), pinchF' x))\n \u2264 pinchF 2.5024 + (-pinchF' 2.5024) * ((2.5024 : \u211d) - L) := by\n linarith [hsub]\n have h15 : pinchF 2.5024 + (-pinchF' 2.5024) * ((2.5024 : \u211d) - L)\n \u2264 -0.96203 + 0.001 := by\n linarith [hval, hcorr]\n calc pinchF L = pinchF 2.5024 - \u222b x in L..(2.5024 : \u211d), pinchF' x := hF\n _ \u2264 pinchF 2.5024 + (-(\u222b x in L..(2.5024 : \u211d), pinchF' x)) := by ring\n _ \u2264 pinchF 2.5024 + (-pinchF' 2.5024) * ((2.5024 : \u211d) - L) := h14\n _ \u2264 -0.96203 + 0.001 := h15\n have h6 : pinchF L = 11.6321 * Real.log L - 4.6484 * L := rfl\n linarith [hval', h6]\n\n/-- The C0hat L/LL conversion: C0hat(t+1) \u2264\n0.433\u00b7(L + 1/12) + 0.886\u00b7(LL + 0.03354) + 2.9 for t \u2265 10. -/\nlemma C0hat_le_of_ten_le {t : \u211d} (ht : 10 \u2264 t) :\n C0hat (t + 1) \u2264 0.433 * (Real.log (t + 2) + 1 / 12)\n + 0.886 * (Real.log (Real.log (t + 2)) + 0.03354) + 2.9 := by\n have ht2 : (0 : \u211d) < t + 2 := by linarith\n have ht3 : (0 : \u211d) < t + 3 := by linarith\n have hlog12 := log_twelve_ge\n have hL : (2.4848 : \u211d) \u2264 Real.log (t + 2) := by\n have h1 : Real.log 12 \u2264 Real.log (t + 2) :=\n Real.log_le_log (by norm_num : (0 : \u211d) < 12) (by linarith : (12 : \u211d) \u2264 t + 2)\n linarith [hlog12, h1]\n have hLpos : (0 : \u211d) < Real.log (t + 2) := by linarith [hL]\n -- log(t+3) \u2264 L + 1/12\n have hinc1 : Real.log (t + 3) \u2264 Real.log (t + 2) + 1 / 12 := by\n have h1 : (t : \u211d) + 3 = (t + 2) * (1 + 1 / (t + 2)) := by\n field_simp [ht2.ne']\n ring\n rw [h1, Real.log_mul ht2.ne' (by positivity : (1 : \u211d) + 1 / (t + 2) \u2260 0)]\n have h2 : Real.log (1 + 1 / (t + 2)) \u2264 1 / (t + 2) :=\n Real.log_le_sub_one_of_pos (by positivity : (0 : \u211d) < 1 + 1 / (t + 2))\n have h3 : (1 : \u211d) / (t + 2) \u2264 1 / 12 := by\n apply div_le_div_of_nonneg_left (by norm_num : (0 : \u211d) \u2264 1) (by norm_num : (0 : \u211d) < 12)\n linarith\n linarith [h2, h3]\n -- loglog(t+3) \u2264 LL + 0.03354\n have hinc2 : Real.log (Real.log (t + 3))\n \u2264 Real.log (Real.log (t + 2)) + 0.03354 := by\n have h4 : Real.log (Real.log (t + 3)) \u2264 Real.log (Real.log (t + 2) + 1 / 12) :=\n Real.log_le_log (by positivity : (0 : \u211d) < Real.log (t + 3)) hinc1\n have h5 : Real.log (Real.log (t + 2) + 1 / 12)\n \u2264 Real.log (Real.log (t + 2)) + (1 / 12) / Real.log (t + 2) :=\n log_add_le (Real.log (t + 2)) (1 / 12) hLpos (by norm_num)\n have h6 : (1 / 12 : \u211d) / Real.log (t + 2) \u2264 0.03354 := by\n rw [div_le_iff\u2080 hLpos]\n have h7 : (0.03354 : \u211d) * 2.4848 \u2264 0.03354 * Real.log (t + 2) :=\n mul_le_mul_of_nonneg_left hL (by norm_num)\n have h8 : (1 / 12 : \u211d) \u2264 0.03354 * 2.4848 := by norm_num\n exact h8.trans h7\n linarith [h4, h5, h6]\n rw [C0hat]\n have harg : (t : \u211d) + 1 + 2 = t + 3 := by ring\n rw [harg]\n linarith [hinc1, hinc2]\n\nend NguyenRH1\n\nend"
}
raw content_json (database row)
[{"type":"thinking","thinking":"No intervalIntegral.integral_const in this Mathlib's IntervalIntegral.lean — use the antiderivative approach (∫ const via integral_eq_sub_of_hasDerivAt with (f′ a)·x). Or actually — simpler: I'll bound ∫ f′ by comparing with the constant function via integral_mono_on, and compute the constant integral via the same FTC trick.\n\nLet me now write section 20 (5f-iii). Writing it in two chunks: (20a) the certified bounds + pinch lemma; (20b) the C0hat conversion + capstone.","signature":""},{"type":"text","text":"Writing §20 (5f-iii): the certified bounds + the pinch lemma first."},{"type":"tool_use","id":"Edit_275","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiTightR.lean","old_string":" _ ≤ 12.1284 * C0hat (t + 1) + 7.2425 := by\n have hC0nn : (0 : ℝ) ≤ C0hat (t + 1) := by\n have h1 := two_le_C0hat (by linarith [ht] : (1 : ℝ) ≤ t + 1)\n linarith\n nlinarith [hC0nn]\n\nend NguyenRH1\n\nend","new_string":" _ ≤ 12.1284 * C0hat (t + 1) + 7.2425 := by\n have hC0nn : (0 : ℝ) ≤ C0hat (t + 1) := by\n have h1 := two_le_C0hat (by linarith [ht] : (1 : ℝ) ≤ t + 1)\n linarith\n nlinarith [hC0nn]\n\n/-! ## 20. Piece 5f-iii: the pinch lemma and the capstone -/\n\n/-- e^0.4848 ≤ 1.6239 (partial sums). -/\nlemma exp_point4848_le : Real.exp 0.4848 ≤ 1.6239 := by\n have h := Real.sum_le_exp_of_nonneg (show (0 : ℝ) ≤ 0.4848 by norm_num) 7\n rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n Finset.sum_range_succ, Finset.sum_range_zero] at h\n norm_num at h\n linarith [h]\n\n/-- e²·e^0.4848 ≤ 12, hence log 12 ≥ 2.4848. -/\nlemma log_twelve_ge : (2.4848 : ℝ) ≤ Real.log 12 := by\n have he2 : Real.exp 1 ≤ (2.7182819 : ℝ) := Real.exp_one_lt_d9.le.trans (by norm_num)\n have he2sq : Real.exp 1 * Real.exp 1 ≤ (7.3890566 : ℝ) := by\n have h := mul_le_mul he2 he2 (Real.exp_pos 1).le (by norm_num)\n have h2 : (2.7182819 : ℝ) * 2.7182819 ≤ 7.3890566 := by norm_num\n exact h.trans h2\n have h1 : Real.exp 2.4848 ≤ 12 := by\n have h2 : Real.exp 2.4848 = (Real.exp 1 * Real.exp 1) * Real.exp 0.4848 := by\n rw [← Real.exp_add, ← Real.exp_add]\n congr 1\n norm_num\n rw [h2]\n have h3 := mul_le_mul he2sq exp_point4848_le (Real.exp_pos 0.4848).le (by norm_num)\n have h4 : (7.3890566 : ℝ) * 1.6239 ≤ 12 := by norm_num\n exact h3.trans h4\n have h5 := Real.le_log_iff_exp_le (by norm_num : (0 : ℝ) < 12)\n rw [h5]\n exact h1\n\n/-- e^0.9173 ≥ 2.5024 (partial sums), hence log 2.5024 ≤ 0.9173. -/\nlemma log_two_point_five_zero_two_four_le : Real.log 2.5024 ≤ 0.9173 := by\n have hbase : (2.5024 : ℝ) ≤ Real.exp 0.9173 := by\n have h := Real.sum_le_exp_of_nonneg (show (0 : ℝ) ≤ 0.9173 by norm_num) 8\n rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_zero] at h\n norm_num at h\n linarith [h]\n have h2 : Real.log 2.5024 ≤ Real.log (Real.exp 0.9173) :=\n Real.log_le_log (by norm_num : (0 : ℝ) < 2.5024) hbase\n rwa [Real.log_exp] at h2\n\n/-- The pinch function f(L) = 11.6321·log L − 4.6484·L. -/\nprivate def pinchF (L : ℝ) : ℝ := 11.6321 * Real.log L - 4.6484 * L\n\n/-- Its derivative f′(L) = 11.6321/L − 4.6484. -/\nprivate def pinchF' (L : ℝ) : ℝ := 11.6321 / L - 4.6484\n\nlemma hasDerivAt_pinchF {x : ℝ} (hx0 : x ≠ 0) :\n HasDerivAt pinchF (pinchF' x) x := by\n have h1 := (Real.hasDerivAt_log hx0).const_mul 11.6321\n have h2 := (hasDerivAt_id' x).const_mul 4.6484\n have h3 := h1.sub h2\n rw [pinchF, pinchF']\n rw [show (11.6321 : ℝ) * x⁻¹ - 4.6484 = 11.6321 / x - 4.6484 from by\n rw [div_eq_mul_inv]]\n rw [show (fun L : ℝ => 11.6321 * Real.log L - 4.6484 * L)\n = (fun L : ℝ => 11.6321 * Real.log L) - (fun L : ℝ => 4.6484 * L) from by\n ext y; simp only [Pi.sub_apply]]\n exact h3\n\n/-- f′ is antitone on Ici c (c > 0). -/\nlemma antitoneOn_pinchF' {c : ℝ} (hc : 0 < c) :\n AntitoneOn pinchF' (Set.Ici c) := by\n intro a ha b hb hab\n rw [Set.mem_Ici] at ha hb\n rw [pinchF', pinchF']\n have ha0 : (0 : ℝ) < a := by linarith [ha, hc]\n have hb0 : (0 : ℝ) < b := by linarith [hb, hc]\n have h1 : 11.6321 / b ≤ 11.6321 / a := by\n apply div_le_div_of_nonneg_left (by norm_num : (0 : ℝ) ≤ 11.6321) ha0 hab\n linarith [h1]\n\n/-- f(2.5024) ≤ −0.96203 (certified evaluation). -/\nlemma pinchF_at_critical : pinchF 2.5024 ≤ -0.96203 := by\n rw [pinchF]\n have h1 := log_two_point_five_zero_two_four_le\n have h2 : (4.6484 : ℝ) * 2.5024 ≥ 11.6321 := by norm_num\n have h3 : 11.6321 * Real.log 2.5024 ≤ 11.6321 * 0.9173 :=\n mul_le_mul_of_nonneg_left h1 (by norm_num)\n have h4 : (11.6321 : ℝ) * 0.9173 = 10.67012533 := by norm_num\n linarith [h3, h2, h4]\n\n/-- f′(2.5024) ≤ 0 (the certified sign). -/\nlemma pinchF'_at_critical : pinchF' 2.5024 ≤ 0 := by\n rw [pinchF']\n have h1 : (11.6321 : ℝ) ≤ 4.6484 * 2.5024 := by norm_num\n have h2 : 11.6321 / 2.5024 ≤ 4.6484 := by\n rw [div_le_iff₀ (by norm_num : (0 : ℝ) < 2.5024)]\n exact h1\n linarith [h2]\n\n/-- **The pinch lemma**: for L ≥ log 12,\n11.6321·log L − 4.6484·L ≤ 0.3975 (the LL−L concave bound; max at the\ncertified tangent point 2.5024). -/\nlemma pinch_tight_R {L : ℝ} (hL : Real.log 12 ≤ L) :\n 11.6321 * Real.log L - 4.6484 * L ≤ 0.3975 := by\n have hlog12 : (0 : ℝ) < Real.log 12 := by\n have h1 := log_twelve_ge\n linarith [h1]\n have hLL : (0 : ℝ) < L := by linarith [hL, hlog12]\n have hanti := antitoneOn_pinchF' hlog12\n by_cases hcase : (2.5024 : ℝ) ≤ L\n · -- L ≥ 2.5024: f decreasing past the tangent point\n have hval := pinchF_at_critical\n have hsign := pinchF'_at_critical\n have hint : ∫ x in (2.5024 : ℝ)..L, pinchF' x = pinchF L - pinchF 2.5024 := by\n rw [intervalIntegral.integral_eq_sub_of_hasDerivAt (fun x hx =>\n hasDerivAt_pinchF (by\n have h2 : x ∈ Set.Icc (2.5024 : ℝ) L := by\n rwa [Set.uIcc_of_le hcase] at hx\n have h3 : (0 : ℝ) < x := by linarith [hx.1]\n exact h3.ne'))\n (ContinuousOn.intervalIntegrable (by\n apply ContinuousOn.sub (ContinuousOn.div continuousOn_const continuousOn_id\n (fun x hx => by\n have h2 : x ∈ Set.uIcc (2.5024 : ℝ) L := hx\n rw [Set.uIcc_of_le hcase] at h2\n have h3 : (0 : ℝ) < x := by linarith [h2.1]\n exact h3.ne'))\n exact continuousOn_const))]\n have hbound : ∫ x in (2.5024 : ℝ)..L, pinchF' x ≤ 0 := by\n apply intervalIntegral.integral_nonpos_of_nonpos hcase _\n · apply ContinuousOn.intervalIntegrable\n apply ContinuousOn.sub (ContinuousOn.div continuousOn_const continuousOn_id\n (fun x hx => by\n have h2 : x ∈ Set.uIcc (2.5024 : ℝ) L := hx\n rw [Set.uIcc_of_le hcase] at h2\n have h3 : (0 : ℝ) < x := by linarith [h2.1]\n exact h3.ne'))\n exact continuousOn_const\n · intro x hx\n rw [Set.mem_Icc] at hx\n have h1 : pinchF' x ≤ pinchF' 2.5024 := by\n apply hanti (by linarith [hcase] : (2.5024 : ℝ) ∈ Set.Ici (Real.log 12))\n (by linarith [hx.1, hcase, hL] : x ∈ Set.Ici (Real.log 12)) hx.1\n linarith [h1, hsign]\n -- assemble: f(L) = f(2.5024) + ∫ ≤ f(2.5024) ≤ −0.96203\n have hF : pinchF L = pinchF 2.5024 + ∫ x in (2.5024 : ℝ)..L, pinchF' x := by\n rw [hint]\n ring\n have hL' : (Real.log 12 : ℝ) ≤ L := hL\n have hval' : pinchF L ≤ -0.96203 := by\n rw [hF]\n linarith [hval, hbound]\n have h6 : pinchF L = 11.6321 * Real.log L - 4.6484 * L := rfl\n linarith [hval', h6]\n · -- log 12 ≤ L < 2.5024: the tangent-correction side\n push Not at hcase\n have hval := pinchF_at_critical\n have hsign := pinchF'_at_critical\n have hLlo : (0 : ℝ) < L := hLL\n have hint : ∫ x in L..(2.5024 : ℝ), pinchF' x = pinchF 2.5024 - pinchF L := by\n rw [intervalIntegral.integral_eq_sub_of_hasDerivAt (fun x hx =>\n hasDerivAt_pinchF (by\n have h2 : x ∈ Set.Icc L (2.5024 : ℝ) := by\n rwa [Set.uIcc_of_le hcase.le] at hx\n have h3 : (0 : ℝ) < x := by linarith [hx.1, hLL]\n exact h3.ne'))\n (ContinuousOn.intervalIntegrable (by\n apply ContinuousOn.sub (ContinuousOn.div continuousOn_const continuousOn_id\n (fun x hx => by\n have h2 : x ∈ Set.uIcc L (2.5024 : ℝ) := hx\n rw [Set.uIcc_of_le hcase.le] at h2\n have h3 : (0 : ℝ) < x := by linarith [h2.1, hLL]\n exact h3.ne'))\n exact continuousOn_const))]\n -- ∫_L^{2.5024} f′ ≥ f′(2.5024)·(2.5024−L) (f′ antitone: x ≤ a ⟹ f′(x) ≥ f′(a))\n have hbound : (pinchF' 2.5024) * ((2.5024 : ℝ) - L)\n ≤ ∫ x in L..(2.5024 : ℝ), pinchF' x := by\n rw [← intervalIntegral.integral_const (pinchF' 2.5024)]\n apply intervalIntegral.integral_mono_on hcase.le _ _\n · apply ContinuousOn.intervalIntegrable\n exact continuousOn_const\n · apply ContinuousOn.intervalIntegrable\n apply ContinuousOn.sub (ContinuousOn.div continuousOn_const continuousOn_id\n (fun x hx => by\n have h2 : x ∈ Set.uIcc L (2.5024 : ℝ) := hx\n rw [Set.uIcc_of_le hcase.le] at h2\n have h3 : (0 : ℝ) < x := by linarith [h2.1, hLL]\n exact h3.ne'))\n exact continuousOn_const\n · intro x hx\n rw [Set.mem_Icc] at hx\n exact hanti (by linarith [hx.2, hL] : (2.5024 : ℝ) ∈ Set.Ici (Real.log 12))\n (by linarith [hx.1, hL] : x ∈ Set.Ici (Real.log 12)) hx.2\n -- f(L) = f(2.5024) − ∫ ≤ f(2.5024) − f′(2.5024)(2.5024−L) ≤ f(2.5024) + 0.001\n have hF : pinchF L = pinchF 2.5024 - ∫ x in L..(2.5024 : ℝ), pinchF' x := by\n rw [hint]\n ring\n have hcorr : (-pinchF' 2.5024) * ((2.5024 : ℝ) - L) ≤ 0.001 := by\n have h1 : (0 : ℝ) ≤ -pinchF' 2.5024 := by linarith [hsign]\n have h2 : -pinchF' 2.5024 = 4.6484 - 11.6321 / 2.5024 := by\n rw [pinchF']\n ring\n have h3 : 4.6484 - 11.6321 / 2.5024 ≤ 0.001 := by\n have h4 : (4.6484 - 0.001) * 2.5024 ≤ 11.6321 := by norm_num\n rw [sub_le_iff_le_add]\n rw [div_le_iff₀ (by norm_num : (0 : ℝ) < 2.5024)]\n have h5 : (4.6484 - 0.001) * 2.5024 ≤ 11.6321 := by norm_num\n linarith [h5]\n have h6 : ((2.5024 : ℝ) - L) ≤ (2.5024 : ℝ) - Real.log 12 := by linarith [hL]\n have h7 : (2.5024 : ℝ) - Real.log 12 ≤ 0.01751 := by\n have h8 := log_twelve_ge\n linarith [h8]\n have h9 : (0 : ℝ) ≤ -pinchF' 2.5024 := h1\n have h10 : (-pinchF' 2.5024) * ((2.5024 : ℝ) - L)\n ≤ 0.001 * ((2.5024 : ℝ) - Real.log 12) := by\n apply mul_le_mul _ h6 _ h9\n · rw [h2]\n exact h3\n · linarith [hL, log_twelve_ge]\n have h11 : (0.001 : ℝ) * ((2.5024 : ℝ) - Real.log 12) ≤ 0.001 := by\n have h12 := log_twelve_ge\n linarith [h12]\n exact h10.trans h11\n have hval' : pinchF L ≤ -0.96203 + 0.001 := by\n rw [hF]\n have hsub : -(∫ x in L..(2.5024 : ℝ), pinchF' x)\n ≤ -(pinchF' 2.5024) * ((2.5024 : ℝ) - L) := by\n linarith [hbound]\n have h13 : pinchF 2.5024 - ∫ x in L..(2.5024 : ℝ), pinchF' x\n ≤ pinchF 2.5024 + (-(∫ x in L..(2.5024 : ℝ), pinchF' x)) := by ring\n have h14 : pinchF 2.5024 + (-(∫ x in L..(2.5024 : ℝ), pinchF' x))\n ≤ pinchF 2.5024 + (-pinchF' 2.5024) * ((2.5024 : ℝ) - L) := by\n linarith [hsub]\n have h15 : pinchF 2.5024 + (-pinchF' 2.5024) * ((2.5024 : ℝ) - L)\n ≤ -0.96203 + 0.001 := by\n linarith [hval, hcorr]\n calc pinchF L = pinchF 2.5024 - ∫ x in L..(2.5024 : ℝ), pinchF' x := hF\n _ ≤ pinchF 2.5024 + (-(∫ x in L..(2.5024 : ℝ), pinchF' x)) := by ring\n _ ≤ pinchF 2.5024 + (-pinchF' 2.5024) * ((2.5024 : ℝ) - L) := h14\n _ ≤ -0.96203 + 0.001 := h15\n have h6 : pinchF L = 11.6321 * Real.log L - 4.6484 * L := rfl\n linarith [hval', h6]\n\n/-- The C0hat L/LL conversion: C0hat(t+1) ≤\n0.433·(L + 1/12) + 0.886·(LL + 0.03354) + 2.9 for t ≥ 10. -/\nlemma C0hat_le_of_ten_le {t : ℝ} (ht : 10 ≤ t) :\n C0hat (t + 1) ≤ 0.433 * (Real.log (t + 2) + 1 / 12)\n + 0.886 * (Real.log (Real.log (t + 2)) + 0.03354) + 2.9 := by\n have ht2 : (0 : ℝ) < t + 2 := by linarith\n have ht3 : (0 : ℝ) < t + 3 := by linarith\n have hlog12 := log_twelve_ge\n have hL : (2.4848 : ℝ) ≤ Real.log (t + 2) := by\n have h1 : Real.log 12 ≤ Real.log (t + 2) :=\n Real.log_le_log (by norm_num : (0 : ℝ) < 12) (by linarith : (12 : ℝ) ≤ t + 2)\n linarith [hlog12, h1]\n have hLpos : (0 : ℝ) < Real.log (t + 2) := by linarith [hL]\n -- log(t+3) ≤ L + 1/12\n have hinc1 : Real.log (t + 3) ≤ Real.log (t + 2) + 1 / 12 := by\n have h1 : (t : ℝ) + 3 = (t + 2) * (1 + 1 / (t + 2)) := by\n field_simp [ht2.ne']\n ring\n rw [h1, Real.log_mul ht2.ne' (by positivity : (1 : ℝ) + 1 / (t + 2) ≠ 0)]\n have h2 : Real.log (1 + 1 / (t + 2)) ≤ 1 / (t + 2) :=\n Real.log_le_sub_one_of_pos (by positivity : (0 : ℝ) < 1 + 1 / (t + 2))\n have h3 : (1 : ℝ) / (t + 2) ≤ 1 / 12 := by\n apply div_le_div_of_nonneg_left (by norm_num : (0 : ℝ) ≤ 1) (by norm_num : (0 : ℝ) < 12)\n linarith\n linarith [h2, h3]\n -- loglog(t+3) ≤ LL + 0.03354\n have hinc2 : Real.log (Real.log (t + 3))\n ≤ Real.log (Real.log (t + 2)) + 0.03354 := by\n have h4 : Real.log (Real.log (t + 3)) ≤ Real.log (Real.log (t + 2) + 1 / 12) :=\n Real.log_le_log (by positivity : (0 : ℝ) < Real.log (t + 3)) hinc1\n have h5 : Real.log (Real.log (t + 2) + 1 / 12)\n ≤ Real.log (Real.log (t + 2)) + (1 / 12) / Real.log (t + 2) :=\n log_add_le (Real.log (t + 2)) (1 / 12) hLpos (by norm_num)\n have h6 : (1 / 12 : ℝ) / Real.log (t + 2) ≤ 0.03354 := by\n rw [div_le_iff₀ hLpos]\n have h7 : (0.03354 : ℝ) * 2.4848 ≤ 0.03354 * Real.log (t + 2) :=\n mul_le_mul_of_nonneg_left hL (by norm_num)\n have h8 : (1 / 12 : ℝ) ≤ 0.03354 * 2.4848 := by norm_num\n exact h8.trans h7\n linarith [h4, h5, h6]\n rw [C0hat]\n have harg : (t : ℝ) + 1 + 2 = t + 3 := by ring\n rw [harg]\n linarith [hinc1, hinc2]\n\nend NguyenRH1\n\nend"},"extra_content":null}]