Documentation Verification Report

Bernstein

📁 Source: Mathlib/Analysis/SpecialFunctions/Bernstein.lean

Statistics

Metric	Count
Definitions `evalBernstein`, `bernstein`, `z`, `bernsteinApproximation`	4
Theorems `probability`, `variance`, `z_last`, `z_zero`, `apply`, `apply_one`, `apply_zero`, `bernsteinApproximation_uniform`, `bernstein_apply`, `bernstein_nonneg`	10
Total	14

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`evalBernstein` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`bernstein` 📖	CompOp	5 math math: `bernstein.variance`, `bernstein_apply`, `bernstein_nonneg`, `bernstein.probability`, `bernsteinApproximation.apply`
`bernsteinApproximation` 📖	CompOp	4 math math: `bernsteinApproximation.apply_zero`, `bernsteinApproximation.apply_one`, `bernsteinApproximation_uniform`, `bernsteinApproximation.apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bernsteinApproximation_uniform` 📖	mathematical	—	`Filter.Tendsto` `ContinuousMap` `Set.Elem` `Real` `unitInterval` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `bernsteinApproximation` `Filter.atTop` `Nat.instPreorder` `nhds` `ContinuousMap.compactOpen`	—	`isUniformAddGroup_of_addCommGroup` `Continuous.comp'` `continuous_gauge` `Continuous.sub` `IsTopologicalAddGroup.to_continuousSub` `ContinuousMapClass.map_continuous` `ContinuousMap.instContinuousMapClass` `Continuous.fst` `continuous_id'` `Continuous.snd` `IsCompact.bddAbove` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `isCompact_range` `instCompactSpaceProd` `compactSpace_Icc` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `instOrderTopologyReal` `le_trans` `Real.instIsOrderedRing` `gauge_nonneg` `Nat.instAtLeastTwoHAddOfNat` `CompactSpace.uniformContinuous_of_continuous` `Filter.HasBasis.uniformContinuous_iff` `Metric.uniformity_basis_dist` `Filter.HasBasis.uniformity_of_nhds_zero_swapped` `Filter.basis_sets` `Filter.Tendsto.eventually_lt_const` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Meta.NormNum.instAtLeastTwo` `tendsto_gauge_nhds_zero` `tendsto_const_div_atTop_nhds_zero_nat` `RCLike.charZero_rclike` `NNRat.instContinuousSMulOfIsScalarTowerOfRat` `IsScalarTower.nnrat` `Rat.instCharZero` `NNRat.instContinuousSMulRatReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Filter.mp_mem` `Filter.eventually_ne_atTop` `instNoTopOrderOfNoMaxOrder` `Nat.instNoMaxOrder` `half_pos` `one_pos` `Real.instZeroLEOneClass` `NeZero.charZero_one` `Filter.univ_mem'` `bernsteinApproximation.apply` `Finset.sum_congr` `smul_sub` `Finset.sum_sub_distrib` `bernstein.probability` `one_smul` `gauge_sum_le` `absorbent_nhds_zero` `gauge_smul_of_nonneg` `IsStrictOrderedRing.toIsStrictOrderedModule` `Set.isScalarTower` `IsScalarTower.left` `Finset.sum_add_sum_compl` `add_lt_add_of_le_of_lt` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `Finset.sum_le_sum` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `LT.lt.le` `bernstein_nonneg` `mul_comm` `Finset.sum_mul` `Finset.sum_le_sum_of_subset_of_nonneg` `Finset.subset_univ` `le_of_lt` `mul_one` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Finset.mul_sum` `one_mul` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `abs_of_pos` `dist_comm` `Finset.compl_filter` `Finset.filter.congr_simp` `mul_nonneg` `Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos` `Even.pow_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `AddGroup.existsAddOfLE` `even_two_mul` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `bernstein.variance` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `div_le_div_of_nonneg_right` `mul_le_mul` `unitInterval.le_one` `unitInterval.one_minus_le_one` `unitInterval.one_minus_nonneg` `Nat.cast_pos'` `lt_of_le_of_ne'` `zero_le` `Nat.instCanonicallyOrderedAdd` `add_halves` `CharZero.NeZero.two` `Filter.HasBasis.tendsto_right_iff` `nhds_basis_uniformity` `Filter.HasBasis.compactConvergenceUniformity_of_compact` `LocallyConvexSpace.convex_basis_zero` `gauge_lt_one_subset_self` `mem_of_mem_nhds`
`bernstein_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `Set.Elem` `Real` `unitInterval` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `bernstein` `Real.instMul` `Real.instNatCast` `Nat.choose` `Monoid.toNatPow` `Real.instMonoid` `Real.instSub` `Real.instOne`	—	`Polynomial.eval_mul` `Polynomial.eval_natCast` `Polynomial.eval_pow` `Polynomial.eval_X` `Polynomial.eval_sub` `Polynomial.eval_one`
`bernstein_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `DFunLike.coe` `ContinuousMap` `Set.Elem` `unitInterval` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `bernstein`	—	`bernstein_apply` `unitInterval.nonneg` `unitInterval.one_minus_nonneg` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass`

bernstein

Definitions

Name	Category	Theorems
`z` 📖	CompOp	4 math math: `variance`, `z_zero`, `z_last`, `bernsteinApproximation.apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`probability` 📖	mathematical	—	`Finset.sum` `Real` `Real.instAddCommMonoid` `Finset.univ` `Fin.fintype` `DFunLike.coe` `ContinuousMap` `Set.Elem` `unitInterval` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `bernstein` `Real.instOne`	—	`bernsteinPolynomial.sum` `Finset.sum_range` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Finset.sum_congr` `Polynomial.eval_one`
`variance` 📖	mathematical	—	`Finset.sum` `Real` `Real.instAddCommMonoid` `Finset.univ` `Fin.fintype` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Real.instSub` `Set` `Set.instMembership` `unitInterval` `z` `DFunLike.coe` `ContinuousMap` `Set.Elem` `instTopologicalSpaceSubtype` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `bernstein` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instNatCast`	—	`Finset.sum_congr` `bernstein_apply` `nsmul_eq_mul` `Finset.sum_range` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Polynomial.eval_mul` `Polynomial.eval_pow` `Polynomial.eval_sub` `Polynomial.eval_natCast` `Polynomial.eval_X` `Polynomial.eval_one` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.pow_eq_eval` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `ne_of_gt` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `lt_of_le_of_ne'` `zero_le` `Nat.instCanonicallyOrderedAdd` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq` `Mathlib.Tactic.FieldSimp.eq_div_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div'` `Mathlib.Tactic.FieldSimp.zpow'_ofNat` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Finset.sum_div` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `bernsteinPolynomial.variance`
`z_last` 📖	mathematical	—	`z` `Set.Elem` `Real` `unitInterval` `Set.Icc.instOne` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing`	—	`Real.instIsOrderedRing` `div_self` `RCLike.charZero_rclike`
`z_zero` 📖	mathematical	—	`z` `Set.Elem` `Real` `unitInterval` `Set.Icc.instZero` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing`	—	`Real.instIsOrderedRing` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `zero_div`

bernsteinApproximation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `Set.Elem` `Real` `unitInterval` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `bernsteinApproximation` `Finset.sum` `AddCommGroup.toAddCommMonoid` `Finset.univ` `Fin.fintype` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `bernstein` `bernstein.z`	—	`ContinuousMap.coe_sum` `Finset.sum_congr` `Finset.sum_apply`
`apply_one` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `Set.Elem` `Real` `unitInterval` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `bernsteinApproximation` `Set.Icc.instOne` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing`	—	`Real.instIsOrderedRing` `apply` `Finset.sum_congr` `bernstein_apply` `one_pow` `mul_one` `sub_self` `Fin.sum_univ_castSucc` `zero_pow` `MulZeroClass.mul_zero` `zero_smul` `Finset.sum_const_zero` `Nat.choose_self` `Nat.cast_one` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pow_zero` `bernstein.z_last` `one_smul` `zero_add`
`apply_zero` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `Set.Elem` `Real` `unitInterval` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `bernsteinApproximation` `Set.Icc.instZero` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing`	—	`Real.instIsOrderedRing` `apply` `Finset.sum_congr` `bernstein_apply` `sub_zero` `one_pow` `mul_one` `Fin.sum_univ_succ` `Nat.choose_zero_right` `Nat.cast_one` `pow_zero` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `zero_div` `one_smul` `Nat.cast_add` `zero_pow` `MulZeroClass.mul_zero` `zero_smul` `Finset.sum_const_zero` `add_zero`

---

← Back to Index