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

Update mathlib

Browse Source
This commit is contained in:
Stefan Kebekus
2024-10-31 07:37:54 +01:00
parent 279dcd32b9
commit 449de2e42a
2 changed files with 4 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
Nevanlinna/specialFunctions_Integral_log_sin.lean
View File

@@ -24,7 +24,7 @@ lemma logsinBound : ∀ x ∈ (Set.Icc 0 1), ‖(log ∘ sin) x‖ ≤ ‖log ((
exact zero_lt_two
apply (Set.mem_Icc.1 hx).1
simp
apply mul_le_one
apply mul_le_one₀
rw [div_le_one pi_pos]
exact two_le_pi
exact (Set.mem_Icc.1 hx).1