Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 468b141

Browse files
hrmacbethhrmacbeth
committed
refactor(analysis/complex/basic, data/complex/is_R_or_C): downgrade imports (#18217)
The files `data/complex/is_R_or_C` and `analysis/complex/basic` are imported widely across the analysis library: for example - `data/complex/is_R_or_C` into inner product spaces - `analysis/complex/basic` into the construction of `rpow` and thence into Lp spaces and the Bochner integral So it is useful (for the port and for compilation time) to make them as elementary as possible. Currently they both import `analysis/normed_space/operator_norm` and `analysis/normed_space/finite_dimension`, rather heavy imports, but use quite little from these files: they provide lemmas about the operator norms of `re`/`im`/`conj`/`of_real`, and get cheaply some facts about the topology of `ℂ`/`is_R_or_C` via real-finite-dimensionality. This PR splits both files. - `analysis/complex/basic` is split in place, with substantially downgraded imports, and with a few heavier lemmas moved to `analysis/complex/operator_norm`. (And a few lemmas moved earlier to `data/complex/module`.). I wrote direct proofs for the completeness and properness of `ℂ` so that these facts can remain available by importing this file, even though with heavier imports these facts can be deduced from the real-finite-dimensionality of `ℂ`. - `data/complex/is_R_or_C` is split into `data/is_R_or_C/basic` (lightweight file containing most of the former file) and `data/is_R_or_C/lemmas` (a few heavier lemmas). Also rename `equiv_real_prod_add_hom_lm` to `equiv_real_prod_lm` (an apparent typo), and `equiv_real_prodₗ` to `equiv_real_prod_clm` (also an apparent error since in our naming convention `ₗ` usually refers to linearity, not continuous-linearity).
1 parent 6862653 commit 468b141

29 files changed

Lines changed: 245 additions & 146 deletions

File tree

‎src/algebra/star/chsh.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Scott Morrison
55
-/
6-
import algebra.star.basic
7-
import data.complex.is_R_or_C
6+
import algebra.char_p.invertible
7+
import data.real.sqrt
88

99
/-!
1010
# The Clauser-Horne-Shimony-Holt inequality and Tsirelson's inequality.

‎src/analysis/calculus/cont_diff.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Sébastien Gouëzel
55
-/
66
import analysis.calculus.mean_value
7+
import analysis.normed_space.finite_dimension
78
import analysis.normed_space.multilinear
89
import analysis.calculus.formal_multilinear_series
910
import data.enat.basic

‎src/analysis/calculus/mean_value.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,8 @@ Authors: Sébastien Gouëzel, Yury Kudryashov
66
import analysis.calculus.local_extr
77
import analysis.convex.slope
88
import analysis.convex.normed
9-
import data.complex.is_R_or_C
9+
import data.is_R_or_C.basic
10+
import topology.instances.real_vector_space
1011

1112
/-!
1213
# The mean value inequality and equalities

‎src/analysis/complex/basic.lean‎

Lines changed: 38 additions & 56 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,10 @@ Copyright (c) Sébastien Gouëzel. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Sébastien Gouëzel
55
-/
6-
import data.complex.determinant
7-
import data.complex.is_R_or_C
6+
import data.complex.module
7+
import data.is_R_or_C.basic
8+
import topology.algebra.module.infinite_sum
9+
import topology.instances.real_vector_space
810

911
/-!
1012
# Normed space structure on `ℂ`.
@@ -28,6 +30,9 @@ isometries in `of_real_li` and `conj_lie`.
2830
2931
We also register the fact that `ℂ` is an `is_R_or_C` field.
3032
-/
33+
34+
assert_not_exists absorbs
35+
3136
noncomputable theory
3237

3338
namespace complex
@@ -151,6 +156,36 @@ lemma norm_eq_one_of_pow_eq_one {ζ : ℂ} {n : ℕ} (h : ζ ^ n = 1) (hn : n
151156
‖ζ‖ = 1 :=
152157
congr_arg coe (nnnorm_eq_one_of_pow_eq_one h hn)
153158

159+
lemma equiv_real_prod_apply_le (z : ℂ) : ‖equiv_real_prod z‖ ≤ abs z :=
160+
by simp [prod.norm_def, abs_re_le_abs, abs_im_le_abs]
161+
162+
lemma equiv_real_prod_apply_le' (z : ℂ) : ‖equiv_real_prod z‖ ≤ 1 * abs z :=
163+
by simpa using equiv_real_prod_apply_le z
164+
165+
lemma lipschitz_equiv_real_prod : lipschitz_with 1 equiv_real_prod :=
166+
by simpa using
167+
add_monoid_hom_class.lipschitz_of_bound equiv_real_prod_lm 1 equiv_real_prod_apply_le'
168+
169+
lemma antilipschitz_equiv_real_prod : antilipschitz_with (nnreal.sqrt 2) equiv_real_prod :=
170+
by simpa using
171+
add_monoid_hom_class.antilipschitz_of_bound equiv_real_prod_lm abs_le_sqrt_two_mul_max
172+
173+
lemma uniform_embedding_equiv_real_prod : uniform_embedding equiv_real_prod :=
174+
antilipschitz_equiv_real_prod.uniform_embedding lipschitz_equiv_real_prod.uniform_continuous
175+
176+
instance : complete_space ℂ :=
177+
(complete_space_congr uniform_embedding_equiv_real_prod).mpr infer_instance
178+
179+
/-- The natural `continuous_linear_equiv` from `ℂ` to `ℝ × ℝ`. -/
180+
@[simps apply symm_apply_re symm_apply_im { simp_rhs := tt }]
181+
def equiv_real_prod_clm : ℂ ≃L[ℝ] ℝ × ℝ :=
182+
equiv_real_prod_lm.to_continuous_linear_equiv_of_bounds 1 (real.sqrt 2)
183+
equiv_real_prod_apply_le'
184+
(λ p, abs_le_sqrt_two_mul_max (equiv_real_prod.symm p))
185+
186+
instance : proper_space ℂ :=
187+
(id lipschitz_equiv_real_prod : lipschitz_with 1 equiv_real_prod_clm.to_homeomorph).proper_space
188+
154189
/-- The `abs` function on `ℂ` is proper. -/
155190
lemma tendsto_abs_cocompact_at_top : filter.tendsto abs (filter.cocompact ℂ) filter.at_top :=
156191
tendsto_norm_cocompact_at_top
@@ -172,13 +207,6 @@ def re_clm : ℂ →L[ℝ] ℝ := re_lm.mk_continuous 1 (λ x, by simp [abs_re_l
172207

173208
@[simp] lemma re_clm_apply (z : ℂ) : (re_clm : ℂ → ℝ) z = z.re := rfl
174209

175-
@[simp] lemma re_clm_norm : ‖re_clm‖ = 1 :=
176-
le_antisymm (linear_map.mk_continuous_norm_le _ zero_le_one _) $
177-
calc 1 = ‖re_clm 1‖ : by simp
178-
... ≤ ‖re_clm‖ : unit_le_op_norm _ _ (by simp)
179-
180-
@[simp] lemma re_clm_nnnorm : ‖re_clm‖₊ = 1 := subtype.ext re_clm_norm
181-
182210
/-- Continuous linear map version of the real part function, from `ℂ` to `ℝ`. -/
183211
def im_clm : ℂ →L[ℝ] ℝ := im_lm.mk_continuous 1 (λ x, by simp [abs_im_le_abs])
184212

@@ -188,13 +216,6 @@ def im_clm : ℂ →L[ℝ] ℝ := im_lm.mk_continuous 1 (λ x, by simp [abs_im_l
188216

189217
@[simp] lemma im_clm_apply (z : ℂ) : (im_clm : ℂ → ℝ) z = z.im := rfl
190218

191-
@[simp] lemma im_clm_norm : ‖im_clm‖ = 1 :=
192-
le_antisymm (linear_map.mk_continuous_norm_le _ zero_le_one _) $
193-
calc 1 = ‖im_clm I‖ : by simp
194-
... ≤ ‖im_clm‖ : unit_le_op_norm _ _ (by simp)
195-
196-
@[simp] lemma im_clm_nnnorm : ‖im_clm‖₊ = 1 := subtype.ext im_clm_norm
197-
198219
lemma restrict_scalars_one_smul_right' (x : E) :
199220
continuous_linear_map.restrict_scalars ℝ ((1 : ℂ →L[ℂ] ℂ).smul_right x : ℂ →L[ℂ] E) =
200221
re_clm.smul_right x + I • im_clm.smul_right x :=
@@ -225,14 +246,6 @@ by rw [← dist_conj_conj, conj_conj]
225246
lemma nndist_conj_comm (z w : ℂ) : nndist (conj z) w = nndist z (conj w) :=
226247
subtype.ext $ dist_conj_comm _ _
227248

228-
/-- The determinant of `conj_lie`, as a linear map. -/
229-
@[simp] lemma det_conj_lie : (conj_lie.to_linear_equiv : ℂ →ₗ[ℝ] ℂ).det = -1 :=
230-
det_conj_ae
231-
232-
/-- The determinant of `conj_lie`, as a linear equiv. -/
233-
@[simp] lemma linear_equiv_det_conj_lie : conj_lie.to_linear_equiv.det = -1 :=
234-
linear_equiv_det_conj_ae
235-
236249
instance : has_continuous_star ℂ := ⟨conj_lie.continuous⟩
237250

238251
@[continuity] lemma continuous_conj : continuous (conj : ℂ → ℂ) := continuous_star
@@ -253,11 +266,6 @@ def conj_cle : ℂ ≃L[ℝ] ℂ := conj_lie
253266

254267
@[simp] lemma conj_cle_apply (z : ℂ) : conj_cle z = conj z := rfl
255268

256-
@[simp] lemma conj_cle_norm : ‖(conj_cle : ℂ →L[ℝ] ℂ)‖ = 1 :=
257-
conj_lie.to_linear_isometry.norm_to_continuous_linear_map
258-
259-
@[simp] lemma conj_cle_nnorm : ‖(conj_cle : ℂ →L[ℝ] ℂ)‖₊ = 1 := subtype.ext conj_cle_norm
260-
261269
/-- Linear isometry version of the canonical embedding of `ℝ` in `ℂ`. -/
262270
def of_real_li : ℝ →ₗᵢ[ℝ] ℂ := ⟨of_real_am.to_linear_map, norm_real⟩
263271

@@ -281,10 +289,6 @@ def of_real_clm : ℝ →L[ℝ] ℂ := of_real_li.to_continuous_linear_map
281289

282290
@[simp] lemma of_real_clm_apply (x : ℝ) : of_real_clm x = x := rfl
283291

284-
@[simp] lemma of_real_clm_norm : ‖of_real_clm‖ = 1 := of_real_li.norm_to_continuous_linear_map
285-
286-
@[simp] lemma of_real_clm_nnnorm : ‖of_real_clm‖₊ = 1 := subtype.ext $ of_real_clm_norm
287-
288292
noncomputable instance : is_R_or_C ℂ :=
289293
{ re := ⟨complex.re, complex.zero_re, complex.add_re⟩,
290294
im := ⟨complex.im, complex.zero_im, complex.add_im⟩,
@@ -320,36 +324,14 @@ by rw [eq_re_of_real_le hz, is_R_or_C.norm_of_real, real.norm_of_nonneg (complex
320324

321325
end complex_order
322326

323-
section
324-
325-
variables {α β γ : Type*}
326-
[add_comm_monoid α] [topological_space α] [add_comm_monoid γ] [topological_space γ]
327-
328-
/-- The natural `add_equiv` from `ℂ` to `ℝ × ℝ`. -/
329-
@[simps apply symm_apply_re symm_apply_im { simp_rhs := tt }]
330-
def equiv_real_prod_add_hom : ℂ ≃+ ℝ × ℝ :=
331-
{ map_add' := by simp, .. equiv_real_prod }
332-
333-
/-- The natural `linear_equiv` from `ℂ` to `ℝ × ℝ`. -/
334-
@[simps apply symm_apply_re symm_apply_im { simp_rhs := tt }]
335-
def equiv_real_prod_add_hom_lm : ℂ ≃ₗ[ℝ] ℝ × ℝ :=
336-
{ map_smul' := by simp [equiv_real_prod_add_hom], .. equiv_real_prod_add_hom }
337-
338-
/-- The natural `continuous_linear_equiv` from `ℂ` to `ℝ × ℝ`. -/
339-
@[simps apply symm_apply_re symm_apply_im { simp_rhs := tt }]
340-
def equiv_real_prodₗ : ℂ ≃L[ℝ] ℝ × ℝ :=
341-
equiv_real_prod_add_hom_lm.to_continuous_linear_equiv
342-
343-
end
344-
345327
lemma has_sum_iff {α} (f : α → ℂ) (c : ℂ) :
346328
has_sum f c ↔ has_sum (λ x, (f x).re) c.re ∧ has_sum (λ x, (f x).im) c.im :=
347329
begin
348330
-- For some reason, `continuous_linear_map.has_sum` is orders of magnitude faster than
349331
-- `has_sum.mapL` here:
350332
refine ⟨λ h, ⟨re_clm.has_sum h, im_clm.has_sum h⟩, _⟩,
351333
rintro ⟨h₁, h₂⟩,
352-
convert (h₁.prod_mk h₂).mapL equiv_real_prodₗ.symm.to_continuous_linear_map,
334+
convert (h₁.prod_mk h₂).mapL equiv_real_prod_clm.symm.to_continuous_linear_map,
353335
{ ext x; refl },
354336
{ cases c, refl }
355337
end

‎src/analysis/complex/cauchy_integral.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -169,7 +169,7 @@ lemma integral_boundary_rect_of_has_fderiv_at_real_off_countable (f : ℂ → E)
169169
(I • ∫ y : ℝ in z.im..w.im, f (re w + y * I)) - I • ∫ y : ℝ in z.im..w.im, f (re z + y * I) =
170170
∫ x : ℝ in z.re..w.re, ∫ y : ℝ in z.im..w.im, I • f' (x + y * I) 1 - f' (x + y * I) I :=
171171
begin
172-
set e : (ℝ × ℝ) ≃L[ℝ] ℂ := equiv_real_prodₗ.symm,
172+
set e : (ℝ × ℝ) ≃L[ℝ] ℂ := equiv_real_prod_clm.symm,
173173
have he : ∀ x y : ℝ, ↑x + ↑y * I = e (x, y), from λ x y, (mk_eq_add_mul_I x y).symm,
174174
have he₁ : e (1, 0) = 1 := rfl, have he₂ : e (0, 1) = I := rfl,
175175
simp only [he] at *,

‎src/analysis/complex/conformal.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ Authors: Yourong Zang
55
-/
66
import analysis.complex.isometry
77
import analysis.normed_space.conformal_linear_map
8+
import analysis.normed_space.finite_dimension
89

910
/-!
1011
# Conformal maps between complex vector spaces

‎src/analysis/complex/operator_norm.lean‎

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
/-
2+
Copyright (c) Sébastien Gouëzel. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Sébastien Gouëzel
5+
-/
6+
import analysis.complex.basic
7+
import analysis.normed_space.operator_norm
8+
import data.complex.determinant
9+
10+
/-! # The basic continuous linear maps associated to `ℂ`
11+
12+
The continuous linear maps `complex.re_clm` (real part), `complex.im_clm` (imaginary part),
13+
`complex.conj_cle` (conjugation), and `complex.of_real_clm` (inclusion of `ℝ`) were introduced in
14+
`analysis.complex.operator_norm`. This file contains a few calculations requiring more imports:
15+
the operator norm and (for `complex.conj_cle`) the determinant.
16+
-/
17+
18+
open continuous_linear_map
19+
20+
namespace complex
21+
22+
/-- The determinant of `conj_lie`, as a linear map. -/
23+
@[simp] lemma det_conj_lie : (conj_lie.to_linear_equiv : ℂ →ₗ[ℝ] ℂ).det = -1 :=
24+
det_conj_ae
25+
26+
/-- The determinant of `conj_lie`, as a linear equiv. -/
27+
@[simp] lemma linear_equiv_det_conj_lie : conj_lie.to_linear_equiv.det = -1 :=
28+
linear_equiv_det_conj_ae
29+
30+
@[simp] lemma re_clm_norm : ‖re_clm‖ = 1 :=
31+
le_antisymm (linear_map.mk_continuous_norm_le _ zero_le_one _) $
32+
calc 1 = ‖re_clm 1‖ : by simp
33+
... ≤ ‖re_clm‖ : unit_le_op_norm _ _ (by simp)
34+
35+
@[simp] lemma re_clm_nnnorm : ‖re_clm‖₊ = 1 := subtype.ext re_clm_norm
36+
37+
@[simp] lemma im_clm_norm : ‖im_clm‖ = 1 :=
38+
le_antisymm (linear_map.mk_continuous_norm_le _ zero_le_one _) $
39+
calc 1 = ‖im_clm I‖ : by simp
40+
... ≤ ‖im_clm‖ : unit_le_op_norm _ _ (by simp)
41+
42+
@[simp] lemma im_clm_nnnorm : ‖im_clm‖₊ = 1 := subtype.ext im_clm_norm
43+
44+
@[simp] lemma conj_cle_norm : ‖(conj_cle : ℂ →L[ℝ] ℂ)‖ = 1 :=
45+
conj_lie.to_linear_isometry.norm_to_continuous_linear_map
46+
47+
@[simp] lemma conj_cle_nnorm : ‖(conj_cle : ℂ →L[ℝ] ℂ)‖₊ = 1 := subtype.ext conj_cle_norm
48+
49+
@[simp] lemma of_real_clm_norm : ‖of_real_clm‖ = 1 := of_real_li.norm_to_continuous_linear_map
50+
51+
@[simp] lemma of_real_clm_nnnorm : ‖of_real_clm‖₊ = 1 := subtype.ext $ of_real_clm_norm
52+
53+
end complex

‎src/analysis/complex/re_im_topology.lean‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -38,11 +38,11 @@ namespace complex
3838

3939
/-- `complex.re` turns `ℂ` into a trivial topological fiber bundle over `ℝ`. -/
4040
lemma is_homeomorphic_trivial_fiber_bundle_re : is_homeomorphic_trivial_fiber_bundle ℝ re :=
41-
⟨equiv_real_prodₗ.to_homeomorph, λ z, rfl⟩
41+
⟨equiv_real_prod_clm.to_homeomorph, λ z, rfl⟩
4242

4343
/-- `complex.im` turns `ℂ` into a trivial topological fiber bundle over `ℝ`. -/
4444
lemma is_homeomorphic_trivial_fiber_bundle_im : is_homeomorphic_trivial_fiber_bundle ℝ im :=
45-
⟨equiv_real_prodₗ.to_homeomorph.trans (homeomorph.prod_comm ℝ ℝ), λ z, rfl⟩
45+
⟨equiv_real_prod_clm.to_homeomorph.trans (homeomorph.prod_comm ℝ ℝ), λ z, rfl⟩
4646

4747
lemma is_open_map_re : is_open_map re := is_homeomorphic_trivial_fiber_bundle_re.is_open_map_proj
4848
lemma is_open_map_im : is_open_map im := is_homeomorphic_trivial_fiber_bundle_im.is_open_map_proj
@@ -117,17 +117,17 @@ by simpa only [frontier_Ioi] using frontier_preimage_re (Ioi a)
117117
by simpa only [frontier_Ioi] using frontier_preimage_im (Ioi a)
118118

119119
lemma closure_re_prod_im (s t : set ℝ) : closure (s ×ℂ t) = closure s ×ℂ closure t :=
120-
by simpa only [← preimage_eq_preimage equiv_real_prodₗ.symm.to_homeomorph.surjective,
121-
equiv_real_prodₗ.symm.to_homeomorph.preimage_closure]
120+
by simpa only [← preimage_eq_preimage equiv_real_prod_clm.symm.to_homeomorph.surjective,
121+
equiv_real_prod_clm.symm.to_homeomorph.preimage_closure]
122122
using @closure_prod_eq _ _ _ _ s t
123123

124124
lemma interior_re_prod_im (s t : set ℝ) : interior (s ×ℂ t) = interior s ×ℂ interior t :=
125125
by rw [re_prod_im, re_prod_im, interior_inter, interior_preimage_re, interior_preimage_im]
126126

127127
lemma frontier_re_prod_im (s t : set ℝ) :
128128
frontier (s ×ℂ t) = (closure s ×ℂ frontier t) ∪ (frontier s ×ℂ closure t) :=
129-
by simpa only [← preimage_eq_preimage equiv_real_prodₗ.symm.to_homeomorph.surjective,
130-
equiv_real_prodₗ.symm.to_homeomorph.preimage_frontier]
129+
by simpa only [← preimage_eq_preimage equiv_real_prod_clm.symm.to_homeomorph.surjective,
130+
equiv_real_prod_clm.symm.to_homeomorph.preimage_frontier]
131131
using frontier_prod_eq s t
132132

133133
lemma frontier_set_of_le_re_and_le_im (a b : ℝ) :
@@ -152,4 +152,4 @@ lemma is_closed.re_prod_im (hs : is_closed s) (ht : is_closed t) : is_closed (s
152152
(hs.preimage continuous_re).inter (ht.preimage continuous_im)
153153

154154
lemma metric.bounded.re_prod_im (hs : bounded s) (ht : bounded t) : bounded (s ×ℂ t) :=
155-
equiv_real_prodₗ.antilipschitz.bounded_preimage (hs.prod ht)
155+
antilipschitz_equiv_real_prod.bounded_preimage (hs.prod ht)

‎src/analysis/convex/gauge.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ Authors: Yaël Dillies, Bhavik Mehta
66
import analysis.convex.basic
77
import analysis.normed_space.pointwise
88
import analysis.seminorm
9-
import data.complex.is_R_or_C
9+
import data.is_R_or_C.basic
1010
import tactic.congrm
1111

1212
/-!

‎src/analysis/inner_product_space/projection.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ Authors: Zhouhang Zhou, Frédéric Dupuis, Heather Macbeth
66
import analysis.convex.basic
77
import analysis.inner_product_space.symmetric
88
import analysis.normed_space.is_R_or_C
9+
import data.is_R_or_C.lemmas
910

1011
/-!
1112
# The orthogonal projection

0 commit comments

Comments
 (0)