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_target :
polarCoord.target =
@[simp]
theorem polarCoord_source :
polarCoord.source = {q : | 0 < q.1} {q : | q.2 0}
@[simp]
theorem polarCoord_symm_apply (p : ) :
= (p.1 * Real.cos p.2, p.1 * Real.sin p.2)
@[simp]
theorem polarCoord_apply (q : ) :
= ((q.1 ^ 2 + q.2 ^ 2), Complex.arg ( q))

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 (LinearMap.toContinuousLinearMap ( (Matrix.of ![![Real.cos p.2, -p.1 * Real.sin p.2], ![Real.sin p.2, p.1 * Real.cos p.2]]))) p
theorem integral_comp_polarCoord_symm {E : Type u_1} [] (f : E) :
∫ (p : ) in polarCoord.target, p.1 f () = ∫ (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, )
@[simp]
theorem Complex.polarCoord_symm_apply (p : ) :
= p.1 * ((Real.cos p.2) + (Real.sin p.2) * Complex.I)
theorem Complex.polardCoord_symm_abs (p : ) :
Complex.abs = |p.1|
theorem Complex.integral_comp_polarCoord_symm {E : Type u_1} [] (f : E) :
∫ (p : ) in polarCoord.target, p.1 = ∫ (p : ), f p