feat: a few lemmata about ℂ (#30305)

These are useful for facts about unitary elements in C⋆-algebras.

Author: j-loreaux

Mathlib/Analysis/Complex/Basic.lean

@@ -627,6 +627,18 @@ lemma ball_one_subset_slitPlane : Metric.ball 1 1 ⊆ slitPlane := fun z hz ↦
 lemma mem_slitPlane_of_norm_lt_one {z : ℂ} (hz : ‖z‖ < 1) : 1 + z ∈ slitPlane :=
   ball_one_subset_slitPlane <| by simpa
 
+open Metric in
+/-- A subset of the circle centered at the origin in `ℂ` of radius `r` is a subset of
+the `slitPlane` if it does not contain `-r`. -/
+lemma subset_slitPlane_iff_of_subset_sphere {r : ℝ} {s : Set ℂ} (hs : s ⊆ sphere 0 r) :
+    s ⊆ slitPlane ↔ (-r : ℂ) ∉ s := by
+  simp_rw +singlePass [← not_iff_not, Set.subset_def, mem_slitPlane_iff_not_le_zero]
+  push ¬ _
+  refine ⟨?_, fun hr ↦ ⟨_, hr, by simpa using hs hr⟩⟩
+  rintro ⟨z, hzs, hz⟩
+  have : ‖z‖ = r := by simpa using hs hzs
+  simpa [← this, ← norm_neg z ▸ eq_coe_norm_of_nonneg (neg_nonneg.mpr hz)]
+
 end slitPlane
 
 lemma _root_.IsCompact.reProdIm {s t : Set ℝ} (hs : IsCompact s) (ht : IsCompact t) :

Mathlib/Analysis/Complex/Norm.lean

@@ -354,4 +354,27 @@ lemma re_neg_ne_zero_of_re_pos {s : ℂ} (hs : 0 < s.re) : (-s).re ≠ 0 :=
 lemma re_neg_ne_zero_of_one_lt_re {s : ℂ} (hs : 1 < s.re) : (-s).re ≠ 0 :=
   re_neg_ne_zero_of_re_pos <| zero_lt_one.trans hs
 
+lemma norm_sub_one_sq_eq_of_norm_one {z : ℂ} (hz : ‖z‖ = 1) :
+    ‖z - 1‖ ^ 2 = 2 * (1 - z.re) := by
+  have : z.im * z.im = 1 - z.re * z.re := by
+    replace hz := sq_eq_one_iff.mpr (.inl hz)
+    rw [Complex.sq_norm, normSq_apply] at hz
+    linarith
+  simp [Complex.sq_norm, normSq_apply, this]
+  ring
+
+lemma norm_sub_one_sq_eqOn_sphere :
+    (Metric.sphere (0 : ℂ) 1).EqOn (‖· - 1‖ ^ 2) (fun z ↦ 2 * (1 - z.re)) :=
+  fun z hz ↦ norm_sub_one_sq_eq_of_norm_one (by simpa using hz)
+
+lemma normSq_ofReal_add_I_mul_sqrt_one_sub {x : ℝ} (hx : ‖x‖ ≤ 1) :
+    normSq (x + I * √(1 - x ^ 2)) = 1 := by
+  simp [mul_comm I, normSq_add_mul_I,
+    Real.sq_sqrt (x := 1 - x ^ 2) (by nlinarith [abs_le.mp hx])]
+
+lemma normSq_ofReal_sub_I_mul_sqrt_one_sub {x : ℝ} (hx : ‖x‖ ≤ 1) :
+    normSq (x - I * √(1 - x ^ 2)) = 1 := by
+  rw [← normSq_neg, neg_sub', sub_neg_eq_add]
+  simpa using normSq_ofReal_add_I_mul_sqrt_one_sub (x := -x) (by simpa)
+
 end Complex

Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean

@@ -574,6 +574,10 @@ theorem continuousAt_arg (h : x ∈ slitPlane) : ContinuousAt arg x := by
           (continuous_re.continuousAt.div continuous_norm.continuousAt h₀)).congr
       (arg_eq_nhds_of_im_pos hx_im).symm]
 
+@[fun_prop]
+theorem continuousOn_arg : ContinuousOn arg slitPlane :=
+  fun _ h ↦ continuousAt_arg h |>.continuousWithinAt
+
 theorem tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0)
     (him : z.im = 0) : Tendsto arg (𝓝[{ z : ℂ | z.im < 0 }] z) (𝓝 (-π)) := by
   suffices H : Tendsto (fun x : ℂ => Real.arcsin ((-x).im / ‖x‖) - π)