Finite exponential families

This module adds the finite one-parameter exponential-family companion to the Fisher-information and Cramer-Rao layer.

For a finite sample space with positive base weights h and statistic T, the normalizer is

Z(theta) = sum_x h x * exp(theta * T x)

and the log-partition is A(theta) = log Z(theta). The normalized mass function is p_theta(x) = h x * exp(theta * T x - A(theta)).

The main results are the finite-sum textbook identities:

• A'(theta) = E_theta[T];
• the derivative of E_theta[T] is Var_theta(T), so A''(theta) = Var_theta(T);
• the natural-parameter Fisher information equals that same variance.

The Bernoulli witness uses Bool, statistic 1{true}, base weights 1, and theta = 0, giving A'(0) = 1/2, A''(0) = 1/4, and Fisher information 1/4.

@[implicit_reducible]

def FormalSLT.Statistics.ExponentialFamily.instAddCommGroupReal_formalSLT : AddCommGroup ℝ

Equations

• FormalSLT.Statistics.ExponentialFamily.instAddCommGroupReal_formalSLT = Real.normedCommRing.toAddCommGroup

@[implicit_reducible]

noncomputable def FormalSLT.Statistics.ExponentialFamily.instModuleReal_formalSLT : Module ℝ ℝ

Equations

• FormalSLT.Statistics.ExponentialFamily.instModuleReal_formalSLT = inferInstance.toModule

Finite exponential-family primitives

noncomputable def FormalSLT.Statistics.ExponentialFamily.finitePartition {Ω : Type u_1} [Fintype Ω] (h T : Ω → ℝ) (theta : ℝ) : ℝ

The finite partition sum Z(theta).

Equations

• FormalSLT.Statistics.ExponentialFamily.finitePartition h T theta = ∑ x : Ω, h x * Real.exp (theta * T x)

noncomputable def FormalSLT.Statistics.ExponentialFamily.finiteLogPartition {Ω : Type u_1} [Fintype Ω] (h T : Ω → ℝ) (theta : ℝ) : ℝ

The log-partition function A(theta) = log Z(theta).

Equations

• FormalSLT.Statistics.ExponentialFamily.finiteLogPartition h T theta = Real.log (FormalSLT.Statistics.ExponentialFamily.finitePartition h T theta)

noncomputable def FormalSLT.Statistics.ExponentialFamily.finiteExponentialPMF {Ω : Type u_1} [Fintype Ω] (h T : Ω → ℝ) (theta : ℝ) (x : Ω) : ℝ

The natural-parameter finite exponential-family mass function.

Equations

• FormalSLT.Statistics.ExponentialFamily.finiteExponentialPMF h T theta x = h x * Real.exp (theta * T x - FormalSLT.Statistics.ExponentialFamily.finiteLogPartition h T theta)

noncomputable def FormalSLT.Statistics.ExponentialFamily.finiteExponentialPMFDeriv {Ω : Type u_1} [Fintype Ω] (h T : Ω → ℝ) (theta : ℝ) (x : Ω) : ℝ

The natural-parameter derivative of the finite exponential-family mass.

Equations

• One or more equations did not get rendered due to their size.

theorem FormalSLT.Statistics.ExponentialFamily.finitePartition_pos {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {h T : Ω → ℝ} (hpos : ∀ (x : Ω), 0 < h x) (theta : ℝ) : 0 < finitePartition h T theta

Positivity of the finite partition sum under positive base weights.

theorem FormalSLT.Statistics.ExponentialFamily.finiteExponentialPMF_sum_one {Ω : Type u_1} [Fintype Ω] {h T : Ω → ℝ} {theta : ℝ} (hZ : 0 < finitePartition h T theta) : ∑ x : Ω, finiteExponentialPMF h T theta x = 1

The normalized exponential-family masses sum to one.

theorem FormalSLT.Statistics.ExponentialFamily.finiteExponentialPMF_pos {Ω : Type u_1} [Fintype Ω] {h T : Ω → ℝ} {theta : ℝ} (hpos : ∀ (x : Ω), 0 < h x) (x : Ω) : 0 < finiteExponentialPMF h T theta x

Exponential-family masses are positive under positive base weights.

theorem FormalSLT.Statistics.ExponentialFamily.finitePartition_hasDerivAt {Ω : Type u_1} [Fintype Ω] (h T : Ω → ℝ) (theta : ℝ) : HasDerivAt (fun (u : ℝ) => finitePartition h T u) (∑ x : Ω, h x * Real.exp (theta * T x) * T x) theta

Differentiating the finite partition sum termwise.

theorem FormalSLT.Statistics.ExponentialFamily.finiteExponentialFamily_mean_eq_logPartition_deriv {Ω : Type u_1} [Fintype Ω] {h T : Ω → ℝ} {theta : ℝ} (hZ : 0 < finitePartition h T theta) : ClassicalEstimation.weightedExpectation (finiteExponentialPMF h T theta) T = (∑ x : Ω, h x * Real.exp (theta * T x) * T x) / finitePartition h T theta

The normalized expectation is the logarithmic derivative numerator divided by Z.

theorem FormalSLT.Statistics.ExponentialFamily.finiteLogPartition_hasDerivAt {Ω : Type u_1} [Fintype Ω] {h T : Ω → ℝ} {theta : ℝ} (hZ : 0 < finitePartition h T theta) : HasDerivAt (fun (u : ℝ) => finiteLogPartition h T u) (ClassicalEstimation.weightedExpectation (finiteExponentialPMF h T theta) T) theta

Log-partition derivative identity.

For a finite exponential family, the derivative of A(theta) is the finite expectation of the sufficient statistic.

theorem FormalSLT.Statistics.ExponentialFamily.finiteLogPartition_hasDerivAt_of_positiveBase {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {h T : Ω → ℝ} {theta : ℝ} (hpos : ∀ (x : Ω), 0 < h x) : HasDerivAt (fun (u : ℝ) => finiteLogPartition h T u) (ClassicalEstimation.weightedExpectation (finiteExponentialPMF h T theta) T) theta

Textbook positive-base form of the log-partition derivative identity.

Curvature and variance

theorem FormalSLT.Statistics.ExponentialFamily.finiteExponentialPMF_hasDerivAt {Ω : Type u_1} [Fintype Ω] {h T : Ω → ℝ} {theta : ℝ} (hZ : 0 < finitePartition h T theta) (x : Ω) : HasDerivAt (fun (u : ℝ) => finiteExponentialPMF h T u x) (finiteExponentialPMFDeriv h T theta x) theta

The derivative of the finite exponential-family mass.

theorem FormalSLT.Statistics.ExponentialFamily.finiteMean_hasDerivAt {Ω : Type u_1} [Fintype Ω] {h T : Ω → ℝ} {theta : ℝ} (hZ : 0 < finitePartition h T theta) : HasDerivAt (fun (u : ℝ) => ClassicalEstimation.weightedExpectation (finiteExponentialPMF h T u) T) (∑ x : Ω, finiteExponentialPMF h T theta x * (T x - ClassicalEstimation.weightedExpectation (finiteExponentialPMF h T theta) T) * T x) theta

Differentiating the finite mean gives the centered second moment.

theorem FormalSLT.Statistics.ExponentialFamily.finiteMean_deriv_eq_variance {Ω : Type u_1} [Fintype Ω] {h T : Ω → ℝ} {theta : ℝ} (hZ : 0 < finitePartition h T theta) : ∑ x : Ω, finiteExponentialPMF h T theta x * (T x - ClassicalEstimation.weightedExpectation (finiteExponentialPMF h T theta) T) * T x = FisherInformation.weightedVariance (finiteExponentialPMF h T theta) T

The centered second-moment derivative is the finite variance.

theorem FormalSLT.Statistics.ExponentialFamily.finiteLogPartition_hasSecondDerivAt {Ω : Type u_1} [Fintype Ω] {h T : Ω → ℝ} {theta : ℝ} (hZ : 0 < finitePartition h T theta) : HasDerivAt (fun (u : ℝ) => ClassicalEstimation.weightedExpectation (finiteExponentialPMF h T u) T) (FisherInformation.weightedVariance (finiteExponentialPMF h T theta) T) theta

Log-partition curvature identity.

For a finite exponential family, differentiating the mean gives the variance of the sufficient statistic. This is the one-dimensional Hessian identity A''(theta) = Var_theta(T).

theorem FormalSLT.Statistics.ExponentialFamily.finiteLogPartition_hasSecondDerivAt_of_positiveBase {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {h T : Ω → ℝ} {theta : ℝ} (hpos : ∀ (x : Ω), 0 < h x) : HasDerivAt (fun (u : ℝ) => ClassicalEstimation.weightedExpectation (finiteExponentialPMF h T u) T) (FisherInformation.weightedVariance (finiteExponentialPMF h T theta) T) theta

Textbook positive-base form of the log-partition curvature identity.

theorem FormalSLT.Statistics.ExponentialFamily.finiteExponentialFamily_variance_eq_logPartition_secondDeriv {Ω : Type u_1} [Fintype Ω] {h T : Ω → ℝ} {theta : ℝ} (hZ : 0 < finitePartition h T theta) : HasDerivAt (fun (u : ℝ) => ClassicalEstimation.weightedExpectation (finiteExponentialPMF h T u) T) (FisherInformation.weightedVariance (finiteExponentialPMF h T theta) T) theta

A named equality form of the curvature identity.

Fisher information connection

theorem FormalSLT.Statistics.ExponentialFamily.finiteExponentialFamily_score_eq_centered {Ω : Type u_1} [Fintype Ω] {h T : Ω → ℝ} {theta : ℝ} (hpos : ∀ (x : Ω), 0 < h x) (x : Ω) : FisherInformation.scoreFunction (fun (u : ℝ) => finiteExponentialPMF h T u) (fun (u : ℝ) => finiteExponentialPMFDeriv h T u) theta x = T x - ClassicalEstimation.weightedExpectation (finiteExponentialPMF h T theta) T

The natural-parameter score is T - E_theta[T].

theorem FormalSLT.Statistics.ExponentialFamily.finiteExponentialFamily_fisherInformation_eq_variance {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {h T : Ω → ℝ} {theta : ℝ} (hpos : ∀ (x : Ω), 0 < h x) : FisherInformation.fisherInformation (fun (u : ℝ) => finiteExponentialPMF h T u) (fun (u : ℝ) => finiteExponentialPMFDeriv h T u) theta = FisherInformation.weightedVariance (finiteExponentialPMF h T theta) T

Fisher information equals exponential-family curvature and variance.

theorem FormalSLT.Statistics.ExponentialFamily.finiteExponentialFamily_logPartition_secondDeriv_eq_fisherInformation {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {h T : Ω → ℝ} {theta : ℝ} (hpos : ∀ (x : Ω), 0 < h x) : HasDerivAt (fun (u : ℝ) => ClassicalEstimation.weightedExpectation (finiteExponentialPMF h T u) T) (FisherInformation.fisherInformation (fun (u : ℝ) => finiteExponentialPMF h T u) (fun (u : ℝ) => finiteExponentialPMFDeriv h T u) theta) theta

Direct form of I(theta) = A''(theta) for a positive finite exponential family.

Bernoulli natural-parameter witness

def FormalSLT.Statistics.ExponentialFamily.bernoulliNaturalBase : Bool → ℝ

Bernoulli natural-family base weights on Bool.

Equations

• FormalSLT.Statistics.ExponentialFamily.bernoulliNaturalBase x✝ = 1

def FormalSLT.Statistics.ExponentialFamily.bernoulliNaturalStatistic : Bool → ℝ

Bernoulli natural sufficient statistic 1{true}.

Equations

• FormalSLT.Statistics.ExponentialFamily.bernoulliNaturalStatistic b = if b = true then 1 else 0

theorem FormalSLT.Statistics.ExponentialFamily.bernoulliNatural_partition (theta : ℝ) : finitePartition bernoulliNaturalBase bernoulliNaturalStatistic theta = 1 + Real.exp theta

The Bernoulli natural-parameter partition sum is 1 + exp(theta).

theorem FormalSLT.Statistics.ExponentialFamily.bernoulliNatural_logPartition_zero : finiteLogPartition bernoulliNaturalBase bernoulliNaturalStatistic 0 = Real.log 2

At theta = 0, the Bernoulli natural log-partition is log 2.

theorem FormalSLT.Statistics.ExponentialFamily.bernoulliNatural_mean_zero : ClassicalEstimation.weightedExpectation (finiteExponentialPMF bernoulliNaturalBase bernoulliNaturalStatistic 0) bernoulliNaturalStatistic = 1 / 2

At theta = 0, the Bernoulli natural-family success probability is 1/2.

theorem FormalSLT.Statistics.ExponentialFamily.bernoulliNatural_logPartition_deriv_zero : HasDerivAt (fun (u : ℝ) => finiteLogPartition bernoulliNaturalBase bernoulliNaturalStatistic u) (1 / 2) 0

A'(0) = 1/2 for the Bernoulli natural family.

theorem FormalSLT.Statistics.ExponentialFamily.bernoulliNatural_pmf_zero (b : Bool) : finiteExponentialPMF bernoulliNaturalBase bernoulliNaturalStatistic 0 b = 1 / 2

At theta = 0, both Bernoulli natural-family atoms have mass 1/2.

theorem FormalSLT.Statistics.ExponentialFamily.bernoulliNatural_variance_zero : FisherInformation.weightedVariance (finiteExponentialPMF bernoulliNaturalBase bernoulliNaturalStatistic 0) bernoulliNaturalStatistic = 1 / 4

At theta = 0, Bernoulli natural-family variance is 1/4.

theorem FormalSLT.Statistics.ExponentialFamily.bernoulliNatural_logPartition_secondDeriv_zero : HasDerivAt (fun (u : ℝ) => ClassicalEstimation.weightedExpectation (finiteExponentialPMF bernoulliNaturalBase bernoulliNaturalStatistic u) bernoulliNaturalStatistic) (1 / 4) 0

A''(0) = 1/4 for the Bernoulli natural family.

theorem FormalSLT.Statistics.ExponentialFamily.bernoulliNatural_fisher_zero : FisherInformation.fisherInformation (fun (u : ℝ) => finiteExponentialPMF bernoulliNaturalBase bernoulliNaturalStatistic u) (fun (u : ℝ) => finiteExponentialPMFDeriv bernoulliNaturalBase bernoulliNaturalStatistic u) 0 = 1 / 4

At theta = 0, Bernoulli natural-family Fisher information is 1/4.

theorem FormalSLT.Statistics.ExponentialFamily.bernoulliNatural_fisher_eq_variance_zero : FisherInformation.fisherInformation (fun (u : ℝ) => finiteExponentialPMF bernoulliNaturalBase bernoulliNaturalStatistic u) (fun (u : ℝ) => finiteExponentialPMFDeriv bernoulliNaturalBase bernoulliNaturalStatistic u) 0 = FisherInformation.weightedVariance (finiteExponentialPMF bernoulliNaturalBase bernoulliNaturalStatistic 0) bernoulliNaturalStatistic

Bernoulli natural-family Fisher information equals variance at theta = 0.

theorem FormalSLT.Statistics.ExponentialFamily.bernoulliNatural_witness : ClassicalEstimation.weightedExpectation (finiteExponentialPMF bernoulliNaturalBase bernoulliNaturalStatistic 0) bernoulliNaturalStatistic = 1 / 2 ∧ FisherInformation.weightedVariance (finiteExponentialPMF bernoulliNaturalBase bernoulliNaturalStatistic 0) bernoulliNaturalStatistic = 1 / 4 ∧ FisherInformation.fisherInformation (fun (u : ℝ) => finiteExponentialPMF bernoulliNaturalBase bernoulliNaturalStatistic u) (fun (u : ℝ) => finiteExponentialPMFDeriv bernoulliNaturalBase bernoulliNaturalStatistic u) 0 = 1 / 4

Concrete Bernoulli witness at theta = 0: A'(0) = 1/2, A''(0) = 1/4, and I(0) = Var(T) = 1/4.