Martingale and predictable parts of sumRewards

LeanMachineLearning.lean

@@ -13,6 +13,7 @@ public import LeanMachineLearning.ForMathlib.Probability.Independence.IndepFun
 public import LeanMachineLearning.ForMathlib.Probability.Independence.IndepInfinitePi
 public import LeanMachineLearning.ForMathlib.Probability.Integrable
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.Basic
+public import LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.IntegralCompProd
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.MapComap
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.MeasureCompProd
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.IonescuTulcea.Traj
@@ -29,6 +30,7 @@ public import LeanMachineLearning.Online.Bandit.BayesRegret
 public import LeanMachineLearning.Online.Bandit.Regret
 public import LeanMachineLearning.Online.Bandit.RewardByCountMeasure
 public import LeanMachineLearning.Online.Bandit.SumRewards
+public import LeanMachineLearning.SequentialLearning.ActionIndicator
 public import LeanMachineLearning.SequentialLearning.Algorithm
 public import LeanMachineLearning.SequentialLearning.AlgorithmDensity
 public import LeanMachineLearning.SequentialLearning.AlgorithmDensityBayes
@@ -39,9 +41,12 @@ public import LeanMachineLearning.SequentialLearning.Algorithms.Uniform
 public import LeanMachineLearning.SequentialLearning.BayesStationaryEnv
 public import LeanMachineLearning.SequentialLearning.Deterministic
 public import LeanMachineLearning.SequentialLearning.EvaluationEnv
+public import LeanMachineLearning.SequentialLearning.FeedbackMartingale
 public import LeanMachineLearning.SequentialLearning.FiniteActions
 public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
+public import LeanMachineLearning.SequentialLearning.Means
 public import LeanMachineLearning.SequentialLearning.StationaryEnv
+public import LeanMachineLearning.SequentialLearning.SumRewards
 public import LeanMachineLearning.Tactic.EqLift
 public import LeanMachineLearning.Tactic.EqLift.ForMathlib.Kernel
 public import LeanMachineLearning.Tactic.EqLift.ForMathlib.MeasurableEquiv

LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean

@@ -129,6 +129,13 @@ lemma HasLaw.prod_of_hasCondDistrib {P : Measure β}
     HasLaw (fun ω ↦ (X ω, Y ω)) (P ⊗ₘ κ) μ :=
   ⟨by fun_prop, by rw [h2.map_eq, h1.map_eq]⟩
 
+lemma HasCondDistrib.hasLaw_comp [SFinite μ] [IsSFiniteKernel κ] (h : HasCondDistrib Y X κ μ) :
+    HasLaw Y (κ ∘ₘ (μ.map X)) μ := by
+  refine ⟨by fun_prop, ?_⟩
+  rw [← Measure.snd_compProd, ← h.map_eq, Measure.snd,
+    AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
+  rfl
+
 lemma HasCondDistrib.prod {Z : α → Ω'} {η : Kernel (β × Ω) Ω'}
     (h1 : HasCondDistrib Y X κ μ) (h2 : HasCondDistrib Z (fun ω ↦ (X ω, Y ω)) η μ) :
     HasCondDistrib (fun ω ↦ (Y ω, Z ω)) X (κ ⊗ₖ η) μ := by

LeanMachineLearning/ForMathlib/Probability/Kernel/Composition/IntegralCompProd.lean

@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import Mathlib.Probability.Kernel.Composition.IntegralCompProd
+
+import Mathlib.Analysis.Convex.Integral
+
+/-!
+# Lp functions with respect to a composition of kernels and measures
+-/
+
+@[expose] public section
+
+open ProbabilityTheory
+open scoped ENNReal
+
+namespace MeasureTheory
+
+protected lemma Measure.memLp_comp_iff
+    {α β E : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [NormedAddCommGroup E]
+    {κ : Kernel α β} {μ : Measure α} {f : β → E} {p : ℝ≥0∞} (hp0 : p ≠ 0) (hp_top : p ≠ ∞)
+    (hf : AEStronglyMeasurable f (κ ∘ₘ μ)) :
+    MemLp f p (κ ∘ₘ μ)
+      ↔ (∀ᵐ x ∂μ, MemLp f p (κ x)) ∧ Integrable (fun x ↦ ∫ y, ‖f y‖ ^ p.toReal ∂κ x) μ := by
+    rw [← integrable_norm_rpow_iff (by fun_prop) hp0 hp_top, Measure.integrable_comp_iff]
+    swap; · exact (hf.norm.aemeasurable.pow_const p.toReal).aestronglyMeasurable
+    -- todo extract
+    unfold AEStronglyMeasurable at hf
+    obtain ⟨g, hg, hfg⟩ := hf
+    obtain hfg' := Measure.ae_ae_of_ae_comp hfg
+    have hf' : ∀ᵐ ω ∂μ, AEStronglyMeasurable f (κ ω) := by
+      filter_upwards [hfg'] with ω hω using ⟨g, hg, hω⟩
+    --
+    congr! 1
+    · suffices ∀ᵐ x ∂μ, Integrable (fun x ↦ ‖f x‖ ^ p.toReal) (κ x) ↔ MemLp f p (κ x) by
+        refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+          <;> filter_upwards [h, this] with x hx h_iff
+        · rwa [h_iff] at hx
+        · rwa [← h_iff] at hx
+      filter_upwards [hf'] with ω hω
+      rw [integrable_norm_rpow_iff hω hp0 hp_top]
+    · congr! 4 with y
+      simp only [Real.norm_eq_abs, abs_eq_self]
+      positivity
+
+/-- **Jensen's inequality** for the convex function `x ↦ ‖x‖ ^ p`, `1 ≤ p`. -/
+lemma norm_integral_rpow_le_integral_norm_rpow
+    {α E : Type*} {mα : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ]
+    [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → E} {p : ℝ≥0∞}
+    (hp1 : 1 ≤ p) (hp_top : p ≠ ∞) (hf : MemLp f p μ) :
+    ‖∫ x, f x ∂μ‖ ^ p.toReal ≤ ∫ x, ‖f x‖ ^ p.toReal ∂μ := by
+  have hp0 : p ≠ 0 := by positivity
+  have hp1' : 1 ≤ p.toReal := by simpa using ENNReal.toReal_mono hp_top hp1
+  calc ‖∫ x, f x ∂μ‖ ^ p.toReal
+  _ ≤ (∫ x, ‖f x‖ ∂μ) ^ p.toReal := by
+    gcongr
+    exact norm_integral_le_integral_norm _
+  _ ≤ ∫ x, ‖f x‖ ^ p.toReal ∂μ :=
+    ConvexOn.map_integral_le (convexOn_rpow hp1')
+      (Real.continuous_rpow_const (by positivity)).continuousOn isClosed_Ici
+      (ae_of_all _ fun x ↦ norm_nonneg _) (hf.integrable hp1).norm
+      ((integrable_norm_rpow_iff hf.1 hp0 hp_top).mpr hf)
+
+end MeasureTheory

LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean

@@ -9,7 +9,7 @@ public import LeanMachineLearning.ForMathlib.Probability.Independence.CondIndepF
 public import LeanMachineLearning.ForMathlib.Probability.Independence.IndepFun
 public import LeanMachineLearning.ForMathlib.Probability.Independence.IndepInfinitePi
 public import LeanMachineLearning.ForMathlib.Probability.Integrable
-public import LeanMachineLearning.SequentialLearning.FiniteActions
+public import LeanMachineLearning.SequentialLearning.SumRewards
 public import LeanMachineLearning.SequentialLearning.StationaryEnv
 public import Mathlib.Probability.Independence.Integration
 public import Mathlib.Probability.Kernel.Representation

LeanMachineLearning/SequentialLearning/ActionIndicator.lean

@@ -0,0 +1,110 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import LeanMachineLearning.SequentialLearning.SumRewards
+
+/-!
+# The action indicator
+
+`actionIndicator A k n ω = 𝟙{A n ω = k}` is the `{0,1}`-valued indicator that action `k` was chosen
+at round `n`. It is the increment weight of every per-action sum attached to an action process:
+`pullCount A k n` is its partial sum (`sum_range_actionIndicator_eq_pullCount`) and
+`sumRewards A Y k n` is its reward-weighted partial sum (`sum_actionIndicator_mul`).
+
+
+## Main definitions
+
+* `Learning.actionIndicator`
+
+## Main results
+
+* `Learning.sum_range_actionIndicator_eq_pullCount`, `Learning.sum_actionIndicator_mul` — the two
+  partial-sum identities.
+* `Learning.adapted_actionIndicator`, `Learning.integrable_actionIndicator`.
+-/
+
+@[expose] public section
+
+open MeasureTheory ProbabilityTheory Filter Finset
+
+namespace Learning
+
+variable {Ω 𝓐 𝓨 : Type*} {mΩ : MeasurableSpace Ω} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
+  [MeasurableSingletonClass 𝓐] {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {P : Measure Ω}
+
+/-- The `{0,1}`-valued assignment indicator of action `k`:
+`actionIndicator A k n ω = 𝟙{A n ω = k}`. -/
+noncomputable def actionIndicator (A : ℕ → Ω → 𝓐) (k : 𝓐) (n : ℕ) (ω : Ω) : ℝ :=
+  {ω | A n ω = k}.indicator (fun _ ↦ (1 : ℝ)) ω
+
+/-- `actionIndicator A k n ω = 1` exactly when action `k` is chosen at time `n`. -/
+lemma actionIndicator_eq_one_iff {k : 𝓐} {n : ℕ} {ω : Ω} :
+    actionIndicator A k n ω = 1 ↔ A n ω = k := by simp [actionIndicator]
+
+lemma actionIndicator_nonneg (A : ℕ → Ω → 𝓐) (k : 𝓐) (n : ℕ) (ω : Ω) :
+    0 ≤ actionIndicator A k n ω :=
+  Set.indicator_apply_nonneg fun _ ↦ zero_le_one
+
+lemma actionIndicator_le_one (A : ℕ → Ω → 𝓐) (k : 𝓐) (n : ℕ) (ω : Ω) :
+    actionIndicator A k n ω ≤ 1 := by
+  unfold actionIndicator
+  by_cases h : A n ω = k <;> simp [h]
+
+/-- Exactly one arm is pulled at each round, so the indicators sum to `1`. -/
+lemma sum_actionIndicator [Fintype 𝓐] (A : ℕ → Ω → 𝓐) (j : ℕ) (ω : Ω) :
+    ∑ k, actionIndicator A k j ω = 1 := by
+  classical
+  simp [actionIndicator, Set.indicator_apply]
+
+lemma sum_actionIndicator_eq_pullCount [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐) (k : 𝓐) (n : ℕ)
+    (ω : Ω) :
+    ∑ j ∈ range n, actionIndicator A k j ω = (pullCount A k n ω : ℝ) := by
+  classical
+  rw [pullCount_eq_sum]
+  push_cast
+  refine Finset.sum_congr rfl fun j _ ↦ ?_
+  simp only [actionIndicator, Set.indicator_apply, Set.mem_ofPred_eq]
+
+lemma sum_actionIndicator_smul [DecidableEq 𝓐] [AddCommGroup 𝓨] [Module ℝ 𝓨]
+    (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (k : 𝓐) (t : ℕ) (ω : Ω) :
+    ∑ j ∈ range t, actionIndicator A k j ω • Y j ω = sumRewards A Y k t ω := by
+  rw [sumRewards]
+  refine Finset.sum_congr rfl fun j _ ↦ ?_
+  simp only [actionIndicator, Set.indicator_apply, Set.mem_ofPred_eq]
+  split_ifs <;> simp
+
+lemma sum_actionIndicator_mul [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → ℝ) (k : 𝓐) (t : ℕ)
+    (ω : Ω) :
+    ∑ j ∈ range t, actionIndicator A k j ω * Y j ω = sumRewards A Y k t ω :=
+  sum_actionIndicator_smul A Y k t ω
+
+lemma measurable_actionIndicator (k : 𝓐) {n : ℕ} (hA : Measurable (A n)) :
+    Measurable (actionIndicator A k n) :=
+  measurable_const.indicator (hA (measurableSet_singleton k))
+
+lemma integrable_actionIndicator (P : Measure Ω) [IsFiniteMeasure P]
+    (k : 𝓐) {n : ℕ} (hA : Measurable (A n)) :
+    Integrable (actionIndicator A k n) P :=
+  (integrable_const (1 : ℝ)).indicator (hA (measurableSet_singleton k))
+
+/-- The action indicator is adapted to the history filtration: whether action `k` was chosen at `n`
+is known at time `n`. -/
+lemma IsAlgEnvSeq.adapted_actionIndicator {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨}
+    [IsFiniteMeasure P] (h : IsAlgEnvSeq A Y alg env P) (k : 𝓐) :
+    Adapted h.filtration (actionIndicator A k) :=
+  fun _ ↦ Measurable.indicator measurable_const (h.adapted_action _ (measurableSet_singleton k))
+
+/-- The action indicator is adapted to the history+action filtration: whether action `k` was chosen
+at `n` is known once we know the action at `n`. -/
+lemma IsAlgEnvSeq.adapted_actionIndicator_filtrationAction
+    {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨}
+    [IsFiniteMeasure P] (h : IsAlgEnvSeq A Y alg env P) (k : 𝓐) :
+    Adapted h.filtrationAction (actionIndicator A k) :=
+  fun _ ↦ Measurable.indicator measurable_const
+    (h.adapted_action_filtrationAction _ (measurableSet_singleton k))
+
+end Learning

LeanMachineLearning/SequentialLearning/Algorithm.lean

@@ -250,6 +250,18 @@ lemma IsAlgEnvSeq.hasLaw_history_zero (h : IsAlgEnvSeq A Y alg env P) : HasLaw (
     have hY := h.measurable_feedback
     exact (Measure.map_map (by fun_prop) (by fun_prop)).symm
 
+lemma IsAlgEnvSeq.hasLaw_action_comp (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) :
+    HasLaw (A (n + 1)) (alg.policy n ∘ₘ (P.map (history A Y n))) P :=
+  HasCondDistrib.hasLaw_comp (h.hasCondDistrib_action n)
+
+lemma IsAlgEnvSeq.hasLaw_feedback_comp (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) :
+    HasLaw (Y (n + 1)) ((env.feedback n) ∘ₘ (P.map fun ω ↦ (history A Y n ω, A (n + 1) ω))) P :=
+  HasCondDistrib.hasLaw_comp (h.hasCondDistrib_feedback n)
+
+lemma IsAlgEnvSeq.hasLaw_feedback_zero_comp (h : IsAlgEnvSeq A Y alg env P) :
+    HasLaw (Y 0) (env.ν0 ∘ₘ (P.map (A 0))) P :=
+  HasCondDistrib.hasLaw_comp (h.hasCondDistrib_feedback_zero)
+
 section Filtration
 
 namespace IsAlgEnvSeq