Running maximum auxiliary definition

Definition

KLSModular_MathFin_Foundations_DoobLpMaximalInequality

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-contextvendored-mathfin

Vendored from the formal-mathfin library (https://github.com/raphaelrrcoelho/formal-mathfin). The private definition MeasureTheory.runMax assigns to a real-valued discrete-time process $f$ , an index $n$ , and an outcome $\omega$ the finite supremum of $f(k,\omega)$ over $k\in\{0,\ldots,n\}$ . The uploaded declarations contain this auxiliary definition only; the module text does not provide the stated $L^p$ maximal-inequality theorem.

Original module imports

public import Mathlib.Probability.Martingale.OptionalStopping
public import Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
public import Mathlib.Analysis.SpecialFunctions.Pow.Integral
public import Mathlib.MeasureTheory.Integral.MeanInequalities
public import Mathlib.MeasureTheory.Function.LpSeminorm.Basic
public import Mathlib.Analysis.MeanInequalities

Original declaration excerpt

Shown in the original module context.

private def runMax (f : ℕ → Ω → ℝ) (n : ℕ) (ω : Ω) : ℝ :=
  (Finset.range (n + 1)).sup' Finset.nonempty_range_add_one (fun k ↦ f k ω)

Module navigation

Theorems in source order:

Project result: The KLS conjecture.

Original module · MathFin.Foundations.DoobLpMaximalInequality · Frozen source 408915f.

Definition code

import Mathlib.Probability.Martingale.OptionalStopping
import Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
import Mathlib.Analysis.SpecialFunctions.Pow.Integral
import Mathlib.MeasureTheory.Integral.MeanInequalities
import Mathlib.MeasureTheory.Function.LpSeminorm.Basic
import Mathlib.Analysis.MeanInequalities

/-
Copyright (c) 2026 Raphael Coelho. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Raphael Coelho
-/
-- Vendored from https://github.com/raphaelrrcoelho/formal-mathfin at commit 784a8311f75a1519a23717856df9982bd6a9a370 (upstream path MathFin/Foundations/DoobLpMaximalInequality.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
section
open ProbabilityTheory ENNReal Filter Set Finset
open scoped NNReal
namespace MeasureTheory
variable {Ω : Type*}
/-- Internal abbreviation for the running maximum
`max {f 0 ω, f 1 ω, …, f n ω}`. Kept `private`: the theorem
states the bound in terms of the explicit `Finset.sup'` form to match
`MeasureTheory.maximal_ineq`. -/
 def runMax (f : ℕ → Ω → ℝ) (n : ℕ) (ω : Ω) : ℝ :=
  (Finset.range (n + 1)).sup' Finset.nonempty_range_add_one (fun k ↦ f k ω)
variable [m0 : MeasurableSpace Ω] {μ : Measure Ω}
end MeasureTheory

Source

Lean source: https://github.com/raphaelrrcoelho/formal-mathfin/blob/784a8311f75a1519a23717856df9982bd6a9a370/MathFin/Foundations/DoobLpMaximalInequality.lean#L57-L62 (repository human-ai-mathematics/kls-lean, commit 408915f, module `MathFin.Foundations.DoobLpMaximalInequality`, definition bundle `KLSModular_MathFin_Foundations_DoobLpMaximalInequality`; the repository is private at upload time). Vendored from https://github.com/raphaelrrcoelho/formal-mathfin at commit 784a8311f75a1519a23717856df9982bd6a9a370 (Apache-2.0; upstream copyright notice retained in the Lean text).

View graph