Documentation Verification Report

PositiveLinearMap

📁 Source: Mathlib/Analysis/CStarAlgebra/PositiveLinearMap.lean

Statistics

Metric	Count
Definitions `PositiveLinearMap`	1
Theorems `apply_le_of_isSelfAdjoint`, `exists_norm_apply_le`, `instContinuousLinearMapClassComplexOfLinearMapClassOfOrderHomClass`, `instStarHomClassOfLinearMapClassComplexOfOrderHomClass`, `norm_apply_le_of_nonneg`, `map_isSelfAdjoint`	6
Total	7

PositiveLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_le_of_isSelfAdjoint` 📖	mathematical	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `CStarAlgebra.toNormedRing` `StarRing.toStarAddMonoid` `CStarAlgebra.toStarRing`	`Preorder.toLE` `PartialOrder.toPreorder` `DFunLike.coe` `PositiveLinearMap` `Complex` `Complex.instSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `CStarAlgebra.toNonUnitalCStarAlgebra` `NormedSpace.toModule` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNormedSpace` `instFunLike` `RingHom` `Real` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Real.instCommSemiring` `Ring.toSemiring` `RingHom.instFunLike` `algebraMap` `NormedAlgebra.toAlgebra` `Real.normedField` `NormedAlgebra.complexToReal` `CStarAlgebra.toNormedAlgebra` `Norm.norm` `NormedRing.toNorm`	—	`OrderHomClass.mono` `instOrderHomClass` `IsSelfAdjoint.le_algebraMap_norm_self`
`exists_norm_apply_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `NonUnitalNormedRing.toNorm` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `DFunLike.coe` `PositiveLinearMap` `Complex` `Complex.instSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalCStarAlgebra.toNormedSpace` `instFunLike` `Real.instMul` `NNReal.toReal`	—	`Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Push.not_forall_eq` `eq_zero_or_norm_pos` `norm_zero` `MulZeroClass.mul_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `instLinearMapClass` `smul_nonneg` `IsOrderedModule.toPosSMulMono` `instIsOrderedModule` `Real.instStarOrderedRing` `StarModule.complexToReal` `NonUnitalCStarAlgebra.toStarModule` `IsScalarTower.complexToReal` `NonUnitalCStarAlgebra.toIsScalarTower` `SMulCommClass.complexToReal` `NonUnitalCStarAlgebra.toSMulCommClass` `le_of_lt` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `norm_smul` `NormedSpace.toNormSMulClass` `norm_inv` `norm_norm` `inv_mul_cancel₀` `LT.lt.ne'` `map_smul_of_tower` `LinearMap.IsScalarTower.compatibleSMul` `IsScalarTower.left` `lt_inv_mul_iff₀'` `Summable.of_norm` `NonUnitalCStarAlgebra.toCompleteSpace` `Mathlib.Meta.NormNum.isNNRat_lt_true` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_one` `zpow_neg` `zpow_natCast` `norm_pow` `NormedDivisionRing.to_normOneClass` `NormedDivisionRing.toNormMulClass` `Real.norm_ofNat` `mul_one` `Filter.Eventually.exists` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.Tendsto.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `tendsto_pow_atTop_atTop_of_one_lt` `StarOrderedRing.toExistsAddOfLE` `Real.instArchimedean` `one_lt_two` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `LT.lt.not_ge` `LT.lt.le` `le_inv_mul_iff₀` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `Mathlib.Meta.Positivity.pos_of_isNat` `sq` `pow_mul'` `zpow_pos` `CStarAlgebra.norm_le_norm_of_nonneg_of_le` `map_nonneg` `OrderHomClass.mono` `instOrderHomClass` `Summable.le_tsum` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `StarOrderedRing.toIsOrderedAddMonoid` `CStarAlgebra.instOrderClosedTopology` `SummationFilter.instNeBotUnconditional` `SummationFilter.instLeAtTopUnconditional` `CStarAlgebra.exists_sum_four_nonneg` `map_sum` `Finset.sum_congr` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LE.le.trans` `norm_sum_le` `Complex.norm_I` `one_pow` `one_mul` `Finset.sum_le_sum` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `NNReal.coe_nonneg` `Finset.sum_const` `Fintype.card_fin` `nsmul_eq_mul` `mul_assoc`
`instContinuousLinearMapClassComplexOfLinearMapClassOfOrderHomClass` 📖	mathematical	—	`ContinuousLinearMapClass` `Complex` `Complex.instSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalCStarAlgebra.toNormedSpace`	—	`exists_norm_apply_le` `ContinuousLinearMap.continuous`
`instStarHomClassOfLinearMapClassComplexOfOrderHomClass` 📖	mathematical	—	`StarHomClass` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `StarRing.toStarAddMonoid` `NonUnitalCStarAlgebra.toStarRing`	—	`CStarAlgebra.exists_sum_four_nonneg` `IsSelfAdjoint.star_eq` `LE.le.isSelfAdjoint` `map_nonneg` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `star_sum` `Finset.sum_congr` `StarModule.star_smul` `NonUnitalCStarAlgebra.toStarModule` `star_pow` `Complex.conj_I` `map_sum` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass`
`norm_apply_le_of_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `CStarAlgebra.toNormedRing`	`Real` `Real.instLE` `Norm.norm` `NormedRing.toNorm` `DFunLike.coe` `PositiveLinearMap` `Complex` `Complex.instSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `CStarAlgebra.toNonUnitalCStarAlgebra` `NormedSpace.toModule` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNormedSpace` `instFunLike` `Real.instMul` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`norm_norm` `mul_comm` `norm_smul` `NormedSpace.toNormSMulClass` `CStarAlgebra.norm_le_norm_of_nonneg_of_le` `map_nonneg` `Complex.coe_smul` `LinearMapClass.map_smul` `instLinearMapClass` `OrderHomClass.mono` `instOrderHomClass` `Algebra.algebraMap_eq_smul_one` `IsSelfAdjoint.le_algebraMap_norm_self` `IsSelfAdjoint.of_nonneg`

(root)

Definitions

Name	Category	Theorems
`PositiveLinearMap` 📖	CompData	27 math math: `PositiveLinearMap.apply_le_of_isSelfAdjoint`, `PositiveLinearMap.coe_toLinearMap`, `PositiveLinearMap.nsmul_apply`, `PositiveLinearMap.preGNS_norm_def`, `PositiveLinearMap.map_nonneg`, `PositiveLinearMap.preGNS_inner_def`, `PositiveLinearMap.ext_iff`, `RealRMK.rieszMeasure_le_of_eq_one`, `RealRMK.integral_rieszMeasure`, `CompactlySupportedContinuousMap.toRealPositiveLinear_apply`, `PositiveLinearMap.exists_norm_apply_le`, `PositiveLinearMap.zero_apply`, `PositiveLinearMap.toLinearMap_injective`, `PositiveLinearMap.map_smul_of_tower`, `CompactlySupportedContinuousMap.toNNRealLinear_apply`, `PositiveLinearMap.add_apply`, `PositiveLinearMap.instLinearMapClass`, `PositiveLinearMap.instOrderHomClass`, `CompactlySupportedContinuousMap.eq_toRealPositiveLinear_toReal`, `PositiveLinearMap.norm_apply_le_of_nonneg`, `PositiveLinearMap.toLinearMap_zero`, `CompactlySupportedContinuousMap.integralPositiveLinearMap_toFun`, `RealRMK.le_rieszMeasure_tsupport_subset`, `PositiveLinearMap.toLinearMap_nsmul`, `PositiveLinearMap.preGNS_norm_sq`, `PositiveLinearMap.toLinearMap_add`, `map_isSelfAdjoint`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_isSelfAdjoint` 📖	mathematical	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `StarRing.toStarAddMonoid`	`DFunLike.coe` `PositiveLinearMap` `Complex` `Complex.instSemiring` `PositiveLinearMap.instFunLike`	—	`Real.instNontrivial` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `CFC.posPart_sub_negPart` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `PositiveLinearMap.instLinearMapClass` `IsSelfAdjoint.sub` `IsSelfAdjoint.of_nonneg` `PositiveLinearMap.map_nonneg` `CFC.posPart_nonneg` `CFC.negPart_nonneg`

---

← Back to Index