English
In the complex plane, the polar coordinate map sends z to (|z|, Arg z) and its inverse sends (r, θ) to r (cos θ + i sin θ).
Русский
В комплексной плоскости полярная карта переводит z в (|z|, Arg z), а обратное отображение — (r, θ) в r( cos θ + i sin θ ).
LaTeX
$$$$ \mathrm{Complex}.\mathrm{polarCoord}(z) = (|z|, \operatorname{arg} z). $$$$
Lean4
/-- The polar coordinates open partial homeomorphism in `ℝ^2`, mapping `(r cos θ, r sin θ)` to
`(r, θ)`. It is a homeomorphism between `ℝ^2 - (-∞, 0]` and `(0, +∞) × (-π, π)`. -/
@[simps]
def polarCoord : OpenPartialHomeomorph (ℝ × ℝ) (ℝ × ℝ)
where
toFun q := (√(q.1 ^ 2 + q.2 ^ 2), Complex.arg (Complex.equivRealProd.symm q))
invFun p := (p.1 * cos p.2, p.1 * sin p.2)
source := {q | 0 < q.1} ∪ {q | q.2 ≠ 0}
target := Ioi (0 : ℝ) ×ˢ Ioo (-π) π
map_target' := by
rintro ⟨r, θ⟩ ⟨hr, hθ⟩
dsimp at hr hθ
rcases eq_or_ne θ 0 with (rfl | h'θ)
· simpa using hr
· right
simp at hr
simpa only [ne_of_gt hr, Ne, mem_setOf_eq, mul_eq_zero, false_or, sin_eq_zero_iff_of_lt_of_lt hθ.1 hθ.2] using h'θ
map_source' := by
rintro ⟨x, y⟩ hxy
simp only [prodMk_mem_set_prod_eq, mem_Ioi, sqrt_pos, mem_Ioo, Complex.neg_pi_lt_arg, true_and,
Complex.arg_lt_pi_iff]
constructor
· rcases hxy with hxy | hxy
· dsimp at hxy; linarith [sq_pos_of_ne_zero hxy.ne', sq_nonneg y]
· linarith [sq_nonneg x, sq_pos_of_ne_zero hxy]
· rcases hxy with hxy | hxy
· exact Or.inl (le_of_lt hxy)
· exact Or.inr hxy
right_inv' := by
rintro ⟨r, θ⟩ ⟨hr, hθ⟩
ext <;> dsimp at hr hθ ⊢
· conv_rhs => rw [← sqrt_sq (le_of_lt hr), ← one_mul (r ^ 2), ← sin_sq_add_cos_sq θ]
congr 1
ring
· convert Complex.arg_mul_cos_add_sin_mul_I hr ⟨hθ.1, hθ.2.le⟩
simp only [Complex.equivRealProd_symm_apply, Complex.ofReal_mul, Complex.ofReal_cos, Complex.ofReal_sin]
ring
left_inv' := by
rintro ⟨x, y⟩ _
have A : √(x ^ 2 + y ^ 2) = ‖x + y * Complex.I‖ := by rw [Complex.norm_def, Complex.normSq_add_mul_I]
have Z := Complex.norm_mul_cos_add_sin_mul_I (x + y * Complex.I)
simp only [← Complex.ofReal_cos, ← Complex.ofReal_sin, mul_add, ← Complex.ofReal_mul, ← mul_assoc] at Z
simp [A]
open_target := isOpen_Ioi.prod isOpen_Ioo
open_source := (isOpen_lt continuous_const continuous_fst).union (isOpen_ne_fun continuous_snd continuous_const)
continuousOn_invFun := by fun_prop
continuousOn_toFun := by
refine .prodMk (by fun_prop) ?_
have A : MapsTo Complex.equivRealProd.symm ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0}) Complex.slitPlane := by
rintro ⟨x, y⟩ hxy; simpa only using hxy
refine ContinuousOn.comp (f := Complex.equivRealProd.symm) (g := Complex.arg) (fun z hz => ?_) ?_ A
· exact (Complex.continuousAt_arg hz).continuousWithinAt
· exact Complex.equivRealProdCLM.symm.continuous.continuousOn
