LeanMachineLearning exposition

Learning.Algorithm.«term_≪ₐ_»🔗

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

term_≪ₐ_🔗

DefinitionLearning.Algorithm.«term_≪ₐ_»
Details

For every time and history, the distribution over actions according to alg is absolutely continuous with respect to the distribution over actions according to alg₀.

🔗def
Learning.Algorithm.«term_≪ₐ_» : Lean.TrailingParserDescr
Learning.Algorithm.«term_≪ₐ_» :
  Lean.TrailingParserDescr

Code

scoped notation:50 alg " ≪ₐ " alg₀ => AbsolutelyContinuous alg alg₀
Body uses (1)

Actions: Source · Open Issue

Dependency graph

All dependencies, transitively (2)

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

AbsolutelyContinuous🔗

StructureLearning.Algorithm.AbsolutelyContinuous
Details

For every time and history, the distribution over actions according to alg is absolutely continuous with respect to the distribution over actions according to alg₀.

🔗structure
Learning.Algorithm.AbsolutelyContinuous.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} [MeasurableSpace 𝓐] [MeasurableSpace 𝓨]
  (alg alg₀ : Algorithm 𝓐 𝓨) : Prop
Learning.Algorithm.AbsolutelyContinuous.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  [MeasurableSpace 𝓐] [MeasurableSpace 𝓨]
  (alg alg₀ : Algorithm 𝓐 𝓨) : Prop

Code

structure AbsolutelyContinuous (alg alg₀ : Algorithm 𝓐 𝓨) : Prop where
  p0 : alg.p0 ≪ alg₀.p0
  policy n h : alg.policy n h ≪ alg₀.policy n h
Type uses (1)
Used by (7)

Actions: Source · Open Issue