Clamping Levels with Geometrically Small Mesh

This vendored existence theorem selects clamping levels whose mesh decays geometrically on every bounded window.

Let $P$ be a probability measure, let $H$ and $b$ be measurable coefficient families, and assume:

1. For every coefficient index and every $T>0$, the ENNReal energy of $H$ on $[0,T]$ is finite.
2. For every drift index and every $T>0$, the corresponding ENNReal energy of $b$ on $[0,T]$ is finite.

Then there exists a sequence $m_s:\mathbb N\to\mathbb N$ such that $s\leq m_s$ and, for every $s\in\mathbb N$,

$$\operatorname{clampMesh}(P,H,b,s+1,m_s) < \left(\frac12\right)^{2s}$$

in $[0,\infty]$.

This supplies clamping levels suitable for summability and convergence constructions on increasing windows.

Formalization Note. The mesh and the geometric bound are ENNReal values, and the strict inequality is in ENNReal.

Original Lean declaration header

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

theorem exists_seq_clampMesh_window_lt {H : Fin n → Fin d → Ω → ℝ → ℝ}
    (hm : ∀ p k, Measurable (Function.uncurry (H p k)))
    {b : Fin n → Ω → ℝ → ℝ} (hbm : ∀ p, Measurable (Function.uncurry (b p)))
    (hq : ∀ (p : Fin n) (k : Fin d) (T : ℝ), 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
      (‖H p k ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
    (hbq : ∀ (p : Fin n) (T : ℝ), 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
      (‖b p ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤) :
    ∃ ms : ℕ → ℕ, (∀ i : ℕ, i ≤ ms i) ∧
      ∀ i : ℕ, clampMesh P H b ((i : ℝ) + 1) (ms i) < ((2 : ℝ≥0∞)⁻¹) ^ (2 * i)

Module navigation

Module: LevyStochCalc/Ito/VectorItoVersionLimit.

Definition modules: LevyStochCalc/Ito/ItoFormulaUnboundedClamp.

Supporting theorems: tendsto_energy_window_clamp.

Previous: clampMesh_mono_window · Next: vectorItoProcess_ae_eq_zero.

Source excerpt, lines 124–132 · Frozen source 408915f.

import Definitions.Def_KLSModular_LevyStochCalc_Ito_VectorItoVersionLimit

/-
Copyright (c) 2026 Christian Garry. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Christian Garry
-/
-- Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (upstream path LevyStochCalc/Ito/VectorItoVersionLimit.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
open MeasureTheory ProbabilityTheory LevyStochCalc.Probability
open scoped NNReal ENNReal Topology
universe u
variable {Ω : Type u} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {n d : ℕ}

theorem LevyStochCalc.Brownian.Ito.exists_seq_clampMesh_window_lt_readable {H : Fin n → Fin d → Ω → ℝ → ℝ}
    (hm : ∀ p k, Measurable (Function.uncurry (H p k)))
    {b : Fin n → Ω → ℝ → ℝ} (hbm : ∀ p, Measurable (Function.uncurry (b p)))
    (hq : ∀ (p : Fin n) (k : Fin d) (T : ℝ), 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
      (‖H p k ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
    (hbq : ∀ (p : Fin n) (T : ℝ), 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
      (‖b p ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤) :
    ∃ ms : ℕ → ℕ, (∀ i : ℕ, i ≤ ms i) ∧
      ∀ i : ℕ, clampMesh P H b ((i : ℝ) + 1) (ms i) < ((2 : ℝ≥0∞)⁻¹) ^ (2 * i) := by sorry