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 : β) :
has_dist.dist (s • x) (s • y) ≤ ‖s‖ * has_dist.dist 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 : β) :
has_nndist.nndist (s • x) (s • y) ≤ ‖s‖₊ * has_nndist.nndist 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 : β) :
has_edist.edist (s • x) (s • y) ≤ ‖s‖₊ • has_edist.edist x y
theorem
lipschitz_with_smul
{α : Type u_1}
{β : Type u_2}
[seminormed_add_group α]
[seminormed_add_group β]
[smul_zero_class α β]
[has_bounded_smul α β]
(s : α) :
@[protected, instance]
def
non_unital_semi_normed_ring.to_has_bounded_smul
{α : Type u_1}
[non_unital_semi_normed_ring α] :
has_bounded_smul α α
Left multiplication is bounded.
@[protected, instance]
def
non_unital_semi_normed_ring.to_has_bounded_op_smul
{α : Type u_1}
[non_unital_semi_normed_ring α] :
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‖) :
has_bounded_smul α β
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 : β) :
has_dist.dist (s • x) (s • y) = ‖s‖ * has_dist.dist 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 : β) :
has_nndist.nndist (s • x) (s • y) = ‖s‖₊ * has_nndist.nndist 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 : β) :
has_edist.edist (s • x) (s • y) = ‖s‖₊ • has_edist.edist x y