diff --git a/Cslib.lean b/Cslib.lean
index 5cfc781da5..19ac649da2 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -121,6 +121,7 @@ public import Cslib.Foundations.Control.Monad.IsMonadHom
 public import Cslib.Foundations.Control.Monad.IsMonadHom.List
 public import Cslib.Foundations.Data.BiTape
 public import Cslib.Foundations.Data.BitString
+public import Cslib.Foundations.Data.BitVec
 public import Cslib.Foundations.Data.DecidableEqZero
 public import Cslib.Foundations.Data.FinFun.Basic
 public import Cslib.Foundations.Data.FinFun.Update
@@ -253,6 +254,6 @@ public import Cslib.MachineLearning.PACLearning.Defs
 public import Cslib.MachineLearning.PACLearning.VCDimension
 public import Cslib.MachineLearning.PACLearning.VersionSpace
 public import Cslib.MachineLearning.PACLearning.VersionSpaceLattice
-public import Cslib.Probability.PMF
+public import Cslib.Probability.Measure
 public import Cslib.Probability.StatisticalDistance
 public import Cslib.Tactic.GrindAttrs
diff --git a/Cslib/Crypto/Primitives/PRG/Asymptotic.lean b/Cslib/Crypto/Primitives/PRG/Asymptotic.lean
index 7c9913b5b8..c64dd83b54 100644
--- a/Cslib/Crypto/Primitives/PRG/Asymptotic.lean
+++ b/Cslib/Crypto/Primitives/PRG/Asymptotic.lean
@@ -7,6 +7,7 @@ Authors: Samuel Schlesinger
 module
 
 public import Cslib.Crypto.Primitives.PRG.Basic
+public import Cslib.Foundations.Data.BitVec
 public import Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
 public import Mathlib.Data.FinEnum
 
@@ -41,6 +42,8 @@ abbrev Family (Seed Output : ℕ → Type*) := ∀ n, Generator (Seed n) (Output
 namespace Family
 
 variable {Seed Output : ℕ → Type*}
+variable [∀ n, MeasurableSpace (Seed n)]
+variable [∀ n, MeasurableSpace (Output n)]
 variable [∀ n, Fintype (Seed n)] [∀ n, Nonempty (Seed n)]
 variable [∀ n, Fintype (Output n)] [∀ n, Nonempty (Output n)]
 
@@ -80,6 +83,7 @@ theorem SecureWithError.secure {G : Family Seed Output}
 
 section RangeTests
 
+variable [∀ n, MeasurableSingletonClass (Seed n)] [∀ n, MeasurableSingletonClass (Output n)]
 variable [∀ n, DecidableEq (Output n)]
 
 /-- A non-negligible lower bound on the fraction of outputs outside the image rules out
diff --git a/Cslib/Crypto/Primitives/PRG/Basic.lean b/Cslib/Crypto/Primitives/PRG/Basic.lean
index d6dd70d168..a054b49d35 100644
--- a/Cslib/Crypto/Primitives/PRG/Basic.lean
+++ b/Cslib/Crypto/Primitives/PRG/Basic.lean
@@ -22,12 +22,16 @@ every smaller error bound. No injectivity assumption on the generator is needed.
 
 namespace Cslib.Crypto.PRG.Generator
 
+open MeasureTheory ProbabilityTheory Cslib.Probability.Measure
 open scoped NNReal
 
 variable {Seed Output : Type*}
 
+variable [MeasurableSpace Seed] [MeasurableSingletonClass Seed]
+variable [MeasurableSpace Output] [MeasurableSingletonClass Output]
 variable [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output]
 
+omit [MeasurableSingletonClass Seed] [MeasurableSingletonClass Output] in
 /-- Advantage is nonnegative. -/
 theorem advantage_nonneg (G : Generator Seed Output) (adversary : Adversary Output) :
     0 ≤ G.advantage adversary := abs_nonneg _
@@ -36,47 +40,54 @@ theorem advantage_nonneg (G : Generator Seed Output) (adversary : Adversary Outp
 theorem advantage_le_one (G : Generator Seed Output) (adversary : Adversary Output) :
     G.advantage adversary ≤ 1 := by
   have hreal := ENNReal.toReal_mono ENNReal.one_ne_top
-    (PMF.coe_le_one (G.realExperiment adversary) true)
+    (prob_le_one (μ := G.realExperiment adversary) (s := {true}))
   have hideal := ENNReal.toReal_mono ENNReal.one_ne_top
-    (PMF.coe_le_one (idealExperiment adversary) true)
+    (prob_le_one (μ := idealExperiment adversary) (s := {true}))
   simp only [ENNReal.toReal_one] at hreal hideal
   apply abs_sub_le_iff.mpr
   constructor
-  · linarith [@ENNReal.toReal_nonneg (idealExperiment adversary true)]
-  · linarith [@ENNReal.toReal_nonneg (G.realExperiment adversary true)]
+  · linarith [@ENNReal.toReal_nonneg (idealExperiment adversary {true})]
+  · linarith [@ENNReal.toReal_nonneg (G.realExperiment adversary {true})]
 
 /-- Error one imposes no restriction on a generator. -/
 theorem secure_one (G : Generator Seed Output) (Admissible : Adversary Output → Prop) :
     G.Secure Admissible 1 := fun adversary _ => G.advantage_le_one adversary
 
+omit [MeasurableSingletonClass Output] in
 /-- A test whose output distribution is independent of its input has zero advantage. -/
 @[simp]
-theorem advantage_const (G : Generator Seed Output) (p : PMF Bool) :
+theorem advantage_const (G : Generator Seed Output) (p : ProbabilityMeasure Bool) :
     G.advantage (fun _ => p) = 0 := by
-  simp [advantage, realExperiment, idealExperiment, PMF.bind_const]
+  simp [advantage, realExperiment, idealExperiment, Measure.bind_const]
 
+omit [MeasurableSingletonClass Seed] [MeasurableSingletonClass Output] in
 /-- A generator with exactly uniform output is secure with zero error against any tests. -/
 theorem secure_zero_of_outputDist_eq (G : Generator Seed Output)
-    (hG : G.outputDist = PMF.uniformOfFintype Output)
+    (hG : G.outputDist = uniformOfFintype Output)
     (Admissible : Adversary Output → Prop) : G.Secure Admissible 0 := by
   intro adversary _
   simp [advantage, realExperiment, idealExperiment, hG]
 
 /-- Zero-error security against arbitrary tests is equivalent to exactly uniform output. -/
 theorem secure_zero_iff_outputDist_eq_uniform (G : Generator Seed Output) :
-    G.Secure (fun _ => True) 0 ↔ G.outputDist = PMF.uniformOfFintype Output := by
+    G.Secure (fun _ => True) 0 ↔ G.outputDist = uniformOfFintype Output := by
   classical
   refine ⟨fun h => ?_, fun h => G.secure_zero_of_outputDist_eq h _⟩
-  ext output
-  apply (ENNReal.toReal_eq_toReal_iff' (PMF.apply_ne_top _ _) (PMF.apply_ne_top _ _)).mp
-  simpa [advantage, realExperiment, idealExperiment, PMF.bind_apply, PMF.pure_apply,
-    sub_eq_zero] using h (fun x => PMF.pure (decide (x = output))) trivial
-
+  apply Measure.ext_of_singleton
+  intro output
+  apply (ENNReal.toReal_eq_toReal_iff' (measure_ne_top _ _) (measure_ne_top _ _)).mp
+  simpa [advantage, realExperiment, idealExperiment, Adversary.ofPure,
+    Measure.bind_dirac_eq_map _ (measurable_of_countable _),
+    Measure.map_apply (measurable_of_countable _), Set.preimage, sub_eq_zero] using
+    h (Adversary.ofPure (fun x => decide (x = output))) trivial
+
+omit [MeasurableSingletonClass Seed] [MeasurableSingletonClass Output] in
 /-- Enlarging the allowed advantage preserves security. -/
 theorem Secure.mono {G : Generator Seed Output} {Admissible : Adversary Output → Prop} :
     Monotone (G.Secure Admissible) :=
   fun _ _ hεδ h adversary ha => (h adversary ha).trans (by exact_mod_cast hεδ)
 
+omit [MeasurableSingletonClass Seed] [MeasurableSingletonClass Output] in
 /-- Security against a larger class of adversaries implies security against a smaller class. -/
 theorem Secure.of_admissible {G : Generator Seed Output}
     {Admissible Restricted : Adversary Output → Prop} {ε : ℝ≥0}
@@ -95,37 +106,50 @@ def rangeTest (G : Generator Seed Output) (output : Output) : Bool :=
 omit [Nonempty Seed] [Fintype Output] [Nonempty Output] in
 /-- The deterministic adversary that tests membership in the generator's range. -/
 noncomputable def rangeAdversary (G : Generator Seed Output) : Adversary Output :=
-  fun output => PMF.pure (G.rangeTest output)
+  Adversary.ofPure G.rangeTest
 
 omit [Fintype Output] [Nonempty Output] in
 /-- The range test always accepts a generated output. -/
 @[simp]
 theorem realExperiment_rangeAdversary (G : Generator Seed Output) :
-    G.realExperiment G.rangeAdversary = PMF.pure true := by
-  simp [realExperiment, outputDist, PMF.bind_map, rangeAdversary, rangeTest, Function.comp_def,
-    PMF.bind_const]
-
-omit [Nonempty Seed] in
+    G.realExperiment G.rangeAdversary = Measure.dirac true := by
+  have htest : Measurable G.rangeTest := by
+    change Measurable (fun output => decide (∃ seed, G seed = output))
+    simpa using
+      (measurable_const.ite (Set.finite_range G).measurableSet measurable_const :
+        Measurable (fun output => if output ∈ Set.range G then true else false))
+  simp only [realExperiment, outputDist, rangeAdversary, Adversary.ofPure,
+    Measure.coe_toProbabilityMeasure]
+  rw [Measure.bind_dirac_eq_map _ htest, Measure.map_map htest (measurable_of_countable G)]
+  have h : (G.rangeTest ∘ G) = fun _ => true := by
+    funext seed
+    simp [rangeTest]
+  simp [h]
+
+omit [Nonempty Seed] [MeasurableSpace Seed] [MeasurableSingletonClass Seed] in
 /-- The range test's acceptance probability under uniform sampling is the fraction
 of outputs in the range. -/
 theorem idealExperiment_rangeAdversary (G : Generator Seed Output) :
-    (idealExperiment G.rangeAdversary true).toReal =
+    (idealExperiment G.rangeAdversary {true}).toReal =
       Nat.card (Set.range G) / (Fintype.card Output : ℝ) := by
-  simp only [idealExperiment, rangeAdversary, rangeTest, PMF.bind_apply, PMF.pure_apply,
-    PMF.uniformOfFintype_apply, tsum_fintype]
-  simp only [mul_ite, mul_one, mul_zero, eq_comm (a := true), decide_eq_true_eq]
-  rw [← Finset.sum_filter]
-  simp [Nat.card_eq_fintype_card, Fintype.card_subtype, div_eq_mul_inv]
+  classical
+  simp only [idealExperiment, rangeAdversary, Adversary.ofPure,
+    Measure.coe_toProbabilityMeasure]
+  rw [Measure.bind_dirac_eq_map _ (measurable_of_countable _),
+    Measure.map_apply (measurable_of_countable _) (measurableSet_singleton true)]
+  simp [uniformOn_univ, Measure.count_apply_finite _ (Set.toFinite _),
+    rangeTest, Set.preimage,
+    Fintype.card_subtype, Nat.card_eq_fintype_card, ENNReal.toReal_div]
 
 /-- The exact advantage of the range-membership adversary. -/
 theorem advantage_rangeAdversary (G : Generator Seed Output) :
     G.advantage G.rangeAdversary =
       1 - Nat.card (Set.range G) / (Fintype.card Output : ℝ) := by
-  have hprob : (idealExperiment G.rangeAdversary true).toReal ≤ 1 :=
-    (ENNReal.toReal_le_toReal (PMF.apply_ne_top _ _) ENNReal.one_ne_top).mpr
-      (PMF.coe_le_one _ _)
+  have hprob : (idealExperiment G.rangeAdversary {true}).toReal ≤ 1 := by
+    exact_mod_cast ENNReal.toReal_mono ENNReal.one_ne_top
+      (prob_le_one (μ := idealExperiment G.rangeAdversary) (s := {true}))
   rw [advantage, realExperiment_rangeAdversary]
-  simp only [PMF.pure_apply, ↓reduceIte, ENNReal.toReal_one]
+  simp only [Measure.dirac_apply_of_mem (Set.mem_singleton true), ENNReal.toReal_one]
   rw [abs_of_nonneg (sub_nonneg.mpr hprob), idealExperiment_rangeAdversary]
 
 /-- Every generator has an unbounded distinguisher with advantage at least
diff --git a/Cslib/Crypto/Primitives/PRG/Defs.lean b/Cslib/Crypto/Primitives/PRG/Defs.lean
index 24e1988b8a..91471193c3 100644
--- a/Cslib/Crypto/Primitives/PRG/Defs.lean
+++ b/Cslib/Crypto/Primitives/PRG/Defs.lean
@@ -6,9 +6,7 @@ Authors: Samuel Schlesinger
 
 module
 
-public import Cslib.Init
-public import Mathlib.Probability.Distributions.Uniform
-public import Mathlib.Probability.ProbabilityMassFunction.Constructions
+public import Cslib.Probability.Measure
 
 /-!
 # Pseudorandom generators: games and concrete security
@@ -31,6 +29,7 @@ In particular, a generator need not expand, and an expanding generator need not
 
 namespace Cslib.Crypto.PRG
 
+open MeasureTheory ProbabilityTheory Cslib.Probability.Measure
 open scoped NNReal
 
 /-- A deterministic generator with seed space `Seed` and output space `Output`.
@@ -41,7 +40,11 @@ structure Generator (Seed Output : Type*) where
   toFun : Seed → Output
 
 /-- A randomized statistical test on the output space. -/
-abbrev Adversary (Output : Type*) := Output → PMF Bool
+abbrev Adversary (Output : Type*) := Output → ProbabilityMeasure Bool
+
+/-- A deterministic Boolean test, viewed as a randomized adversary. -/
+noncomputable def Adversary.ofPure {Output : Type*} (f : Output → Bool) : Adversary Output :=
+  fun output => (Measure.dirac (f output)).toProbabilityMeasure
 
 namespace Generator
 
@@ -58,25 +61,40 @@ theorem coe_mk (f : Seed → Output) : ⇑(Generator.mk f) = f := rfl
 def IsExpanding [Fintype Seed] [Fintype Output] (_G : Generator Seed Output) : Prop :=
   Fintype.card Seed < Fintype.card Output
 
+variable [MeasurableSpace Seed] [MeasurableSingletonClass Seed]
+variable [MeasurableSpace Output] [MeasurableSingletonClass Output]
 variable [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output]
 
 /-- The distribution obtained by applying the generator to a uniform seed. -/
-noncomputable def outputDist (G : Generator Seed Output) : PMF Output :=
-  (PMF.uniformOfFintype Seed).map G
+noncomputable def outputDist (G : Generator Seed Output) : Measure Output :=
+  (uniformOfFintype Seed : Measure Seed).map G
+
+instance (G : Generator Seed Output) : IsProbabilityMeasure G.outputDist :=
+  (Measure.isProbabilityMeasure_map_iff (measurable_of_countable G).aemeasurable).2 inferInstance
 
 /-- Experiment 0 of Attack Game 3.1: give the adversary a generated output. -/
 noncomputable def realExperiment (G : Generator Seed Output)
-    (adversary : Adversary Output) : PMF Bool :=
-  G.outputDist.bind adversary
+    (adversary : Adversary Output) : Measure Bool :=
+  G.outputDist.bind (fun output => (adversary output : Measure Bool))
+
+omit [Fintype Output] in
+instance [Countable Output] (G : Generator Seed Output) (adversary : Adversary Output) :
+    IsProbabilityMeasure (G.realExperiment adversary) :=
+  isProbabilityMeasure_bind (measurable_of_countable _).aemeasurable
+    (Filter.Eventually.of_forall fun _ => inferInstance)
 
 /-- Experiment 1 of Attack Game 3.1: give the adversary a uniform output. -/
-noncomputable def idealExperiment (adversary : Adversary Output) : PMF Bool :=
-  (PMF.uniformOfFintype Output).bind adversary
+noncomputable def idealExperiment (adversary : Adversary Output) : Measure Bool :=
+  (uniformOfFintype Output : Measure Output).bind (fun output => (adversary output : Measure Bool))
+
+instance (adversary : Adversary Output) : IsProbabilityMeasure (idealExperiment adversary) :=
+  isProbabilityMeasure_bind (measurable_of_countable _).aemeasurable
+    (Filter.Eventually.of_forall fun _ => inferInstance)
 
 /-- The absolute difference of the probabilities of outputting `true` in the two
 experiments, as in Attack Game 3.1 of [BonehShoup2023]. -/
 noncomputable def advantage (G : Generator Seed Output) (adversary : Adversary Output) : ℝ :=
-  |(G.realExperiment adversary true).toReal - (idealExperiment adversary true).toReal|
+  |(G.realExperiment adversary {true}).toReal - (idealExperiment adversary {true}).toReal|
 
 /-- Concrete security against admissible adversaries. The predicate is supplied by the
 caller, for example to restrict tests to a chosen computational resource bound.
diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/Basic.lean b/Cslib/Crypto/Protocols/PerfectSecrecy/Basic.lean
index 25c96a77bc..ed69ad0bd3 100644
--- a/Cslib/Crypto/Protocols/PerfectSecrecy/Basic.lean
+++ b/Cslib/Crypto/Protocols/PerfectSecrecy/Basic.lean
@@ -7,7 +7,6 @@ Authors: Samuel Schlesinger
 module
 
 public import Cslib.Crypto.Protocols.PerfectSecrecy.Defs
-import Mathlib.Probability.Distributions.Uniform
 
 /-!
 # Perfect Secrecy
@@ -35,98 +34,104 @@ Shannon's key-space bound.
 
 namespace Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme
 
-open Cslib.Probability.PMF
+open MeasureTheory ProbabilityTheory Cslib.Probability.Measure
 
-universe u
-variable {M K C : Type u}
+variable {M K C : Type*} [MeasurableSpace M] [MeasurableSpace K] [MeasurableSpace C]
 
-/-- The joint distribution at `(m, c)` equals `msgDist m * ciphertextDist m c`. -/
-theorem jointDist_eq (scheme : EncScheme M K C) (msgDist : PMF M)
-    (m : M) (c : C) :
-    scheme.jointDist msgDist (m, c) = msgDist m * scheme.ciphertextDist m c :=
-  bind_pair_apply msgDist scheme.ciphertextDist m c
+/-- The joint measure on a rectangle is obtained by integrating the encryption channel. -/
+theorem jointDist_apply_prod (scheme : EncScheme M K C) (msgDist : Measure M) [SFinite msgDist]
+    {messages : Set M} {ciphertexts : Set C}
+    (hm : MeasurableSet messages) (hc : MeasurableSet ciphertexts) :
+    scheme.jointDist msgDist (messages ×ˢ ciphertexts) =
+      ∫⁻ m in messages, scheme.ciphertextDist m ciphertexts ∂msgDist :=
+  Measure.compProd_apply_prod hm hc
 
-/-- Summing the joint distribution over messages gives the marginal ciphertext
-distribution. -/
-theorem jointDist_tsum_fst (scheme : EncScheme M K C) (msgDist : PMF M) (c : C) :
-    ∑' m, scheme.jointDist msgDist (m, c) = scheme.marginalCiphertextDist msgDist c :=
-  bind_pair_tsum_fst msgDist scheme.ciphertextDist c
+/-- The second marginal of the joint distribution is the ciphertext distribution. -/
+theorem jointDist_snd (scheme : EncScheme M K C) (msgDist : Measure M) [SFinite msgDist] :
+    (scheme.jointDist msgDist).snd = scheme.marginalCiphertextDist msgDist :=
+  Measure.snd_compProd _ _
 
-/-- Perfect secrecy is equivalent to message-ciphertext independence.
-The two formulations are related by multiplying/dividing by `marginal(c)`. -/
+/-- Perfect secrecy is equivalent to independence on all measurable events. -/
 theorem perfectlySecret_iff_indep (scheme : EncScheme M K C) :
     scheme.PerfectlySecret ↔
-    ∀ (msgDist : PMF M) (m : M) (c : C),
-      scheme.jointDist msgDist (m, c) =
-        msgDist m * scheme.marginalCiphertextDist msgDist c := by
-  refine ⟨fun h msgDist m c => ?_, fun h msgDist c hc => ?_⟩
-  · by_cases hc : (scheme.marginalCiphertextDist msgDist) c = 0
-    · have := ENNReal.tsum_eq_zero.mp
-        ((jointDist_tsum_fst scheme msgDist c).trans hc) m
-      rw [this, hc, mul_zero]
-    · have hne_top := PMF.apply_ne_top (scheme.marginalCiphertextDist msgDist) c
-      have := DFunLike.congr_fun (h msgDist c ((PMF.mem_support_iff _ _).mpr hc)) m
-      simp only [posteriorMsgDist_apply] at this
-      rw [← this, ENNReal.div_mul_cancel hc hne_top]
-  · ext m
-    simp only [posteriorMsgDist_apply]
-    rw [h msgDist m c, ENNReal.mul_div_cancel_right
-      ((PMF.mem_support_iff _ _).mp hc) (PMF.apply_ne_top _ c)]
-
-/-- A scheme is perfectly secret iff the ciphertext distribution is
-independent of the plaintext ([KatzLindell2020], Lemma 2.5). -/
-theorem perfectlySecret_iff_ciphertextIndist (scheme : EncScheme M K C) :
-    scheme.PerfectlySecret ↔ scheme.CiphertextIndist := by
+      ∀ (msgDist : Measure M) [IsProbabilityMeasure msgDist]
+        (messages : Set M) (ciphertexts : Set C),
+        MeasurableSet messages → MeasurableSet ciphertexts →
+        scheme.jointDist msgDist (messages ×ˢ ciphertexts) =
+          msgDist messages * scheme.marginalCiphertextDist msgDist ciphertexts := by
+  constructor
+  · intro h μ _ messages ciphertexts _ _
+    rw [h μ, Measure.prod_prod]
+  · intro h μ _
+    exact Measure.ext_prod fun hm hc => (h μ _ _ hm hc).trans (Measure.prod_prod _ _).symm
+
+/-- A scheme is perfectly secret iff its ciphertext law is independent of the message
+([KatzLindell2020], Lemma 2.5). Only the message singletons need to be measurable. -/
+theorem perfectlySecret_iff_ciphertextIndist [MeasurableSingletonClass M]
+    (scheme : EncScheme M K C) : scheme.PerfectlySecret ↔ scheme.CiphertextIndist := by
   classical
-  refine ⟨fun h => ?_, fun h msgDist c hc =>
-    posteriorDist_eq_prior_of_outputIndist msgDist scheme.ciphertextDist h c hc⟩
-  rw [perfectlySecret_iff_indep] at h
-  intro m₀ m₁; ext c
-  have hs : ({m₀, m₁} : Finset M).Nonempty := ⟨m₀, Finset.mem_insert_self ..⟩
-  set μ := PMF.uniformOfFinset _ hs
-  suffices key : ∀ m ∈ ({m₀, m₁} : Finset M),
-      scheme.ciphertextDist m c = scheme.marginalCiphertextDist μ c by
-    exact (key m₀ (by simp)).trans (key m₁ (by simp)).symm
-  intro m hm
-  have hne := (PMF.mem_support_uniformOfFinset_iff hs m).mpr hm
-  have hne_top := PMF.apply_ne_top μ m
-  exact (ENNReal.mul_right_inj hne hne_top).mp (by rw [← jointDist_eq]; exact h μ m c)
+  refine ⟨fun h m₀ m₁ => ?_, fun h μ _ => compProd_eq_prod_of_outputIndist μ _ h⟩
+  let messages : Finset M := {m₀, m₁}
+  let μ := uniformOn (messages : Set M)
+  have : IsProbabilityMeasure μ :=
+    isProbabilityMeasure_uniformOn messages.finite_toSet (by simp [messages])
+  have key : ∀ m ∈ messages, scheme.ciphertextDist m = scheme.marginalCiphertextDist μ := by
+    intro m hm
+    apply Measure.ext
+    intro ciphertexts hc
+    have he := (perfectlySecret_iff_indep scheme).mp h μ {m} ciphertexts
+      (measurableSet_singleton m) hc
+    rw [jointDist_apply_prod _ _ (measurableSet_singleton m) hc, lintegral_singleton,
+      mul_comm] at he
+    have hmass : μ {m} ≠ 0 := by
+      change uniformOn (messages : Set M) {m} ≠ 0
+      intro hz
+      have he := (uniformOn_eq_zero_iff messages.finite_toSet).mp hz
+      have hm' : m ∈ (messages : Set M) ∩ {m} := ⟨hm, rfl⟩
+      simp only [he, Set.mem_empty_iff_false] at hm'
+    exact (ENNReal.mul_right_inj hmass (measure_ne_top μ {m})).mp he
+  exact (key m₀ (by simp [messages])).trans (key m₁ (by simp [messages])).symm
 
 /-- Ciphertext indistinguishability implies message-ciphertext independence. -/
 theorem indep_of_ciphertextIndist (scheme : EncScheme M K C)
-    (h : scheme.CiphertextIndist) (msgDist : PMF M) (m : M) (c : C) :
-    scheme.jointDist msgDist (m, c) =
-      msgDist m * scheme.marginalCiphertextDist msgDist c :=
-  (perfectlySecret_iff_indep scheme).mp
-    ((perfectlySecret_iff_ciphertextIndist scheme).mpr h) msgDist m c
-
-/-- If each message maps to a key that encrypts it to a common ciphertext,
-then the key assignment is injective (by correctness of decryption). -/
-private lemma encrypt_key_injective (scheme : EncScheme M K C)
-    (f : M → K) (c₀ : C)
-    (hf_mem : ∀ m, f m ∈ scheme.gen.support)
-    (hf_enc : ∀ m, c₀ ∈ (scheme.enc (f m) m).support) :
-    Function.Injective f :=
-  fun m₁ m₂ heq =>
-    (scheme.correct _ (hf_mem m₁) m₁ c₀ (hf_enc m₁)).symm.trans
-      (heq ▸ scheme.correct _ (hf_mem m₂) m₂ c₀ (hf_enc m₂))
-
-/-- Perfect secrecy requires `|K| ≥ |M|` — Shannon's theorem
+    (h : scheme.CiphertextIndist) (msgDist : Measure M) [IsProbabilityMeasure msgDist] :
+    scheme.jointDist msgDist = msgDist.prod (scheme.marginalCiphertextDist msgDist) :=
+  compProd_eq_prod_of_outputIndist msgDist _ h
+
+/-- Under perfect secrecy, Mathlib's posterior equals the prior almost surely. -/
+theorem posteriorMsgDist_eq_prior [StandardBorelSpace M] [Nonempty M]
+    (scheme : EncScheme M K C) (h : scheme.PerfectlySecret)
+    (msgDist : Measure M) [IsProbabilityMeasure msgDist] :
+    scheme.posteriorMsgDist msgDist =ᵐ[scheme.marginalCiphertextDist msgDist]
+      fun _ => msgDist :=
+  posterior_eq_prior_of_compProd_eq_prod msgDist _ (h msgDist)
+
+/-- Perfect secrecy requires `|K| ≥ |M|` — Shannon's theorem.
+Ciphertexts may have a continuous distribution; correctness is used almost surely
 ([KatzLindell2020], Theorem 2.12). -/
-theorem perfectlySecret_keySpace_ge [Finite K]
+theorem perfectlySecret_keySpace_ge [Finite K] [MeasurableSingletonClass M]
     (scheme : EncScheme M K C) (h : scheme.PerfectlySecret) :
     Nat.card M ≤ Nat.card K := by
   classical
-  have hci := (perfectlySecret_iff_ciphertextIndist scheme).mp h
-  by_cases hM : IsEmpty M; · simp
-  obtain ⟨m₀⟩ := not_isEmpty_iff.mp hM
-  obtain ⟨c₀, hc₀⟩ := (scheme.ciphertextDist m₀).support_nonempty
-  have key_exists : ∀ m, ∃ k ∈ scheme.gen.support, c₀ ∈ (scheme.enc k m).support := by
-    intro m
-    exact (PMF.mem_support_bind_iff _ _ _).mp
-      (show c₀ ∈ (scheme.ciphertextDist m).support by rw [hci m m₀]; exact hc₀)
-  choose f hf_mem hf_enc using key_exists
-  exact Nat.card_le_card_of_injective f
-    (encrypt_key_injective scheme f c₀ hf_mem hf_enc)
+  cases finite_or_infinite M with
+  | inr hM => simp [Nat.card_eq_zero_of_infinite]
+  | inl hM =>
+    have hci := (perfectlySecret_iff_ciphertextIndist scheme).mp h
+    by_cases hM : IsEmpty M
+    · simp
+    obtain ⟨m₀⟩ := not_isEmpty_iff.mp hM
+    have key_exists (m : M) : ∀ᵐ c ∂scheme.ciphertextDist m₀, ∃ k, scheme.dec k c = m := by
+      rw [← hci m m₀, ciphertextDist_eq_comp]
+      apply Measure.ae_comp_of_ae_ae
+      · have hk (k : K) : Measurable (scheme.dec k) :=
+          scheme.dec_measurable.comp measurable_prodMk_left
+        simpa only [Set.ofPred_exists, Set.preimage, Set.mem_singleton_iff] using
+          MeasurableSet.iUnion (fun k => hk k (measurableSet_singleton m))
+      · filter_upwards [scheme.correct] with k hk
+        exact (hk m).mono fun c hc => ⟨k, hc⟩
+    obtain ⟨c, hc⟩ := (ae_all_iff.mpr key_exists).exists
+    choose f hf using hc
+    exact Nat.card_le_card_of_injective f fun m₁ m₂ heq =>
+      (hf m₁).symm.trans (heq ▸ hf m₂)
 
 end Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme
diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/Defs.lean b/Cslib/Crypto/Protocols/PerfectSecrecy/Defs.lean
index 4c1d5dcfba..2b73f64e87 100644
--- a/Cslib/Crypto/Protocols/PerfectSecrecy/Defs.lean
+++ b/Cslib/Crypto/Protocols/PerfectSecrecy/Defs.lean
@@ -7,8 +7,6 @@ Authors: Samuel Schlesinger
 module
 
 public import Cslib.Crypto.Protocols.PerfectSecrecy.Encryption
-public import Cslib.Probability.PMF
-public import Mathlib.Probability.ProbabilityMassFunction.Constructions
 
 /-!
 # Perfect Secrecy: Definitions
@@ -24,7 +22,7 @@ Core definitions for perfect secrecy following [KatzLindell2020], Chapter 2.
 - `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.marginalCiphertextDist`:
   marginal ciphertext distribution given a message prior
 - `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.posteriorMsgDist`:
-  posterior message distribution `Pr[M | C = c]` as a `PMF`
+  posterior message distribution `Pr[M | C = c]` as a regular conditional kernel
 - `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.PerfectlySecret`:
   perfect secrecy ([KatzLindell2020], Definition 2.3)
 - `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.CiphertextIndist`:
@@ -35,48 +33,56 @@ Core definitions for perfect secrecy following [KatzLindell2020], Chapter 2.
 
 namespace Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme
 
-open Cslib.Probability.PMF
+open MeasureTheory ProbabilityTheory
 
-universe u
-variable {M K C : Type u}
+variable {M K C : Type*} [MeasurableSpace M] [MeasurableSpace K] [MeasurableSpace C]
 
-/-- The distribution of `Enc_K(m)` when `K ← Gen`. -/
-noncomputable def ciphertextDist (scheme : EncScheme M K C) (m : M) : PMF C := do
-  scheme.enc (← scheme.gen) m
+/-- The encryption channel, after sampling the key independently of the message. -/
+noncomputable def ciphertextKernel (scheme : EncScheme M K C) : Kernel M C :=
+  scheme.enc ∘ₖ (Kernel.const M scheme.gen ×ₖ Kernel.id)
+
+instance (scheme : EncScheme M K C) : IsMarkovKernel scheme.ciphertextKernel := by
+  unfold ciphertextKernel
+  infer_instance
 
-/-- Joint distribution of `(M, C)` given a message prior. -/
-noncomputable def jointDist (scheme : EncScheme M K C) (msgDist : PMF M) : PMF (M × C) := do
-  let m ← msgDist
-  return (m, ← scheme.ciphertextDist m)
+/-- The distribution of `Enc_K(m)` when `K ← Gen`. -/
+noncomputable def ciphertextDist (scheme : EncScheme M K C) (m : M) : Measure C :=
+  scheme.ciphertextKernel m
+
+/-- The encryption channel at a message integrates encryption over the generated key. -/
+theorem ciphertextDist_eq_comp (scheme : EncScheme M K C) (m : M) :
+    scheme.ciphertextDist m =
+      scheme.enc.comap (fun key => (key, m)) measurable_prodMk_right ∘ₘ scheme.gen := by
+  simp only [ciphertextDist, ciphertextKernel, Kernel.comp_apply, Kernel.prod_apply,
+    Kernel.const_apply, Kernel.id_apply, Measure.prod_dirac, Kernel.coe_comap]
+  exact Measure.bind_map measurable_prodMk_right.aemeasurable scheme.enc.aemeasurable
+
+instance (scheme : EncScheme M K C) (m : M) :
+    IsProbabilityMeasure (scheme.ciphertextDist m) := by
+  unfold ciphertextDist
+  infer_instance
+
+/-- Joint distribution of messages and ciphertexts given a message prior. -/
+noncomputable abbrev jointDist (scheme : EncScheme M K C) (msgDist : Measure M) : Measure (M × C) :=
+  msgDist ⊗ₘ scheme.ciphertextKernel
 
 /-- Marginal ciphertext distribution given a message prior. -/
-noncomputable def marginalCiphertextDist (scheme : EncScheme M K C)
-    (msgDist : PMF M) : PMF C := do
-  scheme.ciphertextDist (← msgDist)
-
-/-- The posterior message distribution `Pr[M | C = c]` as a probability
-distribution, given a message prior and a ciphertext in the support of
-the marginal distribution. -/
-noncomputable def posteriorMsgDist (scheme : EncScheme M K C)
-    (msgDist : PMF M) (c : C)
-    (hc : c ∈ (scheme.marginalCiphertextDist msgDist).support) : PMF M :=
-  posteriorDist msgDist scheme.ciphertextDist c hc
-
-@[simp]
-theorem posteriorMsgDist_apply (scheme : EncScheme M K C)
-    (msgDist : PMF M) (c : C)
-    (hc : c ∈ (scheme.marginalCiphertextDist msgDist).support) (m : M) :
-    scheme.posteriorMsgDist msgDist c hc m =
-      scheme.jointDist msgDist (m, c) / scheme.marginalCiphertextDist msgDist c :=
-  posteriorDist_apply msgDist scheme.ciphertextDist c hc m
-
-/-- An encryption scheme is perfectly secret if the posterior message
-distribution equals the prior for every ciphertext with positive probability
+noncomputable abbrev marginalCiphertextDist (scheme : EncScheme M K C)
+    (msgDist : Measure M) : Measure C :=
+  scheme.ciphertextKernel ∘ₘ msgDist
+
+/-- Mathlib's regular conditional distribution on messages given the ciphertext. -/
+noncomputable abbrev posteriorMsgDist [StandardBorelSpace M] [Nonempty M]
+    (scheme : EncScheme M K C) (msgDist : Measure M) [IsProbabilityMeasure msgDist] :
+    Kernel C M :=
+  posterior scheme.ciphertextKernel msgDist
+
+/-- Messages and ciphertexts are independent for every probability prior.
+This formulation of perfect secrecy also applies to continuous distributions
 ([KatzLindell2020], Definition 2.3). -/
 def PerfectlySecret (scheme : EncScheme M K C) : Prop :=
-  ∀ (msgDist : PMF M) (c : C)
-    (hc : c ∈ (scheme.marginalCiphertextDist msgDist).support),
-    scheme.posteriorMsgDist msgDist c hc = msgDist
+  ∀ (msgDist : Measure M) [IsProbabilityMeasure msgDist],
+    scheme.jointDist msgDist = msgDist.prod (scheme.marginalCiphertextDist msgDist)
 
 /-- Ciphertext indistinguishability: the ciphertext distribution is the same
 for all messages ([KatzLindell2020], Lemma 2.5). -/
diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/Encryption.lean b/Cslib/Crypto/Protocols/PerfectSecrecy/Encryption.lean
index a6896bcdf5..4d915e6cbf 100644
--- a/Cslib/Crypto/Protocols/PerfectSecrecy/Encryption.lean
+++ b/Cslib/Crypto/Protocols/PerfectSecrecy/Encryption.lean
@@ -6,8 +6,7 @@ Authors: Samuel Schlesinger
 
 module
 
-public import Cslib.Init
-public import Mathlib.Probability.ProbabilityMassFunction.Monad
+public import Cslib.Probability.Measure
 
 /-!
 # Private-Key Encryption Schemes (Information-Theoretic)
@@ -29,33 +28,52 @@ constraints.
 
 @[expose] public section
 
+open MeasureTheory ProbabilityTheory
+
 namespace Cslib.Crypto.Protocols.PerfectSecrecy
 
 /--
 A private-key encryption scheme over message space `M`, key space `K`,
 and ciphertext space `C` ([KatzLindell2020], Definition 2.1).
 -/
-structure EncScheme (Message Key Ciphertext : Type*) where
+structure EncScheme (Message Key Ciphertext : Type*)
+    [MeasurableSpace Message] [MeasurableSpace Key] [MeasurableSpace Ciphertext] where
   /-- Probabilistic key generation. -/
-  gen : PMF Key
-  /-- (Possibly randomized) encryption. -/
-  enc (key : Key) (message : Message) : PMF Ciphertext
+  gen : Measure Key
+  /-- Key generation has total mass one. -/
+  gen_isProbabilityMeasure : IsProbabilityMeasure gen
+  /-- Jointly measurable, possibly randomized encryption. -/
+  enc : Kernel (Key × Message) Ciphertext
+  /-- Encryption has total mass one for every key and message. -/
+  enc_isMarkovKernel : IsMarkovKernel enc
   /-- Deterministic decryption. -/
   dec (key : Key) (ciphertext : Ciphertext) : Message
-  /-- Decryption inverts encryption for all keys in the support of `gen`. -/
-  correct : ∀ key, key ∈ gen.support → ∀ message ciphertext,
-    ciphertext ∈ (enc key message).support → dec key ciphertext = message
+  /-- Decryption is jointly measurable. -/
+  dec_measurable : Measurable (Function.uncurry dec)
+  /-- Almost every generated key decrypts correctly for every message, almost surely over
+  encryption randomness. The exceptional set of keys is independent of the message. -/
+  correct : ∀ᵐ key ∂gen, ∀ message, ∀ᵐ ciphertext ∂enc (key, message),
+    dec key ciphertext = message
+
+attribute [instance] EncScheme.gen_isProbabilityMeasure EncScheme.enc_isMarkovKernel
 
-/-- Build an encryption scheme from deterministic pure encryption/decryption
+/-- Build an encryption scheme from measurable deterministic encryption/decryption
 where decryption is a left inverse of encryption for every key. -/
-noncomputable def EncScheme.ofPure.{u} {Message Key Ciphertext : Type u} (gen : PMF Key)
+noncomputable def EncScheme.ofPure {Message Key Ciphertext : Type*}
+    [MeasurableSpace Message] [MeasurableSpace Key] [MeasurableSpace Ciphertext]
+    [MeasurableSingletonClass Message] (gen : Measure Key) [IsProbabilityMeasure gen]
     (enc : Key → Message → Ciphertext) (dec : Key → Ciphertext → Message)
+    (henc : Measurable (Function.uncurry enc)) (hdec : Measurable (Function.uncurry dec))
     (h : ∀ key, Function.LeftInverse (dec key) (enc key)) :
     EncScheme Message Key Ciphertext where
   gen := gen
-  enc key message := PMF.pure (enc key message)
+  gen_isProbabilityMeasure := inferInstance
+  enc := Kernel.deterministic (Function.uncurry enc) henc
+  enc_isMarkovKernel := inferInstance
   dec := dec
-  correct key _ message _ hc := by
-    rw [PMF.mem_support_pure_iff] at hc; subst hc; exact h key message
+  dec_measurable := hdec
+  correct := Filter.Eventually.of_forall fun key message => by
+    exact (ae_dirac_iff ((hdec.comp measurable_prodMk_left)
+      (measurableSet_singleton message))).2 (h key message)
 
 end Cslib.Crypto.Protocols.PerfectSecrecy
diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/OneTimePad.lean b/Cslib/Crypto/Protocols/PerfectSecrecy/OneTimePad.lean
index 1df26b1afc..9127353326 100644
--- a/Cslib/Crypto/Protocols/PerfectSecrecy/OneTimePad.lean
+++ b/Cslib/Crypto/Protocols/PerfectSecrecy/OneTimePad.lean
@@ -7,8 +7,8 @@ Authors: Samuel Schlesinger
 module
 
 public import Cslib.Crypto.Protocols.PerfectSecrecy.Basic
+public import Cslib.Foundations.Data.BitVec
 public import Mathlib.Data.FinEnum
-import Cslib.Probability.PMF
 import Mathlib.Data.LawfulXor.Equiv
 
 /-!
@@ -35,24 +35,26 @@ The one-time pad (Vernam cipher) over `BitVec l`
 
 namespace Cslib.Crypto.Protocols.PerfectSecrecy
 
-open Cslib.Probability.PMF
+open MeasureTheory ProbabilityTheory Cslib.Probability.Measure
 
 /-- The one-time pad over `l`-bit strings. Encryption and decryption
 are XOR ([KatzLindell2020], Construction 2.9). -/
 noncomputable def otp (l : ℕ) :
     EncScheme (BitVec l) (BitVec l) (BitVec l) :=
-  .ofPure (PMF.uniformOfFintype _) (· ^^^ ·) (· ^^^ ·) fun k m => by
-    simp [xor_cancel_left]
+  .ofPure (uniformOfFintype (BitVec l)) (· ^^^ ·) (· ^^^ ·)
+    (measurable_of_countable _) (measurable_of_countable _) fun k m => by
+      simp [xor_cancel_left]
 
 /-- The ciphertext distribution of the OTP is uniform, regardless of the
 message: masking with a uniform key is the permutation `Equiv.xor` of the
 uniform distribution. -/
 theorem otp_ciphertextDist_eq_uniform (l : ℕ) (m : BitVec l) :
-    (otp l).ciphertextDist m = PMF.uniformOfFintype (BitVec l) := by
-  have h : (fun k : BitVec l => PMF.pure (k ^^^ m)) = (PMF.pure ∘ ⇑(Equiv.xor m)) :=
-    congrArg (PMF.pure ∘ ·) xor_right_eq
-  change (PMF.uniformOfFintype (BitVec l)).bind (fun k => PMF.pure (k ^^^ m)) = _
-  rw [h, PMF.bind_pure_comp, uniformOfFintype_map_equiv]
+    (otp l).ciphertextDist m = uniformOfFintype (BitVec l) := by
+  rw [EncScheme.ciphertextDist_eq_comp]
+  change (uniformOfFintype (BitVec l) : Measure (BitVec l)).bind
+    (fun key => Measure.dirac (key ^^^ m)) = _
+  rw [Measure.bind_dirac_eq_map _ (measurable_of_countable _), xor_right_eq]
+  exact uniformOn_univ_map_equiv (Equiv.xor m)
 
 /-- The one-time pad is perfectly secret ([KatzLindell2020], Theorem 2.10). -/
 theorem otp_perfectlySecret (l : ℕ) : (otp l).PerfectlySecret :=
diff --git a/Cslib/Crypto/Protocols/SecretSharing/Defs.lean b/Cslib/Crypto/Protocols/SecretSharing/Defs.lean
index 5da7d70965..4499cc9033 100644
--- a/Cslib/Crypto/Protocols/SecretSharing/Defs.lean
+++ b/Cslib/Crypto/Protocols/SecretSharing/Defs.lean
@@ -6,7 +6,6 @@ Authors: Samuel Schlesinger
 
 module
 
-public import Cslib.Probability.PMF
 public import Cslib.Crypto.Protocols.SecretSharing.Scheme
 
 /-!
@@ -25,9 +24,9 @@ consequences of the built-in privacy field.
 - `Cslib.Crypto.Protocols.SecretSharing.Scheme.posteriorSecretDist`:
   the posterior distribution on secrets after observing one view
 - `Cslib.Crypto.Protocols.SecretSharing.Scheme.PerfectlyPrivate`:
-  posterior equals prior for unauthorized coalitions
+  independence of secrets and unauthorized views
 - `Cslib.Crypto.Protocols.SecretSharing.Scheme.perfectlyPrivate`:
-  every scheme has posterior privacy
+  every scheme has measure-theoretic privacy
 
 ## References
 
@@ -41,19 +40,20 @@ namespace Cslib.Crypto.Protocols.SecretSharing
 
 namespace Scheme
 
-open Cslib.Probability.PMF
+open MeasureTheory ProbabilityTheory Cslib.Probability.Measure
 
 variable {Secret Randomness Party Share : Type*}
+variable [MeasurableSpace Secret] [MeasurableSpace Randomness] [MeasurableSpace Share]
 
 /-- The distribution of the full share assignment for one secret. -/
-noncomputable def shareDist (scheme : Scheme Secret Randomness Party Share)
-    (secret : Secret) : PMF (Party → Share) :=
+noncomputable abbrev shareDist (scheme : Scheme Secret Randomness Party Share)
+    (secret : Secret) : Measure (Party → Share) :=
   scheme.gen.map (fun r => scheme.share r secret)
 
 /-- The view distribution induced on the coalition `s`. -/
-noncomputable def viewDist (scheme : Scheme Secret Randomness Party Share)
-    (s : Finset Party) (secret : Secret) : PMF (s → Share) :=
-  viewDistOf scheme.gen scheme.share s secret
+noncomputable abbrev viewDist (scheme : Scheme Secret Randomness Party Share)
+    (s : Finset Party) (secret : Secret) : Measure (s → Share) :=
+  scheme.viewKernel s secret
 
 /-- Unauthorized coalitions receive secret-independent view distributions. -/
 theorem viewDist_eq_of_not_authorized
@@ -61,42 +61,41 @@ theorem viewDist_eq_of_not_authorized
     {s : Finset Party} (hs : ¬ scheme.authorized s)
     (secret₀ secret₁ : Secret) :
     scheme.viewDist s secret₀ = scheme.viewDist s secret₁ :=
-  scheme.view_indist s hs secret₀ secret₁
+  by
+    simp only [viewDist, viewKernel, sampleKernel_apply]
+    exact scheme.view_indist s hs secret₀ secret₁
 
-/-- The posterior distribution on secrets after observing the coalition view
-`v`. -/
-noncomputable def posteriorSecretDist
+/-- Mathlib's regular conditional distribution on secrets given a coalition view. -/
+noncomputable abbrev posteriorSecretDist [StandardBorelSpace Secret] [Nonempty Secret]
     (scheme : Scheme Secret Randomness Party Share)
-    (s : Finset Party) (secretDist : PMF Secret) (v : s → Share)
-    (hv : v ∈ (secretDist.bind (scheme.viewDist s)).support) : PMF Secret :=
-  posteriorDist (p := secretDist) (f := scheme.viewDist s) v hv
+    (s : Finset Party) (secretDist : Measure Secret) [IsProbabilityMeasure secretDist] :
+    Kernel (s → Share) Secret :=
+  posterior (scheme.viewKernel s) secretDist
 
-@[simp]
-theorem posteriorSecretDist_apply
-    (scheme : Scheme Secret Randomness Party Share)
-    (s : Finset Party) (secretDist : PMF Secret) (v : s → Share)
-    (hv : v ∈ (secretDist.bind (scheme.viewDist s)).support) (secret : Secret) :
-    scheme.posteriorSecretDist s secretDist v hv secret =
-      (secretDist.bind fun secret' =>
-        (scheme.viewDist s secret').bind fun v' => PMF.pure (secret', v')) (secret, v) /
-        (secretDist.bind (scheme.viewDist s)) v :=
-  posteriorDist_apply secretDist (scheme.viewDist s) v hv secret
-
-/-- Perfect privacy for unauthorized coalitions: conditioning on a view does not
-change the prior on secrets. -/
+/-- Unauthorized views and secrets are independent for every probability prior.
+Equality of joint measures also handles observations of zero singleton mass. -/
 def PerfectlyPrivate (scheme : Scheme Secret Randomness Party Share) : Prop :=
-  ∀ (s : Finset Party) (_hs : ¬ scheme.authorized s)
-    (secretDist : PMF Secret) (v : s → Share)
-    (hv : v ∈ (secretDist.bind (scheme.viewDist s)).support),
-      scheme.posteriorSecretDist s secretDist v hv = secretDist
-
-/-- Every scheme has posterior privacy by definition of `Scheme`. -/
-theorem perfectlyPrivate
-    (scheme : Scheme Secret Randomness Party Share) :
-    scheme.PerfectlyPrivate :=
-  fun s hs secretDist v hv =>
-    posteriorDist_eq_prior_of_outputIndist secretDist (scheme.viewDist s)
-      (scheme.viewDist_eq_of_not_authorized hs) v hv
+  ∀ (s : Finset Party), ¬ scheme.authorized s →
+    ∀ (secretDist : Measure Secret) [IsProbabilityMeasure secretDist],
+      secretDist ⊗ₘ scheme.viewKernel s =
+        secretDist.prod (scheme.viewKernel s ∘ₘ secretDist)
+
+/-- Every scheme has measure-theoretic privacy by its view-indistinguishability field. -/
+theorem perfectlyPrivate (scheme : Scheme Secret Randomness Party Share) :
+    scheme.PerfectlyPrivate := by
+  intro s hs secretDist _
+  exact compProd_eq_prod_of_outputIndist secretDist (scheme.viewKernel s)
+    (scheme.viewDist_eq_of_not_authorized hs)
+
+/-- Conditioning on an unauthorized view leaves the prior unchanged almost surely. -/
+theorem posteriorSecretDist_eq_prior [StandardBorelSpace Secret] [Nonempty Secret]
+    (scheme : Scheme Secret Randomness Party Share)
+    {s : Finset Party} (hs : ¬ scheme.authorized s)
+    (secretDist : Measure Secret) [IsProbabilityMeasure secretDist] :
+    scheme.posteriorSecretDist s secretDist =ᵐ[scheme.viewKernel s ∘ₘ secretDist]
+      fun _ => secretDist :=
+  posterior_eq_prior_of_compProd_eq_prod secretDist (scheme.viewKernel s)
+    (scheme.perfectlyPrivate s hs secretDist)
 
 end Scheme
 
diff --git a/Cslib/Crypto/Protocols/SecretSharing/Scheme.lean b/Cslib/Crypto/Protocols/SecretSharing/Scheme.lean
index 937ad0ba67..38cb15e5aa 100644
--- a/Cslib/Crypto/Protocols/SecretSharing/Scheme.lean
+++ b/Cslib/Crypto/Protocols/SecretSharing/Scheme.lean
@@ -6,9 +6,7 @@ Authors: Samuel Schlesinger
 
 module
 
-public import Cslib.Init
-public import Mathlib.Data.Finset.Basic
-public import Mathlib.Probability.ProbabilityMassFunction.Constructions
+public import Cslib.Probability.Measure
 
 /-!
 # Secret Sharing Schemes
@@ -32,13 +30,16 @@ coalitions.
 
 @[expose] public section
 
+open MeasureTheory ProbabilityTheory Cslib.Probability.Measure
+
 namespace Cslib.Crypto.Protocols.SecretSharing
 
 /-- The view distribution induced by raw sharing data. -/
 noncomputable def viewDistOf {Secret Randomness Party Share : Type*}
-    (gen : PMF Randomness) (share : Randomness → Secret → Party → Share)
-    (s : Finset Party) (secret : Secret) : PMF (s → Share) :=
-  PMF.map (fun r : Randomness => (fun i : s => share r secret i : s → Share)) gen
+    [MeasurableSpace Randomness] [MeasurableSpace Share]
+    (gen : Measure Randomness) (share : Randomness → Secret → Party → Share)
+    (s : Finset Party) (secret : Secret) : Measure (s → Share) :=
+  Measure.map (fun r : Randomness => (fun i : s => share r secret i : s → Share)) gen
 
 /--
 A secret-sharing scheme over secret space `Secret`, randomness space
@@ -49,11 +50,16 @@ secret from the shares generated using any randomness seed. Privacy is
 distributional: unauthorized coalitions have the same view distribution for all
 secrets.
 -/
-structure Scheme (Secret Randomness Party Share : Type*) where
+structure Scheme (Secret Randomness Party Share : Type*)
+    [MeasurableSpace Secret] [MeasurableSpace Randomness] [MeasurableSpace Share] where
   /-- The distribution used to sample the protocol's randomness. -/
-  gen : PMF Randomness
+  gen : Measure Randomness
+  /-- Randomness sampling has total mass one. -/
+  gen_isProbabilityMeasure : IsProbabilityMeasure gen
   /-- Sharing algorithm: one randomness seed determines one share per party. -/
   share : Randomness → Secret → Party → Share
+  /-- Sharing is jointly measurable in its randomness and secret. -/
+  share_measurable : Measurable (Function.uncurry share)
   /-- Reconstruction from a coalition's observed shares. -/
   reconstruct (s : Finset Party) : (s → Share) → Secret
   /-- Authorized coalitions. -/
@@ -69,15 +75,29 @@ structure Scheme (Secret Randomness Party Share : Type*) where
     ∀ (s : Finset Party), ¬ authorized s → ∀ secret₀ secret₁ : Secret,
       viewDistOf gen share s secret₀ = viewDistOf gen share s secret₁
 
+attribute [instance] Scheme.gen_isProbabilityMeasure
+
 namespace Scheme
 
 variable {Secret Randomness Party Share : Type*}
+variable [MeasurableSpace Secret] [MeasurableSpace Randomness] [MeasurableSpace Share]
 
 /-- The restricted shares observed by the coalition `s`. -/
 def view (scheme : Scheme Secret Randomness Party Share) (s : Finset Party)
     (r : Randomness) (secret : Secret) : s → Share :=
   fun i => scheme.share r secret i
 
+/-- The measurable channel from secrets to coalition views. -/
+noncomputable def viewKernel (scheme : Scheme Secret Randomness Party Share)
+    (s : Finset Party) : Kernel Secret (s → Share) :=
+  sampleKernel scheme.gen (scheme.view s) <|
+    Measurable.of_eval fun i => (measurable_pi_apply (i : Party)).comp scheme.share_measurable
+
+instance (scheme : Scheme Secret Randomness Party Share) (s : Finset Party) :
+    IsMarkovKernel (scheme.viewKernel s) := by
+  dsimp [viewKernel]
+  infer_instance
+
 @[simp]
 theorem view_apply (scheme : Scheme Secret Randomness Party Share) (s : Finset Party)
     (r : Randomness) (secret : Secret) (i : s) :
diff --git a/Cslib/Crypto/Protocols/SecretSharing/Shamir.lean b/Cslib/Crypto/Protocols/SecretSharing/Shamir.lean
index c85bcb41d4..56ad4c6db9 100644
--- a/Cslib/Crypto/Protocols/SecretSharing/Shamir.lean
+++ b/Cslib/Crypto/Protocols/SecretSharing/Shamir.lean
@@ -7,9 +7,8 @@ Authors: Samuel Schlesinger
 module
 
 public import Cslib.Crypto.Protocols.SecretSharing.Scheme
-public import Mathlib.Probability.Distributions.Uniform
 public import Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial
-import Cslib.Probability.PMF
+import Mathlib.MeasureTheory.Group.Arithmetic
 
 /-!
 # Shamir Secret Sharing
@@ -63,7 +62,7 @@ noncomputable section
 
 namespace Cslib.Crypto.Protocols.SecretSharing.Shamir
 
-open Cslib.Probability.PMF
+open MeasureTheory ProbabilityTheory Cslib.Probability.Measure
 
 variable {F Party : Type*} [Field F] [Fintype Party]
 
@@ -109,21 +108,49 @@ noncomputable def reconstruct (params : Params F Party)
     (s : Finset Party) (σ : s → F) : F :=
   Polynomial.reconstruct (fun i : s => params.point i) σ
 
+section Sampling
+
+variable [MeasurableSpace F]
+
+/-- The polynomial sharing operation is jointly measurable in the coefficients and secret. -/
+theorem share_measurable [MeasurableAdd₂ F] [MeasurableMul₂ F] (params : Params F Party) :
+    Measurable (Function.uncurry (share params)) := by
+  have heval (coeffs : Randomness params) (x : F) :
+      (Polynomial.tailPolynomial params.threshold coeffs).eval x =
+        ∑ i : Fin params.threshold, coeffs i * x ^ (i : ℕ) := by
+    simpa [Polynomial.tailPolynomial] using
+      _root_.Polynomial.eval_eq_sum_degreeLTEquiv
+        (((_root_.Polynomial.degreeLTEquiv F params.threshold).symm coeffs).property) x
+  apply Measurable.of_eval
+  intro i
+  change Measurable (fun x : Randomness params × F =>
+    (Polynomial.sharingPolynomial x.2
+      (Polynomial.tailPolynomial params.threshold x.1)).eval (params.point i))
+  simp_rw [Polynomial.sharingPolynomial_eval, heval]
+  fun_prop
+
 /-- A sampler on Shamir tail coefficients is privacy-compatible when its
 distribution is invariant under translation by any coefficient vector. This is
 the exact symmetry needed in the privacy proof. -/
 structure TailSampler (params : Params F Party) where
   /-- The underlying coefficient distribution. -/
-  gen : PMF (Randomness params)
+  gen : Measure (Randomness params)
+  /-- The sampler has total mass one. -/
+  gen_isProbabilityMeasure : IsProbabilityMeasure gen
   /-- Translating the coefficients does not change the distribution. -/
   map_add_eq_self : ∀ δ : Randomness params, gen.map (fun coeffs => coeffs + δ) = gen
 
+attribute [instance] TailSampler.gen_isProbabilityMeasure
+
 /-- Uniform tail coefficients form the canonical privacy-compatible sampler. -/
 noncomputable def uniformTailSampler (params : Params F Party)
-    [Fintype F] [Nonempty F] : TailSampler params where
-  gen := PMF.uniformOfFintype (Randomness params)
+    [Fintype F] [Nonempty F] [MeasurableSingletonClass F] : TailSampler params where
+  gen := uniformOfFintype (Randomness params)
+  gen_isProbabilityMeasure := inferInstance
   map_add_eq_self δ := by
-    simpa using uniformOfFintype_map_equiv (Equiv.addRight δ)
+    simpa using uniformOn_univ_map_equiv (Equiv.addRight δ)
+
+end Sampling
 
 private noncomputable def privacyCorrectionPolynomial
     (params : Params F Party) (s : Finset Party)
@@ -204,6 +231,8 @@ private theorem view_eq_view_add_privacyCorrection
   field_simp [params.point_nonzero i]
   ring
 
+variable [MeasurableSpace F] [MeasurableAdd₂ F] [MeasurableMul₂ F]
+
 /-- Translation-invariant Shamir tail samplers induce secret-independent views
 for unauthorized coalitions. -/
 theorem view_indist_of_tailSampler (params : Params F Party)
@@ -218,9 +247,9 @@ theorem view_indist_of_tailSampler (params : Params F Party)
     exact Nat.lt_succ_iff.mp (Nat.not_le.mp hs')
   unfold viewDistOf
   calc
-    PMF.map (fun coeffs : Randomness params =>
+    Measure.map (fun coeffs : Randomness params =>
         (fun i : s => share params coeffs secret₀ i : s → F)) sampler.gen =
-      PMF.map
+      Measure.map
         (fun coeffs : Randomness params => (fun i : s =>
           share params
             (coeffs + privacyCorrection (F := F) params s hcard secret₀ secret₁)
@@ -229,14 +258,18 @@ theorem view_indist_of_tailSampler (params : Params F Party)
         funext coeffs
         exact view_eq_view_add_privacyCorrection
           (F := F) params s hcard secret₀ secret₁ coeffs
-    _ = PMF.map (fun coeffs : Randomness params =>
+    _ = Measure.map (fun coeffs : Randomness params =>
           (fun i : s => share params coeffs secret₁ i : s → F))
-        (PMF.map
+        (Measure.map
           (fun coeffs => coeffs + privacyCorrection (F := F) params s hcard secret₀ secret₁)
           sampler.gen) := by
-          rw [PMF.map_comp]
-          rfl
-    _ = PMF.map (fun coeffs : Randomness params =>
+          rw [Measure.map_map]
+          · rfl
+          · exact Measurable.of_eval fun i =>
+              (measurable_pi_apply (i : Party)).comp
+                ((share_measurable params).comp (measurable_id.prodMk measurable_const))
+          · fun_prop
+    _ = Measure.map (fun coeffs : Randomness params =>
           (fun i : s => share params coeffs secret₁ i : s → F)) sampler.gen := by
           rw [sampler.map_add_eq_self]
 
@@ -245,7 +278,9 @@ noncomputable def schemeWith (params : Params F Party) (sampler : TailSampler pa
     :
     SecretSharing.Scheme F (Randomness params) Party F :=
   { gen := sampler.gen
+    gen_isProbabilityMeasure := inferInstance
     share := share params
+    share_measurable := share_measurable params
     reconstruct := reconstruct params
     authorized := authorized params
     authorized_mono := fun _ _ hsu hs => le_trans hs (Finset.card_le_card hsu)
@@ -280,7 +315,7 @@ noncomputable def schemeWith (params : Params F Party) (sampler : TailSampler pa
 /-- The canonical finite-field Shamir scheme with uniformly sampled tail
 coefficients. -/
 noncomputable def scheme (params : Params F Party)
-    [Fintype F] [Nonempty F] :
+    [Fintype F] [Nonempty F] [MeasurableSingletonClass F] :
     SecretSharing.Scheme F (Randomness params) Party F :=
   schemeWith params (uniformTailSampler params)
 
@@ -292,7 +327,7 @@ theorem schemeWith_authorized_iff (params : Params F Party)
 
 @[simp]
 theorem scheme_authorized_iff (params : Params F Party)
-    [Fintype F] [Nonempty F] (s : Finset Party) :
+    [Fintype F] [Nonempty F] [MeasurableSingletonClass F] (s : Finset Party) :
     (scheme params).authorized s ↔ params.threshold + 1 ≤ s.card :=
   Iff.rfl
 
diff --git a/Cslib/Crypto/README.md b/Cslib/Crypto/README.md
index 6d1f4fdac2..3c477eea28 100644
--- a/Cslib/Crypto/README.md
+++ b/Cslib/Crypto/README.md
@@ -22,7 +22,7 @@ To this end, we expect to leverage the combination of `Crypto` and [Languages](.
 ## Pseudorandom generators
 
 [`Primitives/PRG`](Primitives/PRG) formalizes Boneh and Shoup's Attack Game 3.1 using
-PMFs. `Generator.Secure G Admissible ε` bounds the distinguishing advantage of every
+Mathlib probability measures. `Generator.Secure G Admissible ε` bounds the distinguishing advantage of every
 admissible randomized test. `Family.SecureWithError` allows a parameter-dependent error bound;
 `Family.Secure` requires negligible advantage separately for each admissible family, using
 Mathlib's `SuperpolynomialDecay`. A negligible error bound implies this asymptotic notion.
@@ -36,6 +36,27 @@ are consequently insecure against any class admitting this test, with both `Fin
 and `BitVec n` versions and nonexistence corollaries. Zero-error security against all tests
 is equivalent to exactly uniform output; the identity generator is a nonexpanding example.
 
+## Information-theoretic protocols
+
+Perfect secrecy and secret sharing use Mathlib's `Measure` and measurable `Kernel` interfaces.
+Normalization is recorded by `IsProbabilityMeasure` and `IsMarkovKernel`. Secrecy means equality
+of the joint measure and the product of its marginals, for every probability prior.
+This supports continuous distributions as well as discrete ones.
+
+Encryption correctness requires that almost every generated key work for every message,
+with decryption succeeding almost surely over encryption randomness. The exceptional set of
+keys is shared by all messages. For countable message spaces, Mathlib's `ae_all_iff` shows that
+this is equivalent to a separate almost-sure correctness guarantee for each message.
+
+Posterior distributions use Mathlib's regular conditional kernel `ProbabilityTheory.posterior`.
+These APIs require a nonempty standard Borel message or secret space, and posterior equality
+holds almost everywhere under the observation distribution. On countable observation spaces,
+Mathlib's `ae_iff_of_countable` recovers equality at every observation with positive mass.
+The core independence definitions do not require standard Borel spaces.
+
+Finite samplers, including the one-time pad and Shamir's finite-field sampler, use Mathlib's
+`uniformOn`. The finite PRG games retain their finite-space assumptions.
+
 ## Plans and notes
 
 - We plan on developing applied calculi and logics for modelling and reasoning about security protocols.
diff --git a/Cslib/Foundations/Data/BitVec.lean b/Cslib/Foundations/Data/BitVec.lean
new file mode 100644
index 0000000000..85169919d9
--- /dev/null
+++ b/Cslib/Foundations/Data/BitVec.lean
@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Cslib.Init
+public import Mathlib.MeasureTheory.MeasurableSpace.Instances
+
+/-!
+# Measurable bitvectors
+
+Bitvectors carry the discrete measurable space, like `Bool` and `Fin` in Mathlib.
+-/
+
+public section
+
+instance BitVec.instMeasurableSpace (n : ℕ) : MeasurableSpace (BitVec n) := ⊤
+
+instance BitVec.instMeasurableSingletonClass (n : ℕ) :
+    MeasurableSingletonClass (BitVec n) := ⟨fun _ => trivial⟩
diff --git a/Cslib/Probability/Measure.lean b/Cslib/Probability/Measure.lean
new file mode 100644
index 0000000000..16f6b40599
--- /dev/null
+++ b/Cslib/Probability/Measure.lean
@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Cslib.Init
+public import Mathlib.Probability.UniformOn
+public import Mathlib.Probability.Kernel.Posterior
+public import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
+
+/-!
+# Measure and kernel utilities
+
+Small consequences of Mathlib's uniform measures, kernel composition, and posterior API.
+General probability interfaces use `Measure` and `Kernel`; finite sampling uses `uniformOn`.
+-/
+
+@[expose] public section
+
+open MeasureTheory ProbabilityTheory
+open scoped ENNReal
+
+namespace Cslib.Probability.Measure
+
+variable {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
+
+/-- Sample randomness and apply a jointly measurable deterministic computation. -/
+noncomputable def sampleKernel {Randomness : Type*} [MeasurableSpace Randomness]
+    (μ : Measure Randomness) (f : Randomness → α → β)
+    (hf : Measurable (Function.uncurry f)) : Kernel α β :=
+  Kernel.deterministic (Function.uncurry f) hf ∘ₖ (Kernel.const α μ ×ₖ Kernel.id)
+
+@[simp]
+theorem sampleKernel_apply {Randomness : Type*} [MeasurableSpace Randomness]
+    (μ : Measure Randomness) [SFinite μ] (f : Randomness → α → β)
+    (hf : Measurable (Function.uncurry f)) (a : α) :
+    sampleKernel μ f hf a = μ.map (fun r => f r a) := by
+  simp [sampleKernel, Kernel.comp_apply, Kernel.prod_apply, Kernel.id_apply,
+    Measure.deterministic_comp_eq_map, Measure.prod_dirac,
+    Measure.map_map hf measurable_prodMk_right, Function.comp_def]
+
+instance {Randomness : Type*} [MeasurableSpace Randomness]
+    (μ : Measure Randomness) [IsProbabilityMeasure μ] (f : Randomness → α → β)
+    (hf : Measurable (Function.uncurry f)) : IsMarkovKernel (sampleKernel μ f hf) := by
+  unfold sampleKernel
+  infer_instance
+
+/-- Uniform probability measure on a nonempty finite type. -/
+noncomputable abbrev uniformOfFintype (α : Type*) [MeasurableSpace α]
+    [Fintype α] [Nonempty α] : ProbabilityMeasure α :=
+  (uniformOn (Set.univ : Set α)).toProbabilityMeasure
+
+/-- Uniform sampling is invariant under an equivalence of finite discrete spaces. -/
+theorem uniformOn_univ_map_equiv [Finite α] [Finite β]
+    [MeasurableSingletonClass α] [MeasurableSingletonClass β] (e : α ≃ β) :
+    (uniformOn (Set.univ : Set α)).map e = uniformOn (Set.univ : Set β) := by
+  classical
+  let := Fintype.ofFinite α
+  let := Fintype.ofFinite β
+  apply Measure.ext_of_singleton
+  intro b
+  rw [Measure.map_apply (measurable_of_countable e) (measurableSet_singleton b)]
+  have he : e ⁻¹' {b} = {e.symm b} := by
+    ext a
+    change e a = b ↔ a = e.symm b
+    exact ⟨fun h => by simpa using congrArg e.symm h, fun h => by simp [h]⟩
+  simp [he, uniformOn_univ, Fintype.card_congr e]
+
+/-- An input-independent channel produces an independent joint distribution. -/
+theorem compProd_eq_prod_of_outputIndist (μ : Measure α) [IsProbabilityMeasure μ]
+    (κ : Kernel α β) [IsMarkovKernel κ] (h : ∀ a₀ a₁, κ a₀ = κ a₁) :
+    μ ⊗ₘ κ = μ.prod (κ ∘ₘ μ) := by
+  have : Nonempty α := nonempty_of_isProbabilityMeasure μ
+  obtain ⟨a⟩ := ‹Nonempty α›
+  have hκ : κ = Kernel.const α (κ a) := Kernel.ext fun a' => h a' a
+  rw [hκ]
+  simp
+
+/-- Independence leaves the prior unchanged almost surely under conditioning. -/
+theorem posterior_eq_prior_of_compProd_eq_prod [StandardBorelSpace α] [Nonempty α]
+    (μ : Measure α) [IsProbabilityMeasure μ] (κ : Kernel α β) [IsMarkovKernel κ]
+    (h : μ ⊗ₘ κ = μ.prod (κ ∘ₘ μ)) :
+    posterior κ μ =ᵐ[κ ∘ₘ μ] fun _ => μ := by
+  exact (ae_eq_posterior_of_compProd_eq (η := Kernel.const β μ) (by
+    rw [h, Measure.compProd_const, Measure.prod_swap])).symm
+
+end Cslib.Probability.Measure
diff --git a/Cslib/Probability/PMF.lean b/Cslib/Probability/PMF.lean
deleted file mode 100644
index 8c4c8a63d5..0000000000
--- a/Cslib/Probability/PMF.lean
+++ /dev/null
@@ -1,102 +0,0 @@
-/-
-Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Samuel Schlesinger
--/
-
-module
-
-public import Cslib.Init
-public import Mathlib.Probability.ProbabilityMassFunction.Monad
-public import Mathlib.Probability.Distributions.Uniform
-
-/-!
-# PMF Utilities
-
-## NB: This module is temporary
-
-Everything here is a general PMF bind/pure lemma with no dependence on
-any domain-specific structure. It should be upstreamed to Mathlib
-(likely `Mathlib.Probability.ProbabilityMassFunction.Monad` or a new
-`Mathlib.Probability.ProbabilityMassFunction.Prod`). Once accepted
-upstream, this file should be deleted and its consumers should import
-the Mathlib module instead.
-
-## Main results
-
-- `Cslib.Probability.PMF.bind_pair_apply`: the "pairing" bind at `(a, b)` equals `p a * f a b`
-- `Cslib.Probability.PMF.bind_pair_tsum_fst`: marginalizing over the first component
-- `Cslib.Probability.PMF.uniformOfFintype_map_equiv`:
-  a uniform distribution is invariant under equivalence
-- `Cslib.Probability.PMF.posteriorDist`: the posterior as a `PMF`
-- `Cslib.Probability.PMF.posteriorDist_eq_prior_of_outputIndist`:
-  if the output distribution does not depend on the input, conditioning does
-  not change the prior
--/
-
-@[expose] public section
-
-namespace Cslib.Probability.PMF
-
-open ENNReal
-
-universe u v
-variable {α : Type u} {β : Type v}
-
-/-- Evaluating the "pairing" bind `(do let a ← p; return (a, ← f a))` at `(a, b)`
-gives the product `p a * f a b`. -/
-theorem bind_pair_apply (p : PMF α) (f : α → PMF β) (a : α) (b : β) :
-    (p.bind fun a' => (f a').bind fun b' => PMF.pure (a', b')) (a, b) = p a * f a b := by
-  rw [PMF.bind_apply, tsum_eq_single a]
-  · rw [PMF.bind_apply]; congr 1; rw [tsum_eq_single b]
-    · simp [PMF.pure_apply]
-    · intro b' hb'; simp [PMF.pure_apply, hb'.symm]
-  · intro a' ha'; rw [PMF.bind_apply]; simp [PMF.pure_apply, ha'.symm]
-
-/-- Summing the pairing bind over the first component gives the marginal. -/
-theorem bind_pair_tsum_fst (p : PMF α) (f : α → PMF β) (b : β) :
-    ∑' a, (p.bind fun a' => (f a').bind fun b' => PMF.pure (a', b')) (a, b) =
-      (p.bind f) b := by
-  simp_rw [bind_pair_apply, PMF.bind_apply]
-
-/-- A uniform distribution on a finite type is invariant under any equivalence. -/
-theorem uniformOfFintype_map_equiv {γ : Type v} [Fintype α] [Fintype γ] [Nonempty α] [Nonempty γ]
-    (e : α ≃ γ) :
-    (PMF.uniformOfFintype α).map e = PMF.uniformOfFintype γ := by
-  ext c
-  rw [PMF.map_apply, tsum_eq_single (e.symm c)]
-  · simp [Fintype.card_congr e]
-  · exact fun a ha => ite_eq_right fun h => ha (by simp [h])
-
-/-- The posterior distribution `Pr[A = a | B = b]` as a `PMF`,
-given `a ← p`, `b ← f a`, and that `b` has positive marginal probability:
-the joint distribution's slice at `b`, normalized. -/
-noncomputable def posteriorDist (p : PMF α) (f : α → PMF β) (b : β)
-    (hb : b ∈ (p.bind f).support) : PMF α :=
-  PMF.normalize
-    (fun a => (p.bind fun a' => (f a').bind fun b' => PMF.pure (a', b')) (a, b))
-    (by rw [bind_pair_tsum_fst]; exact (PMF.mem_support_iff _ _).mp hb)
-    (by rw [bind_pair_tsum_fst]; exact PMF.apply_ne_top _ _)
-
-@[simp]
-theorem posteriorDist_apply (p : PMF α) (f : α → PMF β) (b : β)
-    (hb : b ∈ (p.bind f).support) (a : α) :
-    posteriorDist p f b hb a =
-      (p.bind fun a' => (f a').bind fun b' => PMF.pure (a', b')) (a, b) /
-        (p.bind f) b := by
-  rw [posteriorDist, PMF.normalize_apply, bind_pair_tsum_fst, div_eq_mul_inv]
-
-/-- If the output distribution of a channel does not depend on the input, then
-conditioning on any output with positive probability leaves the prior unchanged. -/
-theorem posteriorDist_eq_prior_of_outputIndist (p : PMF α) (f : α → PMF β)
-    (h : ∀ a₀ a₁ : α, f a₀ = f a₁)
-    (b : β) (hb : b ∈ (p.bind f).support) :
-    posteriorDist p f b hb = p := by
-  ext a
-  have hbind : p.bind f = f a :=
-    (congrArg p.bind (funext fun a' => h a' a)).trans (PMF.bind_const p (f a))
-  rw [posteriorDist_apply, bind_pair_apply, hbind]
-  exact ENNReal.mul_div_cancel_right ((PMF.mem_support_iff _ _).mp (hbind ▸ hb))
-    (PMF.apply_ne_top _ _)
-
-end Cslib.Probability.PMF
diff --git a/CslibTests.lean b/CslibTests.lean
index b39a27de5e..b4b65dbfdc 100644
--- a/CslibTests.lean
+++ b/CslibTests.lean
@@ -31,6 +31,7 @@ import CslibTests.PACLearning
 import CslibTests.PFunctor
 import CslibTests.PFunctorFree
 import CslibTests.PRG
+import CslibTests.ProbabilityMeasures
 import CslibTests.Reduction
 import CslibTests.StatefulProcesses
 import CslibTests.Synthesis
diff --git a/CslibTests/PRG.lean b/CslibTests/PRG.lean
index aaf4264efa..a35ccca4fd 100644
--- a/CslibTests/PRG.lean
+++ b/CslibTests/PRG.lean
@@ -6,7 +6,7 @@ Authors: Samuel Schlesinger
 
 import Cslib.Crypto.Primitives.PRG.Asymptotic
 
-open Cslib.Crypto.PRG Filter
+open Cslib.Crypto.PRG Cslib.Probability.Measure MeasureTheory Filter
 open scoped NNReal Topology
 
 namespace CslibTests.PRG
@@ -18,12 +18,13 @@ example {Seed Output : Type*} (G H : Generator Seed Output)
 -- The identity generator is secure with zero error.
 example : (Generator.mk (id : Bool → Bool)).Secure (fun _ => True) 0 := by
   apply Generator.secure_zero_of_outputDist_eq
-  exact PMF.map_id _
+  exact Measure.map_id
 
 -- Zero-error security implies uniform output.
-example {Seed Output : Type*} [Fintype Seed] [Nonempty Seed]
+example {Seed Output : Type*} [MeasurableSpace Seed] [MeasurableSingletonClass Seed]
+    [MeasurableSpace Output] [MeasurableSingletonClass Output] [Fintype Seed] [Nonempty Seed]
     [Fintype Output] [Nonempty Output] (G : Generator Seed Output)
-    (h : G.Secure (fun _ => True) 0) : G.outputDist = PMF.uniformOfFintype Output :=
+    (h : G.Secure (fun _ => True) 0) : G.outputDist = uniformOfFintype Output :=
   G.secure_zero_iff_outputDist_eq_uniform.mp h
 
 example (G : Generator Bool (Bool × Bool)) (Admissible : Adversary (Bool × Bool) → Prop)
@@ -32,7 +33,7 @@ example (G : Generator Bool (Bool × Bool)) (Admissible : Adversary (Bool × Boo
 
 -- Tests that ignore their input have zero advantage.
 example (G : Generator Bool (Bool × Bool)) :
-    G.Secure (fun adversary => ∃ p : PMF Bool, adversary = fun _ => p) 0 := by
+    G.Secure (fun adversary => ∃ p : ProbabilityMeasure Bool, adversary = fun _ => p) 0 := by
   rintro adversary ⟨p, rfl⟩
   simp
 
@@ -65,7 +66,7 @@ example : Family.Secure (fun n => Generator.mk (id : (Fin n → Bool) → (Fin n
       (fun _ => True) (fun _ => 0) := by
     intro adversary_family _ n
     simp [Generator.advantage, Generator.realExperiment, Generator.idealExperiment,
-      Generator.outputDist, PMF.map_id]
+      Generator.outputDist, Measure.map_id]
   exact h.secure (Asymptotics.superpolynomialDecay_zero _ _)
 
 -- The inverse-polynomial gap 1 / (n + 2) rules out asymptotic security.
diff --git a/CslibTests/ProbabilityMeasures.lean b/CslibTests/ProbabilityMeasures.lean
new file mode 100644
index 0000000000..5477b7a476
--- /dev/null
+++ b/CslibTests/ProbabilityMeasures.lean
@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Cslib.Crypto.Primitives.PRG.Basic
+import Cslib.Crypto.Protocols.PerfectSecrecy.OneTimePad
+import Cslib.Crypto.Protocols.SecretSharing.Defs
+import Cslib.Crypto.Protocols.SecretSharing.Shamir
+import Mathlib.Probability.Distributions.Gaussian.Real
+import Mathlib.Probability.ProbabilityMassFunction.Constructions
+
+open MeasureTheory ProbabilityTheory Cslib.Probability.Measure
+open scoped ENNReal
+open Cslib.Crypto.Protocols.PerfectSecrecy Cslib.Crypto.PRG
+
+namespace CslibTests.ProbabilityMeasures
+
+-- An independently specified old-style fair bit gives exactly the same output laws.
+private noncomputable def fairBit : PMF Bool :=
+  PMF.ofFintype (fun _ => 1 / 2) (by
+    norm_num [Fintype.sum_bool]
+    exact ENNReal.mul_inv_cancel (by norm_num) (by norm_num))
+
+example (f : Bool → Bool × Bool) :
+    (Generator.mk f).outputDist = (fairBit.map f).toMeasure := by
+  have h : (uniformOfFintype Bool : Measure Bool) = fairBit.toMeasure := by
+    apply Measure.ext_of_singleton
+    intro b
+    change uniformOn (Set.univ : Set Bool) {b} = fairBit.toMeasure {b}
+    rw [uniformOn_univ, PMF.toMeasure_apply_singleton _ _ (measurableSet_singleton _)]
+    simp [fairBit, PMF.ofFintype_apply]
+  change (uniformOfFintype Bool : Measure Bool).map f = _
+  rw [h, PMF.toMeasure_map f fairBit (measurable_of_countable f)]
+
+-- The expected ciphertext probability is unchanged by the migration.
+example (l : ℕ) (m c : BitVec l) :
+    (otp l).ciphertextDist m {c} = (2 ^ l : ℝ≥0∞)⁻¹ := by
+  simp [otp_ciphertextDist_eq_uniform, uniformOfFintype, uniformOn_univ,
+    ← FinEnum.card_eq_fintypeCard, FinEnum.card_bitVec]
+
+-- Almost-sure posterior equality recovers the former positive-mass discrete statement.
+example (l : ℕ) (μ : Measure (BitVec l)) [IsProbabilityMeasure μ] (c : BitVec l)
+    (hc : (otp l).marginalCiphertextDist μ {c} ≠ 0) :
+    (otp l).posteriorMsgDist μ c = μ :=
+  ae_iff_of_countable.mp ((otp l).posteriorMsgDist_eq_prior (otp_perfectlySecret l) μ) c hc
+
+-- Continuous keys and ciphertexts are accepted by the public encryption interface.
+private noncomputable def gaussianMask : EncScheme ℝ ℝ ℝ :=
+  .ofPure (gaussianReal 0 1) (fun key message => key + message)
+    (fun key ciphertext => ciphertext - key) (by fun_prop) (by fun_prop)
+    (fun _ _ => by ring)
+
+example : IsProbabilityMeasure (gaussianMask.ciphertextDist 3) := inferInstance
+
+-- The common set of good keys also covers a message chosen using the sampled key.
+example : ∀ᵐ key ∂gaussianMask.gen, ∀ᵐ c ∂gaussianMask.enc (key, key),
+    gaussianMask.dec key c = key := by
+  filter_upwards [gaussianMask.correct] with key hk
+  exact hk key
+
+-- Independence and conditioning also work with a non-atomic prior and observation law.
+example : posterior (Kernel.const ℝ (gaussianReal 1 2)) (gaussianReal 0 1)
+    =ᵐ[gaussianReal 1 2] fun _ => gaussianReal 0 1 := by
+  simpa using posterior_eq_prior_of_compProd_eq_prod (gaussianReal 0 1)
+    (Kernel.const ℝ (gaussianReal 1 2)) (by simp)
+
+open Cslib.Crypto.Protocols.SecretSharing
+
+-- Shamir's canonical sampler remains normalized, with privacy for unauthorized coalitions.
+example {F Party : Type*} [Field F] [Fintype F] [Fintype Party]
+    [MeasurableSpace F] [MeasurableSingletonClass F] (params : Shamir.Params F Party) :
+    (Shamir.scheme params).PerfectlyPrivate := (Shamir.scheme params).perfectlyPrivate
+
+example {Secret Randomness Party Share : Type*}
+    [MeasurableSpace Secret] [MeasurableSpace Randomness] [MeasurableSpace Share]
+    (scheme : Scheme Secret Randomness Party Share) (s : Finset Party) (secret : Secret) :
+    IsProbabilityMeasure (scheme.viewDist s secret) := inferInstance
+
+end CslibTests.ProbabilityMeasures
diff --git a/lake-manifest.json b/lake-manifest.json
index 3d5b9d01d9..d33e96d0d9 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9a6fbe02d04cd1f582eac50a8a4e34ad67582169",
+   "rev": "be31cde2c2cb07d7562e5e891b302f9286cd0a68",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "9a6fbe02d04cd1f582eac50a8a4e34ad67582169",
+   "inputRev": "be31cde2c2cb07d7562e5e891b302f9286cd0a68",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "679a93b2dc7563f54cc0a851c2574e2647e47ba0",
+   "rev": "914928598160c128affd7a42640b4237b7e4d912",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lakefile.toml b/lakefile.toml
index 447fa37391..9fcbab13cd 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -18,7 +18,7 @@ weak.linter.unicodeLinter = false
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "9a6fbe02d04cd1f582eac50a8a4e34ad67582169"
+rev = "be31cde2c2cb07d7562e5e891b302f9286cd0a68"
 
 [[lean_lib]]
 name = "Cslib"