Functionals on L∞ and finitely additive set functions on measurable sets

Let μ be a measure on a measurable space α. Evaluating a linear functional M on L∞(α, μ) at the classes [1_s] of indicator functions of measurable sets gives a finitely additive real set function s ↦ M [1_s] on the measurable sets (LinearMap.toAddContentLpTop). It vanishes on μ-null sets, since their indicators vanish in L∞, and it is nonnegative when M is positive.

Conversely, every nonnegative real content ν on the measurable sets that vanishes on μ-null sets arises in this way from exactly one positive linear functional on L∞(α, μ) (PositiveLinearMap.ofAddContentLpTop). A real simple function f is integrated by the finite sum ∑ c, c * ν {x | f x = c} (MeasureTheory.AddContent.integralSimple). Null annihilation makes this sum depend only on the class of f in L∞, and bounds it by ν univ times the essential supremum of |f|. Simple functions are uniformly dense among essentially bounded functions (MeasureTheory.SimpleFunc.denseRange_toLpTop), so the integral extends uniquely by continuity, and the extension is positive because its norm is at most its value ν univ at the constant one. The values of a content on nonmeasurable sets play no role: the inverse laws hold on measurable sets.

For a left-invariant measure on a group, left translation of a class in L∞ translates the indicators, and a positive functional is invariant under left translation exactly when its content is invariant under translation of measurable sets (PositiveLinearMap.forall_apply_leftTranslation_eq_iff). Thus left-invariant means on Haar L∞ are the same as left-invariant finitely additive probabilities on the Borel sets vanishing on Haar-null sets (MeasureTheory.exists_invariant_positiveLinearMap_lpTop_iff_exists_invariantContent, with ℝ≥0∞-valued probabilities as in the discrete TauCeti.amenable_iff_exists_invariantContent).

A content on the measurable sets vanishing on μ-null sets extends uniquely to the μ-null-measurable sets (MeasureTheory.AddContent.completion). So positive functionals on L∞(α, μ) correspond equally to nonnegative contents on the measurable sets of the completion of μ vanishing on null sets (PositiveLinearMap.addContentLpTopCompletionEquiv), and invariance under left translation again matches invariance of the content.

The construction follows the discrete case in TauCeti/Topology/ContinuousMap/Bounded/AddContent.lean, and shares its finite sums MeasureTheory.AddContent.integralSimple; the extension is LinearMap.extendOfNorm. The classes TauCeti.linftyIndicator μ s hs of indicators and MeasureTheory.SimpleFunc.toLpTop μ 𝕜 of simple functions in L∞ come from TauCeti/MeasureTheory/Function/Lp/Indicator.lean and TauCeti/MeasureTheory/Function/SimpleFunc/Dense.lean.

Main definitions

• LinearMap.toAddContentLpTop: the content s ↦ M [1_s] of a linear functional on L∞.
• PositiveLinearMap.ofAddContentLpTop: integration against a nonnegative content vanishing on null sets, as a positive linear functional on L∞.
• PositiveLinearMap.addContentLpTopEquiv: the two constructions as an equivalence onto the contents that also vanish on nonmeasurable sets.
• PositiveLinearMap.addContentLpTopCompletionEquiv: the same correspondence with contents on the null-measurable sets.

Main results

• PositiveLinearMap.ofAddContentLpTop_linftyIndicator and PositiveLinearMap.ofAddContentLpTop_toAddContentLpTop: the two constructions are inverse.

• PositiveLinearMap.ofAddContentLpTop_congr: contents agreeing on measurable sets give the same functional.

• PositiveLinearMap.forall_apply_leftTranslation_eq_iff: invariance of a functional under left translation is invariance of its content.

• MeasureTheory.exists_invariant_positiveLinearMap_lpTop_iff_exists_invariantContent: L∞ of a left-invariant measure carries a left-invariant positive functional taking the value one at one exactly when the measurable sets carry a left-invariant finitely additive probability vanishing on null sets.

• PositiveLinearMap.forall_apply_leftTranslation_eq_iff and PositiveLinearMap.forall_apply_leftTranslation_eq_iff_completion: invariance of a functional under left translation is invariance of its content, on the measurable or on the null-measurable sets.

References

• B. Bekka, P. de la Harpe, A. Valette, Kazhdan's Property (T), Appendix G, Theorem G.3.1, for the correspondence between means on L∞ and finitely additive probabilities.
• N. Dunford, J. T. Schwartz, Linear Operators, Part I, §IV.8, Theorem 16, for the dual of L∞ as the space of bounded finitely additive set functions vanishing on null sets.

noncomputable def LinearMap.toAddContentLpTop {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (m : ↥(MeasureTheory.Lp ℝ ⊤ μ) →ₗ[ℝ] ℝ) : MeasureTheory.AddContent ℝ {s : Set α | MeasurableSet s}

The real content s ↦ m [1_s] of a linear functional m on L∞(μ), on the measurable sets. Its value at a nonmeasurable set is zero.

@[simp]

theorem LinearMap.toAddContentLpTop_apply {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (m : ↥(MeasureTheory.Lp ℝ ⊤ μ) →ₗ[ℝ] ℝ) {s : Set α} (hs : MeasurableSet s) : m.toAddContentLpTop s = m (TauCeti.linftyIndicator μ s hs)

On a measurable set s, the content of m is its value at the indicator of s.

theorem LinearMap.toAddContentLpTop_of_not_measurableSet {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (m : ↥(MeasureTheory.Lp ℝ ⊤ μ) →ₗ[ℝ] ℝ) {s : Set α} (hs : ¬MeasurableSet s) : m.toAddContentLpTop s = 0

The content of a functional on L∞ is zero at nonmeasurable sets, by convention.

@[simp]

theorem LinearMap.toAddContentLpTop_univ {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (m : ↥(MeasureTheory.Lp ℝ ⊤ μ) →ₗ[ℝ] ℝ) : m.toAddContentLpTop Set.univ = m 1

The total mass of the content of m is its value at the constant one.

theorem LinearMap.toAddContentLpTop_of_measure_eq_zero {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (m : ↥(MeasureTheory.Lp ℝ ⊤ μ) →ₗ[ℝ] ℝ) {s : Set α} (hs : MeasurableSet s) (h : μ s = 0) : m.toAddContentLpTop s = 0

The content of a functional on L∞(μ) vanishes on μ-null sets.

theorem LinearMap.toAddContentLpTop_comp_leftTranslation {G : Type u_2} [Group G] [MeasurableSpace G] [MeasurableMul G] {ν : MeasureTheory.Measure G} [ν.IsMulLeftInvariant] (m : ↥(MeasureTheory.Lp ℝ ⊤ ν) →ₗ[ℝ] ℝ) (g : G) {s : Set G} (hs : MeasurableSet s) : (m ∘ₗ ↑((MeasureTheory.Lp.leftTranslation ν ⊤ ℝ) g).toLinearEquiv).toAddContentLpTop s = m.toAddContentLpTop (g • s)

Composing a functional on L∞ of a left-invariant measure with left translation by g translates its content by g.

theorem PositiveLinearMap.toAddContentLpTop_nonneg {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (M : ↥(MeasureTheory.Lp ℝ ⊤ μ) →ₚ[ℝ] ℝ) (s : Set α) : 0 ≤ M.toAddContentLpTop s

The content of a positive functional is nonnegative.

Integration against a nonnegative content

A nonnegative real content ν on the measurable sets is integrated first on simple functions, by ∑ c, c * ν {x | f x = c} (AddContent.integralSimple), and then on all of L∞ by uniform approximation. Null annihilation makes the finite sums depend only on the L∞ class.

noncomputable def PositiveLinearMap.ofAddContentLpTop {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (ν : MeasureTheory.AddContent ℝ {s : Set α | MeasurableSet s}) (hν₀ : ∀ (s : Set α), MeasurableSet s → 0 ≤ ν s) (hνμ : ∀ (s : Set α), MeasurableSet s → μ s = 0 → ν s = 0) : ↥(MeasureTheory.Lp ℝ ⊤ μ) →ₚ[ℝ] ℝ

Integration against a nonnegative real content ν on the measurable sets which vanishes on μ-null sets, as a positive linear functional on L∞(μ). It takes the value ν s at the class of the indicator of a measurable set s.

@[simp]

theorem PositiveLinearMap.ofAddContentLpTop_linftyIndicator {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.AddContent ℝ {s : Set α | MeasurableSet s}} (hν₀ : ∀ (s : Set α), MeasurableSet s → 0 ≤ ν s) (hνμ : ∀ (s : Set α), MeasurableSet s → μ s = 0 → ν s = 0) {s : Set α} (hs : MeasurableSet s) : (ofAddContentLpTop ν hν₀ hνμ) (TauCeti.linftyIndicator μ s hs) = ν s

The functional associated to a content takes the value ν s at the indicator of s.

@[simp]

theorem PositiveLinearMap.ofAddContentLpTop_one {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.AddContent ℝ {s : Set α | MeasurableSet s}} (hν₀ : ∀ (s : Set α), MeasurableSet s → 0 ≤ ν s) (hνμ : ∀ (s : Set α), MeasurableSet s → μ s = 0 → ν s = 0) : (ofAddContentLpTop ν hν₀ hνμ) 1 = ν Set.univ

The functional associated to a content takes its total mass at the constant one.

@[simp]

theorem PositiveLinearMap.toAddContentLpTop_ofAddContentLpTop_apply {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.AddContent ℝ {s : Set α | MeasurableSet s}} (hν₀ : ∀ (s : Set α), MeasurableSet s → 0 ≤ ν s) (hνμ : ∀ (s : Set α), MeasurableSet s → μ s = 0 → ν s = 0) {s : Set α} (hs : MeasurableSet s) : (ofAddContentLpTop ν hν₀ hνμ).toAddContentLpTop s = ν s

The content of the functional associated to ν is ν, on measurable sets.

@[simp]

theorem PositiveLinearMap.ofAddContentLpTop_toAddContentLpTop {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (M : ↥(MeasureTheory.Lp ℝ ⊤ μ) →ₚ[ℝ] ℝ) : ofAddContentLpTop M.toAddContentLpTop ⋯ ⋯ = M

A positive functional on L∞(μ) is the integral against its content.

theorem PositiveLinearMap.ofAddContentLpTop_congr {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {ν ν' : MeasureTheory.AddContent ℝ {s : Set α | MeasurableSet s}} (hν₀ : ∀ (s : Set α), MeasurableSet s → 0 ≤ ν s) (hνμ : ∀ (s : Set α), MeasurableSet s → μ s = 0 → ν s = 0) (hν₀' : ∀ (s : Set α), MeasurableSet s → 0 ≤ ν' s) (hνμ' : ∀ (s : Set α), MeasurableSet s → μ s = 0 → ν' s = 0) (h : ∀ (s : Set α), MeasurableSet s → ν s = ν' s) : ofAddContentLpTop ν hν₀ hνμ = ofAddContentLpTop ν' hν₀' hνμ'

Contents agreeing on measurable sets give the same functional on L∞: values of a content on nonmeasurable sets play no role.

noncomputable def PositiveLinearMap.addContentLpTopEquiv {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) : (↥(MeasureTheory.Lp ℝ ⊤ μ) →ₚ[ℝ] ℝ) ≃ { ν : MeasureTheory.AddContent ℝ {s : Set α | MeasurableSet s} // (∀ (s : Set α), 0 ≤ ν s) ∧ (∀ (s : Set α), MeasurableSet s → μ s = 0 → ν s = 0) ∧ ∀ (s : Set α), ¬MeasurableSet s → ν s = 0 }

Positive linear functionals on L∞(μ) correspond to nonnegative real contents on the measurable sets that vanish on μ-null sets and, by the convention of LinearMap.toAddContentLpTop, on nonmeasurable sets. The forward map evaluates at indicators; the inverse is PositiveLinearMap.ofAddContentLpTop.

@[simp]

theorem PositiveLinearMap.coe_addContentLpTopEquiv_apply {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (M : ↥(MeasureTheory.Lp ℝ ⊤ μ) →ₚ[ℝ] ℝ) : ↑((addContentLpTopEquiv μ) M) = M.toAddContentLpTop

The content of M under addContentLpTopEquiv is M.toLinearMap.toAddContentLpTop.

@[simp]

theorem PositiveLinearMap.addContentLpTopEquiv_symm_apply {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (ν : { ν : MeasureTheory.AddContent ℝ {s : Set α | MeasurableSet s} // (∀ (s : Set α), 0 ≤ ν s) ∧ (∀ (s : Set α), MeasurableSet s → μ s = 0 → ν s = 0) ∧ ∀ (s : Set α), ¬MeasurableSet s → ν s = 0 }) : (addContentLpTopEquiv μ).symm ν = ofAddContentLpTop ↑ν ⋯ ⋯

The functional of a content under addContentLpTopEquiv is ofAddContentLpTop.

Contents on the null-measurable sets

A content on the measurable sets vanishing on μ-null sets extends uniquely to the μ-null-measurable sets (MeasureTheory.AddContent.completion), so the correspondence holds equally for the measurable sets of the completion of μ.

noncomputable def PositiveLinearMap.addContentLpTopCompletionEquiv {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) : (↥(MeasureTheory.Lp ℝ ⊤ μ) →ₚ[ℝ] ℝ) ≃ { ν : MeasureTheory.AddContent ℝ {s : Set α | MeasureTheory.NullMeasurableSet s μ} // (∀ (s : Set α), 0 ≤ ν s) ∧ (∀ (s : Set α), μ s = 0 → ν s = 0) ∧ ∀ (s : Set α), ¬MeasureTheory.NullMeasurableSet s μ → ν s = 0 }

Positive linear functionals on L∞(μ) correspond to nonnegative real contents on the μ-null-measurable sets that vanish on μ-null sets and, by convention, on sets that are not null-measurable. The forward map extends the content LinearMap.toAddContentLpTop of a functional to the null-measurable sets; the inverse integrates against the restriction of a content to the measurable sets.

@[simp]

theorem PositiveLinearMap.coe_addContentLpTopCompletionEquiv_apply {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (M : ↥(MeasureTheory.Lp ℝ ⊤ μ) →ₚ[ℝ] ℝ) : ↑((addContentLpTopCompletionEquiv μ) M) = MeasureTheory.AddContent.completion μ M.toAddContentLpTop ⋯

The content of M under addContentLpTopCompletionEquiv extends its content on the measurable sets.

@[simp]

theorem PositiveLinearMap.addContentLpTopCompletionEquiv_symm_apply {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (ν : { ν : MeasureTheory.AddContent ℝ {s : Set α | MeasureTheory.NullMeasurableSet s μ} // (∀ (s : Set α), 0 ≤ ν s) ∧ (∀ (s : Set α), μ s = 0 → ν s = 0) ∧ ∀ (s : Set α), ¬MeasureTheory.NullMeasurableSet s μ → ν s = 0 }) : (addContentLpTopCompletionEquiv μ).symm ν = ofAddContentLpTop ((↑ν).map id ⋯) ⋯ ⋯

The functional of a content under addContentLpTopCompletionEquiv integrates against its restriction to the measurable sets.

theorem PositiveLinearMap.forall_apply_leftTranslation_eq_iff {G : Type u_2} [Group G] [MeasurableSpace G] [MeasurableMul G] {ν : MeasureTheory.Measure G} [ν.IsMulLeftInvariant] (M : ↥(MeasureTheory.Lp ℝ ⊤ ν) →ₚ[ℝ] ℝ) : (∀ (g : G) (φ : ↥(MeasureTheory.Lp ℝ ⊤ ν)), M (((MeasureTheory.Lp.leftTranslation ν ⊤ ℝ) g) φ) = M φ) ↔ ∀ (g : G) (s : Set G), MeasurableSet s → M.toAddContentLpTop (g • s) = M.toAddContentLpTop s

A positive functional on L∞ of a left-invariant measure is invariant under left translation exactly when its content is invariant under left translation of measurable sets.

theorem PositiveLinearMap.forall_apply_leftTranslation_eq_iff_completion {G : Type u_2} [Group G] [MeasurableSpace G] [MeasurableMul G] {ν : MeasureTheory.Measure G} [ν.IsMulLeftInvariant] (M : ↥(MeasureTheory.Lp ℝ ⊤ ν) →ₚ[ℝ] ℝ) : (∀ (g : G) (φ : ↥(MeasureTheory.Lp ℝ ⊤ ν)), M (((MeasureTheory.Lp.leftTranslation ν ⊤ ℝ) g) φ) = M φ) ↔ ∀ (g : G) (s : Set G), ↑((addContentLpTopCompletionEquiv ν) M) (g • s) = ↑((addContentLpTopCompletionEquiv ν) M) s

A positive functional on L∞ of a left-invariant measure is invariant under left translation exactly when its content on the null-measurable sets is invariant under left translation.

theorem MeasureTheory.exists_invariant_positiveLinearMap_lpTop_iff_exists_invariantContent {G : Type u_1} [Group G] [MeasurableSpace G] [MeasurableMul G] {μ : Measure G} [μ.IsMulLeftInvariant] : (∃ (M : ↥(Lp ℝ ⊤ μ) →ₚ[ℝ] ℝ), M 1 = 1 ∧ ∀ (g : G) (φ : ↥(Lp ℝ ⊤ μ)), M (((Lp.leftTranslation μ ⊤ ℝ) g) φ) = M φ) ↔ ∃ (ν : AddContent ENNReal {s : Set G | MeasurableSet s}), ν Set.univ = 1 ∧ (∀ (s : Set G), MeasurableSet s → μ s = 0 → ν s = 0) ∧ ∀ (g : G) (s : Set G), MeasurableSet s → ν (g • s) = ν s

Invariant means on L∞ and invariant finitely additive probabilities. For a left-invariant measure μ on a group, L∞(μ) carries a positive linear functional taking the value one at one and invariant under left translation exactly when the measurable sets carry a finitely additive probability which vanishes on μ-null sets and is invariant under left translation.