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 : ℝ × ℝ) : ↑(PartialHomeomorph.symm polarCoord) p = (p.1 * Real.cos p.2, p.1 * Real.sin p.2)

@[simp]

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

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 (↑(PartialHomeomorph.symm polarCoord)) (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 instIsAddHaarMeasureProdRealInstAddGroupInstAddGroupRealInstTopologicalSpaceProdToTopologicalSpaceToUniformSpacePseudoMetricSpaceToMeasurableSpaceMeasureSpaceMeasureSpaceVolume : MeasureTheory.Measure.IsAddHaarMeasure MeasureTheory.volume

Equations

• One or more equations did not get rendered due to their size.

theorem polarCoord_source_ae_eq_univ : polarCoord.source =ᶠ[MeasureTheory.Measure.ae 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 (↑(PartialHomeomorph.symm polarCoord) 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 = Homeomorph.transPartialHomeomorph (ContinuousLinearEquiv.toHomeomorph Complex.equivRealProdCLM) polarCoord

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

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 : ℝ × ℝ) : ↑(PartialHomeomorph.symm Complex.polarCoord) p = ↑p.1 * (↑(Real.cos p.2) + ↑(Real.sin p.2) * Complex.I)

theorem Complex.polardCoord_symm_abs (p : ℝ × ℝ) : Complex.abs (↑(PartialHomeomorph.symm Complex.polarCoord) 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 (↑(PartialHomeomorph.symm Complex.polarCoord) p) = ∫ (p : ℂ), f p