Documentation

Complexity.Probability.Conditioning

Conditioning discrete joint distributions #

conditionalSnd joint a uses the upstream posterior distribution to recover the second component after observing a in the first. At a zero-probability observation it defaults to the second marginal. The joint law and all weighted averages are independent of this choice. No finiteness assumption is needed for the conditional distribution or its reconstruction law.

Main definitions #

Main results #

References #

Adapted from Probability/Conditioning.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, reusing the upstream PMF operations.

source
theorem Cslib.Probability.PMF.map_fst_apply {α : Type u_1} {β : Type u_2} (joint : PMF (α × β)) (a : α) :
(PMF.map Prod.fst joint) a = ∑' (b : β), joint (a, b)

The first marginal is the sum of the corresponding joint slice.

source
noncomputable def Cslib.Probability.PMF.conditionalSnd {α : Type u_1} {β : Type u_2} (joint : PMF (α × β)) (a : α) :
PMF β

The second component conditioned on the first, defaulting to its marginal at null events.

Instances For
    source
    theorem Cslib.Probability.PMF.conditionalSnd_apply {α : Type u_1} {β : Type u_2} (joint : PMF (α × β)) (a : α) (ha : a ∈ (PMF.map Prod.fst joint).support) (b : β) :
    (conditionalSnd joint a) b = joint (a, b) / (PMF.map Prod.fst joint) a

    At a positive-probability observation, conditional probabilities are normalized joint masses.

    source
    theorem Cslib.Probability.PMF.marginal_mul_conditionalSnd {α : Type u_1} {β : Type u_2} (joint : PMF (α × β)) (a : α) (b : β) :
    (PMF.map Prod.fst joint) a * (conditionalSnd joint a) b = joint (a, b)

    Multiplying by the marginal recovers the joint mass, also at zero-probability observations.

    source
    theorem Cslib.Probability.PMF.apply_le_conditionalSnd {α : Type u_1} {β : Type u_2} (joint : PMF (α × β)) (a : α) (b : β) :
    joint (a, b) ≤ (conditionalSnd joint a) b

    Removing the probability of the observation can only increase the joint outcome's mass.

    source
    theorem Cslib.Probability.PMF.mem_support_conditionalSnd_iff {α : Type u_1} {β : Type u_2} (joint : PMF (α × β)) (a : α) (ha : a ∈ (PMF.map Prod.fst joint).support) (b : β) :
    b ∈ (conditionalSnd joint a).support ↔ (a, b) ∈ joint.support

    At an observable first component, the conditional support is exactly the joint slice.

    source
    theorem Cslib.Probability.PMF.bind_conditionalSnd {α : Type u_1} {β : Type u_2} (joint : PMF (α × β)) :
    ((PMF.map Prod.fst joint).bind fun (a : α) => PMF.map (fun (x : β) => (a, x)) (conditionalSnd joint a)) = joint

    Sampling the marginal and then the conditional distribution reconstructs the joint law.

    source
    theorem Cslib.Probability.PMF.conditionalSnd_bind_pair {α : Type u_1} {β : Type u_2} (p : PMF α) (kernel : α → PMF β) (a : α) (ha : a ∈ p.support) :
    conditionalSnd (p.bind fun (a : α) => PMF.map (fun (x : β) => (a, x)) (kernel a)) a = kernel a

    Conditioning a joint sampler on a possible first component recovers its conditional kernel.

    source
    theorem Cslib.Probability.PMF.sum_conditionalSnd_map {α : Type u_1} {β : Type u_2} [Fintype α] [Finite β] (p : PMF α) (f : α → β) (score : β → α → ℝ) :
    ∑ x : α, (p x).toReal * ∑ y : α, ((conditionalSnd (PMF.map (fun (a : α) => (f a, a)) p) (f x)) y).toReal * score (f x) y = ∑ x : α, (p x).toReal * score (f x) x

    A score can be averaged by first revealing a deterministic observation and then resampling the input conditionally. The score may depend on both the observation and the hidden input.

    source
    theorem Cslib.Probability.PMF.conditionalSnd_uniform_map {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] (f : α → β) (b : β) [Nonempty { a : α // f a = b }] :
    conditionalSnd (PMF.map (fun (a : α) => (f a, a)) (uniformOfFintype α)) b = PMF.map Subtype.val (uniformOfFintype { a : α // f a = b })

    Conditioning a uniform input on its image gives the uniform distribution on that fiber. The nonempty assumption restricts this statement to observable images.