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_apply (q : × ) :
polarCoord q = ((q.1 ^ 2 + q.2 ^ 2), (Complex.equivRealProd.symm q).arg)
@[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}

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 (↑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
    instance instIsAddHaarMeasureProdRealVolume :
    MeasureTheory.volume.IsAddHaarMeasure
    Equations
    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

    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, a.arg)
      @[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.polarCoord_symm_abs (p : × ) :
      Complex.abs (Complex.polarCoord.symm p) = |p.1|
      @[deprecated Complex.polarCoord_symm_abs]
      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