Limits with positive reals and atBot

Stream: new members

[Daniele Pusceddu]

Hello,
I have been working on a project which uses a "Positive Reals" type and I would now like to
work with simple theorem involving limits, in particular "tending to zero from the right" which I believe I may achieve with Filter.atBot. But after browsing around the Mathlib docs for a while, I believe I am stuck. I am here to humbly ask for suggestions in how to prove theorems similar to the ones in the mwe below. Thank you.

import Mathlib.Topology.Basic
import Mathlib.Topology.Instances.Real
import Mathlib.Order.Filter.AtTopBot
import Mathlib.Order.Monotone.Basic

abbrev PReal := { r : ℝ // 0 < r}
notation "ℝ+" => PReal

theorem test1:
  Filter.Tendsto (fun (x: ℝ+) => 1 + x) Filter.atBot (nhds 1)
  := by sorry

-- Additionally "With the limit of f for x leading to 0 from the right being defined"
-- I know `lim` is not recommended but I didn't know how else to state this
theorem test2 (f: ℝ+ → ℝ+) (h1: StrictMono f) (x: ℝ+):
  limUnder Filter.atBot f < f x
  := by sorry

[Patrick Massot]

The ℝ+ notation is really very ambiguous. It could just as well refer to NNReal.

[Patrick Massot]

My first advice is to reconsider whether you really really want this instead of working with reals.

[Daniele Pusceddu]

Patrick Massot said:

My first advice is to reconsider whether you really really want this instead of working with reals.

I invested a bit too much in it already to revert back to reals.

[Patrick Massot]

Here something you can do (but it shows the pain you inflict on yourself with working with PReal):

import Mathlib.Topology.Basic
import Mathlib.Topology.Instances.Real
import Mathlib.Order.Filter.AtTopBot
import Mathlib.Order.Monotone.Basic

abbrev PReal := { r : ℝ // 0 < r}
notation "ℝ>0" => PReal

open Filter Topology

theorem test1: Tendsto (fun x: ℝ>0 => 1 + x) atBot (𝓝 1) := by
  set i : ℝ>0 → ℝ := fun x ↦ x
  set f : ℝ>0 → ℝ>0 := fun x ↦ 1+x
  set g : ℝ → ℝ := fun x ↦ 1+x
  have hg : Tendsto g (𝓝[>] 0) (𝓝 1) := by
    apply tendsto_nhdsWithin_of_tendsto_nhds
    have : Continuous (fun x : ℝ ↦ 1 + x) := by continuity
    convert this.continuousAt.tendsto ; ring
  have : i ∘ f = g ∘ i := by ext x; rfl
  rw [tendsto_subtype_rng, ← comap_coe_Ioi_nhdsWithin_Ioi]
  change Tendsto (i ∘ f) (comap i (𝓝[>] 0)) (𝓝 1)
  rw [this]
  exact hg.comp tendsto_comap

-- Additionally "With the limit of f for x leading to 0 from the right being defined"
-- I know `lim` is not recommended but I didn't know how else to state this
theorem test2 {f : ℝ>0 → ℝ>0} (h1 : StrictMono f) {x y : ℝ>0} {hf : Tendsto f atBot (𝓝 y)} :
    y < f x := by
  sorry

[Patrick Massot]

I also took the opportunity to reformat your code to something more standard. You can clear extract a more general lemma here.

[Daniele Pusceddu]

Patrick Massot said:

I also took the opportunity to reformat your code to something more standard. You can clear extract a more general lemma here.

Thank you very much, seeing this helps a lot already.