Action

📁 Source: Mathlib/Data/ENNReal/Action.lean

Statistics

Metric	Count
Definitions instAlgebraNNReal, instDistribMulActionNNReal, instModuleNNReal, instMulActionNNReal	4
Theorems coe_smul, instIsScalarTowerNNReal, instPosSMulStrictMonoNNReal, instSMulPosMonoNNReal, nnreal_smul_lt_top, nnreal_smul_lt_top_iff, nnreal_smul_ne_top, nnreal_smul_ne_top_iff, smulCommClass_left, smulCommClass_right, smul_def, smul_toNNReal, smul_top, toReal_smul	14
Total	18

ENNReal

Definitions

Name	Category	Theorems
instAlgebraNNReal 📖	CompOp	131 math math: MeasureTheory.Measure.MutuallySingular.smul_nnreal, MeasureTheory.Measure.IsHaarMeasure.nnreal_smul, MeasureTheory.Measure.isAddInvariant_eq_smul_of_compactSpace, MeasureTheory.integral_smul_nnreal_measure, MeasureTheory.Measure.WeaklyRegular.smul_nnreal, nnreal_smul_lt_top, MeasureTheory.Measure.rnDeriv_smul_right', MeasureTheory.Measure.measure_isMulLeftInvariant_eq_smul_of_ne_top, MeasureTheory.smul_le_stoppedValue_hittingBtwn, MeasureTheory.Measure.haveLebesgueDecompositionSMul, MeasureTheory.le_eLpNorm_of_bddBelow, MeasureTheory.Measure.coe_nnreal_smul_apply, MeasureTheory.eLpNorm_smul_measure_of_ne_top', MeasureTheory.Measure.rnDeriv_smul_right, MeasureTheory.eLpNorm_le_of_ae_nnnorm_bound, MeasureTheory.Measure.haarScalarFactor_smul, MeasureTheory.Measure.OuterRegular.smul_nnreal, MeasureTheory.Measure.integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport, ediam_smul_le, MeasureTheory.addEquivAddHaarChar_smul_preimage, instSMulPosMonoNNReal, MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul, MeasureTheory.Measure.smul_measure_isAddInvariant_le_of_isCompact_closure, MeasureTheory.Measure.measure_preimage_isAddLeftInvariant_eq_smul_of_hasCompactSupport, MeasureTheory.lpNorm_smul_measure_of_ne_zero, ProbabilityTheory.setBernoulli_apply', MeasureTheory.FiniteMeasure.self_eq_mass_smul_normalize, MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul', infEDist_smul₀, MeasureTheory.mulEquivHaarChar_smul_map, MeasureTheory.FiniteMeasure.map_fst_prod, MeasureTheory.Measure.hausdorffMeasure_smul₀, MeasureTheory.SMul.sigmaFinite, MeasureTheory.Measure.isMulLeftInvariant_eq_smul_of_innerRegular, MeasureTheory.Measure.rnDeriv_smul_left', MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul', MeasureTheory.Measure.isMulLeftInvariant_eq_smul_of_regular, MeasureTheory.Measure.toSignedMeasure_smul, MeasureTheory.hausdorffMeasure_lineMap_image, infEdist_smul₀, MeasureTheory.FiniteMeasure.instContinuousSMulNNReal, MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul, MeasureTheory.Measure.measure_isAddHaarMeasure_eq_smul_of_isOpen, MeasureTheory.Measure.instSMulCommClassDomMulActNNReal, MeasureTheory.Measure.measure_isMulInvariant_eq_smul_of_isCompact_closure, nnreal_smul_lt_top_iff, MeasureTheory.smul_le_stoppedValue_hitting, MeasureTheory.Measure.isMulInvariant_eq_smul_of_compactSpace, MeasureTheory.Measure.exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport, MeasureTheory.JordanDecomposition.smul_posPart, edist_smul₀, MeasureTheory.Measure.measure_isAddInvariant_eq_smul_of_isCompact_closure, MeasureTheory.FiniteMeasure.smul_testAgainstNN_apply, MeasureTheory.Measure.measure_isHaarMeasure_eq_smul_of_isEverywherePos, MeasureTheory.Measure.nnreal_smul_coe_apply, MeasureTheory.Measure.addHaarScalarFactor_smul_smul, MeasureTheory.JordanDecomposition.real_smul_posPart_nonneg, MeasureTheory.hausdorffMeasure_homothety_image, MeasureTheory.Measure.smul_measure_isMulInvariant_le_of_isCompact_closure, MeasureTheory.FiniteMeasure.toMeasure_normalize_eq_of_nonzero, MeasureTheory.Measure.measure_isAddHaarMeasure_eq_smul_of_isEverywherePos, MeasureTheory.IsFiniteMeasureOnCompacts.smul_nnreal, MeasureTheory.Measure.measure_isMulInvariant_eq_smul_of_isCompact_closure_of_measurableSet, MeasureTheory.FiniteMeasure.normalize_eq_inv_mass_smul_of_nonzero, MeasureTheory.Measure.instSMulCommClassNNRealDomMulAct, MeasureTheory.Measure.map_right_mul_eq_modularCharacterFun_smul, MeasureTheory.addEquivAddHaarChar_smul_map, MeasureTheory.isMulLeftInvariant_smul_nnreal, MeasureTheory.instIsProbabilityMeasureHAddMeasureHSMulNNRealToNNRealSymm, MeasureTheory.hausdorffMeasure_smul_right_image, MeasureTheory.Measure.measure_isAddLeftInvariant_eq_vadd_of_ne_top, MeasureTheory.Measure.mul_addHaarScalarFactor_smul, MeasureTheory.Measure.integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport, NNReal.instMeasurableSMul₂ENNReal, MeasureTheory.Measure.isMulLeftInvariant_eq_smul, MeasureTheory.VAddInvariantMeasure.vadd_nnreal, MeasureTheory.Measure.InnerRegular.smul_nnreal, MeasureTheory.JordanDecomposition.smul_negPart, MeasureTheory.isAddRightInvariant_smul_nnreal, MeasureTheory.SMulInvariantMeasure.smul_nnreal, MeasureTheory.mulEquivHaarChar_smul_preimage, MeasureTheory.Measure.measure_preimage_isMulLeftInvariant_eq_smul_of_hasCompactSupport, MeasureTheory.JordanDecomposition.real_smul_posPart_neg, MeasureTheory.Measure.isAddLeftInvariant_eq_smul_of_regular, ediam_smul₀, MeasureTheory.FiniteMeasure.map_smul, MeasureTheory.addEquivAddHaarChar_smul_eq_comap, MeasureTheory.mulEquivHaarChar_smul_eq_comap, MeasureTheory.Measure.isAddLeftInvariant_eq_smul_of_innerRegular, MeasureTheory.JordanDecomposition.real_smul_negPart_neg, AlternatingMap.measure_def, MeasureTheory.maximal_ineq, MeasureTheory.Measure.haarScalarFactor_smul_smul, MeasureTheory.Measure.rnDeriv_smul_left, MeasureTheory.Measure.exists_integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport, smul_toNNReal, StieltjesFunction.measure_smul, MeasureTheory.Measure.Regular.smul_nnreal, MeasureTheory.isLocallyFiniteMeasureSMulNNReal, MeasureTheory.isFiniteMeasureSMulNNReal, MeasureTheory.Integrable.smul_measure_nnreal, MeasureTheory.Measure.measure_isAddInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop, MeasureTheory.Measure.InnerRegularCompactLTTop.smul_nnreal, MeasureTheory.Measure.IsEverywherePos.smul_measure_nnreal, MeasureTheory.Measure.haveLebesgueDecompositionSMulRight, MeasureTheory.Measure.IsAddHaarMeasure.nnreal_smul, MeasureTheory.Measure.mul_haarScalarFactor_smul, MeasureTheory.Measure.measure_isAddInvariant_eq_smul_of_isCompact_closure_of_measurableSet, MeasureTheory.lpNorm_smul_measure_of_ne_top, MeasureTheory.JordanDecomposition.real_smul_negPart_nonneg, MeasureTheory.isMulRightInvariant_smul_nnreal, MeasureTheory.isAddLeftInvariant_smul_nnreal, MeasureTheory.Measure.map_right_add_eq_addModularCharacterFun_vadd, MeasureTheory.hausdorffMeasure_homothety_preimage, MeasureTheory.FiniteMeasure.map_snd_prod, instMeasurableSMulNNReal, MeasureTheory.eLpNorm_smul_measure_of_ne_zero', MeasureTheory.OuterMeasure.mkMetric_nnreal_smul, MeasureTheory.Measure.singularPart_smul_right, instPosSMulStrictMonoNNReal, toReal_smul, MeasureTheory.Measure.isAddLeftInvariant_eq_smul, ProbabilityTheory.setBernoulli_apply, edist_smul_le, MeasureTheory.Measure.addHaarScalarFactor_smul, MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul, MeasureTheory.Measure.singularPart_smul, MeasureTheory.Measure.measure_isMulInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop, MeasureTheory.measureReal_nnreal_smul_apply, ProbabilityTheory.setBernoulli_eq_map, MeasureTheory.Measure.measure_isHaarMeasure_eq_smul_of_isOpen
instDistribMulActionNNReal 📖	CompOp	—
instModuleNNReal 📖	CompOp	—
instMulActionNNReal 📖	CompOp	11 math math: smul_def, MeasureTheory.FiniteMeasure.self_eq_mass_smul_normalize, instIsScalarTowerNNReal, MeasureTheory.FiniteMeasure.map_fst_prod, MeasureTheory.FiniteMeasure.instContinuousSMulNNReal, MeasureTheory.FiniteMeasure.smul_testAgainstNN_apply, smulCommClass_left, MeasureTheory.FiniteMeasure.normalize_eq_inv_mass_smul_of_nonzero, MeasureTheory.FiniteMeasure.map_smul, MeasureTheory.FiniteMeasure.map_snd_prod, smulCommClass_right

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_smul 📖	mathematical	—	ofNNReal NNReal ENNReal	—	smul_one_smul smul_def smul_eq_mul coe_mul smul_mul_assoc one_mul
instIsScalarTowerNNReal 📖	mathematical	—	IsScalarTower NNReal SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiringNNReal MulAction.toSemigroupAction instMulActionNNReal	—	smul_assoc
instPosSMulStrictMonoNNReal 📖	mathematical	—	PosSMulStrictMono NNReal ENNReal Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring instCommSemiring instAlgebraNNReal Algebra.id PartialOrder.toPreorder instPartialOrderNNReal instPartialOrder instZeroNNReal	—	mul_lt_mul_right LT.lt.ne' coe_pos coe_ne_top
instSMulPosMonoNNReal 📖	mathematical	—	SMulPosMono NNReal ENNReal Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring instCommSemiring instAlgebraNNReal Algebra.id PartialOrder.toPreorder instPartialOrderNNReal instPartialOrder instZeroENNReal	—	mul_le_mul_left covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono instIsOrderedMonoid coe_le_coe
nnreal_smul_lt_top 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder instPartialOrder Top.top instTopENNReal	NNReal Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring instCommSemiring instAlgebraNNReal Algebra.id	—	mul_lt_top
nnreal_smul_lt_top_iff 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder instPartialOrder NNReal Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring instCommSemiring instAlgebraNNReal Algebra.id Top.top instTopENNReal	—	lt_top_iff_ne_top nnreal_smul_ne_top_iff
nnreal_smul_ne_top 📖	—	—	—	—	mul_ne_top
nnreal_smul_ne_top_iff 📖	—	—	—	—	smul_top IsStrictOrderedRing.isDomain NNReal.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE NNReal.instCanonicallyOrderedAdd IsScalarTower.right DivisionSemiring.to_moduleIsTorsionFree nnreal_smul_ne_top
smulCommClass_left 📖	mathematical	—	SMulCommClass NNReal SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiringNNReal MulAction.toSemigroupAction instMulActionNNReal	—	SMulCommClass.smul_comm
smulCommClass_right 📖	mathematical	—	SMulCommClass NNReal SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiringNNReal MulAction.toSemigroupAction instMulActionNNReal	—	SMulCommClass.smul_comm
smul_def 📖	mathematical	—	NNReal SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiringNNReal MulAction.toSemigroupAction instMulActionNNReal ENNReal CommSemiring.toSemiring instCommSemiring ofNNReal	—	—
smul_toNNReal 📖	mathematical	—	toNNReal NNReal ENNReal Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring instCommSemiring instAlgebraNNReal Algebra.id Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	toNNReal_mul
smul_top 📖	mathematical	—	ENNReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instAddCommMonoid Top.top instTopENNReal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instZeroENNReal	—	smul_one_mul mul_top' IsDomain.toIsCancelMulZero one_ne_zero NeZero.charZero_one instCharZero
toReal_smul 📖	mathematical	—	toReal NNReal ENNReal Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring instCommSemiring instAlgebraNNReal Algebra.id Real Real.semiring NNReal.instAlgebraOfReal Real.instCommSemiring	—	smul_def smul_eq_mul toReal_mul coe_toReal

---

← Back to Index