Monotonicity of the Clamping Mesh in the Window

This vendored theorem states that the clamping mesh is monotone in the time window.

Let $P$ be a measure on $\Omega$, let $H$ and $b$ be the coefficient families used to define clampMesh, and let $T\leq T'$ be real numbers. Then, for every $j\in\mathbb N$,

The result allows finite-energy estimates on larger time windows to control the corresponding mesh on smaller windows.

Formalization Note. The mesh is built from ENNReal integrals of squared coefficient-clamping errors; no finiteness assumption is present in the statement.

Original Lean declaration header

Within namespace LevyStochCalc.Brownian.Ito. Shown in its original module context. Proof omitted.

theorem clampMesh_mono_window (P : Measure Ω) (H : Fin n → Fin d → Ω → ℝ → ℝ)
    (b : Fin n → Ω → ℝ → ℝ) {T T' : ℝ} (hTT' : T ≤ T') (j : ℕ) :
    clampMesh P H b T j ≤ clampMesh P H b T' j

Module navigation

Module: LevyStochCalc/Ito/VectorItoVersionLimit.

Definition modules: LevyStochCalc/Ito/ItoFormulaUnboundedClamp.

Previous: le_add_inv_mul_sq · Next: exists_seq_clampMesh_window_lt.

Source excerpt, lines 90–92 · Frozen source 408915f.