Reorder arguments

Author: paulorauber

LeanBandits/BanditAlgorithms/TS.lean

@@ -20,7 +20,7 @@ variable (κ : Kernel (Fin K × E) ℝ) [IsMarkovKernel κ]
 
 noncomputable
 def tsPosterior (n : ℕ) : Kernel (Iic n → (Fin K) × ℝ) E :=
-  Learning.Bayes.posterior Q κ n (uniformAlgorithm hK)
+  Learning.Bayes.posterior Q κ (uniformAlgorithm hK) n
 
 noncomputable
 def isMarkovKernel_tsPosterior (n : ℕ) : IsMarkovKernel (tsPosterior hK Q κ n) := by

LeanBandits/SequentialLearning/BayesStationaryEnv.lean

@@ -38,12 +38,12 @@ def hist (n : ℕ) (ω : ℕ → α × E × R) : Iic n → α × R :=  fun i ↦
 def env (ω : ℕ → α × E × R) : E := (ω 0).2.1
 
 noncomputable
-def posterior [StandardBorelSpace E] [Nonempty E] (n : ℕ) (alg : Algorithm α R) :
+def posterior [StandardBorelSpace E] [Nonempty E] (alg : Algorithm α R) (n : ℕ) :
     Kernel (Iic n → α × R) E :=
   condDistrib env (hist n) (trajMeasure Q κ alg)
 
-instance [StandardBorelSpace E] [Nonempty E] (n : ℕ) (alg : Algorithm α R) :
-    IsMarkovKernel (posterior Q κ n alg) := by
+instance [StandardBorelSpace E] [Nonempty E] (alg : Algorithm α R) (n : ℕ) :
+    IsMarkovKernel (posterior Q κ alg n) := by
   unfold posterior
   infer_instance