Rewrite within Filter.Eventually

Stream: mathlib4

[Enrico Borba]

How can I apply a hypothesis within a Filter.Eventually? Specifically,

import Mathlib

open Topology Filter

theorem eventuallyEq_abs_atTop (f : ℕ → ℝ) (hf : Tendsto f atTop (𝓝 2)) :
    ∀ᶠ x in atTop, |f x| = f x := by
  have : ∀ᶠ x in atTop, 0 ≤ f x := eventually_ge_of_tendsto_gt two_pos hf
  sorry

I'm not sure how to proceed here. I feel like I should be able to use docs#abs_of_nonneg, but I can't quite place it. Still trying to get used to filters.

[Patrick Massot]

In your very simple case simpa using this will probably be enough. But a more general next step would be apply this.mono.

[Yury G. Kudryashov]

Or filter_upwards

[Yury G. Kudryashov]

It would be nice to make simp (config := {contextual := true}) do more inside Filter.Eventually but I'm not sure what's the right way to implement this. E.g., if you have ∀ x, ∀ᶠ y in atTop, f x y = g x y, then you can't use it inside another Filter.Eventually/Filter.Frequently for more than finitely many values of x (or countably many, if it's a filter like Measure.ae).

[Kyle Miller]

There's seems to be a bug in the peel tactic, but this could be a use of it.

theorem eventually_imp {α : Type*} {p q : α → Prop} {f : Filter α}
    (hq : ∀ (x : α), p x → q x) (hp : ∀ᶠ (x : α) in f, p x) : ∀ᶠ (x : α) in f, q x :=
  Filter.Eventually.mp hp (Filter.eventually_of_forall hq)

theorem eventuallyEq_abs_atTop (f : ℕ → ℝ) (hf : Tendsto f atTop (𝓝 2)) :
    ∀ᶠ x in atTop, |f x| = f x := by
  have : ∀ᶠ x in atTop, 0 ≤ f x := eventually_ge_of_tendsto_gt two_pos hf
  refine eventually_imp (fun x h => ?_) this -- should be `peel this with x h`
  rwa [abs_eq_self]

(@Jireh Loreaux I'm not sure what the bug is. It seems like it might be because of mdata, but there's nothing in the code that pops out as being the culprit.)

[Kyle Miller]

(eventually_imp isn't necessary, it's hp.mono hq, but I was just copying implementation from peel)

[Yury G. Kudryashov]

What if I have several Eventually assumptions? Do I have to and all of them first?

[Jireh Loreaux]

@Kyle Miller I'll try to have a look tonight, but no promises.

[Kyle Miller]

@Yury G. Kudryashov peel only works with a single hypothesis, but if you can and them together (and merge quantifiers) then I suppose you could use it here

[Enrico Borba]

Patrick Massot said:

In your very simple case simpa using this will probably be enough. But a more general next step would be apply this.mono.

This is indeed what I was looking for, thanks!

[Mario Carneiro]

isn't this what the filter_upwards tactic is for?

[Yury G. Kudryashov]

With filter_upwards, you can prove some goal, but you can't use one Filter.Eventually to simplify another.

[Yury G. Kudryashov]

Or use an a.e. equality to rewrite inside an integral (without constructing a very specific a.e. equality).

[Yury G. Kudryashov]

E.g., if you know that f is a.e. equal to g, then you can't simplify integral of fun x => (f x)^2 - (g x)^2 to zero.