`Learning.uniformAlgorithm`🔗

This page has the declaration's own card below, then its dependency graph, then a card for each dependency (type dependencies first, then the rest of the transitive closure). For a theorem, the graph and the dependency cards only follow its statement's dependencies (its proof is replaced by sorry, so what it proves doesn't depend on how); for everything else, both the type and the body/value are followed, since their content is part of what later declarations build on.

Minimal Lean file

`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)

Algorithm

Body uses (1)

randomSampling

Used by (4)

Actions: Source · Open Issue

Dependency graph

Type dependencies (1)

`Algorithm`🔗

StructureLearning.Algorithm

Details

A stochastic, sequential algorithm.

structure

Learning.Algorithm.{u_4, u_5} (𝓐 : Type u_4) (𝓨 : Type u_5)
  [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] : Type (max u_4 u_5)
Learning.Algorithm.{u_4, u_5}
  (𝓐 : Type u_4) (𝓨 : Type u_5)
  [MeasurableSpace 𝓐]
  [MeasurableSpace 𝓨] : Type (max u_4 u_5)

Code

structure Algorithm (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] where
  /-- Policy or sampling rule: distribution of the next action. -/
  policy : (n : ℕ) → Kernel (Iic n → 𝓐 × 𝓨) 𝓐
  /-- The policy is a Markov kernel. -/
  [h_policy : ∀ n, IsMarkovKernel (policy n)]
  /-- Distribution of the first action. -/
  p0 : Measure 𝓐
  /-- The first action distribution is a probability measure. -/
  [hp0 : IsProbabilityMeasure p0]

Used by (216)

Actions: Source · Open Issue

All dependencies, transitively (1)

`randomSampling`🔗

DefinitionLearning.randomSampling

Details

The Random Sampling algorithm, which samples from a fixed probability measure at each iteration.

def

Learning.randomSampling.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (μ : MeasureTheory.Measure 𝓐) [MeasureTheory.IsProbabilityMeasure μ] :
  Algorithm 𝓐 𝓨
Learning.randomSampling.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  (μ : MeasureTheory.Measure 𝓐)
  [MeasureTheory.IsProbabilityMeasure μ] :
  Algorithm 𝓐 𝓨

Code

noncomputable def randomSampling (μ : Measure 𝓐) [IsProbabilityMeasure μ] : Algorithm 𝓐 𝓨 where
  policy _ := Kernel.const _ μ
  p0 := μ

Type uses (1)

Algorithm

Used by (5)

Actions: Source · Open Issue

Learning.uniformAlgorithm🔗

uniformAlgorithm🔗

Algorithm🔗

randomSampling🔗

`Learning.uniformAlgorithm`🔗

`uniformAlgorithm`🔗

`Algorithm`🔗

`randomSampling`🔗