internlm/Lean-Github huggingface dataset:
Theorem: MellinOf1
Proof state before:
case h.e'_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
s : ℂ
h : s.re > 0
⊢ ∀ᵐ (x : ℝ),
    x ∈ Ioi 0 →
      (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) x * ↑x ^ (s - 1) = ↑x ^ (s - 1) • (Ioc 0 1).indicator (fun x => 1) x
Tactic:
filter_upwards with _ _
Proof state after:
case h.e'_2.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
s : ℂ
h : s.re > 0
a✝¹ : ℝ
a✝ : a✝¹ ∈ Ioi 0
⊢ (if 0 < a✝¹ ∧ a✝¹ ≤ 1 then 1 else 0) * ↑a✝¹ ^ (s - 1) = ↑a✝¹ ^ (s - 1) • (Ioc 0 1).indicator (fun x => 1) a✝¹
Theorem: MellinOf1
Proof state before:
case h.e'_2.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
s : ℂ
h : s.re > 0
a✝¹ : ℝ
a✝ : a✝¹ ∈ Ioi 0
⊢ (if 0 < a✝¹ ∧ a✝¹ ≤ 1 then 1 else 0) * ↑a✝¹ ^ (s - 1) = ↑a✝¹ ^ (s - 1) • (Ioc 0 1).indicator (fun x => 1) a✝¹
Tactic:
rw [smul_eq_mul, mul_comm]
Proof state after:
case h.e'_2.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
s : ℂ
h : s.re > 0
a✝¹ : ℝ
a✝ : a✝¹ ∈ Ioi 0
⊢ (↑a✝¹ ^ (s - 1) * if 0 < a✝¹ ∧ a✝¹ ≤ 1 then 1 else 0) = ↑a✝¹ ^ (s - 1) * (Ioc 0 1).indicator (fun x => 1) a✝¹
Theorem: MellinOf1
Proof state before:
case h.e'_2.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
s : ℂ
h : s.re > 0
a✝¹ : ℝ
a✝ : a✝¹ ∈ Ioi 0
⊢ (↑a✝¹ ^ (s - 1) * if 0 < a✝¹ ∧ a✝¹ ≤ 1 then 1 else 0) = ↑a✝¹ ^ (s - 1) * (Ioc 0 1).indicator (fun x => 1) a✝¹
Tactic:
congr
Proof state after:
no goals
Theorem: Smooth1Properties_estimate
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
⊢ (1 - 2 ^ (-ε)) / ε < Real.log 2
Tactic:
apply (div_lt_iff' εpos).mpr
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
⊢ 1 - 2 ^ (-ε) < ε * Real.log 2
Theorem: Smooth1Properties_estimate
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
⊢ 1 - 2 ^ (-ε) < ε * Real.log 2
Tactic:
have : 1 - 1 / (2 : ℝ) ^ ε = ((2 : ℝ) ^ ε - 1) / (2 : ℝ) ^ ε := by
  rw [sub_div, div_self (by positivity)]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
this : 1 - 1 / 2 ^ ε = (2 ^ ε - 1) / 2 ^ ε
⊢ 1 - 2 ^ (-ε) < ε * Real.log 2
Theorem: Smooth1Properties_estimate
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
this : 1 - 1 / 2 ^ ε = (2 ^ ε - 1) / 2 ^ ε
⊢ 1 - 2 ^ (-ε) < ε * Real.log 2
Tactic:
rw [← Real.log_rpow (by norm_num), rpow_neg (by norm_num), inv_eq_one_div (2 ^ ε), this]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
this : 1 - 1 / 2 ^ ε = (2 ^ ε - 1) / 2 ^ ε
⊢ (2 ^ ε - 1) / 2 ^ ε < (2 ^ ε).log
Theorem: Smooth1Properties_estimate
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
this : 1 - 1 / 2 ^ ε = (2 ^ ε - 1) / 2 ^ ε
⊢ (2 ^ ε - 1) / 2 ^ ε < (2 ^ ε).log
Tactic:
set c := (2 : ℝ) ^ ε
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
⊢ (c - 1) / c < c.log
Theorem: Smooth1Properties_estimate
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
⊢ (c - 1) / c < c.log
Tactic:
have hc : 1 < c := by
  rw [← rpow_zero (2 : ℝ)]
  apply Real.rpow_lt_rpow_of_exponent_lt (by norm_num) εpos
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
⊢ (c - 1) / c < c.log
Theorem: Smooth1Properties_estimate
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
⊢ (c - 1) / c < c.log
Tactic:
apply (div_lt_iff' (by positivity)).mpr <| lt_sub_iff_add_lt'.mp ?_
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
⊢ -1 < c * c.log - c
Theorem: Smooth1Properties_estimate
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
⊢ -1 < c * c.log - c
Tactic:
let f := (fun x ↦ x * Real.log x - x)
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
⊢ -1 < c * c.log - c
Theorem: Smooth1Properties_estimate
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
⊢ -1 < c * c.log - c
Tactic:
rw [(by simp [f] : -1 = f 1), (by simp : c * Real.log c - c = f c)]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
⊢ f 1 < f c
Theorem: Smooth1Properties_estimate
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
mono : StrictMonoOn f (Ici 1)
⊢ f 1 < f c
Tactic:
exact mono (by rw [mem_Ici]) (mem_Ici.mpr <| le_of_lt hc) hc
Proof state after:
no goals
Theorem: Smooth1Properties_estimate
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
⊢ 1 - 1 / 2 ^ ε = (2 ^ ε - 1) / 2 ^ ε
Tactic:
rw [sub_div, div_self (by positivity)]
Proof state after:
no goals
Theorem: Smooth1Properties_estimate
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
⊢ 2 ^ ε ≠ 0
Tactic:
positivity
Proof state after:
no goals
Theorem: Smooth1Properties_estimate
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
this : 1 - 1 / 2 ^ ε = (2 ^ ε - 1) / 2 ^ ε
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Smooth1Properties_estimate
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
this : 1 - 1 / 2 ^ ε = (2 ^ ε - 1) / 2 ^ ε
⊢ 0 ≤ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Smooth1Properties_estimate
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
⊢ 1 < c
Tactic:
rw [← rpow_zero (2 : ℝ)]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
⊢ 2 ^ 0 < c
Theorem: Smooth1Properties_estimate
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
⊢ 2 ^ 0 < c
Tactic:
apply Real.rpow_lt_rpow_of_exponent_lt (by norm_num) εpos
Proof state after:
no goals
Theorem: Smooth1Properties_estimate
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
⊢ 1 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Smooth1Properties_estimate
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
⊢ 0 < c
Tactic:
positivity
Proof state after:
no goals
Theorem: Smooth1Properties_estimate
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
⊢ -1 = f 1
Tactic:
simp [f]
Proof state after:
no goals
Theorem: Smooth1Properties_estimate
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
⊢ c * c.log - c = f c
Tactic:
simp
Proof state after:
no goals
Theorem: Smooth1Properties_estimate
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
⊢ StrictMonoOn f (Ici 1)
Tactic:
refine strictMonoOn_of_deriv_pos (convex_Ici _) ?_ ?_
Proof state after:
case refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
⊢ ContinuousOn f (Ici 1)

case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
⊢ ∀ x ∈ interior (Ici 1), 0 < deriv f x
Theorem: Smooth1Properties_estimate
Proof state before:
case refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
⊢ ContinuousOn f (Ici 1)
Tactic:
apply continuousOn_id.mul (continuousOn_id.log ?_) |>.sub continuousOn_id
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
⊢ ∀ x ∈ Ici 1, id x ≠ 0
Theorem: Smooth1Properties_estimate
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
⊢ ∀ x ∈ Ici 1, id x ≠ 0
Tactic:
intro x hx
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : x ∈ Ici 1
⊢ id x ≠ 0
Theorem: Smooth1Properties_estimate
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : x ∈ Ici 1
⊢ id x ≠ 0
Tactic:
simp only [mem_Ici] at hx
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 ≤ x
⊢ id x ≠ 0
Theorem: Smooth1Properties_estimate
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 ≤ x
⊢ id x ≠ 0
Tactic:
simp only [id_eq, ne_eq]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 ≤ x
⊢ ¬x = 0
Theorem: Smooth1Properties_estimate
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 ≤ x
⊢ ¬x = 0
Tactic:
linarith
Proof state after:
no goals
Theorem: Smooth1Properties_estimate
Proof state before:
case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
⊢ ∀ x ∈ interior (Ici 1), 0 < deriv f x
Tactic:
intro x hx
Proof state after:
case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : x ∈ interior (Ici 1)
⊢ 0 < deriv f x
Theorem: Smooth1Properties_estimate
Proof state before:
case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : x ∈ interior (Ici 1)
⊢ 0 < deriv f x
Tactic:
simp only [nonempty_Iio, interior_Ici', mem_Ioi] at hx
Proof state after:
case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ 0 < deriv f x
Theorem: Smooth1Properties_estimate
Proof state before:
case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ 0 < deriv f x
Tactic:
dsimp only [f]
Proof state after:
case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ 0 < deriv (fun x => x * x.log - x) x
Theorem: Smooth1Properties_estimate
Proof state before:
case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ 0 < deriv (fun x => x * x.log - x) x
Tactic:
rw [deriv_sub, deriv_mul, deriv_log, deriv_id'', one_mul, mul_inv_cancel]
Proof state after:
case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ 0 < x.log + 1 - (fun x => 1) x

case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ x ≠ 0

case refine_2.hc
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x) x

case refine_2.hd
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x.log) x

case refine_2.hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x * x.log) x

case refine_2.hg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x) x
Theorem: Smooth1Properties_estimate
Proof state before:
case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ 0 < x.log + 1 - (fun x => 1) x

case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ x ≠ 0

case refine_2.hc
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x) x

case refine_2.hd
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x.log) x

case refine_2.hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x * x.log) x

case refine_2.hg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x) x
Tactic:
simp
Proof state after:
case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ 0 < x.log

case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ x ≠ 0

case refine_2.hc
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x) x

case refine_2.hd
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x.log) x

case refine_2.hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x * x.log) x

case refine_2.hg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x) x
Theorem: Smooth1Properties_estimate
Proof state before:
case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ 0 < x.log
Tactic:
exact log_pos hx
Proof state after:
no goals
Theorem: Smooth1Properties_estimate
Proof state before:
case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ x ≠ 0
Tactic:
linarith
Proof state after:
no goals
Theorem: Smooth1Properties_estimate
Proof state before:
case refine_2.hc
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x) x
Tactic:
simp only [differentiableAt_id']
Proof state after:
no goals
Theorem: Smooth1Properties_estimate
Proof state before:
case refine_2.hd
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x.log) x
Tactic:
simp only [differentiableAt_log_iff, ne_eq]
Proof state after:
case refine_2.hd
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ ¬x = 0
Theorem: Smooth1Properties_estimate
Proof state before:
case refine_2.hd
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ ¬x = 0
Tactic:
linarith
Proof state after:
no goals
Theorem: Smooth1Properties_estimate
Proof state before:
case refine_2.hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x * x.log) x
Tactic:
exact differentiableAt_id'.mul <| differentiableAt_id'.log (by linarith)
Proof state after:
no goals
Theorem: Smooth1Properties_estimate
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ x ≠ 0
Tactic:
linarith
Proof state after:
no goals
Theorem: Smooth1Properties_estimate
Proof state before:
case refine_2.hg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x) x
Tactic:
simp only [differentiableAt_id']
Proof state after:
no goals
Theorem: Smooth1Properties_estimate
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
mono : StrictMonoOn f (Ici 1)
⊢ 1 ∈ Ici 1
Tactic:
rw [mem_Ici]
Proof state after:
no goals
Theorem: Smooth1Properties_below_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : x ≤ 1 - Real.log 2 * ε
εpos : 0 < ε
⊢ x < 2 ^ (-ε)
Tactic:
calc
  x ≤ 1 - Real.log 2 * ε := hx
  _ < 2 ^ (-ε) := ?_
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : x ≤ 1 - Real.log 2 * ε
εpos : 0 < ε
⊢ 1 - Real.log 2 * ε < 2 ^ (-ε)
Theorem: Smooth1Properties_below_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : x ≤ 1 - Real.log 2 * ε
εpos : 0 < ε
⊢ 1 - Real.log 2 * ε < 2 ^ (-ε)
Tactic:
rw [sub_lt_iff_lt_add, add_comm, ← sub_lt_iff_lt_add]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : x ≤ 1 - Real.log 2 * ε
εpos : 0 < ε
⊢ 1 - 2 ^ (-ε) < Real.log 2 * ε
Theorem: Smooth1Properties_below_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : x ≤ 1 - Real.log 2 * ε
εpos : 0 < ε
⊢ 1 - 2 ^ (-ε) < Real.log 2 * ε
Tactic:
exact (div_lt_iff εpos).mp <| Smooth1Properties_estimate εpos
Proof state after:
no goals
Theorem: Smooth1Properties_below
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ ∃ c, 0 < c ∧ ∀ (x : ℝ), 0 < x → x ≤ 1 - c * ε → Smooth1 Ψ ε x = 1
Tactic:
set c := Real.log 2
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
⊢ ∃ c, 0 < c ∧ ∀ (x : ℝ), 0 < x → x ≤ 1 - c * ε → Smooth1 Ψ ε x = 1
Theorem: Smooth1Properties_below
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
⊢ ∃ c, 0 < c ∧ ∀ (x : ℝ), 0 < x → x ≤ 1 - c * ε → Smooth1 Ψ ε x = 1
Tactic:
use c
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
⊢ 0 < c ∧ ∀ (x : ℝ), 0 < x → x ≤ 1 - c * ε → Smooth1 Ψ ε x = 1
Theorem: Smooth1Properties_below
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
⊢ 0 < c ∧ ∀ (x : ℝ), 0 < x → x ≤ 1 - c * ε → Smooth1 Ψ ε x = 1
Tactic:
constructor
Proof state after:
case h.left
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
⊢ 0 < c

case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
⊢ ∀ (x : ℝ), 0 < x → x ≤ 1 - c * ε → Smooth1 Ψ ε x = 1
Theorem: Smooth1Properties_below
Proof state before:
case h.left
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
⊢ 0 < c

case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
⊢ ∀ (x : ℝ), 0 < x → x ≤ 1 - c * ε → Smooth1 Ψ ε x = 1
Tactic:
exact log_pos (by norm_num)
Proof state after:
case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
⊢ ∀ (x : ℝ), 0 < x → x ≤ 1 - c * ε → Smooth1 Ψ ε x = 1
Theorem: Smooth1Properties_below
Proof state before:
case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
⊢ ∀ (x : ℝ), 0 < x → x ≤ 1 - c * ε → Smooth1 Ψ ε x = 1
Tactic:
intro x xpos hx
Proof state after:
case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
⊢ Smooth1 Ψ ε x = 1
Theorem: Smooth1Properties_below
Proof state before:
case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
⊢ Smooth1 Ψ ε x = 1
Tactic:
have hx2 := Smooth1Properties_below_aux hx εpos
Proof state after:
case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ Smooth1 Ψ ε x = 1