Skip to content

Bayesian linear regression

DefinitionPosterior variance in Bayesian linear regression#✓fully proved

For a prior variance \(s_0 \ge 0\), a noise variance \(\sigma^2 \ge 0\) and inputs \(x \in \mathbb{R}^n\), the posterior variance of the weight is the nonnegative real number \(s_0 \sigma^2 / (\sigma^2 + s_0 \sum_i x_i^2)\), read as \(0\) when the denominator is \(0\).

noncomputable def linRegPostVar (s₀ σ2 : ℝ≥0) (x : Fin n → ℝ) : ℝ≥0 :=
  s₀ * σ2 / (σ2 + s₀ * (∑ i, x i ^ 2).toNNReal)
Used by 7
Used byCompleting the square for linear regression · Prior times likelihood factors as evidence times posterior · Precisions add in Bayesian linear regression · The evidence density of Bayesian linear regression · The evidence of Bayesian linear regression · Posterior predictive at a new input · Bayesian linear regression

DefinitionPosterior mean in Bayesian linear regression#✓fully proved

For a prior mean \(m_0 \in \mathbb{R}\), a prior variance \(s_0 \ge 0\), a noise variance \(\sigma^2 \ge 0\), inputs \(x \in \mathbb{R}^n\) and responses \(y \in \mathbb{R}^n\), the posterior mean of the weight is the real number \((\sigma^2 m_0 + s_0 \sum_i x_i y_i) / (\sigma^2 + s_0 \sum_i x_i^2)\), read as \(0\) when the denominator is \(0\).

noncomputable def linRegPostMean (m₀ : ℝ) (s₀ σ2 : ℝ≥0) (x y : Fin n → ℝ) : ℝ :=
  (σ2 * m₀ + s₀ * ∑ i, x i * y i) / (σ2 + s₀ * ∑ i, x i ^ 2)
Used by 7
Used byCompleting the square for linear regression · Prior times likelihood factors as evidence times posterior · The evidence density of Bayesian linear regression · The evidence of Bayesian linear regression · Posterior predictive at a new input · Measurability of the posterior mean in Bayesian linear regression · Bayesian linear regression

TheoremPrecisions add in Bayesian linear regression#✓fully proved

Let \(s_0, \sigma^2 \ge 0\) be nonzero and \(x \in \mathbb{R}^n\). Then the posterior variance \(v\) of the weight for prior variance \(s_0\), noise variance \(\sigma^2\) and inputs \(x\) satisfies \(1 / v = 1 / s_0 + (\sum_i x_i^2) / \sigma^2\).

theorem inv_linRegPostVar {s₀ σ2 : ℝ≥0} (h₀ : s₀ ≠ 0) (h : σ2 ≠ 0) (x : Fin n → ℝ) :
    ((linRegPostVar s₀ σ2 x : ℝ))⁻¹ = (s₀ : ℝ)⁻¹ + (∑ i, x i ^ 2) / σ2
Uses 1
Statement usesPosterior variance in Bayesian linear regression

DefinitionThe linear regression likelihood density#✓fully proved

For \(\sigma^2 \ge 0\), \(x, y \in \mathbb{R}^n\) and \(w \in \mathbb{R}\), it is the real number \(\prod_i \varphi(y_i; w x_i, \sigma^2)\), where \(\varphi(t; \mu, \tau) = (2\pi\tau)^{-1/2} e^{-(t - \mu)^2 / (2\tau)}\) is the Gaussian density with mean \(\mu\) and variance \(\tau\) at \(t\), read as \(0\) when \(\tau = 0\). For \(\sigma^2 \ne 0\) it is the Lebesgue density of the responses \(y\) given the weight \(w\), independent with \(y_i \sim \mathcal{N}(w x_i, \sigma^2)\). With no data (\(n = 0\)) it is the empty product \(1\), the density of the unit mass on the single empty response. For \(\sigma^2 = 0\) and \(n > 0\) the responses are deterministic and have no density, and this formula is \(0\).

noncomputable def linRegLikelihoodPDFReal (σ2 : ℝ≥0) (x : Fin n → ℝ) (w : ℝ) (y : Fin n → ℝ) :
    ℝ :=
  ∏ i, gaussianPDFReal (w * x i) σ2 (y i)
Used by 5
Used byCompleting the square for linear regression · Prior times likelihood factors as evidence times posterior · The evidence density of Bayesian linear regression · The evidence of Bayesian linear regression · Bayesian linear regression

TheoremCompleting the square for linear regression#✓fully proved

Let \(m_0 \in \mathbb{R}\), let \(s_0, \sigma^2 \ge 0\) be nonzero, and let \(x, y \in \mathbb{R}^n\). Write \(\varphi(t; \mu, \tau)\) for the Gaussian density with mean \(\mu\) and variance \(\tau\) at \(t\), \(p(w) = \varphi(w; m_0, s_0)\) for the prior density, \(L(y \mid w) = \prod_i \varphi(y_i; w x_i, \sigma^2)\) for the likelihood density, \(m\) and \(v\) for the posterior mean and variance of the weight, and \(r(w) = \varphi(w; m, v)\) for the posterior density. Then for every weight \(w \in \mathbb{R}\),

\[p(w) \, L(y \mid w) \, r(m) = p(m) \, L(y \mid m) \, r(w).\]
theorem gaussianPDFReal_mul_linRegLikelihoodPDFReal (m₀ : ℝ) {s₀ σ2 : ℝ≥0} (h₀ : s₀ ≠ 0)
    (h : σ2 ≠ 0) (x : Fin n → ℝ) (w : ℝ) (y : Fin n → ℝ) :
    gaussianPDFReal m₀ s₀ w * linRegLikelihoodPDFReal σ2 x w y *
        gaussianPDFReal (linRegPostMean m₀ s₀ σ2 x y) (linRegPostVar s₀ σ2 x)
          (linRegPostMean m₀ s₀ σ2 x y) =
      gaussianPDFReal m₀ s₀ (linRegPostMean m₀ s₀ σ2 x y) *
          linRegLikelihoodPDFReal σ2 x (linRegPostMean m₀ s₀ σ2 x y) y *
        gaussianPDFReal (linRegPostMean m₀ s₀ σ2 x y) (linRegPostVar s₀ σ2 x) w
Uses 3 · Used by 1
Statement usesThe linear regression likelihood density · Posterior mean in Bayesian linear regression · Posterior variance in Bayesian linear regression
Used byPrior times likelihood factors as evidence times posterior

DefinitionThe evidence density of Bayesian linear regression#✓fully proved

For \(m_0 \in \mathbb{R}\), \(s_0, \sigma^2 \ge 0\) and \(x, y \in \mathbb{R}^n\), let \(m\) and \(v\) be the posterior mean and variance of the weight, write \(\varphi(t; \mu, \tau) = (2\pi\tau)^{-1/2} e^{-(t - \mu)^2 / (2\tau)}\) for the Gaussian density with mean \(\mu\) and variance \(\tau\) at \(t\) (read as \(0\) when \(\tau = 0\)), and let \(L(y \mid w) = \prod_i \varphi(y_i; w x_i, \sigma^2)\) be the likelihood density. The evidence density at \(y\) is

\[Z(y) = \frac{\varphi(m; m_0, s_0) \, L(y \mid m)}{\varphi(m; m, v)},\]

prior density times likelihood divided by the posterior density, all at the posterior mean (a quotient by \(0\) is read as \(0\)).

For \(s_0 \ne 0\) and \(\sigma^2 \ne 0\) the ratio does not depend on the point where it is evaluated, and \(Z\) is the Lebesgue density of the marginal law of the data. It is not a density of the evidence in the degenerate cases.

noncomputable def linRegEvidencePDFReal (m₀ : ℝ) (s₀ σ2 : ℝ≥0) (x y : Fin n → ℝ) : ℝ :=
  gaussianPDFReal m₀ s₀ (linRegPostMean m₀ s₀ σ2 x y) *
      linRegLikelihoodPDFReal σ2 x (linRegPostMean m₀ s₀ σ2 x y) y /
    gaussianPDFReal (linRegPostMean m₀ s₀ σ2 x y) (linRegPostVar s₀ σ2 x)
      (linRegPostMean m₀ s₀ σ2 x y)
Uses 3 · Used by 3
Statement usesThe linear regression likelihood density · Posterior mean in Bayesian linear regression · Posterior variance in Bayesian linear regression
Used byPrior times likelihood factors as evidence times posterior · The evidence of Bayesian linear regression · Bayesian linear regression

TheoremPrior times likelihood factors as evidence times posterior#✓fully proved

Let \(m_0 \in \mathbb{R}\), let \(s_0, \sigma^2 \ge 0\) be nonzero, let \(x, y \in \mathbb{R}^n\) and let \(w \in \mathbb{R}\). Write \(\varphi(t; \mu, \tau)\) for the Gaussian density with mean \(\mu\) and variance \(\tau\) at \(t\), \(L(y \mid w) = \prod_i \varphi(y_i; w x_i, \sigma^2)\) for the likelihood density, \(m\) and \(v\) for the posterior mean and variance of the weight, and \(Z(y)\) for the evidence density. Then \(\varphi(w; m_0, s_0) \, L(y \mid w) = Z(y) \, \varphi(w; m, v)\).

theorem gaussianPDFReal_mul_linRegLikelihoodPDFReal' (m₀ : ℝ) {s₀ σ2 : ℝ≥0} (h₀ : s₀ ≠ 0)
    (h : σ2 ≠ 0) (x : Fin n → ℝ) (w : ℝ) (y : Fin n → ℝ) :
    gaussianPDFReal m₀ s₀ w * linRegLikelihoodPDFReal σ2 x w y =
      linRegEvidencePDFReal m₀ s₀ σ2 x y *
        gaussianPDFReal (linRegPostMean m₀ s₀ σ2 x y) (linRegPostVar s₀ σ2 x) w
Uses 5 · Used by 2
Statement usesThe evidence density of Bayesian linear regression · The linear regression likelihood density · Posterior mean in Bayesian linear regression · Posterior variance in Bayesian linear regression
Proof usesCompleting the square for linear regression
Used byThe evidence of Bayesian linear regression · Bayesian linear regression
16 fully proved

The likelihood kernel

DefinitionThe extended-real linear regression likelihood density#✓fully proved

For \(\sigma^2 \ge 0\), \(x, y \in \mathbb{R}^n\) and \(w \in \mathbb{R}\), it is \(\prod_i \varphi(y_i; w x_i, \sigma^2)\) as an extended nonnegative real, where \(\varphi(t; \mu, \tau)\) is the Gaussian density with mean \(\mu\) and variance \(\tau\) at \(t\), read as \(0\) when \(\tau = 0\). It is the likelihood density for \(\sigma^2 \ne 0\) or \(n = 0\), and it is \(0\) for \(\sigma^2 = 0\) and \(n > 0\).

noncomputable def linRegLikelihoodPDF (σ2 : ℝ≥0) (x : Fin n → ℝ) (w : ℝ) (y : Fin n → ℝ) :
    ℝ≥0∞ :=
  ∏ i, gaussianPDF (w * x i) σ2 (y i)
Used by 5
Used byThe likelihood of Bayesian linear regression · The linear regression likelihood is a product of Gaussians · The evidence of Bayesian linear regression · The noiseless linear regression likelihood · Bayesian linear regression

DefinitionThe likelihood of Bayesian linear regression#✓fully proved

The likelihood of Bayesian linear regression with one feature and known noise variance \(\sigma^2 \ge 0\), for fixed inputs \(x \in \mathbb{R}^n\): the kernel from the weight \(w \in \mathbb{R}\) to the responses in \(\mathbb{R}^n\) under which, given \(w\), the responses are independent with \(y_i \sim \mathcal{N}(w x_i, \sigma^2)\). For \(\sigma^2 \ne 0\) it is given by the density \(\prod_i \varphi(y_i; w x_i, \sigma^2)\) with respect to Lebesgue measure, where \(\varphi(t; \mu, \tau)\) is the Gaussian density with mean \(\mu\) and variance \(\tau\) at \(t\); for \(\sigma^2 = 0\) it sends \(w\) to the Dirac measure at \((w x_i)_i\).

noncomputable def linRegLikelihood (σ2 : ℝ≥0) (x : Fin n → ℝ) : Kernel ℝ (Fin n → ℝ) :=
  if σ2 = 0 then Kernel.deterministic (fun w i ↦ w * x i) (by fun_prop)
  else (Kernel.const ℝ volume).withDensity (linRegLikelihoodPDF σ2 x)
Uses 1 · Used by 5
Statement usesThe extended-real linear regression likelihood density
Used byThe linear regression likelihood is a product of Gaussians · The evidence of Bayesian linear regression · The noiseless linear regression likelihood · Posterior predictive at a new input · Bayesian linear regression

TheoremThe noiseless linear regression likelihood#✓fully proved

For \(x \in \mathbb{R}^n\) and \(w \in \mathbb{R}\), the linear regression likelihood with noise variance \(0\) and inputs \(x\), given the weight \(w\), is the Dirac measure at the vector \((w x_i)_i\): the responses are exactly \(y_i = w x_i\).

theorem linRegLikelihood_zero_apply (x : Fin n → ℝ) (w : ℝ) :
    linRegLikelihood 0 x w = Measure.dirac fun i ↦ w * x i
Uses 2 · Used by 2
Statement usesThe likelihood of Bayesian linear regression
Proof usesThe extended-real linear regression likelihood density
Used byPosterior predictive at a new input · Bayesian linear regression

TheoremThe linear regression likelihood is a product of Gaussians#✓fully proved

Let \(\sigma^2 \ge 0\) be nonzero, \(x \in \mathbb{R}^n\) and \(w \in \mathbb{R}\). Given the weight \(w\), the linear regression likelihood with noise variance \(\sigma^2\) and inputs \(x\) is the product measure \(\bigotimes_i \mathcal{N}(w x_i, \sigma^2)\) on \(\mathbb{R}^n\).

theorem linRegLikelihood_apply {σ2 : ℝ≥0} (h : σ2 ≠ 0) (x : Fin n → ℝ) (w : ℝ) :
    linRegLikelihood σ2 x w = Measure.pi fun i ↦ gaussianReal (w * x i) σ2
Uses 3 · Used by 2
Statement usesThe likelihood of Bayesian linear regression
Proof usesThe extended-real linear regression likelihood density · A product of measures with densities
Used byPosterior predictive at a new input · Bayesian linear regression

The posterior

TheoremMeasurability of the posterior mean in Bayesian linear regression#✓fully proved

For a prior mean \(m_0 \in \mathbb{R}\), a prior variance \(s_0 \ge 0\), a noise variance \(\sigma^2 \ge 0\) and inputs \(x \in \mathbb{R}^n\), the posterior mean of the weight, as a function of the responses \(y \in \mathbb{R}^n\), is a measurable map from \(\mathbb{R}^n\) to \(\mathbb{R}\).

theorem measurable_linRegPostMean (m₀ : ℝ) (s₀ σ2 : ℝ≥0) (x : Fin n → ℝ) :
    Measurable (linRegPostMean m₀ s₀ σ2 x)
Uses 1 · Used by 2
Statement usesPosterior mean in Bayesian linear regression
Used byThe evidence of Bayesian linear regression · Bayesian linear regression

TheoremThe evidence of Bayesian linear regression#✓fully proved

Let \(m_0 \in \mathbb{R}\), let \(s_0, \sigma^2 \ge 0\) be nonzero, and let \(x \in \mathbb{R}^n\). If the weight has prior \(\mathcal{N}(m_0, s_0)\) and the responses follow the linear regression likelihood with noise variance \(\sigma^2\) and inputs \(x\), then the marginal law of the responses is the measure on \(\mathbb{R}^n\) whose density with respect to Lebesgue measure is the evidence density \(Z\) for \(m_0\), \(s_0\), \(\sigma^2\) and \(x\).

theorem linRegLikelihood_comp_gaussianReal (m₀ : ℝ) {s₀ σ2 : ℝ≥0} (h₀ : s₀ ≠ 0) (h : σ2 ≠ 0)
    (x : Fin n → ℝ) :
    linRegLikelihood σ2 x ∘ₘ gaussianReal m₀ s₀ =
      volume.withDensity fun y ↦ ENNReal.ofReal (linRegEvidencePDFReal m₀ s₀ σ2 x y)
Uses 9 · Used by 1
Statement usesThe evidence density of Bayesian linear regression · The likelihood of Bayesian linear regression
Proof usesThe evidence from a factorization of densities · Prior times likelihood factors as evidence times posterior · The extended-real linear regression likelihood density · The linear regression likelihood density · Posterior mean in Bayesian linear regression · Posterior variance in Bayesian linear regression · Measurability of the posterior mean in Bayesian linear regression
Used byBayesian linear regression

TheoremBayesian linear regression#✓fully proved

Let \(m_0 \in \mathbb{R}\), let \(s_0 > 0\) and \(\sigma^2 > 0\), and let \(x \in \mathbb{R}^n\) be fixed inputs. Put the prior \(N(m_0, s_0)\) (mean \(m_0\), variance \(s_0\)) on a scalar weight \(w\), and let the responses be independent given \(w\) with \(y_i \sim N(w x_i, \sigma^2)\). Then for Lebesgue-almost every response vector \(y \in \mathbb{R}^n\), the posterior of \(w\) given \(y\) is Gaussian with mean \((\sigma^2 m_0 + s_0 \sum_i x_i y_i) / (\sigma^2 + s_0 \sum_i x_i^2)\) and variance \(s_0 \sigma^2 / (\sigma^2 + s_0 \sum_i x_i^2)\).

theorem posterior_linRegLikelihood_gaussianReal (m₀ : ℝ) {s₀ σ2 : ℝ≥0} [NeZero s₀] [NeZero σ2]
    (x : Fin n → ℝ) :
    ∀ᵐ y, ((linRegLikelihood σ2 x)†(gaussianReal m₀ s₀)) y =
      gaussianReal (linRegPostMean m₀ s₀ σ2 x y) (linRegPostVar s₀ σ2 x)
Uses 12 · Used by 1
Statement usesThe likelihood of Bayesian linear regression · The linear regression likelihood is a product of Gaussians · The noiseless linear regression likelihood · Posterior mean in Bayesian linear regression · Posterior variance in Bayesian linear regression
Proof usesPrior times likelihood factors as evidence times posterior · The evidence density of Bayesian linear regression · The extended-real linear regression likelihood density · The linear regression likelihood density · The evidence of Bayesian linear regression · Measurability of the posterior mean in Bayesian linear regression · Bayes' rule for densities
Used byPosterior predictive at a new input

Prediction at a new input

DefinitionPredictive law of a linear-regression response#✓fully proved

For a noise variance \(\sigma^2 \ge 0\) and a new input \(x' \in \mathbb{R}\), the predictive kernel sends a weight \(w \in \mathbb{R}\) to the Gaussian law \(N(w x', \sigma^2)\) of the response at \(x'\), which is the point mass at \(w x'\) when \(\sigma^2 = 0\).

noncomputable def linRegPredictive (σ2 : ℝ≥0) (x' : ℝ) : Kernel ℝ ℝ :=
  (gaussianLikelihood σ2).comap (· * x') (measurable_mul_const x')
Uses 1 · Used by 1
Statement usesGaussian likelihood with known variance
Used byPosterior predictive at a new input

TheoremPosterior predictive at a new input#✓fully proved

Let \(m_0 \in \mathbb{R}\), let \(s_0 > 0\) and \(\sigma^2 > 0\), and let \(x \in \mathbb{R}^n\) and \(x' \in \mathbb{R}\). Put the prior \(N(m_0, s_0)\) (mean \(m_0\), variance \(s_0\)) on a scalar weight \(w\), and let the responses be independent given \(w\) with \(y_i \sim N(w x_i, \sigma^2)\). Then for Lebesgue-almost every response vector \(y \in \mathbb{R}^n\), integrating the law \(N(w x', \sigma^2)\) of the response at \(x'\) against the posterior of \(w\) given \(y\) gives the Gaussian \(N(x' m, x'^2 v + \sigma^2)\), where \(m = (\sigma^2 m_0 + s_0 \sum_i x_i y_i) / (\sigma^2 + s_0 \sum_i x_i^2)\) and \(v = s_0 \sigma^2 / (\sigma^2 + s_0 \sum_i x_i^2)\) are the posterior mean and variance.

theorem linRegPredictive_comp_posterior (m₀ : ℝ) {s₀ σ2 : ℝ≥0} [NeZero s₀] [NeZero σ2]
    (x : Fin n → ℝ) (x' : ℝ) :
    ∀ᵐ y, linRegPredictive σ2 x' ∘ₘ ((linRegLikelihood σ2 x)†(gaussianReal m₀ s₀)) y =
      gaussianReal (x' * linRegPostMean m₀ s₀ σ2 x y)
        (.mk (x' ^ 2) (sq_nonneg _) * linRegPostVar s₀ σ2 x + σ2)
Uses 10
Statement usesThe likelihood of Bayesian linear regression · The linear regression likelihood is a product of Gaussians · The noiseless linear regression likelihood · Posterior mean in Bayesian linear regression · Posterior variance in Bayesian linear regression · Predictive law of a linear-regression response
Proof usesGaussian likelihood with known variance · The marginal of the data · Measurability of the Gaussian density in its mean and argument · Bayesian linear regression

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.