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 = Set.Ioi 0 ×ˢ Set.Ioo (-Real.pi) Real.pi

@[simp]

theorem polarCoord_source : polarCoord.source = {q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0}

@[simp]

theorem polarCoord_symm_apply (p : ℝ × ℝ) : ↑polarCoord.symm p = (p.1 * Real.cos p.2, p.1 * Real.sin p.2)

@[simp]

theorem polarCoord_apply (q : ℝ × ℝ) : ↑polarCoord q = (√(q.1 ^ 2 + q.2 ^ 2), (Complex.equivRealProd.symm q).arg)

def polarCoord : PartialHomeomorph (ℝ × ℝ) (ℝ × ℝ)

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.

theorem hasFDerivAt_polarCoord_symm (p : ℝ × ℝ) : HasFDerivAt (↑polarCoord.symm) (LinearMap.toContinuousLinearMap ((Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ)) (Matrix.of ![![Real.cos p.2, -p.1 * Real.sin p.2], ![Real.sin p.2, p.1 * Real.cos p.2]]))) p

instance instIsAddHaarMeasureProdRealVolume : MeasureTheory.volume.IsAddHaarMeasure

Equations

• instIsAddHaarMeasureProdRealVolume = ⋯

theorem polarCoord_source_ae_eq_univ : polarCoord.source =ᵐ[MeasureTheory.volume] Set.univ

theorem integral_comp_polarCoord_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ × ℝ → E) : ∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (↑polarCoord.symm p) = ∫ (p : ℝ × ℝ), f p

noncomputable def Complex.polarCoord : PartialHomeomorph ℂ (ℝ × ℝ)

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

Equations

• Complex.polarCoord = Complex.equivRealProdCLM.toHomeomorph.transPartialHomeomorph polarCoord

theorem Complex.polarCoord_apply (a : ℂ) : ↑Complex.polarCoord a = (Complex.abs a, a.arg)

theorem Complex.polarCoord_source : Complex.polarCoord.source = Complex.slitPlane

theorem Complex.polarCoord_target : Complex.polarCoord.target = Set.Ioi 0 ×ˢ Set.Ioo (-Real.pi) Real.pi

@[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.polardCoord_symm_abs (p : ℝ × ℝ) : Complex.abs (↑Complex.polarCoord.symm p) = |p.1|

theorem Complex.integral_comp_polarCoord_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℂ → E) : ∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (↑Complex.polarCoord.symm p) = ∫ (p : ℂ), f p