Mathlib.Data.ENNReal.Action

ENNReal.instMulActionNNReal instance

{M : Type*} [MulAction ℝ≥0∞ M] : MulAction ℝ≥0 M

Full source

/-- A `MulAction` over `ℝ≥0∞` restricts to a `MulAction` over `ℝ≥0`. -/
noncomputable instance {M : Type*} [MulAction ℝ≥0∞ M] : MulAction ℝ≥0 M :=
  MulAction.compHom M ofNNRealHom.toMonoidHom

Restriction of Multiplicative Action from Extended Nonnegative Reals to Nonnegative Reals

Informal description

For any type $M$ with a multiplicative action by the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$, there is an induced multiplicative action by the nonnegative real numbers $\mathbb{R}_{\geq 0}$ on $M$. This action is defined by composing the inclusion map $\mathbb{R}_{\geq 0} \hookrightarrow \mathbb{R}_{\geq 0} \cup \{\infty\}$ with the given action.

ENNReal.smul_def theorem

{M : Type*} [MulAction ℝ≥0∞ M] (c : ℝ≥0) (x : M) : c • x = (c : ℝ≥0∞) • x

Full source

theorem smul_def {M : Type*} [MulAction ℝ≥0∞ M] (c : ℝ≥0) (x : M) : c • x = (c : ℝ≥0∞) • x :=
  rfl

Scalar Multiplication Definition for Nonnegative Reals on Extended Nonnegative Reals Action

Informal description

For any type $M$ with a multiplicative action by the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$, and for any nonnegative real number $c \in \mathbb{R}_{\geq 0}$ and any element $x \in M$, the scalar multiplication $c \cdot x$ is equal to the scalar multiplication of the image of $c$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$ with $x$.

ENNReal.instIsScalarTowerNNReal instance

 {M N : Type*} [MulAction ℝ≥0∞ M] [MulAction ℝ≥0∞ N] [SMul M N] [IsScalarTower ℝ≥0∞ M N] : IsScalarTower ℝ≥0 M N

Full source

instance {M N : Type*} [MulAction ℝ≥0∞ M] [MulAction ℝ≥0∞ N] [SMul M N] [IsScalarTower ℝ≥0∞ M N] :
    IsScalarTower ℝ≥0 M N where smul_assoc r := smul_assoc (r : ℝ≥0∞)

Scalar Tower Property for Nonnegative Reals in Extended Nonnegative Real Actions

Informal description

For any types $M$ and $N$ with multiplicative actions by the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$, and a scalar multiplication operation $M \to N \to N$ that forms a scalar tower with $\mathbb{R}_{\geq 0} \cup \{\infty\}$, the same scalar multiplication operation also forms a scalar tower with the nonnegative real numbers $\mathbb{R}_{\geq 0}$.

ENNReal.smulCommClass_left instance

{M N : Type*} [MulAction ℝ≥0∞ N] [SMul M N] [SMulCommClass ℝ≥0∞ M N] : SMulCommClass ℝ≥0 M N

Full source

instance smulCommClass_left {M N : Type*} [MulAction ℝ≥0∞ N] [SMul M N] [SMulCommClass ℝ≥0∞ M N] :
    SMulCommClass ℝ≥0 M N where smul_comm r := smul_comm (r : ℝ≥0∞)

Commutation of Scalar Multiplication with Nonnegative Real Action

Informal description

For any types $M$ and $N$ with a multiplicative action by the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ on $N$, and a scalar multiplication operation $M \times N \to N$ that commutes with the action of $\mathbb{R}_{\geq 0} \cup \{\infty\}$, the scalar multiplication operation also commutes with the action of the nonnegative real numbers $\mathbb{R}_{\geq 0}$.

ENNReal.smulCommClass_right instance

{M N : Type*} [MulAction ℝ≥0∞ N] [SMul M N] [SMulCommClass M ℝ≥0∞ N] : SMulCommClass M ℝ≥0 N

Full source

instance smulCommClass_right {M N : Type*} [MulAction ℝ≥0∞ N] [SMul M N] [SMulCommClass M ℝ≥0∞ N] :
    SMulCommClass M ℝ≥0 N where smul_comm m r := smul_comm m (r : ℝ≥0∞)

Commutation of Scalar Multiplication with Nonnegative Real Action

Informal description

For any types $M$ and $N$ with a multiplicative action by the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ on $N$, and a scalar multiplication operation $M \times N \to N$ that commutes with the action of $\mathbb{R}_{\geq 0} \cup \{\infty\}$, the scalar multiplication operation also commutes with the action of the nonnegative real numbers $\mathbb{R}_{\geq 0}$.

ENNReal.instDistribMulActionNNReal instance

{M : Type*} [AddMonoid M] [DistribMulAction ℝ≥0∞ M] : DistribMulAction ℝ≥0 M

Full source

/-- A `DistribMulAction` over `ℝ≥0∞` restricts to a `DistribMulAction` over `ℝ≥0`. -/
noncomputable instance {M : Type*} [AddMonoid M] [DistribMulAction ℝ≥0∞ M] :
    DistribMulAction ℝ≥0 M :=
  DistribMulAction.compHom M ofNNRealHom.toMonoidHom

Distributive Multiplicative Action of Nonnegative Reals on Monoids with Extended Nonnegative Real Action

Informal description

For any additive monoid $M$ with a distributive multiplicative action by the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$, there is an induced distributive multiplicative action by the nonnegative real numbers $\mathbb{R}_{\geq 0}$ on $M$.

ENNReal.instModuleNNReal instance

{M : Type*} [AddCommMonoid M] [Module ℝ≥0∞ M] : Module ℝ≥0 M

Full source

/-- A `Module` over `ℝ≥0∞` restricts to a `Module` over `ℝ≥0`. -/
noncomputable instance {M : Type*} [AddCommMonoid M] [Module ℝ≥0∞ M] : Module ℝ≥0 M :=
  Module.compHom M ofNNRealHom

Module Structure Restriction from Extended to Nonnegative Reals

Informal description

For any additively commutative monoid $M$ equipped with a module structure over the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$, $M$ is also a module over the nonnegative real numbers $\mathbb{R}_{\geq 0}$.

ENNReal.instAlgebraNNReal instance

{A : Type*} [Semiring A] [Algebra ℝ≥0∞ A] : Algebra ℝ≥0 A

Full source

/-- An `Algebra` over `ℝ≥0∞` restricts to an `Algebra` over `ℝ≥0`. -/
noncomputable instance {A : Type*} [Semiring A] [Algebra ℝ≥0∞ A] : Algebra ℝ≥0 A where
  smul := (· • ·)
  commutes' r x := by simp [Algebra.commutes]
  smul_def' r x := by simp [← Algebra.smul_def (r : ℝ≥0∞) x, smul_def]
  algebraMap := (algebraMap ℝ≥0∞ A).comp (ofNNRealHom : ℝ≥0 →+* ℝ≥0∞)

Algebra Structure Restriction from Extended to Nonnegative Reals

Informal description

For any semiring $A$ with an algebra structure over the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$, $A$ is also an algebra over the nonnegative real numbers $\mathbb{R}_{\geq 0}$.

ENNReal.coe_smul theorem

 {R} (r : R) (s : ℝ≥0) [SMul R ℝ≥0] [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0 ℝ≥0] [IsScalarTower R ℝ≥0 ℝ≥0∞] :
  (↑(r • s) : ℝ≥0∞) = (r : R) • (s : ℝ≥0∞)

Full source

theorem coe_smul {R} (r : R) (s : ℝ≥0) [SMul R ℝ≥0] [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0 ℝ≥0]
    [IsScalarTower R ℝ≥0 ℝ≥0∞] : (↑(r • s) : ℝ≥0∞) = (r : R) • (s : ℝ≥0∞) := by
  rw [← smul_one_smul ℝ≥0 r (s : ℝ≥0∞), smul_def, smul_eq_mul, ← ENNReal.coe_mul, smul_mul_assoc,
    one_mul]

Compatibility of Scalar Multiplication with Inclusion in Extended Nonnegative Reals

Informal description

Let $R$ be a type with scalar multiplication operations on both $\mathbb{R}_{\geq 0}$ and $\mathbb{R}_{\geq 0} \cup \{\infty\}$, such that $R$ forms a scalar tower over $\mathbb{R}_{\geq 0}$ and $\mathbb{R}_{\geq 0} \cup \{\infty\}$. For any $r \in R$ and $s \in \mathbb{R}_{\geq 0}$, the image of the scalar product $r \cdot s$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to the scalar product of $r$ with the image of $s$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$. That is, \[ (r \cdot s : \mathbb{R}_{\geq 0} \cup \{\infty\}) = r \cdot (s : \mathbb{R}_{\geq 0} \cup \{\infty\}). \]

ENNReal.smul_top theorem

 {R} [Zero R] [SMulWithZero R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] [NoZeroSMulDivisors R ℝ≥0∞] [DecidableEq R] (c : R) :
  c • ∞ = if c = 0 then 0 else ∞

Full source

theorem smul_top {R} [Zero R] [SMulWithZero R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞]
    [NoZeroSMulDivisors R ℝ≥0∞] [DecidableEq R] (c : R) :
    c • ∞ = if c = 0 then 0 else ∞ := by
  rw [← smul_one_mul, mul_top']
  simp_rw [smul_eq_zero, or_iff_left one_ne_zero]

Scalar Multiplication of Infinity in Extended Nonnegative Reals: $c \cdot \infty = \begin{cases} 0 & \text{if } c = 0, \\ \infty & \text{otherwise} \end{cases}$

Informal description

Let $R$ be a type with a zero element and a scalar multiplication operation on the extended nonnegative reals $\mathbb{R}_{\geq 0} \cup \{\infty\}$, such that $R$ forms a scalar tower over $\mathbb{R}_{\geq 0} \cup \{\infty\}$ and has no zero scalar divisors. For any $c \in R$, the scalar multiplication of $c$ with $\infty$ is given by: \[ c \cdot \infty = \begin{cases} 0 & \text{if } c = 0, \\ \infty & \text{otherwise.} \end{cases} \]

ENNReal.nnreal_smul_lt_top theorem

{x : ℝ≥0} {y : ℝ≥0∞} (hy : y < ⊤) : x • y < ⊤

Full source

lemma nnreal_smul_lt_top {x : ℝ≥0} {y : ℝ≥0∞} (hy : y < ⊤) : x • y < ⊤ := mul_lt_top (by simp) hy

Finite Scalar Multiplication Preserves Finiteness in Extended Nonnegative Reals

Informal description

For any nonnegative real number $x \in \mathbb{R}_{\geq 0}$ and any extended nonnegative real number $y \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $y < \infty$, then the scalar multiplication $x \cdot y$ is also strictly less than $\infty$.

ENNReal.nnreal_smul_ne_top theorem

{x : ℝ≥0} {y : ℝ≥0∞} (hy : y ≠ ⊤) : x • y ≠ ⊤

Full source

lemma nnreal_smul_ne_top {x : ℝ≥0} {y : ℝ≥0∞} (hy : y ≠ ⊤) : x • y ≠ ⊤ := mul_ne_top (by simp) hy

Nonzero Scalar Multiplication Preserves Finiteness in Extended Nonnegative Reals

Informal description

For any nonnegative real number $x \in \mathbb{R}_{\geq 0}$ and any extended nonnegative real number $y \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $y \neq \infty$, then the scalar multiplication $x \cdot y$ is also not equal to $\infty$.

ENNReal.nnreal_smul_ne_top_iff theorem

{x : ℝ≥0} {y : ℝ≥0∞} (hx : x ≠ 0) : x • y ≠ ⊤ ↔ y ≠ ⊤

Full source

lemma nnreal_smul_ne_top_iff {x : ℝ≥0} {y : ℝ≥0∞} (hx : x ≠ 0) : x • y ≠ ⊤x • y ≠ ⊤ ↔ y ≠ ⊤ :=
  ⟨by rintro h rfl; simp [smul_top, hx] at h, nnreal_smul_ne_top⟩

Scalar Multiplication Finiteness Criterion: $x \cdot y \neq \infty \leftrightarrow y \neq \infty$ for $x \neq 0$

Informal description

For any nonzero nonnegative real number $x \in \mathbb{R}_{\geq 0}$ and any extended nonnegative real number $y \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the scalar multiplication $x \cdot y$ is not equal to $\infty$ if and only if $y$ is not equal to $\infty$.

ENNReal.nnreal_smul_lt_top_iff theorem

{x : ℝ≥0} {y : ℝ≥0∞} (hx : x ≠ 0) : x • y < ⊤ ↔ y < ⊤

Full source

lemma nnreal_smul_lt_top_iff {x : ℝ≥0} {y : ℝ≥0∞} (hx : x ≠ 0) : x • y < ⊤ ↔ y < ⊤ := by
  rw [lt_top_iff_ne_top, lt_top_iff_ne_top, nnreal_smul_ne_top_iff hx]

Scalar Multiplication Strict Finiteness Criterion: $x \cdot y < \infty \leftrightarrow y < \infty$ for $x \neq 0$

Informal description

For any nonzero nonnegative real number $x \in \mathbb{R}_{\geq 0}$ and any extended nonnegative real number $y \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the scalar multiplication $x \cdot y$ is strictly less than $\infty$ if and only if $y$ is strictly less than $\infty$.

ENNReal.smul_toNNReal theorem

(a : ℝ≥0) (b : ℝ≥0∞) : (a • b).toNNReal = a * b.toNNReal

Full source

@[simp]
theorem smul_toNNReal (a : ℝ≥0) (b : ℝ≥0∞) : (a • b).toNNReal = a * b.toNNReal := by
  change ((a : ℝ≥0∞) * b).toNNReal = a * b.toNNReal
  simp only [ENNReal.toNNReal_mul, ENNReal.toNNReal_coe]

Scalar Multiplication Preserves Nonnegative Real Part: $\text{toNNReal}(a \cdot b) = a \cdot \text{toNNReal}(b)$

Informal description

For any nonnegative real number $a$ and any extended nonnegative real number $b$, the nonnegative real part of the scalar product $a \cdot b$ is equal to the product of $a$ and the nonnegative real part of $b$, i.e., \[ \text{toNNReal}(a \cdot b) = a \cdot \text{toNNReal}(b). \]

ENNReal.toReal_smul theorem

(r : ℝ≥0) (s : ℝ≥0∞) : (r • s).toReal = r • s.toReal

Full source

theorem toReal_smul (r : ℝ≥0) (s : ℝ≥0∞) : (r • s).toReal = r • s.toReal := by
  rw [ENNReal.smul_def, smul_eq_mul, toReal_mul, coe_toReal]
  rfl

Real Conversion Preserves Scalar Multiplication: $(r \cdot s).\text{toReal} = r \cdot s.\text{toReal}$

Informal description

For any nonnegative real number $r$ and any extended nonnegative real number $s$, the real-valued conversion of the scalar product $r \cdot s$ is equal to the scalar product of $r$ with the real-valued conversion of $s$, i.e., \[ (r \cdot s).\text{toReal} = r \cdot s.\text{toReal}. \]

ENNReal.instPosSMulStrictMonoNNReal instance

: PosSMulStrictMono ℝ≥0 ℝ≥0∞

Full source

instance : PosSMulStrictMono ℝ≥0 ℝ≥0∞ where
  elim _r hr _a _b hab := ENNReal.mul_lt_mul_left' (coe_pos.2 hr).ne' coe_ne_top hab

Strict Monotonicity of Scalar Multiplication on Extended Nonnegative Reals

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ have a scalar multiplication structure by nonnegative real numbers $\mathbb{R}_{\geq 0}$ that is strictly monotone with respect to the first argument. That is, for any $r_1, r_2 \in \mathbb{R}_{\geq 0}$ and $s \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $r_1 < r_2$ and $s \neq 0$, then $r_1 \cdot s < r_2 \cdot s$.

ENNReal.instSMulPosMonoNNReal instance

: SMulPosMono ℝ≥0 ℝ≥0∞

Full source

instance : SMulPosMono ℝ≥0 ℝ≥0∞ where
  elim _r _ _a _b hab := mul_le_mul_right' (coe_le_coe.2 hab) _

Monotonicity of Scalar Multiplication on Extended Nonnegative Reals

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ have a scalar multiplication structure by nonnegative real numbers $\mathbb{R}_{\geq 0}$ that is monotone with respect to the second argument. That is, for any $r \in \mathbb{R}_{\geq 0}$ and $s_1, s_2 \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $s_1 \leq s_2$, then $r \cdot s_1 \leq r \cdot s_2$.