Complex curve log lift
ProvedBirkhoffGlobalSection.complex_curve_log_liftdifferential-geometryreal-analysis
Every continuous nonvanishing complex curve on the real line has a continuous complex logarithm with any prescribed compatible value at time zero.
All displayed regularity, tangency, normalization and supplied-data hypotheses of the exact formal statement are retained.
Preamble
import Theorems.Thm_BirkhoffGlobalSection_contact_angular_lift_bundle open BirkhoffGlobalSection Set Filter Topology open scoped ContDiff Topology set_option linter.unusedVariables false set_option autoImplicit false set_option maxHeartbeats 800000
Formal statement
theorem BirkhoffGlobalSection.complex_curve_log_lift :
∀ (z : ℝ → ℂ) (hz : Continuous z)
(hne : ∀ t, z t ≠ 0) (a : ℂ) (ha : Complex.exp a = z 0),
∃ f : ℝ → ℂ, Continuous f ∧ f 0 = a ∧ ∀ t, Complex.exp (f t) = z t := by sorrySource
Independent extraction of component 1 of the Proved theorem BirkhoffGlobalSection.contact_angular_lift_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_contact_angular_lift_bundle.lean. Exact original component retained.