expPartialHomeomorph — Mathlib

English

There exists a partial open bijection between the horizontal strip {z ∈ ℂ : -π < Im z < π} and the slit plane, given by exp with inverse log on the respective domains.

Русский

Существует частичное открытое биекция между горизонтальной полосой {z ∈ ℂ : -π < Im z < π} и разрезанной плоскостью, заданная экспонентой с логарифмом в качестве обратной на соответствующих областях.

LaTeX

$$$$ \expPartialHomeomorph : \text{OpenPartialHomeomorph}(\mathbb{C}, \mathbb{C}) \text{ with source } \{ z \in \mathbb{C} \mid -\pi < \mathrm{Im}(z) < \pi \},\; target = \mathrm{slitPlane},\; \text{toFun} = \exp,\; \text{invFun} = \log. $$$$

Lean4

/-- `Complex.exp` as an `OpenPartialHomeomorph` with `source = {z | -π < im z < π}` and
`target = {z | 0 < re z} ∪ {z | im z ≠ 0}`. This definition is used to prove that `Complex.log`
is complex differentiable at all points but the negative real semi-axis. -/
noncomputable def expPartialHomeomorph : OpenPartialHomeomorph ℂ ℂ :=
  OpenPartialHomeomorph.ofContinuousOpen
    { toFun := exp
      invFun := log
      source := {z : ℂ | z.im ∈ Ioo (-π) π}
      target := slitPlane
      map_source' := by
        rintro ⟨x, y⟩ ⟨h₁ : -π < y, h₂ : y < π⟩
        refine (not_or_of_imp fun hz => ?_).symm
        obtain rfl : y = 0 := by
          rw [exp_im] at hz
          simpa [(Real.exp_pos _).ne', Real.sin_eq_zero_iff_of_lt_of_lt h₁ h₂] using hz
        rw [← ofReal_def, exp_ofReal_re]
        exact Real.exp_pos x
      map_target' := fun z h =>
        by
        simp only [mem_setOf, log_im, mem_Ioo, neg_pi_lt_arg, arg_lt_pi_iff, true_and]
        exact h.imp_left le_of_lt
      left_inv' := fun _ hx => log_exp hx.1 (le_of_lt hx.2)
      right_inv' := fun _ hx => exp_log <| slitPlane_ne_zero hx } continuous_exp.continuousOn isOpenMap_exp
    (isOpen_Ioo.preimage continuous_im)

Похожие утверждения