1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57
58. 58
59. 59
60. 60
61. 61
62. 62
63. 63
64. 64
65. 65
66. 66
67. 67
68. 68
69. 69
70. 70
71. 71
72. 72
73. 73
74. 74
75. 75
76. 76
77. 77
78. 78
79. 79
80. 80
81. 81
82. 82
83. 83
84. 84
85. 85
86. 86
87. 87
88. 88
89. 89
90. 90
91. 91
92. 92
93. 93
94. 94
95. 95
96. 96
97. 97
98. 98
99. 99
100. 100
101. 101
102. 102
103. 103
104. 104
105. 105
106. 106
107. 107
108. 108
109. 109

/-
Copyright (c) 2025 Anthony Wang. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Anthony Wang
-/
import Mathlib

/-!
# Spherical coordinates

We define spherical coordinates similarly to polar coordinates, as an open partial homeomorphism
in `ℝ^3` between `ℝ^3 - (-∞, 0]` and `(0, +∞) × (-π, π) × (0, π)`. Its inverse is given by
`(r, θ, φ) ↦ (r sin φ cos θ, r sin φ sin θ, r cos φ)`. TODO

It satisfies the following change of variables formula (see `integral_comp_sphericalCoord_symm`):
`∫ p in sphericalCoord.target, p.1 • f (sphericalCoord.symm p) = ∫ p, f p`

-/

theorem arg_of_im_pos' {z : ℂ} (hz : 0 < z.im) : 0 < Complex.arg z := by
  have h₀ : z ≠ 0 := Ne.symm (mt (congr_arg Complex.im) hz.ne)
  suffices 0 < Real.sin z.arg by
    contrapose! this
    exact Real.sin_nonpos_of_nonnpos_of_neg_pi_le this (by linarith [Complex.neg_pi_lt_arg z])
  simp only [Complex.sin_arg, lt_div_iff₀ (norm_pos_iff.mpr h₀), zero_mul, hz]


noncomputable section Real

open Real Set MeasureTheory

open scoped ENNReal Real Topology

/-- The spherical coordinates are an open partial homeomorphism in `ℝ^3`, mapping `(r sin φ cos θ, r sin φ sin θ, r cos φ)` to
`(r, θ, φ)`. It is a homeomorphism between `ℝ^3 - (-∞, 0]` and `(0, +∞) × (-π, π) × (0, π)`. TODO -/
def sphericalCoord : PartialHomeomorph (ℝ × ℝ × ℝ) (ℝ × ℝ × ℝ) where
  toFun q := (√(q.1 ^ 2 + q.2.1 ^ 2 + q.2.2 ^ 2), Complex.arg (Complex.equivRealProd.symm (q.1, q.2.1)), Complex.arg (Complex.equivRealProd.symm (q.2.2, √(q.1 ^ 2 + q.2.1 ^ 2))))
  invFun p := (p.1 * sin p.2.2 * cos p.2.1, p.1 * sin p.2.2 * sin p.2.1, p.1 * cos p.2.2)
  source := {q | 0 < q.1} ∪ {q | q.2.1 ≠ 0}
  target := Ioi (0 : ℝ) ×ˢ Ioo (-π) π ×ˢ Ioo 0 π
  map_target' := by
    rintro ⟨r, θ, φ⟩ ⟨hr, hθ, hφ⟩
    dsimp at hr hθ hφ
    rcases eq_or_ne θ 0 with (rfl | h'θ)
    · simp only [ne_eq, cos_zero, mul_one, sin_zero, mul_zero, mem_union, mem_setOf_eq]
      left
      exact Left.mul_pos hr (sin_pos_of_mem_Ioo hφ)
    · simp only [ne_eq, mem_union, mem_setOf_eq, mul_eq_zero, not_or]
      right
      and_intros
      · linarith [mem_Ioi.mp hr]
      · linarith [sin_pos_of_mem_Ioo hφ]
      · simp [sin_eq_zero_iff_of_lt_of_lt hθ.1 hθ.2, h'θ]
  map_source' := by
    rintro ⟨x, y, z⟩ hxy
    simp only [prodMk_mem_set_prod_eq, mem_Ioi, sqrt_pos, mem_Ioo, Complex.neg_pi_lt_arg,
      true_and, Complex.arg_lt_pi_iff]
    simp
    have hpos : 0 < x ^ 2 + y ^ 2 := by
      rcases hxy with hxy | hxy
      · dsimp at hxy; linarith [sq_pos_of_ne_zero hxy.ne', sq_nonneg y]
      · linarith [sq_nonneg x, sq_pos_of_ne_zero hxy]
    and_intros
    · rcases hxy with hxy | hxy
      · dsimp at hxy; linarith [sq_pos_of_ne_zero hxy.ne', sq_nonneg y, sq_nonneg z]
      · linarith [sq_nonneg x, sq_pos_of_ne_zero hxy, sq_nonneg z]
    · rcases hxy with hxy | hxy
      · exact Or.inl (le_of_lt hxy)
      · exact Or.inr hxy
    · apply arg_of_im_pos'
      simp [hpos]
    · exact Or.inr (by simp only [sqrt_ne_zero', hpos])
  right_inv' := by
    rintro ⟨r, θ, φ⟩ ⟨hr, hθ, hφ⟩
    ext <;> dsimp at hr hθ hφ ⊢
    · conv_rhs => rw [← sqrt_sq (le_of_lt hr), ← one_mul (r ^ 2), ← sin_sq_add_cos_sq φ, ← one_mul (sin φ ^ 2), ← sin_sq_add_cos_sq θ]
      congr 1
      ring
    · convert Complex.arg_mul_cos_add_sin_mul_I (Left.mul_pos hr (sin_pos_of_mem_Ioo hφ)) ⟨hθ.1, hθ.2.le⟩
      simp only [Complex.equivRealProd_symm_apply, Complex.ofReal_mul, Complex.ofReal_sin,
        Complex.ofReal_cos]
      ring
    · have : -π < φ := by linarith [pi_pos, hφ.1]
      convert Complex.arg_mul_cos_add_sin_mul_I hr ⟨this, hφ.2.le⟩
      have : √((r * sin φ * cos θ) ^ 2 + (r * sin φ * sin θ) ^ 2) = r * sin φ := by
        conv_rhs => rw [← sqrt_sq (le_of_lt (Left.mul_pos hr (sin_pos_of_mem_Ioo hφ))), ← one_mul ((r * sin φ) ^ 2), ← sin_sq_add_cos_sq θ]
        congr 1
        ring
      simp only [this, Complex.equivRealProd_symm_apply, Complex.ofReal_mul, Complex.ofReal_cos,
        Complex.ofReal_sin]
      ring
  left_inv' := by
    rintro ⟨x, y, z⟩ _
    -- have A : √(x ^ 2 + y ^ 2) = ‖x + y * Complex.I‖ := by
    --   rw [Complex.norm_def, Complex.normSq_add_mul_I]
    -- have B : √(x ^ 2 + y ^ 2 + z ^ 2) = ‖z + √(x ^ 2 + y ^ 2) * Complex.I‖ := by
    --   rw [Complex.norm_def, Complex.normSq_add_mul_I]
    simp -- [Complex.sin_arg]
    and_intros
    · sorry
    · sorry
    · sorry
  open_target := isOpen_Ioi.prod (isOpen_Ioo.prod isOpen_Ioo)
  open_source :=
    (isOpen_lt continuous_const continuous_fst).union
      (isOpen_ne_fun (Continuous.fst continuous_snd) continuous_const)
  continuousOn_invFun := by fun_prop
  continuousOn_toFun := by
    sorry