continuousWithinAt_arg_of_re_neg_of_im_zero

English

For θ ∈ ℝ, arg(cos θ + sin θ i) equals θ modulo 2π.

Русский

Для θ ∈ ℝ arg(cos θ + sin θ i) равен θ по модулю 2π.

LaTeX

$$$\\\\arg(\\\\cos\\\\theta + i\\\\sin\\\\theta) = \\\\theta \\\\bmod 2\\\\pi$$$

Lean4

theorem continuousWithinAt_arg_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0) (him : z.im = 0) :
    ContinuousWithinAt arg {z : ℂ | 0 ≤ z.im} z :=
  by
  have : arg =ᶠ[𝓝[{z : ℂ | 0 ≤ z.im}] z] fun x => Real.arcsin ((-x).im / ‖x‖) + π :=
    by
    have : ∀ᶠ x : ℂ in 𝓝 z, x.re < 0 := continuous_re.tendsto z (gt_mem_nhds hre)
    filter_upwards [self_mem_nhdsWithin (s := {z : ℂ | 0 ≤ z.im}), mem_nhdsWithin_of_mem_nhds this] with _ him hre
    rw [arg, if_neg hre.not_ge, if_pos him]
  refine ContinuousWithinAt.congr_of_eventuallyEq ?_ this ?_
  · refine
      (Real.continuousAt_arcsin.comp_continuousWithinAt
            ((continuous_im.continuousAt.comp_continuousWithinAt continuousWithinAt_neg).div
              continuous_norm.continuousWithinAt ?_)).add
        tendsto_const_nhds
    lift z to ℝ using him
    simpa using hre.ne
  · rw [arg, if_neg hre.not_ge, if_pos him.ge]

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