Martingale decomposition of the sum of rewards #

source

noncomputable def Learning.noiseSum {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] (env : Environment 𝓞 𝓐 𝓨) (O : ℕ → Ω → 𝓞) (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (k : 𝓐) (n : ℕ) (ω : Ω) :

𝓨

The sum of noise terms for action k. This is the martingale part of sumRewards A Y k for the filtration IsAlgEnvSeq.filtrationAction.

Equations

Learning.noiseSum env O A Y k n ω = ∑ m ∈ Finset.range n, {ω : Ω | A m ω = k}.indicator (fun (ω : Ω) => Y m ω - env.means O A Y (A m ω) m ω) ω

Instances For

source

noncomputable def Learning.meanSum {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] (env : Environment 𝓞 𝓐 𝓨) (O : ℕ → Ω → 𝓞) (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (k : 𝓐) (n : ℕ) (ω : Ω) :

𝓨

The sum of mean terms for action k. This is the predictable part of sumRewards A Y k for the filtration IsAlgEnvSeq.filtrationAction.

Equations

Learning.meanSum env O A Y k n ω = ∑ m ∈ Finset.range n, {ω : Ω | A m ω = k}.indicator (fun (ω : Ω) => env.means O A Y (A m ω) m ω) ω

Instances For

source

theorem Learning.noiseSum_add_meanSum' {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {env : Environment 𝓞 𝓐 𝓨} (k : 𝓐) (n : ℕ) (ω : Ω) :

noiseSum env O A Y k n ω + meanSum env O A Y k n ω = ∑ m ∈ Finset.range n, {ω : Ω | A m ω = k}.indicator (Y m) ω

source

theorem Learning.noiseSum_add_meanSum {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {env : Environment 𝓞 𝓐 𝓨} [DecidableEq 𝓐] (k : 𝓐) (n : ℕ) (ω : Ω) :

noiseSum env O A Y k n ω + meanSum env O A Y k n ω = sumRewards A Y k n ω

source

@[simp]

theorem Learning.noiseSum_zero {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {env : Environment 𝓞 𝓐 𝓨} (k : 𝓐) :

noiseSum env O A Y k 0 = fun (x : Ω) => 0

source

@[simp]

theorem Learning.meanSum_zero {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {env : Environment 𝓞 𝓐 𝓨} (k : 𝓐) :

meanSum env O A Y k 0 = fun (x : Ω) => 0

source

theorem Learning.noiseSum_succ {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {env : Environment 𝓞 𝓐 𝓨} (k : 𝓐) (n : ℕ) :

noiseSum env O A Y k (n + 1) = noiseSum env O A Y k n + {ω : Ω | A n ω = k}.indicator fun (ω : Ω) => Y n ω - env.means O A Y (A n ω) n ω

source

theorem Learning.noiseSum_succ_sub {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {env : Environment 𝓞 𝓐 𝓨} (k : 𝓐) (n : ℕ) (ω : Ω) :

noiseSum env O A Y k (n + 1) ω - noiseSum env O A Y k n ω = {ω : Ω | A n ω = k}.indicator (fun (ω : Ω) => Y n ω - env.means O A Y (A n ω) n ω) ω

source

theorem Learning.meanSum_succ {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {env : Environment 𝓞 𝓐 𝓨} (k : 𝓐) (n : ℕ) :

meanSum env O A Y k (n + 1) = meanSum env O A Y k n + {ω : Ω | A n ω = k}.indicator fun (ω : Ω) => env.means O A Y (A n ω) n ω

source

theorem Learning.meanSum_succ_sub {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {env : Environment 𝓞 𝓐 𝓨} (k : 𝓐) (n : ℕ) (ω : Ω) :

meanSum env O A Y k (n + 1) ω - meanSum env O A Y k n ω = {ω : Ω | A n ω = k}.indicator (fun (ω : Ω) => env.means O A Y (A n ω) n ω) ω

source

theorem Learning.IsAlgEnvSeq.integrable_noiseSum_increment {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} [MeasurableSingletonClass 𝓐] [SecondCountableTopology 𝓨] [OpensMeasurableSpace 𝓨] {m : ℕ} (h : IsAlgEnvSeq O A Y alg env P) (hint : MeasureTheory.Integrable (Y m) P) (k : 𝓐) :

MeasureTheory.Integrable (fun (ω : Ω) => {ω : Ω | A m ω = k}.indicator (fun (ω : Ω) => Y m ω - env.means O A Y (A m ω) m ω) ω) P

source

theorem Learning.IsAlgEnvSeq.integrable_meanSum_increment {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} [MeasurableSingletonClass 𝓐] [SecondCountableTopology 𝓨] [OpensMeasurableSpace 𝓨] {m : ℕ} (h : IsAlgEnvSeq O A Y alg env P) (hint : MeasureTheory.Integrable (Y m) P) (k : 𝓐) :

MeasureTheory.Integrable (fun (ω : Ω) => {ω : Ω | A m ω = k}.indicator (fun (ω : Ω) => env.means O A Y (A m ω) m ω) ω) P

source

theorem Learning.IsAlgEnvSeq.integrable_noiseSum {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} [MeasurableSingletonClass 𝓐] [SecondCountableTopology 𝓨] [OpensMeasurableSpace 𝓨] (h : IsAlgEnvSeq O A Y alg env P) (hint : ∀ (n : ℕ), MeasureTheory.Integrable (Y n) P) (k : 𝓐) (n : ℕ) :

MeasureTheory.Integrable (noiseSum env O A Y k n) P

source

theorem Learning.IsAlgEnvSeq.integrable_meanSum {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} [MeasurableSingletonClass 𝓐] [SecondCountableTopology 𝓨] [OpensMeasurableSpace 𝓨] (h : IsAlgEnvSeq O A Y alg env P) (hint : ∀ (n : ℕ), MeasureTheory.Integrable (Y n) P) (k : 𝓐) (n : ℕ) :

MeasureTheory.Integrable (meanSum env O A Y k n) P

source

theorem Learning.IsAlgEnvSeq.memLp_noiseSum_increment {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} [MeasurableSingletonClass 𝓐] [SecondCountableTopology 𝓨] [BorelSpace 𝓨] {m : ℕ} (k : 𝓐) (h : IsAlgEnvSeq O A Y alg env P) {p : ENNReal} (hp1 : 1 ≤ p) (hp_top : p ≠ ⊤) (hY : MeasureTheory.MemLp (Y m) p P) :

MeasureTheory.MemLp ({ω : Ω | A m ω = k}.indicator fun (ω : Ω) => Y m ω - env.means O A Y (A m ω) m ω) p P

source

theorem Learning.IsAlgEnvSeq.memLp_meanSum_increment {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} [MeasurableSingletonClass 𝓐] [SecondCountableTopology 𝓨] [BorelSpace 𝓨] {m : ℕ} (k : 𝓐) (h : IsAlgEnvSeq O A Y alg env P) {p : ENNReal} (hp1 : 1 ≤ p) (hp_top : p ≠ ⊤) (hY : MeasureTheory.MemLp (Y m) p P) :

MeasureTheory.MemLp ({ω : Ω | A m ω = k}.indicator fun (ω : Ω) => env.means O A Y (A m ω) m ω) p P

source

theorem Learning.IsAlgEnvSeq.memLp_noiseSum {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} [MeasurableSingletonClass 𝓐] [SecondCountableTopology 𝓨] [BorelSpace 𝓨] (h : IsAlgEnvSeq O A Y alg env P) {p : ENNReal} (hp1 : 1 ≤ p) (hp_top : p ≠ ⊤) (hY : ∀ (n : ℕ), MeasureTheory.MemLp (Y n) p P) (k : 𝓐) (n : ℕ) :

MeasureTheory.MemLp (noiseSum env O A Y k n) p P

source

theorem Learning.IsAlgEnvSeq.memLp_meanSum {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} [MeasurableSingletonClass 𝓐] [SecondCountableTopology 𝓨] [BorelSpace 𝓨] (h : IsAlgEnvSeq O A Y alg env P) {p : ENNReal} (hp1 : 1 ≤ p) (hp_top : p ≠ ⊤) (hY : ∀ (n : ℕ), MeasureTheory.MemLp (Y n) p P) (k : 𝓐) (n : ℕ) :

MeasureTheory.MemLp (meanSum env O A Y k n) p P

source

theorem Learning.IsAlgEnvSeq.adapted_noiseSum {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} [MeasurableSingletonClass 𝓐] [SecondCountableTopology 𝓨] [BorelSpace 𝓨] (h : IsAlgEnvSeq O A Y alg env P) (k : 𝓐) :

MeasureTheory.Adapted h.filtrationAction (noiseSum env O A Y k)

source

theorem Learning.IsAlgEnvSeq.stronglyAdapted_noiseSum {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} [MeasurableSingletonClass 𝓐] [SecondCountableTopology 𝓨] [BorelSpace 𝓨] (h : IsAlgEnvSeq O A Y alg env P) (k : 𝓐) :

MeasureTheory.StronglyAdapted h.filtrationAction (noiseSum env O A Y k)

source

theorem Learning.IsAlgEnvSeq.isStronglyPredictable_meanSum {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} [MeasurableSingletonClass 𝓐] [SecondCountableTopology 𝓨] [BorelSpace 𝓨] (h : IsAlgEnvSeq O A Y alg env P) (k : 𝓐) :

MeasureTheory.IsStronglyPredictable h.filtrationAction (meanSum env O A Y k)

source

theorem Learning.IsAlgEnvSeq.condExp_noiseSum_increment {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} [MeasurableSingletonClass 𝓐] [SecondCountableTopology 𝓨] [BorelSpace 𝓨] [CompleteSpace 𝓨] (h : IsAlgEnvSeq O A Y alg env P) (k : 𝓐) (i : ℕ) (hint : MeasureTheory.Integrable (Y i) P) :

P[{ω : Ω | A i ω = k}.indicator fun (ω : Ω) => Y i ω - env.means O A Y (A i ω) i ω | ↑h.filtrationAction i] =ᵐ[P] 0

source

theorem Learning.IsAlgEnvSeq.martingale_noiseSum {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [NormedSpace ℝ 𝓨] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} [MeasurableSingletonClass 𝓐] [SecondCountableTopology 𝓨] [BorelSpace 𝓨] [CompleteSpace 𝓨] (h : IsAlgEnvSeq O A Y alg env P) (hint : ∀ (n : ℕ), MeasureTheory.Integrable (Y n) P) (k : 𝓐) :

MeasureTheory.Martingale (noiseSum env O A Y k) h.filtrationAction P

Documentation

LeanMachineLearning.SequentialLearning.FeedbackMartingale

Martingale decomposition of the sum of rewards #