Help with numerical computation

Stream: mathlib4

[Gareth Ma]

Hi, it took me couple hours, but I have arrived at this point - one simple computation away from my goal.
And I'm struggling to prove it :) Any help would be appreciated. This is my first time doing stuff like this.

import Mathlib.Tactic

open Real BigOperators

example : 0 ≤ ∑ x in Finset.Icc (1 : ℕ) 6, x * (log (x + 1) - log x) - 7 + log 7 := by
  conv => rhs ; lhs ; lhs ; whnf
  simp only [List.range', List.map, List.foldr]
  norm_num
  ring_nf
  sorry

[Eric Rodriguez]

example : 0 ≤ ∑ x in Finset.Icc (1 : ℕ) 6, x * (log (x + 1) - log x) - 7 + log 7 := by
  have : Finset.Icc 1 6 = {1, 2, 3, 4, 5, 6} := sorry
  norm_num [this]
  ring_nf

I think is probably slightly more principled? Although I'm not sure how to get that top lemma easily, to be fair

But I think the goal after that is just hard until we get these numerical approximation tactics...

[Gareth Ma]

Eric Rodriguez said:

example : 0 ≤ ∑ x in Finset.Icc (1 : ℕ) 6, x * (log (x + 1) - log x) - 7 + log 7 := by
  have : Finset.Icc 1 6 = {1, 2, 3, 4, 5, 6} := sorry
  norm_num [this]
  ring_nf

I think is probably slightly more principled? Although I'm not sure how to get that top lemma easily, to be fair

But I think the goal after that is just hard until we get these numerical approximation tactics...

The stuff I typed is just messing around, but nice (is the first lemma not rfl?). Any help with the log goal would be appreciated :sob:

[Michael Stoll]

I think it would follow from $e \le 87/32$, which (if I'm not mistaken) is one of the continued fraction approximations to $e$. So if someone proves that $e = [2; 1, 2, 1, 1, 4, 1, 1, 6, 1, \dots]$, one could use the theory of continued fractions. However, I think the statement that the approximants give alternatingly lower and upper bounds is missing from Mathlib.

[Gareth Ma]

How did you get that numerical expression?

[Gareth Ma]

I worked on it a bit, and got this far:

```lean
example : 0 ≤ ∑ x in Finset.Icc (1 : ℕ) 6, x * (log (x + 1) - log x) - 7 + log 7 := by
  have : Finset.Icc (1 : ℕ) 6 = {1, 2, 3, 4, 5, 6} := by rfl
  simp [this]
  ring_nf
  save
  rw [add_sub, add_sub]
  repeat rw [←sub_eq_add_neg]
  iterate 4 rw [sub_sub, ←log_mul]
  nth_rw 3 [show (7 : ℝ) = (7 : ℕ) by rfl]
  rw [mul_comm (log _) _, add_comm_sub, ←log_pow, ←log_div]
  all_goals try norm_num
  rw [le_log_iff_exp_le]

Goal:
⊢ rexp 7 ≤ 823543 / 720

[Gareth Ma]

(TLDR expand everything then use $\log(xy) = \log(x) + \log(y)$ and friends

[Gareth Ma]

Your continued fraction way will definitely be a clean way to do these type of inequalities. But I think I will try to bound $\exp\left(1\right)$ then raise it to the $7$ power

[Gareth Ma]

Because there's exp_bound which bounds $\exp(x)$ for $|x| \leq 1$?

[Gareth Ma]

Or I can use Data/Complex/ExponentialBounds.lean

[Oliver Nash]

Incidentally:

import Mathlib.Data.Complex.ExponentialBounds

example : Real.exp 1 < 87 / 32 :=
  lt_trans Real.exp_one_lt_d9 <| by norm_num

[Gareth Ma]

:O

[Gareth Ma]

example : 0 ≤ ∑ x in Finset.Icc (1 : ℕ) 6, x * (log (x + 1) - log x) - 7 + log 7 := by
  have : Finset.Icc (1 : ℕ) 6 = {1, 2, 3, 4, 5, 6} := by rfl
  simp [this]
  ring_nf
  rw [add_sub, add_sub]
  repeat rw [←sub_eq_add_neg]
  iterate 4 rw [sub_sub, ←log_mul]
  nth_rw 3 [show (7 : ℝ) = (7 : ℕ) by rfl]
  rw [mul_comm (log _) _, add_comm_sub, ←log_pow, ←log_div]
  all_goals try norm_num
  rw [le_log_iff_exp_le]
  /- annoying issue: There's both (a : ℝ) ^ (b : ℕ) and (a : ℝ) ^ (b : ℝ) -/
  let h := @rpow_le_rpow _ _ (7 : ℕ) ?_ (tsub_le_iff_left.mp $ (abs_le.mp exp_one_near_20).right) ?_
  rw [exp_one_rpow, rpow_nat_cast] at h
  apply h.trans
  all_goals norm_num
  exact le_of_lt $ exp_pos 1
  done

Tada! Worst code ever :D

[Jireh Loreaux]

@Gareth Ma , do you know about the HPow bug? If not, search Zulip for " local macro"

[Gareth Ma]

Oh someone mentioned it once. Is it what's happening here?

[Gareth Ma]

I think I will investigate and fix it later, I want to finish this proof first :)

[Gareth Ma]

Progress! very excited.

[Gareth Ma]

(Trying to prove $\sum_{x \leq n} \log x = n \log n - n + O(\log n)$...)

[Gareth Ma]

Actually I am proving a stricter version $\left|\sum_{x \leq n} \log x - (n \log n - n)\right| \leq 2\log n$