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

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.

@[simp]

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

@[simp]

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

@[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}

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

theorem det_fderiv_polarCoord_symm (p : ℝ × ℝ) : (LinearMap.toContinuousLinearMap ((Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ)) !![Real.cos p.2, -p.1 * Real.sin p.2; Real.sin p.2, p.1 * Real.cos p.2])).det = p.1

instance instIsAddHaarMeasureProdRealVolume : MeasureTheory.volume.IsAddHaarMeasure

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

theorem lintegral_comp_polarCoord_symm (f : ℝ × ℝ → ENNReal) : ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal 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.measurableEquivRealProd_symm_polarCoord_symm_apply (p : ℝ × ℝ) : Complex.measurableEquivRealProd.symm (↑polarCoord.symm p) = ↑Complex.polarCoord.symm p

theorem Complex.polarCoord_symm_abs (p : ℝ × ℝ) : Complex.abs (↑Complex.polarCoord.symm p) = |p.1|

@[deprecated Complex.polarCoord_symm_abs (since := "2024-07-15")]

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} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℂ → E) : ∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (↑Complex.polarCoord.symm p) = ∫ (p : ℂ), f p

theorem Complex.lintegral_comp_polarCoord_symm (f : ℂ → ENNReal) : ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (↑Complex.polarCoord.symm p) = ∫⁻ (p : ℂ), f p