feat: Add polar change of coordinates for complex variable (#8034)

Author: xroblot

Mathlib/Analysis/Complex/Basic.lean

@@ -234,6 +234,9 @@ def equivRealProdClm : ℂ ≃L[ℝ] ℝ × ℝ :=
     abs_le_sqrt_two_mul_max (equivRealProd.symm p)
 #align complex.equiv_real_prod_clm Complex.equivRealProdClm
 
+theorem equivRealProdClm_symm_apply (p : ℝ × ℝ) :
+    Complex.equivRealProdClm.symm p = p.1 + p.2 * Complex.I := Complex.equivRealProd_symm_apply p
+
 instance : ProperSpace ℂ :=
   (id lipschitz_equivRealProd : LipschitzWith 1 equivRealProdClm.toHomeomorph).properSpace
 

Mathlib/Analysis/SpecialFunctions/PolarCoord.lean

@@ -3,8 +3,8 @@ Copyright (c) 2022 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
 import Mathlib.MeasureTheory.Function.Jacobian
+import Mathlib.MeasureTheory.Measure.Lebesgue.Complex
 
 #align_import analysis.special_functions.polar_coord from "leanprover-community/mathlib"@"8f9fea08977f7e450770933ee6abb20733b47c92"
 
@@ -19,11 +19,10 @@ It satisfies the following change of variables formula (see `integral_comp_polar
 
 -/
 
-
-noncomputable section
-
 local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220
 
+noncomputable section Real
+
 open Real Set MeasureTheory
 
 open scoped Real Topology
@@ -152,3 +151,44 @@ theorem integral_comp_polarCoord_symm {E : Type*} [NormedAddCommGroup E] [Normed
       rw [B_det, abs_of_pos]
       exact hx.1
 #align integral_comp_polar_coord_symm integral_comp_polarCoord_symm
+
+end Real
+
+noncomputable section Complex
+
+namespace Complex
+
+open scoped Real
+
+/-- The polar coordinates local homeomorphism in `ℂ`, mapping `r (cos θ + I * sin θ)` to `(r, θ)`.
+It is a homeomorphism between `ℂ - ℝ≤0` and `(0, +∞) × (-π, π)`. -/
+protected noncomputable def polarCoord : LocalHomeomorph ℂ (ℝ × ℝ) :=
+  equivRealProdClm.toHomeomorph.toLocalHomeomorph.trans polarCoord
+
+protected theorem polarCoord_apply (a : ℂ) :
+    Complex.polarCoord a = (Complex.abs a, Complex.arg a) := by
+  simp_rw [Complex.abs_def, Complex.normSq_apply, ← pow_two]
+  rfl
+
+protected theorem polarCoord_source :
+    Complex.polarCoord.source = {a | 0 < a.re} ∪ {a | a.im ≠ 0} := by simp [Complex.polarCoord]
+
+protected theorem polarCoord_target :
+    Complex.polarCoord.target = Set.Ioi (0 : ℝ) ×ˢ Set.Ioo (-π) π := by simp [Complex.polarCoord]
+
+@[simp]
+protected theorem polarCoord_symm_apply (p : ℝ × ℝ) :
+    Complex.polarCoord.symm p = p.1 * (Real.cos p.2 + Real.sin p.2 * Complex.I) := by
+  simp [Complex.polarCoord, equivRealProdClm_symm_apply, mul_add, mul_assoc]
+
+theorem polardCoord_symm_abs (p : ℝ × ℝ) :
+    Complex.abs (Complex.polarCoord.symm p) = |p.1| := by simp
+
+protected theorem integral_comp_polarCoord_symm {E : Type*} [NormedAddCommGroup E]
+    [NormedSpace ℝ E] (f : ℂ → E) :
+    (∫ p in polarCoord.target, p.1 • f (Complex.polarCoord.symm p)) = ∫ p, f p := by
+  rw [← (Complex.volume_preserving_equiv_real_prod.symm).integral_comp
+    measurableEquivRealProd.symm.measurableEmbedding, ← integral_comp_polarCoord_symm]
+  rfl
+
+end Complex

Mathlib/Data/Complex/Module.lean

@@ -289,6 +289,9 @@ def equivRealProdAddHom : ℂ ≃+ ℝ × ℝ :=
   { equivRealProd with map_add' := by simp }
 #align complex.equiv_real_prod_add_hom Complex.equivRealProdAddHom
 
+theorem equivRealProdAddHom_symm_apply (p : ℝ × ℝ) :
+    Complex.equivRealProdAddHom.symm p = p.1 + p.2 * Complex.I := Complex.equivRealProd_symm_apply p
+
 /-- The natural `LinearEquiv` from `ℂ` to `ℝ × ℝ`. -/
 @[simps! (config := { simpRhs := true }) apply symm_apply_re symm_apply_im]
 def equivRealProdLm : ℂ ≃ₗ[ℝ] ℝ × ℝ :=
@@ -297,6 +300,8 @@ def equivRealProdLm : ℂ ≃ₗ[ℝ] ℝ × ℝ :=
     map_smul' := fun r c => by simp [equivRealProdAddHom, (Prod.smul_def), smul_eq_mul] }
 #align complex.equiv_real_prod_lm Complex.equivRealProdLm
 
+theorem equivRealProdLm_symm_apply (p : ℝ × ℝ) :
+    Complex.equivRealProdLm.symm p = p.1 + p.2 * Complex.I := Complex.equivRealProd_symm_apply p
 section lift
 
 variable {A : Type*} [Ring A] [Algebra ℝ A]

Mathlib/MeasureTheory/Measure/Lebesgue/Complex.lean

@@ -3,9 +3,7 @@ Copyright (c) 2021 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Analysis.SpecialFunctions.Integrals
 import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
-import Mathlib.MeasureTheory.Measure.Lebesgue.Integral
 
 #align_import measure_theory.measure.lebesgue.complex from "leanprover-community/mathlib"@"fd5edc43dc4f10b85abfe544b88f82cf13c5f844"