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

Commit d1bd9c5

Browse files
YaelDilliesYaelDillies
committed
chore(*): Rename normed_group to normed_add_comm_group (#15619)
* `normed_group` → `normed_add_comm_group` * `semi_normed_group` → `seminormed_add_comm_group`. Elision of the underscore corresponds to `seminorm` (and to counterbalance the name being sensibly longer). * `normed_group_hom` → `normed_add_group_hom`
1 parent 989fe52 commit d1bd9c5

201 files changed

Lines changed: 1469 additions & 1406 deletions

File tree

Some content is hidden

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

‎counterexamples/phillips.lean‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -379,18 +379,18 @@ by applying the functional to the indicator functions. -/
379379
def _root_.continuous_linear_map.to_bounded_additive_measure
380380
[topological_space α] [discrete_topology α]
381381
(f : (α →ᵇ ℝ) →L[ℝ] ℝ) : bounded_additive_measure α :=
382-
{ to_fun := λ s, f (of_normed_group_discrete (indicator s 1) 1 (norm_indicator_le_one s)),
382+
{ to_fun := λ s, f (of_normed_add_comm_group_discrete (indicator s 1) 1 (norm_indicator_le_one s)),
383383
additive' := λ s t hst,
384384
begin
385-
have : of_normed_group_discrete (indicator (s ∪ t) 1) 1 (norm_indicator_le_one (s ∪ t))
386-
= of_normed_group_discrete (indicator s 1) 1 (norm_indicator_le_one s)
387-
+ of_normed_group_discrete (indicator t 1) 1 (norm_indicator_le_one t),
385+
have : of_normed_add_comm_group_discrete (indicator (s ∪ t) 1) 1 (norm_indicator_le_one _)
386+
= of_normed_add_comm_group_discrete (indicator s 1) 1 (norm_indicator_le_one s)
387+
+ of_normed_add_comm_group_discrete (indicator t 1) 1 (norm_indicator_le_one t),
388388
by { ext x, simp [indicator_union_of_disjoint hst], },
389389
rw [this, f.map_add],
390390
end,
391391
exists_bound := ⟨∥f∥, λ s, begin
392-
have I : ∥of_normed_group_discrete (indicator s 1) 1 (norm_indicator_le_one s)∥ ≤ 1,
393-
by apply norm_of_normed_group_le _ zero_le_one,
392+
have I : ∥of_normed_add_comm_group_discrete (indicator s 1) 1 (norm_indicator_le_one s)∥ ≤ 1,
393+
by apply norm_of_normed_add_comm_group_le _ zero_le_one,
394394
apply le_trans (f.le_op_norm _),
395395
simpa using mul_le_mul_of_nonneg_left I (norm_nonneg f),
396396
end⟩ }
@@ -410,7 +410,7 @@ lemma to_functions_to_measure [measurable_space α] (μ : measure α) [is_finite
410410
μ.extension_to_bounded_functions.to_bounded_additive_measure s = (μ s).to_real :=
411411
begin
412412
change μ.extension_to_bounded_functions
413-
(of_normed_group_discrete (indicator s (λ x, 1)) 1 (norm_indicator_le_one s)) = (μ s).to_real,
413+
(of_normed_add_comm_group_discrete (indicator s 1) 1 (norm_indicator_le_one s)) = (μ s).to_real,
414414
rw extension_to_bounded_functions_apply,
415415
{ change ∫ x, s.indicator (λ y, (1 : ℝ)) x ∂μ = _,
416416
simp [integral_indicator hs] },
@@ -500,7 +500,7 @@ which is large (it has countable complement), as in the Sierpinski pathological
500500
taking values in `{0, 1}`), indexed by a real parameter `x`, corresponding to the characteristic
501501
functions of the different fibers of the Sierpinski pathological family -/
502502
def f (Hcont : #ℝ = aleph 1) (x : ℝ) : (discrete_copy ℝ →ᵇ ℝ) :=
503-
of_normed_group_discrete (indicator (spf Hcont x) 1) 1 (norm_indicator_le_one _)
503+
of_normed_add_comm_group_discrete (indicator (spf Hcont x) 1) 1 (norm_indicator_le_one _)
504504

505505
lemma apply_f_eq_continuous_part (Hcont : #ℝ = aleph 1)
506506
(φ : (discrete_copy ℝ →ᵇ ℝ) →L[ℝ] ℝ) (x : ℝ)
@@ -579,7 +579,7 @@ end
579579

580580
/-- The function `f Hcont : ℝ → (discrete_copy ℝ →ᵇ ℝ)` is uniformly bounded by `1` in norm. -/
581581
lemma norm_bound (Hcont : #ℝ = aleph 1) (x : ℝ) : ∥f Hcont x∥ ≤ 1 :=
582-
norm_of_normed_group_le _ zero_le_one _
582+
norm_of_normed_add_comm_group_le _ zero_le_one _
583583

584584
/-- The function `f Hcont : ℝ → (discrete_copy ℝ →ᵇ ℝ)` has no Pettis integral. -/
585585
theorem no_pettis_integral (Hcont : #ℝ = aleph 1) :

‎src/algebra/module/pi.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,8 @@ instance module (α) {r : semiring α} {m : ∀ i, add_comm_monoid $ f i}
6363
/- Extra instance to short-circuit type class resolution.
6464
For unknown reasons, this is necessary for certain inference problems. E.g., for this to succeed:
6565
```lean
66-
example (β X : Type*) [normed_group β] [normed_space ℝ β] : module ℝ (X → β) := by apply_instance
66+
example (β X : Type*) [normed_add_comm_group β] [normed_space ℝ β] : module ℝ (X → β) :=
67+
infer_instance
6768
```
6869
See: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Typeclass.20resolution.20under.20binders/near/281296989
6970
-/

‎src/analysis/ODE/gronwall.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -27,8 +27,8 @@ Sec. 4.5][HubbardWest-ode], where `norm_le_gronwall_bound_of_norm_deriv_right_le
2727
of `K x` and `f x`.
2828
-/
2929

30-
variables {E : Type*} [normed_group E] [normed_space ℝ E]
31-
{F : Type*} [normed_group F] [normed_space ℝ F]
30+
variables {E : Type*} [normed_add_comm_group E] [normed_space ℝ E]
31+
{F : Type*} [normed_add_comm_group F] [normed_space ℝ F]
3232

3333
open metric set asymptotics filter real
3434
open_locale classical topological_space nnreal

‎src/analysis/ODE/picard_lindelof.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -33,12 +33,12 @@ open_locale filter topological_space nnreal ennreal nat interval
3333

3434
noncomputable theory
3535

36-
variables {E : Type*} [normed_group E] [normed_space ℝ E]
36+
variables {E : Type*} [normed_add_comm_group E] [normed_space ℝ E]
3737

3838
/-- This structure holds arguments of the Picard-Lipschitz (Cauchy-Lipschitz) theorem. Unless you
3939
want to use one of the auxiliary lemmas, use
4040
`exists_forall_deriv_within_Icc_eq_of_lipschitz_of_continuous` instead of using this structure. -/
41-
structure picard_lindelof (E : Type*) [normed_group E] [normed_space ℝ E] :=
41+
structure picard_lindelof (E : Type*) [normed_add_comm_group E] [normed_space ℝ E] :=
4242
(to_fun : ℝ → E → E)
4343
(t_min t_max : ℝ)
4444
(t₀ : Icc t_min t_max)

‎src/analysis/analytic/basic.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -101,9 +101,9 @@ end formal_multilinear_series
101101

102102

103103
variables [nontrivially_normed_field 𝕜]
104-
[normed_group E] [normed_space 𝕜 E]
105-
[normed_group F] [normed_space 𝕜 F]
106-
[normed_group G] [normed_space 𝕜 G]
104+
[normed_add_comm_group E] [normed_space 𝕜 E]
105+
[normed_add_comm_group F] [normed_space 𝕜 F]
106+
[normed_add_comm_group G] [normed_space 𝕜 G]
107107

108108
namespace formal_multilinear_series
109109

‎src/analysis/analytic/composition.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -289,10 +289,10 @@ end formal_multilinear_series
289289
end topological
290290

291291
variables [nontrivially_normed_field 𝕜]
292-
[normed_group E] [normed_space 𝕜 E]
293-
[normed_group F] [normed_space 𝕜 F]
294-
[normed_group G] [normed_space 𝕜 G]
295-
[normed_group H] [normed_space 𝕜 H]
292+
[normed_add_comm_group E] [normed_space 𝕜 E]
293+
[normed_add_comm_group F] [normed_space 𝕜 F]
294+
[normed_add_comm_group G] [normed_space 𝕜 G]
295+
[normed_add_comm_group H] [normed_space 𝕜 H]
296296

297297
namespace formal_multilinear_series
298298

‎src/analysis/analytic/inverse.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -32,8 +32,8 @@ open finset filter
3232
namespace formal_multilinear_series
3333

3434
variables {𝕜 : Type*} [nontrivially_normed_field 𝕜]
35-
{E : Type*} [normed_group E] [normed_space 𝕜 E]
36-
{F : Type*} [normed_group F] [normed_space 𝕜 F]
35+
{E : Type*} [normed_add_comm_group E] [normed_space 𝕜 E]
36+
{F : Type*} [normed_add_comm_group F] [normed_space 𝕜 F]
3737

3838
/-! ### The left inverse of a formal multilinear series -/
3939

‎src/analysis/analytic/linear.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,9 +13,9 @@ the formal power series `f x = f a + f (x - a)`.
1313
-/
1414

1515
variables {𝕜 : Type*} [nontrivially_normed_field 𝕜]
16-
{E : Type*} [normed_group E] [normed_space 𝕜 E]
17-
{F : Type*} [normed_group F] [normed_space 𝕜 F]
18-
{G : Type*} [normed_group G] [normed_space 𝕜 G]
16+
{E : Type*} [normed_add_comm_group E] [normed_space 𝕜 E]
17+
{F : Type*} [normed_add_comm_group F] [normed_space 𝕜 F]
18+
{G : Type*} [normed_add_comm_group G] [normed_space 𝕜 G]
1919

2020
open_locale topological_space classical big_operators nnreal ennreal
2121
open set filter asymptotics

‎src/analysis/analytic/radius_liminf.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,8 +14,8 @@ $\liminf_{n\to\infty} \frac{1}{\sqrt[n]{∥p n∥}}$. This lemma can't go to `ba
1414
would create a circular dependency once we redefine `exp` using `formal_multilinear_series`.
1515
-/
1616
variables {𝕜 : Type*} [nontrivially_normed_field 𝕜]
17-
{E : Type*} [normed_group E] [normed_space 𝕜 E]
18-
{F : Type*} [normed_group F] [normed_space 𝕜 F]
17+
{E : Type*} [normed_add_comm_group E] [normed_space 𝕜 E]
18+
{F : Type*} [normed_add_comm_group F] [normed_space 𝕜 F]
1919

2020
open_locale topological_space classical big_operators nnreal ennreal
2121
open filter asymptotics

‎src/analysis/asymptotics/asymptotic_equivalent.lean‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,8 @@ In this file, we define the relation `is_equivalent l u v`, which means that `u-
1313
`v` along the filter `l`.
1414
1515
Unlike `is_[oO]` relations, this one requires `u` and `v` to have the same codomain `β`. While the
16-
definition only requires `β` to be a `normed_group`, most interesting properties require it to be a
17-
`normed_field`.
16+
definition only requires `β` to be a `normed_add_comm_group`, most interesting properties require it
17+
to be a `normed_field`.
1818
1919
## Notations
2020
@@ -23,7 +23,7 @@ We introduce the notation `u ~[l] v := is_equivalent l u v`, which you can use b
2323
2424
## Main results
2525
26-
If `β` is a `normed_group` :
26+
If `β` is a `normed_add_comm_group` :
2727
2828
- `_ ~[l] _` is an equivalence relation
2929
- Equivalent statements for `u ~[l] const _ c` :
@@ -59,9 +59,9 @@ namespace asymptotics
5959
open filter function
6060
open_locale topological_space
6161

62-
section normed_group
62+
section normed_add_comm_group
6363

64-
variables {α β : Type*} [normed_group β]
64+
variables {α β : Type*} [normed_add_comm_group β]
6565

6666
/-- Two functions `u` and `v` are said to be asymptotically equivalent along a filter `l` when
6767
`u x - v x = o(v x)` as x converges along `l`. -/
@@ -162,7 +162,7 @@ begin
162162
simp,
163163
end
164164

165-
end normed_group
165+
end normed_add_comm_group
166166

167167
open_locale asymptotics
168168

@@ -217,7 +217,7 @@ end normed_field
217217

218218
section smul
219219

220-
lemma is_equivalent.smul {α E 𝕜 : Type*} [normed_field 𝕜] [normed_group E]
220+
lemma is_equivalent.smul {α E 𝕜 : Type*} [normed_field 𝕜] [normed_add_comm_group E]
221221
[normed_space 𝕜 E] {a b : α → 𝕜} {u v : α → E} {l : filter α} (hab : a ~[l] b) (huv : u ~[l] v) :
222222
(λ x, a x • u x) ~[l] (λ x, b x • v x) :=
223223
begin
@@ -310,7 +310,7 @@ end asymptotics
310310
open filter asymptotics
311311
open_locale asymptotics
312312

313-
variables {α β : Type*} [normed_group β]
313+
variables {α β : Type*} [normed_add_comm_group β]
314314

315315
lemma filter.eventually_eq.is_equivalent {u v : α → β} {l : filter α} (h : u =ᶠ[l] v) : u ~[l] v :=
316316
is_equivalent.congr_right (is_o_refl_left _ _) h

0 commit comments

Comments
 (0)