LeanMachineLearning

3.14. SequentialLearning.Algorithms.RandomSampling.Tendsto🔗

Random Sampling convergence lemmas

This file contains several convergence lemmas for the randomSampling algorithm along with an evalEnv environment, that evaluates the actions using a measurable function.

Main statements

  • hasLaw_feeback: Each feedback follows the distribution μ.map f.

  • iIndep_feedback: Feedbacks are mutually independent across time steps.

  • action_tendsto_any: The minimum distance from sampled actions to any point in α tends to zero in measure.

  • feedback_tendsto_any: The minimum distance from rewards to any value of f tends to zero in measure.

  • tendsto_min: The minimum reward converges in measure to the global minimum value.

  • tendsto_max: The maximum reward converges in measure to the global maximum value.

Module LeanMachineLearning.SequentialLearning.Algorithms.RandomSampling.Tendsto contains 9 exposed declarations.