log over rpow

Stream: Is there code for X?

[Bhavik Mehta]

example {ε : ℝ} (hε : 0 < ε) :
  tendsto (λ x : ℝ, (log (log x) * log x / x ^ ε)) at_top (𝓝 0) :=
begin

end

What's the easiest way to show this?

[Yaël Dillies]

What about breaking x ^ ε into x ^ (ε/2) * x ^ (ε/2) and then use log x / x ^ (ε/2) tends to 0 (and log (log x) ≤ log x)?

[Bhavik Mehta]

Yeah that's what I have right now but it feels like there should be a better way than splitting the rpow up into two

[Yaël Dillies]

Not sure.. You can't really bound log (log x) by anything else than log x here.

[Sebastien Gouezel]

The best way would probably be to convince Manuel Eberl to switch to Lean :-) https://www21.in.tum.de/~eberlm/pubs/diss.html

[Bhavik Mehta]

Here's what I settled on:

lemma log_log_mul_log_div_rpow {ε : ℝ} (hε : 0 < ε) :
  tendsto (λ x : ℝ, log (log x) * log x / x ^ ε) at_top (𝓝 0) :=
begin
  refine is_o.tendsto_div_nhds_zero _,
  refine ((is_o_log_id_at_top.comp_tendsto tendsto_log_at_top).mul_is_O (is_O_refl _ _)).trans _,
  refine ((is_o_log_rpow_at_top (half_pos hε)).pow zero_lt_two).congr' _ _,
  { filter_upwards with x using by simp [sq] },
  filter_upwards [eventually_ge_at_top (0 : ℝ)] with x hx,
  rw [←rpow_two, ←rpow_mul hx, div_mul_cancel ε two_ne_zero],
end

[Yaël Dillies]

That looks short enough! I would just add is_O_rfl to shorten a bit.

[Bhavik Mehta]

Yaël Dillies said:

That looks short enough! I would just add is_O_rfl to shorten a bit.

This doesn't exist

[Yaël Dillies]

Yeah, that's why I would add it.

[Patrick Massot]

Sebastien Gouezel said:

The best way would probably be to convince Manuel Eberl to switch to Lean :-) https://www21.in.tum.de/~eberlm/pubs/diss.html

We've tried that so many times...