kebekus/nevanlinna
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update specialFunctions_Integral_log_sin.lean

Browse Source
This commit is contained in:
Stefan Kebekus 2025-01-03 20:08:33 +01:00
parent 6329e081a3
commit 9341f6a24f
1 changed files with 2 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Nevanlinna/specialFunctions_Integral_log_sin.lean
View File

@ -105,6 +105,8 @@ lemma intervalIntegrable_log_sin₁ : IntervalIntegrable (log ∘ sin) volume 0
have int_log : IntervalIntegrable (fun x ↦ ‖log x‖) volume 0 1 := by have int_log : IntervalIntegrable (fun x ↦ ‖log x‖) volume 0 1 := by
apply IntervalIntegrable.norm apply IntervalIntegrable.norm
-- Extract lemma here: log is integrable on [0, 1], and in fact on any
-- interval [a, b]
rw [← neg_neg log] rw [← neg_neg log]
apply IntervalIntegrable.neg apply IntervalIntegrable.neg
apply intervalIntegrable_deriv_of_nonneg (g := fun x ↦ -(x * log x - x)) apply intervalIntegrable_deriv_of_nonneg (g := fun x ↦ -(x * log x - x))