Sequences drawn from a prediction rule

A prediction rule gives, after every finite sequence of draws, the distribution of the next draw: a family of kernels κ n : Kernel (Fin n → α) α ([Pit06] p. 45 and p. 58). seqLaw κ n is the law of the first n draws, built one draw at a time: the empty sequence, then the joint law of the sequence so far and the next draw, appended with Fin.snoc.

On a countable space the mass of a sequence is the product, along the sequence, of the probability of each draw given the ones before it (seqLaw_singleton). This is the Fin-indexed form of the Ionescu–Tulcea partial trajectory: after the first draw, the law of the next n is ProbabilityTheory.Kernel.partialTraj of the prediction rule read on trajectories (seqLaw_succ_eq_map_partialTraj).

Main definitions

• ProbabilityTheory.seqLaw κ n: the law of the first n draws of the prediction rule κ.
• ProbabilityTheory.seqTrajectory κ: the law of the whole sequence of draws, the Ionescu–Tulcea trajectory measure started at the first draw.

Main results

• ProbabilityTheory.isProbabilityMeasure_seqLaw: a Markov prediction rule gives probability laws.
• ProbabilityTheory.seqLaw_succ_singleton_snoc, ProbabilityTheory.seqLaw_singleton: the chain rule on a countable space.
• ProbabilityTheory.integral_seqLaw_succ: the chain rule for expectations.
• ProbabilityTheory.seqLaw_succ_eq_map_partialTraj: the law as a partial trajectory.
• ProbabilityTheory.seqTrajectory_map_frestrictLe: the first draws of the whole sequence have the law of the first draws.

References

• [Pit06]

theorem ProbabilityTheory.measurable_snoc_prod {α : Type u_1} [MeasurableSpace α] {n : ℕ} : Measurable fun (p : (Fin n → α) × α) => Fin.snoc p.1 p.2

noncomputable def ProbabilityTheory.seqLaw {α : Type u_1} [MeasurableSpace α] (κ : (n : ℕ) → Kernel (Fin n → α) α) (n : ℕ) : MeasureTheory.Measure (Fin n → α)

The law of the first n draws of the sequence with prediction rule κ: each draw is sampled from κ at the sequence so far and appended to it.

Equations

• ProbabilityTheory.seqLaw κ 0 = MeasureTheory.Measure.dirac default
• ProbabilityTheory.seqLaw κ n.succ = MeasureTheory.Measure.map (fun (p : (Fin n → α) × α) => Fin.snoc p.1 p.2) ((ProbabilityTheory.seqLaw κ n).compProd (κ n))

@[simp]

theorem ProbabilityTheory.seqLaw_zero {α : Type u_1} [MeasurableSpace α] {κ : (n : ℕ) → Kernel (Fin n → α) α} : seqLaw κ 0 = MeasureTheory.Measure.dirac default

theorem ProbabilityTheory.seqLaw_succ {α : Type u_1} [MeasurableSpace α] {κ : (n : ℕ) → Kernel (Fin n → α) α} (n : ℕ) : seqLaw κ (n + 1) = MeasureTheory.Measure.map (fun (p : (Fin n → α) × α) => Fin.snoc p.1 p.2) ((seqLaw κ n).compProd (κ n))

theorem ProbabilityTheory.sFinite_seqLaw {α : Type u_1} [MeasurableSpace α] {κ : (n : ℕ) → Kernel (Fin n → α) α} [∀ (n : ℕ), IsSFiniteKernel (κ n)] (n : ℕ) : MeasureTheory.SFinite (seqLaw κ n)

instance ProbabilityTheory.instSFiniteForallFinSeqLawOfIsSFiniteKernel {α : Type u_1} [MeasurableSpace α] {κ : (n : ℕ) → Kernel (Fin n → α) α} [∀ (n : ℕ), IsSFiniteKernel (κ n)] (n : ℕ) : MeasureTheory.SFinite (seqLaw κ n)

theorem ProbabilityTheory.isProbabilityMeasure_seqLaw {α : Type u_1} [MeasurableSpace α] {κ : (n : ℕ) → Kernel (Fin n → α) α} [∀ (n : ℕ), IsMarkovKernel (κ n)] (n : ℕ) : MeasureTheory.IsProbabilityMeasure (seqLaw κ n)

instance ProbabilityTheory.instIsProbabilityMeasureForallFinSeqLawOfIsMarkovKernel {α : Type u_1} [MeasurableSpace α] {κ : (n : ℕ) → Kernel (Fin n → α) α} [∀ (n : ℕ), IsMarkovKernel (κ n)] (n : ℕ) : MeasureTheory.IsProbabilityMeasure (seqLaw κ n)

theorem ProbabilityTheory.integral_seqLaw_succ {α : Type u_1} [MeasurableSpace α] {κ : (n : ℕ) → Kernel (Fin n → α) α} [∀ (n : ℕ), IsSFiniteKernel (κ n)] {n : ℕ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : (Fin (n + 1) → α) → E} (hf : MeasureTheory.Integrable f (seqLaw κ (n + 1))) : ∫ (s : Fin (n + 1) → α), f s ∂seqLaw κ (n + 1) = ∫ (s : Fin n → α), ∫ (x : α), f (Fin.snoc s x) ∂(κ n) s ∂seqLaw κ n

The chain rule for expectations: integrating over the first n + 1 draws integrates the next draw against the prediction rule, then the first n.

theorem ProbabilityTheory.seqLaw_succ_singleton_snoc {α : Type u_1} [MeasurableSpace α] {κ : (n : ℕ) → Kernel (Fin n → α) α} [MeasurableSingletonClass α] [∀ (n : ℕ), IsSFiniteKernel (κ n)] {n : ℕ} (s : Fin n → α) (c : α) : (seqLaw κ (n + 1)) {Fin.snoc s c} = (seqLaw κ n) {s} * ((κ n) s) {c}

The chain rule, one draw at a time: appending c to s multiplies its mass by the probability of drawing c after s.

theorem ProbabilityTheory.seqLaw_singleton {α : Type u_1} [MeasurableSpace α] {κ : (n : ℕ) → Kernel (Fin n → α) α} [MeasurableSingletonClass α] [∀ (n : ℕ), IsSFiniteKernel (κ n)] {n : ℕ} (x : Fin n → α) : (seqLaw κ n) {x} = ∏ i : Fin n, ((κ ↑i) (Fin.take ↑i ⋯ x)) {x i}

The chain rule: the mass of a sequence is the product of the probability of each draw given the draws before it.

The law as a partial trajectory

def Nat.iicEquivFin (n : ℕ) : ↥(Finset.Iic n) ≃ Fin (n + 1)

The times 0, …, n are the indices of the first n + 1 draws.

Equations

• n.iicEquivFin = { toFun := fun (i : ↥(Finset.Iic n)) => ⟨↑i, ⋯⟩, invFun := fun (j : Fin (n + 1)) => ⟨↑j, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

noncomputable def ProbabilityTheory.trajEquivFin {α : Type u_1} [MeasurableSpace α] (n : ℕ) : (↥(Finset.Iic n) → α) ≃ᵐ (Fin (n + 1) → α)

A trajectory up to time n as the sequence of its first n + 1 draws.

Equations

• ProbabilityTheory.trajEquivFin n = MeasurableEquiv.piCongrLeft (fun (x : Fin (n + 1)) => α) n.iicEquivFin

@[simp]

theorem ProbabilityTheory.trajEquivFin_apply {α : Type u_1} [MeasurableSpace α] (n : ℕ) (x : ↥(Finset.Iic n) → α) (j : Fin (n + 1)) : (trajEquivFin n) x j = x ⟨↑j, ⋯⟩

noncomputable def ProbabilityTheory.trajRule {α : Type u_1} [MeasurableSpace α] (κ : (n : ℕ) → Kernel (Fin n → α) α) (n : ℕ) : Kernel (↥(Finset.Iic n) → α) α

The prediction rule read on trajectories: after the draws at times 0, …, n, the law of the draw at time n + 1.

Equations

• ProbabilityTheory.trajRule κ n = (κ (n + 1)).comap ⇑(ProbabilityTheory.trajEquivFin n) ⋯

instance ProbabilityTheory.instIsMarkovKernelForallSubtypeNatMemFinsetIicTrajRule {α : Type u_1} [MeasurableSpace α] {κ : (n : ℕ) → Kernel (Fin n → α) α} [∀ (n : ℕ), IsMarkovKernel (κ n)] (n : ℕ) : IsMarkovKernel (trajRule κ n)

theorem ProbabilityTheory.seqLaw_succ_eq_map_partialTraj {α : Type u_1} [MeasurableSpace α] {κ : (n : ℕ) → Kernel (Fin n → α) α} [Countable α] [MeasurableSingletonClass α] [∀ (n : ℕ), IsMarkovKernel (κ n)] (n : ℕ) : seqLaw κ (n + 1) = MeasureTheory.Measure.map (⇑(trajEquivFin n)) ((MeasureTheory.Measure.map (fun (a : α) (x : ↥(Finset.Iic 0)) => a) ((κ 0) default)).bind ⇑(Kernel.partialTraj (trajRule κ) 0 n))

After the first draw, the next n draws of a prediction rule are the partial trajectory of the rule read on trajectories.

noncomputable def ProbabilityTheory.seqTrajectory {α : Type u_1} [MeasurableSpace α] (κ : (n : ℕ) → Kernel (Fin n → α) α) [∀ (n : ℕ), IsMarkovKernel (κ n)] : MeasureTheory.Measure (ℕ → α)

The law of the whole sequence of draws of the prediction rule κ: the Ionescu–Tulcea trajectory measure started at the first draw.

Equations

• ProbabilityTheory.seqTrajectory κ = ProbabilityTheory.Kernel.trajMeasure ((κ 0) default) (ProbabilityTheory.trajRule κ)

instance ProbabilityTheory.instIsProbabilityMeasureForallNatSeqTrajectory {α : Type u_1} [MeasurableSpace α] {κ : (n : ℕ) → Kernel (Fin n → α) α} [∀ (n : ℕ), IsMarkovKernel (κ n)] : MeasureTheory.IsProbabilityMeasure (seqTrajectory κ)

theorem ProbabilityTheory.seqTrajectory_map_frestrictLe {α : Type u_1} [MeasurableSpace α] {κ : (n : ℕ) → Kernel (Fin n → α) α} [Countable α] [MeasurableSingletonClass α] [∀ (n : ℕ), IsMarkovKernel (κ n)] (n : ℕ) : MeasureTheory.Measure.map (⇑(trajEquivFin n) ∘ Preorder.frestrictLe n) (seqTrajectory κ) = seqLaw κ (n + 1)

The first n + 1 draws of the whole sequence have the law of the first n + 1 draws.