bound

📁 Source: MathlibTest/Bound/bound.lean

Statistics

Metric	Count
Definitions bound, bound, bound, bound	4
Theorems bound, bound, bound, bound, bound, bound, bound, bound, bound, bound, bound	11
Total	15

Asymptotics.IsBigO

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bound 📖	mathematical	Asymptotics.IsBigO	Filter.Eventually Real Real.instLE Norm.norm Real.instMul	—	Asymptotics.isBigO_iff

Asymptotics.IsBigOWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bound 📖	mathematical	Asymptotics.IsBigOWith	Filter.Eventually Real Real.instLE Norm.norm Real.instMul	—	Asymptotics.isBigOWith_iff

Asymptotics.IsLittleO

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bound 📖	mathematical	Asymptotics.IsLittleO Real Real.instLT Real.instZero	Filter.Eventually Real.instLE Norm.norm Real.instMul	—	Asymptotics.isLittleO_iff

Behrend

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bound 📖	mathematical	—	Real Real.instLT DivInvMonoid.toDiv Real.instDivInvMonoid Real.instPow Real.instNatCast Real.instInv nValue Real.exp Real.instOne dValue	—	div_lt_floor Nat.instAtLeastTwoHAddOfNat Real.log_le_log_iff div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing zero_lt_two Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add div_lt_one Real.exp_pos Real.exp_one_gt_two Real.rpow_pos_of_pos Nat.cast_pos' lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Real.log_rpow Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial LE.le.trans_lt' Mathlib.Meta.NormNum.isNat_lt_true Nat.instCharZero mul_comm div_eq_mul_inv nValue.eq_1 le_imp_le_of_le_of_le le_refl div_le_div₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.log_natCast_nonneg Nat.lt_ceil Nat.cast_zero Real.sqrt_pos Real.log_pos Nat.one_lt_cast le_of_lt ceil_lt_mul Real.le_sqrt_of_sq_le Real.rpow_natCast Real.log_le_log pow_pos IsStrictOrderedRing.toZeroLEOneClass Mathlib.Meta.NormNum.instAtLeastTwo le_trans div_le_iff₀' Mathlib.Meta.NormNum.isNat_natCast LE.le.trans' LT.lt.le Real.log_two_gt_d9 Mathlib.Meta.NormNum.isRat_le_true Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_pow Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true Mathlib.Meta.NormNum.isNNRat_ratCast Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_mkRat Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.raw_refl Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1 Mathlib.Meta.NormNum.isNat_intCast Mathlib.Meta.NormNum.isNat_intOfNat Rat.instCharZero div_div Real.div_sqrt le_div_iff₀ Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.IsNNRat.to_eq le_sqrt_log

ContinuousAlternatingMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bound 📖	mathematical	—	Real Real.instLT Real.instZero Real.instLE Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace funLike Real.instMul Finset.prod Real.instCommMonoid Finset.univ	—	ContinuousMultilinearMap.bound

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bound 📖	mathematical	—	Real Real.instLT Real.instZero Real.instLE Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule funLike Real.instMul	—	SemilinearMapClass.bound_of_continuous ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass cont

ContinuousLinearMap.NonlinearRightInverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bound 📖	mathematical	—	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm toFun Real.instMul NNReal.toReal nnnorm	—	bound'

ContinuousMultilinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bound 📖	mathematical	—	Real Real.instLT Real.instZero Real.instLE Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace funLike Real.instMul Finset.prod Real.instCommMonoid Finset.univ	—	MultilinearMap.exists_bound_of_continuous cont

EstimatorData

Definitions

Name	Category	Theorems
bound 📖	CompOp	6 math math: bound_def, Estimator.bound_le, Estimator.improveUntil_spec, Estimator.improveUntilAux_spec, Estimator.improve_spec, instWellFoundedGTElemRangeBound

IsBoundedBilinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bound 📖	mathematical	IsBoundedBilinearMap	Real Real.instLT Real.instZero Real.instLE Norm.norm SeminormedAddCommGroup.toNorm Real.instMul	—	—

IsBoundedLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bound 📖	mathematical	IsBoundedLinearMap	Real Real.instLT Real.instZero Real.instLE Norm.norm SeminormedAddCommGroup.toNorm Real.instMul	—	—

NormedAddGroupHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bound 📖	mathematical	—	Real Real.instLT Real.instZero Real.instLE Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe NormedAddGroupHom funLike Real.instMul	—	bound' exists_pos_bound_of_bound

ProbabilityTheory.IsFiniteKernel

Definitions

Name	Category	Theorems
bound 📖	CompOp	—

ProbabilityTheory.Kernel

Definitions

Name	Category	Theorems
bound 📖	CompOp	17 math math: bound_le_one, ProbabilityTheory.avgRisk_le_mul', ProbabilityTheory.IsMarkovKernel.bound_eq_one, bound_eq_one, ProbabilityTheory.IsFiniteKernel.bound_lt_top, bound_eq_zero_of_isEmpty, ProbabilityTheory.bayesRisk_le_mul', ProbabilityTheory.IsFiniteKernel.bound_eq_zero_of_isEmpty, bound_lt_top, compProd_apply_univ_le, bound_zero, ProbabilityTheory.IsZeroOrMarkovKernel.bound_le_one, ProbabilityTheory.IsFiniteKernel.bound_zero, measure_le_bound, comp_apply_univ_le, ProbabilityTheory.IsFiniteKernel.bound_eq_zero_of_isEmpty', bound_eq_zero_of_isEmpty'

SzemerediRegularity

Definitions

Name	Category	Theorems
bound 📖	CompOp	5 math math: initialBound_le_bound, bound_pos, szemeredi_regularity, SimpleGraph.triangleRemovalBound_le, le_bound

---

← Back to Index