Documentation

Mathlib.Basic.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.

source
@[instance_reducible]
noncomputable instance ENNReal.instSMulNNRealOfMulAction {M : Type u_1} [MulAction ENNReal M] :
SMul NNReal M
source
@[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.

source
theorem ENNReal.smul_def {M : Type u_1} [MulAction ENNReal M] (c : NNReal) (x : M) :
c • x = ↑c • x
source
@[simp]
theorem ENNReal.smul_one (c : NNReal) :
c • 1 = ↑c
source
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
source
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
source
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
source
@[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.

source
@[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.

source
@[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.

source
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
source
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 ⊤
source
theorem ENNReal.nnreal_smul_lt_top {x : NNReal} {y : ENNReal} (hy : y < ⊤) :
x • y < ⊤
source
theorem ENNReal.nnreal_smul_ne_top {x : NNReal} {y : ENNReal} (hy : y ≠ ⊤) :
x • y ≠ ⊤
source
theorem ENNReal.nnreal_smul_ne_top_iff {x : NNReal} {y : ENNReal} (hx : x ≠ 0) :
x • y ≠ ⊤ ↔ y ≠ ⊤
source
theorem ENNReal.nnreal_smul_lt_top_iff {x : NNReal} {y : ENNReal} (hx : x ≠ 0) :
x • y < ⊤ ↔ y < ⊤
source
@[simp]
theorem ENNReal.smul_toNNReal (a : NNReal) (b : ENNReal) :
(a • b).toNNReal = a * b.toNNReal
source
theorem ENNReal.toReal_smul (r : NNReal) (s : ENNReal) :
(r • s).toReal = r • s.toReal
source
instance ENNReal.instPosSMulStrictMonoNNReal :
PosSMulStrictMono NNReal ENNReal
source
instance ENNReal.instSMulPosMonoNNReal :
SMulPosMono NNReal ENNReal
source
instance ENNReal.instIsOrderedModuleNNReal :
IsOrderedModule NNReal ENNReal
source
instance ENNReal.instIsOrderedSMulNNReal :
IsOrderedSMul NNReal ENNReal