Law of the sum of rewards

theorem Bandits.ArrayModel.identDistrib_sum_range_snd {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐} [Countable 𝓐] {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] (a : 𝓐) (k : ℕ) : ProbabilityTheory.IdentDistrib (fun (ω : probSpace 𝓐 ℝ) => ∑ i ∈ Finset.range k, ω.2 i a) (fun (ω : ℕ → 𝓐 → ℝ) => ∑ i ∈ Finset.range k, ω i a) (arrayMeasure ν) (streamMeasure ν)

theorem Bandits.ArrayModel.prob_pullCount_prod_sumRewards_mem_le {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐} [DecidableEq 𝓐] [Countable 𝓐] [StandardBorelSpace 𝓐] [Nonempty 𝓐] {alg : Learning.Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] (a : 𝓐) (n : ℕ) {s : Set (ℕ × ℝ)} [DecidablePred fun (x : ℕ) => x ∈ Prod.fst '' s] (hs : MeasurableSet s) : (arrayMeasure ν) {ω : probSpace 𝓐 ℝ | (Learning.pullCount (action alg) a n ω, Learning.sumRewards (action alg) (reward alg) a n ω) ∈ s} ≤ ∑ k ∈ Finset.range (n + 1) with k ∈ Prod.fst '' s, (streamMeasure ν) {ω : ℕ → 𝓐 → ℝ | ∑ i ∈ Finset.range k, ω i a ∈ Prod.mk k ⁻¹' s}

theorem Bandits.ArrayModel.prob_pullCount_mem_and_sumRewards_mem_le {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐} [DecidableEq 𝓐] [Countable 𝓐] [StandardBorelSpace 𝓐] [Nonempty 𝓐] {alg : Learning.Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] (a : 𝓐) (n : ℕ) {s : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ s] (hs : MeasurableSet s) {B : Set ℝ} (hB : MeasurableSet B) : (arrayMeasure ν) {ω : probSpace 𝓐 ℝ | Learning.pullCount (action alg) a n ω ∈ s ∧ Learning.sumRewards (action alg) (reward alg) a n ω ∈ B} ≤ ∑ k ∈ Finset.range (n + 1) with k ∈ s, (streamMeasure ν) {ω : ℕ → 𝓐 → ℝ | ∑ i ∈ Finset.range k, ω i a ∈ B}

theorem Bandits.ArrayModel.prob_exists_pullCount_eq_and_sumRewards_mem_le {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐} [DecidableEq 𝓐] [Countable 𝓐] [StandardBorelSpace 𝓐] [Nonempty 𝓐] {alg : Learning.Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] (a : 𝓐) (m : ℕ) {B : Set ℝ} (hB : MeasurableSet B) : (arrayMeasure ν) {ω : probSpace 𝓐 ℝ | ∃ (n : ℕ), Learning.pullCount (action alg) a n ω = m ∧ Learning.sumRewards (action alg) (reward alg) a n ω ∈ B} ≤ (streamMeasure ν) {ω : ℕ → 𝓐 → ℝ | ∑ i ∈ Finset.range m, ω i a ∈ B}

theorem Bandits.ArrayModel.prob_sumRewards_le_sumRewards_le {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐} [DecidableEq 𝓐] [Countable 𝓐] [StandardBorelSpace 𝓐] [Nonempty 𝓐] {alg : Learning.Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] [Fintype 𝓐] (a : 𝓐) (n m₁ m₂ : ℕ) : (arrayMeasure ν) {ω : probSpace 𝓐 ℝ | Learning.pullCount (action alg) (bestArm ν) n ω = m₁ ∧ Learning.pullCount (action alg) a n ω = m₂ ∧ Learning.sumRewards (action alg) (reward alg) (bestArm ν) n ω ≤ Learning.sumRewards (action alg) (reward alg) a n ω} ≤ (streamMeasure ν) {ω : ℕ → 𝓐 → ℝ | ∑ i ∈ Finset.range m₁, ω i (bestArm ν) ≤ ∑ i ∈ Finset.range m₂, ω i a}

theorem Bandits.ArrayModel.probReal_sumRewards_le_sumRewards_le {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐} [DecidableEq 𝓐] [Countable 𝓐] [StandardBorelSpace 𝓐] [Nonempty 𝓐] {alg : Learning.Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] [Fintype 𝓐] (a : 𝓐) (n m₁ m₂ : ℕ) : (arrayMeasure ν).real {ω : probSpace 𝓐 ℝ | Learning.pullCount (action alg) (bestArm ν) n ω = m₁ ∧ Learning.pullCount (action alg) a n ω = m₂ ∧ Learning.sumRewards (action alg) (reward alg) (bestArm ν) n ω ≤ Learning.sumRewards (action alg) (reward alg) a n ω} ≤ (streamMeasure ν).real {ω : ℕ → 𝓐 → ℝ | ∑ i ∈ Finset.range m₁, ω i (bestArm ν) ≤ ∑ i ∈ Finset.range m₂, ω i a}

theorem Bandits.sumRewards_eq_comp {𝓐 : Type u_1} {Ω : Type u_2} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {n : ℕ} {a : 𝓐} : Learning.sumRewards A R a n = (fun (p : ℕ → 𝓐 × ℝ) => ∑ i ∈ Finset.range n, if (p i).1 = a then (p i).2 else 0) ∘ fun (ω : Ω) (n : ℕ) => (A n ω, R n ω)

theorem Bandits.pullCount_eq_comp {𝓐 : Type u_1} {Ω : Type u_2} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {n : ℕ} {a : 𝓐} : Learning.pullCount A a n = (fun (p : ℕ → 𝓐 × ℝ) => ∑ i ∈ Finset.range n, if (p i).1 = a then 1 else 0) ∘ fun (ω : Ω) (n : ℕ) => (A n ω, R n ω)

theorem Learning.IsAlgEnvSeq.law_sumRewards_unique {𝓐 : Type u_1} {Ω : Type u_2} {Ω' : Type u_3} [DecidableEq 𝓐] {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {P' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure P'] {alg : Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {A₂ : ℕ → Ω' → 𝓐} {R₂ : ℕ → Ω' → ℝ} {n : ℕ} {a : 𝓐} [StandardBorelSpace 𝓐] [Nonempty 𝓐] (h1 : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (h2 : IsAlgEnvSeq A₂ R₂ alg (stationaryEnv ν) P') : MeasureTheory.Measure.map (sumRewards A R a n) P = MeasureTheory.Measure.map (sumRewards A₂ R₂ a n) P'

theorem Learning.IsAlgEnvSeq.law_pullCount_sumRewards_unique' {𝓐 : Type u_1} {Ω : Type u_2} {Ω' : Type u_3} [DecidableEq 𝓐] {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {P' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure P'] {alg : Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {A₂ : ℕ → Ω' → 𝓐} {R₂ : ℕ → Ω' → ℝ} {n : ℕ} [StandardBorelSpace 𝓐] [Nonempty 𝓐] (h1 : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (h2 : IsAlgEnvSeq A₂ R₂ alg (stationaryEnv ν) P') : ProbabilityTheory.IdentDistrib (fun (ω : Ω) (a : 𝓐) => (pullCount A a n ω, sumRewards A R a n ω)) (fun (ω : Ω') (a : 𝓐) => (pullCount A₂ a n ω, sumRewards A₂ R₂ a n ω)) P P'

theorem Learning.IsAlgEnvSeq.law_pullCount_sumRewards_unique {𝓐 : Type u_1} {Ω : Type u_2} {Ω' : Type u_3} [DecidableEq 𝓐] {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {P' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure P'] {alg : Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {A₂ : ℕ → Ω' → 𝓐} {R₂ : ℕ → Ω' → ℝ} {n : ℕ} {a : 𝓐} [StandardBorelSpace 𝓐] [Nonempty 𝓐] (h1 : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (h2 : IsAlgEnvSeq A₂ R₂ alg (stationaryEnv ν) P') : MeasureTheory.Measure.map (fun (ω : Ω) => (pullCount A a n ω, sumRewards A R a n ω)) P = MeasureTheory.Measure.map (fun (ω : Ω') => (pullCount A₂ a n ω, sumRewards A₂ R₂ a n ω)) P'

theorem Learning.IsAlgEnvSeq.identDistrib_pullCount_sumRewards {𝓐 : Type u_1} {Ω : Type u_2} {Ω' : Type u_3} [DecidableEq 𝓐] {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {P' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure P'] {alg : Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {A₂ : ℕ → Ω' → 𝓐} {R₂ : ℕ → Ω' → ℝ} [StandardBorelSpace 𝓐] [Nonempty 𝓐] (h1 : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (h2 : IsAlgEnvSeq A₂ R₂ alg (stationaryEnv ν) P') : ProbabilityTheory.IdentDistrib (fun (ω : Ω) (n : ℕ) (a : 𝓐) => (pullCount A a n ω, sumRewards A R a n ω)) (fun (ω' : Ω') (n : ℕ) (a : 𝓐) => (pullCount A₂ a n ω', sumRewards A₂ R₂ a n ω')) P P'

theorem Bandits.prob_pullCount_prod_sumRewards_mem_le {𝓐 : Type u_1} {Ω : Type u_2} [DecidableEq 𝓐] {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {n : ℕ} {a : 𝓐} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [Countable 𝓐] (h : Learning.IsAlgEnvSeq A R alg (Learning.stationaryEnv ν) P) {s : Set (ℕ × ℝ)} [DecidablePred fun (x : ℕ) => x ∈ Prod.fst '' s] (hs : MeasurableSet s) : P {ω : Ω | (Learning.pullCount A a n ω, Learning.sumRewards A R a n ω) ∈ s} ≤ ∑ k ∈ Finset.range (n + 1) with k ∈ Prod.fst '' s, (streamMeasure ν) {ω : ℕ → 𝓐 → ℝ | ∑ i ∈ Finset.range k, ω i a ∈ Prod.mk k ⁻¹' s}

theorem Bandits.prob_pullCount_mem_and_sumRewards_mem_le {𝓐 : Type u_1} {Ω : Type u_2} [DecidableEq 𝓐] {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {n : ℕ} {a : 𝓐} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [Countable 𝓐] (h : Learning.IsAlgEnvSeq A R alg (Learning.stationaryEnv ν) P) {s : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ s] (hs : MeasurableSet s) {B : Set ℝ} (hB : MeasurableSet B) : P {ω : Ω | Learning.pullCount A a n ω ∈ s ∧ Learning.sumRewards A R a n ω ∈ B} ≤ ∑ k ∈ Finset.range (n + 1) with k ∈ s, (streamMeasure ν) {ω : ℕ → 𝓐 → ℝ | ∑ i ∈ Finset.range k, ω i a ∈ B}

theorem Bandits.prob_sumRewards_mem_le {𝓐 : Type u_1} {Ω : Type u_2} [DecidableEq 𝓐] {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {n : ℕ} {a : 𝓐} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [Countable 𝓐] (h : Learning.IsAlgEnvSeq A R alg (Learning.stationaryEnv ν) P) {B : Set ℝ} (hB : MeasurableSet B) : P (Learning.sumRewards A R a n ⁻¹' B) ≤ ∑ k ∈ Finset.range (n + 1), (streamMeasure ν) {ω : ℕ → 𝓐 → ℝ | ∑ i ∈ Finset.range k, ω i a ∈ B}

theorem Bandits.prob_pullCount_eq_and_sumRewards_mem_le {𝓐 : Type u_1} {Ω : Type u_2} [DecidableEq 𝓐] {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {n : ℕ} {a : 𝓐} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [Countable 𝓐] (h : Learning.IsAlgEnvSeq A R alg (Learning.stationaryEnv ν) P) {m : ℕ} (hm : m ≤ n) {B : Set ℝ} (hB : MeasurableSet B) : P {ω : Ω | Learning.pullCount A a n ω = m ∧ Learning.sumRewards A R a n ω ∈ B} ≤ (streamMeasure ν) {ω : ℕ → 𝓐 → ℝ | ∑ i ∈ Finset.range m, ω i a ∈ B}

theorem Bandits.prob_exists_pullCount_eq_and_sumRewards_mem_le {𝓐 : Type u_1} {Ω : Type u_2} [DecidableEq 𝓐] {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [Countable 𝓐] (h : Learning.IsAlgEnvSeq A R alg (Learning.stationaryEnv ν) P) (a : 𝓐) (m : ℕ) {B : Set ℝ} (hB : MeasurableSet B) : P {ω : Ω | ∃ (n : ℕ), Learning.pullCount A a n ω = m ∧ Learning.sumRewards A R a n ω ∈ B} ≤ (streamMeasure ν) {ω : ℕ → 𝓐 → ℝ | ∑ i ∈ Finset.range m, ω i a ∈ B}

theorem Bandits.probReal_sumRewards_le_sumRewards_le {𝓐 : Type u_1} {Ω : Type u_2} [DecidableEq 𝓐] {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [Fintype 𝓐] (h : Learning.IsAlgEnvSeq A R alg (Learning.stationaryEnv ν) P) (a : 𝓐) (n m₁ m₂ : ℕ) : P.real {ω : Ω | Learning.pullCount A (bestArm ν) n ω = m₁ ∧ Learning.pullCount A a n ω = m₂ ∧ Learning.sumRewards A R (bestArm ν) n ω ≤ Learning.sumRewards A R a n ω} ≤ (streamMeasure ν).real {ω : ℕ → 𝓐 → ℝ | ∑ i ∈ Finset.range m₁, ω i (bestArm ν) ≤ ∑ i ∈ Finset.range m₂, ω i a}

theorem Bandits.StreamMeasure.prob_sum_range_sub_ge_le_of_HasSubgaussianMGF {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] {a : 𝓐} {σ2 : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF (fun (x : ℝ) => x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a)) {ε : ℝ} (hε : 0 ≤ ε) (n : ℕ) : (streamMeasure ν) {ω : ℕ → 𝓐 → ℝ | ε ≤ ∑ k ∈ Finset.range n, (ω k a - ∫ (x : ℝ), id x ∂ν a)} ≤ ENNReal.ofReal (Real.exp (-ε ^ 2 / (2 * ↑n * ↑σ2)))

theorem Bandits.StreamMeasure.prob_sum_range_sub_le_le_of_HasSubgaussianMGF {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] {a : 𝓐} {σ2 : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF (fun (x : ℝ) => x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a)) {ε : ℝ} (hε : 0 ≤ ε) (n : ℕ) : (streamMeasure ν) {ω : ℕ → 𝓐 → ℝ | ∑ k ∈ Finset.range n, (ω k a - ∫ (x : ℝ), id x ∂ν a) ≤ -ε} ≤ ENNReal.ofReal (Real.exp (-ε ^ 2 / (2 * ↑n * ↑σ2)))

theorem Bandits.StreamMeasure.prob_sum_range_sub_ge_le_of_HasSubgaussianMGF' {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] {n : ℕ} {a : 𝓐} {σ2 : NNReal} (hσ2 : 0 < σ2) (h : ProbabilityTheory.HasSubgaussianMGF (fun (x : ℝ) => x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a)) {δ : ℝ} (hδ : 0 < δ) (hn : 0 < n) : (streamMeasure ν) {ω : ℕ → 𝓐 → ℝ | √(2 * ↑n * ↑σ2 * Real.log (1 / δ)) ≤ ∑ k ∈ Finset.range n, (ω k a - ∫ (x : ℝ), id x ∂ν a)} ≤ ENNReal.ofReal δ

theorem Bandits.StreamMeasure.prob_sum_range_sub_le_le_of_HasSubgaussianMGF' {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] {n : ℕ} {a : 𝓐} {σ2 : NNReal} (hσ2 : 0 < σ2) (h : ProbabilityTheory.HasSubgaussianMGF (fun (x : ℝ) => x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a)) {δ : ℝ} (hδ : 0 < δ) (hn : 0 < n) : (streamMeasure ν) {ω : ℕ → 𝓐 → ℝ | ∑ k ∈ Finset.range n, (ω k a - ∫ (x : ℝ), id x ∂ν a) ≤ -√(2 * ↑n * ↑σ2 * Real.log (1 / δ))} ≤ ENNReal.ofReal δ

theorem Bandits.prob_sumRewards_sub_pullCount_mul_ge_le {𝓐 : Type u_1} {Ω : Type u_2} [DecidableEq 𝓐] {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {n : ℕ} {a : 𝓐} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [Countable 𝓐] {σ2 : NNReal} (hσ2 : 0 < σ2) (ha : ProbabilityTheory.HasSubgaussianMGF (fun (x : ℝ) => x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a)) (h : Learning.IsAlgEnvSeq A R alg (Learning.stationaryEnv ν) P) {δ : ℝ} (hδ : 0 < δ) : P {ω : Ω | ∃ t < n, Learning.pullCount A a t ω ≠ 0 ∧ √(2 * ↑(Learning.pullCount A a t ω) * ↑σ2 * Real.log (1 / δ)) ≤ Learning.sumRewards A R a t ω - ↑(Learning.pullCount A a t ω) * ∫ (x : ℝ), id x ∂ν a} ≤ ENNReal.ofReal ((↑n - 1) * δ)

theorem Bandits.prob_sumRewards_sub_pullCount_mul_le_le {𝓐 : Type u_1} {Ω : Type u_2} [DecidableEq 𝓐] {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {n : ℕ} {a : 𝓐} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [Countable 𝓐] {σ2 : NNReal} (hσ2 : 0 < σ2) (ha : ProbabilityTheory.HasSubgaussianMGF (fun (x : ℝ) => x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a)) (h : Learning.IsAlgEnvSeq A R alg (Learning.stationaryEnv ν) P) {δ : ℝ} (hδ : 0 < δ) : P {ω : Ω | ∃ t < n, Learning.pullCount A a t ω ≠ 0 ∧ Learning.sumRewards A R a t ω - ↑(Learning.pullCount A a t ω) * ∫ (x : ℝ), id x ∂ν a ≤ -√(2 * ↑(Learning.pullCount A a t ω) * ↑σ2 * Real.log (1 / δ))} ≤ ENNReal.ofReal ((↑n - 1) * δ)

theorem Bandits.prob_sumRewards_sub_pullCount_mul_ge_le_of_Fintype {𝓐 : Type u_1} {Ω : Type u_2} [DecidableEq 𝓐] {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {n : ℕ} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [Fintype 𝓐] {σ2 : NNReal} (hσ2 : 0 < σ2) (hν : ∀ (a : 𝓐), ProbabilityTheory.HasSubgaussianMGF (fun (x : ℝ) => x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a)) (h : Learning.IsAlgEnvSeq A R alg (Learning.stationaryEnv ν) P) {δ : ℝ} (hδ : 0 < δ) : P {ω : Ω | ∃ (a : 𝓐), ∃ t < n, Learning.pullCount A a t ω ≠ 0 ∧ √(2 * ↑(Learning.pullCount A a t ω) * ↑σ2 * Real.log (1 / δ)) ≤ Learning.sumRewards A R a t ω - ↑(Learning.pullCount A a t ω) * ∫ (x : ℝ), id x ∂ν a} ≤ ENNReal.ofReal (↑(Fintype.card 𝓐) * (↑n - 1) * δ)

theorem Bandits.probReal_sum_le_sum_streamMeasure {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] [Nonempty 𝓐] [Fintype 𝓐] {c : NNReal} (hν : ∀ (a : 𝓐), ProbabilityTheory.HasSubgaussianMGF (fun (x : ℝ) => x - ∫ (x : ℝ), id x ∂ν a) c (ν a)) (a : 𝓐) (m : ℕ) : (streamMeasure ν).real {ω : ℕ → 𝓐 → ℝ | ∑ s ∈ Finset.range m, ω s (bestArm ν) ≤ ∑ s ∈ Finset.range m, ω s a} ≤ Real.exp (-↑m * gap ν a ^ 2 / (4 * ↑c))

theorem Bandits.prob_sum_le_sqrt_log {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] {n : ℕ} {σ2 : NNReal} (hν : ∀ (a : 𝓐), ProbabilityTheory.HasSubgaussianMGF (fun (x : ℝ) => x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a)) (hσ2 : σ2 ≠ 0) {c : ℝ} (hc : 0 ≤ c) (a : 𝓐) (k : ℕ) (hk : k ≠ 0) : (streamMeasure ν) {ω : ℕ → 𝓐 → ℝ | ∑ s ∈ Finset.range k, (ω s a - ∫ (x : ℝ), id x ∂ν a) ≤ -√(2 * c * ↑k * ↑σ2 * Real.log (↑n + 1))} ≤ 1 / (↑n + 1) ^ c

theorem Bandits.prob_sum_ge_sqrt_log {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] {n : ℕ} {σ2 : NNReal} (hν : ∀ (a : 𝓐), ProbabilityTheory.HasSubgaussianMGF (fun (x : ℝ) => x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a)) (hσ2 : σ2 ≠ 0) {c : ℝ} (hc : 0 ≤ c) (a : 𝓐) (k : ℕ) (hk : k ≠ 0) : (streamMeasure ν) {ω : ℕ → 𝓐 → ℝ | √(2 * c * ↑k * ↑σ2 * Real.log (↑n + 1)) ≤ ∑ s ∈ Finset.range k, (ω s a - ∫ (x : ℝ), id x ∂ν a)} ≤ 1 / (↑n + 1) ^ c

theorem Bandits.prob_avg_add_sqrt_log_le {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] {σ2 : NNReal} {c : ℝ} (hν : ∀ (a : 𝓐), ProbabilityTheory.HasSubgaussianMGF (fun (x : ℝ) => x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a)) (hσ2 : σ2 ≠ 0) (hc : 0 ≤ c) (a : 𝓐) (n k : ℕ) (hk : k ≠ 0) : (streamMeasure ν) {ω : ℕ → 𝓐 → ℝ | (∑ m ∈ Finset.range k, ω m a) / ↑k + √(2 * c * ↑σ2 * Real.log (↑n + 1) / ↑k) ≤ ∫ (x : ℝ), id x ∂ν a} ≤ 1 / (↑n + 1) ^ c

theorem Bandits.prob_avg_sub_sqrt_log_ge {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] {σ2 : NNReal} {c : ℝ} (hν : ∀ (a : 𝓐), ProbabilityTheory.HasSubgaussianMGF (fun (x : ℝ) => x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a)) (hσ2 : σ2 ≠ 0) (hc : 0 ≤ c) (a : 𝓐) (n k : ℕ) (hk : k ≠ 0) : (streamMeasure ν) {ω : ℕ → 𝓐 → ℝ | ∫ (x : ℝ), id x ∂ν a ≤ (∑ m ∈ Finset.range k, ω m a) / ↑k - √(2 * c * ↑σ2 * Real.log (↑n + 1) / ↑k)} ≤ 1 / (↑n + 1) ^ c

theorem Learning.IsBayesAlgEnvSeq.prob_empMean_sub_actionMean_ge_le {𝓔 : 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, ∃ (a : Fin K), pullCount A a t ω ≠ 0 ∧ √(2 * ↑σ2 * Real.log (1 / δ) / ↑(pullCount A a t ω)) ≤ empMean A R a t ω - actionMean κ E a ω} ≤ ENNReal.ofReal (↑K * (↑n - 1) * δ)

theorem Learning.IsBayesAlgEnvSeq.prob_empMean_bestAction_sub_actionMean_le_le {𝓔 : 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) * δ)