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
theorem
hasFDerivAt_polarCoord_symm
(p : ℝ × ℝ)
:
HasFDerivAt (↑polarCoord.symm) (fderivPolarCoordSymm p) p
theorem
integral_comp_polarCoord_symm
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(f : ℝ × ℝ → E)
:
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.integral_comp_polarCoord_symm
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(f : ℂ → E)
:
The derivative of polarCoord.symm
on ι → ℝ × ℝ
, see hasFDerivAt_pi_polarCoord_symm
.
Equations
Instances For
theorem
injOn_pi_polarCoord_symm
{ι : Type u_1}
:
Set.InjOn (fun (p : ι → ℝ × ℝ) (i : ι) => ↑polarCoord.symm (p i)) (Set.univ.pi fun (x : ι) => polarCoord.target)
theorem
hasFDerivAt_pi_polarCoord_symm
{ι : Type u_1}
[Fintype ι]
(p : ι → ℝ × ℝ)
:
HasFDerivAt (fun (x : ι → ℝ × ℝ) (i : ι) => ↑polarCoord.symm (x i)) (fderivPiPolarCoordSymm p) p
theorem
measurableSet_pi_polarCoord_target
{ι : Type u_1}
[Fintype ι]
:
MeasurableSet (Set.univ.pi fun (x : ι) => polarCoord.target)
theorem
integral_comp_pi_polarCoord_symm
{ι : Type u_1}
[Fintype ι]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(f : (ι → ℝ × ℝ) → E)
:
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
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
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