Restricting, rescaling and conditioning a sub-distribution

SDistr α is a probability mass function on Option α, so the mass a restriction removes has a place to go: none, the failure outcome. restrict d P sends the mass outside P there, scale d divides the surviving mass by the total mass, and condition d P is their composite — the distribution of a sample from d given that the sample satisfies P.

Main definitions

• restrict d P — d with the mass outside P sent to failure
• scale d — d rescaled to mass one, and SDistr.fail when d has mass zero
• condition d P — scale (restrict d P)
• excepted d X — condition d (fun a => !X a)

Main results

• restrict_apply_some, mass_restrict — the weight of the restriction
• scale_apply_some, mass_scale — the weight of the rescaling
• condition_apply_some — the pointwise weight of the conditional distribution
• mem_support_condition_iff — the support of the conditional distribution
• condition_eq_pure — conditioning on a predicate met by a single point of positive weight is a point mass at that point

Correspondence with EasyCrypt

The four definitions are the images of drestrict, dscale, dcond and (\) of EasyCrypt's Distr and Dexcepted theories, whose definitions are dcond d p = dscale (drestrict d p) and d \ X = dscale (drestrict d (predC X)). condition_apply_some is the image of dexcepted1E, mem_support_condition_iff of supp_dexcepted, and mass_condition_of_ne_zero of dexcepted_ll.

The mass of a sub-distribution as a sum

theorem CatCrypt.NonUniform.mass_eq_tsum {α : Type u_1} (d : Prob.SDistr α) : d.mass = ∑' (a : α), d (some a)

The mass of a sub-distribution is the total weight it puts on some.

theorem CatCrypt.NonUniform.mass_le_one {α : Type u_1} (d : Prob.SDistr α) : d.mass ≤ 1

The mass of a sub-distribution is at most one.

theorem CatCrypt.NonUniform.mass_ne_top {α : Type u_1} (d : Prob.SDistr α) : d.mass ≠ ⊤

theorem CatCrypt.NonUniform.apply_some_eq_zero_of_mass_eq_zero {α : Type u_1} {d : Prob.SDistr α} (h : d.mass = 0) (a : α) : d (some a) = 0

A sub-distribution of mass zero puts no weight on any value.

Restriction

noncomputable def CatCrypt.NonUniform.restrict {α : Type u_1} (d : Prob.SDistr α) (P : α → Bool) : Prob.SDistr α

The sub-distribution d with the weight outside the predicate P sent to failure.

Equations

• CatCrypt.NonUniform.restrict d P = d.bind fun (a : α) => if P a = true then CatCrypt.Prob.SDistr.pure a else CatCrypt.Prob.SDistr.fail

theorem CatCrypt.NonUniform.restrict_apply_some {α : Type u_1} (d : Prob.SDistr α) (P : α → Bool) (b : α) : (restrict d P) (some b) = if P b = true then d (some b) else 0

A restriction keeps the weight of the values satisfying the predicate and drops the rest.

theorem CatCrypt.NonUniform.mass_restrict {α : Type u_1} (d : Prob.SDistr α) (P : α → Bool) : (restrict d P).mass = ∑' (a : α), if P a = true then d (some a) else 0

The mass surviving a restriction is the weight of the values satisfying the predicate.

Rescaling

noncomputable def CatCrypt.NonUniform.scale {α : Type u_1} (d : Prob.SDistr α) : Prob.SDistr α

d rescaled to mass one. A sub-distribution of mass zero rescales to SDistr.fail, which is what EasyCrypt's dscale returns for the null distribution.

Equations

• CatCrypt.NonUniform.scale d = ⟨fun (oa : Option α) => match oa with | none => if d.mass = 0 then 1 else 0 | some a => d (some a) / d.mass, ⋯⟩

theorem CatCrypt.NonUniform.scale_apply_some {α : Type u_1} (d : Prob.SDistr α) (a : α) : (scale d) (some a) = d (some a) / d.mass

Rescaling divides every weight by the mass.

theorem CatCrypt.NonUniform.scale_apply_none {α : Type u_1} {d : Prob.SDistr α} (h : d.mass ≠ 0) : (scale d) none = 0

A rescaled sub-distribution of nonzero mass never fails.

theorem CatCrypt.NonUniform.mass_scale {α : Type u_1} {d : Prob.SDistr α} (h : d.mass ≠ 0) : (scale d).mass = 1

Rescaling a sub-distribution of nonzero mass gives mass one.

Conditioning

noncomputable def CatCrypt.NonUniform.condition {α : Type u_1} (d : Prob.SDistr α) (P : α → Bool) : Prob.SDistr α

The distribution of a sample from d given that it satisfies P.

Equations

• CatCrypt.NonUniform.condition d P = CatCrypt.NonUniform.scale (CatCrypt.NonUniform.restrict d P)

noncomputable def CatCrypt.NonUniform.excepted {α : Type u_1} (d : Prob.SDistr α) (X : α → Bool) : Prob.SDistr α

The distribution of a sample from d given that it avoids X.

Equations

• CatCrypt.NonUniform.excepted d X = CatCrypt.NonUniform.condition d fun (a : α) => !X a

theorem CatCrypt.NonUniform.condition_not_eq_excepted {α : Type u_1} (d : Prob.SDistr α) (X : α → Bool) : (condition d fun (a : α) => !X a) = excepted d X

Conditioning on the complement of X is avoiding X.

theorem CatCrypt.NonUniform.condition_apply_some {α : Type u_1} (d : Prob.SDistr α) (P : α → Bool) (a : α) : (condition d P) (some a) = (if P a = true then d (some a) else 0) / ∑' (b : α), if P b = true then d (some b) else 0

The weight the conditional distribution puts on a value: its weight under d when it satisfies the predicate, divided by the total weight of the values that do.

theorem CatCrypt.NonUniform.excepted_apply_some {α : Type u_1} (d : Prob.SDistr α) (X : α → Bool) (a : α) : (excepted d X) (some a) = (if X a = true then 0 else d (some a)) / ∑' (b : α), if X b = true then 0 else d (some b)

The weight the excepted distribution puts on a value.

theorem CatCrypt.NonUniform.mem_support_condition_iff {α : Type u_1} (d : Prob.SDistr α) (P : α → Bool) (a : α) : a ∈ (condition d P).support ↔ a ∈ d.support ∧ P a = true

The support of the conditional distribution is the part of d's support the predicate admits.

theorem CatCrypt.NonUniform.mass_condition_of_ne_zero {α : Type u_1} {d : Prob.SDistr α} {P : α → Bool} (h : (∑' (b : α), if P b = true then d (some b) else 0) ≠ 0) : (condition d P).mass = 1

The mass of a conditional distribution is one when the predicate has positive weight.

theorem CatCrypt.NonUniform.condition_eq_pure {α : Type u_1} (d : Prob.SDistr α) (P : α → Bool) (a : α) (hunique : ∀ (b : α), P b = true → b = a) (ha : P a = true) (hd : d (some a) ≠ 0) : condition d P = Prob.SDistr.pure a

Conditioning on a predicate that only one value of positive weight satisfies is a point mass at that value.

Sampling from a conditional distribution

theorem CatCrypt.NonUniform.sampleFrom_condition_eq_pure {α : Type u_1} (d : Prob.SDistr α) (P : α → Bool) (a : α) (hunique : ∀ (b : α), P b = true → b = a) (ha : P a = true) (hd : d (some a) ≠ 0) : sampleFrom (condition d P) = Core.SPComp.pure a

Sampling from a conditional distribution whose predicate admits a single value of positive weight returns that value.