LeanMachineLearning exposition

Learning.IsBayesAlgEnvSeq.prob_empMean_bestAction_sub_actionMean_le_le🔗

This page has the declaration's own card below, then its dependency graph, then a card for each dependency (type dependencies first, then the rest of the transitive closure). For a theorem, the graph and the dependency cards only follow its statement's dependencies (its proof is replaced by sorry, so what it proves doesn't depend on how); for everything else, both the type and the body/value are followed, since their content is part of what later declarations build on.

Minimal Lean file

prob_empMean_bestAction_sub_actionMean_le_le🔗

LemmaLearning.IsBayesAlgEnvSeq.prob_empMean_bestAction_sub_actionMean_le_le
Details

No docstring.

🔗theorem
Learning.IsBayesAlgEnvSeq.prob_empMean_bestAction_sub_actionMean_le_le.{u_1,
    u_2}
  {𝓔 : Type u_1} {Ω : Type u_2} [MeasurableSpace 𝓔] [MeasurableSpace Ω]
  {K : ℕ} [Nonempty (Fin K)] {Q : MeasureTheory.Measure 𝓔}
  {κ : ProbabilityTheory.Kernel (𝓔 × Fin K) ℝ}
  [ProbabilityTheory.IsMarkovKernel κ] {alg : Algorithm (Fin K) ℝ}
  {E : Ω → 𝓔} {A : ℕ → Ω → Fin K} {R : ℕ → Ω → ℝ}
  {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
  (h : IsBayesAlgEnvSeq Q κ alg E A R P) {σ2 : NNReal} (hσ2 : 0 < σ2)
  (hs :
    ∀ (e : 𝓔) (a : Fin K),
      ProbabilityTheory.HasSubgaussianMGF
        (fun x => x - ∫ (x : ℝ), id x ∂κ (e, a)) σ2 (κ (e, a)))
  {δ : ℝ} (hδ : 0 < δ) (n : ℕ) :
  P
      {ω |
        ∃ t < n,
          pullCount A (bestAction κ E ω) t ω ≠ 0 ∧
            empMean A R (bestAction κ E ω) t ω -
                actionMean κ E (bestAction κ E ω) ω ≤
              -√(2 * ↑σ2 * Real.log (1 / δ) /
                    ↑(pullCount A (bestAction κ E ω) t ω))} ≤
    ENNReal.ofReal ((↑n - 1) * δ)
Learning.IsBayesAlgEnvSeq.prob_empMean_bestAction_sub_actionMean_le_le.{u_1,
    u_2}
  {𝓔 : Type u_1} {Ω : Type u_2}
  [MeasurableSpace 𝓔] [MeasurableSpace Ω]
  {K : ℕ} [Nonempty (Fin K)]
  {Q : MeasureTheory.Measure 𝓔}
  {κ :
    ProbabilityTheory.Kernel (𝓔 × Fin K)
      ℝ}
  [ProbabilityTheory.IsMarkovKernel κ]
  {alg : Algorithm (Fin K) ℝ} {E : Ω → 𝓔}
  {A : ℕ → Ω → Fin K} {R : ℕ → Ω → ℝ}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  (h : IsBayesAlgEnvSeq Q κ alg E A R P)
  {σ2 : NNReal} (hσ2 : 0 < σ2)
  (hs :
    ∀ (e : 𝓔) (a : Fin K),
      ProbabilityTheory.HasSubgaussianMGF
        (fun x =>
          x - ∫ (x : ℝ), id x ∂κ (e, a))
        σ2 (κ (e, a)))
  {δ : ℝ} (hδ : 0 < δ) (n : ℕ) :
  P
      {ω |
        ∃ t < n,
          pullCount A (bestAction κ E ω) t
                ω ≠
              0 ∧
            empMean A R (bestAction κ E ω)
                  t ω -
                actionMean κ E
                  (bestAction κ E ω) ω ≤
              -√(2 * ↑σ2 *
                      Real.log (1 / δ) /
                    ↑(pullCount A
                        (bestAction κ E ω)
                        t ω))} ≤
    ENNReal.ofReal ((↑n - 1) * δ)

Code

lemma prob_empMean_bestAction_sub_actionMean_le_le (h : IsBayesAlgEnvSeq Q κ alg E A R P)
    {σ2 : ℝ≥0} (hσ2 : 0 < σ2)
    (hs : ∀ e a, HasSubgaussianMGF (fun x ↦ x - (κ (e, a))[id]) σ2 (κ (e, a)))
    {δ : ℝ} (hδ : 0 < δ) (n : ℕ) :
    P {ω | ∃ t < n, pullCount A (bestAction κ E ω) t ω ≠ 0 ∧
        empMean A R (bestAction κ E ω) t ω - actionMean κ E (bestAction κ E ω) ω ≤
          -√(2 * σ2 * Real.log (1 / δ) / (pullCount A (bestAction κ E ω) t ω))}
      ≤ ENNReal.ofReal ((n - 1) * δ)
Type uses (6)
Body uses (15)
Used by (1)

Actions: Source · Open Issue

Proof
by
  have := h.measurable_param
  have := h.measurable_action
  have := h.measurable_feedback
  let S := {(e, τ) | ∃ t < n, pullCount IT.action (bestAction κ id e) t τ ≠ 0 ∧
    sumRewards IT.action IT.feedback (bestAction κ id e) t τ -
        pullCount IT.action (bestAction κ id e) t τ * actionMean κ id (bestAction κ id e) e ≤
          -√(2 * pullCount IT.action (bestAction κ id e) t τ * σ2 * Real.log (1 / δ))}
  calc
    _ ≤ (P.map (fun ω ↦ (E ω, trajectory A R ω))) S := by
        rw [Measure.map_apply (by fun_prop) (by measurability)]
        apply measure_mono
        intro ω ⟨t, ht, hpc, hle⟩
        rw [empMean] at hle
        exact ⟨t, ht, hpc, sub_le_neg_sqrt_two_mul hpc hle⟩
    _ = (P.map E ⊗ₘ condDistrib (trajectory A R) E P) S := by
        rw [← compProd_map_condDistrib (by fun_prop)]
    _ = ∫⁻ e, condDistrib (trajectory A R) E P e (Prod.mk e ⁻¹' S) ∂(P.map E) :=
        Measure.compProd_apply (by measurability)
    _ ≤ ∫⁻ e, ENNReal.ofReal ((n - 1) * δ) ∂(P.map E) := by
        apply lintegral_mono_ae
        rw [h.hasLaw_env.map_eq]
        filter_upwards [h.ae_IsAlgEnvSeq] with e he
        exact Bandits.prob_sumRewards_sub_pullCount_mul_le_le (ν := κ.sectR e) hσ2 (hs e _) he
          hδ
    _ = ENNReal.ofReal ((n - 1) * δ) := by
      simp [Measure.map_apply h.measurable_param]

Dependency graph

Type dependencies (6)

Algorithm🔗

StructureLearning.Algorithm
Details

A stochastic, sequential algorithm.

🔗structure
Learning.Algorithm.{u_4, u_5} (𝓐 : Type u_4) (𝓨 : Type u_5)
  [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] : Type (max u_4 u_5)
Learning.Algorithm.{u_4, u_5}
  (𝓐 : Type u_4) (𝓨 : Type u_5)
  [MeasurableSpace 𝓐]
  [MeasurableSpace 𝓨] : Type (max u_4 u_5)

Code

structure Algorithm (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] where
  /-- Policy or sampling rule: distribution of the next action. -/
  policy : (n : ℕ) → Kernel (Iic n → 𝓐 × 𝓨) 𝓐
  /-- The policy is a Markov kernel. -/
  [h_policy : ∀ n, IsMarkovKernel (policy n)]
  /-- Distribution of the first action. -/
  p0 : Measure 𝓐
  /-- The first action distribution is a probability measure. -/
  [hp0 : IsProbabilityMeasure p0]
Used by (216)

Actions: Source · Open Issue

IsBayesAlgEnvSeq🔗

StructureLearning.IsBayesAlgEnvSeq
Details

IsBayesAlgEnvSeq Q κ alg E A Y P states that there is a measure P : Measure Ω such that the parameter E : Ω → 𝓔 has law Q and that the sequences of actions A : ℕ → Ω → 𝓐 and feedbacks Y : ℕ → Ω → 𝓨 are generated by the algorithm alg : Algorithm 𝓐 𝓨 interacting with an underlying environment that depends on E and κ (stationaryEnv (κ.sectR (E ω))).

🔗structure
Learning.IsBayesAlgEnvSeq.{u_1, u_2, u_3, u_4} {𝓔 : Type u_1}
  {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} [MeasurableSpace 𝓔]
  [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace Ω]
  (Q : MeasureTheory.Measure 𝓔) (κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨)
  (alg : Algorithm 𝓐 𝓨) (E : Ω → 𝓔) (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨)
  (P : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure P] : Prop
Learning.IsBayesAlgEnvSeq.{u_1, u_2, u_3,
    u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2}
  {𝓨 : Type u_3} {Ω : Type u_4}
  [MeasurableSpace 𝓔] [MeasurableSpace 𝓐]
  [MeasurableSpace 𝓨] [MeasurableSpace Ω]
  (Q : MeasureTheory.Measure 𝓔)
  (κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨)
  (alg : Algorithm 𝓐 𝓨) (E : Ω → 𝓔)
  (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨)
  (P : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure P] : Prop

Code

structure IsBayesAlgEnvSeq
    (Q : Measure 𝓔) (κ : Kernel (𝓔 × 𝓐) 𝓨) (alg : Algorithm 𝓐 𝓨)
    (E : Ω → 𝓔) (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨)
    (P : Measure Ω) [IsFiniteMeasure P] : Prop where
  measurable_param : Measurable E := by fun_prop
  measurable_action n : Measurable (A n) := by fun_prop
  measurable_feedback n : Measurable (Y n) := by fun_prop
  hasLaw_env : HasLaw E Q P
  hasCondDistrib_action_zero : HasCondDistrib (A 0) E (Kernel.const _ alg.p0) P
  hasCondDistrib_feedback_zero : HasCondDistrib (Y 0) (fun ω ↦ (E ω, A 0 ω)) κ P
  hasCondDistrib_action n :
    HasCondDistrib (A (n + 1)) (fun ω ↦ (E ω, history A Y n ω))
      ((alg.policy n).prodMkLeft _) P
  hasCondDistrib_feedback n :
    HasCondDistrib (Y (n + 1)) (fun ω ↦ (history A Y n ω, E ω, A (n + 1) ω))
      (κ.prodMkLeft _) P
Type uses (2)
Used by (22)

Actions: Source · Open Issue

pullCount🔗

DefinitionLearning.pullCount
Details

Number of times action a was chosen up to time t (excluding t).

🔗def
Learning.pullCount.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : ℕ
Learning.pullCount.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐) (a : 𝓐)
  (t : ℕ) (ω : Ω) : ℕ

Code

noncomputable
def pullCount (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : ℕ :=
  #(filter (fun s ↦ A s ω = a) (range t))
Used by (146)

Actions: Source · Open Issue

bestAction🔗

DefinitionLearning.IsBayesAlgEnvSeq.bestAction
Details

A random variable that gives the action with the highest mean feedback.

🔗def
Learning.IsBayesAlgEnvSeq.bestAction.{u_1, u_2, u_4} {𝓔 : Type u_1}
  {𝓐 : Type u_2} {Ω : Type u_4} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐]
  [Nonempty 𝓐] [Fintype 𝓐] (κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) ℝ)
  (E : Ω → 𝓔) (ω : Ω) : 𝓐
Learning.IsBayesAlgEnvSeq.bestAction.{u_1,
    u_2, u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2}
  {Ω : Type u_4} [MeasurableSpace 𝓔]
  [MeasurableSpace 𝓐] [Nonempty 𝓐]
  [Fintype 𝓐]
  (κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) ℝ)
  (E : Ω → 𝓔) (ω : Ω) : 𝓐

Code

noncomputable
def bestAction [Nonempty 𝓐] [Fintype 𝓐] (κ : Kernel (𝓔 × 𝓐) ℝ) (E : Ω → 𝓔) (ω : Ω) : 𝓐 :=
  argmax (fun a ↦ actionMean κ E a ω)
Body uses (2)
Used by (12)

Actions: Source · Open Issue

empMean🔗

DefinitionLearning.empMean
Details

Empirical mean reward obtained when pulling action a up to time t (exclusive).

🔗def
Learning.empMean.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐) (R' : ℕ → Ω → ℝ) (a : 𝓐) (t : ℕ)
  (ω : Ω) : ℝ
Learning.empMean.{u_1, u_3} {𝓐 : Type u_1}
  {Ω : Type u_3} [DecidableEq 𝓐]
  (A : ℕ → Ω → 𝓐) (R' : ℕ → Ω → ℝ) (a : 𝓐)
  (t : ℕ) (ω : Ω) : ℝ

Code

noncomputable
def empMean (A : ℕ → Ω → 𝓐) (R' : ℕ → Ω → ℝ) (a : 𝓐) (t : ℕ) (ω : Ω) : ℝ :=
  sumRewards A R' a t ω / pullCount A a t ω
Body uses (2)
Used by (34)

Actions: Source · Open Issue

actionMean🔗

DefinitionLearning.IsBayesAlgEnvSeq.actionMean
Details

A random variable that gives the mean feedback of action a.

🔗def
Learning.IsBayesAlgEnvSeq.actionMean.{u_1, u_2, u_4} {𝓔 : Type u_1}
  {𝓐 : Type u_2} {Ω : Type u_4} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐]
  (κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) ℝ) (E : Ω → 𝓔) (a : 𝓐) (ω : Ω) :
  ℝ
Learning.IsBayesAlgEnvSeq.actionMean.{u_1,
    u_2, u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2}
  {Ω : Type u_4} [MeasurableSpace 𝓔]
  [MeasurableSpace 𝓐]
  (κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) ℝ)
  (E : Ω → 𝓔) (a : 𝓐) (ω : Ω) : ℝ

Code

noncomputable
def actionMean (κ : Kernel (𝓔 × 𝓐) ℝ) (E : Ω → 𝓔) (a : 𝓐) (ω : Ω) : ℝ := (κ (E ω, a))[id]
Used by (12)

Actions: Source · Open Issue

All dependencies, transitively (5)

history🔗

DefinitionLearning.history
Details

History of the algorithm-environment sequence up to time n.

🔗def
Learning.history.{u_1, u_2, u_3} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {Ω : Type u_3} (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (n : ℕ) (ω : Ω) :
  ↥(Finset.Iic n) → 𝓐 × 𝓨
Learning.history.{u_1, u_2, u_3}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {Ω : Type u_3} (A : ℕ → Ω → 𝓐)
  (Y : ℕ → Ω → 𝓨) (n : ℕ) (ω : Ω) :
  ↥(Finset.Iic n) → 𝓐 × 𝓨

Code

def history (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (n : ℕ) (ω : Ω) : Iic n → 𝓐 × 𝓨 :=
  fun i ↦ (A i ω, Y i ω)
Used by (72)

Actions: Source · Open Issue

max🔗

DefinitionFunction.max
Details

The maximum value of a tuple.

🔗def
Function.max.{u_1, u_2} {ι : Type u_1} {α : Type u_2} [LinearOrder α]
  [Fintype ι] [Nonempty ι] (f : ι → α) : α
Function.max.{u_1, u_2} {ι : Type u_1}
  {α : Type u_2} [LinearOrder α]
  [Fintype ι] [Nonempty ι] (f : ι → α) : α

Code

abbrev max : α := univ.sup' univ_nonempty f
Used by (8)

Actions: Source · Open Issue

exists_argmax🔗

Lemmaexists_argmax
Details

No docstring.

🔗theorem
exists_argmax.{u_1, u_2} {ι : Type u_1} {α : Type u_2} [LinearOrder α]
  [Fintype ι] [Nonempty ι] (f : ι → α) : ∃ i, f i = Function.max f
exists_argmax.{u_1, u_2} {ι : Type u_1}
  {α : Type u_2} [LinearOrder α]
  [Fintype ι] [Nonempty ι] (f : ι → α) :
  ∃ i, f i = Function.max f

Code

lemma exists_argmax : ∃ i, f i = f.max
Type uses (1)
Used by (3)

Actions: Source · Open Issue

Proof
by
  obtain ⟨i, -, hi⟩ := Finset.exists_mem_eq_sup' (by simp : Finset.univ.Nonempty) f
  exact ⟨i, hi.symm⟩

argmax🔗

Definitionargmax
Details

The index of the maximum value of a tuple.

🔗def
argmax.{u_1, u_2} {ι : Type u_1} {α : Type u_2} [LinearOrder α]
  [Fintype ι] [Nonempty ι] (f : ι → α) : ι
argmax.{u_1, u_2} {ι : Type u_1}
  {α : Type u_2} [LinearOrder α]
  [Fintype ι] [Nonempty ι] (f : ι → α) : ι

Code

noncomputable def argmax := (exists_argmax f).choose
Body uses (2)
Used by (17)

Actions: Source · Open Issue

sumRewards🔗

DefinitionLearning.sumRewards
Details

Sum of rewards obtained when pulling action a up to time t (exclusive).

🔗def
Learning.sumRewards.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐) (R' : ℕ → Ω → ℝ) (a : 𝓐) (t : ℕ)
  (ω : Ω) : ℝ
Learning.sumRewards.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐)
  (R' : ℕ → Ω → ℝ) (a : 𝓐) (t : ℕ)
  (ω : Ω) : ℝ

Code

def sumRewards (A : ℕ → Ω → 𝓐) (R' : ℕ → Ω → ℝ) (a : 𝓐) (t : ℕ) (ω : Ω) : ℝ :=
  ∑ s ∈ range t, if A s ω = a then R' s ω else 0
Used by (44)

Actions: Source · Open Issue