Single-Peak Log-Likelihood Covariances

Abstract

Uniformly started paths of the single-peak kernel have explicit one-step moments, finite-range log-likelihood covariances, and an exact path-sum variance.

Definition 1.1 (Even log-likelihood mean function).

$$\forall u\in \mathbb{R},\mathrm{phi}(u)=\frac{(1+u)\log (1+u)+(1-u)\log (1-u)}{2}$$

Formalization. D5/S3/Estimation/TimeArrow/SinglePeakLogLikelihoodCovariance.phi (✓ std3).

Source. Repository-derived.

Commentary.

The function phi is the even weighted logarithmic mean associated with a signed transition bias u.

Definition 1.2 (Odd weighted log-likelihood function).

$$\forall u\in \mathbb{R},\mathrm{xi}(u)=\frac{(1+u)\log (1+u)-(1-u)\log (1-u)}{2}$$

Formalization. D5/S3/Estimation/TimeArrow/SinglePeakLogLikelihoodCovariance.xi (✓ std3).

Source. Repository-derived.

Commentary.

The function xi is the odd part of the same weighted logarithmic expression.

Definition 1.3 (Even log-likelihood second-moment function).

$$\forall u\in \mathbb{R},\mathrm{psi}(u)=\frac{(1+u)\log (1+u{)}^2+(1-u)\log (1-u{)}^2}{2}$$

Formalization. D5/S3/Estimation/TimeArrow/SinglePeakLogLikelihoodCovariance.psi (✓ std3).

Source. Repository-derived.

Commentary.

The function psi is the even weighted second moment of the logarithmic increment.

Definition 1.4 (Uniform-start path weight).

$$\forall X:Type,\mathrm{Fintype}(X),P:X\to X\to \mathbb{R},s\in \mathbb{N},x:\mathrm{Fin}(s+1)\to X,\mathrm{pathWeight}(P,s,x)=\frac{1}{|X|}\prod _{t\in \mathrm{Fin}(s)}P(x_t,x_{t+1})$$

Formalization. D5/S3/Estimation/TimeArrow/SinglePeakLogLikelihoodCovariance.pathWeight (✓ std3).

Source. Repository-derived.

Commentary.

A path of s transitions starts with mass one over the cardinality of X and is weighted by the product of its transition factors.

Definition 1.5 (Finite-path expectation).

$$\forall X:Type,\mathrm{Fintype}(X),P:X\to X\to \mathbb{R},s\in \mathbb{N},f:(\mathrm{Fin}(s+1)\to X)\to \mathbb{R},\mathrm{pathExpectation}(P,s,f)=\sum _{x\in \mathrm{Fin}(s+1)\to X}\mathrm{pathWeight}(P,s,x)f(x)$$

Formalization. D5/S3/Estimation/TimeArrow/SinglePeakLogLikelihoodCovariance.pathExpectation (✓ std3).

Source. Repository-derived.

Commentary.

Expectation is the explicit finite sum of a path observable against the uniform-start path weight.

Definition 1.6 (Single-step log-likelihood increment).

$$\forall X:Type,\mathrm{Fintype}(X),chi:X\to \mathbb{R},z:X,r,q\in \mathbb{R},s\in \mathbb{N},t\in \mathrm{Fin}(s),x:\mathrm{Fin}(s+1)\to X,\mathrm{logIncrement}(chi,z,r,q,t,x)=\log (|X|\mathrm{kernel}(chi,z,r,q,|X|,x_t,x_{t+1}))$$

Formalization. D5/S3/Estimation/TimeArrow/SinglePeakLogLikelihoodCovariance.logIncrement (✓ std3).

Source. Repository-derived.

Commentary.

At time t, the increment is the logarithm of the state-space cardinality times the single-peak transition weight along that edge.

Definition 1.7 (Finite-path covariance).

$$\forall X:Type,\mathrm{Fintype}(X),P:X\to X\to \mathbb{R},s\in \mathbb{N},f,g\in (\mathrm{Fin}(s+1)\to X)\to \mathbb{R},\mathrm{pathCovariance}(P,s,f,g)=\mathrm{pathExpectation}(P,s,fg)-\mathrm{pathExpectation}(P,s,f)\mathrm{pathExpectation}(P,s,g)$$

Formalization. D5/S3/Estimation/TimeArrow/SinglePeakLogLikelihoodCovariance.pathCovariance (✓ std3).

Source. Repository-derived.

Commentary.

The covariance of two path observables is their product expectation minus the product of their expectations.

Definition 1.8 (Finite-path variance).

$$\forall X:Type,\mathrm{Fintype}(X),P:X\to X\to \mathbb{R},s\in \mathbb{N},f:(\mathrm{Fin}(s+1)\to X)\to \mathbb{R},\mathrm{pathVariance}(P,s,f)=\mathrm{pathCovariance}(P,s,f,f)$$

Formalization. D5/S3/Estimation/TimeArrow/SinglePeakLogLikelihoodCovariance.pathVariance (✓ std3).

Source. Repository-derived.

Commentary.

The variance of a path observable is its covariance with itself.

Definition 1.9 (Finite log-likelihood sum).

$$\forall X:Type,\mathrm{Fintype}(X),chi:X\to \mathbb{R},z:X,r,q\in \mathbb{R},s\in \mathbb{N},x:\mathrm{Fin}(s+1)\to X,\mathrm{logLikelihoodSum}(chi,z,r,q,s,x)=\sum _{t\in \mathrm{Fin}(s)}\mathrm{logIncrement}(chi,z,r,q,t,x)$$

Formalization. D5/S3/Estimation/TimeArrow/SinglePeakLogLikelihoodCovariance.logLikelihoodSum (✓ std3).

Source. Repository-derived.

Commentary.

The finite log-likelihood sum adds the increments over all edges of the path.

Theorem 1.10 (Exact single-peak log-likelihood covariances).

$$\begin{array}{rl}& \forall X:Type,\mathrm{Fintype}(X),chi:X\to \mathbb{R},z:X,r,q\in \mathbb{R},M\in \mathbb{N},\\ & (\forall x\in X,\mathrm{chi}(x)=1\vee \mathrm{chi}(x)=-1)\wedge \mathrm{chi}(z)=1\wedge 0<r\wedge r<1,\\ & |X|=2M\wedge |\{x\in X:\mathrm{chi}(x)=1\}|=M\wedge 2\le M\wedge q=\frac{r}{M-1}\Rightarrow \\ & letP=\mathrm{kernel}(chi,z,r,q,|X|);letL(x,y)=\log (|X|P(x,y));\\ & letk=M-1;letI=\frac{\mathrm{phi}(r)+k\mathrm{phi}(q)}{|X|};\\ & letJ=\frac{\mathrm{xi}(r)-k\mathrm{xi}(q)}{|X|};letv=\frac{\mathrm{psi}(r)+k\mathrm{psi}(q)}{|X|}-I^2;\\ & let{\ell }_t=\log (|X|P(x_t,x_{t+1}));(\forall x\in X,\sum _{y\in X}P(x,y)L(x,y)=\mathrm{phi}(\mathrm{profile}(chi,z,r,q,x)))\wedge \\ & (\forall y\in X,\sum _{x\in X}P(x,y)L(x,y)=I+J\mathrm{chi}(y))\wedge \\ & (\forall n\in \mathbb{N},\mathrm{pathExpectation}(P,n+1,{\ell }_n)=I)\wedge \\ & \mathrm{pathCovariance}(P,2,{\ell }_0,{\ell }_1)=IJ\wedge \\ & (\forall j\in \mathbb{N},2\le j\Rightarrow \mathrm{pathCovariance}(P,j+1,{\ell }_0,{\ell }_j)=0)\wedge \\ & \forall s\in \mathbb{N},1\le s\Rightarrow \mathrm{pathVariance}(P,s,\sum _{t\in \mathrm{Fin}(s)}{\ell }_t)=sv+2(s-1)IJ\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Estimation/TimeArrow/SinglePeakLogLikelihoodCovariance.exact_single_peak_log_likelihood_covariances (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let X be a finite sign space of cardinality 2M, with exactly M positive signs and a distinguished positive state z. Assume M is at least two, 0 < r < 1, and q = r/(M - 1). The outgoing conditional mean is phi of the local profile, while the incoming conditional mean is I + J chi(y).

Under the explicit uniform-start path weights, the edge at every time n has mean I. The adjacent covariance is I J, every covariance at lag at least two is zero, and the variance of the sum over s edges is s v + 2(s - 1) I J for s at least one.

The lag cutoff follows from the two-step transition identity: after two transitions, the endpoint is uniform independently of the starting state. The variance then accumulates one-edge second moments and the single adjacent covariance.

References

• Truth anchor: D5/S3/Estimation/TimeArrow/SinglePeakLogLikelihoodCovariance.exact_single_peak_log_likelihood_covariances
• Truth anchor: D5/S3/Estimation/TimeArrow/SinglePeakLogLikelihoodCovariance.logIncrement
• Truth anchor: D5/S3/Estimation/TimeArrow/SinglePeakLogLikelihoodCovariance.logLikelihoodSum
• Truth anchor: D5/S3/Estimation/TimeArrow/SinglePeakLogLikelihoodCovariance.pathCovariance
• Truth anchor: D5/S3/Estimation/TimeArrow/SinglePeakLogLikelihoodCovariance.pathExpectation
• Truth anchor: D5/S3/Estimation/TimeArrow/SinglePeakLogLikelihoodCovariance.pathVariance
• Truth anchor: D5/S3/Estimation/TimeArrow/SinglePeakLogLikelihoodCovariance.pathWeight
• Truth anchor: D5/S3/Estimation/TimeArrow/SinglePeakLogLikelihoodCovariance.phi
• Truth anchor: D5/S3/Estimation/TimeArrow/SinglePeakLogLikelihoodCovariance.psi
• Truth anchor: D5/S3/Estimation/TimeArrow/SinglePeakLogLikelihoodCovariance.xi
• Dependency: D5/S3/Estimation/TimeArrow/SinglePeakPathCurrent