filter_upwards_within

Stream: Is there code for X?

[Alex Kontorovich]

Suppose I have some props P Q : ℝ → Prop and a hypothesis h : ∀ᶠ (c : ℝ) in 𝓝[>]0, P c, and I'm trying to prove the goal

⊢ ∀ᶠ (c : ℝ) in 𝓝[>]0, Q c

I can filter_upwards [h] and it will change the goal to

⊢ ∀ (c : ℝ), P c → Q c

But I want it to change the goal to

⊢ ∀ (c : ℝ), 0 < c → P c → Q c

Is there a way to filter_upwards within a filter? Thanks!

[Eric Rodriguez]

I think you need to use the right lemma for nhds_within, which will be the Eventually statement that 0 < c for all c eventually in the nhds

[Alex Kontorovich]

but how do I filter_upwards with that at the same time?

[Eric Rodriguez]

[h, that_lemma]

[Eric Rodriguez]

I think there's also some way to intro automatically too

[Eric Rodriguez]

Should be in the docs

[Alex Kontorovich]

Got it, thanks!

[Eric Rodriguez]

This simple behaviour is how I came to love filter upwards, because it means you can do (for example) common epsilon delta arguments that require a max in a (to me) much more clear way

[Eric Rodriguez]

Anyways, I digress

[Anatole Dedecker]

Eric Rodriguez said:

This simple behaviour is how I came to love filter upwards, because it means you can do (for example) common epsilon delta arguments that require a max in a (to me) much more clear way

Indeed this is the whole point!

[Yury G. Kudryashov]

The lemma is self_mem_nhdsWithin

[Eric Rodriguez]

I was trying to find a good example where stuff is written in a terrible max sort of way, but could be written in a better way if we had better-looking filter bases (#9258). I am trying to do some thinking, because I think this could legitimately be a much better way to do these sorts of arguments (for teaching, even - we really can make "choose N large such that P N , Q N and T N" rigorous in such a better and more intuitive way!)

[Patrick Massot]

I don’t understand why you say this requires #9258. This issue is very specific. We already have very usable filter bases. And really the reason why you will never convince anyone in the real world is that you are trying to replace non-proofs. There is nothing you can do to be more efficient than not proving something.

[Eric Rodriguez]

How would you simulate this theorem? I do not know how using this is a non-proof - I think it's much much better than Metric.tendsto_nhds

theorem Metric.tendsto_nhds' {f : Filter β} {u : β → α} {a : α} :
    Tendsto u f (𝓝 a) ↔ ∀ᶠ ε in 𝓝[>] 0, ∀ᶠ x in f, dist (u x) a < ε`

[Anatole Dedecker]

I don’t see #9258 as something that we need to be proficient with filter bases, the current situation is already very good. Typically, we have everything necessary for "Choose N large enough such that…". It’s more a potential exploration direction, in the same way that we came up (I think?) with docs#Filter.smallSets

[Eric Rodriguez]

What's the issue/intuition behind smallSets?

[Yury G. Kudryashov]

∀ᶠ s in (𝓝 a).smallSets, p s means that p is true for subsets of suffiiciently small nhds of a.

[Yury G. Kudryashov]

We have docs#Filter.Tendsto.Icc that says (in one of the cases) that if f → a and g → a, then the whole interval [f x, g x] is contained in a small nhd of a, a.k.a. sandwich lemma.