Documentation

Mathlib.Analysis.SpecialFunctions.PolarCoord

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_source :
polarCoord.source = {q : × | 0 < q.1} {q : × | q.2 0}
@[simp]
@[simp]
theorem polarCoord_apply (q : × ) :
polarCoord q = (Real.sqrt (q.1 ^ 2 + q.2 ^ 2), Complex.arg (Complex.equivRealProd.symm q))

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.
Instances For
    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
    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

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

    Equations
    Instances For
      theorem Complex.polarCoord_apply (a : ) :
      Complex.polarCoord a = (Complex.abs a, Complex.arg a)
      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