[{"type":"thinking","thinking":"`ContDiffOn.sqrt (hf : ContDiffOn ℝ n f s) (hs : ∀ x ∈ s, f x ≠ 0) : ContDiffOn ℝ n (fun y => √(f y)) s` ✓ — so ContDiffOn ℝ 2 (fun n => √(n) + 1)?? T = √n+1: (contDiffOn_id.sqrt (fun x hx => ne_of_gt (by ...))).add contDiffOn_const ✓.\n\nNow — big design decision to reduce the assembly pain. Given how much boilerplate the full \"12-piece combinator\" assembly would take, let me simplify: GROUP the pieces to minimize combinator applications:\n\nmarginTilde F = S0 − P1 − IIMaj + K where:\n- S0(n) = ½n log n + cn − 4\n- P1(n) = 2F(Tn) + (all 8 block terms with weights) — ONE combined function whose second derivative I compute via... still needs the per-block split for chain-rule values. Hmm no shortcut there.\n\nAlternative assembly avoiding per-piece combinator chains: compute deriv (deriv (marginTilde F)) n via deriv2_of_hasDerivAt_nhds with the FULL D1/D2 closed forms! I.e., construct HasDerivAt (marginTilde F) (D1 m) per point m (m > 20) by combining per-point HasDerivAts via .add/.sub/.mul/.const_mul chains (term-level, no deriv/differentiable facts needed!), then HasDerivAt D1 (D2 n) n similarly. The VALUE deriv (deriv f) n = D2n directly. This needs NO ContDiffOn, NO combinators — just HasDerivAt term-building. The per-point compositions:\n\nFor each block φᵢ and point m (> 20): HasDerivAt (fun m' => φᵢ(√m'+1)) (φᵢ'(√m+1)·(1/(2√m))) m := (block-HasDerivAt at √m+1).comp m (T-HasDerivAt). The block HasDerivAts I have: hasDerivAt_log_shift (for L1 at point x > −2), hasDerivAt_log_log (L2, x > −1), and for L1², L1L2, L2², TL1, TL2 — the psiOf_* proofs CONTAIN per-point h1's but not as standalone lemmas. Need standalone per-point block derivatives:\n- hasDerivAt_L1sq (x) (hx : -2 < x): HasDerivAt (fun t => (log(t+2))^2) (2*L1*(x+2)⁻¹) x := (hasDerivAt_log_shift x hx).pow 2 (massage pow_one, cast).\n- hasDerivAt_L1L2 (x) (hx : -1 < x): := (hasDerivAt_log_shift x _).mul (hasDerivAt_log_log x _) + massage to (L2+1)*(x+2)⁻¹.\n- hasDerivAt_L2sq (x) (hx): := (hasDerivAt_log_log x _).pow 2 massage to 2*L2*((x+2)*L1)⁻¹.\n- hasDerivAt_TL1 (x) (hx): := (hasDerivAt_id' x).mul (hasDerivAt_log_shift x _) → L1 + x*(x+2)⁻¹ (one_mul).\n- hasDerivAt_TL2 (x) (hx): := (hasDerivAt_id' x).mul (hasDerivAt_log_log x _) → L2 + x*((x+2)*L1)⁻¹ (massage).\n\nT-HasDerivAt at m (m > 0): HasDerivAt (fun m' => √m' + 1) (1/(2√m)) m := (Real.hasDerivAt_sqrt (ne_of_gt hm)).add_const 1 — wait add_const on VALUE: (fun m' => √m' + 1) ✓ correct usage (this matches chain_rule_sqrt_shift's hsqrt.add_const 1 ✓).\n\nComposition: HasDerivAt.comp m (block at √m+1) (T at m) — signature: HasDerivAt.comp (x) (h₂ : HasDerivAt g₂ g₂' (g₁ x)) (h₁ : HasDerivAt g₁ g₁' x) : HasDerivAt (g₂ ∘ g₁) (g₂' * g₁') x ✓ — derivative: φᵢ'(√m+1) * (1/(2√m)) ✓.\n\nF: hF.differentiable (by norm_num) : Differentiable ℝ F → (hF.differentiable _ (√m+1)).hasDerivAt : HasDerivAt F (deriv F (√m+1)) (√m+1) ✓ .comp.\n\nS0: per-point HasDerivAt (marginS-style, as in marginS_deriv2's h1 — make standalone: hasDerivAt_marginS (m) (hm : 0 < m) (c)).\n\nIIMaj: (hasDerivAt_psiTilde (√m)).comp m (Real.hasDerivAt_sqrt hm.ne') ✓.\n\nThen the FULL h1: combine via .add/.sub/.const_mul ~15 steps with final massage (convert...ring on the derivative value: the sum of the per-piece derivatives equals D1 m in the regrouped form — ring with atoms!). The D1 form I choose: make it match the FINAL needed D2 computation. D1(m) = ½(log m + 1) + c − 2·F'(Tm)·(2√m)⁻¹ − Σwᵢφᵢ'(Tm)·(2√m)⁻¹ − ψ̃'(√m)·(2√m)⁻¹.\n\nThen h2: HasDerivAt D1 (D2n) n — differentiating THIS function: each term φᵢ'(Tm)·(2√m)⁻¹ — product of (φᵢ'∘T) and (2√·)⁻¹: per-piece HasDerivAt again: (φᵢ''(Tm)·(2√m)⁻¹)·(2√m)⁻¹ + φᵢ'(Tm)·(−(2√m)⁻²·(√m)')... the derivative of (2√m)⁻¹ = −(2·(1/(2√m)))/(2√m)² — from chain_rule proofs' hB. This is ANOTHER layer of per-point HasDerivAt building (~15 pieces AGAIN with product rules). Total: this is essentially redoing the chain-rule proof for the full sum — the chain-rule lemmas already do exactly this per piece! The combinator route reuses them; the deriv2_of_hasDerivAt_nhds route redoes it. COMBINATORS WIN on reuse.\n\nOK — decision final: combinator route with per-piece ContDiffOn bundles. But actually, hmm — there's an even better trick for the VALUE step: I don't need deriv (deriv (marginTilde F)) n as an equality with the full formula — I need only the INEQUALITY 0 ≤ deriv (deriv (marginTilde F)) n. With the combinators, deriv2_add gives EQUALITY of the sum's second deriv with the sum of second derivs ✓ then substitute the chain-rule values ✓ then the sign argument ✓ — yes, that's the plan.\n\nCombinator chain for 12 pieces: marginTilde = (((S0 − 2F∘T) − B1) − B2) − ... structure as nested subs: I'll write the identity with the block sum as a single big subtraction chain and mirror it with deriv2_sub applications. ~11 deriv2_sub/add/const_mul steps — each needs 4 facts per piece (2 diffAt + 2 eventually)... the facts are per-PIECE not per-step: collect per-piece bundles first (11 bundles: F∘T, 8 blocks, IIMaj, S0... S0's diff facts: from its ContDiffOn too (S0 ContDiffOn Ioi 20: id.mul log + linear ✓).\n\nBundle per piece P: \n  hP1 : DifferentiableAt ℝ (deriv P) n (n > 20)\n  hP2 : ∀ᶠ m in 𝓝 n, DifferentiableAt ℝ P m\n  hP3 : deriv (deriv P) n = [value]\nSources:\n- blocks/F: hP3 from chain_rule_sqrt_shift_on (or _shift for F); hP1 from ContDiffOn(deriv); hP2 from ContDiffOn.differentiableOn.\n- S0: marginS_deriv2 for value; S0's ContDiffOn for hP1/hP2.\n- IIMaj: value from chain_rule_sqrt (as in IIMaj_deriv2_lt); ContDiff from psiTilde_contDiff.comp sqrt → ContDiffOn.\n\nThe block ContDiffOn (Ioi 20) = contDiffOn_Lx.comp (hT, hmaps) where hT : ContDiffOn ℝ 2 (fun m => √m + 1) (Ioi 20), hmaps : MapsTo (fun m => √m+1) (Ioi 20) (Ioi (−1)) ✓.\n\nThis is very mechanical now. Also note — for the deriv2_const_mul combinator, pieces with weights wᵢ·(φᵢ∘T): apply const_mul to the block bundle.\n\nThe VALUE equality shape: deriv (deriv (marginTilde F)) n = marginS-value − 2·Fblock-value − Σwᵢ·blockᵢ-value − IIMaj-value + 0 (const).\nWith chain-rule values: blockᵢ-value = [φᵢ″(Tn) − φᵢ'(Tn)/√n]/(4n) = psiOf φᵢ Tn / (4n) after rewriting √n = Tn − 1: have hsT : Real.sqrt n = (Real.sqrt n + 1) - 1 := by ring ✓ rw to convert psiOf form ✓ then psiOf_* lemmas give closed forms + signs.\n\nSo: deriv (deriv (marginTilde F)) n = 1/(2n) − 2·psiOf F Tn/(4n) − Σ wᵢ·psiOf φᵢ Tn/(4n) − IIMaj″(n).\n\nSign: −2·psiOf F/(4n) > 0 (hψ : psiOf F T < 0 for T ≥ √20+1 — note hψ in the theorem is stated as `deriv (deriv F) T - deriv F T / (T - 1) < 0` = psiOf F T < 0 ✓). −wᵢpsiᵢ/(4n) > 0 (psiOf_*_neg with hT : √20+1 ≤ Tn ✓ from n ≥ 20: Tn = √n+1 ≥ √20+1 ✓). Sum ≥ 0 → margiñ″ ≥ 1/(2n) − IIMaj″(n) > 0 (IIMaj_deriv2_lt) ✓.\n\nStructure of the F proof:\nintro n hn (hn : n ∈ interior (Ici 20) = Ioi 20 → 20 < n)\nhave hn20 : 20 ≤ n := le_of_lt ...\nbuild the identity rewrite: rw [marginTilde_identity] — goal: 0 ≤ deriv (deriv (big-lambda)) n.\napply combinators to split... The identity's RHS lambda: structure as `fun n => ((S0 n − 2*(F∘T) n) − blocksum n) − IIMaj n + K`? Make the identity produce a convenient nesting: fun n => S0 n − 2 * (F∘T n) − (w1*B1 n + w2*B2 n + ... + w8*B8 n) − IIMaj n + K.\n\nderiv (deriv of that) n: via deriv2_sub (needs the two sides' facts)... 4 levels: \nE0 = fun n => S0 n − (2*(F∘T n) + BS n + IIMaj n − K)?? — cleaner: write as S0 + (−)(...)... Let me define the identity as:\nmarginTilde F = fun n => S0 n + ((-2) * (F∘T) n + ((-1) * BS n + (-1) * IIMaj n + K))?? — the const K at the end: + K → deriv of +const = same: handle via deriv2_add with const piece (deriv (deriv (fun _ => K)) n = 0: combinators with const).\n\nHonestly the cleanest: treat the identity RHS as a right-nested ADD chain:\nf0 = S0\nf1 = fun n => (-2) * F(√n+1)\nf2..f9 = fun n => (-wᵢ) * Bᵢ(√n+1)  [weights folded with the MINUS sign — the ψᵢ<0 with −wᵢ gives +]\nf10 = fun n => (-1) * IIMaj n\nf11 = fun _ => K\nmarginTilde F = f0 + (f1 + (f2 + (... + (f10 + f11)...)))\n\nderiv (deriv (marginTilde F)) n = Σ deriv (deriv fᵢ) n via 11 deriv2_add applications ✓ each with the bundles.\n\nValues:\n- f0: 1/(2n).\n- f1: (−2)·ψF(Tn)/(4n) — via deriv2_const_mul on F∘T with chain_rule_sqrt_shift value.\n- f2..f9: (−wᵢ)·psiOf φᵢ Tn/(4n) — wait: (−wᵢ)·[ψᵢ/(4n)] with ψᵢ < 0, wᵢ > 0 → positive ✓.\n- f10: (−1)·IIMaj″(n) = −IIMaj″(n).\n- f11: 0.\n\nSum = 1/(2n) − 2ψF/(4n) − Σwᵢψᵢ/(4n) − IIMaj″(n) ≥ 1/(2n) − IIMaj″(n) > 0 ✓.\n\nderiv2_const_mul combinator:\ntheorem deriv2_const_mul {f : ℝ → ℝ} {n : ℝ} (c : ℝ)\n    (hf1 : DifferentiableAt ℝ (deriv f) n) (hf2 : ∀ᶠ m in 𝓝 n, DifferentiableAt ℝ f m) :\n    deriv (deriv (fun m => c * f m)) n = c * deriv (deriv f) n := by\n  have he : deriv (fun m => c * f m) =ᶠ[𝓝 n] (fun m => c * deriv f m) := by\n    filter_upwards [hf2] with m hfm\n    exact deriv_const_mul c hfm\n  have h2 : HasDerivAt (fun m => c * deriv f m) (c * deriv (deriv f) n) n :=\n    (hf1.const_mul c).hasDerivAt\n  exact (h2.congr_of_eventuallyEq he.symm).deriv\n\nWait — `deriv_const_mul (c) (hf : DifferentiableAt ℝ f x) : deriv (fun x => c * f x) x = c * deriv f x` ✓ exists (I'm fairly confident: deriv_const_mul). hf1.const_mul c : DifferentiableAt ℝ (fun m => c * deriv f m) n ✓ (DifferentiableAt.const_mul ✓).\n\nderiv2_add (as sketched). That's all combinators needed (add + const_mul; K-piece via its own trivial bundle: DifferentiableAt (deriv (fun _ => K)) n = const fun... deriv (fun _ => K) = fun _ => 0: differentiableAt_const; value deriv (deriv (fun _ => K)) n = 0: via deriv2_of_hasDerivAt_nhds? simpler: deriv (fun _ => K) =ᶠ fun _ => 0 (eventually_of_forall deriv_const) → deriv = 0. Small lemma deriv2_const_val:\ntheorem deriv2_const (K n : ℝ) : deriv (deriv fun _ => K) n = 0 := by\n  have he : deriv (fun _ => K) =ᶠ[𝓝 n] fun _ => (0:ℝ) := by filter_upwards [] with m; exact deriv_const m K\n  ... pointwise deriv-eq needed!! he.deriv gives =ᶠ not pointwise (per the psiOf_id lesson) — use deriv2_of_hasDerivAt_nhds: h1 : ∀ᶠ m, HasDerivAt (fun _ => K) 0 m := filter_upwards; exact hasDerivAt_const m K; h2 : HasDerivAt (fun _ => 0) 0 n := hasDerivAt_const n 0; exact deriv2_of_hasDerivAt_nhds h1 h2 ✓.\n\nAnd the eventual-diff facts for const: trivial.\n\nNow the identity: marginTilde F = right-nested add chain — prove by unfold + ring: ring normalizes ANY association ✓.\n\nLet me also handle psiOf F Tn: the theorem's hψ : ∀ T, √20+1 ≤ T → deriv (deriv F) T − deriv F T/(T−1) < 0 = psiOf F T < 0 ✓ directly usable (psiOf F T unfolds to exactly that ✓ — psiOf is a def: hψ T hT : deriv (deriv F) T − deriv F T/(T−1) < 0 — matches psiOf F T < 0 definitionally; `show`/`exact` fine).\n\nNow, the chain-rule VALUES for the blocks: chain_rule_sqrt_shift_on φᵢ hCDi n hn0 : deriv (deriv fun m => φᵢ(√m+1)) n = (φᵢ''(Tn) − φᵢ'(Tn)/√n)/(4n). Need to rewrite to psiOf φᵢ Tn/(4n): psiOf φᵢ Tn = φᵢ''(Tn) − φᵢ'(Tn)/(Tn−1); Tn−1 = √n: rw [show Real.sqrt n = (Real.sqrt n + 1) - 1 by ring] INSIDE the chain-rule result — the term deriv φᵢ (√n+1)/√n: rewrite √n → (√n+1)−1: makes it psiOf ✓. So per block:\nhave hBi : deriv (deriv (fun m => φᵢ (√m+1))) n = psiOf φᵢ (√n+1) / (4*n) := by\n  rw [chain_rule_sqrt_shift_on φᵢ hCDi n hn0]\n  rw [show Real.sqrt n = (Real.sqrt n + 1) - 1 by ring] — CAREFUL: this rewrites ALL √n occurrences including in (4*n) and inside φᵢ-arguments?? The chain-rule result: (deriv (deriv φᵢ) (√n+1) − deriv φᵢ (√n+1)/√n)/(4*n) — rewriting √n everywhere: (√n+1) becomes ((√n+1)−1+1)?? — rw [show √n = (√n+1)−1] rewrites every √n — including inside `√n + 1` — INFINITE loop? No — rw rewrites each occurrence once: (√n+1) → ((√n+1)−1)+1 — creates NEW √n inside — those are NOT re-rewritten (rw does one pass with the instantiated rule) but the new expression has √n again inside ((√n+1)−1)... it rewrites ALL CURRENT occurrences simultaneously, producing ((√n+1)−1+1) mess. BAD. Instead: `conv` to target only the /√n occurrence, or: nth_rewrite: `nth_rewrite 2 [show ...]`? The occurrences of √n: (1) inside √n+1 [deriv (deriv φᵢ) (√n+1)], (2) inside the second √n+1 [deriv φᵢ (√n+1)], (3) the /√n one. Rewrite only #3: nth_rewrite 3 [show (Real.sqrt n) = (Real.sqrt n + 1) - 1 by ring]?? — but occurrences 1,2 are `√n + 1` — the PATTERN √n appears there too — nth_rewrite counts pattern instances: instance 1 = inside first √n+1, 2 = second √n+1, 3 = the /√n ✓ nth_rewrite 3. Fragile but workable. Alternative cleaner: psiOf_rel : psiOf φ (√n+1) = deriv (deriv φ) (√n+1) − deriv φ (√n+1)/√n — prove as a standalone mini-lemma: unfold psiOf; rw [show (Real.sqrt n + 1) - 1 = Real.sqrt n by ring] — rewriting (Tn−1) → √n: occurrences of `Real.sqrt n + 1 - 1` — only in psiOf's T−1 position ✓: unfold psiOf gives deriv (deriv φ) (√n+1) − deriv φ (√n+1)/((√n+1)−1) — rw [show (√n+1)−1 = √n by ring] ✓ rewrites that specific subterm ((√n+1)−1 — appears once) ✓. So:\nhave hpsi_rel : psiOf φ (√n+1) = deriv (deriv φ) (√n+1) − deriv φ (√n+1)/Real.sqrt n := by\n  unfold psiOf; rw [show Real.sqrt n + 1 - 1 = Real.sqrt n by ring]\nthen rw [chain_rule..., ← hpsi_rel] ✓.\n\nFor F: chain_rule_sqrt_shift F hF n hn0 ✓ same treatment.\n\nOK. Time to write. This final assembly is big — split into edits:\nEdit A: per-point standalone block HasDerivAts (not needed for combinators! skip) — NOT needed. What IS needed: per-block ContDiffOn ℝ 2 (Ioi (−1)) + ContDiffOn ℝ 2 (fun m => √m+1) (Ioi 20) + ContDiffOn ℝ 2 compositions + psiOf_rel.\nEdit B: combinators (deriv2_add, deriv2_const_mul, deriv2_const) + marginS_deriv2 + hasDerivAt_marginS helper.\nEdit C: marginTilde_identity + regularity (ContDiffOn of the whole) + the main theorem.\n\nActually for the per-piece bundles in F, the pieces are (φᵢ∘T): I need their ContDiffOn ℝ 2 on Ioi 20 — from block ContDiffOn (Ioi (−1)) ∘ T. Let me define:\n\nhT : ContDiffOn ℝ 2 (fun m => Real.sqrt m + 1) (Set.Ioi 20) :=\n  (contDiffOn_id.sqrt (fun x hx => ne_of_gt (by ...: 0 < x))).add contDiffOn_const\nhmaps : Set.MapsTo (fun m => Real.sqrt m + 1) (Set.Ioi 20) (Set.Ioi (-1)) :=\n  fun x hx => by have : 20 < x := hx; have : 0 < Real.sqrt x := Real.sqrt_pos.mpr (by linarith); linarith [Real.sqrt_nonneg x]?? MapsTo: √x+1 > −1 ⟸ √x ≥ 0 → √x+1 ≥ 1 > −1 ✓.\n\nhCD_L1 : ContDiffOn ℝ 2 (fun t => Real.log (t+2)) (Ioi (−1)) ✓ (above)\npiece ContDiffOn: (hCD_L1.comp hT hmaps) : ContDiffOn ℝ 2 ((fun t => log (t+2)) ∘ (fun m => √m+1)) (Ioi 20) — the composition function vs `fun m => log (√m+1+2)` — defeq; when using in chain_rule_sqrt_shift_on φᵢ — φᵢ is the UNCOMPOSED block ✓ chain-rule takes φᵢ + its ContDiffOn on Ioi(−1) ✓ hCD_Lx directly! The COMPOSITION's ContDiffOn is for the bundles (diff facts). So per block: hCDblock (Ioi(−1)) for chain-rule; hCDpiece := hCDblock.comp hT hmaps for bundles.\n\nFor F: hF.contDiffOn — ContDiffOn ℝ 2 F univ: chain-rule uses global chain_rule_sqrt_shift with hF : ContDiff ℝ 2 F ✓ (given in the theorem). Piece: (hF.contDiffOn).comp hT (mapsTo univ: mapsTo_univ) ✓ or ContDiffOn ℝ 2 (F∘T) (Ioi 20) from (hF.contDiffOn.comp hT (Set.mapsTo_univ _ _)) ✓.\n\nFor IIMaj: psiTilde_contDiff.contDiffOn.comp (contDiffOn_sqrt-part, mapsTo univ) — IIMaj = psiTilde∘√: (psiTilde_contDiff.contDiffOn).comp (contDiffOn_id.sqrt ...) (mapsTo univ) ✓ but the piece in the identity is IIMaj n (folded def!) — deriv facts about IIMaj itself: DifferentiableAt ℝ (deriv IIMaj) n: from ContDiffOn of IIMaj — IIMaj = (fun m => psiTilde (√m)) by hId: rw [hId] at the ContDiffOn? hCD_IIMaj : ContDiffOn ℝ 2 IIMaj (Ioi 20) := by rw [hId]; exact ...comp... ✓ (hId : IIMaj = fun m => psiTilde (√m) — rewrite the ContDiffOn goal ✓).\n\nS0: ContDiffOn ℝ 2 (fun m => ½m log m + cm − 4) (Ioi 20): contDiffOn_id.mul ((contDiffOn_id).log (fun x hx => ne_of_gt (by ... 0 < x))) — (fun m => m * log m); const_mul for ½ and c; sub const ✓.\n\nOK — writing Edit A now: block ContDiffOns (7) + hT + hmaps + psiOf_rel. Wait — psiOf_rel per block is the same lemma with φ variable: one generic lemma psiOf_sqrt_rel (φ) (n) : psiOf φ (√n+1) = deriv (deriv φ) (√n+1) − deriv φ (√n+1)/√n ✓ generic ✓.","signature":""},{"type":"text","text":"All API names confirmed. Writing the final assembly, Edit A: block ContDiffOn lemmas + T-bundle + psiOf bridge."},{"type":"tool_use","id":"Edit_267","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean","old_string":"/-- [SKELETON] Margin convexity (D-057, draft §3.1 Step 4): for any","new_string":"/-! ### Assembly: regularity bundles -/\n\n/-- [PROVED session 011] The blocks are C² on (−1, ∞) (all\nL1/L2-singularities lie at T ≤ −1). -/\ntheorem contDiffOn_L1 : ContDiffOn ℝ 2 (fun t => Real.log (t + 2)) (Set.Ioi (-1)) :=\n  (contDiffOn_id.add contDiffOn_const).log (fun x hx => by\n    have h : -1 < x := hx\n    exact ne_of_gt (by linarith : (0 : ℝ) < x + 2))\n\ntheorem contDiffOn_L2 :\n    ContDiffOn ℝ 2 (fun t => Real.log (Real.log (t + 2))) (Set.Ioi (-1)) :=\n  contDiffOn_L1.log (fun x hx => by\n    have h : -1 < x := hx\n    exact ne_of_gt (Real.log_pos (by linarith : (1 : ℝ) < x + 2)))\n\ntheorem contDiffOn_L1sq :\n    ContDiffOn ℝ 2 (fun t => Real.log (t + 2) ^ 2) (Set.Ioi (-1)) :=\n  contDiffOn_L1.pow 2\n\ntheorem contDiffOn_L1L2 : ContDiffOn ℝ 2\n    (fun t => Real.log (t + 2) * Real.log (Real.log (t + 2))) (Set.Ioi (-1)) :=\n  contDiffOn_L1.mul contDiffOn_L2\n\ntheorem contDiffOn_L2sq :\n    ContDiffOn ℝ 2 (fun t => Real.log (Real.log (t + 2)) ^ 2) (Set.Ioi (-1)) :=\n  contDiffOn_L2.pow 2\n\ntheorem contDiffOn_TL1 :\n    ContDiffOn ℝ 2 (fun t => t * Real.log (t + 2)) (Set.Ioi (-1)) :=\n  contDiffOn_id.mul contDiffOn_L1\n\ntheorem contDiffOn_TL2 :\n    ContDiffOn ℝ 2 (fun t => t * Real.log (Real.log (t + 2))) (Set.Ioi (-1)) :=\n  contDiffOn_id.mul contDiffOn_L2\n\n/-- [PROVED session 011] T(m) = √m + 1 is C² on (20, ∞) and maps it\ninto (−1, ∞). -/\ntheorem contDiffOn_sqrt_shift :\n    ContDiffOn ℝ 2 (fun m => Real.sqrt m + 1) (Set.Ioi 20) :=\n  (contDiffOn_id.sqrt (fun x hx => by\n    have h : 20 < x := hx\n    exact ne_of_gt (by linarith : (0 : ℝ) < x))).add contDiffOn_const\n\ntheorem mapsTo_sqrt_shift :\n    Set.MapsTo (fun m => Real.sqrt m + 1) (Set.Ioi 20) (Set.Ioi (-1)) := by\n  intro x hx\n  have h : 20 < x := hx\n  have h2 : (1 : ℝ) ≤ Real.sqrt x + 1 := by\n    have := Real.sqrt_nonneg x\n    linarith\n  linarith\n\n/-- [PROVED session 011] psiOf at T = √n + 1 in the chain-rule form\n(with T − 1 = √n). -/\ntheorem psiOf_sqrt_rel (φ : ℝ → ℝ) (n : ℝ) :\n    psiOf φ (Real.sqrt n + 1) =\n      deriv (deriv φ) (Real.sqrt n + 1) - deriv φ (Real.sqrt n + 1) / Real.sqrt n := by\n  unfold psiOf\n  rw [show Real.sqrt n + 1 - 1 = Real.sqrt n by ring]\n\n/-- [SKELETON] Margin convexity (D-057, draft §3.1 Step 4): for any"},"extra_content":null}]