Limit definition issue. Probability theory

Stream: new members

[Daniil Homza]

Hi All!

I try to proof Weak law in Lean(there is no in mathlib). I already proof the main step which is the applying chebyshev inequality for our case(ineq in code below). What I want to now is just to say that probability estimated by chebyshev inequality which converges to 0. However, I ran into a problem of definition of tends_to which is definite by filtration.

import tactic
import probability.ident_distrib
import probability.notation
import probability.integration
import probability.variance



open measure_theory filter finset

open_locale topological_space big_operators measure_theory probability_theory ennreal nnreal

namespace probability_theory

variables {Ω : Type*} [measure_space Ω] [is_probability_measure (ℙ : measure Ω)][ω:Ω][c:ℝ]





theorem Weak_Law {X : ℕ → Ω → ℝ}
(hint : ∀ i, integrable (X i)) (hindep : pairwise (λ i j, indep_fun (X i) (X j)))
(hident : ∀ i, ident_distrib (X i) (X 0)) (hs : ∀ i, mem_ℒp (X i) 2)(hc : 0 < c):
tendsto (λ (n : ℕ), ℙ {ω | c*n ≤|(∑ i in range n, X i ) ω - n*𝔼[(X 0)]|}) at_top (𝓝 (0)) :=
begin
  have ineq: ∀ (m:ℕ), (m>0) -> (ℙ {ω | c*m ≤ |(∑ i in range m, X i ) ω - m*𝔼[(X 0)]|}) ≤ ennreal.of_real (Var[(X 0)] / (c^2*m)),
  begin
    sorry,
  end,
  rw tendsto_def,

  end,
end
end probability_theory

As I understand it is very useful in lots of case but here I supposed to use usual definition of limits. Can I try to reformulate it for usual epsilon-delta definition(or analogue) or It should be proofed by filtration tools? Thank you in advance!

[Sebastien Gouezel]

I am not answering your question, but we already have the strong law in mathlib, which is stronger than the weak law. But I would understand perfectly if you want to redo a proof on your own based on elementary principles, as it is always instructive.

[Sebastien Gouezel]

To answer your question, you have the lemma docs#metric.tendsto_at_top

[Daniil Homza]

Sebastien Gouezel said:

To answer your question, you have the lemma docs#metric.tendsto_at_top

I try to use rewrite tactic with docs#metric.tendsto_at_top but lean did not find instance of the pattern. Should I somehow add all necessary information(as in documentation docs#pseudo_metric_space, docs#no_max_order and so on ) about my space (N, R>=0) to be able apply it?

[Sebastien Gouezel]

Sorry, you are in ennreal and not in a metric space. Use docs#ennreal.tendsto_nhds_zero instead.

[Kevin Buzzard]

The original lemma metric.tendsto_at_top wants a so-called pseudo_metric_space. When I hover over this I see the following docstring, which I found unhelpful:

/-- Metric space

Each metric space induces a canonical `uniform_space` and hence a canonical `topological_space`.
This is enforced in the type class definition, by extending the `uniform_space` structure. When
instantiating a `metric_space` structure, the uniformity fields are not necessary, they will be
filled in by default. In the same way, each metric space induces an emetric space structure.
It is included in the structure, but filled in by default.
-/

My question: what is a pseudo-metric space, and should the docstring tell us this, rather than telling us something which I don't really understand (it seems to assume I know what an "emetric space" is) and which doesn't answer the obvious question (namely, what the heck is a pseudo-metric space?)

[Jason KY.]

Sebastien Gouezel said:

I am not answering your question, but we already have the strong law in mathlib, which is stronger than the weak law.

The weak law remains to hold without assuming identically distributed via the Chebyshev inequality proof so its not strictly weaker than the strongly law right?

[Jason KY.]

If you do assume identically distributed (which is what you assume in your current formulation) you can get the weak law by composing the strong law with docs#measure_theory.tendsto_in_measure_of_tendsto_ae

[Riccardo Brasca]

Kevin Buzzard said:

The original lemma metric.tendsto_at_top wants a so-called pseudo_metric_space. When I hover over this I see the following docstring, which I found unhelpful:

/-- Metric space

Each metric space induces a canonical `uniform_space` and hence a canonical `topological_space`.
This is enforced in the type class definition, by extending the `uniform_space` structure. When
instantiating a `metric_space` structure, the uniformity fields are not necessary, they will be
filled in by default. In the same way, each metric space induces an emetric space structure.
It is included in the structure, but filled in by default.
-/

My question: what is a pseudo-metric space, and should the docstring tell us this, rather than telling us something which I don't really understand (it seems to assume I know what an "emetric space" is) and which doesn't answer the obvious question (namely, what the heck is a pseudo-metric space?)

The doc needs to be fixed, but a pseudo_metric_space is like a metric space, without d(x,y)=0 → x = y. They've been introduced because we needed them in the LTE.

[Kevin Buzzard]

Yeah, that sounds like a much better docstring :-) Thanks! I can never remember which generalisation is which (presumably the e one is the one which allows infinity). (oh -- penny drops -- like ereal and enat)

[Riccardo Brasca]

We also have docs#pseudo_emetric_space

[Riccardo Brasca]

It's sad that the normed thing is called docs#seminormed_add_comm_group, but this seems to be the standard terminology

[Riccardo Brasca]

(And in the LTE there are pseudonormed groups, to make things even worse)

[Sebastien Gouezel]

Sebastien Gouezel said:

Sorry, you are in ennreal and not in a metric space. Use docs#ennreal.tendsto_nhds_zero instead.

Or even docs#ennreal.tendsto_at_top_zero

[Daniil Homza]

Jason KY. said:

Sebastien Gouezel said:

I am not answering your question, but we already have the strong law in mathlib, which is stronger than the weak law.

The weak law remains to hold without assuming identically distributed via the Chebyshev inequality proof so its not strictly weaker than the strongly law right?

What do You mean by Weak Law? I am assume that there are i.i.d., but actually it is easy to fixed using only independence and assumption on a same expected value and variance. Is it version which You think of?

[Daniil Homza]

Sebastien Gouezel said:

Sebastien Gouezel said:

Sorry, you are in ennreal and not in a metric space. Use docs#ennreal.tendsto_nhds_zero instead.

Or even docs#ennreal.tendsto_at_top_zero

Yes, now is perfect, Thank you!

[Jason KY.]

Daniil Homza said:

What do You mean by Weak Law? I am assume that there are i.i.d., but actually it is easy to fixed using only independence and assumption on a same expected value and variance. Is it version which You think of?

Yes, that's exactly what I'm saying