## Stream: new members

### Topic: Limits with positive reals and atBot

#### Daniele Pusceddu (Nov 20 2023 at 09:48):

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 (Nov 20 2023 at 14:18):

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

#### Patrick Massot (Nov 20 2023 at 14:19):

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

#### Daniele Pusceddu (Nov 20 2023 at 14:25):

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 (Nov 20 2023 at 14:57):

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 (Nov 20 2023 at 14:58):

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

#### Daniele Pusceddu (Nov 20 2023 at 15:12):

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.

Last updated: Dec 20 2023 at 11:08 UTC