# Polar coordinates #

We define polar coordinates, as an open 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`

source
def polarCoord :
OpenPartialHomeomorph (ℝ × ℝ) (ℝ × ℝ)

The polar coordinates open 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

source
@[simp]
theorem polarCoord_apply (q : ℝ × ℝ) :
↑polarCoord q = (√(q.1 ^ 2 + q.2 ^ 2), (Complex.equivRealProd.symm q).arg)
source
@[simp]
theorem polarCoord_symm_apply (p : ℝ × ℝ) :
↑polarCoord.symm p = (p.1 * Real.cos p.2, p.1 * Real.sin p.2)
source
@[simp]
theorem polarCoord_target :
polarCoord.target = Set.Ioi 0 ×ˢ Set.Ioo (-Real.pi) Real.pi
source
@[simp]
theorem polarCoord_source :
polarCoord.source = {q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0}
source
theorem continuous_polarCoord_symm :
Continuous ↑polarCoord.symm
source
def fderivPolarCoordSymm (p : ℝ × ℝ) :
ℝ × ℝ →L[ℝ] ℝ × ℝ

The derivative of `polarCoord.symm`, see `hasFDerivAt_polarCoord_symm`.

Equations

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

Instances For

source
theorem hasFDerivAt_polarCoord_symm (p : ℝ × ℝ) :
HasFDerivAt (↑polarCoord.symm) (fderivPolarCoordSymm p) p
source
theorem det_fderivPolarCoordSymm (p : ℝ × ℝ) :
(fderivPolarCoordSymm p).det = p.1
source
instance instIsAddHaarMeasureProdRealVolume :
MeasureTheory.volume.IsAddHaarMeasure

This instance is required to see through the defeq `volume = volume.prod volume`.

source
theorem polarCoord_source_ae_eq_univ :
polarCoord.source =ᵐ[MeasureTheory.volume] Set.univ
source
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
source
theorem lintegral_comp_polarCoord_symm (f : ℝ × ℝ → ENNReal) :
∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (↑polarCoord.symm p) = ∫⁻ (p : ℝ × ℝ), f p
source
noncomputable def Complex.polarCoord :
OpenPartialHomeomorph ℂ (ℝ × ℝ)

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

Equations

- Complex.polarCoord = Complex.equivRealProdCLM.toHomeomorph.transOpenPartialHomeomorph polarCoord

Instances For

source
theorem Complex.polarCoord_apply (a : ℂ) :
↑Complex.polarCoord a = (‖a‖, a.arg)
source
theorem Complex.polarCoord_source :
Complex.polarCoord.source = slitPlane
source
theorem Complex.polarCoord_target :
Complex.polarCoord.target = Set.Ioi 0 ×ˢ Set.Ioo (-Real.pi) Real.pi
source
@[simp]
theorem Complex.polarCoord_symm_apply (p : ℝ × ℝ) :
↑Complex.polarCoord.symm p = ↑p.1 * (↑(Real.cos p.2) + ↑(Real.sin p.2) * I)
source
theorem Complex.measurableEquivRealProd_symm_polarCoord_symm_apply (p : ℝ × ℝ) :
measurableEquivRealProd.symm (↑polarCoord.symm p) = ↑Complex.polarCoord.symm p
source
theorem Complex.norm_polarCoord_symm (p : ℝ × ℝ) :
‖↑Complex.polarCoord.symm p‖ = |p.1|
source
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
source
theorem Complex.lintegral_comp_polarCoord_symm (f : ℂ → ENNReal) :
∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (↑Complex.polarCoord.symm p) = ∫⁻ (p : ℂ), f p
source
noncomputable def fderivPiPolarCoordSymm {ι : Type u_1} (p : ι → ℝ × ℝ) :
(ι → ℝ × ℝ) →L[ℝ] ι → ℝ × ℝ

The derivative of `polarCoord.symm` on `ι → ℝ × ℝ`, see `hasFDerivAt_pi_polarCoord_symm`.

Equations

- fderivPiPolarCoordSymm p = ContinuousLinearMap.pi fun (i : ι) => (fderivPolarCoordSymm (p i)).comp (ContinuousLinearMap.proj i)

Instances For

source
theorem injOn_pi_polarCoord_symm {ι : Type u_1} :
Set.InjOn (fun (p : ι → ℝ × ℝ) (i : ι) => ↑polarCoord.symm (p i)) (Set.univ.pi fun (x : ι) => polarCoord.target)
source
theorem abs_fst_of_mem_pi_polarCoord_target {ι : Type u_1} {p : ι → ℝ × ℝ} (hp : p ∈ Set.univ.pi fun (x : ι) => polarCoord.target) (i : ι) :
|(p i).1| = (p i).1
source
theorem hasFDerivAt_pi_polarCoord_symm {ι : Type u_1} [Fintype ι] (p : ι → ℝ × ℝ) :
HasFDerivAt (fun (x : ι → ℝ × ℝ) (i : ι) => ↑polarCoord.symm (x i)) (fderivPiPolarCoordSymm p) p
source
theorem det_fderivPiPolarCoordSymm {ι : Type u_1} [Fintype ι] (p : ι → ℝ × ℝ) :
(fderivPiPolarCoordSymm p).det = ∏ i : ι, (p i).1
source
theorem pi_polarCoord_symm_target_ae_eq_univ {ι : Type u_1} [Fintype ι] :
((Pi.map fun (x : ι) => ↑polarCoord.symm) '' Set.univ.pi fun (x : ι) => polarCoord.target) =ᵐ[MeasureTheory.volume] Set.univ
source
theorem measurableSet_pi_polarCoord_target {ι : Type u_1} [Fintype ι] :
MeasurableSet (Set.univ.pi fun (x : ι) => polarCoord.target)
source
theorem integral_comp_pi_polarCoord_symm {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : (ι → ℝ × ℝ) → E) :
(∫ (p : ι → ℝ × ℝ) in Set.univ.pi fun (x : ι) => polarCoord.target, (∏ i : ι, (p i).1) • f fun (i : ι) => ↑polarCoord.symm (p i)) = ∫ (p : ι → ℝ × ℝ), f p
source
theorem Complex.integral_comp_pi_polarCoord_symm {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : (ι → ℂ) → E) :
(∫ (p : ι → ℝ × ℝ) in Set.univ.pi fun (x : ι) => Complex.polarCoord.target, (∏ i : ι, (p i).1) • f fun (i : ι) => ↑Complex.polarCoord.symm (p i)) = ∫ (p : ι → ℂ), f p
source
theorem lintegral_comp_pi_polarCoord_symm {ι : Type u_1} [Fintype ι] (f : (ι → ℝ × ℝ) → ENNReal) :
(∫⁻ (p : ι → ℝ × ℝ) in Set.univ.pi fun (x : ι) => polarCoord.target, (∏ i : ι, ENNReal.ofReal (p i).1) * f fun (i : ι) => ↑polarCoord.symm (p i)) = ∫⁻ (p : ι → ℝ × ℝ), f p
source
theorem Complex.lintegral_comp_pi_polarCoord_symm {ι : Type u_1} [Fintype ι] (f : (ι → ℂ) → ENNReal) :
(∫⁻ (p : ι → ℝ × ℝ) in Set.univ.pi fun (x : ι) => Complex.polarCoord.target, (∏ i : ι, ENNReal.ofReal (p i).1) * f fun (i : ι) => ↑Complex.polarCoord.symm (p i)) = ∫⁻ (p : ι → ℂ), f p