Blueprint update

LeanBandits/Bandit/Bandit.lean

@@ -44,7 +44,7 @@ lemma snd_stepKernel (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel 
 /-- Measure on the sequence of arms pulled and rewards observed generated by the bandit. -/
 noncomputable
 def trajMeasure (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] : Measure (ℕ → α × R) :=
-  Kernel.trajMeasure (alg.p0 ⊗ₘ ν) (stepKernel alg ν)
+  Learning.trajMeasure alg (stationaryEnv ν)
 deriving IsProbabilityMeasure
 
 /-- Measure of an infinite stream of rewards from each arm. -/

blueprint/lean_decls

@@ -1,38 +1,86 @@
 Learning.Algorithm
 Learning.Environment
+Learning.detAlgorithm
+Learning.stationaryEnv
 ProbabilityTheory.Kernel.traj
 ProbabilityTheory.Kernel.trajMeasure
+Learning.step
+Learning.hist
+Learning.filtration
+Learning.adapted_step
+Learning.adapted_hist
 ProbabilityTheory.Kernel.condDistrib_trajMeasure
+Learning.hasLaw_step_zero
+Learning.action
+Learning.reward
+Learning.adapted_action
+Learning.adapted_reward
 Learning.condDistrib_action
 Learning.condDistrib_reward
 Learning.hasLaw_action_zero
 Learning.condDistrib_reward_zero
-Bandits.Bandit.measure
-Bandits.arm
-Bandits.reward
-Bandits.hist
+Learning.condDistrib_reward_stationaryEnv
+Learning.condIndepFun_reward_hist_action
 Learning.pullCount
-Bandits.filtration
-Bandits.condDistrib_reward
-Bandits.hasLaw_arm_zero
-Bandits.condDistrib_arm
+Learning.pullCount_zero
+Learning.pullCount_mono
+Learning.pullCount_add_one
+Learning.pullCount_le
+Learning.pullCount_congr
+Learning.isPredictable_pullCount
 Learning.stepsUntil
-Learning.rewardByCount
-Bandits.hasLaw_rewardByCount
-Bandits.iIndepFun_rewardByCount
+Learning.stepsUntil_zero_of_ne
+Learning.stepsUntil_zero_of_eq
 Learning.stepsUntil_pullCount_le
 Learning.stepsUntil_pullCount_eq
+Learning.action_stepsUntil
+Learning.pullCount_stepsUntil_add_one
+Learning.pullCount_stepsUntil
+Learning.isStoppingTime_stepsUntil
+Learning.rewardByCount
 Learning.rewardByCount_pullCount_add_one_eq_reward
+Learning.sumRewards
+Learning.empMean
 Learning.sum_rewardByCount_eq_sumRewards
+Bandits.Bandit.trajMeasure
+Bandits.Bandit.measure
+Bandits.measurable_comap_indicator_stepsUntil_eq
+ProbabilityTheory.CondIndepFun.prod_right
+Bandits.condIndepFun_reward_stepsUntil_arm
+Bandits.reward_cond_stepsUntil
+ProbabilityTheory.condDistrib_ae_eq_cond
+Bandits.condDistrib_rewardByCount_stepsUntil
+Bandits.hasLaw_rewardByCount
+ProbabilityTheory.iIndepFun_nat_iff_forall_indepFun
+Bandits.iIndepFun_rewardByCount'
+Bandits.identDistrib_rewardByCount_stream
+Bandits.identDistrib_sum_Icc_rewardByCount
 Bandits.regret
 Bandits.gap
+Learning.sum_pullCount_mul
 Bandits.regret_eq_sum_pullCount_mul_gap
 ProbabilityTheory.HasSubgaussianMGF
 ProbabilityTheory.HasSubgaussianMGF.add_of_indepFun
 ProbabilityTheory.HasSubgaussianMGF.measure_ge_le
 ProbabilityTheory.HasSubgaussianMGF.measure_sum_range_ge_le_of_iIndepFun
+ProbabilityTheory.HasSubgaussianMGF.measure_sum_le_sum_le'
 Bandits.ETC.nextArm
 Bandits.etcAlgorithm
 Bandits.ETC.pullCount_of_ge
+Bandits.ETC.sumRewards_bestArm_le_of_arm_mul_eq
 Bandits.ETC.prob_arm_mul_eq_le
-Bandits.ETC.regret_le
+Bandits.ETC.regret_le
+Bandits.UCB.nextArm
+Bandits.ucbAlgorithm
+Bandits.UCB.ucbIndex_le_ucbIndex_arm
+Bandits.UCB.gap_arm_le_two_mul_ucbWidth
+Bandits.UCB.pullCount_arm_le
+Bandits.UCB.todo
+Bandits.UCB.todo'
+Bandits.UCB.prob_ucbIndex_le
+Bandits.UCB.prob_ucbIndex_ge
+Bandits.UCB.pullCount_le_add_three
+Bandits.UCB.pullCount_le_add_three_ae
+Bandits.UCB.some_sum_eq_zero
+Bandits.UCB.expectation_pullCount_le
+Bandits.UCB.regret_le

blueprint/src/appendix/conditional_independence.tex

@@ -0,0 +1,45 @@
+\chapter{Conditional independence}
+
+
+\begin{lemma}\label{lem:CondIndepFun.prod_right}
+  \leanok
+  \lean{ProbabilityTheory.CondIndepFun.prod_right}
+If $X \ind Y \mid Z$, then $X \ind (Y, Z) \mid Z$.
+\end{lemma}
+
+\begin{proof}
+
+\end{proof}
+
+
+\begin{lemma}[Contraction]\label{lem:indepFun_contraction}
+If $X \ind Y \mid Z$ and $X \ind Z$, then $X \ind (Y, Z)$.
+\end{lemma}
+
+\begin{proof}
+It suffices to show that $\mathcal{L}(X \mid Y, Z) = \mathcal{L}(X)$.
+By conditional independence, $\mathcal{L}(X \mid Y, Z) = \mathcal{L}(X \mid Z)$.
+By independence, $\mathcal{L}(X \mid Z) = \mathcal{L}(X)$.
+\end{proof}
+
+
+\begin{lemma}\label{lem:condIndepFun_contraction}
+If $X \ind Y \mid Z, W$ and $X \ind Z \mid W$, then $X \ind (Y, Z) \mid W$.
+\end{lemma}
+
+\begin{proof}
+It suffices to show that $\mathcal{L}(X \mid Y, Z, W) = \mathcal{L}(X \mid W)$.
+By the first hypothesis, $\mathcal{L}(X \mid Y, Z, W) = \mathcal{L}(X \mid Z, W)$.
+By the second hypothesis, $\mathcal{L}(X \mid Z, W) = \mathcal{L}(X \mid W)$.
+\end{proof}
+
+
+\begin{lemma}\label{lem:iIndepFun_nat_iff_forall_indepFun}
+  \leanok
+  \lean{ProbabilityTheory.iIndepFun_nat_iff_forall_indepFun}
+A family of random variables $(X_i)_{i \in \mathbb{N}}$ is independent if and only if for all $n \in \mathbb{N}$, $X_{n+1}$ is independent of $(X_0, \ldots, X_n)$.
+\end{lemma}
+
+\begin{proof}\leanok
+
+\end{proof}