Density of Dyadic Rationals
ProvedLevyStochCalc.Brownian.Continuity.dense_dyadicRationals_readablefunctional-inequalitieskls-conjecturekls-modularkls-readablelog-concavevendored-levystochcalc
The set dyadicRationals = {k·2^{-n} : k ∈ ℤ, n ∈ ℕ} is dense in ℝ. Equivalently, every real x and every radius r > 0 admit a dyadic rational within distance r of x. The lemma dense_dyadicRationals_readable supplies the dense domain used in the deterministic Kolmogorov–Chentsov extension argument.
Original Lean declaration header
Within namespace LevyStochCalc.Brownian.Continuity. Shown in its original module context. Proof omitted.
lemma dense_dyadicRationals : Dense dyadicRationals
Module navigation
Module: LevyStochCalc/Brownian/ContinuityDyadicChaining.
Next: dyadicTrunc_succ_step.
Source excerpt, lines 120–120 · 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.dense_dyadicRationals_readable : Dense dyadicRationals := by sorry
Source
Lean source: https://github.com/cgarryZA/LevyStochCalc/blob/984dbf0b790031eac05d56fe5a84b65e15e1e932/LevyStochCalc/Brownian/ContinuityDyadicChaining.lean#L117-L150 (repository human-ai-mathematics/kls-lean, commit 408915f, module `LevyStochCalc.Brownian.ContinuityDyadicChaining`, declaration `LevyStochCalc.Brownian.Continuity.dense_dyadicRationals`; 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).