Biased coins: a non-uniform coupling worked out

bernoulli p is the coin that comes up true with probability p. For p ≠ 1/2 it is not the uniform distribution on Bool, and no bijection of Bool carries it to itself, so liftR_uniform_bij and rHoare_bij_step cannot relate two differently-biased coins. Negation does carry bernoulli p to bernoulli (1 - p), which is a pushforward coupling: rHoare_bernoulli_flip turns it into a pRHL sampling step, and bernoulli_flip_program_eq shows a bernoulli p sample can be renamed as the negation of a bernoulli (1 - p) sample inside any program.

Main results

• bernoulli_apply_true, bernoulli_apply_false — the two masses
• bernoulli_ne_uniform, bernoulli_third_ne_uniform — a coin whose two masses differ is not uniform
• bernoulli_bind_not — negation pushes bernoulli p to bernoulli (1 - p)
• liftR_bernoulli_not — the resulting coupling
• rHoare_bernoulli_flip — the pRHL sampling step
• bernoulli_flip_program_eq — the two programs are equal
• prTrue_bernoulli_bind, prTrue_bernoulli — the unary averaging rule applied

The distribution

noncomputable def CatCrypt.NonUniform.bernoulli (p : NNReal) (hp : p ≤ 1) : Prob.SDistr Bool

The coin that comes up true with probability p: the Bernoulli measure on Bool with mass p at true and 1 - p at false, read back as a PMF.

Equations

• CatCrypt.NonUniform.bernoulli p hp = CatCrypt.NonUniform.ofPMF (ProbabilityTheory.bernoulliMeasure true false ⟨↑p, ⋯⟩).toPMF

theorem CatCrypt.NonUniform.bernoulli_apply_some (p : NNReal) (hp : p ≤ 1) (b : Bool) : (bernoulli p hp) (some b) = ↑(bif b then p else 1 - p)

The mass of a Bernoulli coin at a Boolean outcome.

@[simp]

theorem CatCrypt.NonUniform.bernoulli_apply_true (p : NNReal) (hp : p ≤ 1) : (bernoulli p hp) (some true) = ↑p

@[simp]

theorem CatCrypt.NonUniform.bernoulli_apply_false (p : NNReal) (hp : p ≤ 1) : (bernoulli p hp) (some false) = ↑(1 - p)

@[simp]

theorem CatCrypt.NonUniform.mass_bernoulli (p : NNReal) (hp : p ≤ 1) : (bernoulli p hp).mass = 1

theorem CatCrypt.NonUniform.isLossless_sampleFrom_bernoulli (p : NNReal) (hp : p ≤ 1) : Unary.isLossless (sampleFrom (bernoulli p hp))

sampleFrom (bernoulli p) never fails.

theorem CatCrypt.NonUniform.bernoulli_ne_uniform (p : NNReal) (hp : p ≤ 1) (hne : ↑p ≠ ↑(1 - p)) : bernoulli p hp ≠ Prob.SDistr.uniform Bool

A Bernoulli coin can be uniform only if its two masses agree.

The coupling

theorem CatCrypt.NonUniform.bernoulli_bind_not (p : NNReal) (hp : p ≤ 1) (hp' : 1 - p ≤ 1) : ((bernoulli p hp).bind fun (b : Bool) => Prob.SDistr.pure !b) = bernoulli (1 - p) hp'

Negating a bernoulli p sample yields a bernoulli (1 - p) sample.

theorem CatCrypt.NonUniform.liftR_bernoulli_not (p : NNReal) (hp : p ≤ 1) (hp' : 1 - p ≤ 1) : bernoulli p hp ⟨fun (a b : Bool) => (!a) = b⟩# bernoulli (1 - p) hp'

bernoulli p and bernoulli (1 - p) are coupled by Boolean negation.

Unlike the uniform bijection coupling, the two marginals here are different distributions: negation is a bijection of Bool that does not preserve bernoulli p unless p = 1/2.

The pRHL step

theorem CatCrypt.NonUniform.rHoare_bernoulli_flip {γ : Type u_1} {δ : Type u_2} {Φ : Relational.RPre} {Ψ : Relational.RPost γ δ} (p : NNReal) (hp : p ≤ 1) (hp' : 1 - p ≤ 1) {k₁ : Bool → Core.SPComp γ} {k₂ : Bool → Core.SPComp δ} (h : ∀ (b : Bool), Relational.rHoare Φ (k₁ b) (k₂ !b) Ψ) : Relational.rHoare Φ ((sampleFrom (bernoulli p hp)).bind k₁) ((sampleFrom (bernoulli (1 - p) hp')).bind k₂) Ψ

pRHL sampling step for two coins of complementary bias: a bernoulli p sample on the left is matched by the negated bernoulli (1 - p) sample on the right.

theorem CatCrypt.NonUniform.bernoulli_flip_program_eq {α : Type u_3} (p : NNReal) (hp : p ≤ 1) (hp' : 1 - p ≤ 1) (k : Bool → Core.SPComp α) : ((sampleFrom (bernoulli p hp)).bind fun (b : Bool) => k !b) = (sampleFrom (bernoulli (1 - p) hp')).bind k

Sampling bernoulli p and negating is sampling bernoulli (1 - p), inside an arbitrary continuation. Derived from the coupling step at eqPre/eqPost.

The unary rule applied

theorem CatCrypt.NonUniform.prTrue_bernoulli_bind (p : NNReal) (hp : p ≤ 1) (k : Bool → Core.SPComp Bool) (h₀ : Core.Heap) : Crypto.prTrue ((sampleFrom (bernoulli p hp)).bind k) h₀ = ↑p * Crypto.prTrue (k true) h₀ + ↑(1 - p) * Crypto.prTrue (k false) h₀

The success probability of a game that starts with a biased coin is the p-weighted average of the two branch probabilities.

theorem CatCrypt.NonUniform.prTrue_bernoulli (p : NNReal) (hp : p ≤ 1) (h₀ : Core.Heap) : Crypto.prTrue (sampleFrom (bernoulli p hp)) h₀ = ↑p

A biased coin returns true with probability exactly p.

theorem CatCrypt.NonUniform.prTrue_bernoulli_not (p : NNReal) (hp : p ≤ 1) (hp' : 1 - p ≤ 1) (h₀ : Core.Heap) : Crypto.prTrue ((sampleFrom (bernoulli p hp)).bind fun (b : Bool) => Core.SPComp.pure !b) h₀ = ↑(1 - p)

Cross-check of the coupling against the unary rule: negating a bernoulli p coin is a bernoulli (1 - p) coin, both routes giving 1 - p.

Satisfiability witness

The hypotheses of rHoare_bernoulli_flip are inhabited at a concretely non-uniform bias: p = 1/3 gives a coupling of the 1/3-coin with the 2/3-coin, and bernoulli_ne_uniform shows the 1/3-coin is not uniform, so the step is not a disguised uniform one.

theorem CatCrypt.NonUniform.one_third_le_one : 1 / 3 ≤ 1

theorem CatCrypt.NonUniform.one_sub_one_third_le_one : 1 - 1 / 3 ≤ 1

theorem CatCrypt.NonUniform.coe_one_third_ne_coe_two_thirds : ↑(1 / 3) ≠ ↑(1 - 1 / 3)

1/3 ≠ 2/3, transported to ℝ≥0∞.

theorem CatCrypt.NonUniform.bernoulli_third_ne_uniform : bernoulli (1 / 3) one_third_le_one ≠ Prob.SDistr.uniform Bool

The 1/3-coin is not the uniform distribution on Bool.

theorem CatCrypt.NonUniform.liftR_bernoulli_third : bernoulli (1 / 3) one_third_le_one ⟨fun (a b : Bool) => (!a) = b⟩# bernoulli (1 - 1 / 3) one_sub_one_third_le_one

A concrete coupling of the 1/3-coin with the 2/3-coin. Its two marginals are distinct distributions, and the left one is not uniform (bernoulli_third_ne_uniform).

theorem CatCrypt.NonUniform.bernoulli_third_marginals_ne : bernoulli (1 / 3) one_third_le_one ≠ bernoulli (1 - 1 / 3) one_sub_one_third_le_one

The two marginals of liftR_bernoulli_third differ.