Foundations of probability

Construction of probability measures and processes (Kolmogorov extension, measures from Stieltjes functions), independence, conditional expectation and regular conditional distributions, exchangeability and de Finetti's theorem, and zero–one laws for sequences (Hewitt–Savage); zero–one laws for continuous processes go to Brownian motion and stochastic calculus, tail sigma-algebras of random walks to Random walks.

• Conditional expectation as the best predictor
• Hewitt–Savage zero–one law
• Probability measures from distribution functions
• Regular conditional distributions

TheoremDe Finetti's theorem for binary sequences#✓fully proved

Let \(\mu\) be a probability measure on the space \(\{0, 1\}^{\mathbb{N}}\) of binary sequences \(\omega = (\omega_i)_{i \in \mathbb{N}}\), with \(0\) and \(1\) standing for false and true. Suppose \(\mu\) is exchangeable: for every permutation \(\pi\) of \(\mathbb{N}\) that moves only finitely many points, the image of \(\mu\) under the map \(\omega \mapsto \omega \circ \pi\) is \(\mu\). Then there is a probability measure \(\nu\) on \([0, 1]\) such that for all disjoint finite sets \(A, B \subseteq \mathbb{N}\),

\[\mu\{\omega : \omega_i = 1 \text{ for all } i \in A \text{ and } \omega_i = 0 \text{ for all } i \in B\} = \int_{[0, 1]} p^{|A|} (1 - p)^{|B|} \, d\nu(p).\]

theorem deFinetti_binary
    (μ : ProbabilityMeasure (ℕ → Bool))
    (hμ : ∀ (σ : Equiv.Perm ℕ), Set.Finite {n : ℕ | σ n ≠ n} →
      Measure.map (fun ω : ℕ → Bool => ω ∘ ⇑σ) (μ : Measure (ℕ → Bool)) =
        (μ : Measure (ℕ → Bool))) :
    ∃ (ν : ProbabilityMeasure (Set.Icc (0 : ℝ) 1)),
      ∀ (A B : Finset ℕ), Disjoint A B →
        (μ : Measure (ℕ → Bool))
          {ω : ℕ → Bool | (∀ i ∈ A, ω i = true) ∧ (∀ i ∈ B, ω i = false)} =
          ENNReal.ofReal
            (MeasureTheory.integral (ν : Measure (Set.Icc (0 : ℝ) 1))
              (fun p : Set.Icc (0 : ℝ) 1 =>
                (p.val : ℝ) ^ A.card * (1 - (p.val : ℝ)) ^ B.card))

Sources

• B. de Finetti, Funzione caratteristica di un fenomeno aleatorio, Atti Accad. Naz. Lincei 4 (1931) and La prévision: ses lois logiques (1937); textbook in Kallenberg, Probabilistic Symmetries and Invariance Principles; also Durrett, Probability Theory and Examples

TheoremKolmogorov extension theorem#✓fully proved

Let \((\alpha_i)_{i \in \iota}\) be a family of Polish spaces, each with its Borel σ-algebra, indexed by an arbitrary type \(\iota\). For each finite set \(J \subseteq \iota\) let \(P_J\) be a probability measure on \(\prod_{j \in J} \alpha_j\), and suppose the family is projective: whenever \(J \subseteq I\) are finite, the image of \(P_I\) under the restriction map \(\prod_{i \in I} \alpha_i \to \prod_{j \in J} \alpha_j\) is \(P_J\). Then there is a measure \(\mu\) on \(\prod_{i \in \iota} \alpha_i\) whose image under the restriction map to \(\prod_{j \in J} \alpha_j\) is \(P_J\) for every finite \(J \subseteq \iota\).

theorem kolmogorov_extension
    {ι : Type*} {α : ι → Type*}
    [∀ i, TopologicalSpace (α i)] [∀ i, PolishSpace (α i)]
    [∀ i, MeasurableSpace (α i)] [∀ i, BorelSpace (α i)]
    (P : ∀ J : Finset ι, Measure (∀ j : J, α j))
    [∀ J, IsProbabilityMeasure (P J)]
    (hP : IsProjectiveMeasureFamily P) :
    ∃ μ : Measure (∀ i, α i), IsProjectiveLimit μ P

Sources

• A. N. Kolmogorov, Grundbegriffe der Wahrscheinlichkeitsrechnung, 1933; P. J. Daniell 1918 precursor; textbook in Kallenberg, Foundations of Modern Probability, 3rd ed. (Kolmogorov extension) and Tao, Introduction to Measure Theory Lean Polish Borel projective-limit version; full general version handles standard Borel factors.

Used by 2

Used byKolmogorov extension for Markov semigroup laws · Existence of a pre-Brownian motion on path space

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.