`BookProof.LimitCircleExample.lcLog_ode` (x : ℝ) : (((lcP'' x : ℝ) : ℂ) + Complex.I * ((-x : ℝ) : ℂ)) + lcLog' x ^ 2 = ((lcV x : ℝ) : ℂ) - Complex.I

Proved

BookProof.LimitCircleExample.lcLog_ode

by leonardopedro · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterLimitCircleExample.

BookProof.LimitCircleExample.lcLog_ode (x : ℝ) : (((lcP'' x : ℝ) : ℂ) + Complex.I * ((-x : ℝ) : ℂ)) + lcLog' x ^ 2 = ((lcV x : ℝ) : ℂ) - Complex.I

Formalization note: Lean 4 identifier BookProof.LimitCircleExample.lcLog_ode.

Preamble

-- Generated from ChapterLimitCircleExample.lean — theorem BookProof.LimitCircleExample.lcLog_ode
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

Formal statement

theorem BookProof.LimitCircleExample.lcLog_ode (x : ℝ) :
    (((lcP'' x : ℝ) : ℂ) + Complex.I * ((-x : ℝ) : ℂ)) + lcLog' x ^ 2
      = ((lcV x : ℝ) : ℂ) - Complex.I := by sorry

View graph