Polar coordinates #
We define polar coordinates, as a local 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_symm_apply
(p : ℝ × ℝ)
:
↑(LocalHomeomorph.symm polarCoord) p = (p.fst * Real.cos p.snd, p.fst * Real.sin p.snd)
@[simp]
@[simp]
theorem
polarCoord_apply
(q : ℝ × ℝ)
:
↑polarCoord q = (Real.sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))
The polar coordinates local homeomorphism in ℝ^2
, mapping (r cos θ, r sin θ)
to (r, θ)
.
It is a homeomorphism between ℝ^2 - (-∞, 0]
and (0, +∞) × (-π, π)
.
Instances For
theorem
hasFDerivAt_polarCoord_symm
(p : ℝ × ℝ)
:
HasFDerivAt (↑(LocalHomeomorph.symm polarCoord))
(↑LinearMap.toContinuousLinearMap
(↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
(↑Matrix.of ![![Real.cos p.snd, -p.fst * Real.sin p.snd], ![Real.sin p.snd, p.fst * Real.cos p.snd]])))
p
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]
[CompleteSpace E]
(f : ℝ × ℝ → E)
:
∫ (p : ℝ × ℝ) in polarCoord.target, p.fst • f (↑(LocalHomeomorph.symm polarCoord) p) = ∫ (p : ℝ × ℝ), f p