Bayes' rule

DefinitionBayes posterior#✓fully proved

Let \(\kappa\) be a kernel from a measurable space \(\Theta\) of hypotheses to a measurable space \(\mathcal X\) of observations (the likelihood) and \(\mu\) a measure on \(\Theta\) (the prior). The Bayes posterior after observing \(x \in \mathcal X\) is the measure \(\pi_x\) on \(\Theta\) with

\[\pi_x(s) = E(x)^{-1} \int_s \kappa_\theta(\{x\}) \, d\mu(\theta)\]

for every measurable \(s \subseteq \Theta\), where \(E(x) = (\kappa \circ \mu)(\{x\})\) is the evidence of \(x\): the mass of \(\{x\}\) under the composition \(\kappa \circ \mu\) of \(\mu\) with \(\kappa\), the marginal law of the observation. The inverse is taken in \([0, \infty]\), with \(0^{-1} = \infty\), \(\infty^{-1} = 0\) and \(\infty \cdot 0 = 0\); in particular \(\pi_x\) is the zero measure when the evidence is zero.

noncomputable def bayesPosterior (κ : Kernel Θ 𝓧) (μ : Measure Θ) (x : 𝓧) : Measure Θ :=
  ((κ ∘ₘ μ) {x})⁻¹ • μ.withDensity fun θ ↦ κ θ {x}

Used by 10

Used byBayes posterior kernel · Bayes' rule for countably many hypotheses · Evidence times posterior is the joint mass · Maximum a posteriori hypothesis · MAP hypotheses maximize prior times likelihood · MAP hypotheses through the posterior kernel · Bayes' rule for Mathlib's posterior kernel with countably many hypotheses and observations · Bayes' rule for discrete observations · Beta–binomial conjugacy · Dirichlet–multinomial conjugacy

TheoremThe evidence is the integral of the likelihood#✓fully proved

Let \(\kappa\) be a kernel from a measurable space \(\Theta\) to a measurable space \(\mathcal X\) with measurable singletons, and \(\mu\) a measure on \(\Theta\). For every \(x \in \mathcal X\),

\[(\kappa \circ \mu)(\{x\}) = \int_\Theta \kappa_\theta(\{x\}) \, d\mu(\theta),\]

where \(\kappa \circ \mu\) is the composition of \(\mu\) with \(\kappa\) (the marginal law of the observation) and the right side is the Lebesgue integral of a \([0, \infty]\)-valued function.

theorem comp_apply_singleton [MeasurableSingletonClass 𝓧] (κ : Kernel Θ 𝓧) (μ : Measure Θ)
    (x : 𝓧) : (κ ∘ₘ μ) {x} = ∫⁻ θ, κ θ {x} ∂μ

Used by 6

Used byThe evidence as a sum over hypotheses · Evidence times posterior is the joint mass · Bayes' rule for discrete observations · The beta-binomial distribution · Prior predictive of the Dirichlet–categorical model · Dirichlet–multinomial conjugacy

TheoremEvidence times posterior is the joint mass#✓fully proved

Let \(\mathcal X\) be a measurable space with measurable singletons, \(\kappa\) a Markov kernel from a measurable space \(\Theta\) to \(\mathcal X\) and \(\mu\) a finite measure on \(\Theta\). Let \(x \in \mathcal X\) and write \(\pi_x\) for the Bayes posterior of \(\mu\) after observing \(x\) under \(\kappa\). Then for every measurable set \(s \subseteq \Theta\),

\[(\kappa \circ \mu)(\{x\}) \cdot \pi_x(s) = \int_s \kappa_\theta(\{x\}) \, d\mu(\theta),\]

where \(\kappa \circ \mu\) is the composition of \(\mu\) with \(\kappa\), so that the first factor is the evidence of \(x\).

theorem comp_mul_bayesPosterior [MeasurableSingletonClass 𝓧] (κ : Kernel Θ 𝓧) [IsMarkovKernel κ]
    (μ : Measure Θ) [IsFiniteMeasure μ] (x : 𝓧) {s : Set Θ} (hs : MeasurableSet s) :
    (κ ∘ₘ μ) {x} * bayesPosterior κ μ x s = ∫⁻ θ in s, κ θ {x} ∂μ

Uses 2 · Used by 1

Statement usesBayes posterior

Proof usesThe evidence is the integral of the likelihood

Used byBayes' rule for discrete observations

DefinitionMaximum-likelihood hypothesis for a discrete observation#✓fully proved

Let \(\kappa\) be a kernel from a parameter space \(\Theta\) to a countable observation space \(\mathcal X\) with measurable singletons, assigning to each hypothesis \(\theta\) a measure \(\kappa_\theta\) on \(\mathcal X\). A hypothesis \(\theta \in \Theta\) is a maximum-likelihood hypothesis for the observation \(x \in \mathcal X\) when no hypothesis gives \(x\) higher likelihood: \(\kappa_{\theta'}(\{x\}) \le \kappa_\theta(\{x\})\) for every \(\theta' \in \Theta\).

@[nolint unusedArguments]
def IsMLE [Countable 𝓧] [MeasurableSingletonClass 𝓧] (κ : Kernel Θ 𝓧) (x : 𝓧) (θ : Θ) : Prop :=
  ∀ θ', κ θ' {x} ≤ κ θ {x}

Used by 1

Used byUnder a uniform prior, MAP is maximum likelihood

DefinitionMaximum a posteriori hypothesis#✓fully proved

Let \(\Theta\) and \(\mathcal X\) be countable measurable spaces with measurable singletons, \(\kappa\) a kernel from \(\Theta\) to \(\mathcal X\) and \(\mu\) a measure on \(\Theta\), and write \(\pi_x\) for the Bayes posterior of the prior \(\mu\) after observing \(x \in \mathcal X\) under the likelihood \(\kappa\). A hypothesis \(\theta \in \Theta\) is a maximum a posteriori (MAP) hypothesis for \(x\) when \(\pi_x(\{\theta'\}) \le \pi_x(\{\theta\})\) for every \(\theta' \in \Theta\).

@[nolint unusedArguments]
def IsMAP [Countable Θ] [MeasurableSingletonClass Θ] [Countable 𝓧] [MeasurableSingletonClass 𝓧]
    (κ : Kernel Θ 𝓧) (μ : Measure Θ) (x : 𝓧) (θ : Θ) : Prop :=
  ∀ θ', bayesPosterior κ μ x {θ'} ≤ bayesPosterior κ μ x {θ}

Uses 1 · Used by 4

Statement usesBayes posterior

Used byMAP hypotheses maximize prior times likelihood · Under a uniform prior, MAP is maximum likelihood · MAP hypotheses through the posterior kernel · MAP classifiers are posterior argmax classifiers

DefinitionBayes posterior kernel#✓fully proved

Let \(\mathcal X\) be a countable measurable space with measurable singletons, \(\kappa\) a kernel from a measurable space \(\Theta\) to \(\mathcal X\), and \(\mu\) a measure on \(\Theta\). The Bayes posterior kernel is the kernel from \(\mathcal X\) to \(\Theta\) that sends each observation \(x \in \mathcal X\) to the Bayes posterior of the prior \(\mu\) after observing \(x\) under the likelihood \(\kappa\).

noncomputable def bayesKernel (κ : Kernel Θ 𝓧) (μ : Measure Θ) : Kernel 𝓧 Θ :=
  Kernel.ofFunOfCountable (bayesPosterior κ μ)

Uses 1 · Used by 1

Statement usesBayes posterior

Used byBayes' rule for discrete observations

TheoremBayes' rule for discrete observations#✓fully proved

Let the parameter space \(\Theta\) be a nonempty standard Borel space and the observation space \(\mathcal X\) be countable with measurable singletons. Let \(\kappa\) be a Markov kernel from \(\Theta\) to \(\mathcal X\) (the likelihood), writing \(\kappa_\theta\) for the probability measure it assigns to \(\theta \in \Theta\), let \(\mu\) be a finite measure on \(\Theta\) (the prior), and let \(\kappa^\dagger\mu\) be Mathlib's posterior kernel from \(\mathcal X\) to \(\Theta\). If the observation \(x \in \mathcal X\) has nonzero evidence \((\kappa \circ \mu)(\{x\})\), where \(\kappa \circ \mu\) is the law of the observation under the prior, then the posterior measure \(\kappa^\dagger\mu(x)\) equals the Bayes posterior after observing \(x\): the prior \(\mu\) reweighted by the likelihood \(\theta \mapsto \kappa_\theta(\{x\})\) and divided by the evidence.

theorem posterior_eq_bayesPosterior (κ : Kernel Θ 𝓧) [IsMarkovKernel κ] (μ : Measure Θ)
    [IsFiniteMeasure μ] {x : 𝓧} (hx : (κ ∘ₘ μ) {x} ≠ 0) :
    (κ†μ) x = bayesPosterior κ μ x

Uses 4 · Used by 4

Statement usesBayes posterior

Proof usesBayes posterior kernel · The evidence is the integral of the likelihood · Evidence times posterior is the joint mass

Used byMAP hypotheses through the posterior kernel · Bayes' rule for Mathlib's posterior kernel with countably many hypotheses and observations · Beta–binomial conjugacy · Dirichlet–multinomial conjugacy

TheoremThe evidence as a sum over hypotheses#✓fully proved

Let \(\Theta\) be a countable measurable space and \(\mathcal X\) a measurable space, both with measurable singletons, let \(\kappa\) be a kernel from \(\Theta\) to \(\mathcal X\) and \(\mu\) a measure on \(\Theta\). For every \(x \in \mathcal X\),

\[(\kappa \circ \mu)(\{x\}) = \sum_{\theta \in \Theta} \mu(\{\theta\}) \, \kappa_\theta(\{x\}),\]

where \(\kappa \circ \mu\) is the composition of \(\mu\) with \(\kappa\) (the marginal law of the observation) and the sum is taken in \([0, \infty]\).

theorem comp_apply_singleton_eq_tsum (κ : Kernel Θ 𝓧) (μ : Measure Θ) (x : 𝓧) :
    (κ ∘ₘ μ) {x} = ∑' θ, μ {θ} * κ θ {x}

Uses 1 · Used by 2

Proof usesThe evidence is the integral of the likelihood

Used byBayes' rule for countably many hypotheses · MAP hypotheses maximize prior times likelihood

TheoremBayes' rule for countably many hypotheses#✓fully proved

Let \(\Theta\) be a countable measurable space and \(\mathcal X\) a measurable space, both with measurable singletons, let \(\kappa\) be a kernel from \(\Theta\) to \(\mathcal X\) (the likelihood) and \(\mu\) a measure on \(\Theta\) (the prior). For every observation \(x \in \mathcal X\) and every \(\theta \in \Theta\), the Bayes posterior \(\pi_x\) of \(\mu\) after observing \(x\) satisfies

\[\pi_x(\{\theta\}) = \frac{\mu(\{\theta\}) \, \kappa_\theta(\{x\})} {\sum_{\theta' \in \Theta} \mu(\{\theta'\}) \, \kappa_{\theta'}(\{x\})},\]

where the quotient is taken in \([0, \infty]\) with \(0 / 0 = 0\) and \(a / \infty = 0\) for every \(a\). The denominator is the evidence of \(x\).

theorem bayesPosterior_apply_singleton (κ : Kernel Θ 𝓧) (μ : Measure Θ) (x : 𝓧) (θ : Θ) :
    bayesPosterior κ μ x {θ} = μ {θ} * κ θ {x} / ∑' θ', μ {θ'} * κ θ' {x}

Uses 2 · Used by 2

Statement usesBayes posterior

Proof usesThe evidence as a sum over hypotheses

Used byMAP hypotheses maximize prior times likelihood · Bayes' rule for Mathlib's posterior kernel with countably many hypotheses and observations

TheoremBayes' rule for Mathlib's posterior kernel with countably many hypotheses and observations#✓fully proved

Bayes' rule for Mathlib's posterior kernel with countably many hypotheses and observations. Let the parameter space \(\Theta\) be a nonempty countable standard Borel space and the observation space \(\mathcal X\) be countable, both with measurable singletons. Let \(\kappa\) be a Markov kernel from \(\Theta\) to \(\mathcal X\) (the likelihood), writing \(\kappa_\theta\) for the probability measure it assigns to \(\theta \in \Theta\), let \(\mu\) be a finite measure on \(\Theta\) (the prior), and let \(\kappa^\dagger\mu\) be Mathlib's posterior kernel from \(\mathcal X\) to \(\Theta\). If the observation \(x \in \mathcal X\) has nonzero evidence \((\kappa \circ \mu)(\{x\})\), where \(\kappa \circ \mu\) is the law of the observation under the prior, then for every \(\theta \in \Theta\)

\[ \kappa^\dagger\mu(x)(\{\theta\}) = \frac{\mu(\{\theta\})\,\kappa_\theta(\{x\})} {\sum_{\theta' \in \Theta} \mu(\{\theta'\})\,\kappa_{\theta'}(\{x\})}. \]

theorem posterior_apply_singleton (κ : Kernel Θ 𝓧) [IsMarkovKernel κ] (μ : Measure Θ)
    [IsFiniteMeasure μ] {x : 𝓧} (hx : (κ ∘ₘ μ) {x} ≠ 0) (θ : Θ) :
    (κ†μ) x {θ} = μ {θ} * κ θ {x} / ∑' θ', μ {θ'} * κ θ' {x}

Uses 3

Proof usesBayes posterior · Bayes' rule for countably many hypotheses · Bayes' rule for discrete observations

TheoremMAP hypotheses maximize prior times likelihood#✓fully proved

Let \(\Theta\) and \(\mathcal X\) be countable measurable spaces with measurable singletons, \(\kappa\) a Markov kernel from \(\Theta\) to \(\mathcal X\), \(\mu\) a finite measure on \(\Theta\), and \(x \in \mathcal X\) an observation with \((\kappa \circ \mu)(\{x\}) \neq 0\), where \(\kappa \circ \mu\) is the composition of \(\mu\) with \(\kappa\). Then \(\theta \in \Theta\) is a MAP hypothesis for \(x\) under the prior \(\mu\) and the likelihood \(\kappa\) if and only if \(\mu(\{\theta'\}) \, \kappa_{\theta'}(\{x\}) \le \mu(\{\theta\}) \, \kappa_\theta(\{x\})\) for every \(\theta' \in \Theta\).

The evidence \((\kappa \circ \mu)(\{x\})\) is a common factor of all posterior masses.

theorem isMAP_iff (κ : Kernel Θ 𝓧) [IsMarkovKernel κ] (μ : Measure Θ) [IsFiniteMeasure μ]
    {x : 𝓧} (hx : (κ ∘ₘ μ) {x} ≠ 0) (θ : Θ) :
    IsMAP κ μ x θ ↔ ∀ θ', μ {θ'} * κ θ' {x} ≤ μ {θ} * κ θ {x}

Uses 4 · Used by 1

Statement usesMaximum a posteriori hypothesis

Proof usesBayes posterior · Bayes' rule for countably many hypotheses · The evidence as a sum over hypotheses

Used byUnder a uniform prior, MAP is maximum likelihood

TheoremUnder a uniform prior, MAP is maximum likelihood#✓fully proved

Let \(\Theta\) and \(\mathcal X\) be countable measurable spaces with measurable singletons, \(\kappa\) a Markov kernel from \(\Theta\) to \(\mathcal X\), and \(\mu\) a finite measure on \(\Theta\) that is uniform: there is \(c \in [0, \infty]\), \(c \neq 0\), with \(\mu(\{\theta\}) = c\) for every \(\theta \in \Theta\). Let \(x \in \mathcal X\) be an observation with \((\kappa \circ \mu)(\{x\}) \neq 0\), where \(\kappa \circ \mu\) is the composition of \(\mu\) with \(\kappa\). Then a hypothesis \(\theta \in \Theta\) is a MAP hypothesis for \(x\) under the prior \(\mu\) and the likelihood \(\kappa\) if and only if it is a maximum-likelihood hypothesis for \(x\) under \(\kappa\).

theorem isMAP_iff_isMLE_of_uniform (κ : Kernel Θ 𝓧) [IsMarkovKernel κ] (μ : Measure Θ)
    [IsFiniteMeasure μ] {c : ℝ≥0∞} (hμ : ∀ θ, μ {θ} = c) (hc : c ≠ 0) {x : 𝓧}
    (hx : (κ ∘ₘ μ) {x} ≠ 0) (θ : Θ) : IsMAP κ μ x θ ↔ IsMLE κ x θ

Uses 3

Statement usesMaximum a posteriori hypothesis · Maximum-likelihood hypothesis for a discrete observation

Proof usesMAP hypotheses maximize prior times likelihood

TheoremMAP hypotheses through the posterior kernel#✓fully proved

Let \(\Theta\) be a nonempty countable standard Borel space, \(\mathcal X\) a countable measurable space with measurable singletons, \(\kappa\) a Markov kernel from \(\Theta\) to \(\mathcal X\), \(\mu\) a finite measure on \(\Theta\), and \(x \in \mathcal X\) an observation with \((\kappa \circ \mu)(\{x\}) \neq 0\), where \(\kappa \circ \mu\) is the composition of \(\mu\) with \(\kappa\). Write \(\kappa^\dagger_\mu\) for the posterior kernel from \(\mathcal X\) to \(\Theta\), the fixed disintegration of the joint law of hypothesis and observation along the observation. Then \(\theta \in \Theta\) is a MAP hypothesis for \(x\) under the prior \(\mu\) and the likelihood \(\kappa\) if and only if \(\kappa^\dagger_\mu(x)(\{\theta'\}) \le \kappa^\dagger_\mu(x)(\{\theta\})\) for every \(\theta' \in \Theta\).

theorem isMAP_iff_posterior (κ : Kernel Θ 𝓧) [IsMarkovKernel κ] (μ : Measure Θ)
    [IsFiniteMeasure μ] {x : 𝓧} (hx : (κ ∘ₘ μ) {x} ≠ 0) (θ : Θ) :
    IsMAP κ μ x θ ↔ ∀ θ', (κ†μ) x {θ'} ≤ (κ†μ) x {θ}

Uses 3 · Used by 1

Statement usesMaximum a posteriori hypothesis

Proof usesBayes posterior · Bayes' rule for discrete observations

Used byMAP classifiers are posterior argmax classifiers

TheoremThe evidence from a factorization of densities#✓fully proved

Let \(\nu\) be an s-finite measure on a measurable space \(\Theta\) and \(\rho\) an s-finite measure on a measurable space \(\mathcal{X}\). Let \(p : \Theta \to [0, \infty]\), \(q : \Theta \times \mathcal{X} \to [0, \infty]\), \(c : \mathcal{X} \to [0, \infty]\) and \(r : \mathcal{X} \times \Theta \to [0, \infty]\) be measurable functions such that \(\int r(x, \theta) \, d\nu(\theta) = 1\) for every \(x \in \mathcal{X}\) and \(p(\theta) \, q(\theta, x) = c(x) \, r(x, \theta)\) for all \(\theta \in \Theta\) and \(x \in \mathcal{X}\). If the prior \(\mu\) is the measure on \(\Theta\) with density \(p\) with respect to \(\nu\), and the likelihood \(\kappa\) is a kernel from \(\Theta\) to \(\mathcal{X}\) such that each \(\kappa(\theta)\) has density \(q(\theta, \cdot)\) with respect to \(\rho\), then the marginal law of the data, the measure \(\kappa \circ \mu\) on \(\mathcal{X}\) given by \((\kappa \circ \mu)(s) = \int \kappa(\theta)(s) \, d\mu(\theta)\) for measurable \(s\), has density \(c\) with respect to \(\rho\).

theorem comp_eq_withDensity_of_mul_eq (hμ : μ = ν.withDensity p)
    (hκ : ∀ θ, κ θ = ρ.withDensity (q θ)) (hp : Measurable p) (hq : Measurable (Function.uncurry q))
    (hc : Measurable c) (hr : Measurable (Function.uncurry r)) (hr1 : ∀ x, ∫⁻ θ, r x θ ∂ν = 1)
    (hfac : ∀ θ x, p θ * q θ x = c x * r x θ) :
    κ ∘ₘ μ = ρ.withDensity c

Used by 3

Used byDisintegration of the joint law from a factorization of densities · The evidence of Bayesian linear regression · The marginal of the data

TheoremDisintegration of the joint law from a factorization of densities#✓fully proved

Let \(\nu\) be an s-finite measure on a measurable space \(\Theta\) and \(\rho\) an s-finite measure on a measurable space \(\mathcal{X}\). Let \(p : \Theta \to [0, \infty]\), \(q : \Theta \times \mathcal{X} \to [0, \infty]\), \(c : \mathcal{X} \to [0, \infty]\) and \(r : \mathcal{X} \times \Theta \to [0, \infty]\) be measurable functions such that \(\int r(x, \theta) \, d\nu(\theta) = 1\) for every \(x \in \mathcal{X}\) and \(p(\theta) \, q(\theta, x) = c(x) \, r(x, \theta)\) for all \(\theta \in \Theta\) and \(x \in \mathcal{X}\). Let the prior \(\mu\) be an s-finite measure on \(\Theta\) with density \(p\) with respect to \(\nu\), let the likelihood \(\kappa\) be an s-finite kernel from \(\Theta\) to \(\mathcal{X}\) such that each \(\kappa(\theta)\) has density \(q(\theta, \cdot)\) with respect to \(\rho\), and let \(\eta\) be an s-finite kernel from \(\mathcal{X}\) to \(\Theta\) such that each \(\eta(x)\) has density \(r(x, \cdot)\) with respect to \(\nu\). Write \(\kappa \circ \mu\) for the marginal law of the data, \((\kappa \circ \mu)(s) = \int \kappa(\theta)(s) \, d\mu(\theta)\), and \(\mu \otimes \kappa\) for the joint law on \(\Theta \times \mathcal{X}\), \((\mu \otimes \kappa)(t) = \int \kappa(\theta)(\{x : (\theta, x) \in t\}) \, d\mu(\theta)\), and similarly \((\kappa \circ \mu) \otimes \eta\) on \(\mathcal{X} \times \Theta\). Then \((\kappa \circ \mu) \otimes \eta\) is the image of \(\mu \otimes \kappa\) under the swap \((\theta, x) \mapsto (x, \theta)\).

theorem compProd_eq_of_mul_eq [SFinite μ] [IsSFiniteKernel κ] [IsSFiniteKernel η]
    (hμ : μ = ν.withDensity p)
    (hκ : ∀ θ, κ θ = ρ.withDensity (q θ)) (hη : ∀ x, η x = ν.withDensity (r x))
    (hp : Measurable p) (hq : Measurable (Function.uncurry q)) (hc : Measurable c)
    (hr : Measurable (Function.uncurry r)) (hr1 : ∀ x, ∫⁻ θ, r x θ ∂ν = 1)
    (hfac : ∀ θ x, p θ * q θ x = c x * r x θ) :
    (κ ∘ₘ μ) ⊗ₘ η = (μ ⊗ₘ κ).map Prod.swap

Uses 1 · Used by 2

Proof usesThe evidence from a factorization of densities

Used byBayes' rule for densities · Disintegration of the Normal–Normal joint law

TheoremBayes' rule for densities#✓fully proved

Let \(\Theta\) be a nonempty standard Borel space, \(\nu\) an s-finite measure on \(\Theta\) and \(\rho\) an s-finite measure on a measurable space \(\mathcal{X}\). Let \(p : \Theta \to [0, \infty]\), \(q : \Theta \times \mathcal{X} \to [0, \infty]\), \(c : \mathcal{X} \to [0, \infty]\) and \(r : \mathcal{X} \times \Theta \to [0, \infty]\) be measurable functions such that \(\int r(x, \theta) \, d\nu(\theta) = 1\) for every \(x \in \mathcal{X}\) and \(p(\theta) \, q(\theta, x) = c(x) \, r(x, \theta)\) for all \(\theta \in \Theta\) and \(x \in \mathcal{X}\). Let the prior \(\mu\) be a finite measure on \(\Theta\) with density \(p\) with respect to \(\nu\), and let the likelihood \(\kappa\) be a Markov kernel from \(\Theta\) to \(\mathcal{X}\) such that each \(\kappa(\theta)\) has density \(q(\theta, \cdot)\) with respect to \(\rho\). Then for almost every \(x\) with respect to the marginal law of the data \(\kappa \circ \mu\), given by \((\kappa \circ \mu)(s) = \int \kappa(\theta)(s) \, d\mu(\theta)\), the posterior \(\kappa^\dagger_\mu(x)\) of \(\kappa\) with respect to \(\mu\) is the measure with density \(r(x, \cdot)\) with respect to \(\nu\).

theorem posterior_ae_eq_of_mul_eq [StandardBorelSpace Θ] [Nonempty Θ] [IsFiniteMeasure μ]
    [IsMarkovKernel κ] (hμ : μ = ν.withDensity p) (hκ : ∀ θ, κ θ = ρ.withDensity (q θ))
    (hp : Measurable p) (hq : Measurable (Function.uncurry q)) (hc : Measurable c)
    (hr : Measurable (Function.uncurry r)) (hr1 : ∀ x, ∫⁻ θ, r x θ ∂ν = 1)
    (hfac : ∀ θ x, p θ * q θ x = c x * r x θ) :
    ∀ᵐ x ∂(κ ∘ₘ μ), (κ†μ) x = ν.withDensity (r x)

Uses 1 · Used by 2

Proof usesDisintegration of the joint law from a factorization of densities

Used byBayesian linear regression · Normal–Normal conjugacy with known variance

16 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.