From d862c6bbd4792026a50e87991e87371c956c167d Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sun, 28 Dec 2025 19:17:40 -0600 Subject: [PATCH 1/6] feat: define `Complex.UnitDisc.shift` --- Mathlib/Analysis/Complex/UnitDisc/Basic.lean | 107 ++++++++---- Mathlib/Analysis/Complex/UnitDisc/Shift.lean | 172 +++++++++++++++++++ 2 files changed, 242 insertions(+), 37 deletions(-) create mode 100644 Mathlib/Analysis/Complex/UnitDisc/Shift.lean diff --git a/Mathlib/Analysis/Complex/UnitDisc/Basic.lean b/Mathlib/Analysis/Complex/UnitDisc/Basic.lean index bd1f33f30887b8..7eeeaa12d68fdd 100644 --- a/Mathlib/Analysis/Complex/UnitDisc/Basic.lean +++ b/Mathlib/Analysis/Complex/UnitDisc/Basic.lean @@ -17,20 +17,18 @@ introduce some basic operations on this disc. @[expose] public section - open Set Function Metric +open scoped ComplexConjugate noncomputable section -local notation "conj'" => starRingEnd β„‚ - namespace Complex /-- The complex unit disc, denoted as `𝔻` withinin the Complex namespace -/ def UnitDisc : Type := ball (0 : β„‚) 1 deriving TopologicalSpace -@[inherit_doc] scoped[UnitDisc] notation "𝔻" => Complex.UnitDisc +@[inherit_doc] scoped[Complex.UnitDisc] notation "𝔻" => Complex.UnitDisc open UnitDisc namespace UnitDisc @@ -44,6 +42,7 @@ instance instIsCancelMulZero : IsCancelMulZero UnitDisc := by unfold UnitDisc; i instance instHasDistribNeg : HasDistribNeg UnitDisc := by unfold UnitDisc; infer_instance instance instCoe : Coe UnitDisc β„‚ := ⟨UnitDisc.coe⟩ +@[ext] theorem coe_injective : Injective ((↑) : 𝔻 β†’ β„‚) := Subtype.coe_injective @@ -73,11 +72,25 @@ theorem one_add_coe_ne_zero (z : 𝔻) : (1 + z : β„‚) β‰  0 := theorem coe_mul (z w : 𝔻) : ↑(z * w) = (z * w : β„‚) := rfl +@[simp, norm_cast] +theorem coe_neg (z : 𝔻) : ↑(-z) = (-z : β„‚) := rfl + /-- A constructor that assumes `β€–zβ€– < 1` instead of `dist z 0 < 1` and returns an element of `𝔻` instead of `β†₯Metric.ball (0 : β„‚) 1`. -/ def mk (z : β„‚) (hz : β€–zβ€– < 1) : 𝔻 := ⟨z, mem_ball_zero_iff.2 hz⟩ +/-- A cases eliminator that makes `cases z` use `UnitDisc.mk` instead of `Subtype.mk`. -/ +@[elab_as_elim, cases_eliminator] +protected def casesOn {motive : 𝔻 β†’ Sort*} (mk : βˆ€ z hz, motive (.mk z hz)) (z : 𝔻) : + motive z := + mk z z.norm_lt_one + +@[simp] +theorem casesOn_mk {motive : 𝔻 β†’ Sort*} (mk' : βˆ€ z hz, motive (.mk z hz)) {z : β„‚} (hz : β€–zβ€– < 1) : + (mk z hz).casesOn mk' = mk' z hz := + rfl + @[simp] theorem coe_mk (z : β„‚) (hz : β€–zβ€– < 1) : (mk z hz : β„‚) = z := rfl @@ -104,39 +117,42 @@ theorem coe_eq_zero {z : 𝔻} : (z : β„‚) = 0 ↔ z = 0 := instance : Inhabited 𝔻 := ⟨0⟩ -instance circleAction : MulAction Circle 𝔻 := +instance instMulActionCircle : MulAction Circle 𝔻 := mulActionSphereBall -instance isScalarTower_circle_circle : IsScalarTower Circle Circle 𝔻 := +instance instIsScalarTower_circle_circle : IsScalarTower Circle Circle 𝔻 := isScalarTower_sphere_sphere_ball -instance isScalarTower_circle : IsScalarTower Circle 𝔻 𝔻 := +instance instIsScalarTower_circle : IsScalarTower Circle 𝔻 𝔻 := isScalarTower_sphere_ball_ball -instance instSMulCommClass_circle : SMulCommClass Circle 𝔻 𝔻 := +instance instSMulCommClass_circle_left : SMulCommClass Circle 𝔻 𝔻 := instSMulCommClass_sphere_ball_ball -instance instSMulCommClass_circle' : SMulCommClass 𝔻 Circle 𝔻 := +instance instSMulCommClass_circle_right : SMulCommClass 𝔻 Circle 𝔻 := SMulCommClass.symm _ _ _ @[simp, norm_cast] -theorem coe_smul_circle (z : Circle) (w : 𝔻) : ↑(z β€’ w) = (z * w : β„‚) := +theorem coe_circle_smul (z : Circle) (w : 𝔻) : ↑(z β€’ w) = (z * w : β„‚) := rfl -instance closedBallAction : MulAction (closedBall (0 : β„‚) 1) 𝔻 := +@[deprecated (since := "2025-04-21")] +alias Complex.UnitDisc.coe_smul_circle := coe_circle_smul + +instance instMulActionClosedBall : MulAction (closedBall (0 : β„‚) 1) 𝔻 := mulActionClosedBallBall -instance isScalarTower_closedBall_closedBall : +instance instIsScalarTower_closedBall_closedBall : IsScalarTower (closedBall (0 : β„‚) 1) (closedBall (0 : β„‚) 1) 𝔻 := isScalarTower_closedBall_closedBall_ball -instance isScalarTower_closedBall : IsScalarTower (closedBall (0 : β„‚) 1) 𝔻 𝔻 := +instance instIsScalarTower_closedBall : IsScalarTower (closedBall (0 : β„‚) 1) 𝔻 𝔻 := isScalarTower_closedBall_ball_ball -instance instSMulCommClass_closedBall : SMulCommClass (closedBall (0 : β„‚) 1) 𝔻 𝔻 := +instance instSMulCommClass_closedBall_left : SMulCommClass (closedBall (0 : β„‚) 1) 𝔻 𝔻 := ⟨fun _ _ _ => Subtype.ext <| mul_left_comm _ _ _⟩ -instance instSMulCommClass_closedBall' : SMulCommClass 𝔻 (closedBall (0 : β„‚) 1) 𝔻 := +instance instSMulCommClass_closedBall_right : SMulCommClass 𝔻 (closedBall (0 : β„‚) 1) 𝔻 := SMulCommClass.symm _ _ _ instance instSMulCommClass_circle_closedBall : SMulCommClass Circle (closedBall (0 : β„‚) 1) 𝔻 := @@ -146,9 +162,12 @@ instance instSMulCommClass_closedBall_circle : SMulCommClass (closedBall (0 : SMulCommClass.symm _ _ _ @[simp, norm_cast] -theorem coe_smul_closedBall (z : closedBall (0 : β„‚) 1) (w : 𝔻) : ↑(z β€’ w) = (z * w : β„‚) := +theorem coe_closedBall_smul (z : closedBall (0 : β„‚) 1) (w : 𝔻) : ↑(z β€’ w) = (z * w : β„‚) := rfl +@[deprecated (since := "2025-12-25")] +alias coe_smul_closedBall := coe_closedBall_smul + /-- Real part of a point of the unit disc. -/ def re (z : 𝔻) : ℝ := Complex.re z @@ -174,36 +193,50 @@ theorem im_neg (z : 𝔻) : (-z).im = -z.im := rfl /-- Conjugate point of the unit disc. -/ -def conj (z : 𝔻) : 𝔻 := - mk (conj' ↑z) <| (norm_conj z).symm β–Έ z.norm_lt_one +instance : Star 𝔻 where + star z := mk (conj z) <| (norm_conj z).symm β–Έ z.norm_lt_one -@[simp] -theorem coe_conj (z : 𝔻) : (z.conj : β„‚) = conj' ↑z := - rfl +@[deprecated star (since := "2025-12-28")] +protected def Β«conjΒ» (z : 𝔻) := star z -@[simp] -theorem conj_zero : conj 0 = 0 := - coe_injective (map_zero conj') +@[simp] theorem coe_star (z : 𝔻) : (↑(star z) : β„‚) = conj ↑z := rfl -@[simp] -theorem conj_conj (z : 𝔻) : conj (conj z) = z := - coe_injective <| Complex.conj_conj (z : β„‚) +@[deprecated (since := "2025-12-28")] +alias coe_conj := coe_star @[simp] -theorem conj_neg (z : 𝔻) : (-z).conj = -z.conj := - rfl +protected theorem star_eq_zero {z : 𝔻} : star z = 0 ↔ z = 0 := by + simp [← coe_eq_zero] @[simp] -theorem re_conj (z : 𝔻) : z.conj.re = z.re := - rfl +protected theorem star_zero : star (0 : 𝔻) = 0 := by simp -@[simp] -theorem im_conj (z : 𝔻) : z.conj.im = -z.im := - rfl +instance : InvolutiveStar 𝔻 where + star_involutive z := by ext; simp -@[simp] -theorem conj_mul (z w : 𝔻) : (z * w).conj = z.conj * w.conj := - Subtype.ext <| map_mul _ _ _ +@[deprecated star_star (since := "2025-12-28")] +theorem conj_conj (z : 𝔻) : star (star z) = z := star_star z + +@[simp] protected theorem star_neg (z : 𝔻) : star (-z) = -(star z) := rfl + +@[deprecated (since := "2025-12-28")] +alias conj_neg := UnitDisc.star_neg + +@[simp] protected theorem re_star (z : 𝔻) : (star z).re = z.re := rfl + +@[deprecated (since := "2025-12-28")] +alias re_conj := UnitDisc.re_star + +@[simp] protected theorem im_star (z : 𝔻) : (star z).im = -z.im := rfl + +@[deprecated (since := "2025-12-28")] alias im_conj := UnitDisc.im_star + +instance : StarMul 𝔻 where + star_mul z w := coe_injective <| by simp [mul_comm] + +@[deprecated star_mul' (since := "2025-12-28")] +theorem conj_mul (z w : 𝔻) : star (z * w) = star z * star w := + star_mul' z w end UnitDisc diff --git a/Mathlib/Analysis/Complex/UnitDisc/Shift.lean b/Mathlib/Analysis/Complex/UnitDisc/Shift.lean new file mode 100644 index 00000000000000..adabfdd0ed575c --- /dev/null +++ b/Mathlib/Analysis/Complex/UnitDisc/Shift.lean @@ -0,0 +1,172 @@ +/- +Copyright (c) 2025 Yury Kudryashov. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yury Kudryashov +-/ + +module +public import Mathlib.Analysis.Complex.UnitDisc.Basic + +/-! +# Shift on the unit disc + +In this file we define `Complex.UnitDisc.shift z` to be the automorphism of the unit disc +that sends `0` to `z` and preserves the diameter joining `0` to `z`. + +We also prove basic properties of this function. +-/ + +open Set Function Metric +open scoped ComplexConjugate + +noncomputable section + +namespace Complex.UnitDisc + +public section + +lemma shift_den_ne_zero (z w : 𝔻) : 1 + conj (z : β„‚) * w β‰  0 := + (star z * w).one_add_coe_ne_zero + +lemma shift_den_ne_zero' (z w : 𝔻) : 1 + z * conj (w : β„‚) β‰  0 := + (z * star w).one_add_coe_ne_zero + +end + +/-- Auxiliary definition for `shift` below. This function is not a part of the public API. -/ +def shiftFun (z w : 𝔻) : 𝔻 := + mk ((z + w : β„‚) / (1 + conj ↑z * w)) <| by + suffices β€–(z + w : β„‚)β€– < β€–1 + conj (z : β„‚) * wβ€– by + rwa [norm_div, div_lt_one] + exact (norm_nonneg _).trans_lt this + dsimp only [Complex.norm_def] + gcongr + Β· apply normSq_nonneg -- TODO: add a `positivity` extension + Β· rw [← sub_pos] + convert mul_pos (sub_pos.2 z.normSq_lt_one) (sub_pos.2 w.normSq_lt_one) using 1 + simp [normSq] + ring + +theorem coe_shiftFun (z w : 𝔻) : (shiftFun z w : β„‚) = (z + w) / (1 + conj ↑z * w) := rfl + +theorem shiftFun_eq_iff {z w u : 𝔻} : shiftFun z w = u ↔ (z + w : β„‚) = u + u * conj ↑z * w := by + rw [← coe_inj, coe_shiftFun, div_eq_iff (shift_den_ne_zero _ _)] + ring_nf + +theorem shiftFun_neg_apply_shiftFun (z w : 𝔻) : shiftFun (-z) (shiftFun z w) = w := by + rw [shiftFun_eq_iff, coe_shiftFun, add_div_eq_mul_add_div, ← mul_div_assoc, + add_div_eq_mul_add_div] + Β· simp; ring + all_goals exact shift_den_ne_zero z w + +public section + +/-- The automorphism of the unit disc that sends zero to `z`. -/ +def shift (z : 𝔻) : 𝔻 ≃ 𝔻 where + toFun := shiftFun z + invFun := shiftFun (-z) + left_inv := shiftFun_neg_apply_shiftFun _ + right_inv := by simpa using shiftFun_neg_apply_shiftFun (-z) + +/-- An explicit formula for `shift z w`. + +Note that the definition of `shift` is not exposed, so this is not a `dsimp` lemma. -/ +theorem coe_shift (z w : 𝔻) : (shift z w : β„‚) = (z + w) / (1 + conj ↑z * w) := by rfl + +theorem shift_eq_iff {z w u : 𝔻} : shift z w = u ↔ (z + w : β„‚) = u + u * conj ↑z * w := + shiftFun_eq_iff + +theorem symm_shift (z : 𝔻) : (shift z).symm = shift (-z) := by + ext1 + rfl + +@[simp] +theorem star_shift (z w : 𝔻) : star (shift z w) = shift (star z) (star w) := + coe_injective <| by simp [coe_shift] + +theorem norm_shift_swap (z w : 𝔻) : β€–(shift z w : β„‚)β€– = β€–(shift w z : β„‚)β€– := by + rw [coe_shift, norm_div, ← norm_conj (1 + _)] + simp [coe_shift, add_comm, mul_comm] + +theorem neg_shift (z w : 𝔻) : -shift z w = shift (-z) (-w) := by + ext1 + simp [coe_shift, ← neg_add_rev, add_comm, neg_div] + +@[simp] +theorem shift_zero : shift 0 = .refl 𝔻 := by + ext z + simp [coe_shift] + +@[simp] +theorem shift_apply_zero (z : 𝔻) : shift z 0 = z := by simp [shift_eq_iff] + +@[simp] +theorem shift_eq_zero_iff {z w : 𝔻} : shift z w = 0 ↔ w = -z := by + rw [← Equiv.eq_symm_apply, symm_shift, shift_apply_zero] + +@[simp] +theorem shift_apply_neg_self (z : 𝔻) : shift z (-z) = 0 := by simp + +@[simp] +theorem shift_neg_apply_self (z : 𝔻) : shift (-z) z = 0 := by simp + +@[simp] +theorem shift_neg_apply_shift (z w : 𝔻) : shift (-z) (shift z w) = w := by + rw [← symm_shift, Equiv.symm_apply_apply] + +@[simp] +theorem shift_apply_shift_neg (z w : 𝔻) : shift z (shift (-z) w) = w := by + simpa using shift_neg_apply_shift (-z) w + +/-- A shift by `0` is the identity map, and all other shifts have no fixed points. -/ +@[simp] +theorem shift_eq_self_iff {z w : 𝔻} : shift z w = w ↔ z = 0 := by + rcases eq_or_ne z 0 with rfl | hz + Β· simp + suffices (z : β„‚) β‰  w * conj ↑z * w by + simpa [shift_eq_iff, hz, add_comm (z : β„‚)] using this + refine ne_of_apply_ne norm (ne_of_gt ?_) + calc + _ = β€–(z : β„‚)β€– * β€–(w : β„‚)β€– ^ 2 := by simp; ring + _ < β€–(z : β„‚)β€– := mul_lt_of_lt_one_right (by simpa) <| by + rw [← Complex.normSq_eq_norm_sq]; exact w.normSq_lt_one + +lemma shift_apply_circle_smul (c : Circle) (z w : 𝔻) : + shift z (c β€’ w) = c β€’ shift (c⁻¹ β€’ z) w := by + ext1 + simp only [coe_shift, coe_circle_smul, ← mul_div_assoc, mul_add, + map_mul, Circle.coe_inv_eq_conj, Complex.conj_conj, ← mul_assoc] + rw [← Circle.coe_inv_eq_conj, ← Circle.coe_mul] + simp [mul_comm (c : β„‚)] + +/-- The composition of two shifts is a rotation by `shiftCompCoeff z w` composed with a shift. -/ +@[simps! coe] +def shiftCompCoeff (z w : 𝔻) : Circle := + .ofConjDivSelf (1 + conj ↑z * w) (shift_den_ne_zero _ _) + +theorem shift_apply_shift (z w u : 𝔻) : + shift z (shift w u) = shiftCompCoeff z w β€’ shift (shift w z) u := by + ext1 + have H₁ (z w u : 𝔻) : 1 + u * conj (w : β„‚) + (w + u) * conj (z : β„‚) β‰  0 := by + have := shift_den_ne_zero' (shift w u) z + rw [coe_shift, div_mul_eq_mul_divβ‚€, add_div_eq_mul_add_div, div_ne_zero_iff] at this + Β· simpa [mul_comm] using this.left + Β· apply shift_den_ne_zero + have Hβ‚‚ : 1 + w * conj (z : β„‚) + u * (conj ↑w + conj ↑z) β‰  0 := by + simpa [mul_comm] using H₁ (star u) (star w) (star z) + simp [coe_shift] + field_simp + (disch := first | apply shift_den_ne_zero | apply shift_den_ne_zero' | apply H₁ | exact Hβ‚‚) + ring + +theorem shift_trans_shift (z w : 𝔻) : + (shift z).trans (shift w) = + (shift (shift z w)).trans (MulAction.toPerm (shiftCompCoeff w z)) := by + ext1 u + simp [shift_apply_shift] + +end + +end UnitDisc + +end Complex From 24ce7fb6a9707322dfb7504024946a8ffbf17c4d Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Mon, 29 Dec 2025 01:33:45 -0600 Subject: [PATCH 2/6] Add an aux lemma --- Mathlib/Analysis/Complex/UnitDisc/Basic.lean | 8 +++-- Mathlib/Analysis/Complex/UnitDisc/Shift.lean | 34 ++++++++++++++------ 2 files changed, 30 insertions(+), 12 deletions(-) diff --git a/Mathlib/Analysis/Complex/UnitDisc/Basic.lean b/Mathlib/Analysis/Complex/UnitDisc/Basic.lean index 7eeeaa12d68fdd..cbcb5526fdfbc4 100644 --- a/Mathlib/Analysis/Complex/UnitDisc/Basic.lean +++ b/Mathlib/Analysis/Complex/UnitDisc/Basic.lean @@ -55,9 +55,13 @@ theorem norm_lt_one (z : 𝔻) : β€–(z : β„‚)β€– < 1 := theorem norm_ne_one (z : 𝔻) : β€–(z : β„‚)β€– β‰  1 := z.norm_lt_one.ne +theorem sq_norm_lt_one (z : 𝔻) : β€–(z : β„‚)β€– ^ 2 < 1 := by + rw [sq_lt_one_iff_abs_lt_one, abs_norm] + exact z.norm_lt_one + theorem normSq_lt_one (z : 𝔻) : normSq z < 1 := by - convert (Real.sqrt_lt' one_pos).1 z.norm_lt_one - exact (one_pow 2).symm + rw [← Complex.norm_mul_self_eq_normSq, ← sq] + exact z.sq_norm_lt_one theorem coe_ne_one (z : 𝔻) : (z : β„‚) β‰  1 := ne_of_apply_ne (β€–Β·β€–) <| by simp [z.norm_ne_one] diff --git a/Mathlib/Analysis/Complex/UnitDisc/Shift.lean b/Mathlib/Analysis/Complex/UnitDisc/Shift.lean index adabfdd0ed575c..556d6d521fa59e 100644 --- a/Mathlib/Analysis/Complex/UnitDisc/Shift.lean +++ b/Mathlib/Analysis/Complex/UnitDisc/Shift.lean @@ -33,19 +33,29 @@ lemma shift_den_ne_zero' (z w : 𝔻) : 1 + z * conj (w : β„‚) β‰  0 := end +theorem norm_shiftFun_le (z w : 𝔻) : + β€–(z + w : β„‚) / (1 + conj ↑z * w)β€– ≀ (β€–(z : β„‚)β€– + β€–(w : β„‚)β€–) / (1 + β€–(z : β„‚)β€– * β€–(w : β„‚)β€–) := by + have hz := z.sq_norm_lt_one + have hw := w.sq_norm_lt_one + have hzw : z.re * w.re + z.im * w.im ≀ β€–(z : β„‚)β€– * β€–(w : β„‚)β€– := by + rw [norm_def, norm_def, ← Real.sqrt_mul, normSq_apply, normSq_apply] + Β· apply Real.le_sqrt_of_sq_le + linear_combination (norm := {apply le_of_eq; simp; ring}) + sq_nonneg (z.re * w.im - z.im * w.re) + Β· apply normSq_nonneg + rw [norm_div, div_le_div_iffβ‚€, ← sq_le_sqβ‚€] + Β· rw [← sub_nonneg] at hzw + simp [mul_pow, RCLike.norm_sq_eq_def, add_sq] at hz hw ⊒ + linear_combination 2 * mul_nonneg hzw (mul_nonneg (sub_nonneg.2 hz.le) (sub_nonneg.2 hw.le)) + any_goals positivity + simpa using shift_den_ne_zero z w + /-- Auxiliary definition for `shift` below. This function is not a part of the public API. -/ def shiftFun (z w : 𝔻) : 𝔻 := mk ((z + w : β„‚) / (1 + conj ↑z * w)) <| by - suffices β€–(z + w : β„‚)β€– < β€–1 + conj (z : β„‚) * wβ€– by - rwa [norm_div, div_lt_one] - exact (norm_nonneg _).trans_lt this - dsimp only [Complex.norm_def] - gcongr - Β· apply normSq_nonneg -- TODO: add a `positivity` extension - Β· rw [← sub_pos] - convert mul_pos (sub_pos.2 z.normSq_lt_one) (sub_pos.2 w.normSq_lt_one) using 1 - simp [normSq] - ring + refine (norm_shiftFun_le _ _).trans_lt ?_ + rw [div_lt_one (by positivity)] + nlinarith only [z.norm_lt_one, w.norm_lt_one] theorem coe_shiftFun (z w : 𝔻) : (shiftFun z w : β„‚) = (z + w) / (1 + conj ↑z * w) := rfl @@ -118,6 +128,10 @@ theorem shift_neg_apply_shift (z w : 𝔻) : shift (-z) (shift z w) = w := by theorem shift_apply_shift_neg (z w : 𝔻) : shift z (shift (-z) w) = w := by simpa using shift_neg_apply_shift (-z) w +theorem norm_shift_le (z w : 𝔻) : + β€–(z.shift w : β„‚)β€– ≀ (β€–(z : β„‚)β€– + β€–(w : β„‚)β€–) / (1 + β€–(z : β„‚)β€– * β€–(w : β„‚)β€–) := + norm_shiftFun_le z w + /-- A shift by `0` is the identity map, and all other shifts have no fixed points. -/ @[simp] theorem shift_eq_self_iff {z w : 𝔻} : shift z w = w ↔ z = 0 := by From 213150118e037c3246dd09e202860f4ed3ebba91 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Mon, 29 Dec 2025 01:38:57 -0600 Subject: [PATCH 3/6] Run mk_all --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index ae3a5cc2936ad4..dcb5faef342a61 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1697,6 +1697,7 @@ public import Mathlib.Analysis.Complex.TaylorSeries public import Mathlib.Analysis.Complex.Tietze public import Mathlib.Analysis.Complex.Trigonometric public import Mathlib.Analysis.Complex.UnitDisc.Basic +public import Mathlib.Analysis.Complex.UnitDisc.Shift public import Mathlib.Analysis.Complex.UpperHalfPlane.Basic public import Mathlib.Analysis.Complex.UpperHalfPlane.Exp public import Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty From 1babb19cbe938926e11a2d14fd5b3ae4d449c638 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Mon, 29 Dec 2025 07:35:51 -0600 Subject: [PATCH 4/6] Add a missing docstring --- Mathlib/Analysis/Complex/UnitDisc/Basic.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/Analysis/Complex/UnitDisc/Basic.lean b/Mathlib/Analysis/Complex/UnitDisc/Basic.lean index cbcb5526fdfbc4..7f6414f5276b4b 100644 --- a/Mathlib/Analysis/Complex/UnitDisc/Basic.lean +++ b/Mathlib/Analysis/Complex/UnitDisc/Basic.lean @@ -200,6 +200,7 @@ theorem im_neg (z : 𝔻) : (-z).im = -z.im := instance : Star 𝔻 where star z := mk (conj z) <| (norm_conj z).symm β–Έ z.norm_lt_one +/-- Conjugate point of the unit disc. Deprecated, use `star` instead. -/ @[deprecated star (since := "2025-12-28")] protected def Β«conjΒ» (z : 𝔻) := star z From 5c66089c60cf15c78e2ac0df384a002007b2d4a4 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Tue, 30 Dec 2025 08:30:23 -0600 Subject: [PATCH 5/6] Update deprecated dates --- Mathlib/Analysis/Complex/UnitDisc/Basic.lean | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/Mathlib/Analysis/Complex/UnitDisc/Basic.lean b/Mathlib/Analysis/Complex/UnitDisc/Basic.lean index 7f6414f5276b4b..ac78621e52c6b7 100644 --- a/Mathlib/Analysis/Complex/UnitDisc/Basic.lean +++ b/Mathlib/Analysis/Complex/UnitDisc/Basic.lean @@ -140,7 +140,7 @@ instance instSMulCommClass_circle_right : SMulCommClass 𝔻 Circle 𝔻 := theorem coe_circle_smul (z : Circle) (w : 𝔻) : ↑(z β€’ w) = (z * w : β„‚) := rfl -@[deprecated (since := "2025-04-21")] +@[deprecated (since := "2025-12-30")] alias Complex.UnitDisc.coe_smul_circle := coe_circle_smul instance instMulActionClosedBall : MulAction (closedBall (0 : β„‚) 1) 𝔻 := @@ -169,7 +169,7 @@ instance instSMulCommClass_closedBall_circle : SMulCommClass (closedBall (0 : theorem coe_closedBall_smul (z : closedBall (0 : β„‚) 1) (w : 𝔻) : ↑(z β€’ w) = (z * w : β„‚) := rfl -@[deprecated (since := "2025-12-25")] +@[deprecated (since := "2025-12-30")] alias coe_smul_closedBall := coe_closedBall_smul /-- Real part of a point of the unit disc. -/ @@ -201,12 +201,12 @@ instance : Star 𝔻 where star z := mk (conj z) <| (norm_conj z).symm β–Έ z.norm_lt_one /-- Conjugate point of the unit disc. Deprecated, use `star` instead. -/ -@[deprecated star (since := "2025-12-28")] +@[deprecated star (since := "2025-12-30")] protected def Β«conjΒ» (z : 𝔻) := star z @[simp] theorem coe_star (z : 𝔻) : (↑(star z) : β„‚) = conj ↑z := rfl -@[deprecated (since := "2025-12-28")] +@[deprecated (since := "2025-12-30")] alias coe_conj := coe_star @[simp] @@ -219,27 +219,27 @@ protected theorem star_zero : star (0 : 𝔻) = 0 := by simp instance : InvolutiveStar 𝔻 where star_involutive z := by ext; simp -@[deprecated star_star (since := "2025-12-28")] +@[deprecated star_star (since := "2025-12-30")] theorem conj_conj (z : 𝔻) : star (star z) = z := star_star z @[simp] protected theorem star_neg (z : 𝔻) : star (-z) = -(star z) := rfl -@[deprecated (since := "2025-12-28")] +@[deprecated (since := "2025-12-30")] alias conj_neg := UnitDisc.star_neg @[simp] protected theorem re_star (z : 𝔻) : (star z).re = z.re := rfl -@[deprecated (since := "2025-12-28")] +@[deprecated (since := "2025-12-30")] alias re_conj := UnitDisc.re_star @[simp] protected theorem im_star (z : 𝔻) : (star z).im = -z.im := rfl -@[deprecated (since := "2025-12-28")] alias im_conj := UnitDisc.im_star +@[deprecated (since := "2025-12-30")] alias im_conj := UnitDisc.im_star instance : StarMul 𝔻 where star_mul z w := coe_injective <| by simp [mul_comm] -@[deprecated star_mul' (since := "2025-12-28")] +@[deprecated star_mul' (since := "2025-12-30")] theorem conj_mul (z w : 𝔻) : star (z * w) = star z * star w := star_mul' z w From aa86a45784a5e580f1a4d9a83fd9eb399e4663dd Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Tue, 30 Dec 2025 08:45:33 -0600 Subject: [PATCH 6/6] Show that `fun w => z.shift (-w)` is involutive --- Mathlib/Analysis/Complex/UnitDisc/Shift.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Mathlib/Analysis/Complex/UnitDisc/Shift.lean b/Mathlib/Analysis/Complex/UnitDisc/Shift.lean index 556d6d521fa59e..8d4fe0a6def7b7 100644 --- a/Mathlib/Analysis/Complex/UnitDisc/Shift.lean +++ b/Mathlib/Analysis/Complex/UnitDisc/Shift.lean @@ -128,6 +128,15 @@ theorem shift_neg_apply_shift (z w : 𝔻) : shift (-z) (shift z w) = w := by theorem shift_apply_shift_neg (z w : 𝔻) : shift z (shift (-z) w) = w := by simpa using shift_neg_apply_shift (-z) w +theorem neg_shift_neg (z w : 𝔻) : -z.shift (-w) = (-z).shift w := by + rw [eq_comm, shift_eq_iff, coe_neg, coe_neg, coe_shift] + field_simp (disch := apply shift_den_ne_zero') + simp; ring + +theorem involutive_shift_comp_neg (z : 𝔻) : (shift z <| -Β·).Involutive := by + intro x + simp [neg_shift_neg] + theorem norm_shift_le (z w : 𝔻) : β€–(z.shift w : β„‚)β€– ≀ (β€–(z : β„‚)β€– + β€–(w : β„‚)β€–) / (1 + β€–(z : β„‚)β€– * β€–(w : β„‚)β€–) := norm_shiftFun_le z w