BanditRLProof.MartingaleDifference

Global succ-indexed martingale-difference witness. This is the all-time version of `SuccMartingaleDifferencePrefix`. It records the local hypotheses needed to build the Mathlib martingale of partial sums.

structure SuccMartingaleDifference {Omega : Type u} [mOmega : MeasurableSpace Omega] (mu : Measure Omega) (F : Filtration Nat mOmega) (Y : Nat -> Omega -> Real) : Prop where

Finite-prefix succ-indexed martingale-difference witness. For a process `Y`, this records that the prefix up to `n` is integrable and adapted, and that each later increment `Y (i + 1)` has zero conditional expectation against filtration level `i`. This is the local bridge between the compiled conditional-mean-zero leaves and later martingale or concentration consumers.

structure SuccMartingaleDifferencePrefix {Omega : Type u} [mOmega : MeasurableSpace Omega] (mu : Measure Omega) (F : Filtration Nat mOmega) (Y : Nat -> Omega -> Real) (n : Nat) : Prop where

No declaration docstring is present; use the chapter context and exact statement below.

theorem toPrefix {Omega : Type u} [mOmega : MeasurableSpace Omega] {mu : Measure Omega} {F : Filtration Nat mOmega} {Y : Nat -> Omega -> Real} (h : SuccMartingaleDifference mu F Y) (n : Nat) : SuccMartingaleDifferencePrefix mu F Y n where

No declaration docstring is present; use the chapter context and exact statement below.

theorem stronglyAdapted' {Omega : Type u} [mOmega : MeasurableSpace Omega] {mu : Measure Omega} {F : Filtration Nat mOmega} {Y : Nat -> Omega -> Real} (h : SuccMartingaleDifference mu F Y) : StronglyAdapted F Y

No declaration docstring is present; use the chapter context and exact statement below.

theorem integrable' {Omega : Type u} [mOmega : MeasurableSpace Omega] {mu : Measure Omega} {F : Filtration Nat mOmega} {Y : Nat -> Omega -> Real} (h : SuccMartingaleDifference mu F Y) (t : Nat) : Integrable (Y t) mu

No declaration docstring is present; use the chapter context and exact statement below.

theorem condExp_succ_ae_eq_zero {Omega : Type u} [mOmega : MeasurableSpace Omega] {mu : Measure Omega} {F : Filtration Nat mOmega} {Y : Nat -> Omega -> Real} (h : SuccMartingaleDifference mu F Y) (i : Nat) : Filter.EventuallyEq (ae mu) (condExp (F i) mu (Y (i + 1))) (fun _omega => (0 : Real))

No declaration docstring is present; use the chapter context and exact statement below.

theorem stronglyAdapted' {Omega : Type u} [mOmega : MeasurableSpace Omega] {mu : Measure Omega} {F : Filtration Nat mOmega} {Y : Nat -> Omega -> Real} {n : Nat} (h : SuccMartingaleDifferencePrefix mu F Y n) : StronglyAdapted F Y

No declaration docstring is present; use the chapter context and exact statement below.

theorem integrable_of_lt {Omega : Type u} [mOmega : MeasurableSpace Omega] {mu : Measure Omega} {F : Filtration Nat mOmega} {Y : Nat -> Omega -> Real} {n : Nat} (h : SuccMartingaleDifferencePrefix mu F Y n) {t : Nat} (ht : t < n) : Integrable (Y t) mu

No declaration docstring is present; use the chapter context and exact statement below.

theorem condExp_succ_ae_eq_zero {Omega : Type u} [mOmega : MeasurableSpace Omega] {mu : Measure Omega} {F : Filtration Nat mOmega} {Y : Nat -> Omega -> Real} {n : Nat} (h : SuccMartingaleDifferencePrefix mu F Y n) {i : Nat} (hi : i + 1 < n) : Filter.EventuallyEq (ae mu) (condExp (F i) mu (Y (i + 1))) (fun _omega => (0 : Real))

Centered reward process obtained by subtracting a predictable or otherwise chosen baseline from a raw reward process. The baseline is allowed to be random; the martingale-difference builder below therefore asks directly for adaptedness, integrability, and conditional mean-zero of this centered process.

def centeredRewardProcess {Omega : Type u} (reward baseline : Nat -> Omega -> Real) : Nat -> Omega -> Real

Build the global succ-indexed martingale-difference witness for a centered reward process from the exact three local contracts used by Mathlib: adaptedness, integrability, and succ-indexed conditional mean zero.

theorem succMartingaleDifference_centeredRewardProcess_of_condExp {Omega : Type u} [mOmega : MeasurableSpace Omega] (mu : Measure Omega) {F : Filtration Nat mOmega} (reward baseline : Nat -> Omega -> Real) (hadapted : StronglyAdapted F (centeredRewardProcess reward baseline)) (hintegrable : forall t, Integrable (centeredRewardProcess reward baseline t) mu) (hcond : forall i, Filter.EventuallyEq (ae mu) (condExp (F i) mu (centeredRewardProcess reward baseline (i + 1))) (fun _omega => (0 : Real))) : SuccMartingaleDifference mu F (centeredRewardProcess reward baseline) where

Finite-prefix version of `succMartingaleDifference_centeredRewardProcess_of_condExp`.

theorem succMartingaleDifferencePrefix_centeredRewardProcess_of_condExp {Omega : Type u} [mOmega : MeasurableSpace Omega] (mu : Measure Omega) {F : Filtration Nat mOmega} (reward baseline : Nat -> Omega -> Real) (n : Nat) (hadapted : StronglyAdapted F (centeredRewardProcess reward baseline)) (hintegrable : forall t, t < n -> Integrable (centeredRewardProcess reward baseline t) mu) (hcond : forall i, i + 1 < n -> Filter.EventuallyEq (ae mu) (condExp (F i) mu (centeredRewardProcess reward baseline (i + 1))) (fun _omega => (0 : Real))) : SuccMartingaleDifferencePrefix mu F (centeredRewardProcess reward baseline) n where

Partial sums of a succ-indexed martingale-difference process. The sum starts at `Y 1`, so the increment from time `i` to `i + 1` is definitionally `Y (i + 1)`, matching Mathlib's martingale theorem `martingale_of_condExp_sub_eq_zero_nat`.

noncomputable def partialSumsSucc {Omega : Type u} (Y : Nat -> Omega -> Real) : Nat -> Omega -> Real

The partial sums of a global succ-indexed martingale-difference process form a Mathlib martingale. This is a thin wrapper around `MeasureTheory.martingale_of_condExp_sub_eq_zero_nat`. It does not assert optional stopping, concentration, or final regret; it only upgrades the local conditional-mean-zero increment contract to Mathlib's martingale API.

theorem martingale_partialSumsSucc_of_succMartingaleDifference {Omega : Type u} [mOmega : MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] {F : Filtration Nat mOmega} {Y : Nat -> Omega -> Real} (h : SuccMartingaleDifference mu F Y) : Martingale (partialSumsSucc Y) F mu

The partial sums of a global centered reward process form a Mathlib martingale once the centered process satisfies the martingale-difference contracts.

theorem martingale_partialSumsSucc_centeredRewardProcess_of_condExp {Omega : Type u} [mOmega : MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] {F : Filtration Nat mOmega} (reward baseline : Nat -> Omega -> Real) (hadapted : StronglyAdapted F (centeredRewardProcess reward baseline)) (hintegrable : forall t, Integrable (centeredRewardProcess reward baseline t) mu) (hcond : forall i, Filter.EventuallyEq (ae mu) (condExp (F i) mu (centeredRewardProcess reward baseline (i + 1))) (fun _omega => (0 : Real))) : Martingale (partialSumsSucc (centeredRewardProcess reward baseline)) F mu