Quasi-Borel Spaces in Rocq

5 Normal Density Algebra

This chapter develops the algebraic identities needed for the Bayesian regression normalizing constant computation. All proofs use ring/field from math-comp algebra-tactics.

5.1 Completing the Square

Lemma 193 Complete the Square

For \(a \neq 0\): \(ax^2 + bx + c = a\bigl(x + \tfrac {b}{2a}\bigr)^2 - \tfrac {b^2 - 4ac}{4a}\).

Proof

5.2 Product of Gaussian Densities

Theorem 194 Product of Gaussians
#

For \(s, s' \neq 0\):

\[ \mathcal{N}(m, s)(x) \cdot \mathcal{N}(m', s')(x) = K \cdot \mathcal{N}(\mu _{\mathrm{new}}, \sigma _{\mathrm{new}})(x) \]

where \(\mu _{\mathrm{new}} = \frac{m s'^2 + m' s^2}{s^2 + s'^2}\), \(\sigma _{\mathrm{new}} = \frac{s s'}{\sqrt{s^2 + s'^2}}\), and \(K\) is a scalar involving \(|m - m'|\) and \(\sqrt{s^2 + s'^2}\).

Proof
Definition 195 Gaussian Product Parameters

Closed-form expressions for the combined mean, standard deviation, and scalar factor from the product of two Gaussians.

Lemma 196 Product Parameters Properties

The combined \(\sigma \) is nonzero when both inputs are nonzero. The scalar factor is positive.

Proof
Lemma 197 Chained Gaussian Product

\(K \cdot \mathcal{N}(m, s)(x) \cdot \mathcal{N}(m', s')(x) = K \cdot K' \cdot \mathcal{N}(\mu _{\mathrm{new}}, \sigma _{\mathrm{new}})(x)\), allowing iterative combination.

Proof
Lemma 198 Variance Recurrence
#

Algebraic identity for the recurrence \(\frac{1}{V_{n+1}} = \frac{1}{V_n} + \frac{1}{s^2}\) relating successive combined variances.

Proof

5.3 Phase 1: Intercept Combinations

Five steps combining the prior \(\mathcal{N}(0, 3)\) with each of the 5 observation likelihoods for the intercept parameter.

Lemma 199 Phase 1 Steps

Each step computes the combined variance (\(\sigma ^2 \in \{ 9/37, 9/73, 9/109, 9/145, 9/181\} \)) and the combined mean (a linear function of the slope parameter \(s\)).

Proof
Lemma 200 Phase 1 Positivity and Nonzero

Each intermediate variance is positive and its square root is nonzero, ensuring the chain of Gaussian products is well-defined.

Proof

5.4 Phase 2: Slope Combinations

Five steps combining the prior \(\mathcal{N}(0, 3)\) with the slope-dependent scalar from Phase 1.

Lemma 201 Phase 2 Steps

Each step combines the accumulated Gaussian for the slope with the next observation’s contribution.

Proof
Definition 202 Phase 2 Final Parameters
#

The final combined mean, standard deviation, and accumulated constant from all 10 Gaussian combination steps.

Lemma 203 Phase 2 Final Properties

The final \(\sigma \) is nonzero and the accumulated constant is positive.

Proof
Lemma 204 Phase 2 Complete Combination

The full 5-step slope combination yields the final Gaussian times the accumulated constant.

Proof
Lemma 205 Normal PDF Recentering

\(\mathcal{N}(sk + b, \sigma )(y) = \mathcal{N}(y - ks, \sigma )(b)\), used to convert observations from intercept-centered to slope-centered form.

Proof
Lemma 206 Observation Rewrite
#

The 5-observation product rewrites as a product of centered normal densities suitable for Phase 1 integration.

Proof