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}
{šØ : Type u_3}
{mš : MeasurableSpace š}
{mš : MeasurableSpace š}
{mšØ : 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 (Learning.Hist š š šØ x Ć š) Ī¼, isMarkovKernel_policy := āÆ }
Instances For
@[simp]
theorem
Learning.randomSampling_policy
{š : Type u_1}
{š : Type u_2}
{šØ : Type u_3}
{mš : MeasurableSpace š}
{mš : MeasurableSpace š}
{mšØ : MeasurableSpace šØ}
(Ī¼ : MeasureTheory.Measure š)
[MeasureTheory.IsProbabilityMeasure Ī¼]
(xā : ā)
:
(randomSampling Ī¼).policy xā = ProbabilityTheory.Kernel.const (Hist š š šØ xā Ć š) Ī¼
theorem
Learning.randomSampling.hasLaw_action
{š : Type u_1}
{š : Type u_2}
{šØ : Type u_3}
{Ī© : Type u_4}
{mš : MeasurableSpace š}
{mš : MeasurableSpace š}
{mšØ : MeasurableSpace šØ}
{mĪ© : MeasurableSpace Ī©}
{Ī¼ : MeasureTheory.Measure š}
[MeasureTheory.IsProbabilityMeasure Ī¼]
{P : MeasureTheory.Measure Ī©}
[MeasureTheory.IsProbabilityMeasure P]
{O : ā ā Ī© ā š}
{A : ā ā Ī© ā š}
{Y : ā ā Ī© ā šØ}
{env : Environment š š šØ}
(h : IsAlgEnvSeq O 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}
{Ī© : Type u_4}
{mš : MeasurableSpace š}
{mš : MeasurableSpace š}
{mšØ : MeasurableSpace šØ}
{mĪ© : MeasurableSpace Ī©}
{Ī¼ : MeasureTheory.Measure š}
[MeasureTheory.IsProbabilityMeasure Ī¼]
{P : MeasureTheory.Measure Ī©}
[MeasureTheory.IsProbabilityMeasure P]
{O : ā ā Ī© ā š}
{A : ā ā Ī© ā š}
{Y : ā ā Ī© ā šØ}
{env : Environment š š šØ}
(h : IsAlgEnvSeq O A Y (randomSampling Ī¼) env P)
:
Actions are mutually independent.