Stopping rules and stopped histories

A stopping rule is a measurable set S : Set (Σ n, Hist 𝓞 𝓐 𝓨 n) of histories of variable length: the interaction stops after n rounds if the history of these n rounds belongs to S.

Main definitions

• Learning.sigmaHistory O X Y n : Ω → Σ n, Hist 𝓞 𝓐 𝓨 n: the history of the first n rounds, as a history of variable length;
• stoppedHistMeasure alg env S: the law of the history stopped by S.

Main results

• IsAlgEnvSeq.hasLaw_stoppedHist_stoppingTime: the law of the history stopped by S is determined by the algorithm and the environment.

def Learning.sigmaHistory {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (n : ℕ) (ω : Ω) : (n : ℕ) × Hist 𝓞 𝓐 𝓨 n

The history of the first n rounds, as a history of variable length in the sigma type Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n.

Equations

• Learning.sigmaHistory O X Y n ω = ⟨n, Learning.history O X Y n ω⟩

theorem Learning.sigmaHistory_apply {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {O : ℕ → Ω → 𝓞} {X : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (n : ℕ) (ω : Ω) : sigmaHistory O X Y n ω = ⟨n, history O X Y n ω⟩

@[simp]

theorem Learning.fst_sigmaHistory {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {O : ℕ → Ω → 𝓞} {X : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (n : ℕ) (ω : Ω) : (sigmaHistory O X Y n ω).fst = n

theorem Learning.measurable_sigmaHistory {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {X : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (hO : ∀ (n : ℕ), Measurable (O n)) (hX : ∀ (n : ℕ), Measurable (X n)) (hY : ∀ (n : ℕ), Measurable (Y n)) (n : ℕ) : Measurable (sigmaHistory O X Y n)

theorem Learning.measurable_hittingAfter_sigmaHistory {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {X : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {S : Set ((n : ℕ) × Hist 𝓞 𝓐 𝓨 n)} (hO : ∀ (n : ℕ), Measurable (O n)) (hX : ∀ (n : ℕ), Measurable (X n)) (hY : ∀ (n : ℕ), Measurable (Y n)) (hS : MeasurableSet S) : Measurable (MeasureTheory.hittingAfter (sigmaHistory O X Y) S 0)

theorem Learning.measurable_stoppedValue_sigmaHistory {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {X : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {τ : Ω → WithTop ℕ} (hO : ∀ (n : ℕ), Measurable (O n)) (hX : ∀ (n : ℕ), Measurable (X n)) (hY : ∀ (n : ℕ), Measurable (Y n)) (hτ : Measurable τ) : Measurable (MeasureTheory.stoppedValue (sigmaHistory O X Y) τ)

theorem Learning.IsAlgEnvSeq.adapted_sigmaHistory {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {X : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O X Y alg env P) : MeasureTheory.Adapted h.filtration (sigmaHistory O X Y)

The law of the stopped history

The stopping time and the stopped history are functions of the trajectory, whose law is determined by the algorithm and the environment (IsAlgEnvSeq.hasLaw_trajectory). Hence the law of the stopped history is determined by the algorithm and the environment: it is the law stoppedHistMeasure alg env S of the stopped history on the canonical space trajMeasure.

noncomputable def Learning.stoppedHistMeasure {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) (S : Set ((n : ℕ) × Hist 𝓞 𝓐 𝓨 n)) : MeasureTheory.Measure ((n : ℕ) × Hist 𝓞 𝓐 𝓨 n)

The law of the history stopped by the stopping rule S, for the algorithm alg in the environment env: the law of the stopped history on the canonical space trajMeasure alg env. This is the law of the stopped history for any algorithm-environment sequence (IsAlgEnvSeq.hasLaw_stoppedValue_sigmaHistory).

Equations

• One or more equations did not get rendered due to their size.

instance Learning.instIsProbabilityMeasureSigmaNatHistStoppedHistMeasure {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) (S : Set ((n : ℕ) × Hist 𝓞 𝓐 𝓨 n)) : MeasureTheory.IsProbabilityMeasure (stoppedHistMeasure alg env S)

theorem Learning.IsAlgEnvSeq.hasLaw_stoppedValue_sigmaHistory {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {O : ℕ → Ω → 𝓞} {X : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {S : Set ((n : ℕ) × Hist 𝓞 𝓐 𝓨 n)} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (h : IsAlgEnvSeq O X Y alg env P) (hS : MeasurableSet S) : ProbabilityTheory.HasLaw (MeasureTheory.stoppedValue (sigmaHistory O X Y) (MeasureTheory.hittingAfter (sigmaHistory O X Y) S 0)) (stoppedHistMeasure alg env S) P

The law of the history stopped by S under any algorithm-environment sequence for alg and env is stoppedHistMeasure alg env S.