Lemmas for IsBoundedSMul
over normed additive groups #
Lemmas which hold only in NormedSpace α β
are provided in another file.
Notably we prove that NonUnitalSeminormedRing
s have bounded actions by left- and right-
multiplication. This allows downstream files to write general results about IsBoundedSMul
, and
then deduce const_mul
and mul_const
results as an immediate corollary.
theorem
norm_smul_le
{α : Type u_1}
{β : Type u_2}
[SeminormedAddGroup α]
[SeminormedAddGroup β]
[SMulZeroClass α β]
[IsBoundedSMul α β]
(r : α)
(x : β)
:
theorem
nnnorm_smul_le
{α : Type u_1}
{β : Type u_2}
[SeminormedAddGroup α]
[SeminormedAddGroup β]
[SMulZeroClass α β]
[IsBoundedSMul α β]
(r : α)
(x : β)
:
theorem
enorm_smul_le
{α : Type u_1}
{β : Type u_2}
[SeminormedAddGroup α]
[SeminormedAddGroup β]
[SMulZeroClass α β]
[IsBoundedSMul α β]
{r : α}
{x : β}
:
theorem
dist_smul_le
{α : Type u_1}
{β : Type u_2}
[SeminormedAddGroup α]
[SeminormedAddGroup β]
[SMulZeroClass α β]
[IsBoundedSMul α β]
(s : α)
(x y : β)
:
theorem
nndist_smul_le
{α : Type u_1}
{β : Type u_2}
[SeminormedAddGroup α]
[SeminormedAddGroup β]
[SMulZeroClass α β]
[IsBoundedSMul α β]
(s : α)
(x y : β)
:
theorem
lipschitzWith_smul
{α : Type u_1}
{β : Type u_2}
[SeminormedAddGroup α]
[SeminormedAddGroup β]
[SMulZeroClass α β]
[IsBoundedSMul α β]
(s : α)
:
LipschitzWith ‖s‖₊ fun (x : β) => s • x
theorem
edist_smul_le
{α : Type u_1}
{β : Type u_2}
[SeminormedAddGroup α]
[SeminormedAddGroup β]
[SMulZeroClass α β]
[IsBoundedSMul α β]
(s : α)
(x y : β)
:
instance
NonUnitalSeminormedRing.isBoundedSMul
{α : Type u_1}
[NonUnitalSeminormedRing α]
:
IsBoundedSMul α α
Left multiplication is bounded.
instance
NonUnitalSeminormedRing.isBoundedSMulOpposite
{α : Type u_1}
[NonUnitalSeminormedRing α]
:
IsBoundedSMul αᵐᵒᵖ α
Right multiplication is bounded.
theorem
IsBoundedSMul.of_norm_smul_le
{α : Type u_1}
{β : Type u_2}
[SeminormedRing α]
[SeminormedAddCommGroup β]
[Module α β]
(h : ∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖)
:
IsBoundedSMul α β
@[deprecated IsBoundedSMul.of_norm_smul_le (since := "2025-03-10")]
theorem
BoundedSMul.of_norm_smul_le
{α : Type u_1}
{β : Type u_2}
[SeminormedRing α]
[SeminormedAddCommGroup β]
[Module α β]
(h : ∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖)
:
IsBoundedSMul α β
Alias of IsBoundedSMul.of_norm_smul_le
.
theorem
IsBoundedSMul.of_nnnorm_smul_le
{α : Type u_1}
{β : Type u_2}
[SeminormedRing α]
[SeminormedAddCommGroup β]
[Module α β]
(h : ∀ (r : α) (x : β), ‖r • x‖₊ ≤ ‖r‖₊ * ‖x‖₊)
:
IsBoundedSMul α β
@[deprecated IsBoundedSMul.of_nnnorm_smul_le (since := "2025-03-10")]
theorem
BoundedSMul.of_nnnorm_smul_le
{α : Type u_1}
{β : Type u_2}
[SeminormedRing α]
[SeminormedAddCommGroup β]
[Module α β]
(h : ∀ (r : α) (x : β), ‖r • x‖₊ ≤ ‖r‖₊ * ‖x‖₊)
:
IsBoundedSMul α β
Alias of IsBoundedSMul.of_nnnorm_smul_le
.
theorem
norm_smul
{α : Type u_1}
{β : Type u_2}
[NormedDivisionRing α]
[SeminormedAddGroup β]
[MulActionWithZero α β]
[IsBoundedSMul α β]
(r : α)
(x : β)
:
theorem
nnnorm_smul
{α : Type u_1}
{β : Type u_2}
[NormedDivisionRing α]
[SeminormedAddGroup β]
[MulActionWithZero α β]
[IsBoundedSMul α β]
(r : α)
(x : β)
:
theorem
enorm_smul
{α : Type u_1}
{β : Type u_2}
[NormedDivisionRing α]
[SeminormedAddGroup β]
[MulActionWithZero α β]
[IsBoundedSMul α β]
(r : α)
(x : β)
:
theorem
dist_smul₀
{α : Type u_1}
{β : Type u_2}
[NormedDivisionRing α]
[SeminormedAddCommGroup β]
[Module α β]
[IsBoundedSMul α β]
(s : α)
(x y : β)
:
theorem
nndist_smul₀
{α : Type u_1}
{β : Type u_2}
[NormedDivisionRing α]
[SeminormedAddCommGroup β]
[Module α β]
[IsBoundedSMul α β]
(s : α)
(x y : β)
:
theorem
edist_smul₀
{α : Type u_1}
{β : Type u_2}
[NormedDivisionRing α]
[SeminormedAddCommGroup β]
[Module α β]
[IsBoundedSMul α β]
(s : α)
(x y : β)
: