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

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

The polar coordinates are an open partial homeomorphism in ℝ^2, mapping (r cos θ, r sin θ) to (r, θ). It is a homeomorphism between ℝ^2 - (-∞, 0] and (0, +∞) × (-π, π).

@[simp]

theorem polarCoord_target : polarCoord.target = Set.Ioi 0 ×ˢ Set.Ioo (-Real.pi) Real.pi

@[simp]

theorem polarCoord_symm_apply (p : ℝ × ℝ) : ↑polarCoord.symm p = (p.1 * Real.cos p.2, p.1 * Real.sin p.2)

@[simp]

theorem polarCoord_apply (q : ℝ × ℝ) : ↑polarCoord q = (√(q.1 ^ 2 + q.2 ^ 2), (Complex.equivRealProd.symm q).arg)

@[simp]

theorem polarCoord_source : polarCoord.source = {q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0}

theorem continuous_polarCoord_symm : Continuous ↑polarCoord.symm

noncomputable def fderivPolarCoordSymm (p : ℝ × ℝ) : ℝ × ℝ →L[ℝ] ℝ × ℝ

The derivative of polarCoord.symm, see hasFDerivAt_polarCoord_symm.

theorem hasFDerivAt_polarCoord_symm (p : ℝ × ℝ) : HasFDerivAt (↑polarCoord.symm) (fderivPolarCoordSymm p) p

theorem det_fderivPolarCoordSymm (p : ℝ × ℝ) : (fderivPolarCoordSymm p).det = p.1

instance instIsAddHaarMeasureProdRealVolume : MeasureTheory.volume.IsAddHaarMeasure

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

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

theorem lintegral_comp_polarCoord_symm (f : ℝ × ℝ → ENNReal) : ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (↑polarCoord.symm p) = ∫⁻ (p : ℝ × ℝ), f p

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, +∞) × (-π, π).

theorem Complex.polarCoord_apply (a : ℂ) : ↑Complex.polarCoord a = (‖a‖, a.arg)

theorem Complex.polarCoord_source : Complex.polarCoord.source = slitPlane

theorem Complex.polarCoord_target : Complex.polarCoord.target = Set.Ioi 0 ×ˢ Set.Ioo (-Real.pi) Real.pi

@[simp]

theorem Complex.polarCoord_symm_apply (p : ℝ × ℝ) : ↑Complex.polarCoord.symm p = ↑p.1 * (↑(Real.cos p.2) + ↑(Real.sin p.2) * I)

theorem Complex.measurableEquivRealProd_symm_polarCoord_symm_apply (p : ℝ × ℝ) : measurableEquivRealProd.symm (↑polarCoord.symm p) = ↑Complex.polarCoord.symm p

theorem Complex.norm_polarCoord_symm (p : ℝ × ℝ) : ‖↑Complex.polarCoord.symm p‖ = |p.1|

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

theorem Complex.lintegral_comp_polarCoord_symm (f : ℂ → ENNReal) : ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (↑Complex.polarCoord.symm p) = ∫⁻ (p : ℂ), f p

noncomputable def fderivPiPolarCoordSymm {ι : Type u_1} (p : ι → ℝ × ℝ) : (ι → ℝ × ℝ) →L[ℝ] ι → ℝ × ℝ

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

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 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

theorem hasFDerivAt_pi_polarCoord_symm {ι : Type u_1} [Finite ι] (p : ι → ℝ × ℝ) : HasFDerivAt (fun (x : ι → ℝ × ℝ) (i : ι) => ↑polarCoord.symm (x i)) (fderivPiPolarCoordSymm p) p

theorem measurableSet_pi_polarCoord_target {ι : Type u_1} [Finite ι] : MeasurableSet (Set.univ.pi fun (x : ι) => polarCoord.target)

theorem det_fderivPiPolarCoordSymm {ι : Type u_1} [Fintype ι] (p : ι → ℝ × ℝ) : (fderivPiPolarCoordSymm p).det = ∏ i : ι, (p i).1

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

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

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