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 offtends 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.
theorem
Learning.randomSampling.hasLaw_feeback
{𝓐 : Type u_1}
{𝓨 : Type u_2}
{Ω : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure 𝓐}
[MeasureTheory.IsProbabilityMeasure μ]
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{O : ℕ → Ω → Unit}
{A : ℕ → Ω → 𝓐}
{Y : ℕ → Ω → 𝓨}
{f : 𝓐 → 𝓨}
{hf : Measurable f}
[StandardBorelSpace 𝓨]
[Nonempty 𝓨]
(h : IsAlgEnvSeq O A Y (randomSampling μ) (evalEnv f hf) P)
(n : ℕ)
:
ProbabilityTheory.HasLaw (Y n) (MeasureTheory.Measure.map f μ) P
Each reward follows the distribution μ.map f.
theorem
Learning.randomSampling.iIndep_feedback
{𝓐 : Type u_1}
{𝓨 : Type u_2}
{Ω : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure 𝓐}
[MeasureTheory.IsProbabilityMeasure μ]
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{O : ℕ → Ω → Unit}
{A : ℕ → Ω → 𝓐}
{Y : ℕ → Ω → 𝓨}
{f : 𝓐 → 𝓨}
{hf : Measurable f}
[StandardBorelSpace 𝓨]
[Nonempty 𝓨]
(h : IsAlgEnvSeq O A Y (randomSampling μ) (evalEnv f hf) P)
:
Rewards are mutually independent.
theorem
Learning.randomSampling.action_tendsto_any
{𝓐 : Type u_1}
{𝓨 : Type u_2}
{Ω : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure 𝓐}
[MeasureTheory.IsProbabilityMeasure μ]
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{O : ℕ → Ω → Unit}
{A : ℕ → Ω → 𝓐}
{Y : ℕ → Ω → 𝓨}
{f : 𝓐 → 𝓨}
{hf : Measurable f}
[PseudoMetricSpace 𝓐]
[SecondCountableTopology 𝓐]
[OpensMeasurableSpace 𝓐]
[μ.IsOpenPosMeasure]
(h : IsAlgEnvSeq O A Y (randomSampling μ) (evalEnv f hf) P)
(a : 𝓐)
{ε : ℝ}
(hε : 0 < ε)
:
Filter.Tendsto (fun (i : ℕ) => P {x : Ω | ε ≤ Function.min fun (j : ↥(Finset.Iic i)) => dist (A (↑j) x) a}) Filter.atTop
(nhds 0)
The minimum distance from sampled actions to any point tends to zero.
theorem
Learning.randomSampling.image_action_tendsto_any
{𝓐 : Type u_1}
{𝓨 : Type u_2}
{Ω : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure 𝓐}
[MeasureTheory.IsProbabilityMeasure μ]
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{O : ℕ → Ω → Unit}
{A : ℕ → Ω → 𝓐}
{Y : ℕ → Ω → 𝓨}
{f : 𝓐 → 𝓨}
[PseudoMetricSpace 𝓐]
[SecondCountableTopology 𝓐]
[OpensMeasurableSpace 𝓐]
[μ.IsOpenPosMeasure]
[PseudoMetricSpace 𝓨]
[BorelSpace 𝓨]
(hfc : Continuous f)
(h : IsAlgEnvSeq O A Y (randomSampling μ) (evalEnv f ⋯) P)
(a : 𝓐)
{ε : ℝ}
(hε : 0 < ε)
:
Filter.Tendsto (fun (i : ℕ) => P {x : Ω | ε ≤ Function.min fun (j : ↥(Finset.Iic i)) => dist (f (A (↑j) x)) (f a)})
Filter.atTop (nhds 0)
The minimum distance from image of actions to any function value tends to zero.
theorem
Learning.randomSampling.feedback_tendsto_any
{𝓐 : Type u_1}
{𝓨 : Type u_2}
{Ω : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{m𝓨 : MeasurableSpace 𝓨}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure 𝓐}
[MeasureTheory.IsProbabilityMeasure μ]
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{O : ℕ → Ω → Unit}
{A : ℕ → Ω → 𝓐}
{Y : ℕ → Ω → 𝓨}
{f : 𝓐 → 𝓨}
[PseudoMetricSpace 𝓐]
[SecondCountableTopology 𝓐]
[OpensMeasurableSpace 𝓐]
[μ.IsOpenPosMeasure]
[PseudoMetricSpace 𝓨]
[BorelSpace 𝓨]
(hfc : Continuous f)
[StandardBorelSpace 𝓨]
[Nonempty 𝓨]
(h : IsAlgEnvSeq O A Y (randomSampling μ) (evalEnv f ⋯) P)
(a : 𝓐)
{ε : ℝ}
(hε : 0 < ε)
:
Filter.Tendsto (fun (i : ℕ) => P {x : Ω | ε ≤ Function.min fun (j : ↥(Finset.Iic i)) => dist (Y (↑j) x) (f a)})
Filter.atTop (nhds 0)
The minimum distance from rewards to any function value tends to zero.
theorem
Learning.randomSampling.tendsto_min₀
{𝓐 : Type u_1}
{Ω : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure 𝓐}
[MeasureTheory.IsProbabilityMeasure μ]
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{O : ℕ → Ω → Unit}
{A : ℕ → Ω → 𝓐}
[PseudoMetricSpace 𝓐]
[SecondCountableTopology 𝓐]
[OpensMeasurableSpace 𝓐]
[μ.IsOpenPosMeasure]
{R : ℕ → Ω → ℝ}
{f : 𝓐 → ℝ}
(hfc : Continuous f)
{a : 𝓐}
(h : IsAlgEnvSeq O A R (randomSampling μ) (evalEnv f ⋯) P)
(hf_min : ∀ (x : 𝓐), f a ≤ f x)
:
MeasureTheory.TendstoInMeasure P (fun (n : ℕ) (ω : Ω) => Function.min fun (i : ↥(Finset.Iic n)) => f (A (↑i) ω))
Filter.atTop fun (x : Ω) => f a
The minimum image action converges to the function's global minimum.
theorem
Learning.randomSampling.tendsto_min
{𝓐 : Type u_1}
{Ω : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure 𝓐}
[MeasureTheory.IsProbabilityMeasure μ]
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{O : ℕ → Ω → Unit}
{A : ℕ → Ω → 𝓐}
[PseudoMetricSpace 𝓐]
[SecondCountableTopology 𝓐]
[OpensMeasurableSpace 𝓐]
[μ.IsOpenPosMeasure]
{R : ℕ → Ω → ℝ}
{f : 𝓐 → ℝ}
(hfc : Continuous f)
{a : 𝓐}
(h : IsAlgEnvSeq O A R (randomSampling μ) (evalEnv f ⋯) P)
(hf_min : ∀ (x : 𝓐), f a ≤ f x)
:
MeasureTheory.TendstoInMeasure P (fun (n : ℕ) (ω : Ω) => Function.min fun (i : ↥(Finset.Iic n)) => R (↑i) ω)
Filter.atTop fun (x : Ω) => f a
The minimum reward converges to the function's global minimum.
theorem
Learning.randomSampling.tendsto_max₀
{𝓐 : Type u_1}
{Ω : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure 𝓐}
[MeasureTheory.IsProbabilityMeasure μ]
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{O : ℕ → Ω → Unit}
{A : ℕ → Ω → 𝓐}
[PseudoMetricSpace 𝓐]
[SecondCountableTopology 𝓐]
[OpensMeasurableSpace 𝓐]
[μ.IsOpenPosMeasure]
{R : ℕ → Ω → ℝ}
{f : 𝓐 → ℝ}
(hfc : Continuous f)
{a : 𝓐}
(h : IsAlgEnvSeq O A R (randomSampling μ) (evalEnv f ⋯) P)
(hf_max : ∀ (x : 𝓐), f x ≤ f a)
:
MeasureTheory.TendstoInMeasure P (fun (n : ℕ) (ω : Ω) => Function.max fun (i : ↥(Finset.Iic n)) => f (A (↑i) ω))
Filter.atTop fun (x : Ω) => f a
The maximum image action converges to the function's global maximum.
theorem
Learning.randomSampling.tendsto_max
{𝓐 : Type u_1}
{Ω : Type u_3}
{m𝓐 : MeasurableSpace 𝓐}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure 𝓐}
[MeasureTheory.IsProbabilityMeasure μ]
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{O : ℕ → Ω → Unit}
{A : ℕ → Ω → 𝓐}
[PseudoMetricSpace 𝓐]
[SecondCountableTopology 𝓐]
[OpensMeasurableSpace 𝓐]
[μ.IsOpenPosMeasure]
{R : ℕ → Ω → ℝ}
{f : 𝓐 → ℝ}
(hfc : Continuous f)
{a : 𝓐}
(h : IsAlgEnvSeq O A R (randomSampling μ) (evalEnv f ⋯) P)
(hf_max : ∀ (x : 𝓐), f x ≤ f a)
:
MeasureTheory.TendstoInMeasure P (fun (n : ℕ) (ω : Ω) => Function.max fun (i : ↥(Finset.Iic n)) => R (↑i) ω)
Filter.atTop fun (x : Ω) => f a
The maximum reward converges to the function's global maximum.