Polar coordinates #

We define polar coordinates, as a local 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

@[simp]

theorem polarCoord_symm_apply (p : ℝ × ℝ) :

↑(LocalHomeomorph.symm polarCoord) p = (p.fst * Real.cos p.snd, p.fst * Real.sin p.snd)

source

@[simp]

theorem polarCoord_source :

polarCoord.source = {q | 0 < q.fst} ∪ {q | q.snd ≠ 0}

source

@[simp]

theorem polarCoord_target :

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

source

@[simp]

theorem polarCoord_apply (q : ℝ × ℝ) :

↑polarCoord q = (Real.sqrt (q.fst ^ 2 + q.snd ^ 2), Complex.arg (↑Complex.equivRealProd.symm q))

source

def polarCoord :

LocalHomeomorph (ℝ × ℝ) (ℝ × ℝ)

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

Instances For

source

theorem hasFDerivAt_polarCoord_symm (p : ℝ × ℝ) :

HasFDerivAt (↑(LocalHomeomorph.symm polarCoord)) (↑LinearMap.toContinuousLinearMap (↑(Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ)) (↑Matrix.of ![![Real.cos p.snd, -p.fst * Real.sin p.snd], ![Real.sin p.snd, p.fst * Real.cos p.snd]]))) p

source

instance instIsAddHaarMeasureProdRealInstAddGroupInstAddGroupRealInstTopologicalSpaceProdToTopologicalSpaceToUniformSpacePseudoMetricSpaceToMeasurableSpaceMeasureSpaceMeasureSpaceVolume :

MeasureTheory.Measure.IsAddHaarMeasure MeasureTheory.volume

source

theorem polarCoord_source_ae_eq_univ :

polarCoord.source =ᶠ[MeasureTheory.Measure.ae MeasureTheory.volume] Set.univ

source

theorem integral_comp_polarCoord_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (f : ℝ × ℝ → E) :

∫ (p : ℝ × ℝ) in polarCoord.target, p.fst • f (↑(LocalHomeomorph.symm polarCoord) p) = ∫ (p : ℝ × ℝ), f p