0.54 < Real.cos 1 ∧ Real.cos 1 < 0.55

Stream: Is there code for X?

[Kevin Buzzard]

I'm updating course notes. Am I still correct to claim that "Lean is not a calculator -- for example proving 0.54 < Real.cos 1 ∧ Real.cos 1 < 0.55 will probably be quite a difficult task"? As far as I know there has been no progress on questions such as this since last year.

[Alex Kontorovich]

Can't you use the first few terms of the series expansion, which is alternating, so gives upper/lower bounds? (Do we have that in mathlib?)

[Kevin Buzzard]

I guess, but I suppose what I'm really angling for is some kind of := by approx tactic (which I think has been discussed before, but I'm unclear about what the scope should be).

[Eric Rodriguez]

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/New.20.60by_approx.60.20tactic.20for.20proving.20real.20inequalities @Sebastian Zimmer is working on this, it seems

[Kevin Buzzard]

Your answer is quite annoying Alex, because I'm struggling to think of a harder question :-) For 6.082 < Real.sqrt 37 you can just square both sides, for sin and cos you can use the trick you mentioned, exp you can use the power series for lower bounds (and probably there's a simple trick for upper bounds), for log you can use the inverse of exp, and I'm running out of functions. What about the $j$-invariant? :-) Pari-GP can do it...

? ellj((1+sqrt(-163))/2)
%3 = -262537412640768000.00000000000000000000
?

[Kevin Buzzard]

Eric Rodriguez said:

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/New.20.60by_approx.60.20tactic.20for.20proving.20real.20inequalities Sebastian Zimmer is working on this, it seems

Oh nice! Somehow I'd missed this. I've added my :tada: :-)

[Alex J. Best]

Aren't the collection of all such "tricks" exactly how calculators to compute these quantities work, in the end they are also programmed by hand to compute good approximations to values of special functions?

[Jireh Loreaux]

If you want to give them a hard problem, you could ask them to find BB(5). :laughing: But not even calculators / computers can do that.

[Yury G. Kudryashov]

Or $H(2)$ https://en.wikipedia.org/wiki/Hilbert%27s_sixteenth_problem#The_second_part_of_Hilbert's_16th_problem

[Joseph Myers]

In the absence of by approx, it looks something like this. (All those local simp lemmas for powers of I illustrate something that's got worse with Lean 4 - we've lost the effects of I_pow_bit0 and I_pow_bit1 without a replacement to get simp simplifying I to the power of natural number literals automatically.)

import Mathlib.Data.Complex.Exponential

open Complex

@[simp]
theorem I_pow_3 : I ^ 3 = -I := by
  simp [pow_three]

@[simp]
theorem I_pow_4 : I ^ 4 = 1 := by
  change I * I ^ 3 = 1
  simp

@[simp]
theorem I_pow_5 : I ^ 5 = I := by
  change I * I ^ 4 = I
  simp

@[simp]
theorem I_pow_6 : I ^ 6 = -1 := by
  change I * I ^ 5 = -1
  simp

@[simp]
theorem I_pow_7 : I ^ 7 = -I := by
  change I * I ^ 6 = -I
  simp

theorem aux1 : abs (Complex.exp I - (389 / 720 + I * (4241 / 5040))) ≤ 35840⁻¹ := by
  have h := exp_bound abs_I.le (show 0 < 8 by norm_num)
  norm_num [Finset.range, Nat.factorial] at h
  convert h using 1 <;> ring_nf

theorem aux2 : |Real.cos 1 - 389 / 720| ≤ 35840⁻¹ := by
  have h := aux1
  rw [←one_mul I, ←cos_add_sin_I, one_mul] at h
  convert (abs_re_le_abs _).trans h
  simp
  rw [←ofReal_one, cos_ofReal_re, sin_ofReal_im, neg_zero, add_zero]

theorem cos_one : 0.54 < Real.cos 1 ∧ Real.cos 1 < 0.55 := by
  have h := (abs_le'.1 aux2)
  norm_num
  constructor <;> linarith

[Kevin Buzzard]

Thank you Joseph! I chose this example in my course notes because I thought it would be much worse than this!

[Damiano Testa]

Btw, the proofs of the I_pow_j lemmas could also all be simp [pow_succ] (and are not needed for the rest to work).

[Eric Wieser]

Perhaps we should have I ^ (succ (succ n)) = -I ^ n as a simp lemma?

[Damiano Testa]

Eric, I like your suggestion! With that, the proofs of the I_pow_j lemmas are by simp, of course.

[Joseph Myers]

So this does work with pow_succ included in the lemmas passed to norm_num instead of adding all those separate I_pow_ lemmas.

I'm not sure exactly what if any kinds of expressions involving I norm_num is meant to work with (given the unlimited scope of expressions mathematicians may want to be evaluated exactly, many of which have definitely been said to be outside the scope of norm_num), but being able to do exact evaluations of expressions involving I, integer literals and field operations (including integer powers), producing a result in some canonical form such as "rational + rational * I", does seem like it would be useful for some tactic (independent of an approximation tactic). (It's definitely what I wanted to do when evaluating the result given by a particular use of exp_bound in order to work out what the statement of aux1 should be.)

[Eric Rodriguez]

norm_num is, as far as I can tell, presently not great at complex numbers.

[Joseph Myers]

Should it be? Is it in scope for norm_num to be able to prove e.g. I ^ 5 / 2 + I ^ 7 / 3 = I / 6 without needing to pass any extra arguments to norm_num? Or is that beyond the scope of what's considered a "number" that it should normalize?