Theorem: le_log_one_add (Ray/Dynamics/Multibrot/Postcritical.lean)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
⊢ log 2 * x ≤ (1 + x).log
Tactic:
rw [Real.le_log_iff_exp_le (by linarith)]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
⊢ (log 2 * x).exp ≤ 1 + x

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
⊢ (log 2 * x).exp ≤ 1 + x
Tactic:
have x0' : 0 ≤ 1 - x := by linarith
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
x0' : 0 ≤ 1 - x
⊢ (log 2 * x).exp ≤ 1 + x

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
x0' : 0 ≤ 1 - x
⊢ (log 2 * x).exp ≤ 1 + x
Tactic:
have h := convexOn_exp.2 (mem_univ 0) (mem_univ (log 2)) x0' x0 (by abel)
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
x0' : 0 ≤ 1 - x
h : ((1 - x) • 0 + x • log 2).exp ≤ (1 - x) • exp 0 + x • (log 2).exp
⊢ (log 2 * x).exp ≤ 1 + x

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
x0' : 0 ≤ 1 - x
h : ((1 - x) • 0 + x • log 2).exp ≤ (1 - x) • exp 0 + x • (log 2).exp
⊢ (log 2 * x).exp ≤ 1 + x
Tactic:
simp only [smul_eq_mul, mul_zero, zero_add, Real.exp_zero, mul_one, Real.exp_log zero_lt_two] at h
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
x0' : 0 ≤ 1 - x
h : (x * log 2).exp ≤ 1 - x + x * 2
⊢ (log 2 * x).exp ≤ 1 + x

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
x0' : 0 ≤ 1 - x
h : (x * log 2).exp ≤ 1 - x + x * 2
⊢ (log 2 * x).exp ≤ 1 + x
Tactic:
ring_nf at h
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
x0' : 0 ≤ 1 - x
h : (x * log 2).exp ≤ 1 + x
⊢ (log 2 * x).exp ≤ 1 + x

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
x0' : 0 ≤ 1 - x
h : (x * log 2).exp ≤ 1 + x
⊢ (log 2 * x).exp ≤ 1 + x
Tactic:
rwa [mul_comm]
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
⊢ 0 < 1 + x
Tactic:
linarith
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
⊢ 0 ≤ 1 - x
Tactic:
linarith
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
x0' : 0 ≤ 1 - x
⊢ 1 - x + x = 1
Tactic:
abel
State after:
no goals