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) :=
  intros s hs,
  have : filter.tendsto (sets_valued_below X) at_top _,



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