# mathlib3documentation

measure_theory.function.simple_func

# Simple functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 measure_theory.simple_func (α : 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 `measure_theory.simple_func`
@[protected, instance]
def measure_theory.simple_func.has_coe_to_fun {α : Type u_1} {β : Type u_2}  :
(λ (_x : , α β)
Equations
theorem measure_theory.simple_func.coe_injective {α : Type u_1} {β : Type u_2} ⦃f g : β⦄ (H : f = g) :
f = g
@[ext]
theorem measure_theory.simple_func.ext {α : Type u_1} {β : Type u_2} {f g : β} (H : (a : α), f a = g a) :
f = g
theorem measure_theory.simple_func.finite_range {α : Type u_1} {β : Type u_2} (f : β) :
theorem measure_theory.simple_func.measurable_set_fiber {α : Type u_1} {β : Type u_2} (f : β) (x : β) :
@[simp]
theorem measure_theory.simple_func.apply_mk {α : Type u_1} {β : Type u_2} (f : α β) (h : (x : β), measurable_set (f ⁻¹' {x})) (h' : (set.range f).finite) (x : α) :
def measure_theory.simple_func.of_is_empty {α : Type u_1} {β : Type u_2} [is_empty α] :

Simple function defined on the empty type.

Equations
@[protected]
noncomputable def measure_theory.simple_func.range {α : Type u_1} {β : Type u_2} (f : β) :

Range of a simple function `α →ₛ β` as a `finset β`.

Equations
@[simp]
theorem measure_theory.simple_func.mem_range {α : Type u_1} {β : Type u_2} {f : β} {b : β} :
b f.range b
theorem measure_theory.simple_func.mem_range_self {α : Type u_1} {β : Type u_2} (f : β) (x : α) :
@[simp]
theorem measure_theory.simple_func.coe_range {α : Type u_1} {β : Type u_2} (f : β) :
(f.range) =
theorem measure_theory.simple_func.mem_range_of_measure_ne_zero {α : Type u_1} {β : Type u_2} {f : β} {x : β} {μ : measure_theory.measure α} (H : μ (f ⁻¹' {x}) 0) :
theorem measure_theory.simple_func.forall_range_iff {α : Type u_1} {β : Type u_2} {f : β} {p : β Prop} :
( (y : β), y f.range p y) (x : α), p (f x)
theorem measure_theory.simple_func.exists_range_iff {α : Type u_1} {β : Type u_2} {f : β} {p : β Prop} :
( (y : β) (H : y f.range), p y) (x : α), p (f x)
theorem measure_theory.simple_func.preimage_eq_empty_iff {α : Type u_1} {β : Type u_2} (f : β) (b : β) :
theorem measure_theory.simple_func.exists_forall_le {α : Type u_1} {β : Type u_2} [nonempty β] [preorder β] (f : β) :
(C : β), (x : α), f x C
def measure_theory.simple_func.const (α : Type u_1) {β : Type u_2} (b : β) :

Constant function as a `simple_func`.

Equations
@[protected, instance]
def measure_theory.simple_func.inhabited {α : Type u_1} {β : Type u_2} [inhabited β] :
Equations
theorem measure_theory.simple_func.const_apply {α : Type u_1} {β : Type u_2} (a : α) (b : β) :
= b
@[simp]
theorem measure_theory.simple_func.coe_const {α : Type u_1} {β : Type u_2} (b : β) :
@[simp]
theorem measure_theory.simple_func.range_const {β : Type u_2} (α : Type u_1) [nonempty α] (b : β) :
= {b}
theorem measure_theory.simple_func.range_const_subset {β : Type u_2} (α : Type u_1) (b : β) :
{b}
theorem measure_theory.simple_func.simple_func_bot {β : Type u_2} {α : Type u_1} (f : β) [nonempty β] :
(c : β), (x : α), f x = c
theorem measure_theory.simple_func.simple_func_bot' {β : Type u_2} {α : Type u_1} [nonempty β] (f : β) :
(c : β),
theorem measure_theory.simple_func.measurable_set_cut {α : Type u_1} {β : Type u_2} (r : α β Prop) (f : β) (h : (b : β), measurable_set {a : α | r a b}) :
measurable_set {a : α | r a (f a)}
@[measurability]
theorem measure_theory.simple_func.measurable_set_preimage {α : Type u_1} {β : Type u_2} (f : β) (s : set β) :
@[protected, measurability]
theorem measure_theory.simple_func.measurable {α : Type u_1} {β : Type u_2} (f : β) :

A simple function is measurable

@[protected, measurability]
theorem measure_theory.simple_func.ae_measurable {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (f : β) :
@[protected]
theorem measure_theory.simple_func.sum_measure_preimage_singleton {α : Type u_1} {β : Type u_2} (f : β) {μ : measure_theory.measure α} (s : finset β) :
s.sum (λ (y : β), μ (f ⁻¹' {y})) = μ (f ⁻¹' s)
theorem measure_theory.simple_func.sum_range_measure_preimage_singleton {α : Type u_1} {β : Type u_2} (f : β) (μ : measure_theory.measure α) :
f.range.sum (λ (y : β), μ (f ⁻¹' {y})) =
noncomputable def measure_theory.simple_func.piecewise {α : Type u_1} {β : Type u_2} (s : set α) (hs : measurable_set s) (f g : β) :

If-then-else as a `simple_func`.

Equations
@[simp]
theorem measure_theory.simple_func.coe_piecewise {α : Type u_1} {β : Type u_2} {s : set α} (hs : measurable_set s) (f g : β) :
theorem measure_theory.simple_func.piecewise_apply {α : Type u_1} {β : Type u_2} {s : set α} (hs : measurable_set s) (f g : β) (a : α) :
g) a = ite (a s) (f a) (g a)
@[simp]
theorem measure_theory.simple_func.piecewise_compl {α : Type u_1} {β : Type u_2} {s : set α} (hs : measurable_set s) (f g : β) :
@[simp]
theorem measure_theory.simple_func.piecewise_univ {α : Type u_1} {β : Type u_2} (f g : β) :
@[simp]
theorem measure_theory.simple_func.piecewise_empty {α : Type u_1} {β : Type u_2} (f g : β) :
theorem measure_theory.simple_func.support_indicator {α : Type u_1} {β : Type u_2} [has_zero β] {s : set α} (hs : measurable_set s) (f : β) :
theorem measure_theory.simple_func.range_indicator {α : Type u_1} {β : Type u_2} {s : set α} (hs : measurable_set s) (hs_nonempty : s.nonempty) (hs_ne_univ : s set.univ) (x y : β) :
= {x, y}
theorem measure_theory.simple_func.measurable_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β) (g : β α γ) (hg : (b : β), measurable (g b)) :
measurable (λ (a : α), g (f a) a)
def measure_theory.simple_func.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
@[simp]
theorem measure_theory.simple_func.bind_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β) (g : β ) (a : α) :
(f.bind g) a = (g (f a)) a
def measure_theory.simple_func.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
theorem measure_theory.simple_func.map_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β γ) (f : β) (a : α) :
= g (f a)
theorem measure_theory.simple_func.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (g : β γ) (h : γ δ) (f : β) :
@[simp]
theorem measure_theory.simple_func.coe_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β γ) (f : β) :
= g f
@[simp]
theorem measure_theory.simple_func.range_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq γ] (g : β γ) (f : β) :
@[simp]
theorem measure_theory.simple_func.map_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β γ) (b : β) :
theorem measure_theory.simple_func.map_preimage {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β) (g : β γ) (s : set γ) :
= f ⁻¹' (finset.filter (λ (b : β), g b s) f.range)
theorem measure_theory.simple_func.map_preimage_singleton {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β) (g : β γ) (c : γ) :
⁻¹' {c} = f ⁻¹' (finset.filter (λ (b : β), g b = c) f.range)
def measure_theory.simple_func.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : γ) (g : α β) (hgm : measurable g) :

Composition of a `simple_fun` and a measurable function is a `simple_func`.

Equations
@[simp]
theorem measure_theory.simple_func.coe_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : γ) {g : α β} (hgm : measurable g) :
(f.comp g hgm) = f g
theorem measure_theory.simple_func.range_comp_subset_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : γ) {g : α β} (hgm : measurable g) :
(f.comp g hgm).range f.range
noncomputable def measure_theory.simple_func.extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f₁ : γ) (g : α β) (hg : measurable_embedding g) (f₂ : γ) :

Extend a `simple_func` 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
@[simp]
theorem measure_theory.simple_func.extend_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f₁ : γ) {g : α β} (hg : measurable_embedding g) (f₂ : γ) (x : α) :
(f₁.extend g hg f₂) (g x) = f₁ x
@[simp]
theorem measure_theory.simple_func.extend_apply' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f₁ : γ) {g : α β} (hg : measurable_embedding g) (f₂ : γ) {y : β} (h : ¬ (x : α), g x = y) :
(f₁.extend g hg f₂) y = f₂ y
@[simp]
theorem measure_theory.simple_func.extend_comp_eq' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f₁ : γ) {g : α β} (hg : measurable_embedding g) (f₂ : γ) :
(f₁.extend g hg f₂) g = f₁
@[simp]
theorem measure_theory.simple_func.extend_comp_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f₁ : γ) {g : α β} (hg : measurable_embedding g) (f₂ : γ) :
(f₁.extend g hg f₂).comp g _ = f₁
def measure_theory.simple_func.seq {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : γ)) (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
@[simp]
theorem measure_theory.simple_func.seq_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : γ)) (g : β) (a : α) :
(f.seq g) a = f a (g a)
def measure_theory.simple_func.pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β) (g : γ) :
× γ)

Combine two simple functions `f : α →ₛ β` and `g : α →ₛ β` into `λ a, (f a, g a)`.

Equations
@[simp]
theorem measure_theory.simple_func.pair_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β) (g : γ) (a : α) :
(f.pair g) a = (f a, g a)
theorem measure_theory.simple_func.pair_preimage {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β) (g : γ) (s : set β) (t : set γ) :
theorem measure_theory.simple_func.pair_preimage_singleton {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β) (g : γ) (b : β) (c : γ) :
(f.pair g) ⁻¹' {(b, c)} = f ⁻¹' {b} g ⁻¹' {c}
theorem measure_theory.simple_func.bind_const {α : Type u_1} {β : Type u_2} (f : β) :
@[protected, instance]
def measure_theory.simple_func.has_zero {α : Type u_1} {β : Type u_2} [has_zero β] :
Equations
@[protected, instance]
def measure_theory.simple_func.has_one {α : Type u_1} {β : Type u_2} [has_one β] :
Equations
@[protected, instance]
def measure_theory.simple_func.has_add {α : Type u_1} {β : Type u_2} [has_add β] :
Equations
@[protected, instance]
def measure_theory.simple_func.has_mul {α : Type u_1} {β : Type u_2} [has_mul β] :
Equations
@[protected, instance]
def measure_theory.simple_func.has_div {α : Type u_1} {β : Type u_2} [has_div β] :
Equations
@[protected, instance]
def measure_theory.simple_func.has_sub {α : Type u_1} {β : Type u_2} [has_sub β] :
Equations
@[protected, instance]
def measure_theory.simple_func.has_inv {α : Type u_1} {β : Type u_2} [has_inv β] :
Equations
@[protected, instance]
def measure_theory.simple_func.has_neg {α : Type u_1} {β : Type u_2} [has_neg β] :
Equations
@[protected, instance]
def measure_theory.simple_func.has_sup {α : Type u_1} {β : Type u_2} [has_sup β] :
Equations
@[protected, instance]
def measure_theory.simple_func.has_inf {α : Type u_1} {β : Type u_2} [has_inf β] :
Equations
@[protected, instance]
def measure_theory.simple_func.has_le {α : Type u_1} {β : Type u_2} [has_le β] :
Equations
@[simp]
theorem measure_theory.simple_func.const_one {α : Type u_1} {β : Type u_2} [has_one β] :
@[simp]
theorem measure_theory.simple_func.const_zero {α : Type u_1} {β : Type u_2} [has_zero β] :
@[simp, norm_cast]
theorem measure_theory.simple_func.coe_one {α : Type u_1} {β : Type u_2} [has_one β] :
1 = 1
@[simp, norm_cast]
theorem measure_theory.simple_func.coe_zero {α : Type u_1} {β : Type u_2} [has_zero β] :
0 = 0
@[simp, norm_cast]
theorem measure_theory.simple_func.coe_mul {α : Type u_1} {β : Type u_2} [has_mul β] (f g : β) :
(f * g) = f * g
@[simp, norm_cast]
theorem measure_theory.simple_func.coe_add {α : Type u_1} {β : Type u_2} [has_add β] (f g : β) :
(f + g) = f + g
@[simp, norm_cast]
theorem measure_theory.simple_func.coe_inv {α : Type u_1} {β : Type u_2} [has_inv β] (f : β) :
@[simp, norm_cast]
theorem measure_theory.simple_func.coe_neg {α : Type u_1} {β : Type u_2} [has_neg β] (f : β) :
@[simp, norm_cast]
theorem measure_theory.simple_func.coe_div {α : Type u_1} {β : Type u_2} [has_div β] (f g : β) :
(f / g) = f / g
@[simp, norm_cast]
theorem measure_theory.simple_func.coe_sub {α : Type u_1} {β : Type u_2} [has_sub β] (f g : β) :
(f - g) = f - g
@[simp, norm_cast]
theorem measure_theory.simple_func.coe_le {α : Type u_1} {β : Type u_2} [preorder β] {f g : β} :
f g f g
@[simp, norm_cast]
theorem measure_theory.simple_func.coe_sup {α : Type u_1} {β : Type u_2} [has_sup β] (f g : β) :
(f g) = f g
@[simp, norm_cast]
theorem measure_theory.simple_func.coe_inf {α : Type u_1} {β : Type u_2} [has_inf β] (f g : β) :
(f g) = f g
theorem measure_theory.simple_func.add_apply {α : Type u_1} {β : Type u_2} [has_add β] (f g : β) (a : α) :
(f + g) a = f a + g a
theorem measure_theory.simple_func.mul_apply {α : Type u_1} {β : Type u_2} [has_mul β] (f g : β) (a : α) :
(f * g) a = f a * g a
theorem measure_theory.simple_func.div_apply {α : Type u_1} {β : Type u_2} [has_div β] (f g : β) (x : α) :
(f / g) x = f x / g x
theorem measure_theory.simple_func.sub_apply {α : Type u_1} {β : Type u_2} [has_sub β] (f g : β) (x : α) :
(f - g) x = f x - g x
theorem measure_theory.simple_func.neg_apply {α : Type u_1} {β : Type u_2} [has_neg β] (f : β) (x : α) :
(-f) x = -f x
theorem measure_theory.simple_func.inv_apply {α : Type u_1} {β : Type u_2} [has_inv β] (f : β) (x : α) :
theorem measure_theory.simple_func.sup_apply {α : Type u_1} {β : Type u_2} [has_sup β] (f g : β) (a : α) :
(f g) a = f a g a
theorem measure_theory.simple_func.inf_apply {α : Type u_1} {β : Type u_2} [has_inf β] (f g : β) (a : α) :
(f g) a = f a g a
@[simp]
theorem measure_theory.simple_func.range_one {α : Type u_1} {β : Type u_2} [nonempty α] [has_one β] :
1.range = {1}
@[simp]
theorem measure_theory.simple_func.range_zero {α : Type u_1} {β : Type u_2} [nonempty α] [has_zero β] :
0.range = {0}
@[simp]
theorem measure_theory.simple_func.range_eq_empty_of_is_empty {α : Type u_1} {β : Type u_2} [hα : is_empty α] (f : β) :
theorem measure_theory.simple_func.eq_zero_of_mem_range_zero {α : Type u_1} {β : Type u_2} [has_zero β] {y : β} :
y 0.range y = 0
theorem measure_theory.simple_func.add_eq_map₂ {α : Type u_1} {β : Type u_2} [has_add β] (f g : β) :
f + g = measure_theory.simple_func.map (λ (p : β × β), p.fst + p.snd) (f.pair g)
theorem measure_theory.simple_func.mul_eq_map₂ {α : Type u_1} {β : Type u_2} [has_mul β] (f g : β) :
f * g = measure_theory.simple_func.map (λ (p : β × β), p.fst * p.snd) (f.pair g)
theorem measure_theory.simple_func.sup_eq_map₂ {α : Type u_1} {β : Type u_2} [has_sup β] (f g : β) :
f g = measure_theory.simple_func.map (λ (p : β × β), p.fst p.snd) (f.pair g)
theorem measure_theory.simple_func.const_mul_eq_map {α : Type u_1} {β : Type u_2} [has_mul β] (f : β) (b : β) :
= measure_theory.simple_func.map (λ (a : β), b * a) f
theorem measure_theory.simple_func.const_add_eq_map {α : Type u_1} {β : Type u_2} [has_add β] (f : β) (b : β) :
= measure_theory.simple_func.map (λ (a : β), b + a) f
theorem measure_theory.simple_func.map_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_add β] [has_add γ] {g : β γ} (hg : (x y : β), g (x + y) = g x + g y) (f₁ f₂ : β) :
theorem measure_theory.simple_func.map_mul {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_mul β] [has_mul γ] {g : β γ} (hg : (x y : β), g (x * y) = g x * g y) (f₁ f₂ : β) :
@[protected, instance]
def measure_theory.simple_func.has_smul {α : Type u_1} {β : Type u_2} {K : Type u_5} [ β] :
Equations
@[simp]
theorem measure_theory.simple_func.coe_smul {α : Type u_1} {β : Type u_2} {K : Type u_5} [ β] (c : K) (f : β) :
(c f) = c f
theorem measure_theory.simple_func.smul_apply {α : Type u_1} {β : Type u_2} {K : Type u_5} [ β] (k : K) (f : β) (a : α) :
(k f) a = k f a
@[protected, instance]
def measure_theory.simple_func.has_nat_pow {α : Type u_1} {β : Type u_2} [monoid β] :
Equations
@[simp]
theorem measure_theory.simple_func.coe_pow {α : Type u_1} {β : Type u_2} [monoid β] (f : β) (n : ) :
(f ^ n) = f ^ n
theorem measure_theory.simple_func.pow_apply {α : Type u_1} {β : Type u_2} [monoid β] (n : ) (f : β) (a : α) :
(f ^ n) a = f a ^ n
@[protected, instance]
def measure_theory.simple_func.has_int_pow {α : Type u_1} {β : Type u_2}  :
Equations
@[simp]
theorem measure_theory.simple_func.coe_zpow {α : Type u_1} {β : Type u_2} (f : β) (z : ) :
(f ^ z) = f ^ z
theorem measure_theory.simple_func.zpow_apply {α : Type u_1} {β : Type u_2} (z : ) (f : β) (a : α) :
(f ^ z) a = f a ^ z
@[protected, instance]
def measure_theory.simple_func.add_monoid {α : Type u_1} {β : Type u_2} [add_monoid β] :
Equations
@[protected, instance]
def measure_theory.simple_func.add_comm_monoid {α : Type u_1} {β : Type u_2}  :
Equations
@[protected, instance]
def measure_theory.simple_func.add_group {α : Type u_1} {β : Type u_2} [add_group β] :
Equations
@[protected, instance]
def measure_theory.simple_func.add_comm_group {α : Type u_1} {β : Type u_2}  :
Equations
@[protected, instance]
def measure_theory.simple_func.monoid {α : Type u_1} {β : Type u_2} [monoid β] :
Equations
@[protected, instance]
def measure_theory.simple_func.comm_monoid {α : Type u_1} {β : Type u_2} [comm_monoid β] :
Equations
@[protected, instance]
def measure_theory.simple_func.group {α : Type u_1} {β : Type u_2} [group β] :
Equations
@[protected, instance]
def measure_theory.simple_func.comm_group {α : Type u_1} {β : Type u_2} [comm_group β] :
Equations
@[protected, instance]
def measure_theory.simple_func.module {α : Type u_1} {β : Type u_2} {K : Type u_5} [semiring K] [ β] :
Equations
theorem measure_theory.simple_func.smul_eq_map {α : Type u_1} {β : Type u_2} {K : Type u_5} [ β] (k : K) (f : β) :
@[protected, instance]
def measure_theory.simple_func.preorder {α : Type u_1} {β : Type u_2} [preorder β] :
Equations
@[protected, instance]
def measure_theory.simple_func.partial_order {α : Type u_1} {β : Type u_2}  :
Equations
@[protected, instance]
def measure_theory.simple_func.order_bot {α : Type u_1} {β : Type u_2} [has_le β] [order_bot β] :
Equations
@[protected, instance]
def measure_theory.simple_func.order_top {α : Type u_1} {β : Type u_2} [has_le β] [order_top β] :
Equations
@[protected, instance]
def measure_theory.simple_func.semilattice_inf {α : Type u_1} {β : Type u_2}  :
Equations
@[protected, instance]
def measure_theory.simple_func.semilattice_sup {α : Type u_1} {β : Type u_2}  :
Equations
@[protected, instance]
def measure_theory.simple_func.lattice {α : Type u_1} {β : Type u_2} [lattice β] :
Equations
@[protected, instance]
def measure_theory.simple_func.bounded_order {α : Type u_1} {β : Type u_2} [has_le β]  :
Equations
theorem measure_theory.simple_func.finset_sup_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [order_bot β] {f : γ } (s : finset γ) (a : α) :
(s.sup f) a = s.sup (λ (c : γ), (f c) a)
noncomputable def measure_theory.simple_func.restrict {α : Type u_1} {β : Type u_2} [has_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
• f.restrict s = (λ (hs : , 0) (λ (hs : , 0)
theorem measure_theory.simple_func.restrict_of_not_measurable {α : Type u_1} {β : Type u_2} [has_zero β] {f : β} {s : set α} (hs : ¬) :
f.restrict s = 0
@[simp]
theorem measure_theory.simple_func.coe_restrict {α : Type u_1} {β : Type u_2} [has_zero β] (f : β) {s : set α} (hs : measurable_set s) :
@[simp]
theorem measure_theory.simple_func.restrict_univ {α : Type u_1} {β : Type u_2} [has_zero β] (f : β) :
@[simp]
theorem measure_theory.simple_func.restrict_empty {α : Type u_1} {β : Type u_2} [has_zero β] (f : β) :
= 0
theorem measure_theory.simple_func.map_restrict_of_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero β] [has_zero γ] {g : β γ} (hg : g 0 = 0) (f : β) (s : set α) :
theorem measure_theory.simple_func.restrict_apply {α : Type u_1} {β : Type u_2} [has_zero β] (f : β) {s : set α} (hs : measurable_set s) (a : α) :
(f.restrict s) a = s.indicator f a
theorem measure_theory.simple_func.restrict_preimage {α : Type u_1} {β : Type u_2} [has_zero β] (f : β) {s : set α} (hs : measurable_set s) {t : set β} (ht : 0 t) :
theorem measure_theory.simple_func.restrict_preimage_singleton {α : Type u_1} {β : Type u_2} [has_zero β] (f : β) {s : set α} (hs : measurable_set s) {r : β} (hr : r 0) :
(f.restrict s) ⁻¹' {r} = s f ⁻¹' {r}
theorem measure_theory.simple_func.mem_restrict_range {α : Type u_1} {β : Type u_2} [has_zero β] {r : β} {s : set α} {f : β} (hs : measurable_set s) :
r (f.restrict s).range r = 0 r f '' s
theorem measure_theory.simple_func.mem_image_of_mem_range_restrict {α : Type u_1} {β : Type u_2} [has_zero β] {r : β} {s : set α} {f : β} (hr : r (f.restrict s).range) (h0 : r 0) :
r f '' s
theorem measure_theory.simple_func.restrict_mono {α : Type u_1} {β : Type u_2} [has_zero β] [preorder β] (s : set α) {f g : β} (H : f g) :
noncomputable def measure_theory.simple_func.approx {α : Type u_1} {β : Type u_2} [order_bot β] [has_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 `supr_approx_apply` for details.

Equations
theorem measure_theory.simple_func.approx_apply {α : Type u_1} {β : Type u_2} [order_bot β] [has_zero β] {i : β} {f : α β} {n : } (a : α) (hf : measurable f) :
a = (finset.range n).sup (λ (k : ), ite (i k f a) (i k) 0)
theorem measure_theory.simple_func.monotone_approx {α : Type u_1} {β : Type u_2} [order_bot β] [has_zero β] (i : β) (f : α β) :
theorem measure_theory.simple_func.approx_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [order_bot β] [has_zero β] {i : β} {f : γ β} {g : α γ} {n : } (a : α) (hf : measurable f) (hg : measurable g) :
(f g) n) a = (g a)
theorem measure_theory.simple_func.supr_approx_apply {α : Type u_1} {β : Type u_2} [has_zero β] (i : β) (f : α β) (a : α) (hf : measurable f) (h_zero : 0 = ) :
( (n : ), a) = (k : ) (h : i k f a), i k

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

Equations
noncomputable def measure_theory.simple_func.eapprox {α : Type u_1}  :

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

Equations
theorem measure_theory.simple_func.eapprox_lt_top {α : Type u_1} (f : α ennreal) (n : ) (a : α) :
theorem measure_theory.simple_func.supr_eapprox_apply {α : Type u_1} (f : α ennreal) (hf : measurable f) (a : α) :
( (n : ), = f a
theorem measure_theory.simple_func.eapprox_comp {α : Type u_1} {γ : Type u_3} {f : γ ennreal} {g : α γ} {n : } (hf : measurable f) (hg : measurable g) :
n) =
noncomputable def measure_theory.simple_func.eapprox_diff {α : Type u_1} (f : α ennreal) (n : ) :

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

Equations
theorem measure_theory.simple_func.sum_eapprox_diff {α : Type u_1} (f : α ennreal) (n : ) (a : α) :
(finset.range (n + 1)).sum (λ (k : ), a)) =
theorem measure_theory.simple_func.tsum_eapprox_diff {α : Type u_1} (f : α ennreal) (hf : measurable f) (a : α) :
∑' (n : ), = f a
noncomputable def measure_theory.simple_func.lintegral {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) :

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

Equations
theorem measure_theory.simple_func.lintegral_eq_of_subset {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {s : finset ennreal} (hs : (x : α), f x 0 μ (f ⁻¹' {f x}) 0 f x s) :
f.lintegral μ = s.sum (λ (x : ennreal), x * μ (f ⁻¹' {x}))
theorem measure_theory.simple_func.lintegral_eq_of_subset' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {s : finset ennreal} (hs : f.range \ {0} s) :
f.lintegral μ = s.sum (λ (x : ennreal), x * μ (f ⁻¹' {x}))
theorem measure_theory.simple_func.map_lintegral {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} (g : β ennreal) (f : β) :
= f.range.sum (λ (x : β), g x * μ (f ⁻¹' {x}))

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

noncomputable def measure_theory.simple_func.lintegralₗ {α : Type u_1} {m : measurable_space α} :

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

Equations
@[simp]
theorem measure_theory.simple_func.lintegral_sum {α : Type u_1} {m : measurable_space α} {ι : Type u_2} (μ : ι ) :
= ∑' (i : ι), f.lintegral (μ i)
theorem measure_theory.simple_func.restrict_lintegral {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hs : measurable_set s) :
(f.restrict s).lintegral μ = f.range.sum (λ (r : ennreal), r * μ (f ⁻¹' {r} s))
theorem measure_theory.simple_func.lintegral_restrict {α : Type u_1} {m : measurable_space α} (s : set α) (μ : measure_theory.measure α) :
f.lintegral (μ.restrict s) = f.range.sum (λ (y : ennreal), y * μ (f ⁻¹' {y} s))
theorem measure_theory.simple_func.restrict_const_lintegral {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (c : ennreal) {s : set α} (hs : measurable_set s) :
μ = c * μ s
theorem measure_theory.simple_func.lintegral_mono {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} {f g : ennreal} (hfg : f g) (hμν : μ ν) :

`simple_func.lintegral` is monotone both in function and in measure.

theorem measure_theory.simple_func.lintegral_eq_of_measure_preimage {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {ν : measure_theory.measure β} (H : (y : ennreal), μ (f ⁻¹' {y}) = ν (g ⁻¹' {y})) :

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

If two simple functions are equal a.e., then their `lintegral`s are equal.

theorem measure_theory.simple_func.lintegral_map' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} {μ' : measure_theory.measure β} (m' : α β) (eq : (a : α), f a = g (m' a)) (h : (s : set β), μ' s = μ (m' ⁻¹' s)) :
f.lintegral μ = g.lintegral μ'
theorem measure_theory.simple_func.lintegral_map {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} {f : α β} (hf : measurable f) :
= (g.comp f hf).lintegral μ
theorem measure_theory.simple_func.support_eq {α : Type u_1} {β : Type u_2} [has_zero β] (f : β) :
= (y : β) (H : y finset.filter (λ (y : β), y 0) f.range), f ⁻¹' {y}
theorem measure_theory.simple_func.measurable_set_support {α : Type u_1} {β : Type u_2} [has_zero β] (f : β) :
@[protected]
def measure_theory.simple_func.fin_meas_supp {α : Type u_1} {β : Type u_2} [has_zero β] {m : measurable_space α} (f : β) (μ : measure_theory.measure α) :
Prop

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

Equations
theorem measure_theory.simple_func.fin_meas_supp_iff {α : Type u_1} {β : Type u_2} {m : measurable_space α} [has_zero β] {μ : measure_theory.measure α} {f : β} :
(y : β), y 0 μ (f ⁻¹' {y}) <
theorem measure_theory.simple_func.fin_meas_supp.meas_preimage_singleton_ne_zero {α : Type u_1} {β : Type u_2} {m : measurable_space α} [has_zero β] {μ : measure_theory.measure α} {f : β} (h : f.fin_meas_supp μ) {y : β} (hy : y 0) :
μ (f ⁻¹' {y}) <
@[protected]
theorem measure_theory.simple_func.fin_meas_supp.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} [has_zero β] [has_zero γ] {μ : measure_theory.measure α} {f : β} {g : β γ} (hf : f.fin_meas_supp μ) (hg : g 0 = 0) :
theorem measure_theory.simple_func.fin_meas_supp.of_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} [has_zero β] [has_zero γ] {μ : measure_theory.measure α} {f : β} {g : β γ} (h : μ) (hg : (b : β), g b = 0 b = 0) :
theorem measure_theory.simple_func.fin_meas_supp.map_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} [has_zero β] [has_zero γ] {μ : measure_theory.measure α} {f : β} {g : β γ} (hg : {b : β}, g b = 0 b = 0) :
@[protected]
theorem measure_theory.simple_func.fin_meas_supp.pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} [has_zero β] [has_zero γ] {μ : measure_theory.measure α} {f : β} {g : γ} (hf : f.fin_meas_supp μ) (hg : g.fin_meas_supp μ) :
@[protected]
theorem measure_theory.simple_func.fin_meas_supp.map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m : measurable_space α} [has_zero β] [has_zero γ] {μ : measure_theory.measure α} {f : β} [has_zero δ] (hf : f.fin_meas_supp μ) {g : γ} (hg : g.fin_meas_supp μ) {op : β γ δ} (H : op 0 0 = 0) :
(f.pair g)).fin_meas_supp μ
@[protected]
theorem measure_theory.simple_func.fin_meas_supp.add {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} [add_monoid β] {f g : β} (hf : f.fin_meas_supp μ) (hg : g.fin_meas_supp μ) :
(f + g).fin_meas_supp μ
@[protected]
theorem measure_theory.simple_func.fin_meas_supp.mul {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} {f g : β} (hf : f.fin_meas_supp μ) (hg : g.fin_meas_supp μ) :
(f * g).fin_meas_supp μ
@[protected]
theorem measure_theory.simple_func.induction {α : Type u_1} {γ : Type u_2} [add_monoid γ] {P : Prop} (h_ind : (c : γ) {s : set α} (hs : , ) (h_add : ⦃f g : ⦄, P f P g P (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.ennreal_induction {α : Type u_1} {P : ennreal) Prop} (h_ind : (c : ennreal) ⦃s : set α⦄, P (s.indicator (λ (_x : α), c))) (h_add : ⦃f g : ⦄, P f P g P (f + g)) (h_supr : ⦃f : ⦄, ( (n : ), measurable (f n)) ( (n : ), P (f n)) P (λ (x : α), (n : ), f n x)) ⦃f : α ennreal (hf : measurable f) :
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}`.