Prove2Me

Complex plane parameter log lift

Proved
BirkhoffGlobalSection.complex_plane_parameter_log_lift

by Mazecto · Oct 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

differential-geometryreal-analysis

A continuous nonvanishing complex function on the real parameter plane admits a continuous complex logarithm with any compatible prescribed value at the origin.

All displayed regularity, tangency, normalization and supplied-data hypotheses of the exact formal statement are retained.

Preamble
import Theorems.Thm_BirkhoffGlobalSection_contact_winding_interval_bundle

open BirkhoffGlobalSection Set Filter Topology
open scoped ContDiff Topology

set_option maxHeartbeats 800000
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_plane_parameter_log_lift :
∀ (z : ℝ × ℝ → ℂ) (hz : Continuous z)
    (hne : ∀ x, z x ≠ 0) (a : ℂ) (ha : Complex.exp a = z (0, 0)),
    ∃ f : ℝ × ℝ → ℂ, Continuous f ∧ f (0, 0) = a ∧
      ∀ x, Complex.exp (f x) = z x := by sorry
Source
Independent extraction of component 1 of the Proved theorem BirkhoffGlobalSection.contact_winding_interval_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_contact_winding_interval_bundle.lean. Exact original component retained.

View graph