x^r * log x near zero

Stream: new members

[Adomas Baliuka]

In Lean, rpow x y is defined for negative x as exp (y log x) cos (π y) (according to docs). There is the lemma tendsto_log_mul_rpow_nhds_zero, which says that $x^r \log x$ for positive $r$ approaches zero fom above (if I understand filters correctly, which didn't feature in my math lectures). However, given that Real.log is defined as $\log |x|$ (and zero at zero), it seems to me that tendsto_log_mul_rpow_nhds_zero shouldn't need the restriction on the filter and that one could prove r > 0 -> Continuous Real fun x => log x * rpow x r. Am I missing something?