Documentation Verification Report

Expect

📁 Source: Mathlib/Algebra/Order/BigOperators/Expect.lean

Statistics

Metric	Count
Definitions `evalFinsetExpect`	1
Theorems `abs_expect_le`, `exists_lt_of_expect_lt`, `exists_lt_of_lt_expect`, `expect_eq_zero_iff_of_nonneg`, `expect_eq_zero_iff_of_nonpos`, `expect_le`, `expect_le_expect`, `expect_mul_sq_le_sq_mul_sq`, `expect_nonneg`, `expect_pos`, `le_expect`, `le_expect_nonempty_of_subadditive`, `le_expect_nonempty_of_subadditive_on_pred`, `le_expect_of_subadditive`, `le_expect_of_subadditive_on_pred`, `expect_eq_zero_iff_of_nonneg`, `expect_eq_zero_iff_of_nonpos`	17
Total	18

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_expect_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `abs` `AddCommGroup.toAddGroup` `expect` `AddCommGroup.toAddCommMonoid`	—	`le_expect_of_subadditive` `abs_zero` `IsOrderedAddMonoid.toAddLeftMono` `abs_add_le` `abs_nnqsmul`
`exists_lt_of_expect_lt` 📖	mathematical	`Nonempty` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `expect`	`Finset` `instMembership`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_and_eq` `le_expect`
`exists_lt_of_lt_expect` 📖	mathematical	`Nonempty` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `expect`	`Finset` `instMembership`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_and_eq` `expect_le`
`expect_eq_zero_iff_of_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`expect`	—	`sum_congr` `DivisionSemiring.to_moduleIsTorsionFree` `IsDomain.toIsCancelMulZero` `IsStrictOrderedRing.isDomain` `instIsStrictOrderedRingNNRat` `CanonicallyOrderedAdd.toExistsAddOfLE` `NNRat.instCanonicallyOrderedAdd` `NNRat.instCharZero` `sum_eq_zero_iff_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `instIsEmptyFalse`
`expect_eq_zero_iff_of_nonpos` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`expect`	—	`sum_congr` `DivisionSemiring.to_moduleIsTorsionFree` `IsDomain.toIsCancelMulZero` `IsStrictOrderedRing.isDomain` `instIsStrictOrderedRingNNRat` `CanonicallyOrderedAdd.toExistsAddOfLE` `NNRat.instCanonicallyOrderedAdd` `NNRat.instCharZero` `sum_eq_zero_iff_of_nonpos` `IsOrderedAddMonoid.toAddLeftMono` `instIsEmptyFalse`
`expect_le` 📖	mathematical	`Nonempty` `Preorder.toLE` `PartialOrder.toPreorder`	`expect`	—	`inv_smul_le_iff_of_pos` `PosSMulMono.toPosSMulReflectLE` `instIsStrictOrderedRingNNRat` `Nat.cast_zero` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `NNRat.instCharZero` `Nonempty.card_pos` `Nat.cast_smul_eq_nsmul` `sum_le_card_nsmul`
`expect_le_expect` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`expect`	—	`smul_le_smul_of_nonneg_left` `sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `zero_le` `NNRat.instCanonicallyOrderedAdd`
`expect_mul_sq_le_sq_mul_sq` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `expect` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`sum_congr` `smul_pow` `IsScalarTower.nnrat` `SMulCommClass.nnrat` `inv_pow` `smul_mul_smul_comm` `smul_le_smul_of_nonneg_left` `sum_mul_sq_le_sq_mul_sq` `zero_le` `NNRat.instCanonicallyOrderedAdd`
`expect_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`expect`	—	`smul_nonneg` `zero_le` `NNRat.instCanonicallyOrderedAdd` `sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono`
`expect_pos` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nonempty`	`expect`	—	`smul_pos` `inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Nat.cast_zero` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRingNNRat` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `NNRat.instCharZero` `Nonempty.card_pos` `sum_pos`
`le_expect` 📖	mathematical	`Nonempty` `Preorder.toLE` `PartialOrder.toPreorder`	`expect`	—	`le_inv_smul_iff_of_pos` `PosSMulMono.toPosSMulReflectLE` `instIsStrictOrderedRingNNRat` `Nat.cast_zero` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `NNRat.instCharZero` `Nonempty.card_pos` `Nat.cast_smul_eq_nsmul` `card_nsmul_le_sum`
`le_expect_nonempty_of_subadditive` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `NNRat` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `NNRat.instSemifield` `Module.toDistribMulAction` `NNRat.instInv` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Nonempty`	`expect`	—	`le_expect_nonempty_of_subadditive_on_pred`
`le_expect_nonempty_of_subadditive_on_pred` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `NNRat` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `NNRat.instSemifield` `Module.toDistribMulAction` `NNRat.instInv` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Nonempty`	`expect`	—	`sum_congr` `sum_induction_nonempty` `smul_le_smul_of_nonneg_left` `le_sum_nonempty_of_subadditive_on_pred` `zero_le` `NNRat.instCanonicallyOrderedAdd`
`le_expect_of_subadditive` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `NNRat` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `NNRat.instSemifield` `Module.toDistribMulAction` `NNRat.instInv` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	`expect`	—	`le_expect_of_subadditive_on_pred`
`le_expect_of_subadditive_on_pred` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `NNRat` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `NNRat.instSemifield` `Module.toDistribMulAction` `NNRat.instInv` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	`expect`	—	`eq_empty_or_nonempty` `expect_empty` `le_expect_nonempty_of_subadditive_on_pred`

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`expect_eq_zero_iff_of_nonneg` 📖	mathematical	`Pi.hasLe` `Preorder.toLE` `PartialOrder.toPreorder` `Pi.instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`Finset.expect` `Finset.univ`	—	`Finset.expect_eq_zero_iff_of_nonneg`
`expect_eq_zero_iff_of_nonpos` 📖	mathematical	`Pi.hasLe` `Preorder.toLE` `PartialOrder.toPreorder` `Pi.instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`Finset.expect` `Finset.univ`	—	`Finset.expect_eq_zero_iff_of_nonpos`

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`evalFinsetExpect` 📖	CompOp	—

---

← Back to Index