[Merged by Bors] - feat(topology/{continuous_function/bounded, metric_space/algebra}): new mixin classes

docs/overview.yaml

@@ -237,7 +237,7 @@ Topology:
 Analysis:
   Normed vector spaces:
     normed vector space over a normed field: 'normed_space'
-    topology on a normed vector space: 'semi_normed_space.has_continuous_smul'
+    topology on a normed vector space: 'semi_normed_space.has_bounded_smul'
     equivalence of norms in finite dimension: 'linear_equiv.to_continuous_linear_equiv'
     finite dimensional normed spaces over complete normed fields are complete: 'submodule.complete_of_finite_dimensional'
     Heine-Borel theorem (finite dimensional normed spaces are proper): 'finite_dimensional.proper'

docs/undergrad.yaml

@@ -412,7 +412,7 @@ Topology:
     complete metric spaces: 'metric.complete_of_cauchy_seq_tendsto'
     contraction mapping theorem: 'contracting_with.exists_fixed_point'
   Normed vector spaces on $\R$ and $\C$:
-    topology on a normed vector space: 'semi_normed_space.has_continuous_smul'
+    topology on a normed vector space: 'semi_normed_space.has_bounded_smul'
     equivalent norms:
     Banach open mapping theorem: 'open_mapping'
     equivalence of norms in finite dimension: 'linear_equiv.to_continuous_linear_equiv'

src/analysis/normed_space/basic.lean

@@ -7,6 +7,7 @@ import algebra.algebra.subalgebra
 import order.liminf_limsup
 import topology.algebra.group_completion
 import topology.instances.ennreal
+import topology.metric_space.algebra
 import topology.metric_space.completion
 import topology.sequences
 import topology.locally_constant.algebra
@@ -800,15 +801,16 @@ begin
   exact not_le_of_lt zero_lt_one (add_le_iff_nonpos_left.1 hy)
 end
 
+@[priority 100] -- see Note [lower instance priority]
+instance semi_normed_group.has_lipschitz_add : has_lipschitz_add α :=
+{ lipschitz_add := ⟨2, lipschitz_with.prod_fst.add lipschitz_with.prod_snd⟩ }
+
 /-- A seminormed group is a uniform additive group, i.e., addition and subtraction are uniformly
 continuous. -/
 @[priority 100] -- see Note [lower instance priority]
 instance normed_uniform_group : uniform_add_group α :=
 ⟨(lipschitz_with.prod_fst.sub lipschitz_with.prod_snd).uniform_continuous⟩
 
-@[priority 100] -- see Note [lower instance priority]
-instance normed_top_monoid : has_continuous_add α :=
-by apply_instance -- short-circuit type class inference
 @[priority 100] -- see Note [lower instance priority]
 instance normed_top_group : topological_add_group α :=
 by apply_instance -- short-circuit type class inference
@@ -1485,6 +1487,13 @@ end prio
 
 variables [normed_field α] [semi_normed_group β]
 
+@[priority 100] -- see Note [lower instance priority]
+instance semi_normed_space.has_bounded_smul [semi_normed_space α β] : has_bounded_smul α β :=
+{ dist_smul_pair' := λ x y₁ y₂,
+    by simpa [dist_eq_norm, smul_sub] using semi_normed_space.norm_smul_le x (y₁ - y₂),
+  dist_pair_smul' := λ x₁ x₂ y,
+    by simpa [dist_eq_norm, sub_smul] using semi_normed_space.norm_smul_le (x₁ - x₂) y }
+
 instance normed_field.to_normed_space : normed_space α α :=
 { norm_smul_le := λ a b, le_of_eq (normed_field.norm_mul a b) }
 
@@ -1519,23 +1528,6 @@ lemma norm_smul_of_nonneg [semi_normed_space ℝ β] {t : ℝ} (ht : 0 ≤ t) (x
 variables {E : Type*} [semi_normed_group E] [semi_normed_space α E]
 variables {F : Type*} [semi_normed_group F] [semi_normed_space α F]
 
-@[priority 100] -- see Note [lower instance priority]
-instance semi_normed_space.has_continuous_smul : has_continuous_smul α E :=
-begin
-  refine { continuous_smul := continuous_iff_continuous_at.2 $
-    λ p, tendsto_iff_norm_tendsto_zero.2 _ },
-  refine squeeze_zero (λ _, norm_nonneg _) _ _,
-  { exact λ q, ∥q.1 - p.1∥ * ∥q.2∥ + ∥p.1∥ * ∥q.2 - p.2∥ },
-  { intro q,
-    rw [← sub_add_sub_cancel, ← norm_smul, ← norm_smul, smul_sub, sub_smul],
-    exact norm_add_le _ _ },
-  { conv { congr, skip, skip, congr, rw [← zero_add (0:ℝ)], congr,
-      rw [← zero_mul ∥p.2∥], skip, rw [← mul_zero ∥p.1∥] },
-    exact ((tendsto_iff_norm_tendsto_zero.1 (continuous_fst.tendsto p)).mul
-      (continuous_snd.tendsto p).norm).add
-        (tendsto_const_nhds.mul (tendsto_iff_norm_tendsto_zero.1 (continuous_snd.tendsto p))) }
-end
-
 theorem eventually_nhds_norm_smul_sub_lt (c : α) (x : E) {ε : ℝ} (h : 0 < ε) :
   ∀ᶠ y in 𝓝 x, ∥c • (y - x)∥ < ε :=
 have tendsto (λ y, ∥c • (y - x)∥) (𝓝 x) (𝓝 0),

src/topology/continuous_function/bounded.lean

@@ -421,6 +421,101 @@ end
 
 end arzela_ascoli
 
+section has_lipschitz_add
+/- In this section, if `β` is an `add_monoid` whose addition operation is Lipschitz, then we show
+that the space of bounded continuous functions from `α` to `β` inherits a topological `add_monoid`
+structure, by using pointwise operations and checking that they are compatible with the uniform
+distance.
+
+Implementation note: The material in this section could have been written for `has_lipschitz_mul`
+and transported by `@[to_additive]`.  We choose not to do this because this causes a few lemma
+names (for example, `coe_mul`) to conflict with later lemma names for normed rings; this is only a
+trivial inconvenience, but in any case there are no obvious applications of the multiplicative
+version. -/
+
+variables [topological_space α] [metric_space β] [add_monoid β]
+
+instance : has_zero (α →ᵇ β) := ⟨const α 0⟩
+
+@[simp] lemma coe_zero : ((0 : α →ᵇ β) : α → β) = 0 := rfl
+
+lemma forall_coe_zero_iff_zero (f : α →ᵇ β) : (∀x, f x = 0) ↔ f = 0 := (@ext_iff _ _ _ _ f 0).symm
+
+variables [has_lipschitz_add β]
+variables (f g : α →ᵇ β) {x : α} {C : ℝ}
+
+/-- The pointwise sum of two bounded continuous functions is again bounded continuous. -/
+instance : has_add (α →ᵇ β) :=
+{ add := λ f g,
+    bounded_continuous_function.mk_of_bound (f.to_continuous_map + g.to_continuous_map)
+    (↑(has_lipschitz_add.C β) * max (classical.some f.bounded) (classical.some g.bounded))
+    begin
+      intros x y,
+      refine le_trans (lipschitz_with_lipschitz_const_add ⟨f x, g x⟩ ⟨f y, g y⟩) _,
+      rw prod.dist_eq,
+      refine mul_le_mul_of_nonneg_left _ (has_lipschitz_add.C β).coe_nonneg,
+      apply max_le_max,
+      exact classical.some_spec f.bounded x y,
+      exact classical.some_spec g.bounded x y,
+    end }
+
+@[simp] lemma coe_add : ⇑(f + g) = f + g := rfl
+lemma add_apply : (f + g) x = f x + g x := rfl
+
+instance : add_monoid (α →ᵇ β) :=
+{ add_assoc      := assume f g h, by ext; simp [add_assoc],
+  zero_add       := assume f, by ext; simp,
+  add_zero       := assume f, by ext; simp,
+  .. bounded_continuous_function.has_add,
+  .. bounded_continuous_function.has_zero }
+
+instance : has_lipschitz_add (α →ᵇ β) :=
+{ lipschitz_add := ⟨has_lipschitz_add.C β, begin
+    have C_nonneg := (has_lipschitz_add.C β).coe_nonneg,
+    rw lipschitz_with_iff_dist_le_mul,
+    rintros ⟨f₁, g₁⟩ ⟨f₂, g₂⟩,
+    rw dist_le (mul_nonneg C_nonneg dist_nonneg),
+    intros x,
+    refine le_trans (lipschitz_with_lipschitz_const_add ⟨f₁ x, g₁ x⟩ ⟨f₂ x, g₂ x⟩) _,
+    refine mul_le_mul_of_nonneg_left _ C_nonneg,
+    apply max_le_max; exact dist_coe_le_dist x,
+  end⟩ }
+
+/-- Coercion of a `normed_group_hom` is an `add_monoid_hom`. Similar to `add_monoid_hom.coe_fn` -/
+@[simps] def coe_fn_add_hom : (α →ᵇ β) →+ (α → β) :=
+{ to_fun := coe_fn, map_zero' := coe_zero, map_add' := coe_add }
+
+variables (α β)
+
+/-- The additive map forgetting that a bounded continuous function is bounded.
+-/
+@[simps] def forget_boundedness_add_hom : (α →ᵇ β) →+ C(α, β) :=
+{ to_fun := forget_boundedness α β,
+  map_zero' := by { ext, simp, },
+  map_add' := by { intros, ext, simp, }, }
+
+end has_lipschitz_add
+
+section comm_has_lipschitz_add
+
+variables [topological_space α] [metric_space β] [add_comm_monoid β] [has_lipschitz_add β]
+
+@[to_additive] instance : add_comm_monoid (α →ᵇ β) :=
+{ add_comm      := assume f g, by ext; simp [add_comm],
+  .. bounded_continuous_function.add_monoid }
+
+open_locale big_operators
+
+@[simp] lemma coe_sum {ι : Type*} (s : finset ι) (f : ι → (α →ᵇ β)) :
+  ⇑(∑ i in s, f i) = (∑ i in s, (f i : α → β)) :=
+(@coe_fn_add_hom α β _ _ _ _).map_sum f s
+
+lemma sum_apply {ι : Type*} (s : finset ι) (f : ι → (α →ᵇ β)) (a : α) :
+  (∑ i in s, f i) a = (∑ i in s, f i a) :=
+by simp
+
+end comm_has_lipschitz_add
+
 section normed_group
 /- In this section, if β is a normed group, then we show that the space of bounded
 continuous functions from α to β inherits a normed group structure, by using
@@ -429,10 +524,6 @@ pointwise operations and checking that they are compatible with the uniform dist
 variables [topological_space α] [normed_group β]
 variables (f g : α →ᵇ β) {x : α} {C : ℝ}
 
-instance : has_zero (α →ᵇ β) := ⟨const α 0⟩
-
-@[simp] lemma coe_zero : ((0 : α →ᵇ β) : α → β) = 0 := rfl
-
 instance : has_norm (α →ᵇ β) := ⟨λu, dist u 0⟩
 
 lemma norm_def : ∥f∥ = dist f 0 := rfl
@@ -565,11 +656,6 @@ begin
     simp only [forall_apply_eq_imp_iff', mem_range, exists_imp_distrib], },
 end
 
-/-- The pointwise sum of two bounded continuous functions is again bounded continuous. -/
-instance : has_add (α →ᵇ β) :=
-⟨λf g, of_normed_group (f + g) (f.continuous.add g.continuous) (∥f∥ + ∥g∥) $ λ x,
-  le_trans (norm_add_le _ _) (add_le_add (f.norm_coe_le_norm x) (g.norm_coe_le_norm x))⟩
-
 /-- The pointwise opposite of a bounded continuous function is again bounded continuous. -/
 instance : has_neg (α →ᵇ β) :=
 ⟨λf, of_normed_group (-f) f.continuous.neg ∥f∥ $ λ x,
@@ -582,43 +668,20 @@ instance : has_sub (α →ᵇ β) :=
        exact le_trans (norm_add_le _ _) (add_le_add (f.norm_coe_le_norm x) $
          trans_rel_right _ (norm_neg _) (g.norm_coe_le_norm x)) }⟩
 
-@[simp] lemma coe_add : ⇑(f + g) = f + g := rfl
-lemma add_apply : (f + g) x = f x + g x := rfl
 @[simp] lemma coe_neg : ⇑(-f) = -f := rfl
 lemma neg_apply : (-f) x = -f x := rfl
 
-lemma forall_coe_zero_iff_zero : (∀x, f x = 0) ↔ f = 0 :=
-(@ext_iff _ _ _ _ f 0).symm
-
 instance : add_comm_group (α →ᵇ β) :=
-{ add_assoc      := assume f g h, by ext; simp [add_assoc],
-  zero_add       := assume f, by ext; simp,
-  add_zero       := assume f, by ext; simp,
-  add_left_neg   := assume f, by ext; simp,
+{ add_left_neg   := assume f, by ext; simp,
   add_comm       := assume f g, by ext; simp [add_comm],
   sub_eq_add_neg := assume f g, by { ext, apply sub_eq_add_neg },
-  ..bounded_continuous_function.has_add,
+  ..bounded_continuous_function.add_monoid,
   ..bounded_continuous_function.has_neg,
-  ..bounded_continuous_function.has_sub,
-  ..bounded_continuous_function.has_zero }
+  ..bounded_continuous_function.has_sub }
 
 @[simp] lemma coe_sub : ⇑(f - g) = f - g := rfl
 lemma sub_apply : (f - g) x = f x - g x := rfl
 
-/-- Coercion of a `normed_group_hom` is an `add_monoid_hom`. Similar to `add_monoid_hom.coe_fn` -/
-@[simps]
-def coe_fn_add_hom : (α →ᵇ β) →+ (α → β) :=
-{ to_fun := coe_fn, map_zero' := coe_zero, map_add' := coe_add}
-
-open_locale big_operators
-@[simp] lemma coe_sum {ι : Type*} (s : finset ι) (f : ι → (α →ᵇ β)) :
-  ⇑(∑ i in s, f i) = (∑ i in s, (f i : α → β)) :=
-(@coe_fn_add_hom α β _ _).map_sum f s
-
-lemma sum_apply {ι : Type*} (s : finset ι) (f : ι → (α →ᵇ β)) (a : α) :
-  (∑ i in s, f i) a = (∑ i in s, f i a) :=
-by simp
-
 instance : normed_group (α →ᵇ β) :=
 { dist_eq := λ f g, by simp only [norm_eq, dist_eq, dist_eq_norm, sub_apply] }
 
@@ -628,52 +691,64 @@ by { rw dist_eq_norm, exact (f - g).norm_coe_le_norm x }
 lemma coe_le_coe_add_dist {f g : α →ᵇ ℝ} : f x ≤ g x + dist f g :=
 sub_le_iff_le_add'.1 $ (abs_le.1 $ @dist_coe_le_dist _ _ _ _ f g x).2
 
-variables (α β)
-
-/--
-The additive map forgetting that a bounded continuous function is bounded.
--/
-@[simps]
-def forget_boundedness_add_hom : (α →ᵇ β) →+ C(α, β) :=
-{ to_fun := forget_boundedness α β,
-  map_zero' := by { ext, simp, },
-  map_add' := by { intros, ext, simp, }, }
-
 end normed_group
 
-section normed_space
+section has_bounded_smul
 /-!
-### Normed space structure
+### `has_bounded_smul` (in particular, topological module) structure
 
-In this section, if `β` is a normed space, then we show that the space of bounded
-continuous functions from `α` to `β` inherits a normed space structure, by using
-pointwise operations and checking that they are compatible with the uniform distance. -/
+In this section, if `β` is a metric space and a `𝕜`-module whose addition and scalar multiplication
+are compatible with the metric structure, then we show that the space of bounded continuous
+functions from `α` to `β` inherits a so-called `has_bounded_smul` structure (in particular, a
+`has_continuous_mul` structure, which is the mathlib formulation of being a topological module), by
+using pointwise operations and checking that they are compatible with the uniform distance. -/
 
-variables {𝕜 : Type*}
-variables [topological_space α] [normed_group β]
+variables {𝕜 : Type*} [metric_space 𝕜] [semiring 𝕜]
+variables [topological_space α] [metric_space β] [add_comm_monoid β]
+  [module 𝕜 β] [has_bounded_smul 𝕜 β]
 variables {f g : α →ᵇ β} {x : α} {C : ℝ}
 
-section normed_field
-variables [normed_field 𝕜] [normed_space 𝕜 β]
-
 instance : has_scalar 𝕜 (α →ᵇ β) :=
-⟨λ c f, of_normed_group (c • f) (f.continuous.const_smul c) (∥c∥ * ∥f∥) $ λ x,
-  trans_rel_right _ (norm_smul _ _)
-    (mul_le_mul_of_nonneg_left (f.norm_coe_le_norm _) (norm_nonneg _))⟩
+⟨λ c f,
+  bounded_continuous_function.mk_of_bound
+    (c • f.to_continuous_map)
+    (dist c 0 * (classical.some f.bounded))
+    begin
+      intros x y,
+      refine (dist_smul_pair c (f x) (f y)).trans _,
+      refine mul_le_mul_of_nonneg_left _ dist_nonneg,
+      exact classical.some_spec f.bounded x y
+    end ⟩
 
 @[simp] lemma coe_smul (c : 𝕜) (f : α →ᵇ β) : ⇑(c • f) = λ x, c • (f x) := rfl
 lemma smul_apply (c : 𝕜) (f : α →ᵇ β) (x : α) : (c • f) x = c • f x := rfl
 
+instance : has_bounded_smul 𝕜 (α →ᵇ β) :=
+{ dist_smul_pair' := λ c f₁ f₂, begin
+    rw dist_le (mul_nonneg dist_nonneg dist_nonneg),
+    intros x,
+    refine (dist_smul_pair c (f₁ x) (f₂ x)).trans _,
+    exact mul_le_mul_of_nonneg_left (dist_coe_le_dist x) dist_nonneg
+  end,
+  dist_pair_smul' := λ c₁ c₂ f, begin
+    rw dist_le (mul_nonneg dist_nonneg dist_nonneg),
+    intros x,
+    refine (dist_pair_smul c₁ c₂ (f x)).trans _,
+    convert mul_le_mul_of_nonneg_left (dist_coe_le_dist x) dist_nonneg,
+    simp
+  end }
+
+variables [has_lipschitz_add β]
+
 instance : module 𝕜 (α →ᵇ β) :=
-module.of_core $
 { smul     := (•),
   smul_add := λ c f g, ext $ λ x, smul_add c (f x) (g x),
   add_smul := λ c₁ c₂ f, ext $ λ x, add_smul c₁ c₂ (f x),
   mul_smul := λ c₁ c₂ f, ext $ λ x, mul_smul c₁ c₂ (f x),
-  one_smul := λ f, ext $ λ x, one_smul 𝕜 (f x) }
-
-instance : normed_space 𝕜 (α →ᵇ β) := ⟨λ c f, norm_of_normed_group_le _
-  (mul_nonneg (norm_nonneg _) (norm_nonneg _)) _⟩
+  one_smul := λ f, ext $ λ x, one_smul 𝕜 (f x),
+  smul_zero := λ c, ext $ λ x, smul_zero c,
+  zero_smul := λ f, ext $ λ x, zero_smul 𝕜 (f x),
+  .. bounded_continuous_function.add_comm_monoid }
 
 variables (𝕜)
 /-- The evaluation at a point, as a continuous linear map from `α →ᵇ β` to `β`. -/
@@ -694,12 +769,30 @@ def forget_boundedness_linear_map : (α →ᵇ β) →ₗ[𝕜] C(α, β) :=
   map_smul' := by { intros, ext, simp, },
   map_add' := by { intros, ext, simp, }, }
 
-end normed_field
+end has_bounded_smul
+
+section normed_space
+/-!
+### Normed space structure
+
+In this section, if `β` is a normed space, then we show that the space of bounded
+continuous functions from `α` to `β` inherits a normed space structure, by using
+pointwise operations and checking that they are compatible with the uniform distance. -/
+
+variables {𝕜 : Type*}
+variables [topological_space α] [normed_group β]
+variables {f g : α →ᵇ β} {x : α} {C : ℝ}
+
+instance [normed_field 𝕜] [normed_space 𝕜 β] : normed_space 𝕜 (α →ᵇ β) := ⟨λ c f, begin
+  refine norm_of_normed_group_le _ (mul_nonneg (norm_nonneg _) (norm_nonneg _)) _,
+  exact (λ x, trans_rel_right _ (norm_smul _ _)
+    (mul_le_mul_of_nonneg_left (f.norm_coe_le_norm _) (norm_nonneg _))) end⟩
 
 variables [nondiscrete_normed_field 𝕜] [normed_space 𝕜 β]
 variables [normed_group γ] [normed_space 𝕜 γ]
 
 variables (α)
+-- TODO does this work in the `has_bounded_smul` setting, too?
 /--
 Postcomposition of bounded continuous functions into a normed module by a continuous linear map is
 a continuous linear map.