power of difference

Stream: Is there code for X?

[Jakob von Raumer]

Do we have this inequality?

example {a b : ℚ} (n : ℕ) (hn : 0 < n) (hb : 0 < b) (ha : b < a) : a ^ n - b ^ n ≤ n * a ^ (n - 1) * (a - b) := sorry

[Ruben Van de Velde]

It's definitely false for n = 0

[Jakob von Raumer]

Ah right, 0 < n is missing, but that should be it

[Jakob von Raumer]

Ah no, I made another typo above :man_facepalming:

[Geoffrey Irving]

Why is it false for n = 0?

[Damiano Testa]

Also, when a ≤ b, the LHS vanishes, so the inequality should still hold. I thought a b : ℕ!

[Jakob von Raumer]

I fixed the above snippet after @Ruben Van de Velde 's comment :sweat_smile:

[Jakob von Raumer]

Does anyone have a slick way to prove it? I found it here but the proofs don't seem minimal to me

[Kevin Buzzard]

That's the maths proof I was thinking of; you could do this very nicely with a calc block in Lean I think.

[Geoffrey Irving]

Here's the n = 0 case, by the way. Unless I've misread?

import Mathlib

example {a b : ℚ} : a^0 - b^0 ≤ 0 * a ^ (0 - 1) * (a - b) := by
  simp

[Ruben Van de Velde]

It was (a - b) ^ 0 when I commented

[Kevin Buzzard]

You can see edit history of any post on a desktop app by clicking on "edited"

[Jakob von Raumer]

Kevin Buzzard said:

That's the maths proof I was thinking of; you could do this very nicely with a calc block in Lean I think.

Will try and PR if successful

[Riccardo Brasca]

Note that the proof using the intermediate value theorem has the advantage to work for (positive) real exponent.

[Kevin Buzzard]

Why do we want this inequality? And if we do want it, should we consider replacing n by m + 1 and removing the n>0 hypothesis and the horrible n - 1, which we can easily avoid in this case?

[Jakob von Raumer]

Agree to removing n > 0. Well I need it for some error estimates in fixed point arithmetics, and I've certainly seen it before in numerical maths.

[Kevin Buzzard]

If you have an application, then that's a fine response to "why do we want this".

[Jakob von Raumer]

The geometric series proof generalises nicely to StrictOrderedCommRing:

theorem pow_sub_pow_le {R : Type u} [StrictOrderedCommRing R]
    {a b : R} (n : ℕ) (hb : 0 ≤ b) (ha : b ≤ a) :
    a ^ n - b ^ n ≤ n * a ^ (n - 1) * (a - b) := by
  rw [← geom_sum₂_mul]
  apply mul_le_mul_of_nonneg_right _ (sub_nonneg.mpr ha)
  rw [← @geom_sum₂_self]
  apply sum_le_sum
  intros
  apply mul_le_mul_of_nonneg_left _ (pow_nonneg (le_trans hb ha) _)
  apply pow_le_pow_of_le_left hb ha

[Jakob von Raumer]

As for the n - 1, should I bring one a it to the other side for mathlib even if I need it in the form above?