LeanAide GPT-4 documentation

Module: Mathlib.Probability.StrongLaw

ProbabilityTheory.strong_law_aux5

theorem ProbabilityTheory.strong_law_aux5 : βˆ€ {Ξ© : Type u_1} [inst : MeasureTheory.MeasureSpace Ξ©] [inst_1 : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X : β„• β†’ Ξ© β†’ ℝ), MeasureTheory.Integrable (X 0) MeasureTheory.volume β†’ (βˆ€ (i : β„•), ProbabilityTheory.IdentDistrib (X i) (X 0) MeasureTheory.volume MeasureTheory.volume) β†’ (βˆ€ (i : β„•) (Ο‰ : Ξ©), 0 ≀ X i Ο‰) β†’ βˆ€α΅ (Ο‰ : Ξ©), (fun n => ((Finset.range n).sum fun i => ProbabilityTheory.truncation (X i) (↑i) Ο‰) - (Finset.range n).sum fun i => X i Ο‰) =o[Filter.atTop] fun n => ↑n

This theorem, named `ProbabilityTheory.strong_law_aux5`, states that for any sample space Ξ© equipped with a probability measure, and any sequence of real-valued random variables `X` defined on this space, if the first random variable `X 0` is integrable and all the random variables `X i` are identically distributed as `X 0` and are non-negative, then almost surely for each outcome Ο‰ in the sample space, the difference between the sum of the truncated versions of `X i` (truncated to the interval `(-i, i]`) and the sum of the non-truncated versions of `X i`, over the first `n` terms, will tend to 0 as `n` tends to infinity. This is equivalent to saying that the truncated and non-truncated versions of `X i` have the same asymptotic behavior as they almost surely coincide at all but finitely many steps. The theorem is a consequence of a probability computation and the Borel-Cantelli Lemma.

More concisely: Given a probability space and a sequence of identically distributed, non-negative, integrable random variables, almost surely their truncated and non-truncated sums over the first `n` terms converge to each other as `n` approaches infinity.

ProbabilityTheory.strong_law_ae

theorem ProbabilityTheory.strong_law_ae : βˆ€ {Ξ© : Type u_1} [inst : MeasureTheory.MeasureSpace Ξ©] [inst_1 : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {E : Type u_2} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [inst_4 : CompleteSpace E] [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E] (X : β„• β†’ Ξ© β†’ E), MeasureTheory.Integrable (X 0) MeasureTheory.volume β†’ (Pairwise fun i j => ProbabilityTheory.IndepFun (X i) (X j) MeasureTheory.volume) β†’ (βˆ€ (i : β„•), ProbabilityTheory.IdentDistrib (X i) (X 0) MeasureTheory.volume MeasureTheory.volume) β†’ βˆ€α΅ (Ο‰ : Ξ©), Filter.Tendsto (fun n => (↑n)⁻¹ β€’ (Finset.range n).sum fun i => X i Ο‰) Filter.atTop (nhds (∫ (a : Ξ©), X 0 a))

The Strong Law of Large Numbers (almost sure version) is given in this theorem. If `X n` is a sequence of independent and identically distributed integrable random variables in a Banach space, then the scaled sum `n⁻¹ β€’ βˆ‘ i in range n, X i` converges almost surely to the expected value `𝔼[X 0]`. This is a robust version due to Etemadi, which only requires pairwise independence rather than full independence. In more detail, for all measurable spaces `Ξ©` with a probability measure, and for all normed, complete, and measurable spaces `E` where `E` is also a Borel space, given a sequence of functions `X : β„• β†’ Ξ© β†’ E`, if `X 0` is integrable, all the functions in the sequence are pairwise independent, and all the functions are identically distributed, then almost surely (for almost all `Ο‰ : Ξ©`), the sequence `(fun n => (↑n)⁻¹ β€’ (Finset.range n).sum fun i => X i Ο‰)` tends to `𝔼[X 0]` as `n` goes to infinity.

More concisely: For a sequence of independent and identically distributed integrable random variables `X : β„• β†’ Ξ© β†’ E` in a Banach space, where `E` is a Borel space and `Ξ©` has a probability measure, almost surely, the scaled sum `(fun n => (↑n)⁻¹ β€’ (Finset.range n).sum fun i => X i Ο‰)` converges to the expected value `𝔼[X 0]` as `n` goes to infinity, given pairwise independence.

ProbabilityTheory.strong_law_ae_real

theorem ProbabilityTheory.strong_law_ae_real : βˆ€ {Ξ© : Type u_1} [inst : MeasureTheory.MeasureSpace Ξ©] [inst_1 : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X : β„• β†’ Ξ© β†’ ℝ), MeasureTheory.Integrable (X 0) MeasureTheory.volume β†’ (Pairwise fun i j => ProbabilityTheory.IndepFun (X i) (X j) MeasureTheory.volume) β†’ (βˆ€ (i : β„•), ProbabilityTheory.IdentDistrib (X i) (X 0) MeasureTheory.volume MeasureTheory.volume) β†’ βˆ€α΅ (Ο‰ : Ξ©), Filter.Tendsto (fun n => ((Finset.range n).sum fun i => X i Ο‰) / ↑n) Filter.atTop (nhds (∫ (a : Ξ©), X 0 a))

The theorem "ProbabilityTheory.strong_law_ae_real" is a version of the *Strong Law of Large Numbers* for real-valued random variables. It states that, given a sequence of pairwise independent, identically distributed, and integrable real-valued random variables `X n`, the average sum of the first `n` variables `βˆ‘ i in range n, X i / n` converges almost surely to the expectation of the zeroth variable `𝔼[X 0]`. This theorem is a strong version attributed to Etemadi that only requires pairwise independence, as opposed to complete independence. It has been superseded by `strong_law_ae`, which works for random variables taking values in any Banach space. In terms of measure theory, this means that for almost every outcome `Ο‰` in the probability space `Ξ©`, as `n` tends to infinity, the ratio of the sum of the first `n` variables to `n` converges to the integral of the zeroth variable over the entire space.

More concisely: Given a sequence of pairwise independent, identically distributed, integrable real-valued random variables `X n`, the sequence of their averages `βˆ‘ i in range n, X i / n` converges almost surely to the expectation of the first variable `𝔼[X 0]`.

ProbabilityTheory.strong_law_Lp

theorem ProbabilityTheory.strong_law_Lp : βˆ€ {Ξ© : Type u_1} [inst : MeasureTheory.MeasureSpace Ξ©] [inst_1 : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {E : Type u_2} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [inst_4 : CompleteSpace E] [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E] {p : ENNReal}, 1 ≀ p β†’ p β‰  ⊀ β†’ βˆ€ (X : β„• β†’ Ξ© β†’ E), MeasureTheory.Memβ„’p (X 0) p MeasureTheory.volume β†’ (Pairwise fun i j => ProbabilityTheory.IndepFun (X i) (X j) MeasureTheory.volume) β†’ (βˆ€ (i : β„•), ProbabilityTheory.IdentDistrib (X i) (X 0) MeasureTheory.volume MeasureTheory.volume) β†’ Filter.Tendsto (fun n => MeasureTheory.snorm (fun Ο‰ => ((↑n)⁻¹ β€’ (Finset.range n).sum fun i => X i Ο‰) - ∫ (a : Ξ©), X 0 a) p MeasureTheory.volume) Filter.atTop (nhds 0)

This theorem states the **Strong Law of Large Numbers** in its Lα΅– version. The theorem applies to a sequence of independent identically distributed random variables in Lα΅–, denoted as `X n`. It states that the scaled sum of the first `n` variables in this sequence, `(n⁻¹ β€’ βˆ‘ i in range n, X i)`, converges in Lα΅– to the expected value of the first variable, `𝔼[X 0]`. More formally, the Lα΅– norm of the difference between this scaled sum and the integral of `X 0` with respect to the measure tends to zero as n approaches infinity. The conditions for this theorem to hold include that `p` must be greater than or equal to 1 and less than infinity, and `X 0` must belong to the Lα΅– space of the measure space Ξ©. Furthermore, any two variables in the sequence must be independent and each variable must have the same distribution as `X 0`.

More concisely: Given a sequence of independent, identically distributed random variables `X n` in a measure space with `p`-th moment finite and `X_0` integrable, the sequence's scaled sum `(1/n * βˆ‘ i in range n, X_i)` converges in `L^p` to the expected value `𝔼[X_0]`.

ProbabilityTheory.strong_law_ae_of_measurable

theorem ProbabilityTheory.strong_law_ae_of_measurable : βˆ€ {Ξ© : Type u_1} [inst : MeasureTheory.MeasureSpace Ξ©] [inst_1 : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {E : Type u_2} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [inst_4 : CompleteSpace E] [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E] (X : β„• β†’ Ξ© β†’ E), MeasureTheory.Integrable (X 0) MeasureTheory.volume β†’ MeasureTheory.StronglyMeasurable (X 0) β†’ (Pairwise fun i j => ProbabilityTheory.IndepFun (X i) (X j) MeasureTheory.volume) β†’ (βˆ€ (i : β„•), ProbabilityTheory.IdentDistrib (X i) (X 0) MeasureTheory.volume MeasureTheory.volume) β†’ βˆ€α΅ (Ο‰ : Ξ©), Filter.Tendsto (fun n => (↑n)⁻¹ β€’ (Finset.range n).sum fun i => X i Ο‰) Filter.atTop (nhds (∫ (a : Ξ©), X 0 a))

This theorem is a preliminary lemma for the strong law of large numbers for vector-valued random variables, under the assumption of measurability in addition to integrability. Specifically, for a sequence of random variables `X` from natural numbers to a certain measure space `Ξ©` into a normed additive commutative group `E`, if the first random variable in the sequence is integrable and strongly measurable, and if every pair of random variables in the sequence are independent, and every random variable in the sequence is identically distributed with the first random variable, then almost everywhere in `Ξ©`, the sequence of the scaled sum of the first `n` random variables converges to the expected value of the first random variable as `n` goes to infinity. This statement will be subsequently weakened to almost everywhere measurability in the full version of the strong law of large numbers.

More concisely: If a sequence of independent, identically distributed, integrable and strongly measurable vector-valued random variables converges almost everywhere to its expected value as the number of terms increases.

ProbabilityTheory.strong_law_aux7

theorem ProbabilityTheory.strong_law_aux7 : βˆ€ {Ξ© : Type u_1} [inst : MeasureTheory.MeasureSpace Ξ©] [inst_1 : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X : β„• β†’ Ξ© β†’ ℝ), MeasureTheory.Integrable (X 0) MeasureTheory.volume β†’ (Pairwise fun i j => ProbabilityTheory.IndepFun (X i) (X j) MeasureTheory.volume) β†’ (βˆ€ (i : β„•), ProbabilityTheory.IdentDistrib (X i) (X 0) MeasureTheory.volume MeasureTheory.volume) β†’ (βˆ€ (i : β„•) (Ο‰ : Ξ©), 0 ≀ X i Ο‰) β†’ βˆ€α΅ (Ο‰ : Ξ©), Filter.Tendsto (fun n => ((Finset.range n).sum fun i => X i Ο‰) / ↑n) Filter.atTop (nhds (∫ (a : Ξ©), X 0 a))

This theorem, named `ProbabilityTheory.strong_law_aux7`, asserts the Strong Law of Large Numbers in the context of a measure theoretic probability space. It states that, for a sequence of identically distributed, independent, integrable, and non-negative random variables `X` on a probability space `Ξ©`, the average of the first `n` variables converges almost surely to the expected value of `X 0`, as `n` goes to infinity. Formally, this is expressed as the tendency of the function which averages the first `n` variables, `(fun n => ((Finset.range n).sum fun i => X i Ο‰) / ↑n)`, towards the integral of `X 0`, `(∫ (a : Ξ©), X 0 a)`, under the Filter `atTop`, which represents the limit towards infinity. This convergence happens for almost every point `Ο‰` in the measure space `Ξ©`. The proof of the theorem is not shown here.

More concisely: For a sequence of independent, identically distributed, integrable, and non-negative random variables `X` on a probability space `Ξ©`, the average of the first `n` variables converges almost surely to the expected value of `X` as `n` goes to infinity.

ProbabilityTheory.tendsto_integral_truncation

theorem ProbabilityTheory.tendsto_integral_truncation : βˆ€ {Ξ± : Type u_1} {m : MeasurableSpace Ξ±} {ΞΌ : MeasureTheory.Measure Ξ±} {f : Ξ± β†’ ℝ}, MeasureTheory.Integrable f ΞΌ β†’ Filter.Tendsto (fun A => ∫ (x : Ξ±), ProbabilityTheory.truncation f A x βˆ‚ΞΌ) Filter.atTop (nhds (∫ (x : Ξ±), f x βˆ‚ΞΌ))

This theorem states that, given a measurable space and a real-valued function that is integrable over a measure on this space, the integral of the function truncated to the interval `(-A, A]` converges to the integral of the entire function as `A` approaches infinity. In other words, if we consider progressively larger and larger intervals to compute the integral of our function, the result of these computations will tend to the true value of the integral of the function over the entire space.

More concisely: Given a measurable space, a measurable integrable real-valued function, and a sequence of integrals of the function truncated to increasingly larger intervals, the limit of this sequence is equal to the integral of the entire function.

ProbabilityTheory.strong_law_ae_simpleFunc_comp

theorem ProbabilityTheory.strong_law_ae_simpleFunc_comp : βˆ€ {Ξ© : Type u_1} [inst : MeasureTheory.MeasureSpace Ξ©] [inst_1 : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {E : Type u_2} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [inst_4 : CompleteSpace E] [inst_5 : MeasurableSpace E] (X : β„• β†’ Ξ© β†’ E), Measurable (X 0) β†’ (Pairwise fun i j => ProbabilityTheory.IndepFun (X i) (X j) MeasureTheory.volume) β†’ (βˆ€ (i : β„•), ProbabilityTheory.IdentDistrib (X i) (X 0) MeasureTheory.volume MeasureTheory.volume) β†’ βˆ€ (Ο† : MeasureTheory.SimpleFunc E E), βˆ€α΅ (Ο‰ : Ξ©), Filter.Tendsto (fun n => (↑n)⁻¹ β€’ (Finset.range n).sum fun i => ↑φ (X i Ο‰)) Filter.atTop (nhds (∫ (a : Ξ©), (↑φ ∘ X 0) a))

This theorem is a preliminary lemma for the strong law of large numbers for vector-valued random variables. It states that, given a sequence of measurable vector-valued random variables on a probability space that are pairwise independent and identically distributed, and a simple function, almost every outcome in the probability space follows the strong law of large numbers under the transformation of the random variables by this simple function. That means, the arithmetic average of the simple function applied to the sequence of random variables, scaled by the reciprocal of the sample size, tends to the expected value of the simple function composed with the first random variable as the sample size goes to infinity. This holds true for almost every outcome in the probability space.

More concisely: Given a sequence of independent and identically distributed measurable vector-valued random variables and a simple function, for almost every outcome, the sample mean of the simple function applied to the sequence converges to the expected value of the composition of the simple function and the first random variable as the sample size goes to infinity.

ProbabilityTheory.strong_law_aux3

theorem ProbabilityTheory.strong_law_aux3 : βˆ€ {Ξ© : Type u_1} [inst : MeasureTheory.MeasureSpace Ξ©] [inst_1 : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X : β„• β†’ Ξ© β†’ ℝ), MeasureTheory.Integrable (X 0) MeasureTheory.volume β†’ (βˆ€ (i : β„•), ProbabilityTheory.IdentDistrib (X i) (X 0) MeasureTheory.volume MeasureTheory.volume) β†’ (fun n => (∫ (a : Ξ©), (Finset.range n).sum (fun i => ProbabilityTheory.truncation (X i) ↑i) a) - ↑n * ∫ (a : Ξ©), X 0 a) =o[Filter.atTop] Nat.cast

This theorem, named `ProbabilityTheory.strong_law_aux3`, states that for any measure space `Ξ©` and a sequence of real-valued functions `X : β„• β†’ Ξ© β†’ ℝ`, if the function `(X 0)` is integrable and each function `(X i)` is identically distributed with `(X 0)`, then the difference between the expectation of the truncated sum of `X_i` and the whole expectation multiplied by `n` is an infinitesimal of `n` as `n` approaches infinity. In other words, the expected value of the truncated version of `X_i` behaves asymptotically like the whole expectation, which is a result derived from the concepts of convergence and CesΓ ro averaging in Probability Theory.

More concisely: For a measurable space `Ξ©` and a sequence of integrable, identically distributed real-valued functions `X : β„• β†’ Ξ© β†’ ℝ`, the difference between the expectation of the sum of the first `n` functions and `n` times the expectation of each function approaches 0 as `n` goes to infinity.