Prove2Me

Integral Formula for Affine Subtraction

Proved
FunctionalInequalities.Probability.MomentMeasure.integral_affineSubtract_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This gives the exact integral correction under affine subtraction.

Let μ\mu be a finite measure, let f:E→R‾f:E\to\overline{\mathbb R} be potential-integrable, let a∈Ea\in E, and let b∈Rb\in\mathbb R. Assume the identity map is integrable with respect to μ\mu. Then

∫toReal⁡((affineSubtract⁡f a b)(x)) dμ=∫toReal⁡(f(x)) dμ−∫⟨a,x⟩ dμ−(μ(E)).toReal⁡ b.\int \operatorname{toReal}\bigl((\operatorname{affineSubtract} f\ a\ b)(x)\bigr)\,d\mu = \int \operatorname{toReal}(f(x))\,d\mu -\int\langle a,x\rangle\,d\mu -(\mu(E)).\operatorname{toReal}\,b.

The total mass factor is retained; invariance under constant shifts is therefore not asserted for arbitrary finite measures.

Original Lean declaration header

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

theorem integral_affineSubtract
    (f : E → EReal) (a : E) (b : ℝ) (hf : PotentialIntegrable f μ)
    (hfirst : Integrable (fun x : E => x) μ) :
    (∫ x, (affineSubtract f a b x).toReal ∂μ) =
      (∫ x, (f x).toReal ∂μ) - (∫ x, inner ℝ a x ∂μ) - (μ Set.univ).toReal * b

Module navigation

Module: Probability/MomentMeasure/Affine.

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

Previous: affineSubtract_potentialIntegrable.

Source excerpt, lines 95–99 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_MomentMeasure_Affine

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

theorem FunctionalInequalities.Probability.MomentMeasure.integral_affineSubtract_readable
    (f : E → EReal) (a : E) (b : ℝ) (hf : PotentialIntegrable f μ)
    (hfirst : Integrable (fun x : E => x) μ) :
    (∫ x, (affineSubtract f a b x).toReal ∂μ) =
      (∫ x, (f x).toReal ∂μ) - (∫ x, inner ℝ a x ∂μ) - (μ Set.univ).toReal * b := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/MomentMeasure/Affine.lean#L92-L112 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.MomentMeasure.Affine`, declaration `FunctionalInequalities.Probability.MomentMeasure.integral_affineSubtract`; the repository is private at upload time).

View graph