3.12. SequentialLearning.Algorithms.RandomSampling.Basic🔗

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.

Module LeanMachineLearning.SequentialLearning.Algorithms.RandomSampling.Basic contains 5 exposed declarations.

• Learning.randomSamplingDefinition · 1 deps
• Learning.randomSampling_p0Lemma · 2 deps
• Learning.randomSampling_policyLemma · 2 deps
• Learning.randomSampling.hasLaw_actionLemma · 5 deps
• Learning.randomSampling.iIndep_actionLemma · 5 deps