Documentation Verification Report

ConvexSpace

📁 Source: Mathlib/LinearAlgebra/ConvexSpace.lean

Statistics

Metric	Count
Definitions `ConvexSpace`, `convexCombination`, `duple`, `join`, `map`, `single`, `weights`, `convexComboPair`	8
Theorems `assoc`, `single`, `ext`, `ext_iff`, `map_comp`, `map_const`, `map_duple`, `map_id`, `map_map`, `map_single`, `mk_single`, `nonempty`, `nonneg`, `single_weights`, `total`, `convexComboPair_one`, `convexComboPair_same`, `convexComboPair_symm`, `convexComboPair_zero`	19
Total	27

ConvexSpace

Definitions

Name	Category	Theorems
`convexCombination` 📖	CompOp	9 math math: `ofConvex.coe_convexCombination`, `IsConvexMetricSpace.dist_convexCombination_map_le'`, `single`, `dist_convexCombination_map_le`, `AddTorsor.convexCombination_eq_affineCombination`, `dist_convexCombination_left_le`, `convexCombination_eq_sum`, `assoc`, `dist_convexCombination_right_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`assoc` 📖	mathematical	—	`convexCombination` `StdSimplex.map` `StdSimplex` `Preorder.toLE` `PartialOrder.toPreorder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `StdSimplex.join`	—	—
`single` 📖	mathematical	—	`convexCombination` `StdSimplex.single`	—	—

StdSimplex

Definitions

Name	Category	Theorems
`duple` 📖	CompOp	1 math math: `map_duple`
`join` 📖	CompOp	2 math math: `AddTorsor.convexCombination_assoc`, `ConvexSpace.assoc`
`map` 📖	CompOp	11 math math: `map_single`, `ConvexSpace.ofConvex.coe_convexCombination`, `map_duple`, `IsConvexMetricSpace.dist_convexCombination_map_le'`, `AddTorsor.convexCombination_assoc`, `dist_convexCombination_map_le`, `ConvexSpace.assoc`, `map_map`, `map_comp`, `map_id`, `map_const`
`single` 📖	CompOp	6 math math: `map_single`, `mk_single`, `ConvexSpace.single`, `single_weights`, `AddTorsor.convexCombination_single`, `map_const`
`weights` 📖	CompOp	10 math math: `ext_iff`, `IsConvexMetricSpace.dist_convexCombination_map_le'`, `nonneg`, `dist_convexCombination_map_le`, `AddTorsor.convexCombination_eq_affineCombination`, `single_weights`, `dist_convexCombination_left_le`, `total`, `convexCombination_eq_sum`, `dist_convexCombination_right_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`weights` `Preorder.toLE` `PartialOrder.toPreorder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—	—
`ext_iff` 📖	mathematical	—	`weights` `Preorder.toLE` `PartialOrder.toPreorder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`ext`
`map_comp` 📖	mathematical	—	`map`	—	`ext` `Finsupp.ext` `Finsupp.mapDomain_comp`
`map_const` 📖	mathematical	—	`map` `single`	—	`ext` `Finsupp.ext` `total` `Finsupp.sum_fun_zero` `Finsupp.sum_apply` `Finsupp.single_apply`
`map_duple` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`map` `duple`	—	`ext` `Finsupp.ext` `Finsupp.mapDomain_add` `Finsupp.mapDomain_single`
`map_id` 📖	mathematical	—	`map`	—	`ext` `Finsupp.ext` `Finsupp.mapDomain_id`
`map_map` 📖	mathematical	—	`map`	—	`map_comp`
`map_single` 📖	mathematical	—	`map` `single`	—	`ext` `Finsupp.ext` `Finsupp.mapDomain_single`
`mk_single` 📖	mathematical	`Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instLE` `Preorder.toLE` `PartialOrder.toPreorder` `Finsupp.instZero` `Finsupp.single` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Finsupp.sum`	`Preorder.toLE` `PartialOrder.toPreorder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Finsupp.single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `single`	—	—
`nonempty` 📖	—	—	—	—	`Finsupp.instSubsingleton` `NeZero.one` `total`
`nonneg` 📖	mathematical	—	`Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instLE` `Finsupp.instZero` `weights`	—	—
`single_weights` 📖	mathematical	—	`weights` `Preorder.toLE` `PartialOrder.toPreorder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `single` `Finsupp.single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`total` 📖	mathematical	—	`Finsupp.sum` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `weights`	—	—

(root)

Definitions

Name	Category	Theorems
`ConvexSpace` 📖	CompData	3 math math: `ConvexSpace.ofConvex.coe_convexCombination`, `AddTorsor.convexCombination_eq_affineCombination`, `convexCombination_eq_sum`
`convexComboPair` 📖	CompOp	14 math math: `dist_convexComboPair_convexComboPair_le`, `convexComboPair_one`, `continuous_convexComboPair_of_isBounded`, `dist_convexComboPair_left`, `continuous_convexComboPair'`, `dist_convexComboPair_convexComboPair`, `dist_convexComboPair_right`, `convexComboPair_same`, `dist_right_convexComboPair`, `dist_left_convexComboPair`, `convexComboPair_symm`, `continuous_convexComboPair`, `convexComboPair_zero`, `AddTorsor.convexComboPair_eq_lineMap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`convexComboPair_one` 📖	mathematical	—	`convexComboPair` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`Finsupp.single_zero` `add_zero` `ConvexSpace.single`
`convexComboPair_same` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`convexComboPair`	—	`ConvexSpace.single`
`convexComboPair_symm` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`convexComboPair` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `add_comm`	—	`add_comm` `StdSimplex.ext`
`convexComboPair_zero` 📖	mathematical	—	`convexComboPair` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Finsupp.single_zero` `zero_add` `ConvexSpace.single`

---

← Back to Index