Indicator classes in Lᵖ

The class MeasureTheory.indicatorConstLp p hs hμs c of s.indicator fun _ => c is linear in the constant c: Mathlib provides additivity, MeasureTheory.indicatorConstLp_add, and this file adds compatibility with scalar multiplication. Together with the norm formula MeasureTheory.norm_indicatorConstLp, this makes c ↦ indicatorConstLp p hs hμs c a bounded linear map, so closed subspaces of Lᵖ can be tested on indicator classes of a dense set of constants.

Indicator classes of pairwise disjoint sets of finite measure span a weighted finite ℓ¹ space inside L¹: the norm of ∑ i, indicatorConstLp 1 (hs i) (hμs i) (c i) is ∑ i, μ(s i) * ‖c i‖. An Lᵖ class represented by φ ∘ G for a simple function G is the sum of the indicator classes of the fibres of G with constants φ w.

In L∞ the indicator of any measurable set is essentially bounded, whatever its measure. The class TauCeti.linftyIndicator μ s hs of 1_s in real L∞(μ) therefore needs no finiteness of μ s, unlike indicatorConstLp. It is additive on disjoint sets, nonnegative, vanishes on null sets, and equals the constant one at univ.

Main declarations

• TauCeti.indicatorConstLp_smul: the indicator class of a • c is a times that of c.
• TauCeti.norm_sum_indicatorConstLp_one: the L¹ norm of a sum of indicator classes of pairwise disjoint sets.
• TauCeti.eq_sum_indicatorConstLp_fiber: an Lᵖ class represented by φ ∘ G, for a simple function G, as a sum of indicator classes of the fibres of G.
• MeasureTheory.SimpleFunc.memLp_indicator, MeasureTheory.SimpleFunc.integrable_indicator: a simple function cut off to a measurable set of finite measure lies in every Lᵖ.
• TauCeti.linftyIndicator μ s hs: the class in L∞(μ) of the indicator of a measurable set.
• MeasureTheory.SimpleFunc.toLpTop_piecewise_const_zero: the class of a simple function c • 1_s is c • linftyIndicator μ s hs.
• LinearMap.ext_linftyIndicator: a continuous linear map out of real L∞ is determined by its values at the classes linftyIndicator μ s hs.
• PositiveLinearMap.ext_linftyIndicator: the same for positive linear functionals on real L∞, which are automatically continuous.

theorem TauCeti.indicatorConstLp_smul {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedAddCommGroup E] [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (a : 𝕜) (c : E) : MeasureTheory.indicatorConstLp p hs hμs (a • c) = a • MeasureTheory.indicatorConstLp p hs hμs c

A version of Set.indicator_const_smul for MeasureTheory.indicatorConstLp.

theorem TauCeti.norm_sum_indicatorConstLp_one {α : Type u_1} {E : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {ι : Type u_4} [Fintype ι] {s : ι → Set α} (hs : ∀ (i : ι), MeasurableSet (s i)) (hμs : ∀ (i : ι), μ (s i) ≠ ⊤) (hd : Pairwise (Function.onFun Disjoint s)) (c : ι → E) : ‖∑ i : ι, MeasureTheory.indicatorConstLp 1 ⋯ ⋯ (c i)‖ = ∑ i : ι, μ.real (s i) * ‖c i‖

The L¹ norm of a sum of indicator classes of pairwise disjoint sets of finite measure is the sum of the norms of the constants, weighted by the measures of the sets.

theorem TauCeti.eq_sum_indicatorConstLp_fiber {α : Type u_1} {E : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedAddCommGroup E] {F : Type u_5} {G : MeasureTheory.SimpleFunc α F} {φ : F → E} {S : Finset F} (hS : ∀ (a : α), G a ∉ S → φ (G a) = 0) (hμS : ∀ (w : ↥S), μ (⇑G ⁻¹' {↑w}) ≠ ⊤) {x : ↥(MeasureTheory.Lp E p μ)} (hx : ↑↑x =ᵐ[μ] fun (a : α) => φ (G a)) : x = ∑ w : ↥S, MeasureTheory.indicatorConstLp p ⋯ ⋯ (φ ↑w)

An Lᵖ class that is almost everywhere φ ∘ G, for a simple function G, is the sum over a finite set S of values of G of the indicator classes of the fibres G ⁻¹' {w} with constants φ w, provided that φ ∘ G vanishes wherever G takes a value outside S.

theorem TauCeti.memLp_indicator_of_continuousOn_of_norm_le {α : Type u_1} {E : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedAddCommGroup E] {s : Set α} [TopologicalSpace α] [OpensMeasurableSpace α] [SecondCountableTopologyEither α E] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) {g : α → E} (hg : ContinuousOn g s) {M : ℝ} (hM : ∀ x ∈ s, ‖g x‖ ≤ M) : MeasureTheory.MemLp (s.indicator g) p μ

A function that is continuous and bounded on a measurable set of finite measure, extended by zero outside it, lies in every L^p space.

theorem MeasureTheory.SimpleFunc.memLp_indicator {α : Type u_1} {E : Type u_3} [MeasurableSpace α] {μ : Measure α} {p : ENNReal} [NormedAddCommGroup E] {s : Set α} (g : SimpleFunc α E) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) : MemLp (s.indicator ⇑g) p μ

A simple function cut off to a measurable set of finite measure lies in every Lᵖ space.

theorem MeasureTheory.SimpleFunc.integrable_indicator {α : Type u_1} {E : Type u_3} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] {s : Set α} (g : SimpleFunc α E) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) : Integrable (s.indicator ⇑g) μ

A simple function cut off to a measurable set of finite measure is integrable.

noncomputable def TauCeti.linftyIndicator {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α) (hs : MeasurableSet s) : ↥(MeasureTheory.Lp ℝ ⊤ μ)

The class in L∞(μ) of the indicator function of a measurable set. Unlike MeasureTheory.indicatorConstLp, it needs no finiteness of μ s.

@[simp]

theorem MeasureTheory.SimpleFunc.toLpTop_piecewise_const_zero {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {s : Set α} (hs : MeasurableSet s) (c : ℝ) : (toLpTop μ ℝ) (piecewise s hs (const α c) 0) = c • TauCeti.linftyIndicator μ s hs

A constant multiple of an indicator, as a simple function, has class a multiple of TauCeti.linftyIndicator.

theorem TauCeti.coeFn_linftyIndicator {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) : ↑↑(linftyIndicator μ s hs) =ᵐ[μ] s.indicator 1

The class TauCeti.linftyIndicator μ s hs is almost everywhere the indicator of s.

@[simp]

theorem TauCeti.linftyIndicator_empty {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} : linftyIndicator μ ∅ ⋯ = 0

The indicator of the empty set vanishes in L∞.

@[simp]

theorem TauCeti.linftyIndicator_univ {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} : linftyIndicator μ Set.univ ⋯ = 1

The indicator of the whole space is the constant one in L∞.

theorem TauCeti.linftyIndicator_union {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) (hst : Disjoint s t) : linftyIndicator μ (s ∪ t) ⋯ = linftyIndicator μ s hs + linftyIndicator μ t ht

Indicators of disjoint measurable sets add in L∞.

theorem TauCeti.linftyIndicator_nonneg {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) : 0 ≤ linftyIndicator μ s hs

The indicator of a measurable set is nonnegative in L∞.

theorem TauCeti.linftyIndicator_of_measure_eq_zero {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) (h : μ s = 0) : linftyIndicator μ s hs = 0

The indicator of a null set vanishes in L∞.

theorem LinearMap.ext_linftyIndicator {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {E : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [T2Space E] {f g : ↥(MeasureTheory.Lp ℝ ⊤ μ) →ₗ[ℝ] E} (hf : Continuous ⇑f) (hg : Continuous ⇑g) (h : ∀ (s : Set α) (hs : MeasurableSet s), f (TauCeti.linftyIndicator μ s hs) = g (TauCeti.linftyIndicator μ s hs)) : f = g

A continuous linear map out of real L∞ is determined by its values at the indicators of measurable sets.

theorem PositiveLinearMap.ext_linftyIndicator {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {M N : ↥(MeasureTheory.Lp ℝ ⊤ μ) →ₚ[ℝ] ℝ} (h : ∀ (s : Set α) (hs : MeasurableSet s), M (TauCeti.linftyIndicator μ s hs) = N (TauCeti.linftyIndicator μ s hs)) : M = N

A positive linear functional on real L∞ is determined by its values at the indicators of measurable sets.