log 200 * 20000 ≤ 106000

Stream: Is there code for X?

[Geoffrey Irving]

What's the fastest way to prove something like this these days?

import Mathlib.Analysis.SpecialFunctions.Log.Basic

lemma log_mul_le : Real.log 200 * 20000 ≤ 106000 := by
  sorry

(in straight Mathlib, so in particular no https://github.com/girving/interval.)

[Ruben Van de Velde]

That's a pretty tight bound, if I can believe wolfram... I doubt we have anything that can get you there quickly. How would you prove this on paper?

[Geoffrey Irving]

If there's nothing better I'll do stuff like https://github.com/girving/ray/blob/main/Ray/Dynamics/Multibrot/Specific.lean.

[Geoffrey Irving]

That is, rearrange until it's norm_num using the existing bounds on rexp 1.

[Ruben Van de Velde]

Yep, that works

import Mathlib.Analysis.SpecialFunctions.Log.Basic

lemma lt_exp_div {a b : ℕ} {c : ℝ} (a0 : a ≠ 0 := by norm_num) (b0 : b ≠ 0 := by norm_num)
    (c0 : 0 < c := by norm_num) (h0 : c ^ b < 2.7182818283 ^ a := by norm_num) :
    c < Real.exp (a / b) := sorry

lemma log_mul_le : Real.log 200 * 20000 ≤ 106000 := by
  apply mul_le_of_nonneg_of_le_div
  rotate_right
  rw [Real.log_le_iff_le_exp]
  apply le_of_lt
  apply lt_exp_div
  all_goals norm_num

[Geoffrey Irving]

lemma log_mul_le : Real.log 200 * 20000 ≤ 106000 := by
  rw [← le_div_iff (by norm_num), Real.log_le_iff_le_exp (by norm_num)]
  norm_num
  rw [← Real.exp_one_rpow, div_eq_mul_inv, Real.rpow_mul (by positivity),
    Real.le_rpow_inv_iff_of_pos (by norm_num) (by positivity) (by norm_num)]
  refine le_trans ?_ (Real.rpow_le_rpow (by norm_num) Real.exp_one_gt_d9.le (by norm_num))
  norm_num

[Geoffrey Irving]

Nice, yours is significantly cleaner. :)

[Ruben Van de Velde]

Even better:

import Mathlib.Analysis.SpecialFunctions.Log.Basic

lemma lt_exp_div {a b : ℕ} {c : ℝ} (a0 : a ≠ 0 := by norm_num) (b0 : b ≠ 0 := by norm_num)
    (c0 : 0 < c := by norm_num) (h0 : c ^ b < 2.7182818283 ^ a := by norm_num) :
    c < Real.exp (a / b) := sorry

lemma log_mul_lt : Real.log 200 * 20000 < 106000 := by
  rw [← lt_div_iff, Real.log_lt_iff_lt_exp]
  apply lt_exp_div
  all_goals norm_num

lemma log_mul_le : Real.log 200 * 20000 ≤ 106000 :=
  log_mul_lt.le

[Geoffrey Irving]

Where this came up: https://github.com/girving/debate/commit/4e1513b569784ee15713d7fb6c0f9f6934d1a56c

106000 is already horribly large, so I didn't want to make it any embarrassingly looser than it already is. :)

[Ruben Van de Velde]

Btw, you might want to use Nat.ceil_lt_add_one

[Geoffrey Irving]

Aha, nice. Was foolishly searching with “le” instead of “lt”.

[Gareth Ma]

I am not as fancy as Ruben, so here's how I approached it for another project. There are some exponent bounds already in Mathlib. The two I use are Real.exp_one_near_10, which gives an approximation to exp(1) with error 10^-10, and Real.exp_bound, which bounds the Taylor series, which I use for the exp(0.3) part.

Then first I checked how many terms I need for the Taylor series using this (since I read above that the bound is "very tight", but not really):

#eval (Id.run do
  let x : ℚ := 3 / 10
  let n : ℕ := 5
  let exp1L : ℚ := 2244083 / 825552 - 1 / 10 ^ 10
  let exp0_3L := (∑ m ∈ Finset.range n, x ^ m / m.factorial) - |x| ^ n * n.succ / (n.factorial * n)
  let exp5_3L := exp0_3L * exp1L ^ 5
  return exp5_3L) > 200
-- true

Great, we only need 5 terms, so now we can just prove the theorem

open Real Finset in
lemma log_mul_lt : Real.log 200 * 20000 < 106000 := by
  rw [← lt_div_iff (by norm_num), log_lt_iff_lt_exp (by norm_num)]
  norm_num
  rw [show (53 : ℝ) / 10 = 5 + 3 / 10 by norm_num, Real.exp_add]
  -- want exp(5 + 0.3) > 200
  -- Bound on exp(5)
  have h₁ := pow_le_pow_left (by norm_num)
    (tsub_le_iff_tsub_le.mp <| (abs_sub_le_iff.mp exp_one_near_10).right) 5
  -- Bound on exp(0.3)
  have h₂₁ := exp_bound (x := 3 / 10) (abs_le.mpr ⟨by norm_num, by norm_num⟩) zero_lt_four
  have h₂₂ := tsub_le_iff_tsub_le.mp <| (abs_sub_le_iff.mp h₂₁).right
  iterate 4 erw [Finset.sum_range_succ] at h₂₂
  erw [Finset.sum_range_zero, abs_eq_self.mpr (by norm_num)] at h₂₂
  norm_num [Nat.factorial] at h₁ h₂₂
  -- Combine
  refine lt_of_lt_of_le ?_ <| mul_le_mul h₁ h₂₂ (by norm_num) (exp_nonneg _)
  norm_num

[Geoffrey Irving]

I do hope to make the one-word tactic for this using https://github.com/girving/interval someday, but no ETA due to day job. E.g., something like

lemma log_mul_lt : Real.log 200 * 20000 < 106000 := by interval

[Ruben Van de Velde]

I think we've talked about an approx tactic before as well

[Geoffrey Irving]

All of the approximation work is already there in that repo, but I haven't done the tactic work. It would mean walking the expression, turning it into an interval equivalent, proving conservativeness using aesop (this is already set up, though using mono instead of aesop for no good reason), then evaluating the interval expression. But I didn't get quite there before the day job started.

Also it'd be hard to get it into Mathlib as the interval repo is messy.

[Geoffrey Irving]

Also the Mathlib version would probably want to be variable precision, not only 64-bit.

[Geoffrey Irving]

Forgot to add the link to the described interval tactic:

https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/An.20interval.20tactic.20for.20constant.20real.20inequalities/near/445456796

example : log 200 * 20000 ≤ 106000 := by interval

[Kevin Buzzard]

@Bhavik Mehta presumably this would have made your combi formalisations a lot easier?

[Geoffrey Irving]

Though it uses native_decide, which means the standard is not to trust it, I think. It's possible optimizations would make rfl work instead; I haven't tried.

[Bhavik Mehta]

It would have helped a little, but my calculations with interval arithmetic were all generic enough to be auto-generated by external programs which output lean code, and didn't require native_decide, so this wouldn't help much in the cases I have most often

[Julian Berman]

auto-generated by external programs which output lean code

OT for the thread clearly, but can you share a tiny bit more about what that means? You wrote a little metaprogram in some other language and generated some ad hoc Lean code with it?

[Bhavik Mehta]

Not a metaprogram, just a python script which outputted lean code, and the lean code could be pasted in and verified the calculations as necessary. My point being that what I had was worse than Geoffrey's tactic in that it required external programs to generate the proof rather than a lean metaprogram to do such; but better in that the proof doesn't require native_decide. From what I can tell without trying, is that this approach isn't able to generate the precision that my approach had, but should be enough for the precision that I actually needed

[Kyle Miller]

(A program that writes a program is the definition of a metaprogram @Bhavik Mehta :-) It doesn't need to be written in Lean to count, though certainly it's convenient if it's all in Lean.)

[Bhavik Mehta]

Kyle Miller said:

o count, though certainly it's convenie

(Fair point, I meant that it's not a metaprogram in the language it was written in! That is, it wasn't a python program that generates python code, which in my mind is the implication of "a metaprogram in python". But point taken!)