SequentialLearning.Algorithms.RoundRobin

`sum_mod_range`🔗

Lemmasum_mod_range

Details

No docstring.

theorem

sum_mod_range {K : ℕ} (hK : 0 < K) (a : Fin K) :
  (∑ s ∈ Finset.range K, if ⟨s % K, ⋯⟩ = a then 1 else 0) = 1
sum_mod_range {K : ℕ} (hK : 0 < K)
  (a : Fin K) :
  (∑ s ∈ Finset.range K,
      if ⟨s % K, ⋯⟩ = a then 1 else 0) =
    1

Code

lemma sum_mod_range {K : ℕ} (hK : 0 < K) (a : Fin K) :
    (∑ s ∈ range K, if ⟨s % K, Nat.mod_lt _ hK⟩ = a then 1 else 0) = 1

Used by (1)

sum_mod_range_mul

Actions: Source · Open Issue

Proof

by
  have h_iff (s : ℕ) (hs : s < K) : ⟨s % K, Nat.mod_lt _ hK⟩ = a ↔ s = a := by
    simp only [Nat.mod_eq_of_lt hs, Fin.ext_iff]
  calc (∑ s ∈ range K, if ⟨s % K, Nat.mod_lt _ hK⟩ = a then 1 else 0)
  _ = ∑ s ∈ range K, if s = a then 1 else 0 := sum_congr rfl fun s hs ↦ by grind
  _ = _ := by
    rw [sum_ite_eq']
    simp

`sum_mod_range_mul`🔗

Lemmasum_mod_range_mul

Details

No docstring.

theorem

sum_mod_range_mul {K : ℕ} (hK : 0 < K) (m : ℕ) (a : Fin K) :
  (∑ s ∈ Finset.range (K * m), if ⟨s % K, ⋯⟩ = a then 1 else 0) = m
sum_mod_range_mul {K : ℕ} (hK : 0 < K)
  (m : ℕ) (a : Fin K) :
  (∑ s ∈ Finset.range (K * m),
      if ⟨s % K, ⋯⟩ = a then 1 else 0) =
    m

Code

lemma sum_mod_range_mul {K : ℕ} (hK : 0 < K) (m : ℕ) (a : Fin K) :
    (∑ s ∈ range (K * m), if ⟨s % K, Nat.mod_lt _ hK⟩ = a then 1 else 0) = m

Body uses (1)

sum_mod_range

Used by (1)

pullCount_mul

Actions: Source · Open Issue

Proof

by
  induction m with
  | zero => simp
  | succ n hn =>
    calc (∑ s ∈ range (K * (n + 1)), if ⟨s % K, Nat.mod_lt _ hK⟩ = a then 1 else 0)
    _ = (∑ s ∈ range (K * n + K), if ⟨s % K, Nat.mod_lt _ hK⟩ = a then 1 else 0) := by ring_nf
    _ = (∑ s ∈ range (K * n), if ⟨s % K, Nat.mod_lt _ hK⟩ = a then 1 else 0)
        + (∑ s ∈ Ico (K * n) (K * n + K), if ⟨s % K, Nat.mod_lt _ hK⟩ = a then 1 else 0) := by
      rw [sum_range_add_sum_Ico]
      grind
    _ = n + (∑ s ∈ Ico (K * n) (K * n + K), if ⟨s % K, Nat.mod_lt _ hK⟩ = a then 1 else 0) := by
      rw [hn]
    _ = n + (∑ s ∈ range K, if ⟨(s + K * n) % K, Nat.mod_lt _ hK⟩ = a then 1 else 0) := by
      congr 1
      let e : ℕ ↪ ℕ := ⟨fun i : ℕ ↦ i + K * n, fun i j hij ↦ by grind⟩
      have : Finset.map e (range K) = Ico (K * n) (K * n + K) := by
        ext x
        simp only [mem_map, mem_range, Function.Embedding.coeFn_mk, mem_Ico, e]
        refine ⟨fun h ↦ by grind, fun h ↦ ?_⟩
        use x - K * n
        grind
      rw [← this, Finset.sum_map]
      congr
    _ = n + (∑ s ∈ range K, if ⟨s % K, Nat.mod_lt _ hK⟩ = a then 1 else 0) := by simp
    _ = n + 1 := by rw [sum_mod_range hK]

`nextAction`🔗

DefinitionLearning.RoundRobin.nextAction

Details

Action chosen by the Round-Robin algorithm at time n + 1. This is action (n + 1) % K.

def

Learning.RoundRobin.nextAction {K : ℕ} (hK : 0 < K) (n : ℕ) : Fin K
Learning.RoundRobin.nextAction {K : ℕ}
  (hK : 0 < K) (n : ℕ) : Fin K

Code

noncomputable
def RoundRobin.nextAction (hK : 0 < K) (n : ℕ) : Fin K := ⟨(n + 1) % K, Nat.mod_lt _ hK⟩

Used by (14)

Actions: Source · Open Issue

`roundRobinAlgorithm`🔗

DefinitionLearning.roundRobinAlgorithm

Details

The Round-Robin algorithm: deterministic algorithm that chooses action n % K at time n.

def

Learning.roundRobinAlgorithm.{u_1} {𝓨 : Type u_1}
  {m𝓨 : MeasurableSpace 𝓨} {K : ℕ} (hK : 0 < K) : Algorithm (Fin K) 𝓨
Learning.roundRobinAlgorithm.{u_1}
  {𝓨 : Type u_1} {m𝓨 : MeasurableSpace 𝓨}
  {K : ℕ} (hK : 0 < K) :
  Algorithm (Fin K) 𝓨

Code

noncomputable
def roundRobinAlgorithm (hK : 0 < K) : Algorithm (Fin K) 𝓨 :=
  detAlgorithm (fun n _ ↦ RoundRobin.nextAction hK n) (by fun_prop) ⟨0, hK⟩

Type uses (1)

Algorithm

Body uses (2)

Used by (13)

Actions: Source · Open Issue

`action_zero`🔗

LemmaLearning.RoundRobin.action_zero

Details

No docstring.

theorem

Learning.RoundRobin.action_zero.{u_1, u_2} {𝓨 : Type u_1}
  {m𝓨 : MeasurableSpace 𝓨} {K : ℕ} {hK : 0 < K}
  {ν : ProbabilityTheory.Kernel (Fin K) 𝓨}
  [ProbabilityTheory.IsMarkovKernel ν] {Ω : Type u_2}
  {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P] {A : ℕ → Ω → Fin K}
  {Y : ℕ → Ω → 𝓨}
  (h :
    IsAlgEnvSeqUntil A Y (roundRobinAlgorithm hK) (stationaryEnv ν) P
      0) :
  A 0 =ᵐ[P] fun x => ⟨0, hK⟩
Learning.RoundRobin.action_zero.{u_1, u_2}
  {𝓨 : Type u_1} {m𝓨 : MeasurableSpace 𝓨}
  {K : ℕ} {hK : 0 < K}
  {ν : ProbabilityTheory.Kernel (Fin K) 𝓨}
  [ProbabilityTheory.IsMarkovKernel ν]
  {Ω : Type u_2} {mΩ : MeasurableSpace Ω}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : ℕ → Ω → Fin K} {Y : ℕ → Ω → 𝓨}
  (h :
    IsAlgEnvSeqUntil A Y
      (roundRobinAlgorithm hK)
      (stationaryEnv ν) P 0) :
  A 0 =ᵐ[P] fun x => ⟨0, hK⟩

Code

lemma action_zero
    (h : IsAlgEnvSeqUntil A Y (roundRobinAlgorithm hK) (stationaryEnv ν) P 0) :
    A 0 =ᵐ[P] fun _ ↦ ⟨0, hK⟩

Type uses (3)

Body uses (2)

Used by (3)

Actions: Source · Open Issue

Proof

by
  have : Nonempty (Fin K) := Fin.pos_iff_nonempty.mp hK
  exact h.action_zero_detAlgorithm

`action_ae_eq_roundRobinNextAction`🔗

LemmaLearning.RoundRobin.action_ae_eq_roundRobinNextAction

Details

No docstring.

theorem

Learning.RoundRobin.action_ae_eq_roundRobinNextAction.{u_1, u_2}
  {𝓨 : Type u_1} {m𝓨 : MeasurableSpace 𝓨} {K : ℕ} {hK : 0 < K}
  {ν : ProbabilityTheory.Kernel (Fin K) 𝓨}
  [ProbabilityTheory.IsMarkovKernel ν] {Ω : Type u_2}
  {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P] {A : ℕ → Ω → Fin K}
  {Y : ℕ → Ω → 𝓨} (n : ℕ)
  (h :
    IsAlgEnvSeqUntil A Y (roundRobinAlgorithm hK) (stationaryEnv ν) P
      (n + 1)) :
  A (n + 1) =ᵐ[P] fun x => nextAction hK n
Learning.RoundRobin.action_ae_eq_roundRobinNextAction.{u_1,
    u_2}
  {𝓨 : Type u_1} {m𝓨 : MeasurableSpace 𝓨}
  {K : ℕ} {hK : 0 < K}
  {ν : ProbabilityTheory.Kernel (Fin K) 𝓨}
  [ProbabilityTheory.IsMarkovKernel ν]
  {Ω : Type u_2} {mΩ : MeasurableSpace Ω}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : ℕ → Ω → Fin K} {Y : ℕ → Ω → 𝓨}
  (n : ℕ)
  (h :
    IsAlgEnvSeqUntil A Y
      (roundRobinAlgorithm hK)
      (stationaryEnv ν) P (n + 1)) :
  A (n + 1) =ᵐ[P] fun x => nextAction hK n

Code

lemma action_ae_eq_roundRobinNextAction (n : ℕ)
    (h : IsAlgEnvSeqUntil A Y (roundRobinAlgorithm hK) (stationaryEnv ν) P (n + 1)) :
    A (n + 1) =ᵐ[P] fun _ ↦ nextAction hK n

Type uses (4)

Body uses (1)

action_detAlgorithm_ae_eq

Used by (1)

action_ae_eq

Actions: Source · Open Issue

Proof

h.action_detAlgorithm_ae_eq (by grind)

`action_ae_eq`🔗

LemmaLearning.RoundRobin.action_ae_eq

Details

The action chosen at time n is the action n % K.

theorem

Learning.RoundRobin.action_ae_eq.{u_1, u_2} {𝓨 : Type u_1}
  {m𝓨 : MeasurableSpace 𝓨} {K : ℕ} {hK : 0 < K}
  {ν : ProbabilityTheory.Kernel (Fin K) 𝓨}
  [ProbabilityTheory.IsMarkovKernel ν] {Ω : Type u_2}
  {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P] {A : ℕ → Ω → Fin K}
  {Y : ℕ → Ω → 𝓨} (n : ℕ)
  (h :
    IsAlgEnvSeqUntil A Y (roundRobinAlgorithm hK) (stationaryEnv ν) P
      n) :
  A n =ᵐ[P] fun x => ⟨n % K, ⋯⟩
Learning.RoundRobin.action_ae_eq.{u_1,
    u_2}
  {𝓨 : Type u_1} {m𝓨 : MeasurableSpace 𝓨}
  {K : ℕ} {hK : 0 < K}
  {ν : ProbabilityTheory.Kernel (Fin K) 𝓨}
  [ProbabilityTheory.IsMarkovKernel ν]
  {Ω : Type u_2} {mΩ : MeasurableSpace Ω}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : ℕ → Ω → Fin K} {Y : ℕ → Ω → 𝓨}
  (n : ℕ)
  (h :
    IsAlgEnvSeqUntil A Y
      (roundRobinAlgorithm hK)
      (stationaryEnv ν) P n) :
  A n =ᵐ[P] fun x => ⟨n % K, ⋯⟩

Code

lemma action_ae_eq (n : ℕ)
    (h : IsAlgEnvSeqUntil A Y (roundRobinAlgorithm hK) (stationaryEnv ν) P n) :
    A n =ᵐ[P] fun _ ↦ ⟨n % K, Nat.mod_lt _ hK⟩

Type uses (3)

Body uses (3)

Used by (2)

Actions: Source · Open Issue

Proof

by
  cases n with
  | zero => exact action_zero h
  | succ n =>
    filter_upwards [action_ae_eq_roundRobinNextAction n h] with h hn_eq
    rw [hn_eq, nextAction]

`pullCount_mul`🔗

LemmaLearning.RoundRobin.pullCount_mul

Details

At time K * m, the number of times each action is chosen is equal to m.

theorem

Learning.RoundRobin.pullCount_mul.{u_1, u_2} {𝓨 : Type u_1}
  {m𝓨 : MeasurableSpace 𝓨} {K : ℕ} {hK : 0 < K}
  {ν : ProbabilityTheory.Kernel (Fin K) 𝓨}
  [ProbabilityTheory.IsMarkovKernel ν] {Ω : Type u_2}
  {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P] {A : ℕ → Ω → Fin K}
  {Y : ℕ → Ω → 𝓨} (m : ℕ)
  (h :
    IsAlgEnvSeqUntil A Y (roundRobinAlgorithm hK) (stationaryEnv ν) P
      (K * m - 1))
  (a : Fin K) : pullCount A a (K * m) =ᵐ[P] fun x => m
Learning.RoundRobin.pullCount_mul.{u_1,
    u_2}
  {𝓨 : Type u_1} {m𝓨 : MeasurableSpace 𝓨}
  {K : ℕ} {hK : 0 < K}
  {ν : ProbabilityTheory.Kernel (Fin K) 𝓨}
  [ProbabilityTheory.IsMarkovKernel ν]
  {Ω : Type u_2} {mΩ : MeasurableSpace Ω}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : ℕ → Ω → Fin K} {Y : ℕ → Ω → 𝓨}
  (m : ℕ)
  (h :
    IsAlgEnvSeqUntil A Y
      (roundRobinAlgorithm hK)
      (stationaryEnv ν) P (K * m - 1))
  (a : Fin K) :
  pullCount A a (K * m) =ᵐ[P] fun x => m

Code

lemma pullCount_mul (m : ℕ)
    (h : IsAlgEnvSeqUntil A Y (roundRobinAlgorithm hK) (stationaryEnv ν) P (K * m - 1))
    (a : Fin K) :
    pullCount A a (K * m) =ᵐ[P] fun _ ↦ m

Type uses (4)

Body uses (4)

Used by (2)

Actions: Source · Open Issue

Proof

by
  rw [Filter.EventuallyEq]
  simp_rw [pullCount_eq_sum]
  have h_arm (n : range (K * m)) : A n =ᵐ[P] fun _ ↦ ⟨n % K, Nat.mod_lt _ hK⟩ :=
    action_ae_eq n (h.mono (by have := n.2; simp only [mem_range] at this; grind))
  simp_rw [Filter.EventuallyEq, ← ae_all_iff] at h_arm
  filter_upwards [h_arm] with ω h_arm
  have h_arm' {i : ℕ} (hi : i ∈ range (K * m)) : A i ω = ⟨i % K, Nat.mod_lt _ hK⟩ := h_arm ⟨i, hi⟩
  calc (∑ s ∈ range (K * m), if A s ω = a then 1 else 0)
  _ = (∑ s ∈ range (K * m), if ⟨s % K, Nat.mod_lt _ hK⟩ = a then 1 else 0) :=
    sum_congr rfl fun s hs ↦ by rw [h_arm' hs]
  _ = m := sum_mod_range_mul hK m a

`pullCount_eq_one`🔗

LemmaLearning.RoundRobin.pullCount_eq_one

Details

No docstring.

theorem

Learning.RoundRobin.pullCount_eq_one.{u_1, u_2} {𝓨 : Type u_1}
  {m𝓨 : MeasurableSpace 𝓨} {K : ℕ} {hK : 0 < K}
  {ν : ProbabilityTheory.Kernel (Fin K) 𝓨}
  [ProbabilityTheory.IsMarkovKernel ν] {Ω : Type u_2}
  {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P] {A : ℕ → Ω → Fin K}
  {Y : ℕ → Ω → 𝓨}
  (h :
    IsAlgEnvSeqUntil A Y (roundRobinAlgorithm hK) (stationaryEnv ν) P
      (K - 1))
  (a : Fin K) : pullCount A a K =ᵐ[P] fun x => 1
Learning.RoundRobin.pullCount_eq_one.{u_1,
    u_2}
  {𝓨 : Type u_1} {m𝓨 : MeasurableSpace 𝓨}
  {K : ℕ} {hK : 0 < K}
  {ν : ProbabilityTheory.Kernel (Fin K) 𝓨}
  [ProbabilityTheory.IsMarkovKernel ν]
  {Ω : Type u_2} {mΩ : MeasurableSpace Ω}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : ℕ → Ω → Fin K} {Y : ℕ → Ω → 𝓨}
  (h :
    IsAlgEnvSeqUntil A Y
      (roundRobinAlgorithm hK)
      (stationaryEnv ν) P (K - 1))
  (a : Fin K) :
  pullCount A a K =ᵐ[P] fun x => 1

Code

lemma pullCount_eq_one
    (h : IsAlgEnvSeqUntil A Y (roundRobinAlgorithm hK) (stationaryEnv ν) P (K - 1)) (a : Fin K) :
    pullCount A a K =ᵐ[P] fun _ ↦ 1

Type uses (4)

Body uses (3)

Used by (2)

Actions: Source · Open Issue

Proof

by
  suffices pullCount A a (K * 1) =ᵐ[P] fun _ ↦ 1 by simpa using this
  refine pullCount_mul 1 (P := P) (ν := ν) (Y := Y) (hK := hK) ?_ a
  simpa

`time_gt_of_pullCount_gt_one`🔗

LemmaLearning.RoundRobin.time_gt_of_pullCount_gt_one

Details

No docstring.

theorem

Learning.RoundRobin.time_gt_of_pullCount_gt_one.{u_1, u_2}
  {𝓨 : Type u_1} {m𝓨 : MeasurableSpace 𝓨} {K : ℕ} {hK : 0 < K}
  {ν : ProbabilityTheory.Kernel (Fin K) 𝓨}
  [ProbabilityTheory.IsMarkovKernel ν] {Ω : Type u_2}
  {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P] {A : ℕ → Ω → Fin K}
  {Y : ℕ → Ω → 𝓨}
  (h :
    IsAlgEnvSeqUntil A Y (roundRobinAlgorithm hK) (stationaryEnv ν) P
      (K - 1))
  (a : Fin K) : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), 1 < pullCount A a n ω → K < n
Learning.RoundRobin.time_gt_of_pullCount_gt_one.{u_1,
    u_2}
  {𝓨 : Type u_1} {m𝓨 : MeasurableSpace 𝓨}
  {K : ℕ} {hK : 0 < K}
  {ν : ProbabilityTheory.Kernel (Fin K) 𝓨}
  [ProbabilityTheory.IsMarkovKernel ν]
  {Ω : Type u_2} {mΩ : MeasurableSpace Ω}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : ℕ → Ω → Fin K} {Y : ℕ → Ω → 𝓨}
  (h :
    IsAlgEnvSeqUntil A Y
      (roundRobinAlgorithm hK)
      (stationaryEnv ν) P (K - 1))
  (a : Fin K) :
  ∀ᵐ (ω : Ω) ∂P,
    ∀ (n : ℕ),
      1 < pullCount A a n ω → K < n

Code

lemma time_gt_of_pullCount_gt_one
    (h : IsAlgEnvSeqUntil A Y (roundRobinAlgorithm hK) (stationaryEnv ν) P (K - 1)) (a : Fin K) :
    ∀ᵐ ω ∂P, ∀ n, 1 < pullCount A a n ω → K < n

Type uses (4)

Body uses (2)

Used by (2)

Actions: Source · Open Issue

Proof

by
  filter_upwards [pullCount_eq_one h a] with h h_eq n hn
  rw [← h_eq] at hn
  by_contra! h_lt
  exact hn.not_ge (pullCount_mono _ h_lt _)

`pullCount_pos_of_time_ge`🔗

LemmaLearning.RoundRobin.pullCount_pos_of_time_ge

Details

No docstring.

theorem

Learning.RoundRobin.pullCount_pos_of_time_ge.{u_1, u_2} {𝓨 : Type u_1}
  {m𝓨 : MeasurableSpace 𝓨} {K : ℕ} {hK : 0 < K}
  {ν : ProbabilityTheory.Kernel (Fin K) 𝓨}
  [ProbabilityTheory.IsMarkovKernel ν] {Ω : Type u_2}
  {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P] {A : ℕ → Ω → Fin K}
  {Y : ℕ → Ω → 𝓨}
  (h :
    IsAlgEnvSeqUntil A Y (roundRobinAlgorithm hK) (stationaryEnv ν) P
      (K - 1)) :
  ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), K ≤ n → ∀ (b : Fin K), 0 < pullCount A b n ω
Learning.RoundRobin.pullCount_pos_of_time_ge.{u_1,
    u_2}
  {𝓨 : Type u_1} {m𝓨 : MeasurableSpace 𝓨}
  {K : ℕ} {hK : 0 < K}
  {ν : ProbabilityTheory.Kernel (Fin K) 𝓨}
  [ProbabilityTheory.IsMarkovKernel ν]
  {Ω : Type u_2} {mΩ : MeasurableSpace Ω}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : ℕ → Ω → Fin K} {Y : ℕ → Ω → 𝓨}
  (h :
    IsAlgEnvSeqUntil A Y
      (roundRobinAlgorithm hK)
      (stationaryEnv ν) P (K - 1)) :
  ∀ᵐ (ω : Ω) ∂P,
    ∀ (n : ℕ),
      K ≤ n →
        ∀ (b : Fin K),
          0 < pullCount A b n ω

Code

lemma pullCount_pos_of_time_ge
    (h : IsAlgEnvSeqUntil A Y (roundRobinAlgorithm hK) (stationaryEnv ν) P (K - 1)) :
    ∀ᵐ ω ∂P, ∀ n, K ≤ n → ∀ b : Fin K, 0 < pullCount A b n ω

Type uses (4)

Body uses (2)

Used by (1)

pullCount_pos_of_pullCount_gt_one

Actions: Source · Open Issue

Proof

by
  have h_ae a := pullCount_eq_one h a
  simp_rw [Filter.EventuallyEq, ← ae_all_iff] at h_ae
  filter_upwards [h_ae] with ω hω n hn a
  refine Nat.one_pos.trans_le ?_
  rw [← hω a]
  exact pullCount_mono _ hn _

`pullCount_pos_of_pullCount_gt_one`🔗

LemmaLearning.RoundRobin.pullCount_pos_of_pullCount_gt_one

Details

No docstring.

theorem

Learning.RoundRobin.pullCount_pos_of_pullCount_gt_one.{u_1, u_2}
  {𝓨 : Type u_1} {m𝓨 : MeasurableSpace 𝓨} {K : ℕ} {hK : 0 < K}
  {ν : ProbabilityTheory.Kernel (Fin K) 𝓨}
  [ProbabilityTheory.IsMarkovKernel ν] {Ω : Type u_2}
  {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P] {A : ℕ → Ω → Fin K}
  {Y : ℕ → Ω → 𝓨}
  (h :
    IsAlgEnvSeqUntil A Y (roundRobinAlgorithm hK) (stationaryEnv ν) P
      (K - 1))
  (a : Fin K) :
  ∀ᵐ (ω : Ω) ∂P,
    ∀ (n : ℕ),
      1 < pullCount A a n ω → ∀ (b : Fin K), 0 < pullCount A b n ω
Learning.RoundRobin.pullCount_pos_of_pullCount_gt_one.{u_1,
    u_2}
  {𝓨 : Type u_1} {m𝓨 : MeasurableSpace 𝓨}
  {K : ℕ} {hK : 0 < K}
  {ν : ProbabilityTheory.Kernel (Fin K) 𝓨}
  [ProbabilityTheory.IsMarkovKernel ν]
  {Ω : Type u_2} {mΩ : MeasurableSpace Ω}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : ℕ → Ω → Fin K} {Y : ℕ → Ω → 𝓨}
  (h :
    IsAlgEnvSeqUntil A Y
      (roundRobinAlgorithm hK)
      (stationaryEnv ν) P (K - 1))
  (a : Fin K) :
  ∀ᵐ (ω : Ω) ∂P,
    ∀ (n : ℕ),
      1 < pullCount A a n ω →
        ∀ (b : Fin K),
          0 < pullCount A b n ω

Code

lemma pullCount_pos_of_pullCount_gt_one
    (h : IsAlgEnvSeqUntil A Y (roundRobinAlgorithm hK) (stationaryEnv ν) P (K - 1)) (a : Fin K) :
    ∀ᵐ ω ∂P, ∀ n, 1 < pullCount A a n ω → ∀ b : Fin K, 0 < pullCount A b n ω

Type uses (4)

Body uses (2)

Used by (1)

pullCount_pos_of_pullCount_gt_one

Actions: Source · Open Issue

Proof

by
  filter_upwards [time_gt_of_pullCount_gt_one h a, pullCount_pos_of_time_ge h] with ω h1 h2 n h_gt a
  exact h2 n (h1 n h_gt).le a

LeanMachineLearning exposition

3.6. SequentialLearning.Algorithms.RoundRobin🔗

`sum_mod_range`🔗

`sum_mod_range_mul`🔗

`nextAction`🔗

`roundRobinAlgorithm`🔗

`action_zero`🔗

`action_ae_eq_roundRobinNextAction`🔗

`action_ae_eq`🔗

`pullCount_mul`🔗

`pullCount_eq_one`🔗

`time_gt_of_pullCount_gt_one`🔗

`pullCount_pos_of_time_ge`🔗

`pullCount_pos_of_pullCount_gt_one`🔗

3.6. SequentialLearning.Algorithms.RoundRobin🔗

sum_mod_range🔗

sum_mod_range_mul🔗

nextAction🔗

roundRobinAlgorithm🔗

action_zero🔗

action_ae_eq_roundRobinNextAction🔗

action_ae_eq🔗

pullCount_mul🔗

pullCount_eq_one🔗

time_gt_of_pullCount_gt_one🔗

pullCount_pos_of_time_ge🔗

pullCount_pos_of_pullCount_gt_one🔗

`sum_mod_range`🔗

`sum_mod_range_mul`🔗

`nextAction`🔗

`roundRobinAlgorithm`🔗

`action_zero`🔗

`action_ae_eq_roundRobinNextAction`🔗

`action_ae_eq`🔗

`pullCount_mul`🔗

`pullCount_eq_one`🔗

`time_gt_of_pullCount_gt_one`🔗

`pullCount_pos_of_time_ge`🔗

`pullCount_pos_of_pullCount_gt_one`🔗