Lyapunov convexity theorem

DefinitionLyapunov range#✓fully proved

For a measure \(\mu\) on a measurable space \(\alpha\) and a function \(f : \alpha \to E\) into a real normed space \(E\), the Lyapunov range of \(f\) with respect to \(\mu\) is the set \(\lbrace \int_s f \, d\mu : s \subseteq \alpha \text{ measurable} \rbrace\) of integrals of \(f\) over measurable subsets of \(\alpha\).

Here \(\int_s f \, d\mu\) is the Bochner integral, which is \(0\) when \(f\) is not integrable on \(s\) or when \(E\) is not complete.

noncomputable def lyapunovRange {α : Type*} [MeasurableSpace α] {E : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E] (μ : Measure α) (f : α → E) :
    Set E :=
  { y | ∃ (s : Set α), MeasurableSet s ∧ y = ∫ x in s, f x ∂μ }

Used by 1

Used byLyapunov convexity theorem

TheoremLyapunov convexity theorem#✓fully proved

Let \(\mu\) be a finite atomless measure on a measurable space \(\alpha\), let \(E\) be a finite-dimensional real normed space, and let \(f : \alpha \to E\) be Bochner integrable with respect to \(\mu\). Then the Lyapunov range of \(f\) with respect to \(\mu\), the set of integrals \(\int_s f \, d\mu\) over measurable sets \(s \subseteq \alpha\), is compact and convex.

theorem lyapunov_convexity
    {α : Type*} [MeasurableSpace α] {μ : Measure α} [IsFiniteMeasure μ]
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    (f : α → E) (hf : Integrable f μ) (hAtomless : IsAtomless μ) :
    IsCompact (lyapunovRange (μ := μ) (f := f)) ∧
      Convex ℝ (lyapunovRange (μ := μ) (f := f))

Sources

• A. Lyapunov, Izv. Akad. Nauk SSSR 4 (1940) 465–478; Diestel-Uhl, Vector Measures; Lean states atomless finite measure case with Bochner integrable finite-dim integrand, infinite-dim fails.

Uses 4

Statement usesLyapunov range · Atomless measure

Proof usesSierpiński's theorem on atomless measures · Restriction of an atomless measure

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.