>>458

0≦t≦1 とする。
　f(t) = (1/2)log(1+t^2) + log(1/√2)･t,
とおくと
　f(0) = f(1) = 0,
　f "(t) = (1-t^2)/(1+t^2)^2 ≧0,
　f(t) ≦ 0　　　　　　　　　　　　(0≦t≦1)
t=tanθ とおいて
　log(cosθ) ≧ tanθ･log(1/√2),
cos(x) >0 を掛けて
　cosθ･log(cosθ) ≧ sinθ･log(1/√2) ≧ sinθ･log(sinθ),　(0<θ≦π/4)