Finite probability laws and kernels

Definition

fep_finite_laws

by ActiveInference · Sep 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

active-inferencefinite-statefree-energy-principleprobability

The mission's finite substrate: normalized finite laws and finite Markov kernels, plus the joint/predictive/posterior constructions the mission's theorems rest on.

A finite law on a finite type $\alpha$ is a mass function $p : \alpha \to \mathbb{R}$ satisfying two constructor fields: nonnegativity $p(x) \ge 0$ for every $x$ , and normalization $\sum_x p(x) = 1$ . A finite kernel from $\alpha$ to $\beta$ assigns to each $x \in \alpha$ a normalized row $k(x, \cdot)$ : nonnegative and summing to $1$ over $\beta$ .

The file also packages, as proved constructions:

the row law of a kernel at a fixed input;
the joint law of a prior and kernel, $(prior, k)$ with mass $p(x)\,k(x,y)$ ;
the predictive law (the evidence marginal) $\sum_x p(x)\,k(x,y)$ ;
the exact finite Bayes posterior at evidence $y$ with positive predictive mass: $P(x \mid y) = p(x)\,k(x,y)\,/\,P(y)$ , with the reconstruction lemma $P(x \mid y)\,P(y) = p(x)\,k(x,y)$ .

Downstream definitions cannot silently accept arbitrary weight vectors as probability laws: nonnegativity and total mass one are constructor fields, not properties proved later.

Formalization Note — transcribed verbatim (module renamed into the mission namespace FreeEnergyPrinciple) from the proved module FepSketches.finite_probability of the fep_lean formalization (Active Inference Institute, v1.2.0); the file compiles sorry-free.

Definition code

import Mathlib.Algebra.BigOperators.Ring.Finset
import Mathlib.Data.Fintype.Card
import Mathlib.Tactic

/-!
# Finite probability laws and kernels (mission substrate)

Mission `Free Energy Principle I` shared finite substrate, transcribed from the
proved module `FepSketches.finite_probability` of the fep_lean formalization
(Active Inference Institute).  One normalized real-valued carrier for the
finite-state parts of the FEP: nonnegativity and total mass one are
construction fields, so downstream definitions cannot silently accept
arbitrary weight vectors as probability laws.
-/

namespace FreeEnergyPrinciple

open Finset
open scoped BigOperators

/-- A probability law on a finite type, represented by normalized real mass. -/
structure FiniteLaw (α : Type*) [Fintype α] where
  mass : α → ℝ
  nonneg : ∀ x, 0 ≤ mass x
  sum_one : ∑ x, mass x = 1

namespace FiniteLaw

variable {α β γ : Type*} [Fintype α] [Fintype β] [Fintype γ]

instance : CoeFun (FiniteLaw α) (fun _ => α → ℝ) := ⟨FiniteLaw.mass⟩

@[simp]
theorem coe_mass (p : FiniteLaw α) (x : α) : p x = p.mass x := rfl

/-- Finite laws are equal when their mass functions are equal. -/
@[ext]
theorem ext_mass {p q : FiniteLaw α} (h : p.mass = q.mass) : p = q := by
  cases p
  cases q
  cases h
  rfl

/-- Every atom of a finite law lies in the unit interval. -/
theorem mass_le_one (p : FiniteLaw α) (x : α) : p x ≤ 1 := by
  classical
  calc
    p x ≤ ∑ y : α, p y :=
      Finset.single_le_sum (fun y _ => p.nonneg y) (Finset.mem_univ x)
    _ = 1 := p.sum_one

/-- Second marginal of a finite joint law. -/
def sndMarginal (p : FiniteLaw (α × β)) : FiniteLaw β where
  mass y := ∑ x : α, p (x, y)
  nonneg y := Finset.sum_nonneg fun x _ => p.nonneg (x, y)
  sum_one := by
    rw [Finset.sum_comm]
    simpa [Fintype.sum_prod_type] using p.sum_one

end FiniteLaw

/-- A normalized finite Markov kernel. -/
structure FiniteKernel (α β : Type*) [Fintype α] [Fintype β] where
  mass : α → β → ℝ
  nonneg : ∀ x y, 0 ≤ mass x y
  sum_one : ∀ x, ∑ y, mass x y = 1

namespace FiniteKernel

variable {α β γ : Type*} [Fintype α] [Fintype β] [Fintype γ]

instance : CoeFun (FiniteKernel α β) (fun _ => α → β → ℝ) :=
  ⟨FiniteKernel.mass⟩

/-- Finite kernels are equal when their mass functions are equal. -/
@[ext]
theorem ext_mass {kernel₁ kernel₂ : FiniteKernel α β}
    (h : kernel₁.mass = kernel₂.mass) : kernel₁ = kernel₂ := by
  cases kernel₁
  cases kernel₂
  cases h
  rfl

/-- Each input of a normalized kernel indexes a finite output law. -/
def row (kernel : FiniteKernel α β) (x : α) : FiniteLaw β where
  mass y := kernel x y
  nonneg y := kernel.nonneg x y
  sum_one := kernel.sum_one x

/-- Joint law generated by a prior and a normalized finite kernel. -/
def joint (prior : FiniteLaw α) (kernel : FiniteKernel α β) :
    FiniteLaw (α × β) where
  mass xy := prior xy.1 * kernel xy.1 xy.2
  nonneg xy := mul_nonneg (prior.nonneg xy.1) (kernel.nonneg xy.1 xy.2)
  sum_one := by
    classical
    rw [Fintype.sum_prod_type]
    simp_rw [← Finset.mul_sum, kernel.sum_one, mul_one]
    exact prior.sum_one

/-- Predictive output law obtained by marginalizing a prior-kernel joint. -/
def predictive (prior : FiniteLaw α) (kernel : FiniteKernel α β) : FiniteLaw β :=
  (joint prior kernel).sndMarginal

@[simp]
theorem predictive_mass (prior : FiniteLaw α) (kernel : FiniteKernel α β)
    (y : β) :
    predictive prior kernel y = ∑ x : α, prior x * kernel x y := rfl

/-- Exact finite Bayes posterior at evidence with positive predictive mass. -/
noncomputable def posterior (prior : FiniteLaw α) (kernel : FiniteKernel α β)
    (y : β) (hy : 0 < predictive prior kernel y) : FiniteLaw α where
  mass x := prior x * kernel x y / predictive prior kernel y
  nonneg x := div_nonneg (mul_nonneg (prior.nonneg x) (kernel.nonneg x y)) hy.le
  sum_one := by
    rw [← Finset.sum_div]
    exact div_self (ne_of_gt hy)

/-- Bayes reconstruction: posterior mass times evidence equals joint mass. -/
theorem posterior_mul_predictive (prior : FiniteLaw α)
    (kernel : FiniteKernel α β) (y : β)
    (hy : 0 < predictive prior kernel y) (x : α) :
    posterior prior kernel y hy x * predictive prior kernel y =
      prior x * kernel x y := by
  change
    (prior x * kernel x y / predictive prior kernel y) *
        predictive prior kernel y = _
  exact div_mul_cancel₀ _ (ne_of_gt hy)

end FiniteKernel

end FreeEnergyPrinciple

Source

fep_lean / fep_formal v1.2.0 (Active Inference Institute), FepSketches.finite_probability.lean (proved, 0 sorry); https://github.com/ActiveInferenceInstitute/fep_formal

Read-back

What the Lean code literally says, in plain math · glm-flash-latest

Read-back

The declaration contains a single theorem of substantive mathematical content, posterior_mul_predictive, plus several auxiliary definitions. This read-back covers the theorem and each definition it depends on.

Definitions

Finite laws. Let $\alpha$ be a finite type. A finite law on $\alpha$ is a real-valued function $p : \alpha \to \mathbb{R}$ (stored as a field mass) satisfying two conditions:

nonnegativity: $p(x) \ge 0$ for every $x \in \alpha$ ;
total mass one: $\displaystyle\sum_{x \in \alpha} p(x) = 1$ .

Finite kernels. Let $\alpha, \beta$ be finite types. A finite kernel from $\alpha$ to $\beta$ is a real-valued function $k : \alpha \to \beta \to \mathbb{R}$ such that, for every input $x \in \alpha$ :

$k(x, y) \ge 0$ for every $y \in \beta$ ;
$\displaystyle\sum_{y \in \beta} k(x, y) = 1$ .

That is, each row of $k$ is a finite law on $\beta$ (this is the content of the auxiliary definition row).

Joint law. Given a finite law $p$ on $\alpha$ and a finite kernel $k : \alpha \to \beta$ , the joint law is the finite law on $\alpha \times \beta$ defined by

(p \otimes k)\big((x, y)\big) \;=\; p(x)\, k(x, y).

Second marginal. For a finite law $p$ on $\alpha \times \beta$ , the second marginal is the finite law on $\beta$ given by

\operatorname{snd}(p)(y) \;=\; \sum_{x \in \alpha} p\big((x, y)\big).

Predictive law. For a finite law $p$ on $\alpha$ and a kernel $k : \alpha \to \beta$ , the predictive law on $\beta$ is the second marginal of the joint law. By definition (and a stated identity), its mass at $y \in \beta$ is

\operatorname{pred}(p, k)(y) \;=\; \sum_{x \in \alpha} p(x)\, k(x, y).

Posterior. Given $p$ , $k$ , a point $y \in \beta$ , and the hypothesis

h_y:\; \operatorname{pred}(p, k)(y) > 0,

the posterior is the finite law on $\alpha$ defined by

\operatorname{post}(p, k, y, h_y)(x) \;=\; \frac{p(x)\, k(x, y)}{\operatorname{pred}(p, k)(y)}.

Two auxiliary facts hold: every atom of a finite law satisfies $0 \le p(x) \le 1$ ; and two finite laws (respectively, two finite kernels) are equal precisely when their mass functions are equal (respectively, when their two-variable mass functions are equal).

Theorem `posterior_mul_predictive`

Let $\alpha, \beta$ be finite types, let $p$ be a finite law on $\alpha$ and $k : \alpha \to \beta$ a finite kernel. Fix $y \in \beta$ with the hypothesis that

0 \;<\; \operatorname{pred}(p, k)(y) \;=\; \sum_{x \in \alpha} p(x)\, k(x, y),

i.e. the total predictive mass of the evidence $y$ is strictly positive. Then for every $x \in \alpha$ ,

\operatorname{post}(p, k, y, h_y)(x)\;\cdot\;\operatorname{pred}(p, k)(y)\;=\;p(x)\, k(x, y),

i.e. the posterior mass at $x$ , multiplied by the evidence's predictive mass, recovers the joint mass at $(x, y)$ exactly.

Scope notes

All functions here are total. The hypothesis $0 < \operatorname{pred}(p, k)(y)$ is required in the statement; without it, the division in the posterior definition would be undefined (division by a zero denominator), so the theorem does not claim anything for $y$ with zero predictive mass.
There is no a priori constraint on $\alpha$ or $\beta$ beyond being equipped with finite-type structure; the trivial case $\alpha$ or $\beta$ empty is included in the quantification.

Human review

Endorsed by Shuze Chen · Sep 24, 2026
Confirmed by the moderator at approval.
Endorsed by ActiveInference · Sep 24, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Finite probability laws and kernels

Read-back

Definitions

Theorem posterior_mul_predictive

Scope notes

Theorem `posterior_mul_predictive`