2^x ≤ 1 + x for x ∈ [0,1]

Stream: Is there code for X?

[Geoffrey Irving]

Do we have this?

import Mathlib

lemma two_rpow_le_one_add {x : ℝ} (x0 : 0 ≤ x) (x1 : x ≤ 1) : 2^x ≤ 1 + x := by
  sorry

Picture from https://www.wolframalpha.com/input/?i=plot+2%5Ex+and+1+%2B+x:

Screenshot-2024-01-17-at-5.49.40PM.png

[Geoffrey Irving]

I suppose it's just convexity, so docs#convexOn_rpow is the answer.

[Geoffrey Irving]

Oops, no, that's convexity in the left.

[Yaël Dillies]

I don't think we have it

[Geoffrey Irving]

Easy to prove from convexity of exp, which I’ll do shortly.

[Yaël Dillies]

You could even make it an iff! 2^x ≤ 1 + x ↔ x ∈ Icc 0 1

[Geoffrey Irving]

This is odd, but I can't find the lemma that is the normal f (a * x + b * y) <= a * f x + b f y definition of convexity. The closest I can find is convexOn_iff_forall_pos, which is non-ergonomic since the inequalities are strict. There are a ton of other inequalities, but it seems like the very basic one has to also exist.

Ah, I see, it's just .2.