Documentation

Mathlib.Analysis.SpecialFunctions.PolarCoord

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]
theorem polarCoord_source :
polarCoord.source = {q | 0 < q.fst} {q | q.snd 0}
@[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 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