Layer-Cake Inner Integral Evaluation

Proved

MeasureTheory.inner_t_integral_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concavevendored-mathfin

This auxiliary lemma evaluates a pointwise extended-real integral.

Let $f_\ast\geq0$ and $p>1$ . Then

\int_{(0,\infty)} t^{p-2}\,\mathbf 1_{\{t\leq f_\ast\}}\,dt = \frac{f_\ast^{p-1}}{p-1},

with both sides interpreted through ENNReal.ofReal.

The identity is the scalar integration step in the layer-cake proof of Doob's $L^p$ maximal inequality.

Formalization Note. The integral is an ENNReal lower integral over $(0,\infty)$ , and the indicator is $\mathbf 1_{\{t\leq f_\ast\}}$ .

Original Lean declaration header

Within namespace MeasureTheory. Shown in its original module context. Proof omitted.

private lemma inner_t_integral
    {fstar p : ℝ} (hfstar : 0 ≤ fstar) (hp : 1 < p) :
    ∫⁻ t in Set.Ioi (0:ℝ), ENNReal.ofReal (t ^ (p - 2)) *
        {t : ℝ | t ≤ fstar}.indicator (fun _ ↦ (1 : ℝ≥0∞)) t
      = ENNReal.ofReal (fstar ^ (p - 1) / (p - 1))

Module navigation

Module: MathFin/Foundations/DoobLpMaximalInequality.

Next: fubini_swap.

Source excerpt, lines 142–146 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_MathFin_Foundations_DoobLpMaximalInequality

/-
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)
open ProbabilityTheory ENNReal Filter Set Finset
variable {Ω : Type*}

Formal statement


 lemma MeasureTheory.inner_t_integral_readable
    {fstar p : ℝ} (hfstar : 0 ≤ fstar) (hp : 1 < p) :
    ∫⁻ t in Set.Ioi (0:ℝ), ENNReal.ofReal (t ^ (p - 2)) *
        {t : ℝ | t ≤ fstar}.indicator (fun _ ↦ (1 : ℝ≥0∞)) t
      = ENNReal.ofReal (fstar ^ (p - 1) / (p - 1)) := by sorry

Source

Lean source: https://github.com/raphaelrrcoelho/formal-mathfin/blob/784a8311f75a1519a23717856df9982bd6a9a370/MathFin/Foundations/DoobLpMaximalInequality.lean#L140-L187 (repository human-ai-mathematics/kls-lean, commit 408915f, module `MathFin.Foundations.DoobLpMaximalInequality`, declaration `_private.MathFin.Foundations.DoobLpMaximalInequality.0.MeasureTheory.inner_t_integral`; 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