Monotone limits of sub-distributions

A sequence f : ℕ → SDistr α is a MonoSeq when the weight it assigns to each value is non-decreasing in n. Its limit mlim f h assigns to each value the supremum of the weights, and puts the residual mass on failure.

SDistr α is a probability mass function on Option α, of total mass exactly one, so the failure component of the limit is determined: it is 1 minus the total weight of the values, and constructing the limit needs the bound ∑' a, ⨆ n, f n (some a) ≤ 1.

Main definitions

• MonoSeq f — the weight of every value is non-decreasing along f
• mlim f h — the limit of a MonoSeq

Main results

• tsum_iSup_of_monotone — summation commutes with a monotone supremum
• mlim_bind — the limit commutes with bind on the left
• bind_mlim — the limit commutes with bind on the right
• mass_mlim — the mass of the limit is the supremum of the masses
• mlim_const — a constant sequence is its own limit

Correspondence with EasyCrypt

mlim_bind and bind_mlim are the images of dlet_lim and dlim_let of the Distr theory, the two laws that carry the denotation of while through a bind.

Summation against a monotone supremum

theorem CatCrypt.NonUniform.tsum_iSup_of_monotone {α : Type u_1} {g : α → ℕ → ENNReal} (hg : ∀ (a : α), Monotone (g a)) : ∑' (a : α), ⨆ (n : ℕ), g a n = ⨆ (n : ℕ), ∑' (a : α), g a n

Summation commutes with the supremum of a family that is monotone in the supremum index.

The weight a bind assigns to a value

theorem CatCrypt.NonUniform.bind_apply_some {α : Type u_1} {β : Type u_2} (d : Prob.SDistr α) (g : α → Prob.SDistr β) (b : β) : (d.bind g) (some b) = ∑' (a : α), d (some a) * (g a) (some b)

The weight of a value under a bind is the average of its weights under the continuation. The failure branch contributes nothing.

Non-decreasing sequences

def CatCrypt.NonUniform.MonoSeq {α : Type u_1} (f : ℕ → Prob.SDistr α) : Prop

A sequence of sub-distributions whose weight at every value is non-decreasing.

Equations

• CatCrypt.NonUniform.MonoSeq f = ∀ (n m : ℕ), n ≤ m → ∀ (a : α), (f n) (some a) ≤ (f m) (some a)

theorem CatCrypt.NonUniform.MonoSeq.monotone {α : Type u_1} {f : ℕ → Prob.SDistr α} (h : MonoSeq f) (a : α) : Monotone fun (n : ℕ) => (f n) (some a)

The weight of a fixed value along a MonoSeq is a monotone function of the index.

theorem CatCrypt.NonUniform.monoSeq_const {α : Type u_1} (d : Prob.SDistr α) : MonoSeq fun (x : ℕ) => d

A constant sequence is non-decreasing.

theorem CatCrypt.NonUniform.MonoSeq.bind_left {α : Type u_1} {β : Type u_2} {f : ℕ → Prob.SDistr α} (h : MonoSeq f) (g : α → Prob.SDistr β) : MonoSeq fun (n : ℕ) => (f n).bind g

Binding a non-decreasing sequence on the left keeps it non-decreasing.

theorem CatCrypt.NonUniform.monoSeq_bind_right {α : Type u_1} {β : Type u_2} (d : Prob.SDistr α) {f : ℕ → α → Prob.SDistr β} (h : ∀ (a : α), MonoSeq fun (n : ℕ) => f n a) : MonoSeq fun (n : ℕ) => d.bind fun (a : α) => f n a

Binding a pointwise non-decreasing family on the right gives a non-decreasing sequence.

The limit

theorem CatCrypt.NonUniform.tsum_iSup_le_one {α : Type u_1} (f : ℕ → Prob.SDistr α) (h : MonoSeq f) : ∑' (a : α), ⨆ (n : ℕ), (f n) (some a) ≤ 1

The total weight of the values in the limit of a non-decreasing sequence is at most one.

noncomputable def CatCrypt.NonUniform.mlim {α : Type u_1} (f : ℕ → Prob.SDistr α) (h : MonoSeq f) : Prob.SDistr α

The limit of a non-decreasing sequence of sub-distributions: each value gets the supremum of its weights, and failure gets the rest.

Equations

• CatCrypt.NonUniform.mlim f h = ⟨fun (oa : Option α) => match oa with | none => 1 - ∑' (a : α), ⨆ (n : ℕ), (f n) (some a) | some a => ⨆ (n : ℕ), (f n) (some a), ⋯⟩

@[simp]

theorem CatCrypt.NonUniform.mlim_apply_some {α : Type u_1} (f : ℕ → Prob.SDistr α) (h : MonoSeq f) (a : α) : (mlim f h) (some a) = ⨆ (n : ℕ), (f n) (some a)

The limit assigns to a value the supremum of the weights of the sequence.

theorem CatCrypt.NonUniform.mlim_apply_none {α : Type u_1} (f : ℕ → Prob.SDistr α) (h : MonoSeq f) : (mlim f h) none = 1 - ∑' (a : α), ⨆ (n : ℕ), (f n) (some a)

The failure weight of the limit is the mass the values leave over.

theorem CatCrypt.NonUniform.apply_some_le_mlim {α : Type u_1} (f : ℕ → Prob.SDistr α) (h : MonoSeq f) (n : ℕ) (a : α) : (f n) (some a) ≤ (mlim f h) (some a)

Every member of the sequence is below the limit at every value.

theorem CatCrypt.NonUniform.mass_mlim {α : Type u_1} (f : ℕ → Prob.SDistr α) (h : MonoSeq f) : (mlim f h).mass = ⨆ (n : ℕ), (f n).mass

The mass of the limit is the supremum of the masses.

theorem CatCrypt.NonUniform.mlim_const {α : Type u_1} (d : Prob.SDistr α) : mlim (fun (x : ℕ) => d) ⋯ = d

A constant sequence has itself as limit.

Interchange with bind

theorem CatCrypt.NonUniform.mlim_bind {α : Type u_1} {β : Type u_2} (f : ℕ → Prob.SDistr α) (h : MonoSeq f) (g : α → Prob.SDistr β) : (mlim f h).bind g = mlim (fun (n : ℕ) => (f n).bind g) ⋯

The limit commutes with bind on the left: binding the limit of a non-decreasing sequence is the limit of the binds.

theorem CatCrypt.NonUniform.bind_mlim {α : Type u_1} {β : Type u_2} (d : Prob.SDistr α) (f : ℕ → α → Prob.SDistr β) (h : ∀ (a : α), MonoSeq fun (n : ℕ) => f n a) : (d.bind fun (a : α) => mlim (fun (n : ℕ) => f n a) ⋯) = mlim (fun (n : ℕ) => d.bind fun (a : α) => f n a) ⋯

The limit commutes with bind on the right: binding into the limit of a pointwise non-decreasing family is the limit of the binds.