Theorem: chapter02.Bertrand.real_main_inequality (FormalBook/Chapter_02.lean)

State before:
x : ℝ
n_large : 512 ≤ x
⊢ x * (2 * x) ^ (2 * x).sqrt * 4 ^ (2 * x / 3) ≤ 4 ^ x
Tactic:
let f : ℝ → ℝ := fun x => log x + sqrt (2 * x) * log (2 * x) - log 4 / 3 * x
State after:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
⊢ x * (2 * x) ^ (2 * x).sqrt * 4 ^ (2 * x / 3) ≤ 4 ^ x

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
⊢ x * (2 * x) ^ (2 * x).sqrt * 4 ^ (2 * x / 3) ≤ 4 ^ x
Tactic:
have hf' : ∀ x, 0 < x → 0 < x * (2 * x) ^ sqrt (2 * x) / 4 ^ (x / 3) := fun x h =>
  div_pos (mul_pos h (rpow_pos_of_pos (mul_pos two_pos h) _)) (rpow_pos_of_pos four_pos _)
State after:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
⊢ x * (2 * x) ^ (2 * x).sqrt * 4 ^ (2 * x / 3) ≤ 4 ^ x

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
⊢ x * (2 * x) ^ (2 * x).sqrt * 4 ^ (2 * x / 3) ≤ 4 ^ x
Tactic:
have hf : ∀ x, 0 < x → f x = log (x * (2 * x) ^ sqrt (2 * x) / 4 ^ (x / 3)) := by
  intro x h5
  have h6 := mul_pos (zero_lt_two' ℝ) h5
  have h7 := rpow_pos_of_pos h6 (sqrt (2 * x))
  rw [log_div (mul_pos h5 h7).ne' (rpow_pos_of_pos four_pos _).ne', log_mul h5.ne' h7.ne',
    log_rpow h6, log_rpow zero_lt_four, ← mul_div_right_comm, ← mul_div, mul_comm x]
State after:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
⊢ x * (2 * x) ^ (2 * x).sqrt * 4 ^ (2 * x / 3) ≤ 4 ^ x

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
⊢ x * (2 * x) ^ (2 * x).sqrt * 4 ^ (2 * x / 3) ≤ 4 ^ x
Tactic:
have h5 : 0 < x := lt_of_lt_of_le (by norm_num1) n_large
State after:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ x * (2 * x) ^ (2 * x).sqrt * 4 ^ (2 * x / 3) ≤ 4 ^ x

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ x * (2 * x) ^ (2 * x).sqrt * 4 ^ (2 * x / 3) ≤ 4 ^ x
Tactic:
rw [← div_le_one (rpow_pos_of_pos four_pos x), ← div_div_eq_mul_div, ← rpow_sub four_pos, ←
  mul_div 2 x, mul_div_left_comm, ← mul_one_sub, (by norm_num1 : (1 : ℝ) - 2 / 3 = 1 / 3),
  mul_one_div, ← log_nonpos_iff (hf' x h5), ← hf x h5]
State after:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ f x ≤ 0

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ f x ≤ 0
Tactic:
suffices ∃ x1 x2, 0.5 < x1 ∧ x1 < x2 ∧ x2 ≤ x ∧ 0 ≤ f x1 ∧ f x2 ≤ 0 by
  obtain ⟨x1, x2, h1, h2, h0, h3, h4⟩ := this
  exact (h.right_le_of_le_left'' h1 ((h1.trans h2).trans_le h0) h2 h0 (h4.trans h3)).trans h4
State after:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ ∃ x1 x2, 0.5 < x1 ∧ x1 < x2 ∧ x2 ≤ x ∧ 0 ≤ f x1 ∧ f x2 ≤ 0

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ ∃ x1 x2, 0.5 < x1 ∧ x1 < x2 ∧ x2 ≤ x ∧ 0 ≤ f x1 ∧ f x2 ≤ 0
Tactic:
refine' ⟨18, 512, by norm_num1, by norm_num1, n_large, _, _⟩
State after:
case refine'_1
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ 0 ≤ f 18

case refine'_2
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ f 512 ≤ 0

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
⊢ ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
Tactic:
intro x h5
State after:
x✝ : ℝ
n_large : 512 ≤ x✝
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
x : ℝ
h5 : 0 < x
⊢ f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log

State before:
x✝ : ℝ
n_large : 512 ≤ x✝
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
x : ℝ
h5 : 0 < x
⊢ f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
Tactic:
have h6 := mul_pos (zero_lt_two' ℝ) h5
State after:
x✝ : ℝ
n_large : 512 ≤ x✝
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
x : ℝ
h5 : 0 < x
h6 : 0 < 2 * x
⊢ f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log

State before:
x✝ : ℝ
n_large : 512 ≤ x✝
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
x : ℝ
h5 : 0 < x
h6 : 0 < 2 * x
⊢ f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
Tactic:
have h7 := rpow_pos_of_pos h6 (sqrt (2 * x))
State after:
x✝ : ℝ
n_large : 512 ≤ x✝
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
x : ℝ
h5 : 0 < x
h6 : 0 < 2 * x
h7 : 0 < (2 * x) ^ (2 * x).sqrt
⊢ f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log

State before:
x✝ : ℝ
n_large : 512 ≤ x✝
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
x : ℝ
h5 : 0 < x
h6 : 0 < 2 * x
h7 : 0 < (2 * x) ^ (2 * x).sqrt
⊢ f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
Tactic:
rw [log_div (mul_pos h5 h7).ne' (rpow_pos_of_pos four_pos _).ne', log_mul h5.ne' h7.ne',
  log_rpow h6, log_rpow zero_lt_four, ← mul_div_right_comm, ← mul_div, mul_comm x]
State after:
no goals

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
⊢ 0 < 512
Tactic:
norm_num1
State after:
no goals

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ 1 - 2 / 3 = 1 / 3
Tactic:
norm_num1
State after:
no goals

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ ConcaveOn ℝ (Set.Ioi 0.5) f
Tactic:
apply ConcaveOn.sub
State after:
case hf
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ ConcaveOn ℝ (Set.Ioi 0.5) fun x => x.log + (2 * x).sqrt * (2 * x).log

case hg
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ ConvexOn ℝ (Set.Ioi 0.5) fun x => log 4 / 3 * x

State before:
case hf
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ ConcaveOn ℝ (Set.Ioi 0.5) fun x => x.log + (2 * x).sqrt * (2 * x).log

case hg
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ ConvexOn ℝ (Set.Ioi 0.5) fun x => log 4 / 3 * x
Tactic:
apply ConcaveOn.add
State after:
case hf.hf
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ ConcaveOn ℝ (Set.Ioi 0.5) fun x => x.log

case hf.hg
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ ConcaveOn ℝ (Set.Ioi 0.5) fun x => (2 * x).sqrt * (2 * x).log

case hg
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ ConvexOn ℝ (Set.Ioi 0.5) fun x => log 4 / 3 * x

State before:
case hf.hf
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ ConcaveOn ℝ (Set.Ioi 0.5) fun x => x.log

case hf.hg
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ ConcaveOn ℝ (Set.Ioi 0.5) fun x => (2 * x).sqrt * (2 * x).log

case hg
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ ConvexOn ℝ (Set.Ioi 0.5) fun x => log 4 / 3 * x
Tactic:
exact strictConcaveOn_log_Ioi.concaveOn.subset
  (Set.Ioi_subset_Ioi (by norm_num)) (convex_Ioi 0.5)
State after:
case hf.hg
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ ConcaveOn ℝ (Set.Ioi 0.5) fun x => (2 * x).sqrt * (2 * x).log

case hg
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ ConvexOn ℝ (Set.Ioi 0.5) fun x => log 4 / 3 * x

State before:
case hf.hg
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ ConcaveOn ℝ (Set.Ioi 0.5) fun x => (2 * x).sqrt * (2 * x).log

case hg
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ ConvexOn ℝ (Set.Ioi 0.5) fun x => log 4 / 3 * x
Tactic:
convert ((strictConcaveOn_sqrt_mul_log_Ioi.concaveOn.comp_linearMap
  ((2 : ℝ) • LinearMap.id))) using 1
State after:
case h.e'_9
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ Set.Ioi 0.5 = ⇑(2 • LinearMap.id) ⁻¹' Set.Ioi 1

case hg
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ ConvexOn ℝ (Set.Ioi 0.5) fun x => log 4 / 3 * x

State before:
case hg
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ ConvexOn ℝ (Set.Ioi 0.5) fun x => log 4 / 3 * x
Tactic:
apply ConvexOn.smul
State after:
case hg.hc
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ 0 ≤ log 4 / 3

case hg.hf
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ ConvexOn ℝ (Set.Ioi 0.5) fun x => x

State before:
case hg.hc
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ 0 ≤ log 4 / 3

case hg.hf
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ ConvexOn ℝ (Set.Ioi 0.5) fun x => x
Tactic:
refine div_nonneg (log_nonneg (by norm_num1)) (by norm_num1)
State after:
case hg.hf
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ ConvexOn ℝ (Set.Ioi 0.5) fun x => x

State before:
case hg.hf
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ ConvexOn ℝ (Set.Ioi 0.5) fun x => x
Tactic:
exact convexOn_id (convex_Ioi (0.5 : ℝ))
State after:
no goals

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ 0 ≤ 0.5
Tactic:
norm_num
State after:
no goals

State before:
case h.e'_9
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ Set.Ioi 0.5 = ⇑(2 • LinearMap.id) ⁻¹' Set.Ioi 1
Tactic:
ext x
State after:
case h.e'_9.h
x✝ : ℝ
n_large : 512 ≤ x✝
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x✝
x : ℝ
⊢ x ∈ Set.Ioi 0.5 ↔ x ∈ ⇑(2 • LinearMap.id) ⁻¹' Set.Ioi 1

State before:
case h.e'_9.h
x✝ : ℝ
n_large : 512 ≤ x✝
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x✝
x : ℝ
⊢ x ∈ Set.Ioi 0.5 ↔ x ∈ ⇑(2 • LinearMap.id) ⁻¹' Set.Ioi 1
Tactic:
simp only [Set.mem_Ioi, Set.mem_preimage, LinearMap.smul_apply,
  LinearMap.id_coe, id_eq, smul_eq_mul]
State after:
case h.e'_9.h
x✝ : ℝ
n_large : 512 ≤ x✝
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x✝
x : ℝ
⊢ 0.5 < x ↔ 1 < 2 * x

State before:
case h.e'_9.h
x✝ : ℝ
n_large : 512 ≤ x✝
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x✝
x : ℝ
⊢ 0.5 < x ↔ 1 < 2 * x
Tactic:
rw [← mul_lt_mul_left (two_pos)]
State after:
case h.e'_9.h
x✝ : ℝ
n_large : 512 ≤ x✝
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x✝
x : ℝ
⊢ 2 * 0.5 < 2 * x ↔ 1 < 2 * x

State before:
case h.e'_9.h
x✝ : ℝ
n_large : 512 ≤ x✝
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x✝
x : ℝ
⊢ 2 * 0.5 < 2 * x ↔ 1 < 2 * x
Tactic:
norm_num1
State after:
case h.e'_9.h
x✝ : ℝ
n_large : 512 ≤ x✝
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x✝
x : ℝ
⊢ 1 < 2 * x ↔ 1 < 2 * x

State before:
case h.e'_9.h
x✝ : ℝ
n_large : 512 ≤ x✝
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x✝
x : ℝ
⊢ 1 < 2 * x ↔ 1 < 2 * x
Tactic:
rfl
State after:
no goals

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ 1 ≤ 4
Tactic:
norm_num1
State after:
no goals

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
⊢ 0 ≤ 3
Tactic:
norm_num1
State after:
no goals

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : ∃ x1 x2, 0.5 < x1 ∧ x1 < x2 ∧ x2 ≤ x ∧ 0 ≤ f x1 ∧ f x2 ≤ 0
⊢ f x ≤ 0
Tactic:
obtain ⟨x1, x2, h1, h2, h0, h3, h4⟩ := this
State after:
case intro.intro.intro.intro.intro.intro
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
x1 x2 : ℝ
h1 : 0.5 < x1
h2 : x1 < x2
h0 : x2 ≤ x
h3 : 0 ≤ f x1
h4 : f x2 ≤ 0
⊢ f x ≤ 0

State before:
case intro.intro.intro.intro.intro.intro
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
x1 x2 : ℝ
h1 : 0.5 < x1
h2 : x1 < x2
h0 : x2 ≤ x
h3 : 0 ≤ f x1
h4 : f x2 ≤ 0
⊢ f x ≤ 0
Tactic:
exact (h.right_le_of_le_left'' h1 ((h1.trans h2).trans_le h0) h2 h0 (h4.trans h3)).trans h4
State after:
no goals

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ 0.5 < 18
Tactic:
norm_num1
State after:
no goals

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ 18 < 512
Tactic:
norm_num1
State after:
no goals

State before:
case refine'_1
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ 0 ≤ f 18
Tactic:
have : sqrt (2 * 18) = 6 := (sqrt_eq_iff_mul_self_eq_of_pos (by norm_num1)).mpr (by norm_num1)
State after:
case refine'_1
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 18).sqrt = 6
⊢ 0 ≤ f 18

State before:
case refine'_1
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 18).sqrt = 6
⊢ 0 ≤ f 18
Tactic:
rw [hf _ (by norm_num1), log_nonneg_iff (by positivity), this, one_le_div (by norm_num1)]
State after:
case refine'_1
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 18).sqrt = 6
⊢ 4 ^ (18 / 3) ≤ 18 * (2 * 18) ^ 6

State before:
case refine'_1
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 18).sqrt = 6
⊢ 4 ^ (18 / 3) ≤ 18 * (2 * 18) ^ 6
Tactic:
norm_num1
State after:
no goals

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ 0 < 6
Tactic:
norm_num1
State after:
no goals

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ 6 * 6 = 2 * 18
Tactic:
norm_num1
State after:
no goals

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 18).sqrt = 6
⊢ 0 < 18
Tactic:
norm_num1
State after:
no goals

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 18).sqrt = 6
⊢ 0 < 18 * (2 * 18) ^ (2 * 18).sqrt / 4 ^ (18 / 3)
Tactic:
positivity
State after:
no goals

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 18).sqrt = 6
⊢ 0 < 4 ^ (18 / 3)
Tactic:
norm_num1
State after:
no goals

State before:
case refine'_2
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ f 512 ≤ 0
Tactic:
have : sqrt (2 * 512) = 32 :=
  (sqrt_eq_iff_mul_self_eq_of_pos (by norm_num1)).mpr (by norm_num1)
State after:
case refine'_2
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ f 512 ≤ 0

State before:
case refine'_2
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ f 512 ≤ 0
Tactic:
rw [hf _ (by norm_num1), log_nonpos_iff (hf' _ (by norm_num1)), this,
    div_le_one (by positivity)]
State after:
case refine'_2
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ 512 * (2 * 512) ^ 32 ≤ 4 ^ (512 / 3)

State before:
case refine'_2
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ 512 * (2 * 512) ^ 32 ≤ 4 ^ (512 / 3)
Tactic:
conv in 512 => equals 2 ^ 9 => norm_num1
State after:
case refine'_2
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ 2 ^ 9 * (2 * 512) ^ 32 ≤ 4 ^ (512 / 3)

State before:
case refine'_2
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ 2 ^ 9 * (2 * 512) ^ 32 ≤ 4 ^ (512 / 3)
Tactic:
conv in 2 * 512 => equals 2 ^ 10 => norm_num1
State after:
case refine'_2
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ 2 ^ 9 * (2 ^ 10) ^ 32 ≤ 4 ^ (512 / 3)

State before:
case refine'_2
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ 2 ^ 9 * (2 ^ 10) ^ 32 ≤ 4 ^ (512 / 3)
Tactic:
conv in 32 => rw [← Nat.cast_ofNat]
State after:
case refine'_2
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ 2 ^ 9 * (2 ^ 10) ^ ↑32 ≤ 4 ^ (512 / 3)

State before:
case refine'_2
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ 2 ^ 9 * (2 ^ 10) ^ ↑32 ≤ 4 ^ (512 / 3)
Tactic:
rw [rpow_natCast, ← pow_mul, ← pow_add]
State after:
case refine'_2
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ 2 ^ (9 + 10 * 32) ≤ 4 ^ (512 / 3)

State before:
case refine'_2
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ 2 ^ (9 + 10 * 32) ≤ 4 ^ (512 / 3)
Tactic:
conv in 4 => equals 2 ^ (2 : ℝ) => rw [rpow_two]; norm_num1
State after:
case refine'_2
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ 2 ^ (9 + 10 * 32) ≤ (2 ^ 2) ^ (512 / 3)

State before:
case refine'_2
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ 2 ^ (9 + 10 * 32) ≤ (2 ^ 2) ^ (512 / 3)
Tactic:
rw [← rpow_mul, ← rpow_natCast]
State after:
case refine'_2
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ 2 ^ ↑(9 + 10 * 32) ≤ 2 ^ (2 * (512 / 3))

case refine'_2.hx
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ 0 ≤ 2

State before:
case refine'_2
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ 2 ^ ↑(9 + 10 * 32) ≤ 2 ^ (2 * (512 / 3))

case refine'_2.hx
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ 0 ≤ 2
Tactic:
apply rpow_le_rpow_of_exponent_le
State after:
case refine'_2.hx
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ 1 ≤ 2

case refine'_2.hyz
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ ↑(9 + 10 * 32) ≤ 2 * (512 / 3)

case refine'_2.hx
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ 0 ≤ 2

State before:
case refine'_2.hx
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ 1 ≤ 2

case refine'_2.hyz
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ ↑(9 + 10 * 32) ≤ 2 * (512 / 3)

case refine'_2.hx
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ 0 ≤ 2
Tactic:
all_goals norm_num1
State after:
no goals

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ 0 < 32
Tactic:
norm_num1
State after:
no goals

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ 32 * 32 = 2 * 512
Tactic:
norm_num1
State after:
no goals

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ 0 < 512
Tactic:
norm_num1
State after:
no goals

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ 0 < 4 ^ (512 / 3)
Tactic:
positivity
State after:
no goals

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ 512 = 2 ^ 9
Tactic:
norm_num1
State after:
no goals

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ 2 * 512 = 2 ^ 10
Tactic:
norm_num1
State after:
no goals

State before:
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ 4 = 2 ^ 2
Tactic:
norm_num1
State after:
no goals

State before:
case refine'_2.hx
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 512).sqrt = 32
⊢ 0 ≤ 2
Tactic:
norm_num1
State after:
no goals