Mechanism.deterministic: Deterministic-as-Dirac Constructor (V2)

The deterministic mechanism induced by an honest function over parents is built as a Dirac PMF — the exact mathlib pattern from Mathlib/Probability/Kernel/Basic.lean where Kernel.deterministic (f) := dirac ∘ f.

noncomputable def Core.Causal.Mechanism.deterministic {V : Type u_1} {α : V → Type u_2} {G : CausalGraph V} {v : V} (f : ((u : ↥(G.parents v)) → α ↑u) → α v) : Mechanism G α v

The deterministic mechanism induced by an honest function over parents. Mirrors Kernel.deterministic from Mathlib/Probability/Kernel/Basic.lean. Noncomputable because PMF.pure is noncomputable.

Equations

• Core.Causal.Mechanism.deterministic f = { run := fun (ρ : (u : ↥(G.parents v)) → α ↑u) => PMF.pure (f ρ) }

@[simp]

theorem Core.Causal.Mechanism.deterministic_run {V : Type u_1} {α : V → Type u_2} {G : CausalGraph V} {v : V} (f : ((u : ↥(G.parents v)) → α ↑u) → α v) (ρ : (u : ↥(G.parents v)) → α ↑u) : (deterministic f).run ρ = PMF.pure (f ρ)

@[implicit_reducible]

instance Core.Causal.Mechanism.instIsDeterministicDeterministic {V : Type u_1} {α : V → Type u_2} {G : CausalGraph V} {v : V} (f : ((u : ↥(G.parents v)) → α ↑u) → α v) : (deterministic f).IsDeterministic

Deterministic mechanisms satisfy the IsDeterministic mixin.

Equations

• Core.Causal.Mechanism.instIsDeterministicDeterministic f = { toFun := f, run_eq := ⋯ }

@[simp]

theorem Core.Causal.Mechanism.deterministic_toFun {V : Type u_1} {α : V → Type u_2} {G : CausalGraph V} {v : V} (f : ((u : ↥(G.parents v)) → α ↑u) → α v) : IsDeterministic.toFun (deterministic f) = f

noncomputable def Core.Causal.Mechanism.const {V : Type u_1} {α : V → Type u_2} {G : CausalGraph V} {v : V} (x : α v) : Mechanism G α v

A constant mechanism: ignores parents, always returns the same value via Dirac. Useful for intervene-style mechanism replacement. Noncomputable inherited via deterministic.

Equations

• Core.Causal.Mechanism.const x = Core.Causal.Mechanism.deterministic fun (x_1 : (u : ↥(G.parents v)) → α ↑u) => x

@[simp]

theorem Core.Causal.Mechanism.const_run {V : Type u_1} {α : V → Type u_2} {G : CausalGraph V} {v : V} (x : α v) (ρ : (u : ↥(G.parents v)) → α ↑u) : (const x).run ρ = PMF.pure x

@[implicit_reducible]

instance Core.Causal.Mechanism.instIsDeterministicConst {V : Type u_1} {α : V → Type u_2} {G : CausalGraph V} {v : V} (x : α v) : (const x).IsDeterministic

Equations

• Core.Causal.Mechanism.instIsDeterministicConst x = { toFun := fun (x_1 : (u : ↥(G.parents v)) → α ↑u) => x, run_eq := ⋯ }