This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
Approximation tactic #14781
Labels
feature-request
This issue is a feature request, either for mathematics, tactics, or CI
I don't know anything about the implementation of
norm_num
, but in my ideal world, these lemmas would entirely be handled bynorm_num
.Originally posted by @Smaug123 in #8002 (comment)
There are a few lemmas in the Bertrand's postulate proof that bound certain expressions using
sqrt
,log
,exp
. It would be nice ifsome tactic could handle these.norm_num
In particular, if we want to prove a goal of the form
e1 < e2
, wheree1
ande2
are compositions of continuous functions (or are at least continuous at their arguments) applied to rationals, then in principle, we can generate finer and finer approximations of both expressions until eventually we can prove the goal by the triangle inequality.The text was updated successfully, but these errors were encountered: