← Session 35 — ii′-6-R: Lagarias 6.1 right-tail re-proof (E-032/D-073)
Now the scaled chain-rule lemma, cloning the existing proof.
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean",
"old_string": "/-- [PROVED session 011] Chain-rule identity with T(n) = \u221an (no shift),\nfor the IIMaj term: d\u00b2/dn\u00b2 \u03c8(\u221an) = [\u03c8\u2033(\u221an) \u2212 \u03c8\u2032(\u221an)/\u221an] / (4n). -/",
"new_string": "/-- [PROVED session 040] Scaled-shift chain rule: for T(n) = k\u00b7\u221an + 1\n(k > 0), d\u00b2/dn\u00b2 \u03c6(k\u00b7\u221an+1) = k\u00b2\u00b7[\u03c6\u2033(T) \u2212 \u03c6\u2032(T)/(k\u00b7\u221an)]/(4n)\n= k\u00b2\u00b7\u03c8[\u03c6](T)/(4n). The c = 1.5 F-D repair (D-073 \u00a74) moves every\nmargin composition to this form; the c \u2264 1 domain condition and the\nproof structure follow `chain_rule_sqrt_shift_on`. -/\ntheorem chain_rule_sqrt_kshift_on (\u03c6 : \u211d \u2192 \u211d) {k : \u211d} (hk : 0 < k) {c : \u211d}\n (hc : c \u2264 1) (h\u03c6 : ContDiffOn \u211d 2 \u03c6 (Set.Ioi c)) (n : \u211d) (hn : 0 < n) :\n deriv (deriv fun n => \u03c6 (k * Real.sqrt n + 1)) n =\n (k ^ 2) * (deriv (deriv \u03c6) (k * Real.sqrt n + 1) -\n deriv \u03c6 (k * Real.sqrt n + 1) / (k * Real.sqrt n)) / (4 * n) := by\n have h\u03c6d : DifferentiableOn \u211d \u03c6 (Set.Ioi c) :=\n h\u03c6.differentiableOn (by norm_num)\n have h\u03c6dd : DifferentiableOn \u211d (deriv \u03c6) (Set.Ioi c) :=\n (h\u03c6.deriv_of_isOpen (m := 1) isOpen_Ioi (by norm_num)).differentiableOn\n one_ne_zero\n have hmem : \u2200 m : \u211d, 0 < m \u2192 Set.Ioi c \u2208 \ud835\udcdd (k * Real.sqrt m + 1) := by\n intro m hm\n have h1 : (1 : \u211d) < k * Real.sqrt m + 1 := by\n have h := mul_pos hk (Real.sqrt_pos.mpr hm)\n linarith\n exact Ioi_mem_nhds (lt_of_le_of_lt hc h1)\n have h\u03c61 : \u2200 m : \u211d, 0 < m \u2192 DifferentiableAt \u211d \u03c6 (k * Real.sqrt m + 1) :=\n fun m hm => h\u03c6d.differentiableAt (hmem m hm)\n have h\u03c62 : DifferentiableAt \u211d (deriv \u03c6) (k * Real.sqrt n + 1) :=\n h\u03c6dd.differentiableAt (hmem n hn)\n have hsqrt : HasDerivAt Real.sqrt (1 / (2 * Real.sqrt n)) n :=\n Real.hasDerivAt_sqrt hn.ne'\n have hdiff_sqrt : DifferentiableAt \u211d Real.sqrt n := hsqrt.differentiableAt\n have hpos : Set.Ioi (0 : \u211d) \u2208 \ud835\udcdd n := Ioi_mem_nhds hn\n have hg1 : deriv (fun n => \u03c6 (k * Real.sqrt n + 1)) =\u1da0[\ud835\udcdd n]\n fun n => deriv \u03c6 (k * Real.sqrt n + 1) * (k * (2 * Real.sqrt n)\u207b\u00b9) := by\n filter_upwards [hpos] with m hm\n have hsm : HasDerivAt Real.sqrt (1 / (2 * Real.sqrt m)) m :=\n Real.hasDerivAt_sqrt (ne_of_gt hm)\n have hhm : DifferentiableAt \u211d (fun x => k * Real.sqrt x + 1) m :=\n (hsm.differentiableAt.const_mul k).add (differentiableAt_const 1)\n have h1 : deriv (fun x => k * Real.sqrt x + 1) m = k * (1 / (2 * Real.sqrt m)) := by\n rw [deriv_add_const, deriv_const_mul k hsm.differentiableAt, hsm.deriv]\n rw [show (fun x => \u03c6 (k * Real.sqrt x + 1)) = \u03c6 \u2218 (fun x => k * Real.sqrt x + 1)\n from rfl,\n deriv_comp m (h\u03c61 m hm) hhm, h1]\n ring\n have hA : HasDerivAt (fun n => deriv \u03c6 (k * Real.sqrt n + 1))\n (deriv (deriv \u03c6) (k * Real.sqrt n + 1) * (k * (1 / (2 * Real.sqrt n)))) n := by\n have h1 : HasDerivAt (fun x => k * Real.sqrt x + 1) (k * (1 / (2 * Real.sqrt n))) n :=\n (hsqrt.const_mul k).add_const 1\n have h2 : HasDerivAt (deriv \u03c6) (deriv (deriv \u03c6) (k * Real.sqrt n + 1))\n (k * Real.sqrt n + 1) :=\n h\u03c62.hasDerivAt\n have h3 := h2.comp n h1\n rwa [show (fun n => deriv \u03c6 (k * Real.sqrt n + 1)) =\n deriv \u03c6 \u2218 (fun n => k * Real.sqrt n + 1) from rfl]\n have hB : HasDerivAt (fun n => k * (2 * Real.sqrt n)\u207b\u00b9)\n (k * (-(2 * (1 / (2 * Real.sqrt n))) / (2 * Real.sqrt n) ^ 2)) n := by\n have h1 : HasDerivAt (fun n => 2 * Real.sqrt n) (2 * (1 / (2 * Real.sqrt n))) n :=\n hsqrt.const_mul 2\n have h2 : (2 * Real.sqrt n) \u2260 0 :=\n mul_ne_zero two_ne_zero (Real.sqrt_ne_zero'.2 hn)\n exact (h1.inv h2).const_mul k\n have hmul : HasDerivAt (fun n => deriv \u03c6 (k * Real.sqrt n + 1) * (k * (2 * Real.sqrt n)\u207b\u00b9))\n (deriv (deriv \u03c6) (k * Real.sqrt n + 1) * (k * (1 / (2 * Real.sqrt n))) *\n (k * (2 * Real.sqrt n)\u207b\u00b9) +\n deriv \u03c6 (k * Real.sqrt n + 1) *\n (k * (-(2 * (1 / (2 * Real.sqrt n))) / (2 * Real.sqrt n) ^ 2))) n :=\n hA.mul hB\n have hder := (hmul.congr_of_eventuallyEq hg1).deriv\n rw [hder]\n set s := Real.sqrt n with hsdef\n have hs0 : s \u2260 0 := Real.sqrt_ne_zero'.2 hn\n have hk0 : k \u2260 0 := hk.ne'\n have hn_eq : n = s ^ 2 := by\n rw [hsdef]; exact (Real.sq_sqrt hn.le).symm\n rw [hn_eq]\n field_simp [hs0, hk0]\n ring\n\n/-- [PROVED session 011] Chain-rule identity with T(n) = \u221an (no shift),\nfor the IIMaj term: d\u00b2/dn\u00b2 \u03c8(\u221an) = [\u03c8\u2033(\u221an) \u2212 \u03c8\u2032(\u221an)/\u221an] / (4n). -/"
}
raw content_json (database row)
[{"type":"text","text":"Now the scaled chain-rule lemma, cloning the existing proof."},{"type":"tool_use","id":"Edit_83","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean","old_string":"/-- [PROVED session 011] Chain-rule identity with T(n) = √n (no shift),\nfor the IIMaj term: d²/dn² ψ(√n) = [ψ″(√n) − ψ′(√n)/√n] / (4n). -/","new_string":"/-- [PROVED session 040] Scaled-shift chain rule: for T(n) = k·√n + 1\n(k > 0), d²/dn² φ(k·√n+1) = k²·[φ″(T) − φ′(T)/(k·√n)]/(4n)\n= k²·ψ[φ](T)/(4n). The c = 1.5 F-D repair (D-073 §4) moves every\nmargin composition to this form; the c ≤ 1 domain condition and the\nproof structure follow `chain_rule_sqrt_shift_on`. -/\ntheorem chain_rule_sqrt_kshift_on (φ : ℝ → ℝ) {k : ℝ} (hk : 0 < k) {c : ℝ}\n (hc : c ≤ 1) (hφ : ContDiffOn ℝ 2 φ (Set.Ioi c)) (n : ℝ) (hn : 0 < n) :\n deriv (deriv fun n => φ (k * Real.sqrt n + 1)) n =\n (k ^ 2) * (deriv (deriv φ) (k * Real.sqrt n + 1) -\n deriv φ (k * Real.sqrt n + 1) / (k * Real.sqrt n)) / (4 * n) := by\n have hφd : DifferentiableOn ℝ φ (Set.Ioi c) :=\n hφ.differentiableOn (by norm_num)\n have hφdd : DifferentiableOn ℝ (deriv φ) (Set.Ioi c) :=\n (hφ.deriv_of_isOpen (m := 1) isOpen_Ioi (by norm_num)).differentiableOn\n one_ne_zero\n have hmem : ∀ m : ℝ, 0 < m → Set.Ioi c ∈ 𝓝 (k * Real.sqrt m + 1) := by\n intro m hm\n have h1 : (1 : ℝ) < k * Real.sqrt m + 1 := by\n have h := mul_pos hk (Real.sqrt_pos.mpr hm)\n linarith\n exact Ioi_mem_nhds (lt_of_le_of_lt hc h1)\n have hφ1 : ∀ m : ℝ, 0 < m → DifferentiableAt ℝ φ (k * Real.sqrt m + 1) :=\n fun m hm => hφd.differentiableAt (hmem m hm)\n have hφ2 : DifferentiableAt ℝ (deriv φ) (k * Real.sqrt n + 1) :=\n hφdd.differentiableAt (hmem n hn)\n have hsqrt : HasDerivAt Real.sqrt (1 / (2 * Real.sqrt n)) n :=\n Real.hasDerivAt_sqrt hn.ne'\n have hdiff_sqrt : DifferentiableAt ℝ Real.sqrt n := hsqrt.differentiableAt\n have hpos : Set.Ioi (0 : ℝ) ∈ 𝓝 n := Ioi_mem_nhds hn\n have hg1 : deriv (fun n => φ (k * Real.sqrt n + 1)) =ᶠ[𝓝 n]\n fun n => deriv φ (k * Real.sqrt n + 1) * (k * (2 * Real.sqrt n)⁻¹) := by\n filter_upwards [hpos] with m hm\n have hsm : HasDerivAt Real.sqrt (1 / (2 * Real.sqrt m)) m :=\n Real.hasDerivAt_sqrt (ne_of_gt hm)\n have hhm : DifferentiableAt ℝ (fun x => k * Real.sqrt x + 1) m :=\n (hsm.differentiableAt.const_mul k).add (differentiableAt_const 1)\n have h1 : deriv (fun x => k * Real.sqrt x + 1) m = k * (1 / (2 * Real.sqrt m)) := by\n rw [deriv_add_const, deriv_const_mul k hsm.differentiableAt, hsm.deriv]\n rw [show (fun x => φ (k * Real.sqrt x + 1)) = φ ∘ (fun x => k * Real.sqrt x + 1)\n from rfl,\n deriv_comp m (hφ1 m hm) hhm, h1]\n ring\n have hA : HasDerivAt (fun n => deriv φ (k * Real.sqrt n + 1))\n (deriv (deriv φ) (k * Real.sqrt n + 1) * (k * (1 / (2 * Real.sqrt n)))) n := by\n have h1 : HasDerivAt (fun x => k * Real.sqrt x + 1) (k * (1 / (2 * Real.sqrt n))) n :=\n (hsqrt.const_mul k).add_const 1\n have h2 : HasDerivAt (deriv φ) (deriv (deriv φ) (k * Real.sqrt n + 1))\n (k * Real.sqrt n + 1) :=\n hφ2.hasDerivAt\n have h3 := h2.comp n h1\n rwa [show (fun n => deriv φ (k * Real.sqrt n + 1)) =\n deriv φ ∘ (fun n => k * Real.sqrt n + 1) from rfl]\n have hB : HasDerivAt (fun n => k * (2 * Real.sqrt n)⁻¹)\n (k * (-(2 * (1 / (2 * Real.sqrt n))) / (2 * Real.sqrt n) ^ 2)) n := by\n have h1 : HasDerivAt (fun n => 2 * Real.sqrt n) (2 * (1 / (2 * Real.sqrt n))) n :=\n hsqrt.const_mul 2\n have h2 : (2 * Real.sqrt n) ≠ 0 :=\n mul_ne_zero two_ne_zero (Real.sqrt_ne_zero'.2 hn)\n exact (h1.inv h2).const_mul k\n have hmul : HasDerivAt (fun n => deriv φ (k * Real.sqrt n + 1) * (k * (2 * Real.sqrt n)⁻¹))\n (deriv (deriv φ) (k * Real.sqrt n + 1) * (k * (1 / (2 * Real.sqrt n))) *\n (k * (2 * Real.sqrt n)⁻¹) +\n deriv φ (k * Real.sqrt n + 1) *\n (k * (-(2 * (1 / (2 * Real.sqrt n))) / (2 * Real.sqrt n) ^ 2))) n :=\n hA.mul hB\n have hder := (hmul.congr_of_eventuallyEq hg1).deriv\n rw [hder]\n set s := Real.sqrt n with hsdef\n have hs0 : s ≠ 0 := Real.sqrt_ne_zero'.2 hn\n have hk0 : k ≠ 0 := hk.ne'\n have hn_eq : n = s ^ 2 := by\n rw [hsdef]; exact (Real.sq_sqrt hn.le).symm\n rw [hn_eq]\n field_simp [hs0, hk0]\n ring\n\n/-- [PROVED session 011] Chain-rule identity with T(n) = √n (no shift),\nfor the IIMaj term: d²/dn² ψ(√n) = [ψ″(√n) − ψ′(√n)/√n] / (4n). -/"},"extra_content":null}]