Kolmogorov–Chentsov Exponent Identity

Proved

LevyStochCalc.Brownian.Continuity.kc_exponent_identity_readable

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

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

This is an algebraic identity for the per-level Kolmogorov–Chentsov factor. For $\alpha,p,q\in\mathbb R$ and $n\in\mathbb N$ ,

\frac{2^n\bigl((1/2)^n\bigr)^q}{\bigl(((1/2)^\alpha)^n\bigr)^p} =\bigl((1/2)^{q-\alpha p-1}\bigr)^n.

It isolates the geometric ratio governing summability of dyadic-level estimates.

Original Lean declaration header

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

lemma kc_exponent_identity {α p q : ℝ} (n : ℕ) :
    (2 : ℝ) ^ n * ((1 / 2 : ℝ) ^ n) ^ q / (((1 / 2 : ℝ) ^ α) ^ n) ^ p
      = ((1 / 2 : ℝ) ^ (q - α * p - 1)) ^ n

Module navigation

Module: LevyStochCalc/Brownian/ContinuityDyadicChaining.

Previous: rpow_half_pow_le · Next: dyadic_holder_chaining.

Source excerpt, lines 381–383 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_LevyStochCalc_Brownian_ContinuityDyadicChaining

/-
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/Brownian/ContinuityDyadicChaining.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)

Formal statement


lemma LevyStochCalc.Brownian.Continuity.kc_exponent_identity_readable {α p q : ℝ} (n : ℕ) :
    (2 : ℝ) ^ n * ((1 / 2 : ℝ) ^ n) ^ q / (((1 / 2 : ℝ) ^ α) ^ n) ^ p
      = ((1 / 2 : ℝ) ^ (q - α * p - 1)) ^ n := by sorry

Source

Lean source: https://github.com/cgarryZA/LevyStochCalc/blob/984dbf0b790031eac05d56fe5a84b65e15e1e932/LevyStochCalc/Brownian/ContinuityDyadicChaining.lean#L377-L400 (repository human-ai-mathematics/kls-lean, commit 408915f, module `LevyStochCalc.Brownian.ContinuityDyadicChaining`, declaration `LevyStochCalc.Brownian.Continuity.kc_exponent_identity`; the repository is private at upload time). Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (Apache-2.0; upstream copyright notice retained in the Lean text).

View graph