Monotonicity of the Variance Clock

Proved

LevyStochCalc.Brownian.Ito.SimplePredictable.varClock_mono_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concavevendored-levystochcalc

This technical lemma states that the variance clock is monotone in the number of included tiles.

Let $G$ be a simple predictable integrand and let $c_i\in\mathbb R$ be arbitrary coefficient bounds. For natural numbers $k\le l$ ,

\operatorname{varClock}(G,c,k)\le \operatorname{varClock}(G,c,l).

The result relies on the nonnegativity of each summand $c_i^2(\tau_{i+1}-\tau_i)$ and is used to compare partial variance budgets with the full budget.

Original Lean declaration header

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

theorem varClock_mono (c : Fin G.N → ℝ) {k l : ℕ} (h : k ≤ l) :
    G.varClock c k ≤ G.varClock c l

Module navigation

Module: LevyStochCalc/Brownian/ItoFourthMomentIncrements.

Definition modules: LevyStochCalc/Brownian/ItoSimpleIntegrand.

Previous: stronglyMeasurable_partialSum.

Source excerpt, lines 266–267 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_LevyStochCalc_Brownian_ItoFourthMomentIncrements

/-
Copyright (c) 2026 Christian Garry. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Christian Garry
-/
-- Modified 2026-10-12 by the KLS formalization project: ported to Lean v4.33.0 and
-- Mathlib db584cd. The changes are listed in vendor/README.md and vendor/port.patch.
-- Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (upstream path LevyStochCalc/Brownian/ItoFourthMomentIncrements.lean; Apache-2.0; locally patched, see formalization/vendor/port.patch; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
universe u
variable {Ω : Type u} [MeasurableSpace Ω]
variable {T : ℝ} (G : LevyStochCalc.Brownian.Ito.SimplePredictable Ω T)
  {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (W : LevyStochCalc.Brownian.BrownianMotion P)

Formal statement

theorem LevyStochCalc.Brownian.Ito.SimplePredictable.varClock_mono_readable (c : Fin G.N → ℝ) {k l : ℕ} (h : k ≤ l) :
    G.varClock c k ≤ G.varClock c l := by sorry

Source

Lean source: https://github.com/cgarryZA/LevyStochCalc/blob/984dbf0b790031eac05d56fe5a84b65e15e1e932/LevyStochCalc/Brownian/ItoFourthMomentIncrements.lean (repository human-ai-mathematics/kls-lean, commit 408915f, module `LevyStochCalc.Brownian.ItoFourthMomentIncrements`, declaration `LevyStochCalc.Brownian.Ito.SimplePredictable.varClock_mono`; the repository is private at upload time); vendored copy patched by formalization/vendor/port.patch (project file formalization/vendor/LevyStochCalc/LevyStochCalc/Brownian/ItoFourthMomentIncrements.lean, lines 266-278). Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (Apache-2.0; upstream copyright notice retained in the Lean text).

View graph