Random Sampling #
Implementation of the Random Sampling algorithm, which samples from a fixed probability measure at each iteration.
Main definitions #
randomSampling: The random sampling algorithm that samples from a fixed distribution at each iteration.
Main statements #
hasLaw_action: Each action follows the distribution ΞΌ.iIndep_action: Actions are mutually independent across time steps.
noncomputable def
Learning.randomSampling
{π : Type u_1}
{π¨ : Type u_2}
[MeasurableSpace π]
[MeasurableSpace π¨]
(ΞΌ : MeasureTheory.Measure π)
[MeasureTheory.IsProbabilityMeasure ΞΌ]
:
Algorithm π π¨
The Random Sampling algorithm, which samples from a fixed probability measure at each iteration.
Equations
- Learning.randomSampling ΞΌ = { policy := fun (x : β) => ProbabilityTheory.Kernel.const (β₯(Finset.Iic x) β π Γ π¨) ΞΌ, h_policy := β―, p0 := ΞΌ, hp0 := instβ }
Instances For
@[simp]
theorem
Learning.randomSampling_p0
{π : Type u_1}
{π¨ : Type u_2}
[MeasurableSpace π]
[MeasurableSpace π¨]
(ΞΌ : MeasureTheory.Measure π)
[MeasureTheory.IsProbabilityMeasure ΞΌ]
:
@[simp]
theorem
Learning.randomSampling_policy
{π : Type u_1}
{π¨ : Type u_2}
[MeasurableSpace π]
[MeasurableSpace π¨]
(ΞΌ : MeasureTheory.Measure π)
[MeasureTheory.IsProbabilityMeasure ΞΌ]
(xβ : β)
:
(randomSampling ΞΌ).policy xβ = ProbabilityTheory.Kernel.const (β₯(Finset.Iic xβ) β π Γ π¨) ΞΌ
theorem
Learning.randomSampling.hasLaw_action
{π : Type u_1}
{π¨ : Type u_2}
{Ξ© : Type u_3}
[MeasurableSpace π]
[MeasurableSpace π¨]
[StandardBorelSpace π]
[Nonempty π]
[StandardBorelSpace π¨]
[Nonempty π¨]
{ΞΌ : MeasureTheory.Measure π}
[MeasureTheory.IsProbabilityMeasure ΞΌ]
[MeasurableSpace Ξ©]
{P : MeasureTheory.Measure Ξ©}
[MeasureTheory.IsProbabilityMeasure P]
{A : β β Ξ© β π}
{Y : β β Ξ© β π¨}
{env : Environment π π¨}
(h : IsAlgEnvSeq A Y (randomSampling ΞΌ) env P)
(n : β)
:
ProbabilityTheory.HasLaw (A n) ΞΌ P
Each action follows the distribution ΞΌ.
theorem
Learning.randomSampling.iIndep_action
{π : Type u_1}
{π¨ : Type u_2}
{Ξ© : Type u_3}
[MeasurableSpace π]
[MeasurableSpace π¨]
[StandardBorelSpace π]
[Nonempty π]
[StandardBorelSpace π¨]
[Nonempty π¨]
{ΞΌ : MeasureTheory.Measure π}
[MeasureTheory.IsProbabilityMeasure ΞΌ]
[MeasurableSpace Ξ©]
{P : MeasureTheory.Measure Ξ©}
[MeasureTheory.IsProbabilityMeasure P]
{A : β β Ξ© β π}
{Y : β β Ξ© β π¨}
{env : Environment π π¨}
(h : IsAlgEnvSeq A Y (randomSampling ΞΌ) env P)
:
Actions are mutually independent.