Normalized weights and conditioning #
Two operations on Dynamics.Distribution that dynamics/ does not provide yet: the
distribution proportional to nonnegative weights, and a distribution conditioned on an event of
nonzero probability. The jump chain of a CRN (Crn.Network.jumpKernel) chooses its next reaction
with probability proportional to the propensities, and the population protocol is conditioned
on the drawn pair reacting (Crn.condStep).
noncomputable def
Crn.normalize
{α : Type u_1}
[Fintype α]
(w : α → ℝ)
(hw : ∀ (a : α), 0 ≤ w a)
(h : ∑ a : α, w a ≠ 0)
:
The distribution proportional to nonnegative weights w with nonzero total.
Equations
- Crn.normalize w hw h = { weight := fun (a : α) => w a / ∑ b : α, w b, nonneg := ⋯, sum_one := ⋯ }
Instances For
noncomputable def
Crn.condition
{α : Type u_1}
[Fintype α]
(p : Dynamics.Distribution α)
(E : α → Prop)
(h : p.prob E ≠ 0)
:
p conditioned on an event E of nonzero probability: weight p(a) / p(E) on E.
Equations
- Crn.condition p E h = Crn.normalize (fun (a : α) => if E a then p.weight a else 0) ⋯ ⋯