Decomposing a simple function along its fibres

This file also records how products and stars act on simple functions that are constant on a measurable set and zero off it.

A simple function u : SimpleFunc α β is the finite sum, over the values c in its range, of the constant c restricted to the fibre u ⁻¹' {c}. More generally, for any ψ : β → M into an additive commutative monoid, u.map ψ is the sum of the constants ψ c restricted to the same fibres. This is the form in which an operator defined on simple functions is evaluated by linearity, as in the Riesz–Thorin theorem.

A finite family of simple functions is one simple function into the product, MeasureTheory.SimpleFunc.pi.

theorem MeasureTheory.SimpleFunc.map_apply_eq_sum_restrict_const {α : Type u_1} {β : Type u_2} {M : Type u_3} [MeasurableSpace α] [AddCommMonoid M] (u : SimpleFunc α β) (ψ : β → M) (x : α) : (map ψ u) x = ∑ c ∈ u.range, ((const α (ψ c)).restrict (⇑u ⁻¹' {c})) x

The value of u.map ψ at x is the sum, over the range of u, of the constants ψ c restricted to the fibres u ⁻¹' {c} and evaluated at x.

theorem MeasureTheory.SimpleFunc.map_eq_sum_restrict_const {α : Type u_1} {β : Type u_2} {M : Type u_3} [MeasurableSpace α] [AddCommMonoid M] (u : SimpleFunc α β) (ψ : β → M) : map ψ u = ∑ c ∈ u.range, (const α (ψ c)).restrict (⇑u ⁻¹' {c})

A simple function mapped by ψ is the sum, over its range, of the constants ψ c restricted to the fibres u ⁻¹' {c}.

theorem MeasureTheory.SimpleFunc.eq_sum_restrict_const {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [AddCommMonoid β] (u : SimpleFunc α β) : u = ∑ c ∈ u.range, (const α c).restrict (⇑u ⁻¹' {c})

A simple function is the sum, over its range, of its values c restricted to the fibres u ⁻¹' {c}.

theorem MeasureTheory.SimpleFunc.piecewise_const_mul_piecewise_const {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MulZeroClass β] (c d : β) {A B : Set α} (hA : MeasurableSet A) (hB : MeasurableSet B) : piecewise A hA (const α c) (const α 0) * piecewise B hB (const α d) (const α 0) = piecewise (A ∩ B) ⋯ (const α (c * d)) (const α 0)

The product of two simple functions constant on measurable sets A and B and zero elsewhere is constant on A ∩ B and zero elsewhere.

theorem MeasureTheory.SimpleFunc.star_piecewise_const {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [AddMonoid β] [StarAddMonoid β] (c : β) {A : Set α} (hA : MeasurableSet A) : star (piecewise A hA (const α c) (const α 0)) = piecewise A hA (const α (star c)) (const α 0)

The star of a simple function constant on a measurable set A and zero elsewhere is constant with the starred value on A and zero elsewhere.

def MeasureTheory.SimpleFunc.pi {α : Type u_1} [MeasurableSpace α] {ι : Type u_4} [Finite ι] {β : ι → Type u_5} (f : (i : ι) → SimpleFunc α (β i)) : SimpleFunc α ((i : ι) → β i)

A finite family of simple functions f i : α →ₛ β i, as one simple function into the product ∀ i, β i. Its fibres are the intersections of the fibres of the f i.

@[simp]

theorem MeasureTheory.SimpleFunc.coe_pi {α : Type u_1} [MeasurableSpace α] {ι : Type u_4} [Finite ι] {β : ι → Type u_5} (f : (i : ι) → SimpleFunc α (β i)) : ⇑(pi f) = fun (a : α) (i : ι) => (f i) a

The simple function pi f is the function a ↦ (i ↦ f i a).

theorem MeasureTheory.SimpleFunc.pi_apply {α : Type u_1} [MeasurableSpace α] {ι : Type u_4} [Finite ι] {β : ι → Type u_5} (f : (i : ι) → SimpleFunc α (β i)) (a : α) : (pi f) a = fun (i : ι) => (f i) a

The value of pi f at a is the family of the values f i a.