LeanMachineLearning exposition

3.10. SequentialLearning.Algorithms.Uniform🔗

The Uniform algorithm

An algorithm that chooses actions uniformly at random in every situation.

Main definitions

  • uniformAlgorithm: a uniform algorithm with actions in a finite non-empty type 𝓐.

Main results

  • absolutelyContinuous_uniformAlgorithm: every algorithm with actions in 𝓐 is absolutely continuous with respect to the uniform algorithm with the same type of feedback.

Module LeanMachineLearning.SequentialLearning.Algorithms.Uniform contains 2 exposed declarations.

uniformAlgorithm🔗

DefinitionLearning.uniformAlgorithm
Details

The Uniform algorithm: actions are chosen uniformly at random.

🔗def
Learning.uniformAlgorithm.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [Finite 𝓐]
  [Nonempty 𝓐] : Algorithm 𝓐 𝓨
Learning.uniformAlgorithm.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} [Finite 𝓐]
  [Nonempty 𝓐] : Algorithm 𝓐 𝓨

Code

noncomputable
def uniformAlgorithm [Finite 𝓐] [Nonempty 𝓐] : Algorithm 𝓐 𝓨 := randomSampling (uniformOn Set.univ)
Type uses (1)
Body uses (1)
Used by (4)

Actions: Source · Open Issue

absolutelyContinuous_uniformAlgorithm🔗

LemmaLearning.absolutelyContinuous_uniformAlgorithm
Details

No docstring.

🔗theorem
Learning.absolutelyContinuous_uniformAlgorithm.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  [Finite 𝓐] [Nonempty 𝓐] {alg : Algorithm 𝓐 𝓨} :
  Algorithm.AbsolutelyContinuous alg uniformAlgorithm
Learning.absolutelyContinuous_uniformAlgorithm.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} [Finite 𝓐]
  [Nonempty 𝓐] {alg : Algorithm 𝓐 𝓨} :
  Algorithm.AbsolutelyContinuous alg
    uniformAlgorithm

Code

lemma absolutelyContinuous_uniformAlgorithm [Finite 𝓐] [Nonempty 𝓐] {alg : Algorithm 𝓐 𝓨} :
    alg ≪ₐ uniformAlgorithm where
  p0
Type uses (3)
Body uses (3)
Used by (1)

Actions: Source · Open Issue

Proof
Measure.absolutelyContinuous_of_measure_singleton_ne_zero
    (by simp [uniformAlgorithm, uniformOn, ← pos_iff_ne_zero, cond_pos_of_inter_ne_zero])
  policy n h := Measure.absolutelyContinuous_of_measure_singleton_ne_zero
    (by simp [uniformAlgorithm, uniformOn, ← pos_iff_ne_zero, cond_pos_of_inter_ne_zero])
  1. Learning.uniformAlgorithm
  2. Learning.absolutelyContinuous_uniformAlgorithm