awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
t : A
n : ℕ
h :
  Eq (α := A)
    ((PowerSeries.coeff 0 : (a : A⟦X⟧) → A)
        ((PowerSeries.mk fun (n : ℕ) ↦ (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) *
          (exp A - 1)) :
      A)
    ((PowerSeries.coeff 0 : (a : A⟦X⟧) → A)
        (HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) PowerSeries.X ((rescale t : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧)) :
      A)
⊢ Eq (α := A)
    ((PowerSeries.coeff n : (a : A⟦X⟧) → A)
        ((PowerSeries.mk fun (n : ℕ) ↦ (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) *
          (exp A - 1)) :
      A)
    ((PowerSeries.coeff n : (a : A⟦X⟧) → A)
        (HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) PowerSeries.X ((rescale t : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧)) :
      A)
have h₁ : ∀ (n : ℕ),
  Eq (α := A)
    ((PowerSeries.coeff (n + 1) : (a : A⟦X⟧) → A)
        ((PowerSeries.mk fun (n : ℕ) ↦ (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) *
          (exp A - 1)) :
      A)
    ((PowerSeries.coeff (n + 1) : (a : A⟦X⟧) → A)
        (HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) PowerSeries.X ((rescale t : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧)) :
      A)
Tactic: cases n with | zero => simp | succ n =>
  -- n ≥ 1, the coefficients is a sum to n+2, so use `sum_range_succ` to write as
  -- last term plus sum to n+1
  rw [coeff_succ_X_mul, coeff_rescale, coeff_exp, PowerSeries.coeff_mul,
    Nat.sum_antidiagonal_eq_sum_range_succ_mk, sum_range_succ]
  -- last term is zero so kill with `add_zero`
  simp only [map_sub, tsub_self, constantCoeff_one, constantCoeff_exp,
    coeff_zero_eq_constantCoeff, mul_zero, sub_self, add_zero]
  -- Let's multiply both sides by (n+1)! (OK because it's a unit)
  have hnp1 : IsUnit ((n + 1)! : ℚ) := IsUnit.mk0 _ (mod_cast factorial_ne_zero (n + 1))
  rw [← (hnp1.map (algebraMap ℚ A)).mul_right_inj]
  -- do trivial rearrangements to make RHS (n+1)*t^n
  rw [mul_left_comm, ← map_mul]
  change _ = t ^ n * algebraMap ℚ A (((n + 1) * n ! : ℕ) * (1 / n !))
  rw [cast_mul, mul_assoc,
    mul_one_div_cancel (show (n ! : ℚ) ≠ 0 from cast_ne_zero.2 (factorial_ne_zero n)), mul_one,
    mul_comm (t ^ n), ← aeval_monomial, cast_add, cast_one]
  -- But this is the RHS of `Polynomial.sum_bernoulli`
  rw [← sum_bernoulli, Finset.mul_sum, map_sum]
  -- and now we have to prove a sum is a sum, but all the terms are equal.
  apply Finset.sum_congr rfl
  -- The rest is just trivialities, hampered by the fact that we're coercing
  -- factorials and binomial coefficients between ℕ and ℚ and A.
  intro i hi
  -- deal with coefficients of e^X-1
  simp only [Nat.cast_choose ℚ (mem_range_le hi), coeff_mk, if_neg (mem_range_sub_ne_zero hi),
    PowerSeries.coeff_one, coeff_exp, sub_zero, Algebra.smul_def,
    mul_right_comm _ ((aeval t) _), ← mul_assoc, ← map_mul, ← Polynomial.C_eq_algebraMap,
    Polynomial.aeval_mul, Polynomial.aeval_C]
  -- finally cancel the Bernoulli polynomial and the algebra_map
  field_simp
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (hypothesis)
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
⊢ x * (2 * x) ^ √(2 * x) * HPow.hPow (α := ℝ) 4 (2 * x / 3) ≤ HPow.hPow (α := ℝ) 4 x
have hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
Tactic: have hf' : ∀ x, 0 < x → 0 < x * (2 * x) ^ √(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 _)
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (hypothesis)
Goal:
x_1 : ℝ
x_large : 512 ≤ x_1
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
x : ℝ
h5 : 0 < x
⊢ f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
have h6 : 0 < 2 * x
Tactic: have h6 := mul_pos (zero_lt_two' ℝ) h5
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (hypothesis)
Goal:
x_1 : ℝ
x_large : 512 ≤ x_1
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
x : ℝ
h5 : 0 < x
h6 : 0 < 2 * x
⊢ f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
have h7 : 0 < (2 * x) ^ √(2 * x)
Tactic: have h7 := rpow_pos_of_pos h6 (√(2 * x))
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
x_1 : ℝ
x_large : 512 ≤ x_1
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
x : ℝ
h5 : 0 < x
h6 : 0 < 2 * x
h7 : 0 < (2 * x) ^ √(2 * x)
⊢ f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
have rw : f x = log (x * (2 * x) ^ √(2 * x)) - log (HPow.hPow (α := ℝ) 4 (x / 3))
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
x_1 : ℝ
x_large : 512 ≤ x_1
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
x : ℝ
h5 : 0 < x
h6 : 0 < 2 * x
h7 : 0 < (2 * x) ^ √(2 * x)
rw : f x = log (x * (2 * x) ^ √(2 * x)) - log (HPow.hPow (α := ℝ) 4 (x / 3))
⊢ f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
have rw₁ : f x = log x + log ((2 * x) ^ √(2 * x)) - log (HPow.hPow (α := ℝ) 4 (x / 3))
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
x_1 : ℝ
x_large : 512 ≤ x_1
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
x : ℝ
h5 : 0 < x
h6 : 0 < 2 * x
h7 : 0 < (2 * x) ^ √(2 * x)
rw : f x = log (x * (2 * x) ^ √(2 * x)) - log (HPow.hPow (α := ℝ) 4 (x / 3))
rw₁ : f x = log x + log ((2 * x) ^ √(2 * x)) - log (HPow.hPow (α := ℝ) 4 (x / 3))
⊢ f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
have rw₂ : f x = log x + √(2 * x) * log (2 * x) - log (HPow.hPow (α := ℝ) 4 (x / 3))
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
x_1 : ℝ
x_large : 512 ≤ x_1
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
x : ℝ
h5 : 0 < x
h6 : 0 < 2 * x
h7 : 0 < (2 * x) ^ √(2 * x)
rw : f x = log (x * (2 * x) ^ √(2 * x)) - log (HPow.hPow (α := ℝ) 4 (x / 3))
rw₁ : f x = log x + log ((2 * x) ^ √(2 * x)) - log (HPow.hPow (α := ℝ) 4 (x / 3))
rw₂ : f x = log x + √(2 * x) * log (2 * x) - log (HPow.hPow (α := ℝ) 4 (x / 3))
⊢ f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
have rw₃ : f x = log x + √(2 * x) * log (2 * x) - x / 3 * log 4
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
x_1 : ℝ
x_large : 512 ≤ x_1
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
x : ℝ
h5 : 0 < x
h6 : 0 < 2 * x
h7 : 0 < (2 * x) ^ √(2 * x)
rw : f x = log (x * (2 * x) ^ √(2 * x)) - log (HPow.hPow (α := ℝ) 4 (x / 3))
rw₁ : f x = log x + log ((2 * x) ^ √(2 * x)) - log (HPow.hPow (α := ℝ) 4 (x / 3))
rw₂ : f x = log x + √(2 * x) * log (2 * x) - log (HPow.hPow (α := ℝ) 4 (x / 3))
rw₃ : f x = log x + √(2 * x) * log (2 * x) - x / 3 * log 4
⊢ f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
have rw₄ : f x = log x + √(2 * x) * log (2 * x) - x * log 4 / 3
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
x_1 : ℝ
x_large : 512 ≤ x_1
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
x : ℝ
h5 : 0 < x
h6 : 0 < 2 * x
h7 : 0 < (2 * x) ^ √(2 * x)
rw : f x = log (x * (2 * x) ^ √(2 * x)) - log (HPow.hPow (α := ℝ) 4 (x / 3))
rw₁ : f x = log x + log ((2 * x) ^ √(2 * x)) - log (HPow.hPow (α := ℝ) 4 (x / 3))
rw₂ : f x = log x + √(2 * x) * log (2 * x) - log (HPow.hPow (α := ℝ) 4 (x / 3))
rw₃ : f x = log x + √(2 * x) * log (2 * x) - x / 3 * log 4
rw₄ : f x = log x + √(2 * x) * log (2 * x) - x * log 4 / 3
⊢ f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
have rw₅ : f x = log x + √(2 * x) * log (2 * x) - x * (log 4 / 3)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
x_1 : ℝ
x_large : 512 ≤ x_1
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
x : ℝ
h5 : 0 < x
h6 : 0 < 2 * x
h7 : 0 < (2 * x) ^ √(2 * x)
rw : f x = log (x * (2 * x) ^ √(2 * x)) - log (HPow.hPow (α := ℝ) 4 (x / 3))
rw₁ : f x = log x + log ((2 * x) ^ √(2 * x)) - log (HPow.hPow (α := ℝ) 4 (x / 3))
rw₂ : f x = log x + √(2 * x) * log (2 * x) - log (HPow.hPow (α := ℝ) 4 (x / 3))
rw₃ : f x = log x + √(2 * x) * log (2 * x) - x / 3 * log 4
rw₄ : f x = log x + √(2 * x) * log (2 * x) - x * log 4 / 3
rw₅ : f x = log x + √(2 * x) * log (2 * x) - x * (log 4 / 3)
⊢ f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
have rw₆ : f x = log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (hypothesis)
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
⊢ x * (2 * x) ^ √(2 * x) * HPow.hPow (α := ℝ) 4 (2 * x / 3) ≤ HPow.hPow (α := ℝ) 4 x
have hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
Tactic: have hf : ∀ x, 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)) := by
    intro x h5
    have h6 := mul_pos (zero_lt_two' ℝ) h5
    have h7 := rpow_pos_of_pos h6 (√(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]
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (hypothesis)
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
⊢ x * (2 * x) ^ √(2 * x) * HPow.hPow (α := ℝ) 4 (2 * x / 3) ≤ HPow.hPow (α := ℝ) 4 x
have h5 : 0 < x
Tactic: have h5 : 0 < x := lt_of_lt_of_le (by norm_num1) x_large
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
⊢ x * (2 * x) ^ √(2 * x) * HPow.hPow (α := ℝ) 4 (2 * x / 3) ≤ HPow.hPow (α := ℝ) 4 x
have rw : f x ≤ 0
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).le, ← hf x h5]
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
⊢ ConcaveOn ℝ (Set.Ioi 0.5) f
have hf₁ : ConcaveOn ℝ (β := ℝ) (Set.Ioi 0.5) fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x)
Tactic: apply ConcaveOn.sub
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
hf₁ : ConcaveOn ℝ (β := ℝ) (Set.Ioi 0.5) fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x)
⊢ ConcaveOn ℝ (Set.Ioi 0.5) f
have hg : ConvexOn ℝ (E := ℝ) (Set.Ioi 0.5) (HMul.hMul (log 4 / 3))
Tactic: apply ConcaveOn.sub
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
⊢ ConcaveOn ℝ (β := ℝ) (Set.Ioi 0.5) fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x)
have hf₁ : ConcaveOn ℝ (Set.Ioi 0.5) log
Tactic: apply ConcaveOn.add
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
hf₁ : ConcaveOn ℝ (Set.Ioi 0.5) log
⊢ ConcaveOn ℝ (β := ℝ) (Set.Ioi 0.5) fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x)
have hf₂ : ConcaveOn ℝ (β := ℝ) (Set.Ioi 0.5) fun (x : ℝ) ↦ √(2 * x) * log (2 * x)
Tactic: apply ConcaveOn.add
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
⊢ ConcaveOn ℝ (β := ℝ) (Set.Ioi 0.5) fun (x : ℝ) ↦ √(2 * x) * log (2 * x)
have h : Eq (α := Set ℝ) (Set.Ioi 0.5)
  (Set.preimage (β := ℝ) (⇑(HSMul.hSMul (α := ℝ) (β := ℝ →ₗ[ℝ] ℝ) 2 LinearMap.id) : (a : ℝ) → ℝ) (Set.Ioi 1))
Tactic: convert!
        ((strictConcaveOn_sqrt_mul_log_Ioi.concaveOn.comp_linearMap ((2 : ℝ) • LinearMap.id)))
        using 1
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
⊢ Eq (α := Set ℝ) (Set.Ioi 0.5)
    (Set.preimage (β := ℝ) (⇑(HSMul.hSMul (α := ℝ) (β := ℝ →ₗ[ℝ] ℝ) 2 LinearMap.id) : (a : ℝ) → ℝ) (Set.Ioi 1))
have h : ∀ (x : ℝ),
  Membership.mem (γ := Set ℝ) (Set.Ioi 0.5) x ↔
    Membership.mem (γ := Set ℝ)
      (Set.preimage (β := ℝ) (⇑(HSMul.hSMul (α := ℝ) (β := ℝ →ₗ[ℝ] ℝ) 2 LinearMap.id) : (a : ℝ) → ℝ) (Set.Ioi 1)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
x_1 : ℝ
x_large : 512 ≤ x_1
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x_1
x : ℝ
⊢ Membership.mem (γ := Set ℝ) (Set.Ioi 0.5) x ↔
    Membership.mem (γ := Set ℝ)
      (Set.preimage (β := ℝ) (⇑(HSMul.hSMul (α := ℝ) (β := ℝ →ₗ[ℝ] ℝ) 2 LinearMap.id) : (a : ℝ) → ℝ) (Set.Ioi 1)) x
have h : 0.5 < x ↔ 1 < 2 * x
Tactic: simp only [Set.mem_Ioi, Set.mem_preimage, LinearMap.smul_apply,
        LinearMap.id_coe, id_eq, smul_eq_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
x_1 : ℝ
x_large : 512 ≤ x_1
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x_1
x : ℝ
⊢ 0.5 < x ↔ 1 < 2 * x
have h : HMul.hMul (α := ℝ) 2 0.5 < 2 * x ↔ 1 < 2 * x
Tactic: rw [← mul_lt_mul_iff_right₀ (two_pos)]
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
x_1 : ℝ
x_large : 512 ≤ x_1
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x_1
x : ℝ
⊢ HMul.hMul (α := ℝ) 2 0.5 < 2 * x ↔ 1 < 2 * x
have h : 1 < 2 * x ↔ 1 < 2 * x
Tactic: norm_num1
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
⊢ ConvexOn ℝ (E := ℝ) (Set.Ioi 0.5) (HMul.hMul (log 4 / 3))
have hg : 0 ≤ log 4 / 3
Tactic: apply ConvexOn.smul
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
hg : 0 ≤ log 4 / 3
⊢ ConvexOn ℝ (E := ℝ) (Set.Ioi 0.5) (HMul.hMul (log 4 / 3))
have hg₁ : ConvexOn ℝ (β := ℝ) (Set.Ioi 0.5) fun (x : ℝ) ↦ x
Tactic: apply ConvexOn.smul
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (hypothesis)
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
⊢ f x ≤ 0
have h : ConcaveOn ℝ (Set.Ioi 0.5) f
Tactic: have h : ConcaveOn ℝ (Set.Ioi 0.5) f := by
    apply ConcaveOn.sub
    · apply ConcaveOn.add
      · exact strictConcaveOn_log_Ioi.concaveOn.subset
          (Set.Ioi_subset_Ioi (by norm_num)) (convex_Ioi 0.5)
      convert!
        ((strictConcaveOn_sqrt_mul_log_Ioi.concaveOn.comp_linearMap ((2 : ℝ) • LinearMap.id)))
        using 1
      ext x
      simp only [Set.mem_Ioi, Set.mem_preimage, LinearMap.smul_apply,
        LinearMap.id_coe, id_eq, smul_eq_mul]
      rw [← mul_lt_mul_iff_right₀ (two_pos)]
      norm_num1
      rfl
    apply ConvexOn.smul
    · refine div_nonneg (log_nonneg (by norm_num1)) (by norm_num1)
    · exact convexOn_id (convex_Ioi (0.5 : ℝ))
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
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
have obtain : ∀ (x1 x2 : ℝ) (h1 : 0.5 < x1) (h2 : x1 < x2) (h0 : x2 ≤ x) (h3 : 0 ≤ f x1) (h4 : f x2 ≤ 0), f x ≤ 0
Tactic: obtain ⟨x1, x2, h1, h2, h0, h3, h4⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ f x ≤ 0
have suffices : ∃ (x1 : ℝ) (x2 : ℝ), 0.5 < x1 ∧ x1 < x2 ∧ x2 ≤ x ∧ 0 ≤ f x1 ∧ f x2 ≤ 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
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
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
have refine_1 : 0 ≤ f 18
Tactic: refine ⟨18, 512, by norm_num1, by norm_num1, x_large, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
refine_1 : 0 ≤ f 18
⊢ ∃ (x1 : ℝ) (x2 : ℝ), 0.5 < x1 ∧ x1 < x2 ∧ x2 ≤ x ∧ 0 ≤ f x1 ∧ f x2 ≤ 0
have refine_2 : f 512 ≤ 0
Tactic: refine ⟨18, 512, by norm_num1, by norm_num1, x_large, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (hypothesis)
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ 0 ≤ f 18
have this : √(HMul.hMul (α := ℝ) 2 18) = 6
Tactic: have : √(2 * 18 : ℝ) = 6 := (sqrt_eq_iff_mul_self_eq_of_pos (by norm_num1)).mpr (by norm_num1)
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(HMul.hMul (α := ℝ) 2 18) = 6
⊢ 0 ≤ f 18
have refine_1 : HPow.hPow (α := ℝ) 4 (18 / 3) ≤ 18 * HPow.hPow (β := ℝ) (HMul.hMul (α := ℝ) 2 18) 6
Tactic: rw [hf _ (by norm_num1), log_nonneg_iff (by positivity), this, one_le_div (by norm_num1)]
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (hypothesis)
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ f 512 ≤ 0
have this : √(HMul.hMul (α := ℝ) 2 512) = 32
Tactic: have : √(2 * 512) = 32 :=
      (sqrt_eq_iff_mul_self_eq_of_pos (by norm_num1)).mpr (by norm_num1)