Zulip Chat Archive

Stream: new members

Topic: Limit of real->real


view this post on Zulip 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?

view this post on Zulip Iocta (Sep 02 2020 at 22:40):

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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Iocta (Sep 04 2020 at 19:43):

(or do we not do that?)

view this post on Zulip Patrick Massot (Sep 04 2020 at 19:44):

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

view this post on Zulip Patrick Massot (Sep 04 2020 at 19:44):

Using notations for nhds_within and nhds

view this post on Zulip Patrick Massot (Sep 04 2020 at 19:44):

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

view this post on Zulip Anatole Dedecker (Sep 04 2020 at 19:45):

Or tendsto f (𝓝[Iic x] x) (𝓝 1) if you want to include the point x itself

view this post on Zulip Patrick Massot (Sep 04 2020 at 19:45):

Indeed the specification was vague here.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Sep 04 2020 at 19:47):

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

view this post on Zulip 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

view this post on Zulip 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"?

view this post on Zulip Iocta (Sep 04 2020 at 20:05):

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

view this post on Zulip 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

view this post on Zulip Iocta (Sep 07 2020 at 23:42):

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

view this post on Zulip Reid Barton (Sep 08 2020 at 00:40):

Do you have a plan for what to do next?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: May 16 2021 at 05:21 UTC