Lower semicontinuity of a lower semicontinuous integrand in the measure

Fix a lower semicontinuous f : Ω → ℝ≥0∞ on a pseudometric space. This file proves that the pairing μ ↦ ∫⁻ x, f x ∂μ is lower semicontinuous for the weak topology on FiniteMeasure Ω and on ProbabilityMeasure Ω, together with the two consequences the direct method of the calculus of variations runs on: the liminf inequality along a weakly convergent family, and attainment of the infimum on a nonempty compact set of measures.

For a bounded continuous integrand the pairing is continuous — that is what the weak topology is defined by. The content here is that dropping boundedness and continuity down to lower semicontinuity costs exactly one half of that continuity, and no integrability hypothesis at all: the value ∞ is allowed on both sides.

Main results

• TauCeti.lowerSemicontinuous_lintegral_finiteMeasure and TauCeti.lowerSemicontinuous_lintegral_probabilityMeasure: the pairing is lower semicontinuous.
• TauCeti.le_liminf_lintegral_of_tendsto_probabilityMeasure and TauCeti.le_liminf_lintegral_of_tendsto_finiteMeasure: the liminf form along a weakly convergent family.
• TauCeti.exists_isMinOn_lintegral: a nonempty compact set of probability measures contains one minimising the integral, with no finiteness assumption on the minimum value.
• TauCeti.isClosed_setOfPred_lintegral_le_finiteMeasure and TauCeti.isClosed_setOfPred_lintegral_le_probabilityMeasure: the sublevel sets of the pairing are closed.
• TauCeti.lowerSemicontinuousOn_lintegral_comp: for h lower semicontinuous and Φ arbitrary, μ ↦ ∫⁻ x, h (Φ x) ∂μ is lower semicontinuous on a set of finite or probability measures when Φ is continuous on closed sets of uniformly almost full mass.

Implementation notes

The proof is the standard monotone-approximation argument: TauCeti.lscApprox writes f as the pointwise supremum of an increasing sequence of bounded continuous ℝ≥0-valued functions, the monotone convergence theorem turns that into a supremum of integrals, each summand is continuous in the measure because it is a weak-topology test function, and a supremum of continuous functions is lower semicontinuous.

Only OpensMeasurableSpace Ω is used on the measurable side: it is what makes a lower semicontinuous function measurable, and Mathlib's weak topology is already available at that generality.

theorem TauCeti.lintegral_eq_iSup_lintegral_lscApprox {Ω : Type u_1} [PseudoMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] {f : Ω → ENNReal} (hf : LowerSemicontinuous f) (μ : MeasureTheory.Measure Ω) : ∫⁻ (x : Ω), f x ∂μ = ⨆ (n : ℕ), ∫⁻ (x : Ω), ↑((lscApprox f n) x) ∂μ

Monotone convergence applied to the approximating sequence TauCeti.lscApprox: the integral of a lower semicontinuous f is the supremum of the integrals of bounded continuous test functions below it.

theorem TauCeti.lowerSemicontinuous_lintegral_finiteMeasure {Ω : Type u_1} [PseudoMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] {f : Ω → ENNReal} (hf : LowerSemicontinuous f) : LowerSemicontinuous fun (μ : MeasureTheory.FiniteMeasure Ω) => ∫⁻ (x : Ω), f x ∂↑μ

Integration of a lower semicontinuous f : Ω → ℝ≥0∞ is lower semicontinuous in the finite measure, for the topology of weak convergence.

theorem TauCeti.lowerSemicontinuous_lintegral_probabilityMeasure {Ω : Type u_1} [PseudoMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] {f : Ω → ENNReal} (hf : LowerSemicontinuous f) : LowerSemicontinuous fun (μ : MeasureTheory.ProbabilityMeasure Ω) => ∫⁻ (x : Ω), f x ∂↑μ

Integration of a lower semicontinuous f : Ω → ℝ≥0∞ is lower semicontinuous in the probability measure, for the topology of weak convergence.

theorem TauCeti.le_liminf_lintegral_of_tendsto_probabilityMeasure {Ω : Type u_1} [PseudoMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] {f : Ω → ENNReal} {γ : Type u_2} {L : Filter γ} {μs : γ → MeasureTheory.ProbabilityMeasure Ω} {μ : MeasureTheory.ProbabilityMeasure Ω} (hf : LowerSemicontinuous f) (h : Filter.Tendsto μs L (nhds μ)) : ∫⁻ (x : Ω), f x ∂↑μ ≤ Filter.liminf (fun (i : γ) => ∫⁻ (x : Ω), f x ∂↑(μs i)) L

The liminf form of lower semicontinuity: along a weakly convergent family of probability measures, the integral of a lower semicontinuous integrand can only drop in the limit.

theorem TauCeti.le_liminf_lintegral_of_tendsto_finiteMeasure {Ω : Type u_1} [PseudoMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] {f : Ω → ENNReal} {γ : Type u_2} {L : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω} (hf : LowerSemicontinuous f) (h : Filter.Tendsto μs L (nhds μ)) : ∫⁻ (x : Ω), f x ∂↑μ ≤ Filter.liminf (fun (i : γ) => ∫⁻ (x : Ω), f x ∂↑(μs i)) L

The same liminf inequality for a weakly convergent family of finite measures.

theorem TauCeti.isClosed_setOfPred_lintegral_le_finiteMeasure {Ω : Type u_1} [PseudoMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] {f : Ω → ENNReal} (hf : LowerSemicontinuous f) (a : ENNReal) : IsClosed {μ : MeasureTheory.FiniteMeasure Ω | ∫⁻ (x : Ω), f x ∂↑μ ≤ a}

Sublevel sets of the finite-measure pairing against a lower semicontinuous integrand are weakly closed.

theorem TauCeti.isClosed_setOfPred_lintegral_le_probabilityMeasure {Ω : Type u_1} [PseudoMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] {f : Ω → ENNReal} (hf : LowerSemicontinuous f) (a : ENNReal) : IsClosed {μ : MeasureTheory.ProbabilityMeasure Ω | ∫⁻ (x : Ω), f x ∂↑μ ≤ a}

Sublevel sets of the probability-measure pairing against a lower semicontinuous integrand are weakly closed.

theorem TauCeti.exists_isMinOn_lintegral {Ω : Type u_1} [PseudoMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] {f : Ω → ENNReal} {K : Set (MeasureTheory.ProbabilityMeasure Ω)} (hK : K.Nonempty) (hKc : IsCompact K) (hf : LowerSemicontinuous f) : ∃ μ ∈ K, IsMinOn (fun (ν : MeasureTheory.ProbabilityMeasure Ω) => ∫⁻ (x : Ω), f x ∂↑ν) K μ

The direct method of the calculus of variations for a lower semicontinuous integrand: on a nonempty compact set of probability measures, the integral attains its infimum. The minimum value is allowed to be ∞, which happens exactly when every measure in the set gives f infinite integral.

theorem TauCeti.exists_lintegral_eq_iInf {Ω : Type u_1} [PseudoMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] {f : Ω → ENNReal} {K : Set (MeasureTheory.ProbabilityMeasure Ω)} (hK : K.Nonempty) (hKc : IsCompact K) (hf : LowerSemicontinuous f) : ∃ μ ∈ K, ∫⁻ (x : Ω), f x ∂↑μ = ⨅ (ν : ↑K), ∫⁻ (x : Ω), f x ∂↑↑ν

The infimum of the integral over a nonempty compact set of probability measures is a minimum: it is the value at some member of the set.

Integrands that are continuous only on closed sets of uniformly large mass

An integrand h ∘ Φ with h lower semicontinuous but Φ merely measurable is not lower semicontinuous, and its integral is not lower semicontinuous in the measure on all of ProbabilityMeasure Ω. It still is on a set S of measures for which Φ is continuous on closed sets carrying all but an arbitrarily small part of the mass of every member of S at once: the uniformity is what lets the exceptional set be ignored along a convergent family. Lusin's theorem supplies such closed sets whenever the members of S share a fixed image under a map through which Φ factors, as the squares of the couplings of two fixed marginals do.

theorem TauCeti.lowerSemicontinuousOn_lintegral_comp_finiteMeasure {Ω : Type u_1} [PseudoMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] {W : Type u_2} [TopologicalSpace W] {h : W → ENNReal} {Φ : Ω → W} {S : Set (MeasureTheory.FiniteMeasure Ω)} (hh : LowerSemicontinuous h) (hΦ : ∀ (ε : ENNReal), ε ≠ 0 → ∃ (C : Set Ω), IsClosed C ∧ ContinuousOn Φ C ∧ ∀ μ ∈ S, ↑μ Cᶜ ≤ ε) : LowerSemicontinuousOn (fun (μ : MeasureTheory.FiniteMeasure Ω) => ∫⁻ (x : Ω), h (Φ x) ∂↑μ) S

Lower semicontinuity under a uniform Lusin condition. Let h : W → ℝ≥0∞ be lower semicontinuous, Φ : Ω → W arbitrary, and S a set of finite measures on Ω such that for every ε > 0 some closed set C, on which Φ is continuous, has complement of mass at most ε for every member of S. Then μ ↦ ∫⁻ x, h (Φ x) ∂μ is lower semicontinuous on S for the weak topology.

theorem TauCeti.lowerSemicontinuousOn_lintegral_comp {Ω : Type u_1} [PseudoMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] {W : Type u_2} [TopologicalSpace W] {h : W → ENNReal} {Φ : Ω → W} {S : Set (MeasureTheory.ProbabilityMeasure Ω)} (hh : LowerSemicontinuous h) (hΦ : ∀ (ε : ENNReal), ε ≠ 0 → ∃ (C : Set Ω), IsClosed C ∧ ContinuousOn Φ C ∧ ∀ μ ∈ S, ↑μ Cᶜ ≤ ε) : LowerSemicontinuousOn (fun (μ : MeasureTheory.ProbabilityMeasure Ω) => ∫⁻ (x : Ω), h (Φ x) ∂↑μ) S

Lower semicontinuity under a uniform Lusin condition. Let h : W → ℝ≥0∞ be lower semicontinuous, Φ : Ω → W arbitrary, and S a set of probability measures on Ω such that for every ε > 0 some closed set C, on which Φ is continuous, has complement of mass at most ε for every member of S. Then μ ↦ ∫⁻ x, h (Φ x) ∂μ is lower semicontinuous on S for the weak topology.