BookProof.LimitCircleExample.hasDerivAt_lcLog'

-- Generated from ChapterLimitCircleExample.lean — theorem BookProof.LimitCircleExample.hasDerivAt_lcLog'
import Definitions.Def_ChapterFarisLavine
import Definitions.Def_ChapterScalaronCoreEsa
import Definitions.Def_ChapterScalaronWallEsa
import Definitions.Def_ChapterWallDeficiencyObstruction
import Mathlib
import Definitions.Def_ChapterLimitCircleExample
open BookProof.LimitCircleExample



open MeasureTheory Real
open BookProof.FarisLavine BookProof.ScalaronEsa BookProof.ScalaronWallEsa
open BookProof.WallDeficiencyObstruction

noncomputable section

theorem BookProof.LimitCircleExample.hasDerivAt_lcLog_prime (x : ℝ) :
    HasDerivAt lcLog' (((lcP'' x : ℝ) : ℂ) + Complex.I * ((-x : ℝ) : ℂ)) x := by sorry