Autoregressive sequence models

An autoregressive sequence model over an alphabet α gives, after every prefix, a distribution over the next symbol or the end of the string, none [DTHP+23]. The prefix probability of a string is the product of the conditional probabilities along it, and the probability of the string itself multiplies in the probability of ending after it. The string probabilities need not sum to one: the remaining mass leaks to sequences that never end. A model is tight when they do.

Tightness is a statement about survival, the probability that no end symbol appears in the first n steps. The probabilities of the strings shorter than n and the survival at n sum to one, so a model is tight exactly when survival tends to zero. Survival is the product of one minus the end probability at each step given survival to it, so a model is tight exactly when that conditional end probability reaches one or has a divergent sum; an end probability bounded below by a divergent series suffices.

The model is a prediction rule on the extended alphabet, the end of the string absorbing, and the Ionescu–Tulcea theorem gives the law of its whole trajectory, a probability measure on infinite sequences of units or ends. Survival is the probability that none of the first n units is the end, a string's probability is that of the trajectories that spell it and then end, and the model is tight exactly when the trajectory ends almost surely, which is how [DTHP+23] define tightness.

Main definitions

• AutoregressiveSequenceModel α: a Markov kernel from prefixes to Option α.
• condPrefixProb, prefixProb, stringProb, stringMeasure.
• IsTight: the string probabilities sum to one.
• survival, stopProb, eosHazard.
• after: the model after a context.
• rule, trajectory: the model as a prediction rule on the extended alphabet, and the law of its whole trajectory.

Main results

• condPrefixProb_append: the chain rule for prefix probabilities.
• sum_range_stopProb_add_survival, isTight_iff_tendsto_survival.
• survival_eq_prod: survival is a product over the conditional end probabilities.
• isTight_iff: tight exactly when the conditional end probability reaches one or has a divergent sum ([DTHP+23], Theorem 4.7).
• isTight_of_le_next_none: a divergent lower bound on the end probability gives tightness ([DTHP+23], Proposition 4.3).
• survival_le_pow: a constant lower bound makes survival decay geometrically.
• isTight_iff_of_next_none_eq: the criterion when the end probability depends only on length.
• stringMeasure_setOf_length_le, IsTight.stringMeasure_setOf_length_le: survival is at least, and in a tight model exactly, the probability of a string of at least that length.
• lintegral_length_le, IsTight.lintegral_length, lintegral_length_le_div: the expected length is at most, and in a tight model exactly, the total survival after the first step, and at most (1 - c) / c under an end probability of at least c.
• IsTight.tsum_prefixProb: in a tight model the prefix probabilities sum to the expected length plus one ([OCCW24]).
• trajectory_setOf_forall_lt_ne_none, trajectory_cylinder: survival and string probabilities as probabilities of the trajectory.
• isTight_iff_trajectory_setOf_forall_ne_none: tight exactly when the trajectory ends almost surely ([DTHP+23]'s definition).
• stringProb_append, IsTight.after, IsTight.stringMeasure_setOf_prefix: a string's probability factors through the model after its prefix, which inherits tightness, so in a tight model the strings extending a prefix have total probability its prefix probability.

Implementation notes

• The alphabet need only be countable with measurable singletons; [DTHP+23] take it finite.
• The product criterion behind isTight_iff is ENNReal.tendsto_prod_range_one_sub_nhds_zero_iff, [DTHP+23]'s Corollary 4.6 extended to factors that may vanish.
• [DTHP+23] count steps from one, so their conditional end probability at step t is eosHazard (t - 1). Where survival is zero the ratio is 0 by the convention of ℝ≥0∞ division; the characterization is unaffected, since survival first reaching zero forces a conditional end probability of one.
• [DTHP+23] define tightness as zero mass on the infinite sequences under the trajectory measure; IsTight is the equivalent condition that the string probabilities sum to one, and isTight_iff_trajectory_setOf_forall_ne_none is the equivalence.

References

• [DTHP+23]
• [OCCW24]

structure AutoregressiveSequenceModel (α : Type u_1) [MeasurableSpace α] : Type u_1

An autoregressive sequence model over the alphabet α: after each prefix, a distribution over the next symbol, or the end of the string, none.

• next : ProbabilityTheory.Kernel (List α) (Option α)

  The distribution of what follows a prefix.

• isMarkovKernel_next : ProbabilityTheory.IsMarkovKernel self.next

Prefix and string probabilities

noncomputable def AutoregressiveSequenceModel.condPrefixProb {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) : List α → List α → ENNReal

The probability that the continuation of the context c begins with x: the product of the conditional probabilities along x.

Equations

• M.condPrefixProb x✝ [] = 1
• M.condPrefixProb x✝ (a :: x_2) = (M.next x✝) {some a} * M.condPrefixProb (x✝ ++ [a]) x_2

@[simp]

theorem AutoregressiveSequenceModel.condPrefixProb_nil {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) (c : List α) : M.condPrefixProb c [] = 1

@[simp]

theorem AutoregressiveSequenceModel.condPrefixProb_cons {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) (c : List α) (a : α) (x : List α) : M.condPrefixProb c (a :: x) = (M.next c) {some a} * M.condPrefixProb (c ++ [a]) x

theorem AutoregressiveSequenceModel.condPrefixProb_append {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) (c x y : List α) : M.condPrefixProb c (x ++ y) = M.condPrefixProb c x * M.condPrefixProb (c ++ x) y

The chain rule: a continuation begins with x ++ y when it begins with x and the continuation of c ++ x begins with y.

noncomputable def AutoregressiveSequenceModel.prefixProb {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) (x : List α) : ENNReal

The prefix probability of x: the probability that a generated string begins with x.

Equations

• M.prefixProb x = M.condPrefixProb [] x

@[simp]

theorem AutoregressiveSequenceModel.prefixProb_nil {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) : M.prefixProb [] = 1

theorem AutoregressiveSequenceModel.prefixProb_concat {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) (x : List α) (a : α) : M.prefixProb (x ++ [a]) = M.prefixProb x * (M.next x) {some a}

noncomputable def AutoregressiveSequenceModel.stringProb {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) (x : List α) : ENNReal

The probability of generating exactly x: its prefix probability times the probability of ending after it.

Equations

• M.stringProb x = M.prefixProb x * (M.next x) {none}

noncomputable def AutoregressiveSequenceModel.stringMeasure {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) : MeasureTheory.Measure (List α)

The law of the generated string, carried by the finite strings.

Equations

• M.stringMeasure = MeasureTheory.Measure.sum fun (x : List α) => M.stringProb x • MeasureTheory.Measure.dirac x

@[simp]

theorem AutoregressiveSequenceModel.stringMeasure_singleton {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) (x : List α) : M.stringMeasure {x} = M.stringProb x

theorem AutoregressiveSequenceModel.stringMeasure_univ {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) : M.stringMeasure Set.univ = ∑' (x : List α), M.stringProb x

theorem AutoregressiveSequenceModel.lintegral_stringMeasure {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) (f : List α → ENNReal) : ∫⁻ (x : List α), f x ∂M.stringMeasure = ∑' (x : List α), M.stringProb x * f x

An integral against the law of the string is a sum weighted by the string probabilities.

def AutoregressiveSequenceModel.IsTight {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) : Prop

A model is tight when its string probabilities sum to one: no mass leaks to sequences that never end.

Equations

• M.IsTight = (∑' (x : List α), M.stringProb x = 1)

theorem AutoregressiveSequenceModel.isTight_iff_isProbabilityMeasure {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) : M.IsTight ↔ MeasureTheory.IsProbabilityMeasure M.stringMeasure

Continuations

noncomputable def AutoregressiveSequenceModel.after {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) (c : List α) : AutoregressiveSequenceModel α

The model after the context c: after each prefix u it continues as the model does after c ++ u.

Equations

• M.after c = { next := M.next.comap (fun (x : List α) => c ++ x) ⋯, isMarkovKernel_next := ⋯ }

@[simp]

theorem AutoregressiveSequenceModel.next_after {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) (c u : List α) : (M.after c).next u = M.next (c ++ u)

theorem AutoregressiveSequenceModel.condPrefixProb_append_left {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) (c c' z : List α) : M.condPrefixProb (c ++ c') z = (M.after c).condPrefixProb c' z

theorem AutoregressiveSequenceModel.prefixProb_after {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) (c z : List α) : (M.after c).prefixProb z = M.condPrefixProb c z

theorem AutoregressiveSequenceModel.prefixProb_append {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) (x z : List α) : M.prefixProb (x ++ z) = M.prefixProb x * (M.after x).prefixProb z

theorem AutoregressiveSequenceModel.stringProb_append {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) (x z : List α) : M.stringProb (x ++ z) = M.prefixProb x * (M.after x).stringProb z

theorem AutoregressiveSequenceModel.condPrefixProb_le_one {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) (c x : List α) : M.condPrefixProb c x ≤ 1

theorem AutoregressiveSequenceModel.prefixProb_ne_top {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) (x : List α) : M.prefixProb x ≠ ⊤

theorem AutoregressiveSequenceModel.condPrefixProb_ne_zero {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) (h : ∀ (c : List α) (a : α), (M.next c) {some a} ≠ 0) (c x : List α) : M.condPrefixProb c x ≠ 0

A model whose every continuation has positive probability gives every prefix positive probability.

theorem AutoregressiveSequenceModel.stringMeasure_setOf_prefix {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) (x : List α) : M.stringMeasure {y : List α | x <+: y} = M.prefixProb x * ∑' (z : List α), (M.after x).stringProb z

The strings extending x have total probability the prefix probability of x times the total probability of the model after x.

Survival

noncomputable def AutoregressiveSequenceModel.survival {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) (n : ℕ) : ENNReal

The probability that no end symbol appears in the first n steps: the total prefix probability of the strings of length n.

Equations

• M.survival n = ∑' (x : { x : List α // x.length = n }), M.prefixProb ↑x

noncomputable def AutoregressiveSequenceModel.stopProb {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) (n : ℕ) : ENNReal

The probability of generating a string of length n.

Equations

• M.stopProb n = ∑' (x : { x : List α // x.length = n }), M.stringProb ↑x

noncomputable def AutoregressiveSequenceModel.eosHazard {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) (n : ℕ) : ENNReal

The probability of ending after n symbols given survival to that point, the end probability at step n + 1 of [DTHP+23].

Equations

• M.eosHazard n = M.stopProb n / M.survival n

@[simp]

theorem AutoregressiveSequenceModel.survival_zero {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) : M.survival 0 = 1

theorem AutoregressiveSequenceModel.tsum_stringProb {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) : ∑' (x : List α), M.stringProb x = ∑' (n : ℕ), M.stopProb n

theorem AutoregressiveSequenceModel.measurableSet_setOf_forall_lt_ne_none {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (n : ℕ) : MeasurableSet {ω : ℕ → Option α | ∀ i < n, ω i ≠ none}

theorem AutoregressiveSequenceModel.next_none_add_tsum_next_some {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] (x : List α) : (M.next x) {none} + ∑' (a : α), (M.next x) {some a} = 1

After any prefix the model either ends or continues with some symbol.

theorem AutoregressiveSequenceModel.survival_succ_add_stopProb {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] (n : ℕ) : M.survival (n + 1) + M.stopProb n = M.survival n

theorem AutoregressiveSequenceModel.sum_range_stopProb_add_survival {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] (n : ℕ) : ∑ k ∈ Finset.range n, M.stopProb k + M.survival n = 1

theorem AutoregressiveSequenceModel.survival_le_one {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] (n : ℕ) : M.survival n ≤ 1

theorem AutoregressiveSequenceModel.survival_ne_top {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] (n : ℕ) : M.survival n ≠ ⊤

theorem AutoregressiveSequenceModel.stopProb_le_survival {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] (n : ℕ) : M.stopProb n ≤ M.survival n

theorem AutoregressiveSequenceModel.survival_antitone {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] : Antitone M.survival

theorem AutoregressiveSequenceModel.isTight_iff_tendsto_survival {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] : M.IsTight ↔ Filter.Tendsto M.survival Filter.atTop (nhds 0)

The conditional end probability

theorem AutoregressiveSequenceModel.eosHazard_le_one {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] (n : ℕ) : M.eosHazard n ≤ 1

theorem AutoregressiveSequenceModel.survival_succ {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] (n : ℕ) : M.survival (n + 1) = M.survival n * (1 - M.eosHazard n)

theorem AutoregressiveSequenceModel.survival_eq_prod {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] (n : ℕ) : M.survival n = ∏ k ∈ Finset.range n, (1 - M.eosHazard k)

theorem AutoregressiveSequenceModel.isTight_iff {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] : M.IsTight ↔ (∃ (n : ℕ), M.eosHazard n = 1) ∨ ∑' (n : ℕ), M.eosHazard n = ⊤

A model is tight exactly when the conditional end probability reaches one or has a divergent sum ([DTHP+23], Theorem 4.7).

theorem AutoregressiveSequenceModel.mul_survival_le_stopProb {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) {n : ℕ} {c : ENNReal} (hc : ∀ (x : List α), x.length = n → c ≤ (M.next x) {none}) : c * M.survival n ≤ M.stopProb n

The strings of length n end with probability at least c times survival to n when every prefix of length n ends with probability at least c.

theorem AutoregressiveSequenceModel.isTight_of_le_next_none {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] {f : ℕ → ENNReal} (hf : ∀ (x : List α), f (x.length + 1) ≤ (M.next x) {none}) (h : ∑' (t : ℕ), f (t + 1) = ⊤) : M.IsTight

A model whose end probability after every prefix of length t - 1 is at least f t, for a divergent series of bounds, is tight ([DTHP+23], Proposition 4.3).

theorem AutoregressiveSequenceModel.survival_eq_prod_of_next_none_eq {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] {e : ℕ → ENNReal} (he : ∀ (x : List α), (M.next x) {none} = e x.length) (n : ℕ) : M.survival n = ∏ k ∈ Finset.range n, (1 - e k)

When the end probability after a prefix depends only on its length, survival is the product of one minus it.

theorem AutoregressiveSequenceModel.isTight_iff_of_next_none_eq {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] {e : ℕ → ENNReal} (he : ∀ (x : List α), (M.next x) {none} = e x.length) (he1 : ∀ (n : ℕ), e n ≤ 1) : M.IsTight ↔ (∃ (n : ℕ), e n = 1) ∨ ∑' (n : ℕ), e n = ⊤

When the end probability after a prefix depends only on its length, the model is tight exactly when that probability reaches one or has a divergent sum.

theorem AutoregressiveSequenceModel.survival_le_pow {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] {c : ENNReal} (hc : ∀ (x : List α), c ≤ (M.next x) {none}) (n : ℕ) : M.survival n ≤ (1 - c) ^ n

An end probability of at least c after every prefix makes survival decay geometrically.

theorem AutoregressiveSequenceModel.tsum_stringProb_le_one {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] : ∑' (x : List α), M.stringProb x ≤ 1

The string probabilities of any model sum to at most one.

theorem AutoregressiveSequenceModel.prefixProb_mul_survival_after_le {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) (x : List α) (n : ℕ) : M.prefixProb x * (M.after x).survival n ≤ M.survival (n + x.length)

Surviving n steps after x is surviving n + |x| steps through x.

theorem AutoregressiveSequenceModel.IsTight.after {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Countable α] {M : AutoregressiveSequenceModel α} (hM : M.IsTight) {x : List α} (hx : M.prefixProb x ≠ 0) : (M.after x).IsTight

The model after a prefix of positive probability inherits tightness.

theorem AutoregressiveSequenceModel.IsTight.stringMeasure_setOf_prefix {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Countable α] {M : AutoregressiveSequenceModel α} (hM : M.IsTight) (x : List α) : M.stringMeasure {y : List α | x <+: y} = M.prefixProb x

In a tight model the strings extending x have total probability its prefix probability.

Expected length

The law of the generated string is a sum of point masses, so an integral against it is a sum weighted by the string probabilities. Survival to n is at least the probability of a string of length at least n, with equality in a tight model, so the tail-sum formula bounds the expected length by the total survival after the first step.

theorem AutoregressiveSequenceModel.stringMeasure_setOf_length_le {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] (n : ℕ) : M.stringMeasure {y : List α | n ≤ y.length} ≤ M.survival n

Survival to n is at least the probability of a string of length at least n.

theorem AutoregressiveSequenceModel.IsTight.stringMeasure_setOf_length_le {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Countable α] {M : AutoregressiveSequenceModel α} (hM : M.IsTight) (n : ℕ) : M.stringMeasure {y : List α | n ≤ y.length} = M.survival n

In a tight model survival to n is the probability of a string of length at least n.

theorem AutoregressiveSequenceModel.lintegral_length_le {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] : ∫⁻ (x : List α), ↑x.length ∂M.stringMeasure ≤ ∑' (n : ℕ), M.survival (n + 1)

The expected length of the generated string is at most the total survival after the first step.

theorem AutoregressiveSequenceModel.IsTight.lintegral_length {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Countable α] {M : AutoregressiveSequenceModel α} (hM : M.IsTight) : ∫⁻ (x : List α), ↑x.length ∂M.stringMeasure = ∑' (n : ℕ), M.survival (n + 1)

In a tight model the expected length is the total survival after the first step.

theorem AutoregressiveSequenceModel.IsTight.tsum_prefixProb {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Countable α] {M : AutoregressiveSequenceModel α} (hM : M.IsTight) : ∑' (x : List α), M.prefixProb x = ∫⁻ (x : List α), ↑x.length + 1 ∂M.stringMeasure

In a tight model the prefix probabilities sum to the expected length plus one, the normalizing constant of the prefix distribution ([OCCW24], Proposition 1).

theorem AutoregressiveSequenceModel.lintegral_length_le_div {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] {c : ENNReal} (hc : ∀ (x : List α), c ≤ (M.next x) {none}) : ∫⁻ (x : List α), ↑x.length ∂M.stringMeasure ≤ (1 - c) / c

An end probability of at least c after every prefix bounds the expected length by (1 - c) / c.

The trajectory

The model is a prediction rule on the extended alphabet, with the end absorbing, and the law of its whole trajectory is the Ionescu–Tulcea trajectory measure of that rule.

noncomputable def AutoregressiveSequenceModel.rule {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] (n : ℕ) : ProbabilityTheory.Kernel (Fin n → Option α) (Option α)

The model as a prediction rule on the extended alphabet: after a history of units it draws the next unit, and after the end of the string it stays at the end.

Equations

• M.rule n = ProbabilityTheory.Kernel.ofFunOfCountable fun (h : Fin n → Option α) => if ∀ (i : Fin n), h i ≠ none then M.next (List.ofFn h).reduceOption else MeasureTheory.Measure.dirac none

instance AutoregressiveSequenceModel.instIsMarkovKernelForallFinOptionRule {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] (n : ℕ) : ProbabilityTheory.IsMarkovKernel (M.rule n)

theorem AutoregressiveSequenceModel.rule_apply_some {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] {n : ℕ} (f : Fin n → α) : (M.rule n) (some ∘ f) = M.next (List.ofFn f)

After a history of units the rule is the model's next-unit distribution.

theorem AutoregressiveSequenceModel.seqLaw_rule_singleton_some {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] {n : ℕ} (f : Fin n → α) : (ProbabilityTheory.seqLaw M.rule n) {some ∘ f} = M.prefixProb (List.ofFn f)

The mass of a history of units is its prefix probability.

theorem AutoregressiveSequenceModel.survival_eq_seqLaw {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] (n : ℕ) : M.survival n = (ProbabilityTheory.seqLaw M.rule n) {h : Fin n → Option α | ∀ (i : Fin n), h i ≠ none}

Survival to n is the law of the first n draws on the histories of units.

noncomputable def AutoregressiveSequenceModel.trajectory {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] : MeasureTheory.Measure (ℕ → Option α)

The law of the whole trajectory of the model: the units it generates one after another, with the end of the string absorbing.

Equations

• M.trajectory = ProbabilityTheory.seqTrajectory M.rule

instance AutoregressiveSequenceModel.instIsProbabilityMeasureForallNatOptionTrajectory {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] : MeasureTheory.IsProbabilityMeasure M.trajectory

theorem AutoregressiveSequenceModel.trajectory_setOf_forall_lt_ne_none {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] (n : ℕ) : M.trajectory {ω : ℕ → Option α | ∀ i < n, ω i ≠ none} = M.survival n

Survival to n is the probability that none of the first n units is the end.

theorem AutoregressiveSequenceModel.trajectory_setOf_forall_ne_none {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] : M.trajectory {ω : ℕ → Option α | ∀ (i : ℕ), ω i ≠ none} = ⨅ (n : ℕ), M.survival n

The probability that the string never ends is the infimum of survival.

theorem AutoregressiveSequenceModel.isTight_iff_trajectory_setOf_forall_ne_none {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] : M.IsTight ↔ M.trajectory {ω : ℕ → Option α | ∀ (i : ℕ), ω i ≠ none} = 0

A model is tight exactly when its trajectory ends almost surely, [DTHP+23]'s definition of tightness.

theorem AutoregressiveSequenceModel.trajectory_cylinder {α : Type u_1} [MeasurableSpace α] (M : AutoregressiveSequenceModel α) [MeasurableSingletonClass α] [Countable α] {n : ℕ} (f : Fin n → α) : M.trajectory {ω : ℕ → Option α | (∀ (i : Fin n), ω ↑i = some (f i)) ∧ ω n = none} = M.stringProb (List.ofFn f)

The probability of generating exactly the string List.ofFn f is the probability that the trajectory begins with its units and then ends.