Smooth compactly supported multipliers in L²

Definition

KLSModular_FunctionalInequalities_KLS_LogConcave_WeightedGradient_Multiplier

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a smooth compactly supported real function $\phi$ and any $u\in L^2(\nu)$ , memLp_mul_of_contDiff_hasCompactSupport states that $x\mapsto\phi(x)u(x)$ belongs to $L^2(\nu)$ . The result uses only the probability-law measure and the compact support of $\phi$ ; it is an auxiliary integrability statement for multiplier arguments involving the closed weighted gradient.

Original module imports

import FunctionalInequalities.Energy.WeightedGradient.Leibniz
import FunctionalInequalities.Energy.Relaxation.LinearPMap
import FunctionalInequalities.KLS.LogConcave.WeightedGradient.Closure
import FunctionalInequalities.L2.BoundedMultiplier
import FunctionalInequalities.Analysis.Semigroup.AdjointClosure

Original declaration excerpt

Shown in the original module context.

theorem memLp_mul_of_contDiff_hasCompactSupport {φ : V → ℝ} (hφ : ContDiff ℝ ∞ φ)
    (hφc : HasCompactSupport φ) (u : Lp ℝ 2 (ν : Measure V)) :
    MemLp (fun y => φ y * u y) 2 (ν : Measure V) := by
  obtain ⟨M, hM⟩ := hφ.continuous.bounded_above_of_compact_support hφc
  have hb : ∀ᵐ y ∂(ν : Measure V), |φ y| ≤ M :=
    Filter.Eventually.of_forall fun y => by simpa only [Real.norm_eq_abs] using hM y
  simpa only [smul_eq_mul] using
    L2.memLp_bddSmul (H := ℝ) hφ.continuous.aestronglyMeasurable hb u

Module navigation

Direct project imports: Energy/WeightedGradient/Leibniz, Energy/Relaxation/LinearPMap, KLS/LogConcave/WeightedGradient/Closure, L2/BoundedMultiplier, Analysis/Semigroup/AdjointClosure.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.KLS.LogConcave.WeightedGradient.Multiplier · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Energy_WeightedGradient_Leibniz
import Definitions.Def_KLSModular_FunctionalInequalities_Energy_Relaxation_LinearPMap
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_WeightedGradient_Closure
import Definitions.Def_KLSModular_FunctionalInequalities_L2_BoundedMultiplier
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Semigroup_AdjointClosure

noncomputable section
open MeasureTheory Filter Topology
open scoped ContDiff
namespace FunctionalInequalities
namespace KLS
namespace LogConcave
open Energy Energy.WeightedGradient FunctionalInequalities.Analysis.Semigroup
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
section Multiplier
variable {ν : ProbabilityMeasure V} (m : Measure V) [m.IsAddHaarMeasure] (B : V →L[ℝ] V)
  (hν : LogConcave ν) (hi : (interior (ν : Measure V).support).Nonempty)
omit [CompleteSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V] in
/-- A smooth compactly supported multiplier preserves `L²(ν)`. -/
theorem memLp_mul_of_contDiff_hasCompactSupport {φ : V → ℝ} (hφ : ContDiff ℝ ∞ φ)
    (hφc : HasCompactSupport φ) (u : Lp ℝ 2 (ν : Measure V)) :
    MemLp (fun y => φ y * u y) 2 (ν : Measure V) := by
  obtain ⟨M, hM⟩ := hφ.continuous.bounded_above_of_compact_support hφc
  have hb : ∀ᵐ y ∂(ν : Measure V), |φ y| ≤ M :=
    Filter.Eventually.of_forall fun y => by simpa only [Real.norm_eq_abs] using hM y
  simpa only [smul_eq_mul] using
    L2.memLp_bddSmul (H := ℝ) hφ.continuous.aestronglyMeasurable hb u
end Multiplier
end LogConcave
end KLS
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/WeightedGradient/Multiplier.lean#L113-L122 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.WeightedGradient.Multiplier`, definition bundle `KLSModular_FunctionalInequalities_KLS_LogConcave_WeightedGradient_Multiplier`; the repository is private at upload time).

View graph