Exchangeable coin flips: the worked example of a random bias

This file discharges the second worked example of the Exchangeability roadmap (TauCetiRoadmap/Exchangeability/README.md, "Worked examples"):

A Bool-valued sequence generated conditionally i.i.d. given a random θ (draw θ, then flip i.i.d. κ (θ ω)-coins) is exchangeable, with ω ↦ κ (θ ω) (κ a two-point kernel) as the directing measure — genuinely: the generating construction makes it a witness of ConditionallyIIDWith, not merely a mixing representative.

The two-point kernel is coinKernel p = Ber(true, false, p), Mathlib's bernoulliMeasure bundled as a ProbabilityMeasure Bool; the parameter θ is the first coordinate of the canonical space I × (ℕ → Bool) and the bias measure π is arbitrary. As the roadmap insists, the directing measure is the random probability measure ω ↦ coinKernel ω.1, not the bias ω ↦ ω.1 itself.

The example carries weight because the sequence is exchangeable without being independent: not_iIndepFun_coinFlips exhibits a two-point bias law for which the coordinates are dependent, so ConditionallyIID really is a wider class than i.i.d. and the constructed directing measure is not a disguised constant.

Main results

• coinKernel — the two-point kernel p ↦ Ber(true, false, p), with measurable_coinKernel and the bias readout coinKernel_apply_true.
• conditionallyIIDWith_coinFlips — the coin-flip sequence is conditionally i.i.d. with directing measure ω ↦ coinKernel ω.1, hence exchangeable_coinFlips and contractable_coinFlips.
• not_iIndepFun_coinFlips — for a bias that is genuinely random the flips are not independent.

The construction it instantiates is iidMixtureLaw in TauCeti/Probability/Exchangeability/ConditionallyIID/Construct.lean. Nothing here is adapted from cameronfreer/exchangeability.

noncomputable def TauCeti.Probability.coinKernel (p : ↑unitInterval) : MeasureTheory.ProbabilityMeasure Bool

The two-point kernel. coinKernel p is the law of one Bool-valued flip of a coin that comes up true with probability p.

Phrasing the example through this kernel — rather than through a Bernoulli random variable — keeps it independent of any particular parametrized-distribution API: all it needs is that the family is measurable in the bias.

Equations

• TauCeti.Probability.coinKernel p = ⟨ProbabilityTheory.bernoulliMeasure true false p, ⋯⟩

@[simp]

theorem TauCeti.Probability.coinKernel_toMeasure (p : ↑unitInterval) : ↑(coinKernel p) = ProbabilityTheory.bernoulliMeasure true false p

The measure underlying coinKernel p is Mathlib's Bernoulli measure on Bool.

theorem TauCeti.Probability.coinKernel_apply_true (p : ↑unitInterval) : ↑(coinKernel p) {true} = ↑(unitInterval.toNNReal p)

The bias is read back off the coin: coinKernel p gives mass p to {true}.

theorem TauCeti.Probability.measurable_coinKernel : Measurable coinKernel

The two-point kernel is measurable in the bias, so it can direct a mixture.

theorem TauCeti.Probability.conditionallyIIDWith_coinFlips (π : MeasureTheory.Measure ↑unitInterval) : ConditionallyIIDWith (iidMixtureLaw π coinKernel) (fun (n : ℕ) (ω : ↑unitInterval × (ℕ → Bool)) => ω.2 n) fun (ω : ↑unitInterval × (ℕ → Bool)) => coinKernel ω.1

The worked example. Draw a bias from π, then flip i.i.d. coins with that bias: the resulting Bool-valued sequence is conditionally i.i.d. with directing measure ω ↦ coinKernel ω.1.

This is the sharp conditional statement, not just the mixture identity: the generating construction puts the sequence and its directing measure on one space and pins their joint law.

theorem TauCeti.Probability.conditionallyIID_coinFlips (π : MeasureTheory.Measure ↑unitInterval) : ConditionallyIID (iidMixtureLaw π coinKernel) fun (n : ℕ) (ω : ↑unitInterval × (ℕ → Bool)) => ω.2 n

The coin-flip sequence is conditionally i.i.d. (existential form).

theorem TauCeti.Probability.exchangeable_coinFlips (π : MeasureTheory.Measure ↑unitInterval) : Exchangeable (iidMixtureLaw π coinKernel) fun (n : ℕ) (ω : ↑unitInterval × (ℕ → Bool)) => ω.2 n

The coin-flip sequence is exchangeable.

theorem TauCeti.Probability.contractable_coinFlips (π : MeasureTheory.Measure ↑unitInterval) : Contractable (iidMixtureLaw π coinKernel) fun (n : ℕ) (ω : ↑unitInterval × (ℕ → Bool)) => ω.2 n

The coin-flip sequence is contractable.

theorem TauCeti.Probability.exists_map_toNNReal_eq_dirac_of_iIndepFun_coinFlips (π : MeasureTheory.Measure ↑unitInterval) [MeasureTheory.IsProbabilityMeasure π] (h : ProbabilityTheory.iIndepFun (fun (n : ℕ) (ω : ↑unitInterval × (ℕ → Bool)) => ω.2 n) (iidMixtureLaw π coinKernel)) : ∃ (c : ENNReal), MeasureTheory.Measure.map (fun (p : ↑unitInterval) => ↑(unitInterval.toNNReal p)) π = MeasureTheory.Measure.dirac c

Independent flips force a deterministic bias. If the coordinates of the coin-flip sequence are independent, then the law of the bias — pushed forward along toNNReal — is a Dirac measure.

theorem TauCeti.Probability.not_iIndepFun_coinFlips {a b r : ↑unitInterval} (hab : a ≠ b) (hr₀ : r ≠ 0) (hr₁ : r ≠ 1) : ¬ProbabilityTheory.iIndepFun (fun (n : ℕ) (ω : ↑unitInterval × (ℕ → Bool)) => ω.2 n) (iidMixtureLaw (ProbabilityTheory.bernoulliMeasure a b r) coinKernel)

Exchangeable but not independent. With the bias itself drawn from a nondegenerate two-point law Ber(a, b, r) — two distinct biases a ≠ b, each of positive probability — the coin flips are exchangeable (exchangeable_coinFlips) yet dependent.

So ConditionallyIID is strictly wider than i.i.d., and the directing measure the construction supplies is genuinely random rather than an a.e. constant.