Polar coordinates #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We define polar coordinates, as a local homeomorphism in ℝ^2 between ℝ^2 - (-∞, 0] and
(0, +∞) × (-π, π). Its inverse is given by (r, θ) ↦ (r cos θ, r sin θ).
It satisfies the following change of variables formula (see integral_comp_polar_coord_symm):
∫ p in polar_coord.target, p.1 • f (polar_coord.symm p) = ∫ p, f p
@[simp]
The polar coordinates local homeomorphism in ℝ^2, mapping (r cos θ, r sin θ) to (r, θ).
It is a homeomorphism between ℝ^2 - (-∞, 0] and (0, +∞) × (-π, π).
Equations
- polar_coord = {to_local_equiv := {to_fun := λ (q : ℝ × ℝ), (√ (q.fst ^ 2 + q.snd ^ 2), (⇑(complex.equiv_real_prod.symm) q).arg), inv_fun := λ (p : ℝ × ℝ), (p.fst * real.cos p.snd, p.fst * real.sin p.snd), source := {q : ℝ × ℝ | 0 < q.fst} ∪ {q : ℝ × ℝ | q.snd ≠ 0}, target := set.Ioi 0 ×ˢ set.Ioo (-real.pi) real.pi, map_source' := polar_coord._proof_1, map_target' := polar_coord._proof_2, left_inv' := polar_coord._proof_3, right_inv' := polar_coord._proof_4}, open_source := polar_coord._proof_5, open_target := polar_coord._proof_6, continuous_to_fun := polar_coord._proof_7, continuous_inv_fun := polar_coord._proof_8}
theorem
has_fderiv_at_polar_coord_symm
(p : ℝ × ℝ) :
has_fderiv_at ⇑(polar_coord.symm) (⇑linear_map.to_continuous_linear_map (⇑(matrix.to_lin (basis.fin_two_prod ℝ) (basis.fin_two_prod ℝ)) (⇑matrix.of ![![real.cos p.snd, -p.fst * real.sin p.snd], ![real.sin p.snd, p.fst * real.cos p.snd]]))) p
theorem
integral_comp_polar_coord_symm
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
(f : ℝ × ℝ → E) :