Integrability of the Truncated Biconjugate

Proved

FunctionalInequalities.Probability.MomentMeasure.biconjugate_lowerTruncate_potentialIntegrable_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This proves admissibility of the actual biconjugate of a lower truncation.

Let $\mu$ be a nonzero finite Borel measure on a real inner-product space, let $f:E\to\overline{\mathbb R}$ be potential-integrable, and let $M\in\mathbb R$ . Then

\operatorname{Leg}\!\left(\operatorname{Leg}(\max(f,-M))\right)

is potential-integrable with respect to $\mu$ . The statement includes the required Borel measurability and finite-measure assumptions and derives integrability from the truncation bounds rather than requiring it separately for the biconjugate.

Original Lean declaration header

Within namespace FunctionalInequalities.Probability.MomentMeasure. Shown in its original module context. Proof omitted.

theorem biconjugate_lowerTruncate_potentialIntegrable [IsFiniteMeasure μ]
    (f : E → EReal) (M : ℝ) (hμ : μ ≠ 0) (hf : PotentialIntegrable f μ) :
    PotentialIntegrable (legendre (legendre (lowerTruncate f M))) μ

Module navigation

Module: Probability/MomentMeasure/Integrability.

Definition modules: Analysis/Convex/Legendre, Probability/MomentMeasure/Basic.

Supporting theorems: lowerTruncate_convexification.

Source excerpt, lines 71–73 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_MomentMeasure_Integrability

open FunctionalInequalities.Analysis
open MeasureTheory
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E}

Formal statement


theorem FunctionalInequalities.Probability.MomentMeasure.biconjugate_lowerTruncate_potentialIntegrable_readable [IsFiniteMeasure μ]
    (f : E → EReal) (M : ℝ) (hμ : μ ≠ 0) (hf : PotentialIntegrable f μ) :
    PotentialIntegrable (legendre (legendre (lowerTruncate f M))) μ := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/MomentMeasure/Integrability.lean#L68-L101 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.MomentMeasure.Integrability`, declaration `FunctionalInequalities.Probability.MomentMeasure.biconjugate_lowerTruncate_potentialIntegrable`; the repository is private at upload time).

View graph