Identification algorithms: sampling rule, stopping rule, output rule

An identification algorithm A : IdentAlg 𝓞 𝓐 𝓨 𝓓 with outputs in 𝓓 is a sampling rule A.alg : Algorithm 𝓞 𝓐 𝓨 together with

• a stopping rule A.stopSet, a measurable set of histories of variable length: the algorithm stops after n rounds if the history of these n rounds belongs to A.stopSet;
• an output rule A.output, a Markov kernel from histories of variable length to 𝓓: the distribution of the output given the history of the rounds played.

A run of the algorithm in an environment env, on a probability space (Ω, P), consists of observation, action and feedback processes O, X, Y forming an algorithm-environment sequence for A.alg and env (IsAlgEnvSeq) and an output out : Ω → 𝓓 whose conditional law given the history at the stopping time is the output rule (IdentAlg.IsRun).

The law of the output of a run is determined by A and env: it is A.outputMeasure env, see IdentAlg.IsRun.hasLaw_output. Properties of the algorithm are stated in terms of this law: A is PAC at level δ (IdentAlg.IsPAC) for a family of environments env θ and a badness predicate bad θ if, for every θ, the output in env θ is bad θ with probability at most δ.

Main definitions

• IdentAlg 𝓞 𝓐 𝓨 𝓓: the structure.
• IdentAlg.stoppingTime A O X Y : Ω → ℕ∞: the number of rounds played, a hitting time.
• IdentAlg.stoppedHist A O X Y : Ω → Σ n, Hist 𝓞 𝓐 𝓨 n: the history at the stopping time.
• IdentAlg.IsRun A env O X Y out P: (O, X, Y, out) is a run of A in env on (Ω, P).
• IdentAlg.outputMeasure A env : Measure 𝓓: the law of the output of A in env.
• IdentAlg.IsPAC A env bad δ: for every parameter θ, the output of A in env θ is bad θ with probability at most δ.

Time is 0-indexed: after n rounds the actions a_0, …, a_{n-1} have been played.

structure Learning.IdentAlg (𝓞 : Type u_6) (𝓐 : Type u_7) (𝓨 : Type u_8) (𝓓 : Type u_9) [MeasurableSpace 𝓞] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace 𝓓] : Type (max (max (max u_6 u_7) u_8) u_9)

An identification algorithm with outputs in 𝓓: a sampling rule alg, a stopping rule stopSet (the algorithm stops after n rounds if the history of these rounds belongs to stopSet) and an output rule output, a Markov kernel giving the distribution of the output given the history of the rounds played.

• alg : Algorithm 𝓞 𝓐 𝓨

  The sampling rule.

• stopSet : Set ((n : ℕ) × Hist 𝓞 𝓐 𝓨 n)

  The stopping rule: the algorithm stops after n rounds if the history of these rounds belongs to stopSet.

• measurableSet_stopSet : MeasurableSet self.stopSet

  The stopping rule is measurable.

• output : ProbabilityTheory.Kernel ((n : ℕ) × Hist 𝓞 𝓐 𝓨 n) 𝓓

  The output rule: distribution of the output given the history of the rounds played.

• isMarkovKernel_output : ProbabilityTheory.IsMarkovKernel self.output

  The output rule is a Markov kernel.

instance Learning.IdentAlg.instIsMarkovKernelSigmaNatHistOutput {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {𝓓 : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m𝓓 : MeasurableSpace 𝓓} {A : IdentAlg 𝓞 𝓐 𝓨 𝓓} : ProbabilityTheory.IsMarkovKernel A.output

noncomputable def Learning.IdentAlg.stoppingTime {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {𝓓 : Type u_4} {Ω : Type u_5} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m𝓓 : MeasurableSpace 𝓓} (A : IdentAlg 𝓞 𝓐 𝓨 𝓓) (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) : Ω → ℕ∞

The stopping time of A on the observation, action and feedback processes O, X, Y: the number of rounds played, that is the first n such that the history of the first n rounds belongs to the stopping rule A.stopSet (⊤ if there is none).

Equations

• A.stoppingTime O X Y = MeasureTheory.hittingAfter (Learning.sigmaHistory O X Y) A.stopSet 0

theorem Learning.IdentAlg.stoppingTime_def {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {𝓓 : Type u_4} {Ω : Type u_5} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m𝓓 : MeasurableSpace 𝓓} {O : ℕ → Ω → 𝓞} {X : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {A : IdentAlg 𝓞 𝓐 𝓨 𝓓} : A.stoppingTime O X Y = MeasureTheory.hittingAfter (sigmaHistory O X Y) A.stopSet 0

noncomputable def Learning.IdentAlg.stoppedHist {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {𝓓 : Type u_4} {Ω : Type u_5} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m𝓓 : MeasurableSpace 𝓓} (A : IdentAlg 𝓞 𝓐 𝓨 𝓓) (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) : Ω → (n : ℕ) × Hist 𝓞 𝓐 𝓨 n

The history of the rounds played by an identification algorithm A, as a history of variable length: the history stopped at A.stoppingTime O X Y (the history of an arbitrary number of rounds if A never stops).

Equations

• A.stoppedHist O X Y = MeasureTheory.stoppedValue (Learning.sigmaHistory O X Y) (A.stoppingTime O X Y)

theorem Learning.IdentAlg.stoppedHist_def {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {𝓓 : Type u_4} {Ω : Type u_5} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m𝓓 : MeasurableSpace 𝓓} {O : ℕ → Ω → 𝓞} {X : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {A : IdentAlg 𝓞 𝓐 𝓨 𝓓} : A.stoppedHist O X Y = MeasureTheory.stoppedValue (sigmaHistory O X Y) (A.stoppingTime O X Y)

noncomputable def Learning.IdentAlg.outputMeasure {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {𝓓 : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m𝓓 : MeasurableSpace 𝓓} (A : IdentAlg 𝓞 𝓐 𝓨 𝓓) (env : Environment 𝓞 𝓐 𝓨) : MeasureTheory.Measure 𝓓

The law of the output of an identification algorithm in an environment.

Equations

• A.outputMeasure env = (Learning.stoppedHistMeasure A.alg env A.stopSet).bind ⇑A.output

instance Learning.IdentAlg.instIsProbabilityMeasureOutputMeasure {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {𝓓 : Type u_1} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m𝓓 : MeasurableSpace 𝓓} (A : IdentAlg 𝓞 𝓐 𝓨 𝓓) (env : Environment 𝓞 𝓐 𝓨) : MeasureTheory.IsProbabilityMeasure (A.outputMeasure env)

structure Learning.IdentAlg.IsRun {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {𝓓 : Type u_4} {Ω : Type u_5} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m𝓓 : MeasurableSpace 𝓓} {mΩ : MeasurableSpace Ω} (A : IdentAlg 𝓞 𝓐 𝓨 𝓓) (env : Environment 𝓞 𝓐 𝓨) (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (out : Ω → 𝓓) (P : MeasureTheory.Measure Ω := by volume_tac) [MeasureTheory.IsFiniteMeasure P] : Prop

(O, X, Y, out) is a run of the identification algorithm A in the environment env on the probability space (Ω, P): the observation, action and feedback processes O, X, Y form an algorithm-environment sequence for the sampling rule A.alg and env, and the output out has conditional law A.output given the history at the stopping time.

• isAlgEnvSeq : IsAlgEnvSeq O X Y A.alg env P

  The actions and feedbacks are generated by the sampling rule in the environment.

• hasCondDistrib_output : ProbabilityTheory.HasCondDistrib out (A.stoppedHist O X Y) A.output P

  The output is drawn from the output rule applied to the history at the stopping time.

theorem Learning.IdentAlg.isStoppingTime_stoppingTime {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {𝓓 : Type u_4} {Ω : Type u_5} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m𝓓 : MeasurableSpace 𝓓} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {X : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} (A : IdentAlg 𝓞 𝓐 𝓨 𝓓) {alg : Algorithm 𝓞 𝓐 𝓨} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O X Y alg env P) : MeasureTheory.IsStoppingTime h.filtration (A.stoppingTime O X Y)

The stopping time of an identification algorithm A is a stopping time of the history filtration of any algorithm-environment sequence O, X, Y. Most often used with alg = A.alg.

theorem Learning.IdentAlg.stoppedHist_mem_stopSet_of_ne_top {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {𝓓 : Type u_4} {Ω : Type u_5} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m𝓓 : MeasurableSpace 𝓓} {O : ℕ → Ω → 𝓞} {X : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {A : IdentAlg 𝓞 𝓐 𝓨 𝓓} {ω : Ω} (h : A.stoppingTime O X Y ω ≠ ⊤) : A.stoppedHist O X Y ω ∈ A.stopSet

theorem Learning.IdentAlg.IsRun.hasLaw_stoppedHist {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {𝓓 : Type u_4} {Ω : Type u_5} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m𝓓 : MeasurableSpace 𝓓} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {X : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {A : IdentAlg 𝓞 𝓐 𝓨 𝓓} {env : Environment 𝓞 𝓐 𝓨} {out : Ω → 𝓓} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (h : A.IsRun env O X Y out P) : ProbabilityTheory.HasLaw (A.stoppedHist O X Y) (stoppedHistMeasure A.alg env A.stopSet) P

The history at the stopping time of any run of A in env has law stoppedHistMeasure A.alg env A.stopSet.

theorem Learning.IdentAlg.IsRun.hasLaw_output {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {𝓓 : Type u_4} {Ω : Type u_5} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m𝓓 : MeasurableSpace 𝓓} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {X : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {A : IdentAlg 𝓞 𝓐 𝓨 𝓓} {env : Environment 𝓞 𝓐 𝓨} {out : Ω → 𝓓} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (h : A.IsRun env O X Y out P) : ProbabilityTheory.HasLaw out (A.outputMeasure env) P

The output of any run of A in env has law A.outputMeasure env.

def Learning.IdentAlg.IsPAC {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {𝓓 : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m𝓓 : MeasurableSpace 𝓓} {Θ : Type u_6} (A : IdentAlg 𝓞 𝓐 𝓨 𝓓) (env : Θ → Environment 𝓞 𝓐 𝓨) (bad : Θ → 𝓓 → Prop) (δ : ℝ) : Prop

A is PAC at level δ for the family of environments env : Θ → Environment 𝓞 𝓐 𝓨 and the predicate bad : Θ → 𝓓 → Prop if, for every θ, the output of A in env θ is bad θ with probability at most δ. See IsPAC.measureReal_not_good_of_isRun for the corresponding statement about any run of A.

Equations

• A.IsPAC env bad δ = ∀ (θ : Θ), (A.outputMeasure (env θ)).real {d : 𝓓 | bad θ d} ≤ δ

theorem Learning.IdentAlg.IsPAC.measureReal_bad_of_isRun {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {𝓓 : Type u_4} {Ω : Type u_5} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m𝓓 : MeasurableSpace 𝓓} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {X : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {A : IdentAlg 𝓞 𝓐 𝓨 𝓓} {out : Ω → 𝓓} {P : MeasureTheory.Measure Ω} {Θ : Type u_6} {env : Θ → Environment 𝓞 𝓐 𝓨} {bad : Θ → 𝓓 → Prop} {δ : ℝ} [MeasureTheory.IsProbabilityMeasure P] (hA : A.IsPAC env bad δ) {θ : Θ} (hbad : MeasurableSet {d : 𝓓 | bad θ d}) (h : A.IsRun (env θ) O X Y out P) : P.real {ω : Ω | bad θ (out ω)} ≤ δ

For a PAC algorithm at level δ, the output of any run in env θ is bad θ with probability at most δ.