mathlib documentation

analysis.special_functions.polar_coord

Polar coordinates #

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]
theorem polar_coord_source  :
theorem integral_comp_polar_coord_symm {E : Type u_1} [normed_add_comm_group E] [normed_space E] [complete_space E] (f : × → E) :
∫ (p : × ) in polar_coord.to_local_equiv.target, p.fst f ((polar_coord.symm) p) = ∫ (p : × ), f p