# Polar coordinates #

We define polar coordinates, as a partial 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_polarCoord_symm): ∫ p in polarCoord.target, p.1 • f (polarCoord.symm p) = ∫ p, f p

@[simp]
theorem polarCoord_apply (q : ) :
= ((q.1 ^ 2 + q.2 ^ 2), ( q).arg)
@[simp]
theorem polarCoord_symm_apply (p : ) :
polarCoord.symm p = (p.1 * Real.cos p.2, p.1 * Real.sin p.2)
@[simp]
theorem polarCoord_source :
polarCoord.source = {q : | 0 < q.1} {q : | q.2 0}
@[simp]
theorem polarCoord_target :
polarCoord.target =

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem hasFDerivAt_polarCoord_symm (p : ) :
HasFDerivAt (polarCoord.symm) (LinearMap.toContinuousLinearMap ( !![Real.cos p.2, -p.1 * Real.sin p.2; Real.sin p.2, p.1 * Real.cos p.2])) p
Equations
theorem polarCoord_source_ae_eq_univ :
polarCoord.source =ᵐ[MeasureTheory.volume] Set.univ
theorem integral_comp_polarCoord_symm {E : Type u_1} [] (f : E) :
∫ (p : ) in polarCoord.target, p.1 f (polarCoord.symm p) = ∫ (p : ), f p
noncomputable def Complex.polarCoord :

The polar coordinates partial homeomorphism in ℂ, mapping r (cos θ + I * sin θ) to (r, θ). It is a homeomorphism between ℂ - ℝ≤0 and (0, +∞) × (-π, π).

Equations
Instances For
theorem Complex.polarCoord_apply (a : ) :
= (Complex.abs a, a.arg)
@[simp]
theorem Complex.polarCoord_symm_apply (p : ) :
Complex.polarCoord.symm p = p.1 * ((Real.cos p.2) + (Real.sin p.2) * Complex.I)
theorem Complex.polarCoord_symm_abs (p : ) :
Complex.abs (Complex.polarCoord.symm p) = |p.1|
@[deprecated Complex.polarCoord_symm_abs]
theorem Complex.polardCoord_symm_abs (p : ) :
Complex.abs (Complex.polarCoord.symm p) = |p.1|

Alias of Complex.polarCoord_symm_abs.

theorem Complex.integral_comp_polarCoord_symm {E : Type u_1} [] (f : E) :
∫ (p : ) in polarCoord.target, p.1 f (Complex.polarCoord.symm p) = ∫ (p : ), f p