Conjugate priors

DefinitionBinomial likelihood kernel#✓fully proved

For a natural number \(n\), the binomial kernel sends a real \(\theta\) to the binomial distribution \(\mathrm{Bin}(n, p)\) on \(\mathbb{N}\), the law of the number of successes in \(n\) independent coin flips with success probability \(p\), where \(p\) is \(\theta\) clipped to \([0, 1]\).

noncomputable def binomialKernel (n : ℕ) : Kernel ℝ ℕ where
  toFun θ := binomial n (projIcc 0 1 zero_le_one θ)
  measurable' := by
    refine Measure.measurable_of_measurable_coe _ fun s hs ↦ ?_
    simp_rw [← Measure.tsum_indicator_apply_singleton _ s hs]
    refine Measurable.tsum fun k ↦ ?_
    by_cases hk : k ∈ s
    · simp only [Set.indicator_of_mem hk, binomial_singleton]
      refine ENNReal.measurable_ofReal.comp ?_
      fun_prop
    · simp only [Set.indicator_of_notMem hk]
      exact measurable_const

Used by 5

Used byBeta prior times binomial likelihood · The beta-binomial distribution · Prior predictive probability of a success · Beta–binomial conjugacy · Posterior predictive of the beta-binomial model

TheoremRecurrence for the beta function in the first argument#✓fully proved

For real \(a > 0\) and \(b > 0\), the beta function \(B(a, b) = \Gamma(a)\Gamma(b)/\Gamma(a + b)\) satisfies \(B(a + 1, b) = B(a, b) \cdot \frac{a}{a + b}\).

theorem beta_add_one_left {a b : ℝ} (ha : 0 < a) (hb : 0 < b) :
    beta (a + 1) b = beta a b * (a / (a + b))

Used by 1

Used byPrior predictive probability of a success

TheoremConjugacy of the beta density#✓fully proved

Let \(a, b > 0\) be real, \(k, m\) natural numbers and \(\theta\) real. Write \(f_{a,b}\) for the \(\mathrm{Beta}(a, b)\) density (zero outside \((0, 1)\)) and \(B(a, b) = \Gamma(a)\Gamma(b)/\Gamma(a + b)\) for the beta function. Then \(f_{a,b}(\theta) \, \theta^k (1 - \theta)^m = \frac{B(a + k, b + m)}{B(a, b)} f_{a + k, b + m}(\theta)\).

theorem betaPDFReal_mul_pow {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (k m : ℕ) (θ : ℝ) :
    betaPDFReal a b θ * (θ ^ k * (1 - θ) ^ m) =
      beta (a + k) (b + m) / beta a b * betaPDFReal (a + k) (b + m) θ

Used by 1

Used byBeta prior times binomial likelihood

TheoremBeta prior times binomial likelihood#✓fully proved

Let \(a, b > 0\) be real, \(n, k\) natural numbers, \(m = n - k\) if \(k \le n\) and \(m = 0\) otherwise, and \(\theta\) real. Write \(f_{a,b}\) for the \(\mathrm{Beta}(a, b)\) density (zero outside \((0, 1)\)) and \(B\) for the beta function. Then the density \(f_{a,b}(\theta)\) times the probability that the binomial kernel at \(\theta\) gives exactly \(k\) successes in \(n\) trials equals \(\binom{n}{k} \frac{B(a + k, b + m)}{B(a, b)} f_{a + k, b + m}(\theta)\), as an identity in \([0, \infty]\).

theorem betaPDF_mul_binomialKernel (ha : 0 < a) (hb : 0 < b) {n k : ℕ} (θ : ℝ) :
    betaPDF a b θ * binomialKernel n θ {k} =
      ENNReal.ofReal (n.choose k * (beta (a + k) (b + (n - k : ℕ)) / beta a b)) *
        betaPDF (a + k) (b + (n - k : ℕ)) θ

Uses 2 · Used by 2

Statement usesBinomial likelihood kernel

Proof usesConjugacy of the beta density

Used byThe beta-binomial distribution · Beta–binomial conjugacy

TheoremThe beta-binomial distribution#✓fully proved

Let \(a, b > 0\) be real, \(n, k\) natural numbers and \(B(x, y) = \Gamma(x)\Gamma(y)/\Gamma(x + y)\) the beta function. Under a \(\mathrm{Beta}(a, b)\) prior on the success probability, the marginal probability (the evidence) that the binomial kernel gives exactly \(k\) successes in \(n\) trials is \(\binom{n}{k} \frac{B(a + k, b + n - k)}{B(a, b)}\), where \(n - k\) is truncated at \(0\).

theorem binomialKernel_comp_betaMeasure (ha : 0 < a) (hb : 0 < b) {n k : ℕ} :
    (binomialKernel n ∘ₘ betaMeasure a b) {k} =
      ENNReal.ofReal (n.choose k * (beta (a + k) (b + (n - k : ℕ)) / beta a b))

Uses 3 · Used by 2

Statement usesBinomial likelihood kernel

Proof usesBeta prior times binomial likelihood · The evidence is the integral of the likelihood

Used byPrior predictive probability of a success · Beta–binomial conjugacy

TheoremBeta–binomial conjugacy#✓fully proved

Let \(a, b > 0\) be real and \(k \le n\) natural numbers. For the binomial kernel and a \(\mathrm{Beta}(a, b)\) prior, the posterior distribution (Mathlib's posterior kernel) after observing \(k\) successes in \(n\) trials is \(\mathrm{Beta}(a + k, b + n - k)\).

theorem posterior_binomialKernel_betaMeasure (ha : 0 < a) (hb : 0 < b) {n k : ℕ} (hk : k ≤ n) :
    haveI := isProbabilityMeasureBeta ha hb
    ((binomialKernel n)†(betaMeasure a b)) k = betaMeasure (a + k) (b + (n - k : ℕ))

Uses 5 · Used by 1

Statement usesBinomial likelihood kernel

Proof usesBayes posterior · Beta prior times binomial likelihood · The beta-binomial distribution · Bayes' rule for discrete observations

Used byPosterior predictive of the beta-binomial model

TheoremPrior predictive probability of a success#✓fully proved

Let \(a, b > 0\) be real. Under a \(\mathrm{Beta}(a, b)\) prior on the success probability, the probability that a single trial of the binomial kernel succeeds is the prior mean \(a / (a + b)\).

theorem binomialKernel_one_comp_betaMeasure (ha : 0 < a) (hb : 0 < b) :
    (binomialKernel 1 ∘ₘ betaMeasure a b) {1} = ENNReal.ofReal (a / (a + b))

Uses 3 · Used by 1

Statement usesBinomial likelihood kernel

Proof usesRecurrence for the beta function in the first argument · The beta-binomial distribution

Used byPosterior predictive of the beta-binomial model

TheoremPosterior predictive of the beta-binomial model#✓fully proved

Let \(a, b > 0\) be real and \(k \le n\) natural numbers. Under a \(\mathrm{Beta}(a, b)\) prior on the success probability, after observing \(k\) successes in \(n\) trials of the binomial kernel, the posterior predictive probability that one further trial succeeds is \((a + k) / (a + b + n)\).

For \(a = b = 1\) this is Laplace's rule of succession, \((k + 1) / (n + 2)\).

theorem posterior_predictive_betaMeasure (ha : 0 < a) (hb : 0 < b) {n k : ℕ} (hk : k ≤ n) :
    haveI := isProbabilityMeasureBeta ha hb
    (binomialKernel 1 ∘ₘ ((binomialKernel n)†(betaMeasure a b)) k) {1} =
      ENNReal.ofReal ((a + k) / (a + b + n))

Uses 3

Statement usesBinomial likelihood kernel

Proof usesPrior predictive probability of a success · Beta–binomial conjugacy

DefinitionProbability vectors#✓fully proved

For \(n \in \mathbb{N}\), the probability vectors are the \(\theta \in \mathbb{R}^{n+1}\) with \(\theta_i \ge 0\) for every \(i\) and \(\sum_i \theta_i = 1\); they form the parameter space of the categorical model.

def probVectors (n : ℕ) : Set (Fin (n + 1) → ℝ) := {θ | (∀ i, 0 ≤ θ i) ∧ ∑ i, θ i = 1}

Used by 6

Used byThe categorical likelihood · Prior predictive of the Dirichlet–categorical model · The multinomial sampling model · Dirichlet–multinomial conjugacy · Posterior predictive of the Dirichlet–multinomial model · Evidence-weighted Dirichlet prior

DefinitionThe categorical likelihood#✓fully proved

For \(n \in \mathbb{N}\), the categorical likelihood is the kernel from parameters \(\theta \in \mathbb{R}^{n+1}\) to labels \(\{0, \dots, n\}\) that sends a probability vector \(\theta\) (all \(\theta_i \ge 0\) and \(\sum_i \theta_i = 1\)) to the law of one label drawn with probability \(\theta_i\) for label \(i\), and sends every other \(\theta\) to the point mass at label \(0\).

Parameters outside the probability vectors form a null set under a Dirichlet prior.

noncomputable def categoricalKernel (n : ℕ) : Kernel (Fin (n + 1) → ℝ) (Fin (n + 1)) :=
  Kernel.piecewise (measurableSet_probVectors n)
    ⟨fun θ ↦ ∑ i, ENNReal.ofReal (θ i) • Measure.dirac i,
      Measure.measurable_of_measurable_coe _ fun A _ ↦ by
        simp only [Measure.coe_finsetSum, Finset.sum_apply, Measure.smul_apply, smul_eq_mul]
        exact Finset.measurable_sum _ fun i _ ↦
          (ENNReal.measurable_ofReal.comp (measurable_pi_apply i)).mul_const _⟩
    (Kernel.const _ (Measure.dirac 0))

Uses 1 · Used by 2

Statement usesProbability vectors

Used byPrior predictive of the Dirichlet–categorical model · Posterior predictive of the Dirichlet–multinomial model

DefinitionLikelihood of a label sequence#✓fully proved

For \(\theta \in \mathbb{R}^{n+1}\) and a sequence \(s = (s_0, \dots, s_{N-1})\) of labels in \(\{0, \dots, n\}\), the likelihood of \(s\) is the extended nonnegative real \(\prod_{m < N} \theta_{s_m}^+\), where \(x^+ = \max(x, 0)\).

noncomputable def seqLikelihood (θ : Fin (n + 1) → ℝ) (s : Fin N → Fin (n + 1)) : ℝ≥0∞ :=
  ∏ m, ENNReal.ofReal (θ (s m))

Used by 5

Used byThe multinomial sampling model · Dirichlet–multinomial conjugacy · Posterior predictive of the Dirichlet–multinomial model · The sequence likelihood depends only on the label counts · Evidence-weighted Dirichlet prior

DefinitionThe multinomial sampling model#✓fully proved

For \(n, N \in \mathbb{N}\), the multinomial sampling model is the kernel from parameters \(\theta \in \mathbb{R}^{n+1}\) to sequences \(s = (s_0, \dots, s_{N-1})\) of \(N\) labels in \(\{0, \dots, n\}\) that sends a probability vector \(\theta\) (all \(\theta_i \ge 0\) and \(\sum_i \theta_i = 1\)) to the law of \(N\) independent draws from \(\theta\), which gives \(s\) probability \(\prod_{m < N} \theta_{s_m}\), and sends every other \(\theta\) to the point mass at the all-zero sequence.

noncomputable def categoricalSeqKernel (n N : ℕ) :
    Kernel (Fin (n + 1) → ℝ) (Fin N → Fin (n + 1)) :=
  Kernel.piecewise (measurableSet_probVectors n)
    ⟨fun θ ↦ ∑ s, seqLikelihood θ s • Measure.dirac s,
      Measure.measurable_of_measurable_coe _ fun A _ ↦ by
        simp only [Measure.coe_finsetSum, Finset.sum_apply, Measure.smul_apply, smul_eq_mul]
        exact Finset.measurable_sum _ fun s _ ↦ (measurable_seqLikelihood s).mul_const _⟩
    (Kernel.const _ (Measure.dirac fun _ : Fin N ↦ (0 : Fin (n + 1))))

Uses 2 · Used by 3

Statement usesProbability vectors · Likelihood of a label sequence

Used byDirichlet–multinomial conjugacy · Posterior predictive of the Dirichlet–multinomial model · Evidence-weighted Dirichlet prior

DefinitionLabel counts#✓fully proved

For a sequence \(s = (s_0, \dots, s_{N-1})\) of labels in \(\{0, \dots, n\}\) and a label \(i\), the count \(n_i(s)\) is the number of positions \(m < N\) with \(s_m = i\).

def counts (s : Fin N → Fin (n + 1)) (i : Fin (n + 1)) : ℕ :=
  (Finset.univ.filter fun m ↦ s m = i).card

Used by 4

Used byDirichlet–multinomial conjugacy · Posterior predictive of the Dirichlet–multinomial model · The sequence likelihood depends only on the label counts · Evidence-weighted Dirichlet prior

TheoremThe sequence likelihood depends only on the label counts#✓fully proved

For every \(\theta \in \mathbb{R}^{n+1}\) and every sequence \(s\) of \(N\) labels in \(\{0, \dots, n\}\) with label counts \(n_i(s)\), the likelihood \(\prod_{m < N} \theta_{s_m}^+\) of \(s\) equals \(\prod_{i = 0}^{n} (\theta_i^+)^{n_i(s)}\) as extended nonnegative reals, where \(x^+ = \max(x, 0)\).

theorem seqLikelihood_eq_prod_pow (θ : Fin (n + 1) → ℝ) (s : Fin N → Fin (n + 1)) :
    seqLikelihood θ s = ∏ i, ENNReal.ofReal (θ i) ^ counts s i

Uses 3 · Used by 1

Statement usesLabel counts · Likelihood of a label sequence

Proof usesProducts regrouped by the values of a function

Used byEvidence-weighted Dirichlet prior

TheoremEvidence-weighted Dirichlet prior#✓fully proved

Let \(\alpha \in \mathbb{R}^{n+1}\) with \(\alpha_i > 0\) for every \(i\), and let \(s\) be a sequence of \(N\) labels in \(\{0, \dots, n\}\) with label counts \(n_i(s)\). The Dirichlet distribution \(\mathrm{Dir}(\alpha)\) weighted by the density \(\theta \mapsto P_\theta(s)\), the probability of \(s\) under the multinomial sampling model with parameter \(\theta\), equals \(B(\alpha + n(s)) / B(\alpha)\) times \(\mathrm{Dir}(\alpha + n(s))\), where \(B\) is the multivariate Beta function and \(\alpha + n(s)\) has entries \(\alpha_i + n_i(s)\).

theorem withDensity_categoricalSeqKernel (hα : ∀ i, 0 < α i) (s : Fin N → Fin (n + 1)) :
    (dirichletMeasure α).withDensity (fun θ ↦ categoricalSeqKernel n N θ {s}) =
      ENNReal.ofReal (multiBeta (fun i ↦ α i + counts s i) / multiBeta α) •
        dirichletMeasure (fun i ↦ α i + counts s i)

Uses 9 · Used by 1

Statement usesThe multinomial sampling model · Label counts · Dirichlet distribution · Multivariate Beta function

Proof usesProbability vectors · Likelihood of a label sequence · The sequence likelihood depends only on the label counts · The Dirichlet distribution is concentrated on the open simplex · Dirichlet–multinomial conjugacy

Used byDirichlet–multinomial conjugacy

TheoremDirichlet–multinomial conjugacy#✓fully proved

Let \(\alpha \in \mathbb{R}^{n+1}\) with \(\alpha_i > 0\) for every \(i\), and let \(s\) be a sequence of \(N\) labels in \(\{0, \dots, n\}\) with label counts \(n_i(s)\). Under the multinomial sampling model with the Dirichlet prior \(\mathrm{Dir}(\alpha)\), the posterior distribution of the parameter after observing \(s\) is the Dirichlet distribution with parameters \(\alpha_i + n_i(s)\).

theorem posterior_categoricalSeqKernel_dirichletMeasure (hα : ∀ i, 0 < α i)
    (s : Fin N → Fin (n + 1)) :
    haveI := isProbabilityMeasure_dirichletMeasure hα
    ((categoricalSeqKernel n N)†(dirichletMeasure α)) s =
      dirichletMeasure (fun i ↦ α i + counts s i)

Uses 13 · Used by 1

Statement usesThe multinomial sampling model · Label counts · Probability vectors · Likelihood of a label sequence · Unnormalized Dirichlet density · Dirichlet distribution · The Dirichlet integral · Multivariate Beta function · Simplex completion

Proof usesBayes posterior · The evidence is the integral of the likelihood · Bayes' rule for discrete observations · Evidence-weighted Dirichlet prior

Used byPosterior predictive of the Dirichlet–multinomial model

TheoremPrior predictive of the Dirichlet–categorical model#✓fully proved

Let \(\alpha \in \mathbb{R}^{n+1}\) with \(\alpha_i > 0\) for every \(i\). Drawing a parameter \(\theta\) from the Dirichlet distribution \(\mathrm{Dir}(\alpha)\) and then one label from the categorical likelihood with parameter \(\theta\) gives the label \(i \in \{0, \dots, n\}\) with probability \(\alpha_i / \sum_j \alpha_j\), which is the mean of \(\theta_i\) under \(\mathrm{Dir}(\alpha)\).

theorem categoricalKernel_comp_dirichletMeasure (hα : ∀ i, 0 < α i) (i : Fin (n + 1)) :
    (categoricalKernel n ∘ₘ dirichletMeasure α) {i} = ENNReal.ofReal (α i / ∑ j, α j)

Uses 6 · Used by 1

Statement usesThe categorical likelihood · Dirichlet distribution

Proof usesThe evidence is the integral of the likelihood · Probability vectors · The Dirichlet distribution is concentrated on the open simplex · Mean of the Dirichlet distribution

Used byPosterior predictive of the Dirichlet–multinomial model

TheoremPosterior predictive of the Dirichlet–multinomial model#✓fully proved

Let \(\alpha \in \mathbb{R}^{n+1}\) with \(\alpha_i > 0\) for every \(i\), and let \(s\) be a sequence of \(N\) labels in \(\{0, \dots, n\}\) with label counts \(n_i(s)\). Under the multinomial sampling model with the Dirichlet prior \(\mathrm{Dir}(\alpha)\), drawing a parameter from the posterior after observing \(s\) and then one label from the categorical likelihood gives the label \(i\) with probability \((\alpha_i + n_i(s)) / (\sum_j \alpha_j + N)\).

This is the Dirichlet–multinomial analogue of Laplace's rule of succession.

theorem posterior_predictive_dirichletMeasure (hα : ∀ i, 0 < α i) (s : Fin N → Fin (n + 1))
    (i : Fin (n + 1)) :
    haveI := isProbabilityMeasure_dirichletMeasure hα
    (categoricalKernel n ∘ₘ ((categoricalSeqKernel n N)†(dirichletMeasure α)) s) {i} =
      ENNReal.ofReal ((α i + counts s i) / (∑ j, α j + N))

Uses 12

Statement usesThe categorical likelihood · The multinomial sampling model · Label counts · Probability vectors · Likelihood of a label sequence · Unnormalized Dirichlet density · Dirichlet distribution · The Dirichlet integral · Multivariate Beta function · Simplex completion

Proof usesPrior predictive of the Dirichlet–categorical model · Dirichlet–multinomial conjugacy

DefinitionPosterior variance of the normal–normal model#✓fully proved

For variances \(v_0, v \ge 0\), the posterior variance is \(\frac{v_0 v}{v_0 + v}\), taken to be \(0\) when \(v_0 = v = 0\). In the normal–normal model with prior variance \(v_0\) and known noise variance \(v\), this is the variance of the posterior of the mean after one observation.

noncomputable def normalPostVar (v₀ v : ℝ≥0) : ℝ≥0 := v₀ * v / (v₀ + v)

Used by 7

Used byDisintegration of the Normal–Normal joint law · The marginal of the data · Normal–Normal posterior predictive · Completing the square · Precisions add · Candidate posterior kernel of the normal–normal model · Normal–Normal conjugacy with known variance

DefinitionPosterior mean of the Normal–Normal model#✓fully proved

For a prior mean \(m_0 \in \mathbb{R}\), a prior variance \(v_0 \ge 0\), a noise variance \(v \ge 0\) and an observation \(x \in \mathbb{R}\), the posterior mean is \((v m_0 + v_0 x)/(v_0 + v)\), taken to be \(0\) when \(v_0 = v = 0\). When \(v_0 + v > 0\) it is the precision-weighted average of \(m_0\) and \(x\).

noncomputable def normalPostMean (m₀ : ℝ) (v₀ v : ℝ≥0) (x : ℝ) : ℝ :=
  (v * m₀ + v₀ * x) / (v₀ + v)

Used by 7

Used byDisintegration of the Normal–Normal joint law · The marginal of the data · Normal–Normal posterior predictive · Completing the square · Posterior mean as a gain update · Candidate posterior kernel of the normal–normal model · Normal–Normal conjugacy with known variance

TheoremPosterior mean as a gain update#✓fully proved

Let \(m_0, x \in \mathbb{R}\), \(v_0 > 0\) and \(v \ge 0\). The posterior mean \((v m_0 + v_0 x)/(v_0 + v)\) equals \(m_0 + \frac{v_0}{v_0 + v}(x - m_0)\): it moves from the prior mean \(m_0\) toward the observation \(x\) by the gain \(v_0/(v_0 + v)\).

theorem normalPostMean_eq (m₀ : ℝ) {v₀ v : ℝ≥0} (h₀ : v₀ ≠ 0) (x : ℝ) :
    normalPostMean m₀ v₀ v x = m₀ + v₀ / (v₀ + v) * (x - m₀)

Uses 1

Statement usesPosterior mean of the Normal–Normal model

TheoremPrecisions add#✓fully proved

For variances \(v_0, v > 0\), the posterior variance \(s = v_0 v/(v_0 + v)\) satisfies \(s^{-1} = v_0^{-1} + v^{-1}\).

theorem inv_normalPostVar {v₀ v : ℝ≥0} (h₀ : v₀ ≠ 0) (h : v ≠ 0) :
    (normalPostVar v₀ v)⁻¹ = v₀⁻¹ + v⁻¹

Uses 1

Statement usesPosterior variance of the normal–normal model

TheoremCompleting the square#✓fully proved

Let \(m_0, \theta, x \in \mathbb{R}\) and \(v_0, v > 0\), and write \(\varphi_{\mu, s}(y) = (2 \pi s)^{-1/2} \exp(-(y - \mu)^2 / (2 s))\) for the density of the Gaussian with mean \(\mu\) and variance \(s\). With \(\mu(x) = (v m_0 + v_0 x)/(v_0 + v)\) and \(s = v_0 v/(v_0 + v)\),

\[ \varphi_{m_0, v_0}(\theta)\,\varphi_{\theta, v}(x) = \varphi_{m_0, v_0 + v}(x)\,\varphi_{\mu(x), s}(\theta): \]

the prior density at \(\theta\) times the likelihood of \(x\) is the marginal density of \(x\) times the posterior density at \(\theta\).

theorem gaussianPDFReal_mul_gaussianPDFReal (m₀ : ℝ) {v₀ v : ℝ≥0} (h₀ : v₀ ≠ 0) (h : v ≠ 0)
    (θ x : ℝ) :
    gaussianPDFReal m₀ v₀ θ * gaussianPDFReal θ v x =
      gaussianPDFReal m₀ (v₀ + v) x *
        gaussianPDFReal (normalPostMean m₀ v₀ v x) (normalPostVar v₀ v) θ

Uses 2 · Used by 3

Statement usesPosterior mean of the Normal–Normal model · Posterior variance of the normal–normal model

Used byDisintegration of the Normal–Normal joint law · The marginal of the data · Normal–Normal conjugacy with known variance

TheoremMeasurability of the Gaussian density in its mean and argument#✓fully proved

For a variance \(v \ge 0\), write \(\varphi_{\theta, v}(x) = (2 \pi v)^{-1/2} \exp(-(x - \theta)^2 / (2 v))\) for the density at \(x\) of the Gaussian with mean \(\theta\) and variance \(v\), read as \(0\) when \(v = 0\), with values in \([0, \infty]\). Then \((\theta, x) \mapsto \varphi_{\theta, v}(x)\) is a measurable map on \(\mathbb{R} \times \mathbb{R}\).

theorem measurable_gaussianPDF_mean (v : ℝ≥0) :
    Measurable (Function.uncurry fun θ x : ℝ ↦ gaussianPDF θ v x)

Used by 5

Used byPosterior predictive at a new input · Disintegration of the Normal–Normal joint law · The marginal of the data · Normal–Normal posterior predictive · Normal–Normal conjugacy with known variance

DefinitionGaussian likelihood with known variance#✓fully proved

For a noise variance \(v \ge 0\), the Gaussian likelihood is the kernel from \(\mathbb{R}\) to \(\mathbb{R}\) that sends a parameter \(\theta\) to the law of the observation \(x \sim N(\theta, v)\), the Gaussian with mean \(\theta\) and variance \(v\): for \(v > 0\) it is the measure with the \(N(\theta, v)\) density with respect to Lebesgue measure, and for \(v = 0\) it is the point mass at \(\theta\).

noncomputable def gaussianLikelihood (v : ℝ≥0) : Kernel ℝ ℝ :=
  if v = 0 then Kernel.deterministic id measurable_id
  else (Kernel.const ℝ volume).withDensity fun θ x ↦ gaussianPDF θ v x

Used by 7

Used byPredictive law of a linear-regression response · Posterior predictive at a new input · Disintegration of the Normal–Normal joint law · The marginal of the data · Normal–Normal posterior predictive · Noiseless Gaussian likelihood · Normal–Normal conjugacy with known variance

TheoremNoiseless Gaussian likelihood#✓fully proved

With noise variance \(0\), the Gaussian likelihood sends each \(\theta \in \mathbb{R}\) to the Gaussian law with mean \(\theta\) and variance \(0\), which is the point mass at \(\theta\): the observation is the parameter.

theorem gaussianLikelihood_zero_apply (θ : ℝ) : gaussianLikelihood 0 θ = gaussianReal θ 0

Uses 1 · Used by 3

Statement usesGaussian likelihood with known variance

Used byDisintegration of the Normal–Normal joint law · Normal–Normal posterior predictive · Normal–Normal conjugacy with known variance

TheoremThe marginal of the data#✓fully proved

Let \(m_0 \in \mathbb{R}\) and \(v_0, v > 0\), and write \(N(\mu, s)\) for the Gaussian law with mean \(\mu\) and variance \(s\). If the parameter \(\theta\) has prior \(N(m_0, v_0)\) and the observation given \(\theta\) has law \(N(\theta, v)\) (the Gaussian likelihood with noise variance \(v\)), then the marginal law of the observation is \(N(m_0, v_0 + v)\).

Applied with the posterior in place of the prior, this also gives the posterior predictive law.

theorem gaussianLikelihood_comp_gaussianReal (m₀ : ℝ) {v₀ v : ℝ≥0} (h₀ : v₀ ≠ 0) (h : v ≠ 0) :
    gaussianLikelihood v ∘ₘ gaussianReal m₀ v₀ = gaussianReal m₀ (v₀ + v)

Uses 6 · Used by 3

Statement usesGaussian likelihood with known variance

Proof usesThe evidence from a factorization of densities · Completing the square · Measurability of the Gaussian density in its mean and argument · Posterior mean of the Normal–Normal model · Posterior variance of the normal–normal model

Used byPosterior predictive at a new input · Normal–Normal posterior predictive · Normal–Normal conjugacy with known variance

DefinitionCandidate posterior kernel of the normal–normal model#✓fully proved

Let \(m_0 \in \mathbb{R}\) and \(v_0, v \ge 0\), let \(s = \frac{v_0 v}{v_0 + v}\) be the posterior variance and, for \(x \in \mathbb{R}\), let \(\mu(x) = \frac{v m_0 + v_0 x}{v_0 + v}\) be the posterior mean (with \(0 / 0 = 0\)). The kernel from \(\mathbb{R}\) to \(\mathbb{R}\) sends \(x\) to the measure with density \(\theta \mapsto \frac{1}{\sqrt{2 \pi s}} e^{-(\theta - \mu(x))^2 / (2 s)}\) with respect to Lebesgue measure. For \(v_0, v > 0\) this is the normal law \(N(\mu(x), s)\). If \(v_0 = 0\) or \(v = 0\), then \(s = 0\), the density is taken to be \(0\), and the kernel is the zero measure at every \(x\).

noncomputable def normalPosteriorKernel (m₀ : ℝ) (v₀ v : ℝ≥0) : Kernel ℝ ℝ :=
  (Kernel.const ℝ volume).withDensity fun x θ ↦
    gaussianPDF (normalPostMean m₀ v₀ v x) (normalPostVar v₀ v) θ

Uses 2 · Used by 1

Statement usesPosterior mean of the Normal–Normal model · Posterior variance of the normal–normal model

Used byDisintegration of the Normal–Normal joint law

TheoremDisintegration of the Normal–Normal joint law#✓fully proved

Let \(m_0 \in \mathbb{R}\) and \(v_0, v > 0\), and write \(N(\mu, s)\) for the Gaussian law with mean \(\mu\) and variance \(s\). Let \(\pi = N(m_0, v_0)\) be the prior on the parameter \(\theta\), let \(K\) be the Gaussian likelihood with noise variance \(v\), so that \(K(\theta) = N(\theta, v)\), and let \(Q\) be the normal posterior kernel, \(Q(x) = N(\mu(x), s)\) with \(\mu(x) = (v m_0 + v_0 x)/(v_0 + v)\) and \(s = v_0 v/(v_0 + v)\). For a measure \(\rho\) and a kernel \(L\), write \(L \circ \rho = \int L(y)\,d\rho(y)\) and \(\rho \otimes L\) for the law of \((y, z)\) when \(y \sim \rho\) and \(z \sim L(y)\). Then \((K \circ \pi) \otimes Q\) is the image of \(\pi \otimes K\) under \((\theta, x) \mapsto (x, \theta)\): the joint law of \((x, \theta)\) is the marginal law \(K \circ \pi\) of \(x\) followed by the posterior kernel.

theorem compProd_normalPosteriorKernel (m₀ : ℝ) {v₀ v : ℝ≥0} [NeZero v₀] [NeZero v] :
    (gaussianLikelihood v ∘ₘ gaussianReal m₀ v₀) ⊗ₘ normalPosteriorKernel m₀ v₀ v =
      (gaussianReal m₀ v₀ ⊗ₘ gaussianLikelihood v).map Prod.swap

Uses 8

Statement usesGaussian likelihood with known variance · Candidate posterior kernel of the normal–normal model

Proof usesDisintegration of the joint law from a factorization of densities · Noiseless Gaussian likelihood · Completing the square · Measurability of the Gaussian density in its mean and argument · Posterior mean of the Normal–Normal model · Posterior variance of the normal–normal model

TheoremNormal–Normal conjugacy with known variance#✓fully proved

Let \(m_0 \in \mathbb{R}\) and \(v_0, v > 0\). Take the prior \(N(m_0, v_0)\) on the mean \(\theta\) and the likelihood under which an observation \(x\) has law \(N(\theta, v)\). Then for Lebesgue-almost every \(x \in \mathbb{R}\), the posterior distribution of \(\theta\) given \(x\) is the normal law with mean \(\frac{v m_0 + v_0 x}{v_0 + v}\) and variance \(\frac{v_0 v}{v_0 + v}\).

theorem posterior_gaussianLikelihood_gaussianReal (m₀ : ℝ) {v₀ v : ℝ≥0} [NeZero v₀] [NeZero v] :
    ∀ᵐ x, ((gaussianLikelihood v)†(gaussianReal m₀ v₀)) x =
      gaussianReal (normalPostMean m₀ v₀ v x) (normalPostVar v₀ v)

Uses 8 · Used by 1

Statement usesGaussian likelihood with known variance · Noiseless Gaussian likelihood · Measurability of the Gaussian density in its mean and argument · Posterior mean of the Normal–Normal model · Posterior variance of the normal–normal model

Proof usesThe marginal of the data · Completing the square · Bayes' rule for densities

Used byNormal–Normal posterior predictive

TheoremNormal–Normal posterior predictive#✓fully proved

Let \(m_0 \in \mathbb{R}\) and \(v_0, v > 0\), and write \(N(\mu, s)\) for the Gaussian law with mean \(\mu\) and variance \(s\). Take the prior \(N(m_0, v_0)\) on the parameter \(\theta\) and the Gaussian likelihood \(\theta \mapsto N(\theta, v)\), and let \(\mu(x) = (v m_0 + v_0 x)/(v_0 + v)\) and \(s = v_0 v/(v_0 + v)\). For Lebesgue-almost every observation \(x\), a new observation drawn from the likelihood, with \(\theta\) distributed according to the posterior given \(x\), has law \(N(\mu(x), s + v)\).

theorem gaussianLikelihood_comp_posterior (m₀ : ℝ) {v₀ v : ℝ≥0} [NeZero v₀] [NeZero v] :
    ∀ᵐ x, gaussianLikelihood v ∘ₘ ((gaussianLikelihood v)†(gaussianReal m₀ v₀)) x =
      gaussianReal (normalPostMean m₀ v₀ v x) (normalPostVar v₀ v + v)

Uses 7

Statement usesGaussian likelihood with known variance · Noiseless Gaussian likelihood · Measurability of the Gaussian density in its mean and argument · Posterior mean of the Normal–Normal model · Posterior variance of the normal–normal model

Proof usesThe marginal of the data · Normal–Normal conjugacy with known variance

31 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.