Documentation Verification Report

Estimator

📁 Source: Mathlib/Deprecated/Estimator.lean

Statistics

Metric	Count
Definitions `Estimator`, `fst`, `inner`, `fstInst`, `improveUntil`, `improveUntilAux`, `toEstimatorData`, `trivial`, `EstimatorData`, `improve`, `instBotTrivial`, `instEstimatorDataFstProdOfDecidableLTOfWellFoundedGTSubtypeProdLe`, `instEstimatorDataHAddThunkProd`, `instEstimatorNatHAddThunkProd`, `instEstimatorPureTrivial`	15
Theorems `bound_le`, `improveUntilAux_spec`, `improveUntil_spec`, `improve_spec`, `bound_def`, `improve_def`, `instWellFoundedGTElemRangeBound`, `instWellFoundedGTTrivial`, `instWellFoundedGTUnit`	9
Total	24

Estimator

Definitions

Name	Category	Theorems
`fst` 📖	CompData	—
`fstInst` 📖	CompOp	—
`improveUntil` 📖	CompOp	1 math math: `improveUntil_spec`
`improveUntilAux` 📖	CompOp	1 math math: `improveUntilAux_spec`
`toEstimatorData` 📖	CompOp	5 math math: `bound_le`, `improveUntil_spec`, `improveUntilAux_spec`, `improve_spec`, `instWellFoundedGTElemRangeBound`
`trivial` 📖	CompOp	1 math math: `instWellFoundedGTTrivial`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bound_le` 📖	mathematical	—	`Preorder.toLE` `EstimatorData.bound` `toEstimatorData`	—	—
`improveUntilAux_spec` 📖	mathematical	—	`improveUntilAux` `EstimatorData.bound` `toEstimatorData`	—	—
`improveUntil_spec` 📖	mathematical	—	`improveUntil` `EstimatorData.bound` `toEstimatorData`	—	`improveUntilAux_spec`
`improve_spec` 📖	mathematical	—	`EstimatorData.improve` `toEstimatorData` `EstimatorData.bound` `Preorder.toLT`	—	—

Estimator.fst

Definitions

Name	Category	Theorems
`inner` 📖	CompOp	—

EstimatorData

Definitions

Name	Category	Theorems
`improve` 📖	CompOp	2 math math: `improve_def`, `Estimator.improve_spec`

(root)

Definitions

Name	Category	Theorems
`Estimator` 📖	CompData	—
`EstimatorData` 📖	CompData	—
`instBotTrivial` 📖	CompOp	—
`instEstimatorDataFstProdOfDecidableLTOfWellFoundedGTSubtypeProdLe` 📖	CompOp	—
`instEstimatorDataHAddThunkProd` 📖	CompOp	2 math math: `bound_def`, `improve_def`
`instEstimatorNatHAddThunkProd` 📖	CompOp	—
`instEstimatorPureTrivial` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bound_def` 📖	mathematical	—	`EstimatorData.bound` `Thunk.instAdd_mathlib` `instEstimatorDataHAddThunkProd`	—	—
`improve_def` 📖	mathematical	—	`EstimatorData.improve` `Thunk.instAdd_mathlib` `instEstimatorDataHAddThunkProd`	—	—
`instWellFoundedGTElemRangeBound` 📖	mathematical	`WellFoundedGT` `Preorder.toLE` `PartialOrder.toPreorder` `Preorder.toLT`	`Set.Elem` `Set.range` `EstimatorData.bound` `Estimator.toEstimatorData` `Set` `Set.instMembership`	—	`Estimator.bound_le` `OrderEmbedding.wellFoundedGT`
`instWellFoundedGTTrivial` 📖	mathematical	—	`WellFoundedGT` `Estimator.trivial` `Preorder.toLT`	—	`instReflLe` `OrderEmbedding.wellFoundedGT` `instWellFoundedGTUnit`
`instWellFoundedGTUnit` 📖	mathematical	—	`WellFoundedGT` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `PUnit.instBiheytingAlgebra`	—	—

---

← Back to Index