antitone function tendsto its liminf

Stream: Is there code for X?

[Bhavik Mehta]

Do we have anything like this?

import Mathlib

open ENNReal Filter Topology

lemma tendsto_liminf {f : ℝ≥0∞ → ℝ≥0∞} (hf : Antitone f) :
    Tendsto f (𝓝[>] 0) (𝓝 (liminf f (𝓝[>] 0))) := by
  sorry

I'd be equally happy with the limit expressed as limsup, or as ⨆ r, ⨆ (_ : a < r), f r, but everything I can find is where the filter is atTop, atBot, or nhds.

[Bhavik Mehta]

(deleted)

[Bhavik Mehta]

@loogle Filter.Tendsto, Filter.liminf, Antitone

[loogle]

:shrug: nothing found

[Bhavik Mehta]

My broader context is I have a goal of this shape:

example {f g : ℝ≥0∞ → ℝ≥0∞} {φ ψ : ℕ → ℝ≥0∞}
    (hf : Antitone f) (hg : Antitone g)
    (hφ : Antitone φ) (hφ₀ : ∀ n, 0 < φ n) (hψ : Antitone ψ) (hψ₀ : ∀ n, 0 < ψ n)
    (hφ_lim : Tendsto φ atTop (𝓝[>] 0)) (hψ_lim : Tendsto ψ atTop (𝓝[>] 0))
    (hfg : ∀ n, f (φ n) ≤ g (φ n) + ψ n) :
    ⨆ r, ⨆ (_ : 0 < r), f r ≤ ⨆ r, ⨆ (_ : 0 < r), g r := by
  sorry

where the informal proof should be just "take n big in hfg", but I can't figure out a filter way of doing that nicely

[Bhavik Mehta]

(and in case it's useful, here's my lemma for passing between liminf and iSup2, which I have proved)

lemma iSup₂_eq_liminf {α β : Type*}
    [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α]
    [CompleteLattice β]
    (a : α) (hb : ∃ b, a < b) {f : α → β} (hf : Antitone f) :
    ⨆ r, ⨆ (_ : a < r), f r = Filter.liminf f (𝓝[>] a) := by

[Bhavik Mehta]

Ah! Found it, docs#Antitone.tendsto_nhdsGT was my missing ingredient