Documentation

Mathlib.Data.ENNReal.Action

Scalar multiplication on `ℝ≥0∞`. #

This file defines basic scalar actions on extended nonnegative reals, showing that MulActions, DistribMulActions, Modules and Algebras restrict from ℝ≥0∞ to ℝ≥0.

noncomputable instance ENNReal.instMulActionNNReal {M : Type u_1} [MulAction ENNReal M] :

MulAction NNReal M

A MulAction over ℝ≥0∞ restricts to a MulAction over ℝ≥0.

Equations

theorem ENNReal.smul_def {M : Type u_1} [MulAction ENNReal M] (c : NNReal) (x : M) :

c • x = ↑c • x

instance ENNReal.instIsScalarTowerNNReal {M : Type u_1} {N : Type u_2} [MulAction ENNReal M] [MulAction ENNReal N] [SMul M N] [IsScalarTower ENNReal M N] :

IsScalarTower NNReal M N

instance ENNReal.smulCommClass_left {M : Type u_1} {N : Type u_2} [MulAction ENNReal N] [SMul M N] [SMulCommClass ENNReal M N] :

SMulCommClass NNReal M N

instance ENNReal.smulCommClass_right {M : Type u_1} {N : Type u_2} [MulAction ENNReal N] [SMul M N] [SMulCommClass M ENNReal N] :

SMulCommClass M NNReal N

noncomputable instance ENNReal.instDistribMulActionNNReal {M : Type u_1} [AddMonoid M] [DistribMulAction ENNReal M] :

DistribMulAction NNReal M

A DistribMulAction over ℝ≥0∞ restricts to a DistribMulAction over ℝ≥0.

Equations

noncomputable instance ENNReal.instModuleNNReal {M : Type u_1} [AddCommMonoid M] [Module ENNReal M] :

Module NNReal M

A Module over ℝ≥0∞ restricts to a Module over ℝ≥0.

Equations

noncomputable instance ENNReal.instAlgebraNNReal {A : Type u_1} [Semiring A] [Algebra ENNReal A] :

Algebra NNReal A

An Algebra over ℝ≥0∞ restricts to an Algebra over ℝ≥0.

Equations

theorem ENNReal.coe_smul {R : Type u_1} (r : R) (s : NNReal) [SMul R NNReal] [SMul R ENNReal] [IsScalarTower R NNReal NNReal] [IsScalarTower R NNReal ENNReal] :

↑(r • s) = r • ↑s

theorem ENNReal.smul_top {R : Type u_1} [Zero R] [SMulWithZero R ENNReal] [IsScalarTower R ENNReal ENNReal] [NoZeroSMulDivisors R ENNReal] [DecidableEq R] (c : R) :

c • ⊤ = if c = 0 then 0 else ⊤

theorem ENNReal.nnreal_smul_lt_top {x : NNReal} {y : ENNReal} (hy : y < ⊤) :

theorem ENNReal.nnreal_smul_ne_top {x : NNReal} {y : ENNReal} (hy : y ≠ ⊤) :

x • y ≠ ⊤

theorem ENNReal.nnreal_smul_ne_top_iff {x : NNReal} {y : ENNReal} (hx : x ≠ 0) :

x • y ≠ ⊤ ↔ y ≠ ⊤

theorem ENNReal.nnreal_smul_lt_top_iff {x : NNReal} {y : ENNReal} (hx : x ≠ 0) :

x • y < ⊤ ↔ y < ⊤

@[simp]

theorem ENNReal.smul_toNNReal (a : NNReal) (b : ENNReal) :

(a • b).toNNReal = a * b.toNNReal

theorem ENNReal.toReal_smul (r : NNReal) (s : ENNReal) :

(r • s).toReal = r • s.toReal

instance ENNReal.instPosSMulStrictMonoNNReal :

PosSMulStrictMono NNReal ENNReal

instance ENNReal.instSMulPosMonoNNReal :

SMulPosMono NNReal ENNReal