norm_num extensions

Stream: mathlib4

[Patrick Massot]

Terence Tao was disappointed that Lean cannot provide numerical estimates for common functions. He specifically points out:

import Mathlib

open Real

example : rexp 1 * 2 - 2 ≤ 8 * (rexp 1 - 2) := by
  linarith [quadratic_le_exp_of_nonneg (show 0 ≤ 1 by norm_num)]

example : 2*sqrt 7 ≤ 7 := by
  sorry

example : exp (4/exp 1) ≤ 7 := by
  sorry

where the first example works but requires an idea. I guess the second example would be doable pretty quickly deducing from concavity of sqrtthat sqrt x ≤ (x-9)/6+3 (the right-hand side is the first-order approximation at (9, 3)). And I don't want to think about the third example. But really all three examples should be by norm_num. How far are we from that? @Mario Carneiro

[Geoffrey Irving]

I’m working on fixed point interval arithmetic now, which could be one attack on this problem if it’s lifted to floating point (fixed point works only if one is willing do to manual work to pick the exponent).

[Rob Lewis]

I agree this kind of thing should be automated, but I'm not convinced norm_num is the tool. This sounds like a numeric approximation tactic, not numeral normalization.

[Patrick Massot]

Ok, I would be happy with approx_num.

[Geoffrey Irving]

I’ll share my interval arithmetic code once it’s in reasonable shape. Unless someone else has a better version, in which case I’ll switch to that. :)

[Geoffrey Irving]

It uses only UInt64 arithmetic, so no additional axioms (though it’ll be fastest with reduce_bool).

[Rob Lewis]

Incidentally, I tried this (thinking of a sequence of lemmas for rexp 1 parallel to docs#Real.pi_gt_three) and it failed. Looks like linarith's parser needs to learn about ofScientific.

import Mathlib

open Real

lemma two_lt_rexp_1 : 2.5 < rexp 1 := sorry

example : rexp 1 * 2 - 2 ≤ 8 * (rexp 1 - 2) := by
  linarith [two_lt_rexp_1]

[Jireh Loreaux]

Here @Mario Carneiro mentions he has some version of an approx tactic, but it's not clear to me if it is still in Lean 3, ported to Lean 4, almost ready for a PR, or what.

[Mario Carneiro]

It's not almost ready for a PR. In lean 3 it was almost ready as a backend (there was no frontend to speak of), and since mathporting there is still a lot of stuff that has to be done manually to port the tactic part, and after that one also has to design a usable frontend. I tried to give this out as a project but it wasn't a good choice at the time, and right now I think there are other projects higher on the priority list for me.

[Joseph Myers]

You could no doubt prove the third inequality along the lines of my Lean 3 example of bounding powers - https://leanprover.zulipchat.com/#narrow/stream/208328-IMO-grand-challenge/topic/IMO.202020/near/212247641 (the bounds for $e$ are now in mathlib) - though of course an approx tactic would be much better.

[Joseph Myers]

The square root example is at least straightforward by squaring both sides.

import Mathlib.Data.Real.Sqrt

open Real

example : 2 * sqrt 7 ≤ 7 := by
  refine nonneg_le_nonneg_of_sq_le_sq (by positivity) ?_
  rw [← pow_two, mul_pow]
  norm_num

[Arend Mellendijk]

For what it's worth this bound is loose enough that you can get away with some pretty bad estimates for the exponential case. That said this really should be a one-liner.

import Mathlib

open Real

lemma expon_help : 4 / exp 1 ≤ 8/5 := by
  have h := Real.one_sub_div_pow_le_exp_neg (n:=6) (t:=-1) (by norm_num)
  norm_num at h
  rw [div_le_iff (by positivity)]
  linarith

lemma help : exp (8/5) ≤ 7 := by
  have h := Real.one_sub_div_pow_le_exp_neg (n:=5) (t:=8/5) (by norm_num)
  rw[←inv_le_inv (by positivity) (by positivity), ←Real.exp_neg] at h
  norm_num at h
  linarith

example : exp (4/exp 1) ≤ 7 :=
  (exp_le_exp.mpr expon_help).trans help

[Bolton Bailey]

A tactic like this has been desired for a while.

[Gareth Ma]

I think for these lemmas one possible way is to evaluate exp and other terms to some precision using the taylor series using Complex.exp_bound' or their Real equivalent, then use linarith to handle the rest?

[Adomas Baliuka]

For the general tactic, maybe the approach used for the Coq Interval library is an idea?

There's also something confusing me about linarith Never mind, it just can't deal with decimal notation... Replace the goal 4.96 => 496 / 100 and it works.

import Mathlib
open Real
-- Note `exp (8/5) ≈  4.953032424395114803654286356423964256413`
lemma help : exp (8/5) ≤ 4.96 := by
  have h := Real.one_sub_div_pow_le_exp_neg (n:=9999) (t:=8/5) (by norm_num)
  rw[←inv_le_inv (by positivity) (by positivity), ←Real.exp_neg] at h
  norm_num at h
  -- the bound obtained is `exp (8/5) ≤ 4.953666584191391635467168979...`
  linarith -- so maybe this could work?