Numeric estimates for logarithms

Stream: mathlib4

[Michael Rothgang]

Formalising some analysis, I need to prove the following numeric calculation. Is there any way to make them less tedious?

Firstly, the basic one: perhaps this is really fodder for an approx tactic.

example : 68/100 < Real.log 2 := by
  rw [Real.lt_log_iff_exp_lt (by norm_num)]
  -- goal is now Real.exp 68/100 < 2; the LHS is about 1.97
  sorry

However, behold the tedium for the following

example : 3 * (4 : Real)⁻¹ ≤ 12 * Real.log 2 := by
  have : 68/100 < Real.log 2 := sorry -- previous sorry
  trans 12 * (68/100)
  · norm_num
  · gcongr

Is there a way to make this less tedious? For instance, a norm_num extension for logarithms? Can norm_num pick up facts in the local context (perhaps not)? Is there a better tactic?

[Kenny Lau]

@Michael Rothgang linarith solves the second example

[Kenny Lau]

as for the first example, I'm not saying this is the desired outcome, but I'm saying that if anyone is interested to write a tactic for exp, here is what you would use:

example : 68/100 < Real.log 2 := by
  rw [Real.lt_log_iff_exp_lt (by norm_num)]
  exact (Real.exp_bound' (by norm_num) (by norm_num) (by norm_num : 0 < 10)).trans_lt (by norm_num)

[Michael Rothgang]

Thanks a lot! You've golfed today's proof for the Carleson project!

[Sébastien Gouëzel]

An even better golf is to use docs#Real.log_two_gt_d9 :-)

[Luigi Massacci]

Didn't @Geoffrey Irving develop a tactic that could do this kind of stuff?

[Sébastien Gouëzel]

So,

import Mathlib

example : 3 * (4 : Real)⁻¹ ≤ 12 * Real.log 2 := by linarith [Real.log_two_gt_d9]

[Michael Rothgang]

There's also #8949 by @Sebastian Zimmer

[Michael Rothgang]

which depends on #8167: that PR has been waiting for review for a long time.

[Kevin Buzzard]

I guess the way to get such a PR in is to first establish that at least one maintainer wants it in and then to continue approaching people saying "please review this" until someone gives in. It doesn't look like it's going to get over the line "organically".

[Bryan Gin-ge Chen]

#8167 at least seems to have maintainer interest since two maintainers are listed as co-authors; unfortunately maybe they would have been best placed to merge...

[Bhavik Mehta]

Calculations like this show up all the time for me, for instance all of these were needed in the ramsey project:
image.png
I'd be very happy to see a general tactics which makes these easier, since I had a couple of ad-hoc methods to make these work

[Alex Meiburg]

ComputableReal is for exactly this type of goal, if you're okay with native_decide!

[Kevin Buzzard]

Unfortunately I think we want proofs that the kernel will be happy with here.

[Joseph Myers]

I had such a statement in my PhD whose proof ended up involving numerical bounds on logarithms (I definitely don't plan for formalize this!).

a.png

($p_0$ is defined elsewhere as the real root of a certain cubic polynomial.)

[Bhavik Mehta]

Yeah, all of these were done without native_decide. Looking at ComputableReal, it also doesn't support logs or real powers, both of which I worked with a ton

[Alex Meiburg]

Ah shoot, it does support logs - but on the dev branch, where it's not 100% done. (The specific case of Real.exp 68/100 < 2 from the original message would be done though.)

[Jireh Loreaux]

Alex, I think this is addressed elsewhere, but I can't find it at the moment. What would it take to eliminate native_decide from ComputableReal?

[Alex Meiburg]

From the Lean side: allowing decide (or decide +kernel) to reduce a partial def would be sufficient, and "cleanest" in the very particular sense that it wouldn't require other modifications to that library.

The other way - which would involve changes only to the library, but many of them - would be to add some kind of gas parameters to all operations (notably, inv and Real.log need this). Then the decidable instance would be something like, trying to find a witness in the first gas many steps of some sequence of bounds, and then otherwise "falling back" to Classical.propDecidable.