Finite-grid identities for the stopped energy calculation

The algebraic identity uses right endpoint values of the correction and retains the sum of squared finite-variation increments. This remainder must be removed by continuity in a subsequent mesh limit; no continuity of the martingale is needed here.

References

• J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.

theorem BGW.StableTrees.stopped_energy_grid_identity (D C : ℕ → ℝ) (hD : D 0 = 0) (hC : C 0 = 0) (N : ℕ) : D N ^ 2 = 2 * ∑ k ∈ Finset.range N, C k * (D (k + 1) - D k) + 2 * ∑ k ∈ Finset.range N, (D (k + 1) - C (k + 1)) * (C (k + 1) - C k) + ∑ k ∈ Finset.range N, (C (k + 1) - C k) ^ 2 + (D N - C N) ^ 2

Summation by parts for D = C + w, retaining the square-increment remainder of C.

theorem BGW.StableTrees.integral_mul_martingale_increment_eq_zero {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [Preorder ι] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {ℱ : MeasureTheory.Filtration ι inst✝} {D : ι → Ω → ℝ} (hD : MeasureTheory.Martingale D ℱ μ) {s t : ι} (hst : s ≤ t) {X : Ω → ℝ} (hX : MeasureTheory.StronglyMeasurable X) (hi : MeasureTheory.Integrable (fun (ω : Ω) => X ω * (D t ω - D s ω)) μ) : ∫ (ω : Ω), X ω * (D t ω - D s ω) ∂μ = 0

An adapted multiplier is orthogonal to a future martingale increment whenever their product is integrable. In applications the multiplier is bounded on the stopped interval.