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

Commit 46b633f

Browse files
eric-wiesereric-wieser
committed
refactor(analysis/inner_product_space/basic): do not extend normed_add_comm_group (#18583)
This replaces `[inner_product_space K V]` with `[normed_add_comm_group V] [inner_product_space K V]`. Before this PR, we had `inner_product_space K V extends normed_add_comm_group V`. At first glance this is a rather strange arrangement; we certainly don't have `module R V extends add_comm_group V`. The argument usually goes that `Derived A B extends Base B` is unsafe, because the `Derived.toBase` instance has no way of knowing which `A` to look for. For `inner_product_space K V` we argued that this problem doesn't apply, as `is_R_or_C K` means that in practice there are only two possible values of `K`. This is indeed enough to stop typeclass search grinding to a halt. The motivation for the old design is described by @dupuisf [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Dangerous.20instance.20vs.20elaboration.20problems/near/210594971): > However, when I do (the contents of this PR), I run into some very annoying elaboration issues where I have to constantly spoonfeed it `𝕜` and/or `α` in lemmas that rewrite norms in terms of inner products, even though the relevant instance is directly present in the context. While it may ease elaboration issues, there are a number of new problems that `inner_product_space K V extends normed_add_comm_group V` causes: 1. It is confusing when compared to all other typeclasses. After being told to write ```lean variables [add_comm_group U] [module R U] variables [normed_add_comm_group V] [normed_space R V] ``` it is natural to assume that the inner product space version would be ```lean variables [normed_add_comm_group W] [inner_product_space K W] ``` But writing this leads to `W` having two unrelated addition operations! 2. It doesn't allow a space `W` to be an inner product space over both R and C. For a (normed) module, you can write ```lean variables [add_comm_group U] [module R U] [module C U] variables [normed_add_comm_group V] [normed_space R V] [normed_space C V] ``` but writing `[inner_product_space R W] [inner_product_space C W]` again puts two unrelated `+` operators on `V` 3. It doesn't compose with other normed typeclasses. We can talk about a (normed) module with multiplication as ```lean variables [ring U] [module R U] variables [normed_ring V] [normed_space K V] ``` but once again, typing `[normed_ring W] [inner_product_space K W]` gives us two unrelated `+` operators. This prevents us generalizing over `real`, `complex`, and `quaternion`. We could work around this by defining variants of `inner_product_space` for `normed_ring A`, `normed_comm_ring A`, `normed_division_ring A`, `normed_field A`, but this doesn't scale well. If we do things "the module way" then we only need one new typeclass instead of four, ```lean class inner_product_algebra (K A) [is_R_or_C K] [normed_ring A] extends normed_algebra K A, inner_product_space K A ``` 5. The "`is_R_or_C` makes it OK" argument stops working if we generalize to [quaternionic inner product spaces](https://link.springer.com/chapter/10.1007/978-94-009-3713-0_13) The majority of this PR is adding `[normed_add_comm_group _]` to every `variables` line about `inner_product_space`. The rest is specifying the scalar manually where previously unification would find it for us. [This Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/inner_product_space.20and.20normed_algebra/near/341848831) has some initial discussion about this change.
1 parent d11893b commit 46b633f

57 files changed

Lines changed: 367 additions & 288 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎archive/100-theorems-list/57_herons_formula.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,8 +23,8 @@ open_locale real euclidean_geometry
2323

2424
local notation `√` := real.sqrt
2525

26-
variables {V : Type*} {P : Type*} [inner_product_space ℝ V] [metric_space P]
27-
[normed_add_torsor V P]
26+
variables {V : Type*} {P : Type*}
27+
[normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P]
2828

2929
include V
3030

‎archive/imo/imo2019_q2.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,8 @@ open_locale affine euclidean_geometry real
6363

6464
local attribute [instance] fact_finite_dimensional_of_finrank_eq_succ
6565

66-
variables (V : Type*) (Pt : Type*) [inner_product_space ℝ V] [metric_space Pt]
66+
variables (V : Type*) (Pt : Type*)
67+
variables [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space Pt]
6768
variables [normed_add_torsor V Pt] [hd2 : fact (finrank ℝ V = 2)]
6869
include hd2
6970

‎src/analysis/calculus/bump_function_inner.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -306,7 +306,7 @@ nonempty.some hb.out
306306

307307
/-- Any inner product space has smooth bump functions. -/
308308
@[priority 100] instance has_cont_diff_bump_of_inner_product_space
309-
(E : Type*) [inner_product_space ℝ E] : has_cont_diff_bump E :=
309+
(E : Type*) [normed_add_comm_group E] [inner_product_space ℝ E] : has_cont_diff_bump E :=
310310
let e : cont_diff_bump_base E :=
311311
{ to_fun := λ R x, real.smooth_transition ((R - ‖x‖) / (R - 1)),
312312
mem_Icc := λ R x, ⟨real.smooth_transition.nonneg _, real.smooth_transition.le_one _⟩,
@@ -331,7 +331,7 @@ let e : cont_diff_bump_base E :=
331331
exact cont_diff_at_const.congr_of_eventually_eq this },
332332
{ refine real.smooth_transition.cont_diff_at.comp _ _,
333333
refine cont_diff_at.div _ _ (sub_pos.2 hR).ne',
334-
{ exact cont_diff_at_fst.sub (cont_diff_at_snd.norm hx) },
334+
{ exact cont_diff_at_fst.sub (cont_diff_at_snd.norm ℝ hx) },
335335
{ exact cont_diff_at_fst.sub cont_diff_at_const } }
336336
end,
337337
eq_one := λ R hR x hx, real.smooth_transition.one_of_one_le $

‎src/analysis/calculus/conformal/inner_product.lean‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,9 @@ is conformal at `x` iff the derivative preserves inner products up to a scalar m
1515

1616
noncomputable theory
1717

18-
variables {E F : Type*} [inner_product_space ℝ E] [inner_product_space ℝ F]
18+
variables {E F : Type*}
19+
variables [normed_add_comm_group E] [normed_add_comm_group F]
20+
variables [inner_product_space ℝ E] [inner_product_space ℝ F]
1921

2022
open_locale real_inner_product_space
2123

‎src/analysis/convex/cone/basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -717,7 +717,7 @@ end
717717
/-! ### The dual cone -/
718718

719719
section dual
720-
variables {H : Type*} [inner_product_space ℝ H] (s t : set H)
720+
variables {H : Type*} [normed_add_comm_group H] [inner_product_space ℝ H] (s t : set H)
721721
open_locale real_inner_product_space
722722

723723
/-- The dual cone is the cone consisting of all points `y` such that for

‎src/analysis/fourier/add_circle.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -426,7 +426,7 @@ begin
426426
{ exact_mod_cast lp.norm_rpow_eq_tsum _ (fourier_basis.repr f),
427427
norm_num },
428428
have H₂ : ‖fourier_basis.repr f‖ ^ 2 = ‖f‖ ^ 2 := by simp,
429-
have H₃ := congr_arg is_R_or_C.re (@L2.inner_def (add_circle T) ℂ ℂ _ _ _ _ f f),
429+
have H₃ := congr_arg is_R_or_C.re (@L2.inner_def (add_circle T) ℂ ℂ _ _ _ _ _ f f),
430430
rw ← integral_re at H₃,
431431
{ simp only [← norm_sq_eq_inner] at H₃,
432432
rw [← H₁, H₂, H₃], },

‎src/analysis/inner_product_space/adjoint.lean‎

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,7 @@ open is_R_or_C
4444
open_locale complex_conjugate
4545

4646
variables {𝕜 E F G : Type*} [is_R_or_C 𝕜]
47+
variables [normed_add_comm_group E] [normed_add_comm_group F] [normed_add_comm_group G]
4748
variables [inner_product_space 𝕜 E] [inner_product_space 𝕜 F] [inner_product_space 𝕜 G]
4849
local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y
4950

@@ -206,7 +207,9 @@ end⟩
206207

207208
section real
208209

209-
variables {E' : Type*} {F' : Type*} [inner_product_space ℝ E'] [inner_product_space ℝ F']
210+
variables {E' : Type*} {F' : Type*}
211+
variables [normed_add_comm_group E'] [normed_add_comm_group F']
212+
variables [inner_product_space ℝ E'] [inner_product_space ℝ F']
210213
variables [complete_space E'] [complete_space F']
211214

212215
-- Todo: Generalize this to `is_R_or_C`.
@@ -402,7 +405,9 @@ by { rw [is_self_adjoint_iff', is_symmetric, ← linear_map.eq_adjoint_iff], exa
402405

403406
section real
404407

405-
variables {E' : Type*} {F' : Type*} [inner_product_space ℝ E'] [inner_product_space ℝ F']
408+
variables {E' : Type*} {F' : Type*}
409+
variables [normed_add_comm_group E'] [normed_add_comm_group F']
410+
variables [inner_product_space ℝ E'] [inner_product_space ℝ F']
406411
variables [finite_dimensional ℝ E'] [finite_dimensional ℝ F']
407412

408413
-- Todo: Generalize this to `is_R_or_C`.

0 commit comments

Comments
 (0)