Approximating a lower semicontinuous function from below

On a pseudometric space, an ℝ≥0∞-valued lower semicontinuous function is the pointwise supremum of an increasing sequence of bounded Lipschitz functions. This file builds that sequence explicitly, as the truncated inf-convolution

lscApproxAux f n x = ⨅ y, ((f y ⊓ n).toReal + n * dist x y),

and packages it as a sequence in Ω →ᵇ ℝ≥0.

Monotone approximation from below by bounded continuous functions is what turns the monotone convergence theorem into a lower semicontinuity statement for integrals against a varying measure, which is why the target of the approximation is Ω →ᵇ ℝ≥0 rather than merely a continuous function: the weak topology on measures is defined by pairing with exactly these test functions.

Main declarations

• TauCeti.lscApproxAux: the truncated inf-convolution, a real-valued function bounded by n and Lipschitz with constant n.
• TauCeti.iSup_ofReal_lscApproxAux: at a point where f is lower semicontinuous, the approximations increase to the value of f.
• TauCeti.lscApprox: the same sequence bundled as bounded continuous ℝ≥0-valued functions.
• LowerSemicontinuous.exists_boundedContinuous_monotone_iSup_eq: the resulting interface, stating only that some monotone sequence of bounded continuous functions has pointwise supremum f.

Implementation notes

The inf-convolution is taken of the truncation f ⊓ n rather than of f itself, so that the n-th approximation is bounded by n; truncating is what allows infinite values of f to be reached in the limit. The infimum is formed in ℝ (rather than in ℝ≥0∞) because the Lipschitz estimate is then Mathlib's LipschitzWith.of_le_add_mul, and because bounded continuous functions are the intended target. The construction is the one used for LipschitzOnWith.extend_real.

noncomputable def TauCeti.lscApproxAux {Ω : Type u_1} [PseudoMetricSpace Ω] (f : Ω → ENNReal) (n : ℕ) (x : Ω) : ℝ

The n-th truncated inf-convolution of f : Ω → ℝ≥0∞ on a pseudometric space: the infimum over y of (f y ⊓ n).toReal + n * dist x y. It is nonnegative, bounded by n, Lipschitz with constant n, increasing in n, and, when f is lower semicontinuous, increases pointwise to f.

theorem TauCeti.lscApproxAux_le_add {Ω : Type u_1} [PseudoMetricSpace Ω] (f : Ω → ENNReal) (n : ℕ) (x y : Ω) : lscApproxAux f n x ≤ (min (f y) ↑n).toReal + ↑n * dist x y

The defining upper bound for TauCeti.lscApproxAux, one for each competitor y.

theorem TauCeti.le_lscApproxAux {Ω : Type u_1} [PseudoMetricSpace Ω] {f : Ω → ENNReal} {n : ℕ} {x : Ω} {a : ℝ} (h : ∀ (y : Ω), a ≤ (min (f y) ↑n).toReal + ↑n * dist x y) : a ≤ lscApproxAux f n x

A lower bound valid for every competitor y is a lower bound for TauCeti.lscApproxAux.

theorem TauCeti.lscApproxAux_nonneg {Ω : Type u_1} [PseudoMetricSpace Ω] (f : Ω → ENNReal) (n : ℕ) (x : Ω) : 0 ≤ lscApproxAux f n x

The approximations are nonnegative.

theorem TauCeti.lscApproxAux_le_toReal_inf {Ω : Type u_1} [PseudoMetricSpace Ω] (f : Ω → ENNReal) (n : ℕ) (x : Ω) : lscApproxAux f n x ≤ (min (f x) ↑n).toReal

Taking y = x in the defining infimum bounds the approximation by the truncation of f at x.

theorem TauCeti.lscApproxAux_le_natCast {Ω : Type u_1} [PseudoMetricSpace Ω] (f : Ω → ENNReal) (n : ℕ) (x : Ω) : lscApproxAux f n x ≤ ↑n

The n-th approximation is bounded by n.

theorem TauCeti.ofReal_lscApproxAux_le {Ω : Type u_1} [PseudoMetricSpace Ω] (f : Ω → ENNReal) (n : ℕ) (x : Ω) : ENNReal.ofReal (lscApproxAux f n x) ≤ f x

Every approximation lies below f.

theorem TauCeti.lipschitzWith_lscApproxAux {Ω : Type u_1} [PseudoMetricSpace Ω] (f : Ω → ENNReal) (n : ℕ) : LipschitzWith (↑n) (lscApproxAux f n)

The n-th approximation is Lipschitz with constant n.

theorem TauCeti.continuous_lscApproxAux {Ω : Type u_1} [PseudoMetricSpace Ω] (f : Ω → ENNReal) (n : ℕ) : Continuous (lscApproxAux f n)

The approximations are continuous.

theorem TauCeti.monotone_lscApproxAux {Ω : Type u_1} [PseudoMetricSpace Ω] (f : Ω → ENNReal) (x : Ω) : Monotone fun (n : ℕ) => lscApproxAux f n x

The approximations increase with n, both the truncation level and the Lipschitz constant growing.

theorem TauCeti.iSup_ofReal_lscApproxAux {Ω : Type u_1} [PseudoMetricSpace Ω] {f : Ω → ENNReal} {x : Ω} (hf : LowerSemicontinuousAt f x) : ⨆ (n : ℕ), ENNReal.ofReal (lscApproxAux f n x) = f x

At a point where f : Ω → ℝ≥0∞ is lower semicontinuous, its truncated inf-convolutions increase to the value of f.

noncomputable def TauCeti.lscApprox {Ω : Type u_1} [PseudoMetricSpace Ω] (f : Ω → ENNReal) (n : ℕ) : BoundedContinuousFunction Ω NNReal

The truncated inf-convolution of f : Ω → ℝ≥0∞, bundled as a bounded continuous ℝ≥0-valued function: the nonnegative part of TauCeti.lscApproxAux f n, which is bounded by n.

theorem TauCeti.lscApprox_apply {Ω : Type u_1} [PseudoMetricSpace Ω] (f : Ω → ENNReal) (n : ℕ) (x : Ω) : (lscApprox f n) x = (lscApproxAux f n x).toNNReal

The value of the bundled approximation, as a nonnegative real. This is deliberately not @[simp]: the ℝ≥0∞ coercion TauCeti.coe_lscApprox_apply is the simp-normal form, and marking this lemma as well would pre-simplify that lemma's left-hand side (the simpNF linter rejects the pair).

@[simp]

theorem TauCeti.coe_lscApprox_apply {Ω : Type u_1} [PseudoMetricSpace Ω] (f : Ω → ENNReal) (n : ℕ) (x : Ω) : ↑((lscApprox f n) x) = ENNReal.ofReal (lscApproxAux f n x)

The value of the bundled approximation, as an element of ℝ≥0∞.

theorem TauCeti.monotone_coe_lscApprox {Ω : Type u_1} [PseudoMetricSpace Ω] (f : Ω → ENNReal) : Monotone fun (n : ℕ) (x : Ω) => ↑((lscApprox f n) x)

The bundled approximations increase pointwise with n.

theorem TauCeti.iSup_coe_lscApprox {Ω : Type u_1} [PseudoMetricSpace Ω] {f : Ω → ENNReal} {x : Ω} (hf : LowerSemicontinuousAt f x) : ⨆ (n : ℕ), ↑((lscApprox f n) x) = f x

At a point where f is lower semicontinuous, the bundled approximations increase to the value of f.

theorem LowerSemicontinuous.exists_boundedContinuous_monotone_iSup_eq {Ω : Type u_1} [PseudoMetricSpace Ω] {f : Ω → ENNReal} (hf : LowerSemicontinuous f) : ∃ (g : ℕ → BoundedContinuousFunction Ω NNReal), (Monotone fun (n : ℕ) (x : Ω) => ↑((g n) x)) ∧ ∀ (x : Ω), ⨆ (n : ℕ), ↑((g n) x) = f x

On a pseudometric space, a lower semicontinuous f : Ω → ℝ≥0∞ is the pointwise supremum of an increasing sequence of bounded continuous ℝ≥0-valued functions.