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.

@[instance_reducible]

noncomputable instance ENNReal.instSMulNNRealOfMulAction {M : Type u_1} [MulAction ENNReal M] : SMul NNReal M

Equations

• ENNReal.instSMulNNRealOfMulAction = { smul := fun (c : NNReal) (m : M) => ↑c • m }

@[instance_reducible]

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 = { toSMul := ENNReal.instSMulNNRealOfMulAction, mul_smul := ⋯, one_smul := ⋯ }

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

@[simp]

theorem ENNReal.smul_one (c : NNReal) : c • 1 = ↑c

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

@[instance_reducible]

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 = { toMulAction := ENNReal.instMulActionNNReal, smul_zero := ⋯, smul_add := ⋯ }

@[instance_reducible]

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 = { toDistribMulAction := ENNReal.instDistribMulActionNNReal, add_smul := ⋯, zero_smul := ⋯ }

@[instance_reducible]

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 = { toSMul := ENNReal.instSMulNNRealOfMulAction, 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} [Semiring R] [IsDomain R] [Module R ENNReal] [IsScalarTower R ENNReal ENNReal] [Module.IsTorsionFree 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

instance ENNReal.instIsOrderedModuleNNReal : IsOrderedModule NNReal ENNReal

instance ENNReal.instIsOrderedSMulNNReal : IsOrderedSMul NNReal ENNReal