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 187 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 188 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 189 Gaussian Product Parameters

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

Lemma 190 Product Parameters Properties

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

Proof
Lemma 191 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 192 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 193 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 194 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 195 Phase 2 Steps

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

Proof
Definition 196 Phase 2 Final Parameters
#

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

Lemma 197 Phase 2 Final Properties

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

Proof
Lemma 198 Phase 2 Complete Combination

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

Proof
Lemma 199 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 200 Observation Rewrite
#

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

Proof