internlm/Lean-Github huggingface dataset:
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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
Proof 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
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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
Proof state after:
no goals
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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
Proof state after:
no goals
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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
Proof state after:
no goals
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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)
Proof 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
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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)]
Proof 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
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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
Proof state after:
no goals
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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
Proof state after:
no goals
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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
Proof state after:
no goals
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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
Proof state after:
no goals
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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
Proof state after:
no goals
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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
Proof state after:
no goals
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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)
Proof 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
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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)]
Proof 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)
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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
Proof 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)
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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
Proof 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)
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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]
Proof 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)
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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]
Proof 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)
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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
Proof 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)
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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]
Proof 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
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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
Proof 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
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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
Proof state after:
no goals
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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
Proof state after:
no goals
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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
Proof state after:
no goals
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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
Proof state after:
no goals
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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
Proof state after:
no goals
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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
Proof state after:
no goals
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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
Proof state after:
no goals
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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
Proof state after:
no goals
Theorem: chapter02.Bertrand.real_main_inequality
Proof 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
Proof state after:
no goals
Theorem: chapter02.bertrand_main_inequality
Proof state before:
n : ℕ
n_large : 512 ≤ n
⊢ n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
Tactic:
rw [← @cast_le ℝ]
Proof state after:
n : ℕ
n_large : 512 ≤ n
⊢ ↑(n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)) ≤ ↑(4 ^ n)
Theorem: chapter02.bertrand_main_inequality
Proof state before:
n : ℕ
n_large : 512 ≤ n
⊢ ↑(n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)) ≤ ↑(4 ^ n)
Tactic:
simp only [cast_add, cast_one, cast_mul, cast_pow, ← Real.rpow_natCast]
Proof state after:
n : ℕ
n_large : 512 ≤ n
⊢ ↑n * (↑2 * ↑n) ^ ↑(2 * n).sqrt * ↑4 ^ ↑(2 * n / 3) ≤ ↑4 ^ ↑n
Theorem: chapter02.bertrand_main_inequality
Proof state before:
n : ℕ
n_large : 512 ≤ n
⊢ ↑n * (↑2 * ↑n) ^ ↑(2 * n).sqrt * ↑4 ^ ↑(2 * n / 3) ≤ ↑4 ^ ↑n
Tactic:
refine' _root_.trans ?_ (Bertrand.real_main_inequality (by exact_mod_cast n_large))
Proof state after:
n : ℕ
n_large : 512 ≤ n
⊢ ↑n * (↑2 * ↑n) ^ ↑(2 * n).sqrt * ↑4 ^ ↑(2 * n / 3) ≤ ↑n * (2 * ↑n) ^ (2 * ↑n).sqrt * 4 ^ (2 * ↑n / 3)
Theorem: chapter02.bertrand_main_inequality
Proof state before:
n : ℕ
n_large : 512 ≤ n
⊢ ↑n * (↑2 * ↑n) ^ ↑(2 * n).sqrt * ↑4 ^ ↑(2 * n / 3) ≤ ↑n * (2 * ↑n) ^ (2 * ↑n).sqrt * 4 ^ (2 * ↑n / 3)
Tactic:
gcongr
Proof state after:
case h₁.h.hx
n : ℕ
n_large : 512 ≤ n
⊢ 1 ≤ ↑2 * ↑n

case h₁.h.hyz
n : ℕ
n_large : 512 ≤ n
⊢ ↑(2 * n).sqrt ≤ (2 * ↑n).sqrt

case h₂.hx
n : ℕ
n_large : 512 ≤ n
⊢ 1 ≤ ↑4

case h₂.hyz
n : ℕ
n_large : 512 ≤ n
⊢ ↑(2 * n / 3) ≤ 2 * ↑n / 3
Theorem: chapter02.bertrand_main_inequality
Proof state before:
n : ℕ
n_large : 512 ≤ n
⊢ 512 ≤ ↑n
Tactic:
exact_mod_cast n_large
Proof state after:
no goals
Theorem: chapter02.bertrand_main_inequality
Proof state before:
case h₁.h.hx
n : ℕ
n_large : 512 ≤ n
⊢ 1 ≤ ↑2 * ↑n
Tactic:
have n2_pos : 0 < 2 * n := by positivity
Proof state after:
case h₁.h.hx
n : ℕ
n_large : 512 ≤ n
n2_pos : 0 < 2 * n
⊢ 1 ≤ ↑2 * ↑n
Theorem: chapter02.bertrand_main_inequality
Proof state before:
case h₁.h.hx
n : ℕ
n_large : 512 ≤ n
n2_pos : 0 < 2 * n
⊢ 1 ≤ ↑2 * ↑n
Tactic:
exact mod_cast n2_pos
Proof state after:
no goals
Theorem: chapter02.bertrand_main_inequality
Proof state before:
n : ℕ
n_large : 512 ≤ n
⊢ 0 < 2 * n
Tactic:
positivity
Proof state after:
no goals
Theorem: chapter02.bertrand_main_inequality
Proof state before:
case h₁.h.hyz
n : ℕ
n_large : 512 ≤ n
⊢ ↑(2 * n).sqrt ≤ (2 * ↑n).sqrt
Tactic:
exact_mod_cast Real.nat_sqrt_le_real_sqrt
Proof state after:
no goals
Theorem: chapter02.bertrand_main_inequality
Proof state before:
case h₂.hx
n : ℕ
n_large : 512 ≤ n
⊢ 1 ≤ ↑4
Tactic:
norm_num1
Proof state after:
no goals
Theorem: chapter02.bertrand_main_inequality
Proof state before:
case h₂.hyz
n : ℕ
n_large : 512 ≤ n
⊢ ↑(2 * n / 3) ≤ 2 * ↑n / 3
Tactic:
exact cast_div_le.trans (by norm_cast)
Proof state after:
no goals
Theorem: chapter02.bertrand_main_inequality
Proof state before:
n : ℕ
n_large : 512 ≤ n
⊢ ↑(2 * n) / ↑3 ≤ 2 * ↑n / 3
Tactic:
norm_cast
Proof state after:
no goals
Theorem: chapter02.centralBinom_factorization_small
Proof state before:
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
⊢ n.centralBinom = ∏ p ∈ Finset.range (2 * n / 3 + 1), p ^ n.centralBinom.factorization p
Tactic:
refine' (Eq.trans _ n.prod_pow_factorization_centralBinom).symm
Proof state after:
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
⊢ ∏ p ∈ Finset.range (2 * n / 3 + 1), p ^ n.centralBinom.factorization p =
    ∏ p ∈ Finset.range (2 * n + 1), p ^ n.centralBinom.factorization p