← Session 31 — ii′-5f: tight R-bound 10.5/48 (piece 3 + pinch)
thinking (5534 chars)
`div_le_iff₀ (hc : 0 < c) : b / c ≤ a ↔ b ≤ a * c` — for my use: 11.6321/2.5024 ≤ 4.6484 ⟺ 11.6321 ≤ 4.6484 * 2.5024 ✓ — the form b/c ≤ a with b = 11.6321, a = 4.6484: rw [div_le_iff₀ hc] gives `11.6321 ≤ 4.6484 * 2.5024` ✓ — my error at 3998 said the pattern `?m/2.5024 ≤ ?m` didn't match `11.6321 / 2.5024 ≤ 4.6484`... hmm — it SHOULD match. Unless the hc arg position: div_le_iff₀ (hc : 0 < c) — with c implicit from hc. My call `rw [div_le_iff₀ (by norm_num : (0:ℝ) < 2.5024)]` ✓ should work. The error might be the ascription binding issue again (`by norm_num : (0:ℝ) < 2.5024` parsing weirdly with the `:`). Let me use show-forms throughout.
Now the bigger issue list. Let me write the fixes:
1. Replace exp_point4848_le + log_twelve_ge with the log(4/3) route:
```
/-- The 4-term alternating bound: −log(1−y) ≤ y + y²/2 + y³/3 + y⁴/(4(1−y)). -/
lemma neg_log_one_sub_le_four {y : ℝ} (hy0 : 0 ≤ y) (hy1 : y < 1) :
-Real.log (1 - y) ≤ y + y ^ 2 / 2 + y ^ 3 / 3 + y ^ 4 / (4 * (1 - y)) := by
-- same integral machine as neg_log_one_sub_le with the t³ term
...
```
The machine: 1/(1−t) ≤ 1+t+t²+t³/(1−y) on [0,y]: (1−t)(1+t+t²+t³/(1−y)) = 1−t³ + t³(1−t)/(1−y) ≥ 1 ⟺ t³(1−t)/(1−y) ≥ t³ ⟺ (1−t)/(1−y) ≥ 1 ⟺ t ≤ y ✓. The antiderivative: y+y²/2+y³/3+y⁴/(4(1−y)) — HasDerivAt of the poly ✓ (same hG pattern).
```
/-- log(4/3) ≤ 0.28777 (the 4-term bound at y = 1/4). -/
lemma log_four_thirds_le : Real.log (4 / 3) ≤ 0.28777 := by
have h1 : Real.log (4 / 3) = -Real.log (3 / 4) := by
rw [show (4 : ℝ) / 3 = (3 / 4)⁻¹ from by norm_num, Real.log_inv]
rw [h1]
have h2 : (3 : ℝ) / 4 = 1 - 1 / 4 := by norm_num
rw [h2]
have h3 := neg_log_one_sub_le_four (y := 1 / 4) (by norm_num) (by norm_num)
-- 1/4 + (1/4)²/2 + (1/4)³/3 + (1/4)⁴/(4(1−1/4)) = 0.2877604 ≤ 0.28777
have h4 : (1 : ℝ) / 4 + (1 / 4) ^ 2 / 2 + (1 / 4) ^ 3 / 3 + (1 / 4) ^ 4 / (4 * (1 - 1 / 4))
≤ 0.28777 := by norm_num
linarith [h3, h4]
/-- log 12 ≥ 2.4848: log 12 = 4·log 2 − log(4/3). -/
lemma log_twelve_ge : (2.4848 : ℝ) ≤ Real.log 12 := by
have hlog2 : (0.6931471 : ℝ) ≤ Real.log 2 :=
(by norm_num : (0.6931471 : ℝ) ≤ 0.6931471803).trans Real.log_two_gt_d9.le
have h43 := log_four_thirds_le
have hdecomp : Real.log 12 = 4 * Real.log 2 - Real.log (4 / 3) := by
have h1 : (12 : ℝ) = 2 ^ 4 * (3 / 4) := by norm_num
rw [h1, Real.log_mul (by norm_num : ((2 : ℝ) ^ 4) ≠ 0) (by norm_num : (3 / 4 : ℝ) ≠ 0)]
have h2 : Real.log ((2 : ℝ) ^ 4) = 4 * Real.log 2 := by
rw [Real.log_pow]
push_cast
ring
rw [h2]
have h3 : Real.log (3 / 4) = -Real.log (4 / 3) := by
rw [show (3 : ℝ) / 4 = (4 / 3)⁻¹ from by norm_num, Real.log_inv]
rw [h3]
ring
linarith [hdecomp, hlog2, h43]
```
Check: 4·0.6931471 − 0.28777 = 2.7725884−0.28777 = 2.4848184 ≥ 2.4848 ✓ (margin 1.84e-5 — wait — but the TRUE log(4/3) = 0.287682 and my bound is ≤ 0.28777 — the 4-term gives 0.2877604 ≤ 0.28777 ✓ — so log 12 ≥ 2.7725884−0.28777 = 2.4848184 ✓ margin 1.84e-5 — TIGHT but exact. Hmm — actually, with the sharper 4-term value 0.2877604: 2.7725884−0.2877604 = 2.484828 ✓ margin 2.8e-5.)
2. log_twelve_le : Real.log 12 ≤ 2.5024: log 12 = 2 log 2 + log 3 ≤ 2·0.69315+1.0987 = 2.485 ≤ 2.5024: log 3 ≤ 1.0987 via 3 ≤ e^1.0987 (partial sums e^1.0987 = e·e^0.0987 ≥ 2.7182818·1.103735 ≥ 3 ✓).
```
lemma log_three_le : Real.log 3 ≤ 1.0987 := by
have h1 : (3 : ℝ) ≤ Real.exp 1.0987 := by
have h2 : Real.exp 1.0987 = Real.exp 1 * Real.exp 0.0987 := by
rw [← Real.exp_add]
congr 1
norm_num
rw [h2]
have h3 : (1.10374 : ℝ) ≤ Real.exp 0.0987 := by
have h := Real.sum_le_exp_of_nonneg (show (0 : ℝ) ≤ 0.0987 by norm_num) 6
rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,
Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,
Finset.sum_range_zero] at h
norm_num at h
linarith [h]
have h4 : (2.7182818 : ℝ) ≤ Real.exp 1 :=
(by norm_num : (2.7182818 : ℝ) ≤ 2.7182818283).trans Real.exp_one_gt_d9.le
have h5 : (3 : ℝ) ≤ 2.7182818 * 1.10374 := by norm_num
have h6 := mul_le_mul h4 h3 (by positivity : (0 : ℝ) ≤ 1.10374) (Real.exp_pos 1).le
exact h5.trans h6
have h2 := Real.log_le_log (by norm_num : (0 : ℝ) < 3) h1
rwa [Real.log_exp] at h2
lemma log_twelve_le : Real.log 12 ≤ 2.5024 := by
have hlog2 : Real.log 2 ≤ 0.69315 := Real.log_two_lt_d9.le.trans (by norm_num)
have h3 := log_three_le
have hdecomp : Real.log 12 = 2 * Real.log 2 + Real.log 3 := by
have h1 : (12 : ℝ) = 4 * 3 := by norm_num
rw [h1, Real.log_mul (by norm_num : (4 : ℝ) ≠ 0) (by norm_num : (3 : ℝ) ≠ 0)]
have h2 : Real.log 4 = 2 * Real.log 2 := by
have h3' : (4 : ℝ) = 2 ^ 2 := by norm_num
rw [h3', Real.log_pow]
push_cast
ring
rw [h2]
linarith [hdecomp, hlog2, h3]
```
2·0.69315+1.0987 = 1.3863+1.0987 = 2.4850 ≤ 2.5024 ✓.
3. h5 ascription in log_twelve_ge — gone (new route).
4. pinchF unfolds: use `rw [show pinchF 2.5024 = 11.6321 * Real.log 2.5024 - 4.6484 * 2.5024 from rfl]` in pinchF_at_critical, and similarly pinchF'. And in hasDerivAt_pinchF's `rw [pinchF, pinchF']` — same issue possibly — use show-forms or `unfold`. Let me use `simp only [pinchF, pinchF']`? — simp only with the def name unfolds via equation lemmas ✓ standard. Or just `unfold pinchF pinchF'`. I'll use unfold.
5. div_le_iff₀ ascription: `rw [div_le_iff₀ (show (0:ℝ) < 2.5024 by norm_num)]`.
6. The pinch's Ici-memberships: now have log_twelve_le for them.
Let me write the fix patch.
Writing the fix patch for §20's issues.
tool: Write ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\patch_s20.py",
"content": "p = 'NguyenRH1/LiTightR.lean'\nsrc = open(p, encoding='utf-8').read()\n\n# Replace exp_point4848_le + log_twelve_ge with the log(4/3) route\nstart = src.index(\"\"\"/-- e^0.4848 \u2264 1.6239 (partial sums). -/\"\"\")\nend = src.index(\"\"\"/-- e^0.9173 \u2265 2.5024 (partial sums), hence log 2.5024 \u2264 0.9173. -/\"\"\")\nnew_pre = \"\"\"/-- The 4-term alternating bound: \u2212log(1\u2212y) \u2264 y + y\u00b2/2 + y\u00b3/3 + y\u2074/(4(1\u2212y)). -/\nlemma neg_log_one_sub_le_four {y : \u211d} (hy0 : 0 \u2264 y) (hy1 : y < 1) :\n -Real.log (1 - y) \u2264 y + y ^ 2 / 2 + y ^ 3 / 3 + y ^ 4 / (4 * (1 - y)) := by\n have hcont1 : ContinuousOn (fun t : \u211d => 1 / (1 - t)) (Set.uIcc 0 y) := by\n rw [Set.uIcc_of_le hy0]\n apply ContinuousOn.div continuousOn_const (continuousOn_const.sub continuousOn_id)\n intro t ht\n rw [Set.mem_Icc] at ht\n simp only [Pi.sub_apply, Pi.one_apply, id]\n linarith [ht.2, hy1]\n have hF : \u2200 t \u2208 Set.uIcc 0 y,\n HasDerivAt (fun x => -Real.log (1 - x)) (1 / (1 - t)) t := by\n intro t ht\n rw [Set.uIcc_of_le hy0, Set.mem_Icc] at ht\n have h1 : HasDerivAt (fun x : \u211d => 1 - x) (-1 : \u211d) t := by\n simpa using (hasDerivAt_id' t).const_sub 1\n have h2 := ((Real.hasDerivAt_log (by linarith [ht.2, hy1] : (1 : \u211d) - t \u2260 0)).comp t h1).neg\n rw [show (-(Real.log \u2218 fun x : \u211d => 1 - x)) = (fun x => -Real.log (1 - x)) from by\n ext y'\n simp only [Pi.neg_apply, Function.comp_apply]] at h2\n rw [one_div]\n simpa [Function.comp_def, mul_neg, neg_neg, one_mul] using h2\n have hG : \u2200 t \u2208 Set.uIcc 0 y,\n HasDerivAt (fun x => x + x ^ 2 / 2 + x ^ 3 / 3 + x ^ 4 / (4 * (1 - y)))\n (1 + t + t ^ 2 + t ^ 3 / (1 - y)) t := by\n intro t _\n have ha : HasDerivAt (fun x : \u211d => x) (1 : \u211d) t := hasDerivAt_id' t\n have hb : HasDerivAt (fun x : \u211d => x ^ 2 / 2) t t := by\n have h := (hasDerivAt_pow 2 t).div_const (2 : \u211d)\n rw [show ((2 : \u2115) : \u211d) * t ^ (2 - 1) / 2 = t 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 hc : HasDerivAt (fun x : \u211d => x ^ 3 / 3) (t ^ 2) t := by\n have h := (hasDerivAt_pow 3 t).div_const (3 : \u211d)\n rw [show ((3 : \u2115) : \u211d) * t ^ (3 - 1) / 3 = t ^ 2 from by\n rw [show (3 : \u2115) - 1 = 2 from rfl]\n push_cast\n ring] at h\n exact h\n have hd : HasDerivAt (fun x : \u211d => x ^ 4 / (4 * (1 - y))) (t ^ 3 / (1 - y)) t := by\n have h := (hasDerivAt_pow 4 t).div_const (4 * (1 - y))\n rw [show ((4 : \u2115) : \u211d) * t ^ (4 - 1) / (4 * (1 - y)) = t ^ 3 / (1 - y) from by\n rw [show (4 : \u2115) - 1 = 3 from rfl]\n push_cast\n field_simp [show (1 : \u211d) - y \u2260 0 by linarith [hy1]]\n ring] at h\n exact h\n exact (((ha.add hb).add hc).add hd)\n have hInt1 : \u222b t in (0 : \u211d)..y, 1 / (1 - t) = -Real.log (1 - y) := by\n rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hF\n (ContinuousOn.intervalIntegrable hcont1)]\n simp [Real.log_one]\n have hInt2 : \u222b t in (0 : \u211d)..y, (1 + t + t ^ 2 + t ^ 3 / (1 - y))\n = y + y ^ 2 / 2 + y ^ 3 / 3 + y ^ 4 / (4 * (1 - y)) := by\n rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hG\n (ContinuousOn.intervalIntegrable (by fun_prop))]\n ring_nf\n have hmono : \u222b t in (0 : \u211d)..y, 1 / (1 - t)\n \u2264 \u222b t in (0 : \u211d)..y, (1 + t + t ^ 2 + t ^ 3 / (1 - y)) := by\n apply intervalIntegral.integral_mono_on hy0\n (ContinuousOn.intervalIntegrable hcont1)\n (ContinuousOn.intervalIntegrable (by fun_prop))\n intro t ht\n rw [Set.mem_Icc] at ht\n have h1 : (0 : \u211d) < 1 - t := by linarith [ht.2, hy1]\n have h2 : (0 : \u211d) < 1 - y := by linarith [hy1]\n rw [div_le_iff\u2080 h1]\n have h3 : (1 + t + t ^ 2 + t ^ 3 / (1 - y)) * (1 - t)\n = 1 - t ^ 3 + t ^ 3 * (1 - t) / (1 - y) := by field_simp; ring\n rw [h3]\n have h4 : (t : \u211d) ^ 3 \u2264 t ^ 3 * (1 - t) / (1 - y) := by\n have h5 : (1 - y) \u2264 (1 - t) := by linarith [ht.2]\n have h6 : (0 : \u211d) \u2264 t ^ 3 := by positivity\n rw [div_le_iff\u2080 h2]\n calc t ^ 3 * (1 - y) \u2264 t ^ 3 * (1 - t) := mul_le_mul_of_nonneg_left h5 h6\n _ = t ^ 3 * (1 - t) * 1 := (mul_one _).symm\n linarith\n rw [hInt1, hInt2] at hmono\n exact hmono\n\n/-- log(4/3) \u2264 0.28777 (the 4-term bound at y = 1/4). -/\nlemma log_four_thirds_le : Real.log (4 / 3) \u2264 0.28777 := by\n have h1 : Real.log (4 / 3) = -Real.log (3 / 4) := by\n rw [show (4 : \u211d) / 3 = (3 / 4)\u207b\u00b9 from by norm_num, Real.log_inv]\n rw [h1]\n have h2 : (3 : \u211d) / 4 = 1 - 1 / 4 := by norm_num\n rw [h2]\n have h3 := neg_log_one_sub_le_four (y := 1 / 4) (by norm_num) (by norm_num)\n have h4 : (1 : \u211d) / 4 + (1 / 4) ^ 2 / 2 + (1 / 4) ^ 3 / 3 + (1 / 4) ^ 4 / (4 * (1 - 1 / 4))\n \u2264 0.28777 := by norm_num\n linarith [h3, h4]\n\n/-- e^0.0987 \u2265 1.10374, hence log 3 \u2264 1.0987. -/\nlemma log_three_le : Real.log 3 \u2264 1.0987 := by\n have h1 : (3 : \u211d) \u2264 Real.exp 1.0987 := by\n have h2 : Real.exp 1.0987 = Real.exp 1 * Real.exp 0.0987 := by\n rw [\u2190 Real.exp_add]\n congr 1\n norm_num\n rw [h2]\n have h3 : (1.10374 : \u211d) \u2264 Real.exp 0.0987 := by\n have h := Real.sum_le_exp_of_nonneg (show (0 : \u211d) \u2264 0.0987 by norm_num) 6\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_zero] at h\n norm_num at h\n linarith [h]\n have h4 : (2.7182818 : \u211d) \u2264 Real.exp 1 :=\n (by norm_num : (2.7182818 : \u211d) \u2264 2.7182818283).trans Real.exp_one_gt_d9.le\n have h5 : (3 : \u211d) \u2264 2.7182818 * 1.10374 := by norm_num\n have h6 := mul_le_mul h4 h3 (by positivity : (0 : \u211d) \u2264 1.10374) (Real.exp_pos 1).le\n exact h5.trans h6\n have h2 := Real.log_le_log (show (0 : \u211d) < 3 by norm_num) h1\n rwa [Real.log_exp] at h2\n\n/-- log 12 \u2265 2.4848: log 12 = 4\u00b7log 2 \u2212 log(4/3). -/\nlemma log_twelve_ge : (2.4848 : \u211d) \u2264 Real.log 12 := by\n have hlog2 : (0.6931471 : \u211d) \u2264 Real.log 2 :=\n (by norm_num : (0.6931471 : \u211d) \u2264 0.6931471803).trans Real.log_two_gt_d9.le\n have h43 := log_four_thirds_le\n have hdecomp : Real.log 12 = 4 * Real.log 2 - Real.log (4 / 3) := by\n have h1 : (12 : \u211d) = 2 ^ 4 * (3 / 4) := by norm_num\n rw [h1, Real.log_mul (by norm_num : ((2 : \u211d) ^ 4) \u2260 0) (by norm_num : (3 / 4 : \u211d) \u2260 0)]\n have h2 : Real.log ((2 : \u211d) ^ 4) = 4 * Real.log 2 := by\n rw [Real.log_pow]\n push_cast\n ring\n have h3 : Real.log (3 / 4) = -Real.log (4 / 3) := by\n rw [show (3 : \u211d) / 4 = (4 / 3)\u207b\u00b9 from by norm_num, Real.log_inv]\n rw [h2, h3]\n ring\n linarith [hdecomp, hlog2, h43]\n\n/-- log 12 \u2264 2.5024: log 12 = 2\u00b7log 2 + log 3. -/\nlemma log_twelve_le : Real.log 12 \u2264 2.5024 := by\n have hlog2 : Real.log 2 \u2264 0.69315 := Real.log_two_lt_d9.le.trans (by norm_num)\n have h3 := log_three_le\n have hdecomp : Real.log 12 = 2 * Real.log 2 + Real.log 3 := by\n have h1 : (12 : \u211d) = 4 * 3 := by norm_num\n rw [h1, Real.log_mul (by norm_num : (4 : \u211d) \u2260 0) (by norm_num : (3 : \u211d) \u2260 0)]\n have h2 : Real.log 4 = 2 * Real.log 2 := by\n have h3' : (4 : \u211d) = 2 ^ 2 := by norm_num\n rw [h3', Real.log_pow]\n push_cast\n ring\n rw [h2]\n linarith [hdecomp, hlog2, h3]\n\n\"\"\"\nsrc = src[:start] + new_pre + src[end:]\n\n# pinchF unfolds: use show-rfl forms\nsrc = src.replace(\"\"\"lemma pinchF_at_critical : pinchF 2.5024 \u2264 -0.96203 := by\n rw [pinchF]\"\"\", \"\"\"lemma pinchF_at_critical : pinchF 2.5024 \u2264 -0.96203 := by\n rw [show pinchF 2.5024 = 11.6321 * Real.log 2.5024 - 4.6484 * 2.5024 from rfl]\"\"\")\n\nsrc = src.replace(\"\"\"lemma 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]\"\"\", \"\"\"lemma pinchF'_at_critical : pinchF' 2.5024 \u2264 0 := by\n rw [show pinchF' 2.5024 = 11.6321 / 2.5024 - 4.6484 from rfl]\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 (show (0 : \u211d) < 2.5024 by norm_num)]\n exact h1\n linarith [h2]\"\"\")\n\nsrc = src.replace(\"\"\" 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]]\"\"\", \"\"\" unfold 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\nopen(p, 'w', encoding='utf-8').write(src)\nprint(\"done\")\n"
}
result 2026-08-24 21:35:51Z → 2026-08-24 21:35:51Z
{
"type": "create",
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\patch_s20.py",
"content": "p = 'NguyenRH1/LiTightR.lean'\nsrc = open(p, encoding='utf-8').read()\n\n# Replace exp_point4848_le + log_twelve_ge with the log(4/3) route\nstart = src.index(\"\"\"/-- e^0.4848 \u2264 1.6239 (partial sums). -/\"\"\")\nend = src.index(\"\"\"/-- e^0.9173 \u2265 2.5024 (partial sums), hence log 2.5024 \u2264 0.9173. -/\"\"\")\nnew_pre = \"\"\"/-- The 4-term alternating bound: \u2212log(1\u2212y) \u2264 y + y\u00b2/2 + y\u00b3/3 + y\u2074/(4(1\u2212y)). -/\nlemma neg_log_one_sub_le_four {y : \u211d} (hy0 : 0 \u2264 y) (hy1 : y < 1) :\n -Real.log (1 - y) \u2264 y + y ^ 2 / 2 + y ^ 3 / 3 + y ^ 4 / (4 * (1 - y)) := by\n have hcont1 : ContinuousOn (fun t : \u211d => 1 / (1 - t)) (Set.uIcc 0 y) := by\n rw [Set.uIcc_of_le hy0]\n apply ContinuousOn.div continuousOn_const (continuousOn_const.sub continuousOn_id)\n intro t ht\n rw [Set.mem_Icc] at ht\n simp only [Pi.sub_apply, Pi.one_apply, id]\n linarith [ht.2, hy1]\n have hF : \u2200 t \u2208 Set.uIcc 0 y,\n HasDerivAt (fun x => -Real.log (1 - x)) (1 / (1 - t)) t := by\n intro t ht\n rw [Set.uIcc_of_le hy0, Set.mem_Icc] at ht\n have h1 : HasDerivAt (fun x : \u211d => 1 - x) (-1 : \u211d) t := by\n simpa using (hasDerivAt_id' t).const_sub 1\n have h2 := ((Real.hasDerivAt_log (by linarith [ht.2, hy1] : (1 : \u211d) - t \u2260 0)).comp t h1).neg\n rw [show (-(Real.log \u2218 fun x : \u211d => 1 - x)) = (fun x => -Real.log (1 - x)) from by\n ext y'\n simp only [Pi.neg_apply, Function.comp_apply]] at h2\n rw [one_div]\n simpa [Function.comp_def, mul_neg, neg_neg, one_mul] using h2\n have hG : \u2200 t \u2208 Set.uIcc 0 y,\n HasDerivAt (fun x => x + x ^ 2 / 2 + x ^ 3 / 3 + x ^ 4 / (4 * (1 - y)))\n (1 + t + t ^ 2 + t ^ 3 / (1 - y)) t := by\n intro t _\n have ha : HasDerivAt (fun x : \u211d => x) (1 : \u211d) t := hasDerivAt_id' t\n have hb : HasDerivAt (fun x : \u211d => x ^ 2 / 2) t t := by\n have h := (hasDerivAt_pow 2 t).div_const (2 : \u211d)\n rw [show ((2 : \u2115) : \u211d) * t ^ (2 - 1) / 2 = t 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 hc : HasDerivAt (fun x : \u211d => x ^ 3 / 3) (t ^ 2) t := by\n have h := (hasDerivAt_pow 3 t).div_const (3 : \u211d)\n rw [show ((3 : \u2115) : \u211d) * t ^ (3 - 1) / 3 = t ^ 2 from by\n rw [show (3 : \u2115) - 1 = 2 from rfl]\n push_cast\n ring] at h\n exact h\n have hd : HasDerivAt (fun x : \u211d => x ^ 4 / (4 * (1 - y))) (t ^ 3 / (1 - y)) t := by\n have h := (hasDerivAt_pow 4 t).div_const (4 * (1 - y))\n rw [show ((4 : \u2115) : \u211d) * t ^ (4 - 1) / (4 * (1 - y)) = t ^ 3 / (1 - y) from by\n rw [show (4 : \u2115) - 1 = 3 from rfl]\n push_cast\n field_simp [show (1 : \u211d) - y \u2260 0 by linarith [hy1]]\n ring] at h\n exact h\n exact (((ha.add hb).add hc).add hd)\n have hInt1 : \u222b t in (0 : \u211d)..y, 1 / (1 - t) = -Real.log (1 - y) := by\n rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hF\n (ContinuousOn.intervalIntegrable hcont1)]\n simp [Real.log_one]\n have hInt2 : \u222b t in (0 : \u211d)..y, (1 + t + t ^ 2 + t ^ 3 / (1 - y))\n = y + y ^ 2 / 2 + y ^ 3 / 3 + y ^ 4 / (4 * (1 - y)) := by\n rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hG\n (ContinuousOn.intervalIntegrable (by fun_prop))]\n ring_nf\n have hmono : \u222b t in (0 : \u211d)..y, 1 / (1 - t)\n \u2264 \u222b t in (0 : \u211d)..y, (1 + t + t ^ 2 + t ^ 3 / (1 - y)) := by\n apply intervalIntegral.integral_mono_on hy0\n (ContinuousOn.intervalIntegrable hcont1)\n (ContinuousOn.intervalIntegrable (by fun_prop))\n intro t ht\n rw [Set.mem_Icc] at ht\n have h1 : (0 : \u211d) < 1 - t := by linarith [ht.2, hy1]\n have h2 : (0 : \u211d) < 1 - y := by linarith [hy1]\n rw [div_le_iff\u2080 h1]\n have h3 : (1 + t + t ^ 2 + t ^ 3 / (1 - y)) * (1 - t)\n = 1 - t ^ 3 + t ^ 3 * (1 - t) / (1 - y) := by field_simp; ring\n rw [h3]\n have h4 : (t : \u211d) ^ 3 \u2264 t ^ 3 * (1 - t) / (1 - y) := by\n have h5 : (1 - y) \u2264 (1 - t) := by linarith [ht.2]\n have h6 : (0 : \u211d) \u2264 t ^ 3 := by positivity\n rw [div_le_iff\u2080 h2]\n calc t ^ 3 * (1 - y) \u2264 t ^ 3 * (1 - t) := mul_le_mul_of_nonneg_left h5 h6\n _ = t ^ 3 * (1 - t) * 1 := (mul_one _).symm\n linarith\n rw [hInt1, hInt2] at hmono\n exact hmono\n\n/-- log(4/3) \u2264 0.28777 (the 4-term bound at y = 1/4). -/\nlemma log_four_thirds_le : Real.log (4 / 3) \u2264 0.28777 := by\n have h1 : Real.log (4 / 3) = -Real.log (3 / 4) := by\n rw [show (4 : \u211d) / 3 = (3 / 4)\u207b\u00b9 from by norm_num, Real.log_inv]\n rw [h1]\n have h2 : (3 : \u211d) / 4 = 1 - 1 / 4 := by norm_num\n rw [h2]\n have h3 := neg_log_one_sub_le_four (y := 1 / 4) (by norm_num) (by norm_num)\n have h4 : (1 : \u211d) / 4 + (1 / 4) ^ 2 / 2 + (1 / 4) ^ 3 / 3 + (1 / 4) ^ 4 / (4 * (1 - 1 / 4))\n \u2264 0.28777 := by norm_num\n linarith [h3, h4]\n\n/-- e^0.0987 \u2265 1.10374, hence log 3 \u2264 1.0987. -/\nlemma log_three_le : Real.log 3 \u2264 1.0987 := by\n have h1 : (3 : \u211d) \u2264 Real.exp 1.0987 := by\n have h2 : Real.exp 1.0987 = Real.exp 1 * Real.exp 0.0987 := by\n rw [\u2190 Real.exp_add]\n congr 1\n norm_num\n rw [h2]\n have h3 : (1.10374 : \u211d) \u2264 Real.exp 0.0987 := by\n have h := Real.sum_le_exp_of_nonneg (show (0 : \u211d) \u2264 0.0987 by norm_num) 6\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_zero] at h\n norm_num at h\n linarith [h]\n have h4 : (2.7182818 : \u211d) \u2264 Real.exp 1 :=\n (by norm_num : (2.7182818 : \u211d) \u2264 2.7182818283).trans Real.exp_one_gt_d9.le\n have h5 : (3 : \u211d) \u2264 2.7182818 * 1.10374 := by norm_num\n have h6 := mul_le_mul h4 h3 (by positivity : (0 : \u211d) \u2264 1.10374) (Real.exp_pos 1).le\n exact h5.trans h6\n have h2 := Real.log_le_log (show (0 : \u211d) < 3 by norm_num) h1\n rwa [Real.log_exp] at h2\n\n/-- log 12 \u2265 2.4848: log 12 = 4\u00b7log 2 \u2212 log(4/3). -/\nlemma log_twelve_ge : (2.4848 : \u211d) \u2264 Real.log 12 := by\n have hlog2 : (0.6931471 : \u211d) \u2264 Real.log 2 :=\n (by norm_num : (0.6931471 : \u211d) \u2264 0.6931471803).trans Real.log_two_gt_d9.le\n have h43 := log_four_thirds_le\n have hdecomp : Real.log 12 = 4 * Real.log 2 - Real.log (4 / 3) := by\n have h1 : (12 : \u211d) = 2 ^ 4 * (3 / 4) := by norm_num\n rw [h1, Real.log_mul (by norm_num : ((2 : \u211d) ^ 4) \u2260 0) (by norm_num : (3 / 4 : \u211d) \u2260 0)]\n have h2 : Real.log ((2 : \u211d) ^ 4) = 4 * Real.log 2 := by\n rw [Real.log_pow]\n push_cast\n ring\n have h3 : Real.log (3 / 4) = -Real.log (4 / 3) := by\n rw [show (3 : \u211d) / 4 = (4 / 3)\u207b\u00b9 from by norm_num, Real.log_inv]\n rw [h2, h3]\n ring\n linarith [hdecomp, hlog2, h43]\n\n/-- log 12 \u2264 2.5024: log 12 = 2\u00b7log 2 + log 3. -/\nlemma log_twelve_le : Real.log 12 \u2264 2.5024 := by\n have hlog2 : Real.log 2 \u2264 0.69315 := Real.log_two_lt_d9.le.trans (by norm_num)\n have h3 := log_three_le\n have hdecomp : Real.log 12 = 2 * Real.log 2 + Real.log 3 := by\n have h1 : (12 : \u211d) = 4 * 3 := by norm_num\n rw [h1, Real.log_mul (by norm_num : (4 : \u211d) \u2260 0) (by norm_num : (3 : \u211d) \u2260 0)]\n have h2 : Real.log 4 = 2 * Real.log 2 := by\n have h3' : (4 : \u211d) = 2 ^ 2 := by norm_num\n rw [h3', Real.log_pow]\n push_cast\n ring\n rw [h2]\n linarith [hdecomp, hlog2, h3]\n\n\"\"\"\nsrc = src[:start] + new_pre + src[end:]\n\n# pinchF unfolds: use show-rfl forms\nsrc = src.replace(\"\"\"lemma pinchF_at_critical : pinchF 2.5024 \u2264 -0.96203 := by\n rw [pinchF]\"\"\", \"\"\"lemma pinchF_at_critical : pinchF 2.5024 \u2264 -0.96203 := by\n rw [show pinchF 2.5024 = 11.6321 * Real.log 2.5024 - 4.6484 * 2.5024 from rfl]\"\"\")\n\nsrc = src.replace(\"\"\"lemma 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]\"\"\", \"\"\"lemma pinchF'_at_critical : pinchF' 2.5024 \u2264 0 := by\n rw [show pinchF' 2.5024 = 11.6321 / 2.5024 - 4.6484 from rfl]\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 (show (0 : \u211d) < 2.5024 by norm_num)]\n exact h1\n linarith [h2]\"\"\")\n\nsrc = src.replace(\"\"\" 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]]\"\"\", \"\"\" unfold 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\nopen(p, 'w', encoding='utf-8').write(src)\nprint(\"done\")\n",
"structuredPatch": [],
"originalFile": null
}
raw content_json (database row)
[{"type":"thinking","thinking":"`div_le_iff₀ (hc : 0 < c) : b / c ≤ a ↔ b ≤ a * c` — for my use: 11.6321/2.5024 ≤ 4.6484 ⟺ 11.6321 ≤ 4.6484 * 2.5024 ✓ — the form b/c ≤ a with b = 11.6321, a = 4.6484: rw [div_le_iff₀ hc] gives `11.6321 ≤ 4.6484 * 2.5024` ✓ — my error at 3998 said the pattern `?m/2.5024 ≤ ?m` didn't match `11.6321 / 2.5024 ≤ 4.6484`... hmm — it SHOULD match. Unless the hc arg position: div_le_iff₀ (hc : 0 < c) — with c implicit from hc. My call `rw [div_le_iff₀ (by norm_num : (0:ℝ) < 2.5024)]` ✓ should work. The error might be the ascription binding issue again (`by norm_num : (0:ℝ) < 2.5024` parsing weirdly with the `:`). Let me use show-forms throughout.\n\nNow the bigger issue list. Let me write the fixes:\n\n1. Replace exp_point4848_le + log_twelve_ge with the log(4/3) route:\n```\n/-- The 4-term alternating bound: −log(1−y) ≤ y + y²/2 + y³/3 + y⁴/(4(1−y)). -/\nlemma neg_log_one_sub_le_four {y : ℝ} (hy0 : 0 ≤ y) (hy1 : y < 1) :\n -Real.log (1 - y) ≤ y + y ^ 2 / 2 + y ^ 3 / 3 + y ^ 4 / (4 * (1 - y)) := by\n -- same integral machine as neg_log_one_sub_le with the t³ term\n ...\n```\nThe machine: 1/(1−t) ≤ 1+t+t²+t³/(1−y) on [0,y]: (1−t)(1+t+t²+t³/(1−y)) = 1−t³ + t³(1−t)/(1−y) ≥ 1 ⟺ t³(1−t)/(1−y) ≥ t³ ⟺ (1−t)/(1−y) ≥ 1 ⟺ t ≤ y ✓. The antiderivative: y+y²/2+y³/3+y⁴/(4(1−y)) — HasDerivAt of the poly ✓ (same hG pattern).\n\n```\n/-- log(4/3) ≤ 0.28777 (the 4-term bound at y = 1/4). -/\nlemma log_four_thirds_le : Real.log (4 / 3) ≤ 0.28777 := by\n have h1 : Real.log (4 / 3) = -Real.log (3 / 4) := by\n rw [show (4 : ℝ) / 3 = (3 / 4)⁻¹ from by norm_num, Real.log_inv]\n rw [h1]\n have h2 : (3 : ℝ) / 4 = 1 - 1 / 4 := by norm_num\n rw [h2]\n have h3 := neg_log_one_sub_le_four (y := 1 / 4) (by norm_num) (by norm_num)\n -- 1/4 + (1/4)²/2 + (1/4)³/3 + (1/4)⁴/(4(1−1/4)) = 0.2877604 ≤ 0.28777\n have h4 : (1 : ℝ) / 4 + (1 / 4) ^ 2 / 2 + (1 / 4) ^ 3 / 3 + (1 / 4) ^ 4 / (4 * (1 - 1 / 4))\n ≤ 0.28777 := by norm_num\n linarith [h3, h4]\n\n/-- log 12 ≥ 2.4848: log 12 = 4·log 2 − log(4/3). -/\nlemma log_twelve_ge : (2.4848 : ℝ) ≤ Real.log 12 := by\n have hlog2 : (0.6931471 : ℝ) ≤ Real.log 2 :=\n (by norm_num : (0.6931471 : ℝ) ≤ 0.6931471803).trans Real.log_two_gt_d9.le\n have h43 := log_four_thirds_le\n have hdecomp : Real.log 12 = 4 * Real.log 2 - Real.log (4 / 3) := by\n have h1 : (12 : ℝ) = 2 ^ 4 * (3 / 4) := by norm_num\n rw [h1, Real.log_mul (by norm_num : ((2 : ℝ) ^ 4) ≠ 0) (by norm_num : (3 / 4 : ℝ) ≠ 0)]\n have h2 : Real.log ((2 : ℝ) ^ 4) = 4 * Real.log 2 := by\n rw [Real.log_pow]\n push_cast\n ring\n rw [h2]\n have h3 : Real.log (3 / 4) = -Real.log (4 / 3) := by\n rw [show (3 : ℝ) / 4 = (4 / 3)⁻¹ from by norm_num, Real.log_inv]\n rw [h3]\n ring\n linarith [hdecomp, hlog2, h43]\n```\nCheck: 4·0.6931471 − 0.28777 = 2.7725884−0.28777 = 2.4848184 ≥ 2.4848 ✓ (margin 1.84e-5 — wait — but the TRUE log(4/3) = 0.287682 and my bound is ≤ 0.28777 — the 4-term gives 0.2877604 ≤ 0.28777 ✓ — so log 12 ≥ 2.7725884−0.28777 = 2.4848184 ✓ margin 1.84e-5 — TIGHT but exact. Hmm — actually, with the sharper 4-term value 0.2877604: 2.7725884−0.2877604 = 2.484828 ✓ margin 2.8e-5.)\n\n2. log_twelve_le : Real.log 12 ≤ 2.5024: log 12 = 2 log 2 + log 3 ≤ 2·0.69315+1.0987 = 2.485 ≤ 2.5024: log 3 ≤ 1.0987 via 3 ≤ e^1.0987 (partial sums e^1.0987 = e·e^0.0987 ≥ 2.7182818·1.103735 ≥ 3 ✓).\n```\nlemma log_three_le : Real.log 3 ≤ 1.0987 := by\n have h1 : (3 : ℝ) ≤ Real.exp 1.0987 := by\n have h2 : Real.exp 1.0987 = Real.exp 1 * Real.exp 0.0987 := by\n rw [← Real.exp_add]\n congr 1\n norm_num\n rw [h2]\n have h3 : (1.10374 : ℝ) ≤ Real.exp 0.0987 := by\n have h := Real.sum_le_exp_of_nonneg (show (0 : ℝ) ≤ 0.0987 by norm_num) 6\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_zero] at h\n norm_num at h\n linarith [h]\n have h4 : (2.7182818 : ℝ) ≤ Real.exp 1 :=\n (by norm_num : (2.7182818 : ℝ) ≤ 2.7182818283).trans Real.exp_one_gt_d9.le\n have h5 : (3 : ℝ) ≤ 2.7182818 * 1.10374 := by norm_num\n have h6 := mul_le_mul h4 h3 (by positivity : (0 : ℝ) ≤ 1.10374) (Real.exp_pos 1).le\n exact h5.trans h6\n have h2 := Real.log_le_log (by norm_num : (0 : ℝ) < 3) h1\n rwa [Real.log_exp] at h2\nlemma log_twelve_le : Real.log 12 ≤ 2.5024 := by\n have hlog2 : Real.log 2 ≤ 0.69315 := Real.log_two_lt_d9.le.trans (by norm_num)\n have h3 := log_three_le\n have hdecomp : Real.log 12 = 2 * Real.log 2 + Real.log 3 := by\n have h1 : (12 : ℝ) = 4 * 3 := by norm_num\n rw [h1, Real.log_mul (by norm_num : (4 : ℝ) ≠ 0) (by norm_num : (3 : ℝ) ≠ 0)]\n have h2 : Real.log 4 = 2 * Real.log 2 := by\n have h3' : (4 : ℝ) = 2 ^ 2 := by norm_num\n rw [h3', Real.log_pow]\n push_cast\n ring\n rw [h2]\n linarith [hdecomp, hlog2, h3]\n```\n2·0.69315+1.0987 = 1.3863+1.0987 = 2.4850 ≤ 2.5024 ✓.\n\n3. h5 ascription in log_twelve_ge — gone (new route).\n\n4. pinchF unfolds: use `rw [show pinchF 2.5024 = 11.6321 * Real.log 2.5024 - 4.6484 * 2.5024 from rfl]` in pinchF_at_critical, and similarly pinchF'. And in hasDerivAt_pinchF's `rw [pinchF, pinchF']` — same issue possibly — use show-forms or `unfold`. Let me use `simp only [pinchF, pinchF']`? — simp only with the def name unfolds via equation lemmas ✓ standard. Or just `unfold pinchF pinchF'`. I'll use unfold.\n\n5. div_le_iff₀ ascription: `rw [div_le_iff₀ (show (0:ℝ) < 2.5024 by norm_num)]`.\n\n6. The pinch's Ici-memberships: now have log_twelve_le for them.\n\nLet me write the fix patch.","signature":""},{"type":"text","text":"Writing the fix patch for §20's issues."},{"type":"tool_use","id":"Write_283","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\patch_s20.py","content":"p = 'NguyenRH1/LiTightR.lean'\nsrc = open(p, encoding='utf-8').read()\n\n# Replace exp_point4848_le + log_twelve_ge with the log(4/3) route\nstart = src.index(\"\"\"/-- e^0.4848 ≤ 1.6239 (partial sums). -/\"\"\")\nend = src.index(\"\"\"/-- e^0.9173 ≥ 2.5024 (partial sums), hence log 2.5024 ≤ 0.9173. -/\"\"\")\nnew_pre = \"\"\"/-- The 4-term alternating bound: −log(1−y) ≤ y + y²/2 + y³/3 + y⁴/(4(1−y)). -/\nlemma neg_log_one_sub_le_four {y : ℝ} (hy0 : 0 ≤ y) (hy1 : y < 1) :\n -Real.log (1 - y) ≤ y + y ^ 2 / 2 + y ^ 3 / 3 + y ^ 4 / (4 * (1 - y)) := by\n have hcont1 : ContinuousOn (fun t : ℝ => 1 / (1 - t)) (Set.uIcc 0 y) := by\n rw [Set.uIcc_of_le hy0]\n apply ContinuousOn.div continuousOn_const (continuousOn_const.sub continuousOn_id)\n intro t ht\n rw [Set.mem_Icc] at ht\n simp only [Pi.sub_apply, Pi.one_apply, id]\n linarith [ht.2, hy1]\n have hF : ∀ t ∈ Set.uIcc 0 y,\n HasDerivAt (fun x => -Real.log (1 - x)) (1 / (1 - t)) t := by\n intro t ht\n rw [Set.uIcc_of_le hy0, Set.mem_Icc] at ht\n have h1 : HasDerivAt (fun x : ℝ => 1 - x) (-1 : ℝ) t := by\n simpa using (hasDerivAt_id' t).const_sub 1\n have h2 := ((Real.hasDerivAt_log (by linarith [ht.2, hy1] : (1 : ℝ) - t ≠ 0)).comp t h1).neg\n rw [show (-(Real.log ∘ fun x : ℝ => 1 - x)) = (fun x => -Real.log (1 - x)) from by\n ext y'\n simp only [Pi.neg_apply, Function.comp_apply]] at h2\n rw [one_div]\n simpa [Function.comp_def, mul_neg, neg_neg, one_mul] using h2\n have hG : ∀ t ∈ Set.uIcc 0 y,\n HasDerivAt (fun x => x + x ^ 2 / 2 + x ^ 3 / 3 + x ^ 4 / (4 * (1 - y)))\n (1 + t + t ^ 2 + t ^ 3 / (1 - y)) t := by\n intro t _\n have ha : HasDerivAt (fun x : ℝ => x) (1 : ℝ) t := hasDerivAt_id' t\n have hb : HasDerivAt (fun x : ℝ => x ^ 2 / 2) t t := by\n have h := (hasDerivAt_pow 2 t).div_const (2 : ℝ)\n rw [show ((2 : ℕ) : ℝ) * t ^ (2 - 1) / 2 = t from by\n rw [show (2 : ℕ) - 1 = 1 from rfl, pow_one]\n push_cast\n ring] at h\n exact h\n have hc : HasDerivAt (fun x : ℝ => x ^ 3 / 3) (t ^ 2) t := by\n have h := (hasDerivAt_pow 3 t).div_const (3 : ℝ)\n rw [show ((3 : ℕ) : ℝ) * t ^ (3 - 1) / 3 = t ^ 2 from by\n rw [show (3 : ℕ) - 1 = 2 from rfl]\n push_cast\n ring] at h\n exact h\n have hd : HasDerivAt (fun x : ℝ => x ^ 4 / (4 * (1 - y))) (t ^ 3 / (1 - y)) t := by\n have h := (hasDerivAt_pow 4 t).div_const (4 * (1 - y))\n rw [show ((4 : ℕ) : ℝ) * t ^ (4 - 1) / (4 * (1 - y)) = t ^ 3 / (1 - y) from by\n rw [show (4 : ℕ) - 1 = 3 from rfl]\n push_cast\n field_simp [show (1 : ℝ) - y ≠ 0 by linarith [hy1]]\n ring] at h\n exact h\n exact (((ha.add hb).add hc).add hd)\n have hInt1 : ∫ t in (0 : ℝ)..y, 1 / (1 - t) = -Real.log (1 - y) := by\n rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hF\n (ContinuousOn.intervalIntegrable hcont1)]\n simp [Real.log_one]\n have hInt2 : ∫ t in (0 : ℝ)..y, (1 + t + t ^ 2 + t ^ 3 / (1 - y))\n = y + y ^ 2 / 2 + y ^ 3 / 3 + y ^ 4 / (4 * (1 - y)) := by\n rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hG\n (ContinuousOn.intervalIntegrable (by fun_prop))]\n ring_nf\n have hmono : ∫ t in (0 : ℝ)..y, 1 / (1 - t)\n ≤ ∫ t in (0 : ℝ)..y, (1 + t + t ^ 2 + t ^ 3 / (1 - y)) := by\n apply intervalIntegral.integral_mono_on hy0\n (ContinuousOn.intervalIntegrable hcont1)\n (ContinuousOn.intervalIntegrable (by fun_prop))\n intro t ht\n rw [Set.mem_Icc] at ht\n have h1 : (0 : ℝ) < 1 - t := by linarith [ht.2, hy1]\n have h2 : (0 : ℝ) < 1 - y := by linarith [hy1]\n rw [div_le_iff₀ h1]\n have h3 : (1 + t + t ^ 2 + t ^ 3 / (1 - y)) * (1 - t)\n = 1 - t ^ 3 + t ^ 3 * (1 - t) / (1 - y) := by field_simp; ring\n rw [h3]\n have h4 : (t : ℝ) ^ 3 ≤ t ^ 3 * (1 - t) / (1 - y) := by\n have h5 : (1 - y) ≤ (1 - t) := by linarith [ht.2]\n have h6 : (0 : ℝ) ≤ t ^ 3 := by positivity\n rw [div_le_iff₀ h2]\n calc t ^ 3 * (1 - y) ≤ t ^ 3 * (1 - t) := mul_le_mul_of_nonneg_left h5 h6\n _ = t ^ 3 * (1 - t) * 1 := (mul_one _).symm\n linarith\n rw [hInt1, hInt2] at hmono\n exact hmono\n\n/-- log(4/3) ≤ 0.28777 (the 4-term bound at y = 1/4). -/\nlemma log_four_thirds_le : Real.log (4 / 3) ≤ 0.28777 := by\n have h1 : Real.log (4 / 3) = -Real.log (3 / 4) := by\n rw [show (4 : ℝ) / 3 = (3 / 4)⁻¹ from by norm_num, Real.log_inv]\n rw [h1]\n have h2 : (3 : ℝ) / 4 = 1 - 1 / 4 := by norm_num\n rw [h2]\n have h3 := neg_log_one_sub_le_four (y := 1 / 4) (by norm_num) (by norm_num)\n have h4 : (1 : ℝ) / 4 + (1 / 4) ^ 2 / 2 + (1 / 4) ^ 3 / 3 + (1 / 4) ^ 4 / (4 * (1 - 1 / 4))\n ≤ 0.28777 := by norm_num\n linarith [h3, h4]\n\n/-- e^0.0987 ≥ 1.10374, hence log 3 ≤ 1.0987. -/\nlemma log_three_le : Real.log 3 ≤ 1.0987 := by\n have h1 : (3 : ℝ) ≤ Real.exp 1.0987 := by\n have h2 : Real.exp 1.0987 = Real.exp 1 * Real.exp 0.0987 := by\n rw [← Real.exp_add]\n congr 1\n norm_num\n rw [h2]\n have h3 : (1.10374 : ℝ) ≤ Real.exp 0.0987 := by\n have h := Real.sum_le_exp_of_nonneg (show (0 : ℝ) ≤ 0.0987 by norm_num) 6\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_zero] at h\n norm_num at h\n linarith [h]\n have h4 : (2.7182818 : ℝ) ≤ Real.exp 1 :=\n (by norm_num : (2.7182818 : ℝ) ≤ 2.7182818283).trans Real.exp_one_gt_d9.le\n have h5 : (3 : ℝ) ≤ 2.7182818 * 1.10374 := by norm_num\n have h6 := mul_le_mul h4 h3 (by positivity : (0 : ℝ) ≤ 1.10374) (Real.exp_pos 1).le\n exact h5.trans h6\n have h2 := Real.log_le_log (show (0 : ℝ) < 3 by norm_num) h1\n rwa [Real.log_exp] at h2\n\n/-- log 12 ≥ 2.4848: log 12 = 4·log 2 − log(4/3). -/\nlemma log_twelve_ge : (2.4848 : ℝ) ≤ Real.log 12 := by\n have hlog2 : (0.6931471 : ℝ) ≤ Real.log 2 :=\n (by norm_num : (0.6931471 : ℝ) ≤ 0.6931471803).trans Real.log_two_gt_d9.le\n have h43 := log_four_thirds_le\n have hdecomp : Real.log 12 = 4 * Real.log 2 - Real.log (4 / 3) := by\n have h1 : (12 : ℝ) = 2 ^ 4 * (3 / 4) := by norm_num\n rw [h1, Real.log_mul (by norm_num : ((2 : ℝ) ^ 4) ≠ 0) (by norm_num : (3 / 4 : ℝ) ≠ 0)]\n have h2 : Real.log ((2 : ℝ) ^ 4) = 4 * Real.log 2 := by\n rw [Real.log_pow]\n push_cast\n ring\n have h3 : Real.log (3 / 4) = -Real.log (4 / 3) := by\n rw [show (3 : ℝ) / 4 = (4 / 3)⁻¹ from by norm_num, Real.log_inv]\n rw [h2, h3]\n ring\n linarith [hdecomp, hlog2, h43]\n\n/-- log 12 ≤ 2.5024: log 12 = 2·log 2 + log 3. -/\nlemma log_twelve_le : Real.log 12 ≤ 2.5024 := by\n have hlog2 : Real.log 2 ≤ 0.69315 := Real.log_two_lt_d9.le.trans (by norm_num)\n have h3 := log_three_le\n have hdecomp : Real.log 12 = 2 * Real.log 2 + Real.log 3 := by\n have h1 : (12 : ℝ) = 4 * 3 := by norm_num\n rw [h1, Real.log_mul (by norm_num : (4 : ℝ) ≠ 0) (by norm_num : (3 : ℝ) ≠ 0)]\n have h2 : Real.log 4 = 2 * Real.log 2 := by\n have h3' : (4 : ℝ) = 2 ^ 2 := by norm_num\n rw [h3', Real.log_pow]\n push_cast\n ring\n rw [h2]\n linarith [hdecomp, hlog2, h3]\n\n\"\"\"\nsrc = src[:start] + new_pre + src[end:]\n\n# pinchF unfolds: use show-rfl forms\nsrc = src.replace(\"\"\"lemma pinchF_at_critical : pinchF 2.5024 ≤ -0.96203 := by\n rw [pinchF]\"\"\", \"\"\"lemma pinchF_at_critical : pinchF 2.5024 ≤ -0.96203 := by\n rw [show pinchF 2.5024 = 11.6321 * Real.log 2.5024 - 4.6484 * 2.5024 from rfl]\"\"\")\n\nsrc = src.replace(\"\"\"lemma 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]\"\"\", \"\"\"lemma pinchF'_at_critical : pinchF' 2.5024 ≤ 0 := by\n rw [show pinchF' 2.5024 = 11.6321 / 2.5024 - 4.6484 from rfl]\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₀ (show (0 : ℝ) < 2.5024 by norm_num)]\n exact h1\n linarith [h2]\"\"\")\n\nsrc = src.replace(\"\"\" rw [pinchF, pinchF']\n rw [show (11.6321 : ℝ) * x⁻¹ - 4.6484 = 11.6321 / x - 4.6484 from by\n rw [div_eq_mul_inv]]\"\"\", \"\"\" unfold pinchF pinchF'\n rw [show (11.6321 : ℝ) * x⁻¹ - 4.6484 = 11.6321 / x - 4.6484 from by\n rw [div_eq_mul_inv]]\"\"\")\n\nopen(p, 'w', encoding='utf-8').write(src)\nprint(\"done\")\n"},"extra_content":null}]