Learning.absolutelyContinuous_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.
absolutelyContinuous_uniformAlgorithmπ
Learning.absolutelyContinuous_uniformAlgorithmNo docstring.
Learning.absolutelyContinuous_uniformAlgorithm.{u_1, u_2} {π : Type u_1} {π¨ : Type u_2} {mπ : MeasurableSpace π} {mπ¨ : MeasurableSpace π¨} [Finite π] [Nonempty π] {alg : Algorithm π π¨} : Algorithm.AbsolutelyContinuous alg uniformAlgorithmLearning.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
p0Type 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])Dependency graph
Type dependencies (3)
Algorithmπ
Learning.AlgorithmA stochastic, sequential algorithm.
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π
Learning.Algorithm.AbsolutelyContinuous
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β.
Learning.Algorithm.AbsolutelyContinuous.{u_1, u_2} {π : Type u_1} {π¨ : Type u_2} [MeasurableSpace π] [MeasurableSpace π¨] (alg algβ : Algorithm π π¨) : PropLearning.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
uniformAlgorithmπ
Learning.uniformAlgorithmThe Uniform algorithm: actions are chosen uniformly at random.
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
All dependencies, transitively (1)
randomSamplingπ
Learning.randomSamplingThe Random Sampling algorithm, which samples from a fixed probability measure at each iteration.
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)
Actions: Source Β· Open Issue