# Simple functions #

A function f from a measurable space to any type is called simple, if every preimage f ⁻¹' {x} is measurable, and the range is finite. In this file, we define simple functions and establish their basic properties; and we construct a sequence of simple functions approximating an arbitrary Borel measurable function f : α → ℝ≥0∞.

The theorem Measurable.ennreal_induction shows that in order to prove something for an arbitrary measurable function into ℝ≥0∞, it is sufficient to show that the property holds for (multiples of) characteristic functions and is closed under addition and supremum of increasing sequences of functions.

structure MeasureTheory.SimpleFunc (α : Type u) [] (β : Type v) :
Type (max u v)

A function f from a measurable space to any type is called simple, if every preimage f ⁻¹' {x} is measurable, and the range is finite. This structure bundles a function with these properties.

Instances For
instance MeasureTheory.SimpleFunc.instCoeFun {α : Type u_1} {β : Type u_2} [] :
CoeFun () fun (x : ) => αβ
Equations
• MeasureTheory.SimpleFunc.instCoeFun = { coe := MeasureTheory.SimpleFunc.toFun }
theorem MeasureTheory.SimpleFunc.coe_injective {α : Type u_1} {β : Type u_2} [] ⦃f : ⦃g : (H : f = g) :
f = g
theorem MeasureTheory.SimpleFunc.ext {α : Type u_1} {β : Type u_2} [] {f : } {g : } (H : ∀ (a : α), f a = g a) :
f = g
theorem MeasureTheory.SimpleFunc.finite_range {α : Type u_1} {β : Type u_2} [] (f : ) :
theorem MeasureTheory.SimpleFunc.measurableSet_fiber {α : Type u_1} {β : Type u_2} [] (f : ) (x : β) :
theorem MeasureTheory.SimpleFunc.apply_mk {α : Type u_1} {β : Type u_2} [] (f : αβ) (h : ∀ (x : β), MeasurableSet (f ⁻¹' {x})) (h' : ) (x : α) :
{ toFun := f, measurableSet_fiber' := h, finite_range' := h' } x = f x
def MeasureTheory.SimpleFunc.ofFinite {α : Type u_1} {β : Type u_2} [] [] (f : αβ) :

Simple function defined on a finite type.

Equations
• = { toFun := f, measurableSet_fiber' := , finite_range' := }
Instances For
@[deprecated MeasureTheory.SimpleFunc.ofFinite]
def MeasureTheory.SimpleFunc.ofFintype {α : Type u_1} {β : Type u_2} [] [] (f : αβ) :

Alias of MeasureTheory.SimpleFunc.ofFinite.

Simple function defined on a finite type.

Equations
Instances For
def MeasureTheory.SimpleFunc.ofIsEmpty {α : Type u_1} {β : Type u_2} [] [] :

Simple function defined on the empty type.

Equations
Instances For
def MeasureTheory.SimpleFunc.range {α : Type u_1} {β : Type u_2} [] (f : ) :

Range of a simple function α →ₛ β as a Finset β.

Equations
Instances For
@[simp]
theorem MeasureTheory.SimpleFunc.mem_range {α : Type u_1} {β : Type u_2} [] {f : } {b : β} :
b
theorem MeasureTheory.SimpleFunc.mem_range_self {α : Type u_1} {β : Type u_2} [] (f : ) (x : α) :
@[simp]
theorem MeasureTheory.SimpleFunc.coe_range {α : Type u_1} {β : Type u_2} [] (f : ) :
theorem MeasureTheory.SimpleFunc.mem_range_of_measure_ne_zero {α : Type u_1} {β : Type u_2} [] {f : } {x : β} {μ : } (H : μ (f ⁻¹' {x}) 0) :
theorem MeasureTheory.SimpleFunc.forall_mem_range {α : Type u_1} {β : Type u_2} [] {f : } {p : βProp} :
(y, p y) ∀ (x : α), p (f x)
theorem MeasureTheory.SimpleFunc.exists_range_iff {α : Type u_1} {β : Type u_2} [] {f : } {p : βProp} :
(∃ y ∈ , p y) ∃ (x : α), p (f x)
theorem MeasureTheory.SimpleFunc.preimage_eq_empty_iff {α : Type u_1} {β : Type u_2} [] (f : ) (b : β) :
f ⁻¹' {b} =
theorem MeasureTheory.SimpleFunc.exists_forall_le {α : Type u_1} {β : Type u_2} [] [] [] [IsDirected β fun (x x_1 : β) => x x_1] (f : ) :
∃ (C : β), ∀ (x : α), f x C
def MeasureTheory.SimpleFunc.const (α : Type u_5) {β : Type u_6} [] (b : β) :

Constant function as a SimpleFunc.

Equations
• = { toFun := fun (x : α) => b, measurableSet_fiber' := , finite_range' := }
Instances For
instance MeasureTheory.SimpleFunc.instInhabited {α : Type u_1} {β : Type u_2} [] [] :
Equations
theorem MeasureTheory.SimpleFunc.const_apply {α : Type u_1} {β : Type u_2} [] (a : α) (b : β) :
a = b
@[simp]
theorem MeasureTheory.SimpleFunc.coe_const {α : Type u_1} {β : Type u_2} [] (b : β) :
@[simp]
theorem MeasureTheory.SimpleFunc.range_const {β : Type u_2} (α : Type u_5) [] [] (b : β) :
theorem MeasureTheory.SimpleFunc.range_const_subset {β : Type u_2} (α : Type u_5) [] (b : β) :
theorem MeasureTheory.SimpleFunc.simpleFunc_bot {β : Type u_2} {α : Type u_5} (f : ) [] :
∃ (c : β), ∀ (x : α), f x = c
theorem MeasureTheory.SimpleFunc.simpleFunc_bot' {β : Type u_2} {α : Type u_5} [] (f : ) :
∃ (c : β),
theorem MeasureTheory.SimpleFunc.measurableSet_cut {α : Type u_1} {β : Type u_2} [] (r : αβProp) (f : ) (h : ∀ (b : β), MeasurableSet {a : α | r a b}) :
MeasurableSet {a : α | r a (f a)}
theorem MeasureTheory.SimpleFunc.measurableSet_preimage {α : Type u_1} {β : Type u_2} [] (f : ) (s : Set β) :
theorem MeasureTheory.SimpleFunc.measurable {α : Type u_1} {β : Type u_2} [] [] (f : ) :

A simple function is measurable

theorem MeasureTheory.SimpleFunc.aemeasurable {α : Type u_1} {β : Type u_2} [] [] {μ : } (f : ) :
AEMeasurable (f) μ
theorem MeasureTheory.SimpleFunc.sum_measure_preimage_singleton {α : Type u_1} {β : Type u_2} [] (f : ) {μ : } (s : ) :
(Finset.sum s fun (y : β) => μ (f ⁻¹' {y})) = μ (f ⁻¹' s)
theorem MeasureTheory.SimpleFunc.sum_range_measure_preimage_singleton {α : Type u_1} {β : Type u_2} [] (f : ) (μ : ) :
(Finset.sum fun (y : β) => μ (f ⁻¹' {y})) = μ Set.univ
def MeasureTheory.SimpleFunc.piecewise {α : Type u_1} {β : Type u_2} [] (s : Set α) (hs : ) (f : ) (g : ) :

If-then-else as a SimpleFunc.

Equations
• = { toFun := Set.piecewise s f g, measurableSet_fiber' := , finite_range' := }
Instances For
@[simp]
theorem MeasureTheory.SimpleFunc.coe_piecewise {α : Type u_1} {β : Type u_2} [] {s : Set α} (hs : ) (f : ) (g : ) :
() = Set.piecewise s f g
theorem MeasureTheory.SimpleFunc.piecewise_apply {α : Type u_1} {β : Type u_2} [] {s : Set α} (hs : ) (f : ) (g : ) (a : α) :
() a = if a s then f a else g a
@[simp]
theorem MeasureTheory.SimpleFunc.piecewise_compl {α : Type u_1} {β : Type u_2} [] {s : Set α} (hs : ) (f : ) (g : ) :
@[simp]
theorem MeasureTheory.SimpleFunc.piecewise_univ {α : Type u_1} {β : Type u_2} [] (f : ) (g : ) :
@[simp]
theorem MeasureTheory.SimpleFunc.piecewise_empty {α : Type u_1} {β : Type u_2} [] (f : ) (g : ) :
@[simp]
theorem MeasureTheory.SimpleFunc.piecewise_same {α : Type u_1} {β : Type u_2} [] (f : ) {s : Set α} (hs : ) :
= f
theorem MeasureTheory.SimpleFunc.support_indicator {α : Type u_1} {β : Type u_2} [] [Zero β] {s : Set α} (hs : ) (f : ) :
theorem MeasureTheory.SimpleFunc.range_indicator {α : Type u_1} {β : Type u_2} [] {s : Set α} (hs : ) (hs_nonempty : ) (hs_ne_univ : s Set.univ) (x : β) (y : β) :
= {x, y}
theorem MeasureTheory.SimpleFunc.measurable_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] (f : ) (g : βαγ) (hg : ∀ (b : β), Measurable (g b)) :
Measurable fun (a : α) => g (f a) a
def MeasureTheory.SimpleFunc.bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] (f : ) (g : β) :

If f : α →ₛ β is a simple function and g : β → α →ₛ γ is a family of simple functions, then f.bind g binds the first argument of g to f. In other words, f.bind g a = g (f a) a.

Equations
• = { toFun := fun (a : α) => (g (f a)) a, measurableSet_fiber' := , finite_range' := }
Instances For
@[simp]
theorem MeasureTheory.SimpleFunc.bind_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] (f : ) (g : β) (a : α) :
a = (g (f a)) a
def MeasureTheory.SimpleFunc.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] (g : βγ) (f : ) :

Given a function g : β → γ and a simple function f : α →ₛ β, f.map g return the simple function g ∘ f : α →ₛ γ

Equations
Instances For
theorem MeasureTheory.SimpleFunc.map_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] (g : βγ) (f : ) (a : α) :
a = g (f a)
theorem MeasureTheory.SimpleFunc.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [] (g : βγ) (h : γδ) (f : ) :
@[simp]
theorem MeasureTheory.SimpleFunc.coe_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] (g : βγ) (f : ) :
= g f
@[simp]
theorem MeasureTheory.SimpleFunc.range_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] (g : βγ) (f : ) :
@[simp]
theorem MeasureTheory.SimpleFunc.map_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] (g : βγ) (b : β) :
theorem MeasureTheory.SimpleFunc.map_preimage {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] (f : ) (g : βγ) (s : Set γ) :
⁻¹' s = f ⁻¹' (Finset.filter (fun (b : β) => g b s) )
theorem MeasureTheory.SimpleFunc.map_preimage_singleton {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] (f : ) (g : βγ) (c : γ) :
⁻¹' {c} = f ⁻¹' (Finset.filter (fun (b : β) => g b = c) )
def MeasureTheory.SimpleFunc.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] (f : ) (g : αβ) (hgm : ) :

Composition of a SimpleFun and a measurable function is a SimpleFunc.

Equations
• = { toFun := f g, measurableSet_fiber' := , finite_range' := }
Instances For
@[simp]
theorem MeasureTheory.SimpleFunc.coe_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] (f : ) {g : αβ} (hgm : ) :
() = f g
theorem MeasureTheory.SimpleFunc.range_comp_subset_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] (f : ) {g : αβ} (hgm : ) :
def MeasureTheory.SimpleFunc.extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] (f₁ : ) (g : αβ) (hg : ) (f₂ : ) :

Extend a SimpleFunc along a measurable embedding: f₁.extend g hg f₂ is the function F : β →ₛ γ such that F ∘ g = f₁ and F y = f₂ y whenever y ∉ range g.

Equations
• = { toFun := Function.extend g f₁ f₂, measurableSet_fiber' := , finite_range' := }
Instances For
@[simp]
theorem MeasureTheory.SimpleFunc.extend_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] (f₁ : ) {g : αβ} (hg : ) (f₂ : ) (x : α) :
() (g x) = f₁ x
@[simp]
theorem MeasureTheory.SimpleFunc.extend_apply' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] (f₁ : ) {g : αβ} (hg : ) (f₂ : ) {y : β} (h : ¬∃ (x : α), g x = y) :
() y = f₂ y
@[simp]
theorem MeasureTheory.SimpleFunc.extend_comp_eq' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] (f₁ : ) {g : αβ} (hg : ) (f₂ : ) :
() g = f₁
@[simp]
theorem MeasureTheory.SimpleFunc.extend_comp_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] (f₁ : ) {g : αβ} (hg : ) (f₂ : ) :
def MeasureTheory.SimpleFunc.seq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] (f : MeasureTheory.SimpleFunc α (βγ)) (g : ) :

If f is a simple function taking values in β → γ and g is another simple function with the same domain and codomain β, then f.seq g = f a (g a).

Equations
Instances For
@[simp]
theorem MeasureTheory.SimpleFunc.seq_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] (f : MeasureTheory.SimpleFunc α (βγ)) (g : ) (a : α) :
a = f a (g a)
def MeasureTheory.SimpleFunc.pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] (f : ) (g : ) :

Combine two simple functions f : α →ₛ β and g : α →ₛ β into fun a => (f a, g a).

Equations
Instances For
@[simp]
theorem MeasureTheory.SimpleFunc.pair_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] (f : ) (g : ) (a : α) :
a = (f a, g a)
theorem MeasureTheory.SimpleFunc.pair_preimage {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] (f : ) (g : ) (s : Set β) (t : Set γ) :
⁻¹' s ×ˢ t = f ⁻¹' s g ⁻¹' t
theorem MeasureTheory.SimpleFunc.pair_preimage_singleton {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] (f : ) (g : ) (b : β) (c : γ) :
⁻¹' {(b, c)} = f ⁻¹' {b} g ⁻¹' {c}
theorem MeasureTheory.SimpleFunc.bind_const {α : Type u_1} {β : Type u_2} [] (f : ) :
instance MeasureTheory.SimpleFunc.instZero {α : Type u_1} {β : Type u_2} [] [Zero β] :
Equations
• MeasureTheory.SimpleFunc.instZero = { zero := }
instance MeasureTheory.SimpleFunc.instOne {α : Type u_1} {β : Type u_2} [] [One β] :
Equations
• MeasureTheory.SimpleFunc.instOne = { one := }
instance MeasureTheory.SimpleFunc.instAdd {α : Type u_1} {β : Type u_2} [] [Add β] :
Equations
• One or more equations did not get rendered due to their size.
instance MeasureTheory.SimpleFunc.instMul {α : Type u_1} {β : Type u_2} [] [Mul β] :
Equations
• One or more equations did not get rendered due to their size.
instance MeasureTheory.SimpleFunc.instSub {α : Type u_1} {β : Type u_2} [] [Sub β] :
Equations
• One or more equations did not get rendered due to their size.
instance MeasureTheory.SimpleFunc.instDiv {α : Type u_1} {β : Type u_2} [] [Div β] :
Equations
• One or more equations did not get rendered due to their size.
instance MeasureTheory.SimpleFunc.instNeg {α : Type u_1} {β : Type u_2} [] [Neg β] :
Equations
instance MeasureTheory.SimpleFunc.instInv {α : Type u_1} {β : Type u_2} [] [Inv β] :
Equations
instance MeasureTheory.SimpleFunc.instSup {α : Type u_1} {β : Type u_2} [] [Sup β] :
Equations
• One or more equations did not get rendered due to their size.
instance MeasureTheory.SimpleFunc.instInf {α : Type u_1} {β : Type u_2} [] [Inf β] :
Equations
• One or more equations did not get rendered due to their size.
instance MeasureTheory.SimpleFunc.instLE {α : Type u_1} {β : Type u_2} [] [LE β] :
Equations
• MeasureTheory.SimpleFunc.instLE = { le := fun (f g : ) => ∀ (a : α), f a g a }
@[simp]
theorem MeasureTheory.SimpleFunc.const_zero {α : Type u_1} {β : Type u_2} [] [Zero β] :
@[simp]
theorem MeasureTheory.SimpleFunc.const_one {α : Type u_1} {β : Type u_2} [] [One β] :
@[simp]
theorem MeasureTheory.SimpleFunc.coe_zero {α : Type u_1} {β : Type u_2} [] [Zero β] :
0 = 0
@[simp]
theorem MeasureTheory.SimpleFunc.coe_one {α : Type u_1} {β : Type u_2} [] [One β] :
1 = 1
@[simp]
theorem MeasureTheory.SimpleFunc.coe_add {α : Type u_1} {β : Type u_2} [] [Add β] (f : ) (g : ) :
(f + g) = f + g
@[simp]
theorem MeasureTheory.SimpleFunc.coe_mul {α : Type u_1} {β : Type u_2} [] [Mul β] (f : ) (g : ) :
(f * g) = f * g
@[simp]
theorem MeasureTheory.SimpleFunc.coe_neg {α : Type u_1} {β : Type u_2} [] [Neg β] (f : ) :
(-f) = -f
@[simp]
theorem MeasureTheory.SimpleFunc.coe_inv {α : Type u_1} {β : Type u_2} [] [Inv β] (f : ) :
f⁻¹ = (f)⁻¹
@[simp]
theorem MeasureTheory.SimpleFunc.coe_sub {α : Type u_1} {β : Type u_2} [] [Sub β] (f : ) (g : ) :
(f - g) = f - g
@[simp]
theorem MeasureTheory.SimpleFunc.coe_div {α : Type u_1} {β : Type u_2} [] [Div β] (f : ) (g : ) :
(f / g) = f / g
@[simp]
theorem MeasureTheory.SimpleFunc.coe_le {α : Type u_1} {β : Type u_2} [] [] {f : } {g : } :
f g f g
@[simp]
theorem MeasureTheory.SimpleFunc.coe_sup {α : Type u_1} {β : Type u_2} [] [Sup β] (f : ) (g : ) :
(f g) = f g
@[simp]
theorem MeasureTheory.SimpleFunc.coe_inf {α : Type u_1} {β : Type u_2} [] [Inf β] (f : ) (g : ) :
(f g) = f g
theorem MeasureTheory.SimpleFunc.add_apply {α : Type u_1} {β : Type u_2} [] [Add β] (f : ) (g : ) (a : α) :
(f + g) a = f a + g a
theorem MeasureTheory.SimpleFunc.mul_apply {α : Type u_1} {β : Type u_2} [] [Mul β] (f : ) (g : ) (a : α) :
(f * g) a = f a * g a
theorem MeasureTheory.SimpleFunc.sub_apply {α : Type u_1} {β : Type u_2} [] [Sub β] (f : ) (g : ) (x : α) :
(f - g) x = f x - g x
theorem MeasureTheory.SimpleFunc.div_apply {α : Type u_1} {β : Type u_2} [] [Div β] (f : ) (g : ) (x : α) :
(f / g) x = f x / g x
theorem MeasureTheory.SimpleFunc.neg_apply {α : Type u_1} {β : Type u_2} [] [Neg β] (f : ) (x : α) :
(-f) x = -f x
theorem MeasureTheory.SimpleFunc.inv_apply {α : Type u_1} {β : Type u_2} [] [Inv β] (f : ) (x : α) :
f⁻¹ x = (f x)⁻¹
theorem MeasureTheory.SimpleFunc.sup_apply {α : Type u_1} {β : Type u_2} [] [Sup β] (f : ) (g : ) (a : α) :
(f g) a = f a g a
theorem MeasureTheory.SimpleFunc.inf_apply {α : Type u_1} {β : Type u_2} [] [Inf β] (f : ) (g : ) (a : α) :
(f g) a = f a g a
@[simp]
theorem MeasureTheory.SimpleFunc.range_zero {α : Type u_1} {β : Type u_2} [] [] [Zero β] :
@[simp]
theorem MeasureTheory.SimpleFunc.range_one {α : Type u_1} {β : Type u_2} [] [] [One β] :
@[simp]
theorem MeasureTheory.SimpleFunc.range_eq_empty_of_isEmpty {α : Type u_1} [] {β : Type u_5} [hα : ] (f : ) :
theorem MeasureTheory.SimpleFunc.eq_zero_of_mem_range_zero {α : Type u_1} {β : Type u_2} [] [Zero β] {y : β} :
y = 0
theorem MeasureTheory.SimpleFunc.add_eq_map₂ {α : Type u_1} {β : Type u_2} [] [Add β] (f : ) (g : ) :
f + g = MeasureTheory.SimpleFunc.map (fun (p : β × β) => p.1 + p.2)
theorem MeasureTheory.SimpleFunc.mul_eq_map₂ {α : Type u_1} {β : Type u_2} [] [Mul β] (f : ) (g : ) :
f * g = MeasureTheory.SimpleFunc.map (fun (p : β × β) => p.1 * p.2)
theorem MeasureTheory.SimpleFunc.sup_eq_map₂ {α : Type u_1} {β : Type u_2} [] [Sup β] (f : ) (g : ) :
f g = MeasureTheory.SimpleFunc.map (fun (p : β × β) => p.1 p.2)
theorem MeasureTheory.SimpleFunc.const_add_eq_map {α : Type u_1} {β : Type u_2} [] [Add β] (f : ) (b : β) :
= MeasureTheory.SimpleFunc.map (fun (a : β) => b + a) f
theorem MeasureTheory.SimpleFunc.const_mul_eq_map {α : Type u_1} {β : Type u_2} [] [Mul β] (f : ) (b : β) :
= MeasureTheory.SimpleFunc.map (fun (a : β) => b * a) f
theorem MeasureTheory.SimpleFunc.map_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [Add β] [Add γ] {g : βγ} (hg : ∀ (x y : β), g (x + y) = g x + g y) (f₁ : ) (f₂ : ) :
theorem MeasureTheory.SimpleFunc.map_mul {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [Mul β] [Mul γ] {g : βγ} (hg : ∀ (x y : β), g (x * y) = g x * g y) (f₁ : ) (f₂ : ) :
instance MeasureTheory.SimpleFunc.instVAdd {α : Type u_1} {β : Type u_2} [] {K : Type u_5} [VAdd K β] :
Equations
instance MeasureTheory.SimpleFunc.instSMul {α : Type u_1} {β : Type u_2} [] {K : Type u_5} [SMul K β] :
SMul K ()
Equations
@[simp]
theorem MeasureTheory.SimpleFunc.coe_vadd {α : Type u_1} {β : Type u_2} [] {K : Type u_5} [VAdd K β] (c : K) (f : ) :
(c +ᵥ f) = c +ᵥ f
@[simp]
theorem MeasureTheory.SimpleFunc.coe_smul {α : Type u_1} {β : Type u_2} [] {K : Type u_5} [SMul K β] (c : K) (f : ) :
(c f) = c f
@[simp]
theorem MeasureTheory.SimpleFunc.vadd_apply {α : Type u_1} {β : Type u_2} [] {K : Type u_5} [VAdd K β] (k : K) (f : ) (a : α) :
(k +ᵥ f) a = k +ᵥ f a
@[simp]
theorem MeasureTheory.SimpleFunc.smul_apply {α : Type u_1} {β : Type u_2} [] {K : Type u_5} [SMul K β] (k : K) (f : ) (a : α) :
(k f) a = k f a
instance MeasureTheory.SimpleFunc.hasNatSMul {α : Type u_1} {β : Type u_2} [] [] :
Equations
• MeasureTheory.SimpleFunc.hasNatSMul = inferInstance
instance MeasureTheory.SimpleFunc.hasNatPow {α : Type u_1} {β : Type u_2} [] [] :
Equations
@[simp]
theorem MeasureTheory.SimpleFunc.coe_pow {α : Type u_1} {β : Type u_2} [] [] (f : ) (n : ) :
(f ^ n) = f ^ n
theorem MeasureTheory.SimpleFunc.pow_apply {α : Type u_1} {β : Type u_2} [] [] (n : ) (f : ) (a : α) :
(f ^ n) a = f a ^ n
instance MeasureTheory.SimpleFunc.hasIntPow {α : Type u_1} {β : Type u_2} [] [] :
Equations
@[simp]
theorem MeasureTheory.SimpleFunc.coe_zpow {α : Type u_1} {β : Type u_2} [] [] (f : ) (z : ) :
(f ^ z) = f ^ z
theorem MeasureTheory.SimpleFunc.zpow_apply {α : Type u_1} {β : Type u_2} [] [] (z : ) (f : ) (a : α) :
(f ^ z) a = f a ^ z
instance MeasureTheory.SimpleFunc.instAddMonoid {α : Type u_1} {β : Type u_2} [] [] :
Equations
instance MeasureTheory.SimpleFunc.instAddCommMonoid {α : Type u_1} {β : Type u_2} [] [] :
Equations
instance MeasureTheory.SimpleFunc.instAddGroup {α : Type u_1} {β : Type u_2} [] [] :
Equations
instance MeasureTheory.SimpleFunc.instAddCommGroup {α : Type u_1} {β : Type u_2} [] [] :
Equations
instance MeasureTheory.SimpleFunc.instMonoid {α : Type u_1} {β : Type u_2} [] [] :
Equations
instance MeasureTheory.SimpleFunc.instCommMonoid {α : Type u_1} {β : Type u_2} [] [] :
Equations
instance MeasureTheory.SimpleFunc.instGroup {α : Type u_1} {β : Type u_2} [] [] :
Equations
• MeasureTheory.SimpleFunc.instGroup = Function.Injective.group (fun (f : ) => let_fun this := f; this)
instance MeasureTheory.SimpleFunc.instCommGroup {α : Type u_1} {β : Type u_2} [] [] :
Equations
instance MeasureTheory.SimpleFunc.instModule {α : Type u_1} {β : Type u_2} [] {K : Type u_5} [] [] [Module K β] :
Equations
• One or more equations did not get rendered due to their size.
theorem MeasureTheory.SimpleFunc.smul_eq_map {α : Type u_1} {β : Type u_2} [] {K : Type u_5} [SMul K β] (k : K) (f : ) :
k f = MeasureTheory.SimpleFunc.map (fun (x : β) => k x) f
instance MeasureTheory.SimpleFunc.instPreorder {α : Type u_1} {β : Type u_2} [] [] :
Equations
• MeasureTheory.SimpleFunc.instPreorder = let __src := MeasureTheory.SimpleFunc.instLE; Preorder.mk
instance MeasureTheory.SimpleFunc.instPartialOrder {α : Type u_1} {β : Type u_2} [] [] :
Equations
• MeasureTheory.SimpleFunc.instPartialOrder = let __src := MeasureTheory.SimpleFunc.instPreorder;
instance MeasureTheory.SimpleFunc.instOrderBot {α : Type u_1} {β : Type u_2} [] [LE β] [] :
Equations
• MeasureTheory.SimpleFunc.instOrderBot =
instance MeasureTheory.SimpleFunc.instOrderTop {α : Type u_1} {β : Type u_2} [] [LE β] [] :
Equations
• MeasureTheory.SimpleFunc.instOrderTop =
instance MeasureTheory.SimpleFunc.instSemilatticeInf {α : Type u_1} {β : Type u_2} [] [] :
Equations
• MeasureTheory.SimpleFunc.instSemilatticeInf = let __src := MeasureTheory.SimpleFunc.instPartialOrder;
instance MeasureTheory.SimpleFunc.instSemilatticeSup {α : Type u_1} {β : Type u_2} [] [] :
Equations
• MeasureTheory.SimpleFunc.instSemilatticeSup = let __src := MeasureTheory.SimpleFunc.instPartialOrder;
instance MeasureTheory.SimpleFunc.instLattice {α : Type u_1} {β : Type u_2} [] [] :
Equations
• MeasureTheory.SimpleFunc.instLattice = let __src := MeasureTheory.SimpleFunc.instSemilatticeSup; let __src_1 := MeasureTheory.SimpleFunc.instSemilatticeInf; Lattice.mk
instance MeasureTheory.SimpleFunc.instBoundedOrder {α : Type u_1} {β : Type u_2} [] [LE β] [] :
Equations
• MeasureTheory.SimpleFunc.instBoundedOrder = let __src := MeasureTheory.SimpleFunc.instOrderBot; let __src_1 := MeasureTheory.SimpleFunc.instOrderTop; BoundedOrder.mk
theorem MeasureTheory.SimpleFunc.finset_sup_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f : γ} (s : ) (a : α) :
() a = Finset.sup s fun (c : γ) => (f c) a
def MeasureTheory.SimpleFunc.restrict {α : Type u_1} {β : Type u_2} [] [Zero β] (f : ) (s : Set α) :

Restrict a simple function f : α →ₛ β to a set s. If s is measurable, then f.restrict s a = if a ∈ s then f a else 0, otherwise f.restrict s = const α 0.

Equations
• = if hs : then else 0
Instances For
theorem MeasureTheory.SimpleFunc.restrict_of_not_measurable {α : Type u_1} {β : Type u_2} [] [Zero β] {f : } {s : Set α} (hs : ) :
@[simp]
theorem MeasureTheory.SimpleFunc.coe_restrict {α : Type u_1} {β : Type u_2} [] [Zero β] (f : ) {s : Set α} (hs : ) :
=
@[simp]
theorem MeasureTheory.SimpleFunc.restrict_univ {α : Type u_1} {β : Type u_2} [] [Zero β] (f : ) :
@[simp]
theorem MeasureTheory.SimpleFunc.restrict_empty {α : Type u_1} {β : Type u_2} [] [Zero β] (f : ) :
theorem MeasureTheory.SimpleFunc.map_restrict_of_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [Zero β] [Zero γ] {g : βγ} (hg : g 0 = 0) (f : ) (s : Set α) :
theorem MeasureTheory.SimpleFunc.restrict_apply {α : Type u_1} {β : Type u_2} [] [Zero β] (f : ) {s : Set α} (hs : ) (a : α) :
= Set.indicator s (f) a
theorem MeasureTheory.SimpleFunc.restrict_preimage {α : Type u_1} {β : Type u_2} [] [Zero β] (f : ) {s : Set α} (hs : ) {t : Set β} (ht : 0t) :
= s f ⁻¹' t
theorem MeasureTheory.SimpleFunc.restrict_preimage_singleton {α : Type u_1} {β : Type u_2} [] [Zero β] (f : ) {s : Set α} (hs : ) {r : β} (hr : r 0) :
⁻¹' {r} = s f ⁻¹' {r}
theorem MeasureTheory.SimpleFunc.mem_restrict_range {α : Type u_1} {β : Type u_2} [] [Zero β] {r : β} {s : Set α} {f : } (hs : ) :
r = 0 s Set.univ r f '' s
theorem MeasureTheory.SimpleFunc.mem_image_of_mem_range_restrict {α : Type u_1} {β : Type u_2} [] [Zero β] {r : β} {s : Set α} {f : } (hr : ) (h0 : r 0) :
r f '' s
theorem MeasureTheory.SimpleFunc.restrict_mono {α : Type u_1} {β : Type u_2} [] [Zero β] [] (s : Set α) {f : } {g : } (H : f g) :
def MeasureTheory.SimpleFunc.approx {α : Type u_1} {β : Type u_2} [] [] [] [Zero β] (i : β) (f : αβ) (n : ) :

Fix a sequence i : ℕ → β. Given a function α → β, its n-th approximation by simple functions is defined so that in case β = ℝ≥0∞ it sends each a to the supremum of the set {i k | k ≤ n ∧ i k ≤ f a}, see approx_apply and iSup_approx_apply for details.

Equations
Instances For
theorem MeasureTheory.SimpleFunc.approx_apply {α : Type u_1} {β : Type u_2} [] [] [] [Zero β] [] [] {i : β} {f : αβ} {n : } (a : α) (hf : ) :
() a = Finset.sup () fun (k : ) => if i k f a then i k else 0
theorem MeasureTheory.SimpleFunc.monotone_approx {α : Type u_1} {β : Type u_2} [] [] [] [Zero β] (i : β) (f : αβ) :
theorem MeasureTheory.SimpleFunc.approx_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [Zero β] [] [] [] {i : β} {f : γβ} {g : αγ} {n : } (a : α) (hf : ) (hg : ) :
(MeasureTheory.SimpleFunc.approx i (f g) n) a = () (g a)
theorem MeasureTheory.SimpleFunc.iSup_approx_apply {α : Type u_1} {β : Type u_2} [] [] [] [Zero β] [] (i : β) (f : αβ) (a : α) (hf : ) (h_zero : 0 = ) :
⨆ (n : ), () a = ⨆ (k : ), ⨆ (_ : i k f a), i k

A sequence of ℝ≥0∞s such that its range is the set of non-negative rational numbers.

Equations
Instances For
def MeasureTheory.SimpleFunc.eapprox {α : Type u_1} [] :
(αENNReal)

Approximate a function α → ℝ≥0∞ by a sequence of simple functions.

Equations
• MeasureTheory.SimpleFunc.eapprox =
Instances For
theorem MeasureTheory.SimpleFunc.eapprox_lt_top {α : Type u_1} [] (f : αENNReal) (n : ) (a : α) :
a <
theorem MeasureTheory.SimpleFunc.monotone_eapprox {α : Type u_1} [] (f : αENNReal) :
theorem MeasureTheory.SimpleFunc.iSup_eapprox_apply {α : Type u_1} [] (f : αENNReal) (hf : ) (a : α) :
⨆ (n : ), a = f a
theorem MeasureTheory.SimpleFunc.eapprox_comp {α : Type u_1} {γ : Type u_3} [] [] {f : γENNReal} {g : αγ} {n : } (hf : ) (hg : ) :
() =
def MeasureTheory.SimpleFunc.eapproxDiff {α : Type u_1} [] (f : αENNReal) :

Approximate a function α → ℝ≥0∞ by a series of simple functions taking their values in ℝ≥0.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem MeasureTheory.SimpleFunc.sum_eapproxDiff {α : Type u_1} [] (f : αENNReal) (n : ) (a : α) :
(Finset.sum (Finset.range (n + 1)) fun (k : ) => ()) = a
theorem MeasureTheory.SimpleFunc.tsum_eapproxDiff {α : Type u_1} [] (f : αENNReal) (hf : ) (a : α) :
∑' (n : ), () = f a
def MeasureTheory.SimpleFunc.lintegral {α : Type u_1} {_m : } (f : ) (μ : ) :

Integral of a simple function whose codomain is ℝ≥0∞.

Equations
Instances For
theorem MeasureTheory.SimpleFunc.lintegral_eq_of_subset {α : Type u_1} {m : } {μ : } (f : ) {s : } (hs : ∀ (x : α), f x 0μ (f ⁻¹' {f x}) 0f x s) :
= Finset.sum s fun (x : ENNReal) => x * μ (f ⁻¹' {x})
theorem MeasureTheory.SimpleFunc.lintegral_eq_of_subset' {α : Type u_1} {m : } {μ : } (f : ) {s : } (hs : s) :
= Finset.sum s fun (x : ENNReal) => x * μ (f ⁻¹' {x})
theorem MeasureTheory.SimpleFunc.map_lintegral {α : Type u_1} {β : Type u_2} {m : } {μ : } (g : βENNReal) (f : ) :
= Finset.sum fun (x : β) => g x * μ (f ⁻¹' {x})

Calculate the integral of (g ∘ f), where g : β → ℝ≥0∞ and f : α →ₛ β.

theorem MeasureTheory.SimpleFunc.add_lintegral {α : Type u_1} {m : } {μ : } (f : ) (g : ) :
theorem MeasureTheory.SimpleFunc.const_mul_lintegral {α : Type u_1} {m : } {μ : } (f : ) (x : ENNReal) :

Integral of a simple function α →ₛ ℝ≥0∞ as a bilinear map.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MeasureTheory.SimpleFunc.zero_lintegral {α : Type u_1} {m : } {μ : } :
theorem MeasureTheory.SimpleFunc.lintegral_add {α : Type u_1} {m : } {μ : } {ν : } (f : ) :
theorem MeasureTheory.SimpleFunc.lintegral_smul {α : Type u_1} {m : } {μ : } (f : ) (c : ENNReal) :
@[simp]
theorem MeasureTheory.SimpleFunc.lintegral_zero {α : Type u_1} [] (f : ) :
theorem MeasureTheory.SimpleFunc.lintegral_sum {α : Type u_1} {m : } {ι : Type u_5} (f : ) (μ : ) :
= ∑' (i : ι),
theorem MeasureTheory.SimpleFunc.restrict_lintegral {α : Type u_1} {m : } {μ : } (f : ) {s : Set α} (hs : ) :
= Finset.sum fun (r : ENNReal) => r * μ (f ⁻¹' {r} s)
theorem MeasureTheory.SimpleFunc.lintegral_restrict {α : Type u_1} {m : } (f : ) (s : Set α) (μ : ) :
MeasureTheory.SimpleFunc.lintegral f (μ.restrict s) = Finset.sum fun (y : ENNReal) => y * μ (f ⁻¹' {y} s)
theorem MeasureTheory.SimpleFunc.restrict_lintegral_eq_lintegral_restrict {α : Type u_1} {m : } {μ : } (f : ) {s : Set α} (hs : ) :
theorem MeasureTheory.SimpleFunc.const_lintegral {α : Type u_1} {m : } {μ : } (c : ENNReal) :
= c * μ Set.univ
theorem MeasureTheory.SimpleFunc.const_lintegral_restrict {α : Type u_1} {m : } {μ : } (c : ENNReal) (s : Set α) :
MeasureTheory.SimpleFunc.lintegral (μ.restrict s) = c * μ s
theorem MeasureTheory.SimpleFunc.restrict_const_lintegral {α : Type u_1} {m : } {μ : } (c : ENNReal) {s : Set α} (hs : ) :
theorem MeasureTheory.SimpleFunc.le_sup_lintegral {α : Type u_1} {m : } {μ : } (f : ) (g : ) :
theorem MeasureTheory.SimpleFunc.lintegral_mono {α : Type u_1} {m : } {μ : } {ν : } {f : } {g : } (hfg : f g) (hμν : μ ν) :

SimpleFunc.lintegral is monotone both in function and in measure.

theorem MeasureTheory.SimpleFunc.lintegral_eq_of_measure_preimage {α : Type u_1} {β : Type u_2} {m : } {μ : } [] {f : } {g : } {ν : } (H : ∀ (y : ENNReal), μ (f ⁻¹' {y}) = ν (g ⁻¹' {y})) :

SimpleFunc.lintegral depends only on the measures of f ⁻¹' {y}.

theorem MeasureTheory.SimpleFunc.lintegral_congr {α : Type u_1} {m : } {μ : } {f : } {g : } (h : ) :

If two simple functions are equal a.e., then their lintegrals are equal.

theorem MeasureTheory.SimpleFunc.lintegral_map' {α : Type u_1} {m : } {μ : } {β : Type u_5} [] {μ' : } (f : ) (g : ) (m' : αβ) (eq : ∀ (a : α), f a = g (m' a)) (h : ∀ (s : Set β), μ' s = μ (m' ⁻¹' s)) :
theorem MeasureTheory.SimpleFunc.lintegral_map {α : Type u_1} {m : } {μ : } {β : Type u_5} [] (g : ) {f : αβ} (hf : ) :
theorem MeasureTheory.SimpleFunc.support_eq {α : Type u_1} {β : Type u_2} [] [Zero β] (f : ) :
= ⋃ y ∈ Finset.filter (fun (y : β) => y 0) , f ⁻¹' {y}
theorem MeasureTheory.SimpleFunc.measurableSet_support {α : Type u_1} {β : Type u_2} [Zero β] [] (f : ) :
def MeasureTheory.SimpleFunc.FinMeasSupp {α : Type u_1} {β : Type u_2} [Zero β] {_m : } (f : ) (μ : ) :

A SimpleFunc has finite measure support if it is equal to 0 outside of a set of finite measure.

Equations
Instances For
theorem MeasureTheory.SimpleFunc.finMeasSupp_iff_support {α : Type u_1} {β : Type u_2} {m : } [Zero β] {μ : } {f : } :
μ () <
theorem MeasureTheory.SimpleFunc.finMeasSupp_iff {α : Type u_1} {β : Type u_2} {m : } [Zero β] {μ : } {f : } :
∀ (y : β), y 0μ (f ⁻¹' {y}) <
theorem MeasureTheory.SimpleFunc.FinMeasSupp.meas_preimage_singleton_ne_zero {α : Type u_1} {β : Type u_2} {m : } [Zero β] {μ : } {f : } (h : ) {y : β} (hy : y 0) :
μ (f ⁻¹' {y}) <
theorem MeasureTheory.SimpleFunc.FinMeasSupp.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : } [Zero β] [Zero γ] {μ : } {f : } {g : βγ} (hf : ) (hg : g 0 = 0) :
theorem MeasureTheory.SimpleFunc.FinMeasSupp.of_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : } [Zero β] [Zero γ] {μ : } {f : } {g : βγ} (hg : ∀ (b : β), g b = 0b = 0) :
theorem MeasureTheory.SimpleFunc.FinMeasSupp.map_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : } [Zero β] [Zero γ] {μ : } {f : } {g : βγ} (hg : ∀ {b : β}, g b = 0 b = 0) :
theorem MeasureTheory.SimpleFunc.FinMeasSupp.pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : } [Zero β] [Zero γ] {μ : } {f : } {g : } (hf : ) (hg : ) :
theorem MeasureTheory.SimpleFunc.FinMeasSupp.map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m : } [Zero β] [Zero γ] {μ : } {f : } [Zero δ] (hf : ) {g : } (hg : ) {op : βγδ} (H : op 0 0 = 0) :
theorem MeasureTheory.SimpleFunc.FinMeasSupp.add {α : Type u_1} {m : } {μ : } {β : Type u_5} [] {f : } {g : } (hf : ) (hg : ) :
theorem MeasureTheory.SimpleFunc.FinMeasSupp.mul {α : Type u_1} {m : } {μ : } {β : Type u_5} [] {f : } {g : } (hf : ) (hg : ) :
theorem MeasureTheory.SimpleFunc.FinMeasSupp.lintegral_lt_top {α : Type u_1} {m : } {μ : } {f : } (hm : ) (hf : ∀ᵐ (a : α) ∂μ, f a ) :
theorem MeasureTheory.SimpleFunc.FinMeasSupp.of_lintegral_ne_top {α : Type u_1} {m : } {μ : } {f : } (h : ) :
theorem MeasureTheory.SimpleFunc.FinMeasSupp.iff_lintegral_lt_top {α : Type u_1} {m : } {μ : } {f : } (hf : ∀ᵐ (a : α) ∂μ, f a ) :
theorem MeasureTheory.SimpleFunc.induction {α : Type u_5} {γ : Type u_6} [] [] {P : } (h_ind : ∀ (c : γ) {s : Set α} (hs : ), ) (h_add : ∀ ⦃f g : ⦄, Disjoint () ()P fP gP (f + g)) (f : ) :
P f

To prove something for an arbitrary simple function, it suffices to show that the property holds for (multiples of) characteristic functions and is closed under addition (of functions with disjoint support).

It is possible to make the hypotheses in h_add a bit stronger, and such conditions can be added once we need them (for example it is only necessary to consider the case where g is a multiple of a characteristic function, and that this multiple doesn't appear in the image of f)

theorem Measurable.add_simpleFunc {α : Type u_1} {E : Type u_5} :
∀ {x : } [inst : ] [inst_1 : ] [inst_2 : ] {g : αE}, ∀ (f : ), Measurable (g + f)

In a topological vector space, the addition of a measurable function and a simple function is measurable.

theorem Measurable.simpleFunc_add {α : Type u_1} {E : Type u_5} :
∀ {x : } [inst : ] [inst_1 : ] [inst_2 : ] {g : αE}, ∀ (f : ), Measurable (f + g)

In a topological vector space, the addition of a simple function and a measurable function is measurable.

theorem Measurable.ennreal_induction {α : Type u_1} [] {P : (αENNReal)Prop} (h_ind : ∀ (c : ENNReal) ⦃s : Set α⦄, P (Set.indicator s fun (x : α) => c)) (h_add : ∀ ⦃f g : αENNReal⦄, P fP gP (f + g)) (h_iSup : ∀ ⦃f : αENNReal⦄, (∀ (n : ), Measurable (f n))(∀ (n : ), P (f n))P fun (x : α) => ⨆ (n : ), f n x) ⦃f : αENNReal (hf : ) :
P f

To prove something for an arbitrary measurable function into ℝ≥0∞, it suffices to show that the property holds for (multiples of) characteristic functions and is closed under addition and supremum of increasing sequences of functions.

It is possible to make the hypotheses in the induction steps a bit stronger, and such conditions can be added once we need them (for example in h_add it is only necessary to consider the sum of a simple function with a multiple of a characteristic function and that the intersection of their images is a subset of {0}.