mathlib3 documentation


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, p.1 • f (polar_coord.symm p) = ∫ p, f p

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, +∞) × (-π, π).

theorem polar_coord_source  :