Limit of real->real

Stream: new members

[Iocta]

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]

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

[Anatole Dedecker]

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]

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

[Iocta]

(or do we not do that?)

[Patrick Massot]

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

[Patrick Massot]

Using notations for nhds_within and nhds

[Patrick Massot]

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

[Anatole Dedecker]

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

[Patrick Massot]

Indeed the specification was vague here.

[Patrick Massot]

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]

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

[Anatole Dedecker]

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]

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]

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

[Iocta]

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]

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

[Reid Barton]

Do you have a plan for what to do next?

[Iocta]

@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]

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]

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

[Reid Barton]

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

[Reid Barton]

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]

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