Rewrite "within" in Tendsto nhdsWithin

Stream: new members

[Adomas Baliuka]

I want to prove

import Mathlib

open Real Filter Classical Set Topology

lemma tendsto_abs_logx_rpow {r : ℝ} (hr: 0 < r)
: Tendsto (fun x => |log x| * |x| ^ r) (𝓝[>] 0) (𝓝 0) := by
    sorry

I want to "rewrite" using the fact that I only care about x > 0. So I want to do something like rw and reduce the goal to Tendsto (fun x => |log x| * x ^ r) (𝓝[>] 0) (𝓝 0). Then, I want to do a by-cases analysis of x < 1 or x > 1, which removes the absolute value around log. Then the rest follows from tendsto_log_mul_rpow_nhds_zero.

I didn't find a way to do this "rewrite". Is the following theorem true? I was looking for something like that. I also didn't find anything looking for "eventually equal" (a lemma that might be called "tendsto_nhdsWithin_of_eventuallyEqual").

lemma tendstoNhdsWithin_of_eq_within
    {f g : ℝ → ℝ} {l : ℝ} {S : Set ℝ} {x : ℝ}
    (eq_within : ∀x∈S, f x = g x)
    (tenF : Tendsto g (𝓝[S] x) (𝓝 l))
    : Tendsto f (𝓝[S] x) (𝓝 l) := by
    sorry

Maybe this isn't the idiomatic approach?

[Patrick Massot]

That second lemma isn't true. The eq_within assumption isn't strong enough.

[Eric Wieser]

docs#Filter.Tendsto.congr' might be what you're looking for?

[Patrick Massot]

Sorry, I got interrupted by a student question. Yes, the lemma that Eric pointed out is the main relevant lemma.

[Eric Wieser]

This works:

lemma tendstoNhdsWithin_of_eq_within
    {f g : ℝ → ℝ} {l : ℝ} {S : Set ℝ} {x : ℝ}
    (eq_within : ∀x∈S, f x = g x)
    (tenF : Tendsto g (𝓝[S] x) (𝓝 l)) :
    Tendsto f (𝓝[S] x) (𝓝 l) :=
  tenF.congr' (Set.EqOn.symm eq_within).eventuallyEq_nhdsWithin

[Adomas Baliuka]

Patrick Massot said:

That second lemma isn't true. The eq_within assumption isn't strong enough.

Which lemma isn't true? Eric Wieser proved what I would have called "the second lemma" from my post.

[Eric Wieser]

Which seems to contradict Patrick's claim that it's false: perhaps this was fixed in an edit that Zulip is not loading for me; or maybe there's a junk value coming into play somewhere

[Patrick Massot]

Sorry, I read your lemma too quickly. I shouldn't try to answer questions on Zulip and questions from students in parallel.

[Patrick Massot]

I think I was misled by the surrounding text and this influenced my reading of the Lean code. Why did you discuss splitting depending on x < 1?

[Adomas Baliuka]

It's not really splitting I guess, it's just saying "wlog x < 1". I want to use it to remove the absolute value around the log. (Will post solution later if I manage to get it)

[Jireh Loreaux]

I think you just want to apply docs#squeeze_zero_norm'

[Jireh Loreaux]

oh, or even just docs#Filter.Tendsto.norm, which makes more sense

[Adomas Baliuka]

Thanks! As an aside, I just saw squeeze_one_norm' (and squeeze_zero_norm', which have the same docstring, which might be a typo?). I'm really confused why squeeze_one_norm' is true (must be misunderstanding it). Maybe I'll have to learn filters properly after all

[Jireh Loreaux]

Yes, the docstring should be fixed. Note the difference between SeminormedGroup and SeminormedAddGroup.

[Adomas Baliuka]

Can/should one PR individual small doc typos like this?

[Jireh Loreaux]

Yes, definitely. You can mark it as easy.

[Jireh Loreaux]

import Mathlib

open Real Filter Classical Set Topology

lemma tendsto_abs_logx_rpow {r : ℝ} (hr: 0 < r) :
    Tendsto (fun x => |log x| * |x| ^ r) (𝓝[>] 0) (𝓝 0) := by
  convert (tendsto_log_mul_rpow_nhds_zero hr).norm.congr' ?_
  · simp
  · filter_upwards [self_mem_nhdsWithin] with x hx
    simp_rw [norm_mul, norm_rpow_of_nonneg (mem_Ioi.mp hx).le, norm_eq_abs]

[Patrick Massot]

I'm sorry I keep being interrupted, but I'm in office hours. Closer to the intended proof is:

import Mathlib

open Real Filter Classical Set Topology

lemma tendsto_abs_logx_rpow {r : ℝ} (hr: 0 < r) :
    Tendsto (fun x ↦ |log x| * |x| ^ r) (𝓝[>] 0) (𝓝 0) := by
  suffices Tendsto (fun x ↦ -log x * x ^ r) (𝓝[>] 0) (𝓝 0) by
    apply this.congr'
    rw [eventuallyEq_nhdsWithin_iff]
    have : Ioo (-1) 1 ∈  𝓝 (0 : ℝ) := by
      apply Ioo_mem_nhds <;> norm_num
    apply mem_of_superset this
    rintro x ⟨-, hx⟩ (hx' : 0 < x)
    rw [abs_of_pos hx', abs_of_neg (log_neg hx' hx)]
  convert (tendsto_log_mul_rpow_nhds_zero hr).neg using 1
  simp

I hope this will be useful for future proofs.

[Adomas Baliuka]

Wow, thanks a lot! I didn't even ask for the proof of this :)

[Adomas Baliuka]

Oh, the reason for that "typo" is actually that squeeze_zero_norm' is auto-generated by to_additive. I guess it's fine then

[Riccardo Brasca]

You can still fix the docstring!

[Adomas Baliuka]

You mean write it so it matches both cases? Or is there some trick to customize to_additive?

[Riccardo Brasca]

@[to_additive "blah blah"]

[Patrick Massot]

There is already a hand-written docstring there, but it's wrong.

[Adomas Baliuka]

I made a PR