mathlib3 documentation

analysis.special_functions.polar_coord

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]
noncomputable def polar_coord  :

The polar coordinates local homeomorphism in ℝ^2, mapping (r cos θ, r sin θ) to (r, θ). It is a homeomorphism between ℝ^2 - (-∞, 0] and (0, +∞) × (-π, π).

Equations
@[simp]
@[simp]
theorem polar_coord_source  :