{
  "file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean",
  "offset": 1900,
  "limit": 40
}

{
  "type": "text",
  "file": {
    "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean",
    "content": "included \u2014 the C\u00b2 regularity on (20, \u221e) does not give the endpoint). -/\ntheorem continuousOn_marginExpanded (F : \u211d \u2192 \u211d) (hF : ContDiffOn \u211d 2 F (Set.Ioi 1)) :\n    ContinuousOn (marginExpanded F) (Set.Ici 20) := by\n  have hsqrt : ContinuousOn Real.sqrt (Set.Ici 20) := Real.continuous_sqrt.continuousOn\n  have hT : ContinuousOn (fun m => Real.sqrt m + 1) (Set.Ici 20) :=\n    hsqrt.add continuousOn_const\n  have hmaps : Set.MapsTo (fun m => Real.sqrt m + 1) (Set.Ici 20) (Set.Ioi (-1)) := by\n    intro x hx\n    have h : 20 \u2264 x := hx\n    have hnn := Real.sqrt_nonneg x\n    exact Set.mem_Ioi.mpr (by linarith)\n  have hlog : ContinuousOn Real.log (Set.Ici 20) :=\n    Real.continuousOn_log.mono (fun x hx => by\n      have h : 20 \u2264 x := hx\n      exact ne_of_gt (by linarith : (0 : \u211d) < x))\n  have hId : IIMaj = fun m => psiTilde (Real.sqrt m) :=\n    funext fun m => IIMaj_eq_psiTilde_sqrt m\n  have hIIMc : ContinuousOn IIMaj (Set.Ici 20) := by\n    rw [hId]\n    exact (psiTilde_contDiff.continuous.continuousOn).comp hsqrt (Set.mapsTo_univ _ _)\n  have hSc : ContinuousOn\n      (fun m => (1/2)*m*Real.log m + (lagariasC1 - Real.eulerMascheroniConstant/2)*m - 4)\n      (Set.Ici 20) :=\n    (((continuousOn_const.mul continuousOn_id).mul hlog).add\n      (continuousOn_const.mul continuousOn_id)).sub continuousOn_const\n  unfold marginExpanded mFblock mTL1b mTL2b mIdb mL1sqb mL1L2b mL2sqb mL1b mL2b mIIM\n  refine (((((((((((hSc.add\n    ((hF.continuousOn.comp hT mapsTo_sqrt_shift_Ici_Ioi1).const_mul (-2))).add\n    ((contDiffOn_TL1.continuousOn.comp hT hmaps).const_mul _)).add\n    ((contDiffOn_TL2.continuousOn.comp hT hmaps).const_mul _)).add\n    (hT.const_mul _)).add\n    ((contDiffOn_L1sq.continuousOn.comp hT hmaps).const_mul _)).add\n    ((contDiffOn_L1L2.continuousOn.comp hT hmaps).const_mul _)).add\n    ((contDiffOn_L2sq.continuousOn.comp hT hmaps).const_mul _)).add\n    ((contDiffOn_L1.continuousOn.comp hT hmaps).const_mul _)).add\n    ((contDiffOn_L2.continuousOn.comp hT hmaps).const_mul _)).add\n    (hIIMc.const_mul (-1)))).add\n    continuousOn_const\n\n/-- [PROVED session 011] The full margin is C\u00b2 on (20, \u221e). -/",
    "numLines": 40,
    "startLine": 1900,
    "totalLines": 2793
  }
}