← Session 35 — ii′-6-R: Lagarias 6.1 right-tail re-proof (E-032/D-073)
thinking (10078 chars)
Now the big one: marginTilde_convex. The pieces to change:
1. hTn: `Real.sqrt 20 + 1 ≤ Real.sqrt n + 1` → `Real.sqrt 20 + 1 ≤ 1.5 * Real.sqrt n + 1`.
2. Composition bundles hCDFc, hCDTL1c, hCDTL2c, hCDL1sqc, hCDL1L2c, hCDL2sqc, hCDL1c, hCDL2c: inner fun → 1.5·√m+1 with the k-lemmas.
3. vF, vTL1, vTL2, vId, vL1sq, vL1L2, vL2sq, vL1, vL2: use chain_rule_sqrt_kshift_on + ← psiOf_sqrt_krel; values get the 1.5² factor.
4. vIIM: (−1.5)·IIMaj″.
5. hnn1–hnn9: adapt with 1.5².
6. hIIM → IIMaj_deriv2_lt_three; final linarith with the reciprocal bridge.
Let me write the whole replacement for the v-block section and the sign-assembly section. The current text (with shifted line numbers) — I need to replace from `have hCDFc` through the final linarith. Let me do it in two edits: (a) the composition bundles + hTn + v-blocks; (b) the hnn* + final linarith.
For (a), the current text:
```
have hTn : Real.sqrt 20 + 1 ≤ Real.sqrt n + 1 := by
have h := Real.sqrt_le_sqrt (show (20 : ℝ) ≤ n by linarith)
linarith
```
New:
```
have hTn : Real.sqrt 20 + 1 ≤ 1.5 * Real.sqrt n + 1 := by
have h := Real.sqrt_le_sqrt (show (20 : ℝ) ≤ n by linarith)
have hnn := Real.sqrt_nonneg n
linarith
```
Composition bundles — current:
```
have hCDFc : ContDiffOn ℝ 2 (fun m => F (Real.sqrt m + 1)) (Set.Ioi 20) :=
hF.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift_Ioi1
have hCDTL1c : ContDiffOn ℝ 2
(fun m => (fun t => t * Real.log (t + 2)) (Real.sqrt m + 1)) (Set.Ioi 20) :=
contDiffOn_TL1.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift
...
```
New: inner fun 1.5·√m+1, k-lemmas.
vF current:
```
have vF : deriv (deriv (mFblock F)) n =
(-4) * (psiOf F (Real.sqrt n + 1) / (4 * n)) := by
unfold mFblock
rw [deriv2_const_mul (-4) (hdd hCDFc) (hev hCDFc),
chain_rule_sqrt_shift_on F (le_refl 1) hF n hn0, ← psiOf_sqrt_rel]
```
New:
```
have vF : deriv (deriv (mFblock F)) n =
(-4) * (1.5 ^ 2 * psiOf F (1.5 * Real.sqrt n + 1) / (4 * n)) := by
unfold mFblock
rw [deriv2_const_mul (-4) (hdd hCDFc) (hev hCDFc),
chain_rule_sqrt_kshift_on F (by norm_num : (0:ℝ) < 1.5) (le_refl 1) hF n hn0,
← psiOf_sqrt_krel]
```
Wait — the chain_rule_sqrt_kshift_on outputs `(k ^ 2) * (deriv (deriv φ) T − deriv φ T/(k√n)) / (4 * n)`. After ← psiOf_sqrt_krel: `(1.5 ^ 2) * (psiOf F T) / (4 * n)` — parses as ((1.5^2)·psiOf)/(4n). My vF statement says `1.5 ^ 2 * psiOf F (1.5*√n+1) / (4*n)` — same form ✓ (a * b / c = (a*b)/c ✓).
The rw: `chain_rule_sqrt_kshift_on F h01 hc hF n hn0` rewrites `deriv (deriv fun n => F (1.5·√n+1)) n` — but the goal after `unfold mFblock; rw [deriv2_const_mul ...]` is `(−4) * deriv (deriv fun m => F (1.5·√m+1)) n = ...` — the chain rule rewrites the deriv (deriv (fun n => F (1.5√n+1))) n ✓. Then ← psiOf_sqrt_krel rewrites `deriv (deriv F) T − deriv F T/(1.5√n)` → psiOf F T ✓.
For the other v-blocks: same pattern with contDiffOn_TL1 etc. Note: the blocks' old rw used `chain_rule_sqrt_shift_on _ (by norm_num : (-1:ℝ) ≤ 1) contDiffOn_TL1 n hn0` — new: `chain_rule_sqrt_kshift_on _ (by norm_num : (0:ℝ) < 1.5) (by norm_num : (-1:ℝ) ≤ 1) contDiffOn_TL1 n hn0`.
vIIM:
```
have vIIM : deriv (deriv mIIM) n = (-1.5) * deriv (deriv IIMaj) n := by
unfold mIIM
rw [deriv2_const_mul (-1.5) (hdd hCDIIM) (hev hCDIIM)]
```
Sign assembly hnn1–hnn9: current forms e.g.:
```
have hnn2 : (0 : ℝ) ≤ (-((8/3)*0.6 + 42)) *
(psiOf (fun t => t * Real.log (t + 2)) (Real.sqrt n + 1) / (4 * n)) :=
mul_nonneg_of_nonpos_of_nonpos (by norm_num)
(div_neg_of_neg_of_pos (psiOf_T_mul_log_shift_neg hTn) hn4).le
```
New form: (−w)·(1.5^2·psiOf φ T/(4n)) ≥ 0:
```
have hnn2 : (0 : ℝ) ≤ (-((8/3)*0.6 + 42)) *
(1.5 ^ 2 * psiOf (fun t => t * Real.log (t + 2)) (1.5 * Real.sqrt n + 1) / (4 * n)) := by
have hneg : (1.5 : ℝ) ^ 2 * psiOf (fun t => t * Real.log (t + 2)) (1.5 * Real.sqrt n + 1) /
(4 * n) < 0 :=
mul_neg_of_pos_of_neg (by norm_num)
(div_neg_of_neg_of_pos (psiOf_T_mul_log_shift_neg hTn) hn4)
exact mul_nonneg_of_nonpos_of_nonpos (by norm_num) hneg.le
```
mul_neg_of_pos_of_neg : 0 < a → b < 0 → a * b < 0 ✓ — form a·b: `1.5^2 * (psiOf/(4n))` — the expression `1.5^2 * psiOf ... / (4*n)` parses as `(1.5^2 * psiOf ...)/(4*n)` — hmm — a*b/c = (a*b)/c ✓ so the mul_neg applies to (1.5^2)·(psiOf/(4n))?? NO: `1.5^2 * psiOf X / (4 * n)` = `(1.5^2 * psiOf X) / (4*n)` — division at the OUTSIDE. mul_neg_of_pos_of_neg proves `a * b < 0` — to use on `(1.5^2 * psiOf X)/(4n)` = `(1.5^2 * psiOf X) * (4*n)⁻¹`... division is multiplication by inverse: `(1.5^2 * psiOf X)/(4n)` — the whole thing is neg since numerator < 0 and denominator > 0: use `div_neg_of_neg_of_pos`: needs `1.5^2 * psiOf X < 0` and `0 < 4n`:
```
have hneg1 : (1.5 : ℝ) ^ 2 * psiOf (fun t => t * Real.log (t + 2)) (1.5 * Real.sqrt n + 1) < 0 :=
mul_neg_of_pos_of_neg (by norm_num) (psiOf_T_mul_log_shift_neg hTn)
have hneg : (1.5 : ℝ) ^ 2 * psiOf (fun t => t * Real.log (t + 2)) (1.5 * Real.sqrt n + 1) /
(4 * n) < 0 := div_neg_of_neg_of_pos hneg1 hn4
exact mul_nonneg_of_nonpos_of_nonpos (by norm_num) hneg.le
```
✓ cleaner. For the (Real.exp (16/9)+1)-containing coefficients the (−w ≤ 0) side uses nlinarith [Real.exp_pos (16/9)] as the old ones did with Real.exp_pos 4.
The final:
```
have hIIM := IIMaj_deriv2_lt_three (show 20 ≤ n by linarith)
have hbridge : (1.5 : ℝ) * (1 / (3 * n)) = 1 / (2 * n) := by
field_simp [hn0.ne']
linarith [hIIM, hbridge, hnn1, hnn2, hnn3, hnn4, hnn5, hnn6, hnn7, hnn8, hnn9]
```
Wait — the goal after the rw chain: `0 ≤ 1/(2*n) + (−4)·(1.5²ψ_F/(4n)) + ... + (−1.5)·IIMaj″` (sum in the left-nested order + mK = 0). linarith needs: 1/(2n) + (−1.5)·IIMaj″ > 0: from hIIM : IIMaj″ < 1/(3n): 1.5·IIMaj″ < 1.5·(1/(3n)) = 1/(2n) via hbridge ✓ linarith can multiply hIIM by 1.5 (positive rational) ✓ and use hbridge as an equation ✓.
But CAREFUL: does the goal's `1/(2*n)` atom match hbridge's RHS `1/(2*n)`? The vS value is `1/(2*n)` ✓ same syntactic form ✓.
Also `field_simp [hn0.ne']` for hbridge: 1.5·(1/(3n)) = 1/(2n) ⟺ 1.5·(2n) = 3n ⟺ 3n = 3n ✓ field_simp should close; if not, add `ring` fallback... field_simp clears denominators then needs ring or closes by itself — old proofs used `field_simp [hn0.ne']; ring` pattern... The e in IIMaj_deriv2_lt_three used field_simp + ring. For hbridge: `field_simp [hn0.ne']` may leave `1.5 * (2 * n) = 3 * n` — add ring... Let me write `by field_simp [hn0.ne']` and if it fails, ring. Actually to be safe:
```
have hbridge : (1.5 : ℝ) * (1 / (3 * n)) = 1 / (2 * n) := by
field_simp [hn0.ne']
```
field_simp's normal form might close it (it proved 1/(2n) = 2/(4n) earlier without ring... that one had `field_simp [hn0.ne']; ring`? The old e at IIMaj_deriv2_lt: `field_simp [hn0.ne']; ring` — two steps. And earlier at 2153: `have e : (1 : ℝ) / (2 * n) = 2 / (4 * n) := by field_simp [hn0.ne']; ring` — wait no, looking at the old IIMaj_deriv2_lt:
```
have e : (1 : ℝ) / (2 * n) = 2 / (4 * n) := by
field_simp [hn0.ne']
ring
```
So field_simp alone didn't close; ring after. I'll use the same two-liner for hbridge (harmless if field_simp closes it — ring then errors "no goals"... hmm, that WOULD error. The old proofs used both, meaning field_simp didn't close there. Use both; if field_simp closes, ring errors — risk. Alternative: `by field_simp [hn0.ne']; ring_nf` — same issue. Use `by rw [div_eq_div_iff ...]`? Simplest robust:
```
have hbridge : (1.5 : ℝ) * (1 / (3 * n)) = 1 / (2 * n) := by
have hn3 : (0 : ℝ) < 3 * n := by linarith
have hn2 : (0 : ℝ) < 2 * n := by linarith
rw [div_eq_div_iff hn3.ne' hn2.ne']
ring
```
div_eq_div_iff : a/b = c/d ↔ a*d = c*b (needs b≠0, d≠0) — here form is 1.5·(1/(3n)) = 1/(2n) — LHS is 1.5·(1/(3n)) not a/b... after rw one_div: 1.5·(3n)⁻¹... hmm messy. Cleaner: prove `1/(2*n) = 1.5*(1/(3*n))` direction... Actually simplest: just compute: 1.5·(1/(3n)) = 1.5/(3n) = 1/(2n):
```
have hbridge : (1.5 : ℝ) * (1 / (3 * n)) = 1 / (2 * n) := by
field_simp [hn0.ne']
```
and test — field_simp [hn0.ne'] on goal `1.5 * (1/(3*n)) = 1/(2*n)`: it multiplies out: 1.5·(2n) = 1·(3n)?? → 3n = 3n → closes by rfl/ring-like finish internally? Mathlib's field_simp usually finishes with `ring1` attempt — often closes such goals alone (session-033 banked: "field_simp can close the goal"). I'll write `field_simp [hn0.ne']` alone; if the build complains I'll adjust.
Now also don't forget: the hnn4 (psiOf id) and hnn8/hnn9 (psiOf_log_shift_neg / psiOf_log_log_shift_neg with `1 < T` derived inline) — adapt T to 1.5√n+1: psiOf_id (1.5√n+1) (by have h := Real.sqrt_pos.mpr hn0; linarith [mul_pos (by norm_num : (0:ℝ)<1.5) h]) — actually 1 < 1.5√n+1 ⟸ 0 < 1.5√n ✓ linarith with mul_pos. psiOf_log_shift_neg takes hT : 1 < T directly ✓ same.
Also the hTn-dependent ψ-neg lemmas (psiOf_log_sq_shift_neg etc. take hT : √20+1 ≤ T) — hTn now gives √20+1 ≤ 1.5√n+1 ✓ direct fit.
Now write the convexity edit. The section from `have hCDFc` to the final linarith — I'll replace carefully. The current text is at what was lines 2202–2389 (now shifted by my inserts: +~46 (bracket/IIMaj doc) + ~58 (k-shift) + ~90 (chain rule) — but content matching handles it).
Let me construct the replacement text for the whole region from `have hCDFc` to `linarith [hIIM, hnn1, ...]`. I have the current text from my earlier reads (2100–2300 + 2299–2389). Let me write the edits as two big chunks: chunk 1 (hTn + composition bundles + v-blocks), chunk 2 (the hnn* + final).
Chunk 1 old text (from the read at 2189–2293):
- hTn
- hdd/hev helpers (UNCHANGED)
- hCDFc ... hCDIIM bundles
- vS ... vIIM
The hdd/hev helpers don't reference the shift — keep. hCDIIM (IIMaj) unchanged.
Let me write chunk 1's old_string from `have hTn : Real.sqrt 20 + 1 ≤ Real.sqrt n + 1 := by` through the vIIM block, replacing with the new versions. That's a big edit but safer as one chunk to avoid partial mismatches.
Now the `marginTilde_convex` re-proof — the biggest edit. Replacing the composition bundles and v-block computations with the k-shifted forms.
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean",
"old_string": " have hTn : Real.sqrt 20 + 1 \u2264 Real.sqrt n + 1 := by\n have h := Real.sqrt_le_sqrt (show (20 : \u211d) \u2264 n by linarith)\n linarith\n -- diff-fact helpers\n have hdd : \u2200 {P : \u211d \u2192 \u211d}, ContDiffOn \u211d 2 P (Set.Ioi 20) \u2192\n DifferentiableAt \u211d (deriv P) n := fun hCD =>\n ((hCD.deriv_of_isOpen (m := 1) isOpen_Ioi (by norm_num)).differentiableOn\n one_ne_zero).differentiableAt (Ioi_mem_nhds hn20)\n have hev : \u2200 {P : \u211d \u2192 \u211d}, ContDiffOn \u211d 2 P (Set.Ioi 20) \u2192\n (\u2200\u1da0 m in \ud835\udcdd n, DifferentiableAt \u211d P m) := fun hCD => by\n filter_upwards [Ioi_mem_nhds hn20] with m hm\n exact (hCD.differentiableOn (by norm_num)).differentiableAt (Ioi_mem_nhds hm)\n -- unweighted composition bundles\n have hCDFc : ContDiffOn \u211d 2 (fun m => F (Real.sqrt m + 1)) (Set.Ioi 20) :=\n hF.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift_Ioi1\n have hCDTL1c : ContDiffOn \u211d 2\n (fun m => (fun t => t * Real.log (t + 2)) (Real.sqrt m + 1)) (Set.Ioi 20) :=\n contDiffOn_TL1.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift\n have hCDTL2c : ContDiffOn \u211d 2\n (fun m => (fun t => t * Real.log (Real.log (t + 2))) (Real.sqrt m + 1))\n (Set.Ioi 20) :=\n contDiffOn_TL2.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift\n have hCDL1sqc : ContDiffOn \u211d 2\n (fun m => (fun t => Real.log (t + 2) ^ 2) (Real.sqrt m + 1)) (Set.Ioi 20) :=\n contDiffOn_L1sq.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift\n have hCDL1L2c : ContDiffOn \u211d 2\n (fun m => (fun t => Real.log (t + 2) * Real.log (Real.log (t + 2)))\n (Real.sqrt m + 1)) (Set.Ioi 20) :=\n contDiffOn_L1L2.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift\n have hCDL2sqc : ContDiffOn \u211d 2\n (fun m => (fun t => Real.log (Real.log (t + 2)) ^ 2) (Real.sqrt m + 1))\n (Set.Ioi 20) :=\n contDiffOn_L2sq.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift\n have hCDL1c : ContDiffOn \u211d 2\n (fun m => (fun t => Real.log (t + 2)) (Real.sqrt m + 1)) (Set.Ioi 20) :=\n contDiffOn_L1.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift\n have hCDL2c : ContDiffOn \u211d 2\n (fun m => (fun t => Real.log (Real.log (t + 2))) (Real.sqrt m + 1))\n (Set.Ioi 20) :=\n contDiffOn_L2.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift\n have hCDIIM : ContDiffOn \u211d 2 IIMaj (Set.Ioi 20) := by\n have hId : IIMaj = fun m => psiTilde (Real.sqrt m) :=\n funext fun m => IIMaj_eq_psiTilde_sqrt m\n rw [hId]\n exact (psiTilde_contDiff.contDiffOn).comp\n (contDiffOn_id.sqrt (fun x hx => by\n have h : 20 < x := hx\n exact ne_of_gt (by linarith : (0 : \u211d) < x))) (Set.mapsTo_univ _ _)\n -- piece values\n have vS : deriv (deriv fun m => (1/2)*m*Real.log m +\n (lagariasC1 - Real.eulerMascheroniConstant/2)*m - 4) n = 1/(2*n) :=\n marginS_deriv2 _ hn0\n have vF : deriv (deriv (mFblock F)) n =\n (-4) * (psiOf F (Real.sqrt n + 1) / (4 * n)) := by\n unfold mFblock\n rw [deriv2_const_mul (-4) (hdd hCDFc) (hev hCDFc),\n chain_rule_sqrt_shift_on F (le_refl 1) hF n hn0, \u2190 psiOf_sqrt_rel]\n have vTL1 : deriv (deriv mTL1b) n = (-((8/3)*0.6 + 42)) *\n (psiOf (fun t => t * Real.log (t + 2)) (Real.sqrt n + 1) / (4 * n)) := by\n unfold mTL1b\n rw [deriv2_const_mul _ (hdd hCDTL1c) (hev hCDTL1c),\n chain_rule_sqrt_shift_on _ (by norm_num : (-1 : \u211d) \u2264 1) contDiffOn_TL1 n hn0, \u2190 psiOf_sqrt_rel]\n have vTL2 : deriv (deriv mTL2b) n = (-((8/3)*0.886)) *\n (psiOf (fun t => t * Real.log (Real.log (t + 2))) (Real.sqrt n + 1) / (4 * n)) := by\n unfold mTL2b\n rw [deriv2_const_mul _ (hdd hCDTL2c) (hev hCDTL2c),\n chain_rule_sqrt_shift_on _ (by norm_num : (-1 : \u211d) \u2264 1) contDiffOn_TL2 n hn0, \u2190 psiOf_sqrt_rel]\n have vId : deriv (deriv mIdb) n = (-((8/3)*2.7 + 192)) *\n (psiOf id (Real.sqrt n + 1) / (4 * n)) := by\n unfold mIdb\n have hCDidc : ContDiffOn \u211d 2 (fun m => id (Real.sqrt m + 1)) (Set.Ioi 20) :=\n contDiffOn_id.comp contDiffOn_sqrt_shift (Set.mapsTo_univ _ _)\n rw [show (fun m => -(8/3*2.7 + 192) * (Real.sqrt m + 1)) =\n (fun m => -(8/3*2.7 + 192) * id (Real.sqrt m + 1)) from rfl,\n deriv2_const_mul _ (hdd hCDidc) (hev hCDidc),\n chain_rule_sqrt_shift_on _ (by norm_num : (-1 : \u211d) \u2264 1) contDiffOn_id n hn0, \u2190 psiOf_sqrt_rel]\n have vL1sq : deriv (deriv mL1sqb) n = (-(42*0.433^2*(Real.exp 4 + 1))) *\n (psiOf (fun t => Real.log (t + 2) ^ 2) (Real.sqrt n + 1) / (4 * n)) := by\n unfold mL1sqb\n rw [deriv2_const_mul _ (hdd hCDL1sqc) (hev hCDL1sqc),\n chain_rule_sqrt_shift_on _ (by norm_num : (-1 : \u211d) \u2264 1) contDiffOn_L1sq n hn0, \u2190 psiOf_sqrt_rel]\n have vL1L2 : deriv (deriv mL1L2b) n = (-(42*(2*0.433*0.886)*(Real.exp 4 + 1))) *\n (psiOf (fun t => Real.log (t + 2) * Real.log (Real.log (t + 2)))\n (Real.sqrt n + 1) / (4 * n)) := by\n unfold mL1L2b\n rw [deriv2_const_mul _ (hdd hCDL1L2c) (hev hCDL1L2c),\n chain_rule_sqrt_shift_on _ (by norm_num : (-1 : \u211d) \u2264 1) contDiffOn_L1L2 n hn0, \u2190 psiOf_sqrt_rel]\n have vL2sq : deriv (deriv mL2sqb) n = (-(42*0.886^2*(Real.exp 4 + 1))) *\n (psiOf (fun t => Real.log (Real.log (t + 2)) ^ 2) (Real.sqrt n + 1) / (4 * n)) := by\n unfold mL2sqb\n rw [deriv2_const_mul _ (hdd hCDL2sqc) (hev hCDL2sqc),\n chain_rule_sqrt_shift_on _ (by norm_num : (-1 : \u211d) \u2264 1) contDiffOn_L2sq n hn0, \u2190 psiOf_sqrt_rel]\n have vL1 : deriv (deriv mL1b) n = (-((42*(2*0.433*2.9) + 147)*(Real.exp 4 + 1))) *\n (psiOf (fun t => Real.log (t + 2)) (Real.sqrt n + 1) / (4 * n)) := by\n unfold mL1b\n rw [deriv2_const_mul _ (hdd hCDL1c) (hev hCDL1c),\n chain_rule_sqrt_shift_on _ (by norm_num : (-1 : \u211d) \u2264 1) contDiffOn_L1 n hn0, \u2190 psiOf_sqrt_rel]\n have vL2 : deriv (deriv mL2b) n = (-(42*(2*0.886*2.9)*(Real.exp 4 + 1))) *\n (psiOf (fun t => Real.log (Real.log (t + 2))) (Real.sqrt n + 1) / (4 * n)) := by\n unfold mL2b\n rw [deriv2_const_mul _ (hdd hCDL2c) (hev hCDL2c),\n chain_rule_sqrt_shift_on _ (by norm_num : (-1 : \u211d) \u2264 1) contDiffOn_L2 n hn0, \u2190 psiOf_sqrt_rel]\n have vIIM : deriv (deriv mIIM) n = (-1) * deriv (deriv IIMaj) n := by\n unfold mIIM\n rw [deriv2_const_mul (-1) (hdd hCDIIM) (hev hCDIIM)]",
"new_string": " have hTn : Real.sqrt 20 + 1 \u2264 1.5 * Real.sqrt n + 1 := by\n have h := Real.sqrt_le_sqrt (show (20 : \u211d) \u2264 n by linarith)\n have hnn := Real.sqrt_nonneg n\n linarith\n -- diff-fact helpers\n have hdd : \u2200 {P : \u211d \u2192 \u211d}, ContDiffOn \u211d 2 P (Set.Ioi 20) \u2192\n DifferentiableAt \u211d (deriv P) n := fun hCD =>\n ((hCD.deriv_of_isOpen (m := 1) isOpen_Ioi (by norm_num)).differentiableOn\n one_ne_zero).differentiableAt (Ioi_mem_nhds hn20)\n have hev : \u2200 {P : \u211d \u2192 \u211d}, ContDiffOn \u211d 2 P (Set.Ioi 20) \u2192\n (\u2200\u1da0 m in \ud835\udcdd n, DifferentiableAt \u211d P m) := fun hCD => by\n filter_upwards [Ioi_mem_nhds hn20] with m hm\n exact (hCD.differentiableOn (by norm_num)).differentiableAt (Ioi_mem_nhds hm)\n -- unweighted composition bundles (the c = 1.5 k-shift, D-073)\n have hk15 : (0 : \u211d) < 1.5 := by norm_num\n have hCDFc : ContDiffOn \u211d 2 (fun m => F (1.5 * Real.sqrt m + 1)) (Set.Ioi 20) :=\n hF.comp (contDiffOn_ksqrt_shift 1.5 hk15) (mapsTo_ksqrt_shift_Ioi1 1.5 hk15)\n have hCDTL1c : ContDiffOn \u211d 2\n (fun m => (fun t => t * Real.log (t + 2)) (1.5 * Real.sqrt m + 1)) (Set.Ioi 20) :=\n contDiffOn_TL1.comp (contDiffOn_ksqrt_shift 1.5 hk15) (mapsTo_ksqrt_shift 1.5 hk15)\n have hCDTL2c : ContDiffOn \u211d 2\n (fun m => (fun t => t * Real.log (Real.log (t + 2))) (1.5 * Real.sqrt m + 1))\n (Set.Ioi 20) :=\n contDiffOn_TL2.comp (contDiffOn_ksqrt_shift 1.5 hk15) (mapsTo_ksqrt_shift 1.5 hk15)\n have hCDL1sqc : ContDiffOn \u211d 2\n (fun m => (fun t => Real.log (t + 2) ^ 2) (1.5 * Real.sqrt m + 1)) (Set.Ioi 20) :=\n contDiffOn_L1sq.comp (contDiffOn_ksqrt_shift 1.5 hk15) (mapsTo_ksqrt_shift 1.5 hk15)\n have hCDL1L2c : ContDiffOn \u211d 2\n (fun m => (fun t => Real.log (t + 2) * Real.log (Real.log (t + 2)))\n (1.5 * Real.sqrt m + 1)) (Set.Ioi 20) :=\n contDiffOn_L1L2.comp (contDiffOn_ksqrt_shift 1.5 hk15) (mapsTo_ksqrt_shift 1.5 hk15)\n have hCDL2sqc : ContDiffOn \u211d 2\n (fun m => (fun t => Real.log (Real.log (t + 2)) ^ 2) (1.5 * Real.sqrt m + 1))\n (Set.Ioi 20) :=\n contDiffOn_L2sq.comp (contDiffOn_ksqrt_shift 1.5 hk15) (mapsTo_ksqrt_shift 1.5 hk15)\n have hCDL1c : ContDiffOn \u211d 2\n (fun m => (fun t => Real.log (t + 2)) (1.5 * Real.sqrt m + 1)) (Set.Ioi 20) :=\n contDiffOn_L1.comp (contDiffOn_ksqrt_shift 1.5 hk15) (mapsTo_ksqrt_shift 1.5 hk15)\n have hCDL2c : ContDiffOn \u211d 2\n (fun m => (fun t => Real.log (Real.log (t + 2))) (1.5 * Real.sqrt m + 1))\n (Set.Ioi 20) :=\n contDiffOn_L2.comp (contDiffOn_ksqrt_shift 1.5 hk15) (mapsTo_ksqrt_shift 1.5 hk15)\n have hCDIIM : ContDiffOn \u211d 2 IIMaj (Set.Ioi 20) := by\n have hId : IIMaj = fun m => psiTilde (Real.sqrt m) :=\n funext fun m => IIMaj_eq_psiTilde_sqrt m\n rw [hId]\n exact (psiTilde_contDiff.contDiffOn).comp\n (contDiffOn_id.sqrt (fun x hx => by\n have h : 20 < x := hx\n exact ne_of_gt (by linarith : (0 : \u211d) < x))) (Set.mapsTo_univ _ _)\n -- piece values\n have vS : deriv (deriv fun m => (1/2)*m*Real.log m +\n (lagariasC1 - Real.eulerMascheroniConstant/2)*m - 4) n = 1/(2*n) :=\n marginS_deriv2 _ hn0\n have vF : deriv (deriv (mFblock F)) n =\n (-4) * (1.5 ^ 2 * psiOf F (1.5 * Real.sqrt n + 1) / (4 * n)) := by\n unfold mFblock\n rw [deriv2_const_mul (-4) (hdd hCDFc) (hev hCDFc),\n chain_rule_sqrt_kshift_on F hk15 (le_refl 1) hF n hn0, \u2190 psiOf_sqrt_krel]\n have vTL1 : deriv (deriv mTL1b) n = (-((8/3)*0.6 + 42)) *\n (1.5 ^ 2 * psiOf (fun t => t * Real.log (t + 2)) (1.5 * Real.sqrt n + 1) / (4 * n)) := by\n unfold mTL1b\n rw [deriv2_const_mul _ (hdd hCDTL1c) (hev hCDTL1c),\n chain_rule_sqrt_kshift_on _ hk15 (by norm_num : (-1 : \u211d) \u2264 1) contDiffOn_TL1 n hn0,\n \u2190 psiOf_sqrt_krel]\n have vTL2 : deriv (deriv mTL2b) n = (-((8/3)*0.886)) *\n (1.5 ^ 2 * psiOf (fun t => t * Real.log (Real.log (t + 2))) (1.5 * Real.sqrt n + 1) /\n (4 * n)) := by\n unfold mTL2b\n rw [deriv2_const_mul _ (hdd hCDTL2c) (hev hCDTL2c),\n chain_rule_sqrt_kshift_on _ hk15 (by norm_num : (-1 : \u211d) \u2264 1) contDiffOn_TL2 n hn0,\n \u2190 psiOf_sqrt_krel]\n have vId : deriv (deriv mIdb) n = (-((8/3)*2.7 + 192)) *\n (1.5 ^ 2 * psiOf id (1.5 * Real.sqrt n + 1) / (4 * n)) := by\n unfold mIdb\n have hCDidc : ContDiffOn \u211d 2 (fun m => id (1.5 * Real.sqrt m + 1)) (Set.Ioi 20) :=\n contDiffOn_id.comp (contDiffOn_ksqrt_shift 1.5 hk15) (Set.mapsTo_univ _ _)\n rw [show (fun m => -(8/3*2.7 + 192) * (1.5 * Real.sqrt m + 1)) =\n (fun m => -(8/3*2.7 + 192) * id (1.5 * Real.sqrt m + 1)) from rfl,\n deriv2_const_mul _ (hdd hCDidc) (hev hCDidc),\n chain_rule_sqrt_kshift_on _ hk15 (by norm_num : (-1 : \u211d) \u2264 1) contDiffOn_id n hn0,\n \u2190 psiOf_sqrt_krel]\n have vL1sq : deriv (deriv mL1sqb) n = (-(42*0.433^2*(Real.exp (16/9) + 1))) *\n (1.5 ^ 2 * psiOf (fun t => Real.log (t + 2) ^ 2) (1.5 * Real.sqrt n + 1) / (4 * n)) := by\n unfold mL1sqb\n rw [deriv2_const_mul _ (hdd hCDL1sqc) (hev hCDL1sqc),\n chain_rule_sqrt_kshift_on _ hk15 (by norm_num : (-1 : \u211d) \u2264 1) contDiffOn_L1sq n hn0,\n \u2190 psiOf_sqrt_krel]\n have vL1L2 : deriv (deriv mL1L2b) n = (-(42*(2*0.433*0.886)*(Real.exp (16/9) + 1))) *\n (1.5 ^ 2 * psiOf (fun t => Real.log (t + 2) * Real.log (Real.log (t + 2)))\n (1.5 * Real.sqrt n + 1) / (4 * n)) := by\n unfold mL1L2b\n rw [deriv2_const_mul _ (hdd hCDL1L2c) (hev hCDL1L2c),\n chain_rule_sqrt_kshift_on _ hk15 (by norm_num : (-1 : \u211d) \u2264 1) contDiffOn_L1L2 n hn0,\n \u2190 psiOf_sqrt_krel]\n have vL2sq : deriv (deriv mL2sqb) n = (-(42*0.886^2*(Real.exp (16/9) + 1))) *\n (1.5 ^ 2 * psiOf (fun t => Real.log (Real.log (t + 2)) ^ 2) (1.5 * Real.sqrt n + 1) /\n (4 * n)) := by\n unfold mL2sqb\n rw [deriv2_const_mul _ (hdd hCDL2sqc) (hev hCDL2sqc),\n chain_rule_sqrt_kshift_on _ hk15 (by norm_num : (-1 : \u211d) \u2264 1) contDiffOn_L2sq n hn0,\n \u2190 psiOf_sqrt_krel]\n have vL1 : deriv (deriv mL1b) n = (-((42*(2*0.433*2.9) + 147)*(Real.exp (16/9) + 1))) *\n (1.5 ^ 2 * psiOf (fun t => Real.log (t + 2)) (1.5 * Real.sqrt n + 1) / (4 * n)) := by\n unfold mL1b\n rw [deriv2_const_mul _ (hdd hCDL1c) (hev hCDL1c),\n chain_rule_sqrt_kshift_on _ hk15 (by norm_num : (-1 : \u211d) \u2264 1) contDiffOn_L1 n hn0,\n \u2190 psiOf_sqrt_krel]\n have vL2 : deriv (deriv mL2b) n = (-(42*(2*0.886*2.9)*(Real.exp (16/9) + 1))) *\n (1.5 ^ 2 * psiOf (fun t => Real.log (Real.log (t + 2))) (1.5 * Real.sqrt n + 1) /\n (4 * n)) := by\n unfold mL2b\n rw [deriv2_const_mul _ (hdd hCDL2c) (hev hCDL2c),\n chain_rule_sqrt_kshift_on _ hk15 (by norm_num : (-1 : \u211d) \u2264 1) contDiffOn_L2 n hn0,\n \u2190 psiOf_sqrt_krel]\n have vIIM : deriv (deriv mIIM) n = (-1.5) * deriv (deriv IIMaj) n := by\n unfold mIIM\n rw [deriv2_const_mul (-1.5) (hdd hCDIIM) (hev hCDIIM)]"
}
raw content_json (database row)
[{"type":"thinking","thinking":"Now the big one: marginTilde_convex. The pieces to change:\n\n1. hTn: `Real.sqrt 20 + 1 ≤ Real.sqrt n + 1` → `Real.sqrt 20 + 1 ≤ 1.5 * Real.sqrt n + 1`.\n2. Composition bundles hCDFc, hCDTL1c, hCDTL2c, hCDL1sqc, hCDL1L2c, hCDL2sqc, hCDL1c, hCDL2c: inner fun → 1.5·√m+1 with the k-lemmas.\n3. vF, vTL1, vTL2, vId, vL1sq, vL1L2, vL2sq, vL1, vL2: use chain_rule_sqrt_kshift_on + ← psiOf_sqrt_krel; values get the 1.5² factor.\n4. vIIM: (−1.5)·IIMaj″.\n5. hnn1–hnn9: adapt with 1.5².\n6. hIIM → IIMaj_deriv2_lt_three; final linarith with the reciprocal bridge.\n\nLet me write the whole replacement for the v-block section and the sign-assembly section. The current text (with shifted line numbers) — I need to replace from `have hCDFc` through the final linarith. Let me do it in two edits: (a) the composition bundles + hTn + v-blocks; (b) the hnn* + final linarith.\n\nFor (a), the current text:\n\n```\n have hTn : Real.sqrt 20 + 1 ≤ Real.sqrt n + 1 := by\n have h := Real.sqrt_le_sqrt (show (20 : ℝ) ≤ n by linarith)\n linarith\n```\nNew:\n```\n have hTn : Real.sqrt 20 + 1 ≤ 1.5 * Real.sqrt n + 1 := by\n have h := Real.sqrt_le_sqrt (show (20 : ℝ) ≤ n by linarith)\n have hnn := Real.sqrt_nonneg n\n linarith\n```\n\nComposition bundles — current:\n```\n have hCDFc : ContDiffOn ℝ 2 (fun m => F (Real.sqrt m + 1)) (Set.Ioi 20) :=\n hF.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift_Ioi1\n have hCDTL1c : ContDiffOn ℝ 2\n (fun m => (fun t => t * Real.log (t + 2)) (Real.sqrt m + 1)) (Set.Ioi 20) :=\n contDiffOn_TL1.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift\n ...\n```\nNew: inner fun 1.5·√m+1, k-lemmas.\n\nvF current:\n```\n have vF : deriv (deriv (mFblock F)) n =\n (-4) * (psiOf F (Real.sqrt n + 1) / (4 * n)) := by\n unfold mFblock\n rw [deriv2_const_mul (-4) (hdd hCDFc) (hev hCDFc),\n chain_rule_sqrt_shift_on F (le_refl 1) hF n hn0, ← psiOf_sqrt_rel]\n```\nNew:\n```\n have vF : deriv (deriv (mFblock F)) n =\n (-4) * (1.5 ^ 2 * psiOf F (1.5 * Real.sqrt n + 1) / (4 * n)) := by\n unfold mFblock\n rw [deriv2_const_mul (-4) (hdd hCDFc) (hev hCDFc),\n chain_rule_sqrt_kshift_on F (by norm_num : (0:ℝ) < 1.5) (le_refl 1) hF n hn0,\n ← psiOf_sqrt_krel]\n```\nWait — the chain_rule_sqrt_kshift_on outputs `(k ^ 2) * (deriv (deriv φ) T − deriv φ T/(k√n)) / (4 * n)`. After ← psiOf_sqrt_krel: `(1.5 ^ 2) * (psiOf F T) / (4 * n)` — parses as ((1.5^2)·psiOf)/(4n). My vF statement says `1.5 ^ 2 * psiOf F (1.5*√n+1) / (4*n)` — same form ✓ (a * b / c = (a*b)/c ✓).\n\nThe rw: `chain_rule_sqrt_kshift_on F h01 hc hF n hn0` rewrites `deriv (deriv fun n => F (1.5·√n+1)) n` — but the goal after `unfold mFblock; rw [deriv2_const_mul ...]` is `(−4) * deriv (deriv fun m => F (1.5·√m+1)) n = ...` — the chain rule rewrites the deriv (deriv (fun n => F (1.5√n+1))) n ✓. Then ← psiOf_sqrt_krel rewrites `deriv (deriv F) T − deriv F T/(1.5√n)` → psiOf F T ✓.\n\nFor the other v-blocks: same pattern with contDiffOn_TL1 etc. Note: the blocks' old rw used `chain_rule_sqrt_shift_on _ (by norm_num : (-1:ℝ) ≤ 1) contDiffOn_TL1 n hn0` — new: `chain_rule_sqrt_kshift_on _ (by norm_num : (0:ℝ) < 1.5) (by norm_num : (-1:ℝ) ≤ 1) contDiffOn_TL1 n hn0`.\n\nvIIM:\n```\n have vIIM : deriv (deriv mIIM) n = (-1.5) * deriv (deriv IIMaj) n := by\n unfold mIIM\n rw [deriv2_const_mul (-1.5) (hdd hCDIIM) (hev hCDIIM)]\n```\n\nSign assembly hnn1–hnn9: current forms e.g.:\n```\n have hnn2 : (0 : ℝ) ≤ (-((8/3)*0.6 + 42)) *\n (psiOf (fun t => t * Real.log (t + 2)) (Real.sqrt n + 1) / (4 * n)) :=\n mul_nonneg_of_nonpos_of_nonpos (by norm_num)\n (div_neg_of_neg_of_pos (psiOf_T_mul_log_shift_neg hTn) hn4).le\n```\nNew form: (−w)·(1.5^2·psiOf φ T/(4n)) ≥ 0: \n```\n have hnn2 : (0 : ℝ) ≤ (-((8/3)*0.6 + 42)) *\n (1.5 ^ 2 * psiOf (fun t => t * Real.log (t + 2)) (1.5 * Real.sqrt n + 1) / (4 * n)) := by\n have hneg : (1.5 : ℝ) ^ 2 * psiOf (fun t => t * Real.log (t + 2)) (1.5 * Real.sqrt n + 1) /\n (4 * n) < 0 :=\n mul_neg_of_pos_of_neg (by norm_num)\n (div_neg_of_neg_of_pos (psiOf_T_mul_log_shift_neg hTn) hn4)\n exact mul_nonneg_of_nonpos_of_nonpos (by norm_num) hneg.le\n```\nmul_neg_of_pos_of_neg : 0 < a → b < 0 → a * b < 0 ✓ — form a·b: `1.5^2 * (psiOf/(4n))` — the expression `1.5^2 * psiOf ... / (4*n)` parses as `(1.5^2 * psiOf ...)/(4*n)` — hmm — a*b/c = (a*b)/c ✓ so the mul_neg applies to (1.5^2)·(psiOf/(4n))?? NO: `1.5^2 * psiOf X / (4 * n)` = `(1.5^2 * psiOf X) / (4*n)` — division at the OUTSIDE. mul_neg_of_pos_of_neg proves `a * b < 0` — to use on `(1.5^2 * psiOf X)/(4n)` = `(1.5^2 * psiOf X) * (4*n)⁻¹`... division is multiplication by inverse: `(1.5^2 * psiOf X)/(4n)` — the whole thing is neg since numerator < 0 and denominator > 0: use `div_neg_of_neg_of_pos`: needs `1.5^2 * psiOf X < 0` and `0 < 4n`:\n```\n have hneg1 : (1.5 : ℝ) ^ 2 * psiOf (fun t => t * Real.log (t + 2)) (1.5 * Real.sqrt n + 1) < 0 :=\n mul_neg_of_pos_of_neg (by norm_num) (psiOf_T_mul_log_shift_neg hTn)\n have hneg : (1.5 : ℝ) ^ 2 * psiOf (fun t => t * Real.log (t + 2)) (1.5 * Real.sqrt n + 1) /\n (4 * n) < 0 := div_neg_of_neg_of_pos hneg1 hn4\n exact mul_nonneg_of_nonpos_of_nonpos (by norm_num) hneg.le\n```\n✓ cleaner. For the (Real.exp (16/9)+1)-containing coefficients the (−w ≤ 0) side uses nlinarith [Real.exp_pos (16/9)] as the old ones did with Real.exp_pos 4.\n\nThe final:\n```\n have hIIM := IIMaj_deriv2_lt_three (show 20 ≤ n by linarith)\n have hbridge : (1.5 : ℝ) * (1 / (3 * n)) = 1 / (2 * n) := by\n field_simp [hn0.ne']\n linarith [hIIM, hbridge, hnn1, hnn2, hnn3, hnn4, hnn5, hnn6, hnn7, hnn8, hnn9]\n```\nWait — the goal after the rw chain: `0 ≤ 1/(2*n) + (−4)·(1.5²ψ_F/(4n)) + ... + (−1.5)·IIMaj″` (sum in the left-nested order + mK = 0). linarith needs: 1/(2n) + (−1.5)·IIMaj″ > 0: from hIIM : IIMaj″ < 1/(3n): 1.5·IIMaj″ < 1.5·(1/(3n)) = 1/(2n) via hbridge ✓ linarith can multiply hIIM by 1.5 (positive rational) ✓ and use hbridge as an equation ✓. \n\nBut CAREFUL: does the goal's `1/(2*n)` atom match hbridge's RHS `1/(2*n)`? The vS value is `1/(2*n)` ✓ same syntactic form ✓.\n\nAlso `field_simp [hn0.ne']` for hbridge: 1.5·(1/(3n)) = 1/(2n) ⟺ 1.5·(2n) = 3n ⟺ 3n = 3n ✓ field_simp should close; if not, add `ring` fallback... field_simp clears denominators then needs ring or closes by itself — old proofs used `field_simp [hn0.ne']; ring` pattern... The e in IIMaj_deriv2_lt_three used field_simp + ring. For hbridge: `field_simp [hn0.ne']` may leave `1.5 * (2 * n) = 3 * n` — add ring... Let me write `by field_simp [hn0.ne']` and if it fails, ring. Actually to be safe: \n```\n have hbridge : (1.5 : ℝ) * (1 / (3 * n)) = 1 / (2 * n) := by\n field_simp [hn0.ne']\n```\nfield_simp's normal form might close it (it proved 1/(2n) = 2/(4n) earlier without ring... that one had `field_simp [hn0.ne']; ring`? The old e at IIMaj_deriv2_lt: `field_simp [hn0.ne']; ring` — two steps. And earlier at 2153: `have e : (1 : ℝ) / (2 * n) = 2 / (4 * n) := by field_simp [hn0.ne']; ring` — wait no, looking at the old IIMaj_deriv2_lt: \n```\n have e : (1 : ℝ) / (2 * n) = 2 / (4 * n) := by\n field_simp [hn0.ne']\n ring\n```\nSo field_simp alone didn't close; ring after. I'll use the same two-liner for hbridge (harmless if field_simp closes it — ring then errors \"no goals\"... hmm, that WOULD error. The old proofs used both, meaning field_simp didn't close there. Use both; if field_simp closes, ring errors — risk. Alternative: `by field_simp [hn0.ne']; ring_nf` — same issue. Use `by rw [div_eq_div_iff ...]`? Simplest robust: \n```\n have hbridge : (1.5 : ℝ) * (1 / (3 * n)) = 1 / (2 * n) := by\n have hn3 : (0 : ℝ) < 3 * n := by linarith\n have hn2 : (0 : ℝ) < 2 * n := by linarith\n rw [div_eq_div_iff hn3.ne' hn2.ne']\n ring\n```\ndiv_eq_div_iff : a/b = c/d ↔ a*d = c*b (needs b≠0, d≠0) — here form is 1.5·(1/(3n)) = 1/(2n) — LHS is 1.5·(1/(3n)) not a/b... after rw one_div: 1.5·(3n)⁻¹... hmm messy. Cleaner: prove `1/(2*n) = 1.5*(1/(3*n))` direction... Actually simplest: just compute: 1.5·(1/(3n)) = 1.5/(3n) = 1/(2n): \n```\n have hbridge : (1.5 : ℝ) * (1 / (3 * n)) = 1 / (2 * n) := by\n field_simp [hn0.ne']\n```\nand test — field_simp [hn0.ne'] on goal `1.5 * (1/(3*n)) = 1/(2*n)`: it multiplies out: 1.5·(2n) = 1·(3n)?? → 3n = 3n → closes by rfl/ring-like finish internally? Mathlib's field_simp usually finishes with `ring1` attempt — often closes such goals alone (session-033 banked: \"field_simp can close the goal\"). I'll write `field_simp [hn0.ne']` alone; if the build complains I'll adjust.\n\nNow also don't forget: the hnn4 (psiOf id) and hnn8/hnn9 (psiOf_log_shift_neg / psiOf_log_log_shift_neg with `1 < T` derived inline) — adapt T to 1.5√n+1: psiOf_id (1.5√n+1) (by have h := Real.sqrt_pos.mpr hn0; linarith [mul_pos (by norm_num : (0:ℝ)<1.5) h]) — actually 1 < 1.5√n+1 ⟸ 0 < 1.5√n ✓ linarith with mul_pos. psiOf_log_shift_neg takes hT : 1 < T directly ✓ same.\n\nAlso the hTn-dependent ψ-neg lemmas (psiOf_log_sq_shift_neg etc. take hT : √20+1 ≤ T) — hTn now gives √20+1 ≤ 1.5√n+1 ✓ direct fit.\n\nNow write the convexity edit. The section from `have hCDFc` to the final linarith — I'll replace carefully. The current text is at what was lines 2202–2389 (now shifted by my inserts: +~46 (bracket/IIMaj doc) + ~58 (k-shift) + ~90 (chain rule) — but content matching handles it).\n\nLet me construct the replacement text for the whole region from `have hCDFc` to `linarith [hIIM, hnn1, ...]`. I have the current text from my earlier reads (2100–2300 + 2299–2389). Let me write the edits as two big chunks: chunk 1 (hTn + composition bundles + v-blocks), chunk 2 (the hnn* + final).\n\nChunk 1 old text (from the read at 2189–2293):\n- hTn\n- hdd/hev helpers (UNCHANGED)\n- hCDFc ... hCDIIM bundles\n- vS ... vIIM\n\nThe hdd/hev helpers don't reference the shift — keep. hCDIIM (IIMaj) unchanged.\n\nLet me write chunk 1's old_string from `have hTn : Real.sqrt 20 + 1 ≤ Real.sqrt n + 1 := by` through the vIIM block, replacing with the new versions. That's a big edit but safer as one chunk to avoid partial mismatches.","signature":""},{"type":"text","text":"Now the `marginTilde_convex` re-proof — the biggest edit. Replacing the composition bundles and v-block computations with the k-shifted forms."},{"type":"tool_use","id":"Edit_89","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean","old_string":" have hTn : Real.sqrt 20 + 1 ≤ Real.sqrt n + 1 := by\n have h := Real.sqrt_le_sqrt (show (20 : ℝ) ≤ n by linarith)\n linarith\n -- diff-fact helpers\n have hdd : ∀ {P : ℝ → ℝ}, ContDiffOn ℝ 2 P (Set.Ioi 20) →\n DifferentiableAt ℝ (deriv P) n := fun hCD =>\n ((hCD.deriv_of_isOpen (m := 1) isOpen_Ioi (by norm_num)).differentiableOn\n one_ne_zero).differentiableAt (Ioi_mem_nhds hn20)\n have hev : ∀ {P : ℝ → ℝ}, ContDiffOn ℝ 2 P (Set.Ioi 20) →\n (∀ᶠ m in 𝓝 n, DifferentiableAt ℝ P m) := fun hCD => by\n filter_upwards [Ioi_mem_nhds hn20] with m hm\n exact (hCD.differentiableOn (by norm_num)).differentiableAt (Ioi_mem_nhds hm)\n -- unweighted composition bundles\n have hCDFc : ContDiffOn ℝ 2 (fun m => F (Real.sqrt m + 1)) (Set.Ioi 20) :=\n hF.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift_Ioi1\n have hCDTL1c : ContDiffOn ℝ 2\n (fun m => (fun t => t * Real.log (t + 2)) (Real.sqrt m + 1)) (Set.Ioi 20) :=\n contDiffOn_TL1.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift\n have hCDTL2c : ContDiffOn ℝ 2\n (fun m => (fun t => t * Real.log (Real.log (t + 2))) (Real.sqrt m + 1))\n (Set.Ioi 20) :=\n contDiffOn_TL2.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift\n have hCDL1sqc : ContDiffOn ℝ 2\n (fun m => (fun t => Real.log (t + 2) ^ 2) (Real.sqrt m + 1)) (Set.Ioi 20) :=\n contDiffOn_L1sq.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift\n have hCDL1L2c : ContDiffOn ℝ 2\n (fun m => (fun t => Real.log (t + 2) * Real.log (Real.log (t + 2)))\n (Real.sqrt m + 1)) (Set.Ioi 20) :=\n contDiffOn_L1L2.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift\n have hCDL2sqc : ContDiffOn ℝ 2\n (fun m => (fun t => Real.log (Real.log (t + 2)) ^ 2) (Real.sqrt m + 1))\n (Set.Ioi 20) :=\n contDiffOn_L2sq.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift\n have hCDL1c : ContDiffOn ℝ 2\n (fun m => (fun t => Real.log (t + 2)) (Real.sqrt m + 1)) (Set.Ioi 20) :=\n contDiffOn_L1.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift\n have hCDL2c : ContDiffOn ℝ 2\n (fun m => (fun t => Real.log (Real.log (t + 2))) (Real.sqrt m + 1))\n (Set.Ioi 20) :=\n contDiffOn_L2.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift\n have hCDIIM : ContDiffOn ℝ 2 IIMaj (Set.Ioi 20) := by\n have hId : IIMaj = fun m => psiTilde (Real.sqrt m) :=\n funext fun m => IIMaj_eq_psiTilde_sqrt m\n rw [hId]\n exact (psiTilde_contDiff.contDiffOn).comp\n (contDiffOn_id.sqrt (fun x hx => by\n have h : 20 < x := hx\n exact ne_of_gt (by linarith : (0 : ℝ) < x))) (Set.mapsTo_univ _ _)\n -- piece values\n have vS : deriv (deriv fun m => (1/2)*m*Real.log m +\n (lagariasC1 - Real.eulerMascheroniConstant/2)*m - 4) n = 1/(2*n) :=\n marginS_deriv2 _ hn0\n have vF : deriv (deriv (mFblock F)) n =\n (-4) * (psiOf F (Real.sqrt n + 1) / (4 * n)) := by\n unfold mFblock\n rw [deriv2_const_mul (-4) (hdd hCDFc) (hev hCDFc),\n chain_rule_sqrt_shift_on F (le_refl 1) hF n hn0, ← psiOf_sqrt_rel]\n have vTL1 : deriv (deriv mTL1b) n = (-((8/3)*0.6 + 42)) *\n (psiOf (fun t => t * Real.log (t + 2)) (Real.sqrt n + 1) / (4 * n)) := by\n unfold mTL1b\n rw [deriv2_const_mul _ (hdd hCDTL1c) (hev hCDTL1c),\n chain_rule_sqrt_shift_on _ (by norm_num : (-1 : ℝ) ≤ 1) contDiffOn_TL1 n hn0, ← psiOf_sqrt_rel]\n have vTL2 : deriv (deriv mTL2b) n = (-((8/3)*0.886)) *\n (psiOf (fun t => t * Real.log (Real.log (t + 2))) (Real.sqrt n + 1) / (4 * n)) := by\n unfold mTL2b\n rw [deriv2_const_mul _ (hdd hCDTL2c) (hev hCDTL2c),\n chain_rule_sqrt_shift_on _ (by norm_num : (-1 : ℝ) ≤ 1) contDiffOn_TL2 n hn0, ← psiOf_sqrt_rel]\n have vId : deriv (deriv mIdb) n = (-((8/3)*2.7 + 192)) *\n (psiOf id (Real.sqrt n + 1) / (4 * n)) := by\n unfold mIdb\n have hCDidc : ContDiffOn ℝ 2 (fun m => id (Real.sqrt m + 1)) (Set.Ioi 20) :=\n contDiffOn_id.comp contDiffOn_sqrt_shift (Set.mapsTo_univ _ _)\n rw [show (fun m => -(8/3*2.7 + 192) * (Real.sqrt m + 1)) =\n (fun m => -(8/3*2.7 + 192) * id (Real.sqrt m + 1)) from rfl,\n deriv2_const_mul _ (hdd hCDidc) (hev hCDidc),\n chain_rule_sqrt_shift_on _ (by norm_num : (-1 : ℝ) ≤ 1) contDiffOn_id n hn0, ← psiOf_sqrt_rel]\n have vL1sq : deriv (deriv mL1sqb) n = (-(42*0.433^2*(Real.exp 4 + 1))) *\n (psiOf (fun t => Real.log (t + 2) ^ 2) (Real.sqrt n + 1) / (4 * n)) := by\n unfold mL1sqb\n rw [deriv2_const_mul _ (hdd hCDL1sqc) (hev hCDL1sqc),\n chain_rule_sqrt_shift_on _ (by norm_num : (-1 : ℝ) ≤ 1) contDiffOn_L1sq n hn0, ← psiOf_sqrt_rel]\n have vL1L2 : deriv (deriv mL1L2b) n = (-(42*(2*0.433*0.886)*(Real.exp 4 + 1))) *\n (psiOf (fun t => Real.log (t + 2) * Real.log (Real.log (t + 2)))\n (Real.sqrt n + 1) / (4 * n)) := by\n unfold mL1L2b\n rw [deriv2_const_mul _ (hdd hCDL1L2c) (hev hCDL1L2c),\n chain_rule_sqrt_shift_on _ (by norm_num : (-1 : ℝ) ≤ 1) contDiffOn_L1L2 n hn0, ← psiOf_sqrt_rel]\n have vL2sq : deriv (deriv mL2sqb) n = (-(42*0.886^2*(Real.exp 4 + 1))) *\n (psiOf (fun t => Real.log (Real.log (t + 2)) ^ 2) (Real.sqrt n + 1) / (4 * n)) := by\n unfold mL2sqb\n rw [deriv2_const_mul _ (hdd hCDL2sqc) (hev hCDL2sqc),\n chain_rule_sqrt_shift_on _ (by norm_num : (-1 : ℝ) ≤ 1) contDiffOn_L2sq n hn0, ← psiOf_sqrt_rel]\n have vL1 : deriv (deriv mL1b) n = (-((42*(2*0.433*2.9) + 147)*(Real.exp 4 + 1))) *\n (psiOf (fun t => Real.log (t + 2)) (Real.sqrt n + 1) / (4 * n)) := by\n unfold mL1b\n rw [deriv2_const_mul _ (hdd hCDL1c) (hev hCDL1c),\n chain_rule_sqrt_shift_on _ (by norm_num : (-1 : ℝ) ≤ 1) contDiffOn_L1 n hn0, ← psiOf_sqrt_rel]\n have vL2 : deriv (deriv mL2b) n = (-(42*(2*0.886*2.9)*(Real.exp 4 + 1))) *\n (psiOf (fun t => Real.log (Real.log (t + 2))) (Real.sqrt n + 1) / (4 * n)) := by\n unfold mL2b\n rw [deriv2_const_mul _ (hdd hCDL2c) (hev hCDL2c),\n chain_rule_sqrt_shift_on _ (by norm_num : (-1 : ℝ) ≤ 1) contDiffOn_L2 n hn0, ← psiOf_sqrt_rel]\n have vIIM : deriv (deriv mIIM) n = (-1) * deriv (deriv IIMaj) n := by\n unfold mIIM\n rw [deriv2_const_mul (-1) (hdd hCDIIM) (hev hCDIIM)]","new_string":" have hTn : Real.sqrt 20 + 1 ≤ 1.5 * Real.sqrt n + 1 := by\n have h := Real.sqrt_le_sqrt (show (20 : ℝ) ≤ n by linarith)\n have hnn := Real.sqrt_nonneg n\n linarith\n -- diff-fact helpers\n have hdd : ∀ {P : ℝ → ℝ}, ContDiffOn ℝ 2 P (Set.Ioi 20) →\n DifferentiableAt ℝ (deriv P) n := fun hCD =>\n ((hCD.deriv_of_isOpen (m := 1) isOpen_Ioi (by norm_num)).differentiableOn\n one_ne_zero).differentiableAt (Ioi_mem_nhds hn20)\n have hev : ∀ {P : ℝ → ℝ}, ContDiffOn ℝ 2 P (Set.Ioi 20) →\n (∀ᶠ m in 𝓝 n, DifferentiableAt ℝ P m) := fun hCD => by\n filter_upwards [Ioi_mem_nhds hn20] with m hm\n exact (hCD.differentiableOn (by norm_num)).differentiableAt (Ioi_mem_nhds hm)\n -- unweighted composition bundles (the c = 1.5 k-shift, D-073)\n have hk15 : (0 : ℝ) < 1.5 := by norm_num\n have hCDFc : ContDiffOn ℝ 2 (fun m => F (1.5 * Real.sqrt m + 1)) (Set.Ioi 20) :=\n hF.comp (contDiffOn_ksqrt_shift 1.5 hk15) (mapsTo_ksqrt_shift_Ioi1 1.5 hk15)\n have hCDTL1c : ContDiffOn ℝ 2\n (fun m => (fun t => t * Real.log (t + 2)) (1.5 * Real.sqrt m + 1)) (Set.Ioi 20) :=\n contDiffOn_TL1.comp (contDiffOn_ksqrt_shift 1.5 hk15) (mapsTo_ksqrt_shift 1.5 hk15)\n have hCDTL2c : ContDiffOn ℝ 2\n (fun m => (fun t => t * Real.log (Real.log (t + 2))) (1.5 * Real.sqrt m + 1))\n (Set.Ioi 20) :=\n contDiffOn_TL2.comp (contDiffOn_ksqrt_shift 1.5 hk15) (mapsTo_ksqrt_shift 1.5 hk15)\n have hCDL1sqc : ContDiffOn ℝ 2\n (fun m => (fun t => Real.log (t + 2) ^ 2) (1.5 * Real.sqrt m + 1)) (Set.Ioi 20) :=\n contDiffOn_L1sq.comp (contDiffOn_ksqrt_shift 1.5 hk15) (mapsTo_ksqrt_shift 1.5 hk15)\n have hCDL1L2c : ContDiffOn ℝ 2\n (fun m => (fun t => Real.log (t + 2) * Real.log (Real.log (t + 2)))\n (1.5 * Real.sqrt m + 1)) (Set.Ioi 20) :=\n contDiffOn_L1L2.comp (contDiffOn_ksqrt_shift 1.5 hk15) (mapsTo_ksqrt_shift 1.5 hk15)\n have hCDL2sqc : ContDiffOn ℝ 2\n (fun m => (fun t => Real.log (Real.log (t + 2)) ^ 2) (1.5 * Real.sqrt m + 1))\n (Set.Ioi 20) :=\n contDiffOn_L2sq.comp (contDiffOn_ksqrt_shift 1.5 hk15) (mapsTo_ksqrt_shift 1.5 hk15)\n have hCDL1c : ContDiffOn ℝ 2\n (fun m => (fun t => Real.log (t + 2)) (1.5 * Real.sqrt m + 1)) (Set.Ioi 20) :=\n contDiffOn_L1.comp (contDiffOn_ksqrt_shift 1.5 hk15) (mapsTo_ksqrt_shift 1.5 hk15)\n have hCDL2c : ContDiffOn ℝ 2\n (fun m => (fun t => Real.log (Real.log (t + 2))) (1.5 * Real.sqrt m + 1))\n (Set.Ioi 20) :=\n contDiffOn_L2.comp (contDiffOn_ksqrt_shift 1.5 hk15) (mapsTo_ksqrt_shift 1.5 hk15)\n have hCDIIM : ContDiffOn ℝ 2 IIMaj (Set.Ioi 20) := by\n have hId : IIMaj = fun m => psiTilde (Real.sqrt m) :=\n funext fun m => IIMaj_eq_psiTilde_sqrt m\n rw [hId]\n exact (psiTilde_contDiff.contDiffOn).comp\n (contDiffOn_id.sqrt (fun x hx => by\n have h : 20 < x := hx\n exact ne_of_gt (by linarith : (0 : ℝ) < x))) (Set.mapsTo_univ _ _)\n -- piece values\n have vS : deriv (deriv fun m => (1/2)*m*Real.log m +\n (lagariasC1 - Real.eulerMascheroniConstant/2)*m - 4) n = 1/(2*n) :=\n marginS_deriv2 _ hn0\n have vF : deriv (deriv (mFblock F)) n =\n (-4) * (1.5 ^ 2 * psiOf F (1.5 * Real.sqrt n + 1) / (4 * n)) := by\n unfold mFblock\n rw [deriv2_const_mul (-4) (hdd hCDFc) (hev hCDFc),\n chain_rule_sqrt_kshift_on F hk15 (le_refl 1) hF n hn0, ← psiOf_sqrt_krel]\n have vTL1 : deriv (deriv mTL1b) n = (-((8/3)*0.6 + 42)) *\n (1.5 ^ 2 * psiOf (fun t => t * Real.log (t + 2)) (1.5 * Real.sqrt n + 1) / (4 * n)) := by\n unfold mTL1b\n rw [deriv2_const_mul _ (hdd hCDTL1c) (hev hCDTL1c),\n chain_rule_sqrt_kshift_on _ hk15 (by norm_num : (-1 : ℝ) ≤ 1) contDiffOn_TL1 n hn0,\n ← psiOf_sqrt_krel]\n have vTL2 : deriv (deriv mTL2b) n = (-((8/3)*0.886)) *\n (1.5 ^ 2 * psiOf (fun t => t * Real.log (Real.log (t + 2))) (1.5 * Real.sqrt n + 1) /\n (4 * n)) := by\n unfold mTL2b\n rw [deriv2_const_mul _ (hdd hCDTL2c) (hev hCDTL2c),\n chain_rule_sqrt_kshift_on _ hk15 (by norm_num : (-1 : ℝ) ≤ 1) contDiffOn_TL2 n hn0,\n ← psiOf_sqrt_krel]\n have vId : deriv (deriv mIdb) n = (-((8/3)*2.7 + 192)) *\n (1.5 ^ 2 * psiOf id (1.5 * Real.sqrt n + 1) / (4 * n)) := by\n unfold mIdb\n have hCDidc : ContDiffOn ℝ 2 (fun m => id (1.5 * Real.sqrt m + 1)) (Set.Ioi 20) :=\n contDiffOn_id.comp (contDiffOn_ksqrt_shift 1.5 hk15) (Set.mapsTo_univ _ _)\n rw [show (fun m => -(8/3*2.7 + 192) * (1.5 * Real.sqrt m + 1)) =\n (fun m => -(8/3*2.7 + 192) * id (1.5 * Real.sqrt m + 1)) from rfl,\n deriv2_const_mul _ (hdd hCDidc) (hev hCDidc),\n chain_rule_sqrt_kshift_on _ hk15 (by norm_num : (-1 : ℝ) ≤ 1) contDiffOn_id n hn0,\n ← psiOf_sqrt_krel]\n have vL1sq : deriv (deriv mL1sqb) n = (-(42*0.433^2*(Real.exp (16/9) + 1))) *\n (1.5 ^ 2 * psiOf (fun t => Real.log (t + 2) ^ 2) (1.5 * Real.sqrt n + 1) / (4 * n)) := by\n unfold mL1sqb\n rw [deriv2_const_mul _ (hdd hCDL1sqc) (hev hCDL1sqc),\n chain_rule_sqrt_kshift_on _ hk15 (by norm_num : (-1 : ℝ) ≤ 1) contDiffOn_L1sq n hn0,\n ← psiOf_sqrt_krel]\n have vL1L2 : deriv (deriv mL1L2b) n = (-(42*(2*0.433*0.886)*(Real.exp (16/9) + 1))) *\n (1.5 ^ 2 * psiOf (fun t => Real.log (t + 2) * Real.log (Real.log (t + 2)))\n (1.5 * Real.sqrt n + 1) / (4 * n)) := by\n unfold mL1L2b\n rw [deriv2_const_mul _ (hdd hCDL1L2c) (hev hCDL1L2c),\n chain_rule_sqrt_kshift_on _ hk15 (by norm_num : (-1 : ℝ) ≤ 1) contDiffOn_L1L2 n hn0,\n ← psiOf_sqrt_krel]\n have vL2sq : deriv (deriv mL2sqb) n = (-(42*0.886^2*(Real.exp (16/9) + 1))) *\n (1.5 ^ 2 * psiOf (fun t => Real.log (Real.log (t + 2)) ^ 2) (1.5 * Real.sqrt n + 1) /\n (4 * n)) := by\n unfold mL2sqb\n rw [deriv2_const_mul _ (hdd hCDL2sqc) (hev hCDL2sqc),\n chain_rule_sqrt_kshift_on _ hk15 (by norm_num : (-1 : ℝ) ≤ 1) contDiffOn_L2sq n hn0,\n ← psiOf_sqrt_krel]\n have vL1 : deriv (deriv mL1b) n = (-((42*(2*0.433*2.9) + 147)*(Real.exp (16/9) + 1))) *\n (1.5 ^ 2 * psiOf (fun t => Real.log (t + 2)) (1.5 * Real.sqrt n + 1) / (4 * n)) := by\n unfold mL1b\n rw [deriv2_const_mul _ (hdd hCDL1c) (hev hCDL1c),\n chain_rule_sqrt_kshift_on _ hk15 (by norm_num : (-1 : ℝ) ≤ 1) contDiffOn_L1 n hn0,\n ← psiOf_sqrt_krel]\n have vL2 : deriv (deriv mL2b) n = (-(42*(2*0.886*2.9)*(Real.exp (16/9) + 1))) *\n (1.5 ^ 2 * psiOf (fun t => Real.log (Real.log (t + 2))) (1.5 * Real.sqrt n + 1) /\n (4 * n)) := by\n unfold mL2b\n rw [deriv2_const_mul _ (hdd hCDL2c) (hev hCDL2c),\n chain_rule_sqrt_kshift_on _ hk15 (by norm_num : (-1 : ℝ) ≤ 1) contDiffOn_L2 n hn0,\n ← psiOf_sqrt_krel]\n have vIIM : deriv (deriv mIIM) n = (-1.5) * deriv (deriv IIMaj) n := by\n unfold mIIM\n rw [deriv2_const_mul (-1.5) (hdd hCDIIM) (hev hCDIIM)]"},"extra_content":null}]