# Zulip Chat Archive

## Stream: new members

### Topic: Limit of real->real

#### Iocta (Sep 02 2020 at 22:38):

I have `f : real -> real`

and I want to say "\lim_{x \to \infty} f x = 1". Should I define lim using epsilon-delta, or is there some higher-level construct I can use?

#### Iocta (Sep 02 2020 at 22:40):

One of the tutorials uses epsilon delta, but I don't see that in mathlib

#### Anatole Dedecker (Sep 02 2020 at 22:48):

The mathlib way to formulate what you want to prove is `filter.tendsto f at_top (nhds 1)`

. See https://leanprover-community.github.io/theories/topology.html

#### Iocta (Sep 04 2020 at 19:30):

How do I write left- and right-hand limits? "The limit at x of f from the left is 1"

#### Iocta (Sep 04 2020 at 19:43):

(or do we not do that?)

#### Patrick Massot (Sep 04 2020 at 19:44):

`tendsto f (𝓝[Iio x] x) (𝓝 1)`

#### Patrick Massot (Sep 04 2020 at 19:44):

Using notations for `nhds_within`

and `nhds`

#### Patrick Massot (Sep 04 2020 at 19:44):

see https://github.com/leanprover-community/mathlib/blob/master/src/topology/algebra/ordered.lean

#### Anatole Dedecker (Sep 04 2020 at 19:45):

Or `tendsto f (𝓝[Iic x] x) (𝓝 1)`

if you want to include the point `x`

itself

#### Patrick Massot (Sep 04 2020 at 19:45):

Indeed the specification was vague here.

#### Patrick Massot (Sep 04 2020 at 19:46):

If you're struggling with filters then docs#metric.tendsto_nhds_within_nhds will probably help bridging between this and more familiar things.

#### Patrick Massot (Sep 04 2020 at 19:47):

You also need to know about docs#set.Iic and its friends.

#### Anatole Dedecker (Sep 04 2020 at 19:48):

Oh that reminds me I started working on a PR adding more lemmas like this one about translating filters to epsilons, I should finish it at some point

#### Iocta (Sep 04 2020 at 20:00):

does mathlib have something like "When X has distribution F with the form F(x) \int_\infty^x f(y)dy, we say that X has density function f"?

#### Iocta (Sep 04 2020 at 20:05):

does density_function want to be a type, or a Prop-valued function, or a structure?

#### Iocta (Sep 07 2020 at 21:59):

I want to say "as x -> infty, { w | X w < x } -> univ" in the `have`

. I think that means filling the `_`

with "neighborhoods surrounding `univ`

". How can I do that?

```
import algebra.big_operators
import algebra.big_operators.intervals
import measure_theory.measure_space
open measure_theory set filter
open_locale big_operators topological_space filter
noncomputable theory
variables {Ω : Type*} [measurable_space Ω] (p : measure Ω) [probability_measure p] (X Y : Ω → ℝ)
def sets_valued_below (x : ℝ) : set Ω :=
{ ω | X ω ≤ x }
def F : ℝ → ennreal :=
λx, p (sets_valued_below X x)
lemma lim_infty_F_eq_1 : filter.tendsto (F p X) at_top (𝓝 1) :=
begin
intros s hs,
have : filter.tendsto (sets_valued_below X) at_top _,
{
},
end
```

#### Iocta (Sep 07 2020 at 23:42):

In other words, how do you say a sequence of sets converges to `univ`

?

#### Reid Barton (Sep 08 2020 at 00:40):

Do you have a plan for what to do next?

#### Iocta (Sep 08 2020 at 01:37):

@Reid Barton The idea is, if {X <= x} converges to univ as x converges to infinity, and `p univ = 1`

by `measure_univ`

, then `F`

should converge to 1 too.

#### Iocta (Sep 08 2020 at 01:45):

tbh I'm not sure if I'm making reasonable progress or I'm in over my head. If it seems like I should work on something easier instead that would be useful feedback for me.

#### Reid Barton (Sep 08 2020 at 01:47):

Okay, but is there actually a lemma that will allow you to conclude that the measures tend to 1?

#### Reid Barton (Sep 08 2020 at 01:47):

If there is, you can take a look at its statement to see what form the hypothesis takes.

#### Reid Barton (Sep 08 2020 at 01:49):

If there isn't, then you have to prove it yourself and figuring out how will probably guide you to the right statement.

#### Reid Barton (Sep 08 2020 at 01:50):

I have no idea how hard this is as I'm not familiar with the measure theory library.

Last updated: Dec 20 2023 at 11:08 UTC