Mechanism.pmf: Stochastic Mechanism Constructor (V2) #
Trivial wrapper turning a PMF-valued function into a Mechanism.
Symmetric counterpart to Mechanism.deterministic — kept for naming
parallelism and discoverability.
def
Core.Causal.Mechanism.pmf
{V : Type u_1}
{α : V → Type u_2}
{G : CausalGraph V}
{v : V}
(f : ((u : ↥(G.parents v)) → α ↑u) → PMF (α v))
:
Mechanism G α v
The general (probabilistic) mechanism constructor. Turns any
PMF-valued function over parents into a Mechanism.
Equations
- Core.Causal.Mechanism.pmf f = { run := f }
Instances For
@[simp]
theorem
Core.Causal.Mechanism.pmf_run
{V : Type u_1}
{α : V → Type u_2}
{G : CausalGraph V}
{v : V}
(f : ((u : ↥(G.parents v)) → α ↑u) → PMF (α v))
(ρ : (u : ↥(G.parents v)) → α ↑u)
: