-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem intervalIntegrable_log' : IntervalIntegrable log volume a b

Proof state:
case h₂f.hab.h.hpos
a b x : ℝ
hx : 0 < x
s : ℝ
hs₁ : 0 < s
hs₂ : s < 1
⊢ log s ≤ 0

Tactic:
exact (log_nonpos_iff hs₁.le).mpr hs₂.le

Result:
no goals

Proof state:
case h₂f.hab.h
a b x : ℝ
hx : 0 < x
⊢ IntervalIntegrable (-log) volume 0 1

Tactic:
apply intervalIntegrable_deriv_of_nonneg (g := fun x ↦ -(x * log x - x))

Result:
case h₂f.hab.h.hcont
a b x : ℝ
hx : 0 < x
⊢ ContinuousOn (fun x => -(x * log x - x)) [[0, 1]]

case h₂f.hab.h.hderiv
a b x : ℝ
hx : 0 < x
⊢ ∀ x ∈ Set.Ioo (0 ⊓ 1) (0 ⊔ 1), HasDerivAt (fun x => -(x * log x - x)) ((-log) x) x

case h₂f.hab.h.hpos
a b x : ℝ
hx : 0 < x
⊢ ∀ x ∈ Set.Ioo (0 ⊓ 1) (0 ⊔ 1), 0 ≤ (-log) x

Proof state:
case h₂f
a b x : ℝ
hx : 0 < x
⊢ IntervalIntegrable log volume 0 x

Tactic:
apply IntervalIntegrable.trans (b := 1)

Result:
case h₂f.hab
a b x : ℝ
hx : 0 < x
⊢ IntervalIntegrable log volume 0 1

case h₂f.hbc
a b x : ℝ
hx : 0 < x
⊢ IntervalIntegrable log volume 1 x

Proof state:
case h₂f.hab.h.hderiv
a b x : ℝ
hx : 0 < x
s : ℝ
hs : 0 < s
right✝ : s < 1
⊢ HasDerivAt (fun x => x - x * log x) (-log s) s

Tactic:
simpa using (hasDerivAt_id s).sub (hasDerivAt_mul_log hs.ne.symm)

Result:
no goals

Proof state:
case h₂f.hbc.hu
a b x : ℝ
hx✝ : 0 < x
hx : 0 ∉ [[1, x]]
⊢ [[1, x]] ⊆ {0}ᶜ

Tactic:
simpa

Result:
no goals

Proof state:
case h₂f.hbc
a b x : ℝ
hx : 0 < x
⊢ IntervalIntegrable log volume 1 x

Tactic:
apply ContinuousOn.intervalIntegrable

Result:
case h₂f.hbc.hu
a b x : ℝ
hx : 0 < x
⊢ ContinuousOn log [[1, x]]

Proof state:
case h₂f.hab.h.hcont
a b x : ℝ
hx : 0 < x
⊢ ContinuousOn (fun x => -(x * log x - x)) [[0, 1]]

Tactic:
exact (continuous_mul_log.continuousOn.sub continuous_id.continuousOn).neg

Result:
no goals

Proof state:
case h₂f.hbc.hu
a b x : ℝ
hx : 0 < x
⊢ ContinuousOn log [[1, x]]

Tactic:
apply Real.continuousOn_log.mono

Result:
case h₂f.hbc.hu
a b x : ℝ
hx : 0 < x
⊢ [[1, x]] ⊆ {0}ᶜ

Proof state:
case h₂f.hab.h.hpos
a b x : ℝ
hx : 0 < x
s : ℝ
hs₁ : 0 ⊓ 1 < s
hs₂ : s < 0 ⊔ 1
⊢ 0 ≤ (-log) s

Tactic:
norm_num at *

Result:
case h₂f.hab.h.hpos
a b x : ℝ
hx : 0 < x
s : ℝ
hs₁ : 0 < s
hs₂ : s < 1
⊢ log s ≤ 0

Proof state:
case h₂f.hab
a b x : ℝ
hx : 0 < x
⊢ IntervalIntegrable (- -log) volume 0 1

Tactic:
apply IntervalIntegrable.neg

Result:
case h₂f.hab.h
a b x : ℝ
hx : 0 < x
⊢ IntervalIntegrable (-log) volume 0 1

Proof state:
case h₂f.hab
a b x : ℝ
hx : 0 < x
⊢ IntervalIntegrable log volume 0 1

Tactic:
rw [← neg_neg log]

Result:
case h₂f.hab
a b x : ℝ
hx : 0 < x
⊢ IntervalIntegrable (- -log) volume 0 1

Proof state:
case h₂f.hab.h.hpos
a b x : ℝ
hx : 0 < x
⊢ ∀ x ∈ Set.Ioo (0 ⊓ 1) (0 ⊔ 1), 0 ≤ (-log) x

Tactic:
intro s ⟨hs₁, hs₂⟩

Result:
case h₂f.hab.h.hpos
a b x : ℝ
hx : 0 < x
s : ℝ
hs₁ : 0 ⊓ 1 < s
hs₂ : s < 0 ⊔ 1
⊢ 0 ≤ (-log) s

Proof state:
case h₂f.hab.h.hderiv
a b x : ℝ
hx : 0 < x
s : ℝ
hs : 0 ⊓ 1 < s
right✝ : s < 0 ⊔ 1
⊢ HasDerivAt (fun x => -(x * log x - x)) ((-log) s) s

Tactic:
norm_num at *

Result:
case h₂f.hab.h.hderiv
a b x : ℝ
hx : 0 < x
s : ℝ
hs : 0 < s
right✝ : s < 1
⊢ HasDerivAt (fun x => x - x * log x) (-log s) s

Proof state:
case h₂f
a b : ℝ
⊢ ∀ (x : ℝ), 0 < x → IntervalIntegrable log volume 0 x

Tactic:
intro x hx

Result:
case h₂f
a b x : ℝ
hx : 0 < x
⊢ IntervalIntegrable log volume 0 x

Proof state:
case h₂f.hbc.hu
a b x : ℝ
hx : 0 < x
⊢ [[1, x]] ⊆ {0}ᶜ

Tactic:
apply Set.not_mem_uIcc_of_lt zero_lt_one at hx

Result:
case h₂f.hbc.hu
a b x : ℝ
hx✝ : 0 < x
hx : 0 ∉ [[1, x]]
⊢ [[1, x]] ⊆ {0}ᶜ

Proof state:
case h₂f.hab.h.hderiv
a b x : ℝ
hx : 0 < x
⊢ ∀ x ∈ Set.Ioo (0 ⊓ 1) (0 ⊔ 1), HasDerivAt (fun x => -(x * log x - x)) ((-log) x) x

Tactic:
intro s ⟨hs, _⟩

Result:
case h₂f.hab.h.hderiv
a b x : ℝ
hx : 0 < x
s : ℝ
hs : 0 ⊓ 1 < s
right✝ : s < 0 ⊔ 1
⊢ HasDerivAt (fun x => -(x * log x - x)) ((-log) s) s