Prefix/tail integral representation of the exposure martingale

Stage B sub-PR 2c of docs/plans/mcdiarmid-rademacher-plan.md.

For an integrable real-valued function f : (Fin n → Z) → ℝ and a probability measure μ on Z, the Doob exposure martingale value M_k = E[f | F_k] admits a prefix/tail integral representation: conditioning on the first k coordinates equals integrating out the last n - k coordinates pointwise.

Mathlib has no condExp_pi machinery, so we build the structural prefix/tail decomposition and the partial-integral candidate from scratch in this PR. The full conditional-expectation identification itself, the bounded-increment range bound, the conditional Hoeffding lemma, and the Filtration ℕ adapter are explicit follow-ups.

Contents (this module)

• splice k S T — combine prefix coords from S and tail coords from T along the predicate (i : ℕ) < (k : ℕ).
• splice_zero, splice_last — boundary identities.
• measurable_splice — joint measurability of splice in (S, T).
• partialIntegral μ k f S — the prefix/tail integral candidate ∫ T, f(splice k S T) ∂μⁿ.
• partialIntegral_zero — at k = 0, equals ∫ f dμⁿ pointwise (no prefix to condition on).
• partialIntegral_last — at k = Fin.last n, equals f S pointwise under a probability measure (full prefix recovers f).
• partialIntegral_invariant_on_tail_update — the invariance partialIntegral S = partialIntegral (Function.update S i z') for any tail index i ≥ k. This is the structural property that makes partialIntegral coordinateSubAlgebra k-measurable in spirit; the full strongly-measurable statement is deferred to a follow-up sub-PR of B2c.

Constraints

• No sorry, no admit, no custom axiom. All lemmas close.
• No manifest entry. No /lean dashboard update.
• No concentration claim. The strongest identity here is a pointwise equality of two real-valued functions on Fin n → Z.
• [StandardBorelSpace Z] is not assumed in this module. It will appear only in the conditional-Hoeffding sub-PR (B2c-3) where condExpKernel enters.

Splice: combine prefix and tail coordinates

splice k S T : Fin n → Z agrees with S on indices in the prefix {i | (i : ℕ) < (k : ℕ)} and with T on the tail.

def FormalSLT.Azuma.ExposureMartingale.splice {n : ℕ} {Z : Type u_1} (k : Fin (n + 1)) (S T : Fin n → Z) : Fin n → Z

Splice prefix coords from S with tail coords from T.

Equations

• FormalSLT.Azuma.ExposureMartingale.splice k S T i = if ↑i < ↑k then S i else T i

@[simp]

theorem FormalSLT.Azuma.ExposureMartingale.splice_zero {n : ℕ} {Z : Type u_1} (S T : Fin n → Z) : splice 0 S T = T

@[simp]

theorem FormalSLT.Azuma.ExposureMartingale.splice_last {n : ℕ} {Z : Type u_1} (S T : Fin n → Z) : splice (Fin.last n) S T = S

theorem FormalSLT.Azuma.ExposureMartingale.measurable_splice {n : ℕ} {Z : Type u_1} [MeasurableSpace Z] (k : Fin (n + 1)) : Measurable fun (ST : (Fin n → Z) × (Fin n → Z)) => splice k ST.1 ST.2

Joint measurability of splice in (S, T).

theorem FormalSLT.Azuma.ExposureMartingale.splice_update_tail {n : ℕ} {Z : Type u_1} (k : Fin (n + 1)) (S T : Fin n → Z) {i : Fin n} (hi : ¬↑i < ↑k) (z' : Z) : splice k (Function.update S i z') T = splice k S T

splice is unaffected by changing S at any tail index.

theorem FormalSLT.Azuma.ExposureMartingale.splice_update_prefix {n : ℕ} {Z : Type u_1} (k : Fin (n + 1)) (S T : Fin n → Z) {i : Fin n} (hi : ↑i < ↑k) (z' : Z) : splice k S (Function.update T i z') = splice k S T

splice is unaffected by changing T at any prefix index.

Partial-integral candidate for M_k

partialIntegral μ k f S = ∫ T, f(splice k S T) ∂μⁿ is the natural prefix/tail integral candidate for the Doob exposure martingale.

Note: we integrate over the whole μⁿ rather than just the tail factor μⁿ⁻ᵏ. Under any probability measure μ, by Fubini this equals integrating only over tail coords (the prefix coords of T do not enter splice k S T). Using μⁿ keeps the type signature simple and avoids subtype arithmetic on Fin n.

noncomputable def FormalSLT.Azuma.ExposureMartingale.partialIntegral {n : ℕ} {Z : Type u_1} [MeasurableSpace Z] (μ : Fin n → MeasureTheory.Measure Z) (k : Fin (n + 1)) (f : (Fin n → Z) → ℝ) : (Fin n → Z) → ℝ

The prefix/tail integral candidate for the Doob exposure martingale.

Equations

• FormalSLT.Azuma.ExposureMartingale.partialIntegral μ k f S = ∫ (T : Fin n → Z), f (FormalSLT.Azuma.ExposureMartingale.splice k S T) ∂MeasureTheory.Measure.pi μ

theorem FormalSLT.Azuma.ExposureMartingale.partialIntegral_zero {n : ℕ} {Z : Type u_1} [MeasurableSpace Z] {μ : Fin n → MeasureTheory.Measure Z} (f : (Fin n → Z) → ℝ) (S : Fin n → Z) : partialIntegral μ 0 f S = ∫ (T : Fin n → Z), f T ∂MeasureTheory.Measure.pi μ

At k = 0, the prefix is empty, so the candidate equals the unconditional expectation of f.

theorem FormalSLT.Azuma.ExposureMartingale.partialIntegral_last {n : ℕ} {Z : Type u_1} [MeasurableSpace Z] {μ : Fin n → MeasureTheory.Measure Z} [MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.pi μ)] (f : (Fin n → Z) → ℝ) (S : Fin n → Z) : partialIntegral μ (Fin.last n) f S = f S

At k = Fin.last n, the prefix is the full sample, so the candidate equals f S (under a probability measure).

theorem FormalSLT.Azuma.ExposureMartingale.partialIntegral_invariant_on_tail_update {n : ℕ} {Z : Type u_1} [MeasurableSpace Z] {μ : Fin n → MeasureTheory.Measure Z} (k : Fin (n + 1)) (f : (Fin n → Z) → ℝ) (S : Fin n → Z) {i : Fin n} (hi : ¬↑i < ↑k) (z' : Z) : partialIntegral μ k f (Function.update S i z') = partialIntegral μ k f S

Tail-update invariance: partialIntegral is unchanged by updating S at any index in the tail i ≥ k. This is the structural property that supports partialIntegral being measurable w.r.t. the prefix-only σ-algebra coordinateSubAlgebra n Z k.

Strong measurability w.r.t. the full pi σ-algebra

partialIntegral μ k f is strongly measurable w.r.t. the full product σ-algebra on Fin n → Z. This follows from joint measurability of splice k and mathlib's parametric integral measurability lemma MeasureTheory.StronglyMeasurable.integral_prod_right'.

The strengthening to coordinateSubAlgebra n Z k-strong-measurability is a separate sub-PR and uses the tail-update invariance lemma above to factor partialIntegral through the prefix coordinates.

theorem FormalSLT.Azuma.ExposureMartingale.stronglyMeasurable_partialIntegral {n : ℕ} {Z : Type u_1} [MeasurableSpace Z] {μ : Fin n → MeasureTheory.Measure Z} [MeasureTheory.SFinite (MeasureTheory.Measure.pi μ)] (k : Fin (n + 1)) {f : (Fin n → Z) → ℝ} (hf : MeasureTheory.StronglyMeasurable f) : MeasureTheory.StronglyMeasurable (partialIntegral μ k f)

Strong measurability of partialIntegral w.r.t. the full product σ-algebra on Fin n → Z.

Prefix-agreement principle

partialIntegral μ k f depends only on the prefix coordinates of its argument. This is the pointwise structural property that supports the eventual coordinateSubAlgebra n Z k-strong-measurability of partialIntegral (deferred to a follow-up sub-PR, where it is needed for the conditional-expectation identification).

theorem FormalSLT.Azuma.ExposureMartingale.partialIntegral_eq_of_agree_prefix {n : ℕ} {Z : Type u_1} [MeasurableSpace Z] {μ : Fin n → MeasureTheory.Measure Z} (k : Fin (n + 1)) (f : (Fin n → Z) → ℝ) (S S' : Fin n → Z) (hagree : ∀ (i : Fin n), ↑i < ↑k → S i = S' i) : partialIntegral μ k f S = partialIntegral μ k f S'

Pointwise prefix-agreement principle: partialIntegral μ k f depends only on the prefix coords of its argument.

Prefix-σ-algebra strong measurability

The prefix-agreement principle above yields measurability of partialIntegral w.r.t. coordinateSubAlgebra n Z k. We factor partialIntegral μ k f through a prefix→full round-trip prefixToFull that fills the tail with a default Z-value and prove its measurability via the comap characterization of Measurable.

[Nonempty Z] is needed only for the default tail value.

theorem FormalSLT.Azuma.ExposureMartingale.stronglyMeasurable_coordinateSubAlgebra_partialIntegral {n : ℕ} {Z : Type u_1} [MeasurableSpace Z] {μ : Fin n → MeasureTheory.Measure Z} [Nonempty Z] [MeasureTheory.SFinite (MeasureTheory.Measure.pi μ)] (k : Fin (n + 1)) {f : (Fin n → Z) → ℝ} (hf : MeasureTheory.StronglyMeasurable f) : MeasureTheory.StronglyMeasurable (partialIntegral μ k f)

Strong measurability of partialIntegral μ k f w.r.t. coordinateSubAlgebra n Z k. The proof factors partialIntegral through the prefix-only round-trip prefixToFull.

Splice as a measure-preserving map

Under any probability measure μ on Z, the joint splice map (S, T) ↦ splice k S T is measure-preserving from μⁿ × μⁿ to μⁿ. We prove this by factoring splice through MeasurableEquiv.piEquivPiSubtypeProd (mathlib's prefix/tail equivalence). This is the change-of-variables tool needed for the prefix/tail integral identification of the exposure martingale.

theorem FormalSLT.Azuma.ExposureMartingale.measurePreserving_splice {n : ℕ} {Z : Type u_1} [MeasurableSpace Z] {μ : Fin n → MeasureTheory.Measure Z} [∀ (i : Fin n), MeasureTheory.IsProbabilityMeasure (μ i)] (k : Fin (n + 1)) : MeasureTheory.MeasurePreserving (fun (ST : (Fin n → Z) × (Fin n → Z)) => splice k ST.1 ST.2) ((MeasureTheory.Measure.pi μ).prod (MeasureTheory.Measure.pi μ)) (MeasureTheory.Measure.pi μ)

Under any probability measure μ, the joint splice map (S, T) ↦ splice k S T is measure-preserving from μⁿ × μⁿ to μⁿ.

coordinateSubAlgebra as a comap σ-algebra

coordinateSubAlgebra n Z k is the comap of the prefix-only product σ-algebra under the prefix-restriction map. This characterization is the structural fact that lets us turn ℱ_k-measurable sets into preimages of prefix-measurable sets, and yields the set-invariance lemma mem_iff_of_agree_prefix.

Integrability and the set-integral identity

theorem FormalSLT.Azuma.ExposureMartingale.integrable_partialIntegral {n : ℕ} {Z : Type u_1} [MeasurableSpace Z] {μ : Fin n → MeasureTheory.Measure Z} [∀ (i : Fin n), MeasureTheory.IsProbabilityMeasure (μ i)] (k : Fin (n + 1)) {f : (Fin n → Z) → ℝ} (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.pi μ)) : MeasureTheory.Integrable (partialIntegral μ k f) (MeasureTheory.Measure.pi μ)

partialIntegral μ k f is integrable when f is.

theorem FormalSLT.Azuma.ExposureMartingale.setIntegral_partialIntegral_eq {n : ℕ} {Z : Type u_1} [MeasurableSpace Z] {μ : Fin n → MeasureTheory.Measure Z} [∀ (i : Fin n), MeasureTheory.IsProbabilityMeasure (μ i)] (k : Fin (n + 1)) {f : (Fin n → Z) → ℝ} (hf : MeasureTheory.StronglyMeasurable f) (hfi : MeasureTheory.Integrable f (MeasureTheory.Measure.pi μ)) {s : Set (Fin n → Z)} (hs : MeasurableSet s) : ∫ (x : Fin n → Z) in s, partialIntegral μ k f x ∂MeasureTheory.Measure.pi μ = ∫ (x : Fin n → Z) in s, f x ∂MeasureTheory.Measure.pi μ

The set-integral identity: for any ℱ_k-measurable set s, the set-integral of partialIntegral μ k f equals that of f.

theorem FormalSLT.Azuma.ExposureMartingale.partialIntegral_eq_condExp_ae {n : ℕ} {Z : Type u_1} [MeasurableSpace Z] {μ : Fin n → MeasureTheory.Measure Z} [Nonempty Z] [∀ (i : Fin n), MeasureTheory.IsProbabilityMeasure (μ i)] (k : Fin (n + 1)) {f : (Fin n → Z) → ℝ} (hf : MeasureTheory.StronglyMeasurable f) (hfi : MeasureTheory.Integrable f (MeasureTheory.Measure.pi μ)) : partialIntegral μ k f =ᵐ[MeasureTheory.Measure.pi μ] (MeasureTheory.Measure.pi μ)[f | coordinateSubAlgebra n Z k]

The exposure martingale is the partial integral, almost everywhere. This is the conditional-expectation identification: it says that M_k S = E[f | first k coords](S) admits the explicit prefix/tail integral representation partialIntegral μ k f S = ∫ T, f(splice k S T) ∂μⁿ.