OAI/Probability/SATComputability/WeightedExpressions.lean
13 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.FixedClauseThreshold.Computability.FiniteArithmetic.rational_abs_le_numline 11 - def
OAI.FixedClauseThreshold.Computability.FiniteArithmetic.expressionBoundline 23 - theorem
OAI.FixedClauseThreshold.Computability.FiniteArithmetic.expressionBound_computableline 28 - theorem
OAI.FixedClauseThreshold.Computability.FiniteArithmetic.expressionBound_validline 37 - def
OAI.FixedClauseThreshold.Computability.FiniteArithmetic.mixtureBoundline 53 - def
OAI.FixedClauseThreshold.Computability.FiniteArithmetic.mixtureExpressionline 56 - def
OAI.FixedClauseThreshold.Computability.FiniteArithmetic.logMixtureExpressionline 59 - theorem
OAI.FixedClauseThreshold.Computability.FiniteArithmetic.mixtureBound_computableline 62 - theorem
OAI.FixedClauseThreshold.Computability.FiniteArithmetic.mixtureExpression_computableline 69 - theorem
OAI.FixedClauseThreshold.Computability.FiniteArithmetic.logMixtureExpression_computableline 77 - theorem
OAI.FixedClauseThreshold.Computability.FiniteArithmetic.mixtureExpression_valueline 81 - theorem
OAI.FixedClauseThreshold.Computability.FiniteArithmetic.small_exp_lowerline 87 - theorem
OAI.FixedClauseThreshold.Computability.FiniteArithmetic.logMixtureExpression_valueline 94