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

• ENNReal.instMulActionNNReal = MulAction.compHom M ↑ENNReal.ofNNRealHom

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

• ENNReal.instDistribMulActionNNReal = DistribMulAction.compHom M ↑ENNReal.ofNNRealHom

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

• ENNReal.instModuleNNReal = Module.compHom M ENNReal.ofNNRealHom

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

• ENNReal.instAlgebraNNReal = { smul := fun (x1 : NNReal) (x2 : A) => x1 • x2, algebraMap := (algebraMap ENNReal A).comp ENNReal.ofNNRealHom, commutes' := ⋯, smul_def' := ⋯ }

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 < ⊤) : x • 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