Emission posterior: inferring a partially observed joint action

For a kernel κ : α → PMF (β × γ) emitting a pair of which only the first component is observed, PMF.emissionPosterior κ μ b is the Bayesian posterior over α × γ — state together with unobserved component — given observation b: the normalization of (a, g) ↦ μ a · κ a (b, g).

This is the dual of JointPosterior.lean: there the state is a product and the observation is total; here the emission is a product and the observation is partial, which no PMF-valued kernel into β can express (the slice (a, g) ↦ κ a (b, g) sums to the γ-marginal, not to 1). At γ := Unit the construction collapses to PMF.posterior.

Main definitions

• PMF.emissionPosterior — posterior over α × γ from observing the first component of a jointly emitted pair.

Main results

• emissionPosterior_fst_lt_iff / emissionPosterior_snd_lt_iff — marginal comparisons reduce to prior-weighted emission sums.
• emissionPosterior_uniform_fst_lt_iff / _uniform_snd_lt_iff — at a uniform prior, to bare emission sums.

theorem PMF.tsum_emission_score_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype β] [Fintype γ] [DecidableEq β] (κ : α → PMF (β × γ)) (μ : PMF α) (b : β) : ∑' (x : α × γ), μ x.1 * (κ x.1) (b, x.2) = marginal (fun (a : α) => (κ a).fst) μ b

The total score of an emission posterior is the observation marginal of the fst-projected kernel.

noncomputable def PMF.emissionPosterior {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype β] [Fintype γ] [DecidableEq β] (κ : α → PMF (β × γ)) (μ : PMF α) (b : β) (h : marginal (fun (a : α) => (κ a).fst) μ b ≠ 0) : PMF (α × γ)

The conditional distribution over state and unobserved emission component (a, g), given that the kernel κ emitted a pair with observed first component b.

Equations

• PMF.emissionPosterior κ μ b h = PMF.normalize (fun (x : α × γ) => μ x.1 * (κ x.1) (b, x.2)) ⋯ ⋯

theorem PMF.emissionPosterior_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype β] [Fintype γ] [DecidableEq β] (κ : α → PMF (β × γ)) (μ : PMF α) (b : β) (h : marginal (fun (a : α) => (κ a).fst) μ b ≠ 0) (x : α × γ) : (emissionPosterior κ μ b h) x = μ x.1 * (κ x.1) (b, x.2) * (marginal (fun (a : α) => (κ a).fst) μ b)⁻¹

theorem PMF.emission_marginal_ne_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype β] [Fintype γ] [DecidableEq β] (κ : α → PMF (β × γ)) (μ : PMF α) {a : α} {b : β} {g : γ} (hμ : μ a ≠ 0) (hκ : (κ a) (b, g) ≠ 0) : marginal (fun (a : α) => (κ a).fst) μ b ≠ 0

A single witness (a, g) with μ a ≠ 0 and κ a (b, g) ≠ 0 makes the observation marginal non-zero.

theorem PMF.emissionPosterior_fst_lt_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype β] [Fintype γ] [DecidableEq β] [Fintype α] [DecidableEq α] (κ : α → PMF (β × γ)) (μ : PMF α) (b : β) (h : marginal (fun (a : α) => (κ a).fst) μ b ≠ 0) (a₁ a₂ : α) : (emissionPosterior κ μ b h).fst a₁ < (emissionPosterior κ μ b h).fst a₂ ↔ ∑ g : γ, μ a₁ * (κ a₁) (b, g) < ∑ g : γ, μ a₂ * (κ a₂) (b, g)

Comparing state marginals of the emission posterior reduces to comparing prior-weighted emission sums; the observation marginal cancels.

theorem PMF.emissionPosterior_snd_lt_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype β] [Fintype γ] [DecidableEq β] [Fintype α] [DecidableEq γ] (κ : α → PMF (β × γ)) (μ : PMF α) (b : β) (h : marginal (fun (a : α) => (κ a).fst) μ b ≠ 0) (g₁ g₂ : γ) : (emissionPosterior κ μ b h).snd g₁ < (emissionPosterior κ μ b h).snd g₂ ↔ ∑ a : α, μ a * (κ a) (b, g₁) < ∑ a : α, μ a * (κ a) (b, g₂)

Companion of emissionPosterior_fst_lt_iff for the unobserved component.

theorem PMF.emissionPosterior_uniform_fst_lt_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype β] [Fintype γ] [DecidableEq β] [Fintype α] [DecidableEq α] [Nonempty α] (κ : α → PMF (β × γ)) (b : β) (h : marginal (fun (a : α) => (κ a).fst) (uniformOfFintype α) b ≠ 0) (a₁ a₂ : α) : (emissionPosterior κ (uniformOfFintype α) b h).fst a₁ < (emissionPosterior κ (uniformOfFintype α) b h).fst a₂ ↔ ∑ g : γ, (κ a₁) (b, g) < ∑ g : γ, (κ a₂) (b, g)

At a uniform prior the prior cancels: state comparison reduces to bare emission sums over the unobserved component.

theorem PMF.emissionPosterior_uniform_snd_lt_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype β] [Fintype γ] [DecidableEq β] [Fintype α] [DecidableEq γ] [Nonempty α] (κ : α → PMF (β × γ)) (b : β) (h : marginal (fun (a : α) => (κ a).fst) (uniformOfFintype α) b ≠ 0) (g₁ g₂ : γ) : (emissionPosterior κ (uniformOfFintype α) b h).snd g₁ < (emissionPosterior κ (uniformOfFintype α) b h).snd g₂ ↔ ∑ a : α, (κ a) (b, g₁) < ∑ a : α, (κ a) (b, g₂)

At a uniform prior the prior cancels: emission-component comparison reduces to bare emission sums over states.