Vanishing continuous-variation remainder for the stopped energy estimate

The equally spaced mesh controls the squared-increment remainder by uniform continuity of the difference and the total increments of its two monotone components.

References

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

noncomputable def BGW.StableTrees.stoppedEnergyGrid (T : NNReal) (N k : ℕ) : NNReal

Equally spaced grid on a fixed nonnegative time interval.

Equations

• BGW.StableTrees.stoppedEnergyGrid T N k = ↑k / (↑N + 1) * T

theorem BGW.StableTrees.tendsto_stoppedEnergyGrid_sq_increments (O M : NNReal → ℝ) (hO : Monotone O) (hM : Monotone M) (hC : Continuous fun (s : NNReal) => O s - M s) (T : NNReal) : Filter.Tendsto (fun (N : ℕ) => ∑ k ∈ Finset.range (N + 1), (O (stoppedEnergyGrid T N (k + 1)) - M (stoppedEnergyGrid T N (k + 1)) - (O (stoppedEnergyGrid T N k) - M (stoppedEnergyGrid T N k))) ^ 2) Filter.atTop (nhds 0)

Squared increments of a continuous difference of two monotone paths vanish on equally spaced grids.

theorem BGW.StableTrees.stopped_energy_grid_le (D O M : ℕ → ℝ) (hD : D 0 = 0) (hO0 : O 0 = 0) (hM0 : M 0 = 0) (hO : Monotone O) (hM : Monotone M) {B : ℝ} (N : ℕ) (hw : ∀ k ≤ N, 0 ≤ D k - (O k - M k) ∧ D k - (O k - M k) ≤ B) : D N ^ 2 ≤ 2 * B * O N + B ^ 2 + ∑ k ∈ Finset.range N, (O (k + 1) - M (k + 1) - (O k - M k)) ^ 2 + 2 * ∑ k ∈ Finset.range N, (O k - M k) * (D (k + 1) - D k)

Finite-grid energy bound for a nonnegative bounded correction, retaining the continuous-variation remainder and the predictable martingale sum.

theorem BGW.StableTrees.integral_sq_le_of_martingale_nonneg_correction {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ℱ : MeasureTheory.Filtration NNReal inst✝} {D O M : NNReal → Ω → ℝ} (hD : MeasureTheory.Martingale D ℱ μ) (hO : MeasureTheory.StronglyAdapted ℱ O) (hM : MeasureTheory.StronglyAdapted ℱ M) (T : NNReal) {K L B : ℝ} (hK : 0 ≤ K) (hL : 0 ≤ L) (hDi : MeasureTheory.Integrable (fun (ω : Ω) => D T ω ^ 2) μ) (hpaths : ∀ᵐ (ω : Ω) ∂μ, O 0 ω = 0 ∧ M 0 ω = 0 ∧ D 0 ω = 0 ∧ (Monotone fun (s : NNReal) => O s ω) ∧ (Monotone fun (s : NNReal) => M s ω) ∧ (Continuous fun (s : NNReal) => O s ω - M s ω) ∧ O T ω ≤ K ∧ M T ω ≤ L ∧ ∀ s ≤ T, 0 ≤ D s ω - (O s ω - M s ω) ∧ D s ω - (O s ω - M s ω) ≤ B) : ∫ (ω : Ω), D T ω ^ 2 ∂μ ≤ 2 * B * ∫ (ω : Ω), O T ω ∂μ + B ^ 2

A bounded nonnegative correction to the difference of two continuous increasing processes controls the terminal martingale energy. The proof takes expectations on finite meshes and then removes the squared-increment remainder by dominated convergence.