Mathlib.Analysis.Normed.MulAction

norm_smul_le theorem

(r : α) (x : β) : ‖r • x‖ ≤ ‖r‖ * ‖x‖

Full source

@[bound]
theorem norm_smul_le (r : α) (x : β) : ‖r • x‖ ≤ ‖r‖ * ‖x‖ := by
  simpa [smul_zero] using dist_smul_pair r 0 x

Norm Bound for Scalar Multiplication: $\|r \cdot x\| \leq \|r\| \cdot \|x\|$

Informal description

For any element $r$ in a normed space $\alpha$ and any element $x$ in a normed space $\beta$, the norm of the scalar multiplication $r \cdot x$ is bounded by the product of the norms of $r$ and $x$, i.e., \[ \|r \cdot x\| \leq \|r\| \cdot \|x\|. \]

nnnorm_smul_le theorem

(r : α) (x : β) : ‖r • x‖₊ ≤ ‖r‖₊ * ‖x‖₊

Full source

@[bound]
theorem nnnorm_smul_le (r : α) (x : β) : ‖r • x‖₊ ≤ ‖r‖₊ * ‖x‖₊ :=
  norm_smul_le _ _

Non-Negative Norm Bound for Scalar Multiplication: $\|r \cdot x\|_+ \leq \|r\|_+ \cdot \|x\|_+$

Informal description

For any element $r$ in a normed space $\alpha$ and any element $x$ in a normed space $\beta$, the non-negative norm of the scalar multiplication $r \cdot x$ is bounded by the product of the non-negative norms of $r$ and $x$, i.e., \[ \|r \cdot x\|_+ \leq \|r\|_+ \cdot \|x\|_+. \]

enorm_smul_le theorem

: ‖r • x‖ₑ ≤ ‖r‖ₑ * ‖x‖ₑ

Full source

@[bound]
lemma enorm_smul_le : ‖r • x‖ₑ ≤ ‖r‖ₑ * ‖x‖ₑ := by
  simpa [enorm, ← ENNReal.coe_mul] using nnnorm_smul_le ..

Extended Norm Bound for Scalar Multiplication: $\|r \cdot x\|_e \leq \|r\|_e \cdot \|x\|_e$

Informal description

For any element $r$ in a seminormed additive group $\alpha$ and any element $x$ in a seminormed additive group $\beta$, the extended norm of the scalar multiplication $r \cdot x$ is bounded by the product of the extended norms of $r$ and $x$, i.e., \[ \|r \cdot x\|_e \leq \|r\|_e \cdot \|x\|_e. \]

dist_smul_le theorem

(s : α) (x y : β) : dist (s • x) (s • y) ≤ ‖s‖ * dist x y

Full source

theorem dist_smul_le (s : α) (x y : β) : dist (s • x) (s • y) ≤ ‖s‖ * dist x y := by
  simpa only [dist_eq_norm, sub_zero] using dist_smul_pair s x y

Distance Bound for Scalar Multiplication: $\text{dist}(s \cdot x, s \cdot y) \leq \|s\| \cdot \text{dist}(x, y)$

Informal description

For any element $s$ in a seminormed additive group $\alpha$ and any elements $x, y$ in a seminormed additive group $\beta$, the distance between the scalar multiplications $s \cdot x$ and $s \cdot y$ is bounded by the product of the norm of $s$ and the distance between $x$ and $y$, i.e., \[ \text{dist}(s \cdot x, s \cdot y) \leq \|s\| \cdot \text{dist}(x, y). \]

nndist_smul_le theorem

(s : α) (x y : β) : nndist (s • x) (s • y) ≤ ‖s‖₊ * nndist x y

Full source

theorem nndist_smul_le (s : α) (x y : β) : nndist (s • x) (s • y) ≤ ‖s‖₊ * nndist x y :=
  dist_smul_le s x y

Non-Negative Distance Bound for Scalar Multiplication: $\text{nndist}(s \cdot x, s \cdot y) \leq \|s\| \cdot \text{nndist}(x, y)$

Informal description

For any element $s$ in a seminormed additive group $\alpha$ and any elements $x, y$ in a seminormed additive group $\beta$, the non-negative distance between the scalar multiplications $s \cdot x$ and $s \cdot y$ is bounded by the product of the seminorm of $s$ and the non-negative distance between $x$ and $y$, i.e., \[ \text{nndist}(s \cdot x, s \cdot y) \leq \|s\| \cdot \text{nndist}(x, y). \]

lipschitzWith_smul theorem

(s : α) : LipschitzWith ‖s‖₊ (s • · : β → β)

Full source

theorem lipschitzWith_smul (s : α) : LipschitzWith ‖s‖₊ (s • · : β → β) :=
  lipschitzWith_iff_dist_le_mul.2 <| dist_smul_le _

Lipschitz Continuity of Scalar Multiplication with Constant $\|s\|$

Informal description

For any element $s$ in a seminormed additive group $\alpha$, the scalar multiplication map $x \mapsto s \cdot x$ from $\beta$ to $\beta$ is Lipschitz continuous with constant $\|s\|$.

edist_smul_le theorem

(s : α) (x y : β) : edist (s • x) (s • y) ≤ ‖s‖₊ • edist x y

Full source

theorem edist_smul_le (s : α) (x y : β) : edist (s • x) (s • y) ≤ ‖s‖₊ • edist x y :=
  lipschitzWith_smul s x y

Extended Distance Bound for Scalar Multiplication: $\text{edist}(s \cdot x, s \cdot y) \leq \|s\| \cdot \text{edist}(x, y)$

Informal description

For any element $s$ in a seminormed additive group $\alpha$ and any elements $x, y$ in a seminormed additive group $\beta$, the extended distance between the scalar multiplications $s \cdot x$ and $s \cdot y$ is bounded by the product of the seminorm of $s$ and the extended distance between $x$ and $y$, i.e., \[ \text{edist}(s \cdot x, s \cdot y) \leq \|s\| \cdot \text{edist}(x, y). \]

NonUnitalSeminormedRing.isBoundedSMul instance

[NonUnitalSeminormedRing α] : IsBoundedSMul α α

Full source

/-- Left multiplication is bounded. -/
instance NonUnitalSeminormedRing.isBoundedSMul [NonUnitalSeminormedRing α] :
    IsBoundedSMul α α where
  dist_smul_pair' x y₁ y₂ := by simpa [mul_sub, dist_eq_norm] using norm_mul_le x (y₁ - y₂)
  dist_pair_smul' x₁ x₂ y := by simpa [sub_mul, dist_eq_norm] using norm_mul_le (x₁ - x₂) y

Bounded Left Multiplication in Non-Unital Seminormed Rings

Informal description

For any non-unital seminormed ring $\alpha$, the scalar multiplication operation on $\alpha$ is bounded. This means that left multiplication by any element $a \in \alpha$ is a bounded operator with respect to the norm, satisfying $\|a \cdot x\| \leq \|a\| \cdot \|x\|$ for all $x \in \alpha$.

NonUnitalSeminormedRing.isBoundedSMulOpposite instance

[NonUnitalSeminormedRing α] : IsBoundedSMul αᵐᵒᵖ α

Full source

/-- Right multiplication is bounded. -/
instance NonUnitalSeminormedRing.isBoundedSMulOpposite [NonUnitalSeminormedRing α] :
    IsBoundedSMul αᵐᵒᵖ α where
  dist_smul_pair' x y₁ y₂ := by
    simpa [sub_mul, dist_eq_norm, mul_comm] using norm_mul_le (y₁ - y₂) x.unop
  dist_pair_smul' x₁ x₂ y := by
    simpa [mul_sub, dist_eq_norm, mul_comm] using norm_mul_le y (x₁ - x₂).unop

Bounded Right Multiplication in Non-Unital Seminormed Rings

Informal description

For any non-unital seminormed ring $\alpha$, the scalar multiplication operation on $\alpha$ by elements from its multiplicative opposite $\alpha^\text{op}$ is bounded. This means that right multiplication by any element $a \in \alpha$ is a bounded operator with respect to the norm, satisfying $\|x \cdot a\| \leq \|x\| \cdot \|a\|$ for all $x \in \alpha$.

IsBoundedSMul.of_norm_smul_le theorem

(h : ∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖) : IsBoundedSMul α β

Full source

theorem IsBoundedSMul.of_norm_smul_le (h : ∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖) :
    IsBoundedSMul α β :=
  { dist_smul_pair' := fun a b₁ b₂ => by simpa [smul_sub, dist_eq_norm] using h a (b₁ - b₂)
    dist_pair_smul' := fun a₁ a₂ b => by simpa [sub_smul, dist_eq_norm] using h (a₁ - a₂) b }

Boundedness of Scalar Multiplication via Norm Inequality

Informal description

Let $\alpha$ and $\beta$ be seminormed additive commutative groups. If for all $r \in \alpha$ and $x \in \beta$ the norm of the scalar multiplication satisfies $\|r \cdot x\| \leq \|r\| \cdot \|x\|$, then the scalar multiplication operation is bounded (i.e., satisfies the conditions of `IsBoundedSMul`).

IsBoundedSMul.of_nnnorm_smul_le theorem

(h : ∀ (r : α) (x : β), ‖r • x‖₊ ≤ ‖r‖₊ * ‖x‖₊) : IsBoundedSMul α β

Full source

theorem IsBoundedSMul.of_nnnorm_smul_le (h : ∀ (r : α) (x : β), ‖r • x‖₊ ≤ ‖r‖₊ * ‖x‖₊) :
    IsBoundedSMul α β := .of_norm_smul_le h

Boundedness of Scalar Multiplication via Non-Negative Norm Inequality

Informal description

Let $\alpha$ and $\beta$ be seminormed additive commutative groups. If for all $r \in \alpha$ and $x \in \beta$ the non-negative norm of the scalar multiplication satisfies $\|r \cdot x\|_{\text{nn}} \leq \|r\|_{\text{nn}} \cdot \|x\|_{\text{nn}}$, then the scalar multiplication operation is bounded (i.e., satisfies the conditions of `IsBoundedSMul`).

norm_smul theorem

(r : α) (x : β) : ‖r • x‖ = ‖r‖ * ‖x‖

Full source

theorem norm_smul (r : α) (x : β) : ‖r • x‖ = ‖r‖ * ‖x‖ := by
  by_cases h : r = 0
  · simp [h, zero_smul α x]
  · refine le_antisymm (norm_smul_le r x) ?_
    calc
      ‖r‖ * ‖x‖ = ‖r‖ * ‖r⁻¹ • r • x‖ := by rw [inv_smul_smul₀ h]
      _ ≤ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖) := by gcongr; apply norm_smul_le
      _ = ‖r • x‖ := by rw [norm_inv, ← mul_assoc, mul_inv_cancel₀ (mt norm_eq_zero.1 h), one_mul]

Norm Multiplicativity in Scalar Multiplication: $\|r \cdot x\| = \|r\| \cdot \|x\|$

Informal description

For any element $r$ in a normed division ring $\alpha$ and any element $x$ in a normed space $\beta$, the norm of the scalar multiplication $r \cdot x$ equals the product of the norms of $r$ and $x$, i.e., \[ \|r \cdot x\| = \|r\| \cdot \|x\|. \]

nnnorm_smul theorem

(r : α) (x : β) : ‖r • x‖₊ = ‖r‖₊ * ‖x‖₊

Full source

theorem nnnorm_smul (r : α) (x : β) : ‖r • x‖₊ = ‖r‖₊ * ‖x‖₊ :=
  NNReal.eq <| norm_smul r x

Non-Negative Norm Multiplicativity in Scalar Multiplication: $\|r \cdot x\|_{\text{nn}} = \|r\|_{\text{nn}} \cdot \|x\|_{\text{nn}}$

Informal description

For any element $r$ in a normed division ring $\alpha$ and any element $x$ in a normed space $\beta$, the non-negative norm of the scalar multiplication $r \cdot x$ equals the product of the non-negative norms of $r$ and $x$, i.e., \[ \|r \cdot x\|_{\text{nn}} = \|r\|_{\text{nn}} \cdot \|x\|_{\text{nn}}. \]

enorm_smul theorem

(r : α) (x : β) : ‖r • x‖ₑ = ‖r‖ₑ * ‖x‖ₑ

Full source

lemma enorm_smul (r : α) (x : β) : ‖r • x‖ₑ = ‖r‖ₑ * ‖x‖ₑ := by simp [enorm, nnnorm_smul]

Extended Norm Multiplicativity in Scalar Multiplication: $\|r \cdot x\|_e = \|r\|_e \cdot \|x\|_e$

Informal description

For any element $r$ in a normed division ring $\alpha$ and any element $x$ in a seminormed additive commutative group $\beta$, the extended norm of the scalar multiplication $r \cdot x$ equals the product of the extended norms of $r$ and $x$, i.e., \[ \|r \cdot x\|_e = \|r\|_e \cdot \|x\|_e. \]

dist_smul₀ theorem

(s : α) (x y : β) : dist (s • x) (s • y) = ‖s‖ * dist x y

Full source

theorem dist_smul₀ (s : α) (x y : β) : dist (s • x) (s • y) = ‖s‖ * dist x y := by
  simp_rw [dist_eq_norm, (norm_smul s (x - y)).symm, smul_sub]

Distance Preservation under Scalar Multiplication: $\text{dist}(s \cdot x, s \cdot y) = \|s\| \cdot \text{dist}(x, y)$

Informal description

For any scalar $s$ in a normed division ring $\alpha$ and any elements $x, y$ in a seminormed additive commutative group $\beta$, the distance between the scalar multiples $s \cdot x$ and $s \cdot y$ is equal to the product of the norm of $s$ and the distance between $x$ and $y$, i.e., \[ \text{dist}(s \cdot x, s \cdot y) = \|s\| \cdot \text{dist}(x, y). \]

nndist_smul₀ theorem

(s : α) (x y : β) : nndist (s • x) (s • y) = ‖s‖₊ * nndist x y

Full source

theorem nndist_smul₀ (s : α) (x y : β) : nndist (s • x) (s • y) = ‖s‖₊ * nndist x y :=
  NNReal.eq <| dist_smul₀ s x y

Non-Negative Distance Preservation under Scalar Multiplication: $\text{nndist}(s \cdot x, s \cdot y) = \|s\|_+ \cdot \text{nndist}(x, y)$

Informal description

For any scalar $s$ in a normed division ring $\alpha$ and any elements $x, y$ in a seminormed additive commutative group $\beta$, the non-negative distance between the scalar multiples $s \cdot x$ and $s \cdot y$ is equal to the product of the non-negative norm of $s$ and the non-negative distance between $x$ and $y$, i.e., \[ \text{nndist}(s \cdot x, s \cdot y) = \|s\|_+ \cdot \text{nndist}(x, y). \]

edist_smul₀ theorem

(s : α) (x y : β) : edist (s • x) (s • y) = ‖s‖₊ • edist x y

Full source

theorem edist_smul₀ (s : α) (x y : β) : edist (s • x) (s • y) = ‖s‖₊ • edist x y := by
  simp only [edist_nndist, nndist_smul₀, ENNReal.coe_mul, ENNReal.smul_def, smul_eq_mul]

Extended Distance Preservation under Scalar Multiplication: $\text{edist}(s \cdot x, s \cdot y) = \|s\|_+ \cdot \text{edist}(x, y)$

Informal description

For any scalar $s$ in a normed division ring $\alpha$ and any elements $x, y$ in a seminormed additive commutative group $\beta$, the extended distance between the scalar multiples $s \cdot x$ and $s \cdot y$ is equal to the extended nonnegative real number obtained by multiplying the non-negative norm of $s$ with the extended distance between $x$ and $y$, i.e., \[ \text{edist}(s \cdot x, s \cdot y) = \|s\|_+ \cdot \text{edist}(x, y). \]