Lower Semicontinuity Of Sequential Relaxation

Proved

FunctionalInequalities.Energy.PreEnergy.lowerSemicontinuous_sequentialRelaxation_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This theorem states that sequential relaxation is lower semicontinuous in a pseudometric ambient space.

Let $X$ be a pseudometric space and let $P$ be any pre-energy on $X$ . Then the function assigning to $x\in X$ the ENNReal-valued sequentially relaxed energy is lower semicontinuous:

\operatorname{LowerSemicontinuous}\!\left( x\mapsto P.\operatorname{sequentialRelaxation}(x) \right).

The declaration is lowerSemicontinuous_sequentialRelaxation_readable. The conclusion allows relaxed energy equal to $\top$ and does not require a dense realization, quadratic structure, closability, or a Markov property.

Original Lean declaration header

Within namespace FunctionalInequalities.Energy.PreEnergy. Shown in its original module context. Proof omitted.

theorem lowerSemicontinuous_sequentialRelaxation :
    LowerSemicontinuous (fun x ↦ P.sequentialRelaxation x)

Module navigation

Module: Energy/Relaxation/LowerSemicontinuous.

Definition modules: Energy/Form/Functional, Energy/Relaxation/Basic.

Supporting theorems: exists_test_near_of_relaxation_lt.

Source excerpt, lines 32–33 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Energy_Relaxation_LowerSemicontinuous

universe u
variable {X : Type u} [PseudoMetricSpace X] (P : FunctionalInequalities.Energy.PreEnergy X)

Formal statement


theorem FunctionalInequalities.Energy.PreEnergy.lowerSemicontinuous_sequentialRelaxation_readable :
    LowerSemicontinuous (fun x ↦ P.sequentialRelaxation x) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Energy/Relaxation/LowerSemicontinuous.lean#L31-L78 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Energy.Relaxation.LowerSemicontinuous`, declaration `FunctionalInequalities.Energy.PreEnergy.lowerSemicontinuous_sequentialRelaxation`; the repository is private at upload time).

View graph