mathlib3 documentation

analysis.normed.mul_action

Lemmas for has_bounded_smul over normed additive groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Lemmas which hold only in normed_space α β are provided in another file.

Notably we prove that non_unital_semi_normed_rings have bounded actions by left- and right- multiplication. This allows downstream files to write general results about bounded_smul, and then deduce const_mul and mul_const results as an immediate corollary.

theorem norm_smul_le {α : Type u_1} {β : Type u_2} [seminormed_add_group α] [seminormed_add_group β] [smul_zero_class α β] [has_bounded_smul α β] (r : α) (x : β) :
theorem nnnorm_smul_le {α : Type u_1} {β : Type u_2} [seminormed_add_group α] [seminormed_add_group β] [smul_zero_class α β] [has_bounded_smul α β] (r : α) (x : β) :
theorem dist_smul_le {α : Type u_1} {β : Type u_2} [seminormed_add_group α] [seminormed_add_group β] [smul_zero_class α β] [has_bounded_smul α β] (s : α) (x y : β) :
theorem nndist_smul_le {α : Type u_1} {β : Type u_2} [seminormed_add_group α] [seminormed_add_group β] [smul_zero_class α β] [has_bounded_smul α β] (s : α) (x y : β) :
theorem edist_smul_le {α : Type u_1} {β : Type u_2} [seminormed_add_group α] [seminormed_add_group β] [smul_zero_class α β] [has_bounded_smul α β] (s : α) (x y : β) :
@[protected, instance]

Left multiplication is bounded.

@[protected, instance]

Right multiplication is bounded.

theorem has_bounded_smul.of_norm_smul_le {α : Type u_1} {β : Type u_2} [semi_normed_ring α] [seminormed_add_comm_group β] [module α β] (h : (r : α) (x : β), r x r * x) :
theorem norm_smul {α : Type u_1} {β : Type u_2} [normed_division_ring α] [seminormed_add_group β] [mul_action_with_zero α β] [has_bounded_smul α β] (r : α) (x : β) :
theorem nnnorm_smul {α : Type u_1} {β : Type u_2} [normed_division_ring α] [seminormed_add_group β] [mul_action_with_zero α β] [has_bounded_smul α β] (r : α) (x : β) :
theorem dist_smul₀ {α : Type u_1} {β : Type u_2} [normed_division_ring α] [seminormed_add_comm_group β] [module α β] [has_bounded_smul α β] (s : α) (x y : β) :
theorem nndist_smul₀ {α : Type u_1} {β : Type u_2} [normed_division_ring α] [seminormed_add_comm_group β] [module α β] [has_bounded_smul α β] (s : α) (x y : β) :
theorem edist_smul₀ {α : Type u_1} {β : Type u_2} [normed_division_ring α] [seminormed_add_comm_group β] [module α β] [has_bounded_smul α β] (s : α) (x y : β) :