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) [MeasurableSpace α] (β : 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.

• toFun : α → β

  The underlying function

• measurableSet_fiber' (x : β) : MeasurableSet (self.toFun ⁻¹' {x})
• finite_range' : (Set.range self.toFun).Finite

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instFunLike {α : Type u_1} {β : Type u_2} [MeasurableSpace α] : FunLike (SimpleFunc α β) α β

theorem MeasureTheory.SimpleFunc.coe_injective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] ⦃f g : SimpleFunc α β⦄ (H : ⇑f = ⇑g) : f = g

theorem MeasureTheory.SimpleFunc.ext {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {f g : SimpleFunc α β} (H : ∀ (a : α), f a = g a) : f = g

theorem MeasureTheory.SimpleFunc.ext_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {f g : SimpleFunc α β} : f = g ↔ ∀ (a : α), f a = g a

theorem MeasureTheory.SimpleFunc.finite_range {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (f : SimpleFunc α β) : (Set.range ⇑f).Finite

theorem MeasureTheory.SimpleFunc.measurableSet_fiber {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (f : SimpleFunc α β) (x : β) : MeasurableSet (⇑f ⁻¹' {x})

@[simp]

theorem MeasureTheory.SimpleFunc.coe_mk {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (f : α → β) (h : ∀ (x : β), MeasurableSet (f ⁻¹' {x})) (h' : (Set.range f).Finite) : ⇑{ toFun := f, measurableSet_fiber' := h, finite_range' := h' } = f

theorem MeasureTheory.SimpleFunc.apply_mk {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (f : α → β) (h : ∀ (x : β), MeasurableSet (f ⁻¹' {x})) (h' : (Set.range f).Finite) (x : α) : { toFun := f, measurableSet_fiber' := h, finite_range' := h' } x = f x

def MeasureTheory.SimpleFunc.ofFinite {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Finite α] [MeasurableSingletonClass α] (f : α → β) : SimpleFunc α β

Simple function defined on a finite type.

def MeasureTheory.SimpleFunc.ofIsEmpty {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [IsEmpty α] : SimpleFunc α β

Simple function defined on the empty type.

noncomputable def MeasureTheory.SimpleFunc.range {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (f : SimpleFunc α β) : Finset β

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

@[simp]

theorem MeasureTheory.SimpleFunc.mem_range {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {f : SimpleFunc α β} {b : β} : b ∈ f.range ↔ b ∈ Set.range ⇑f

theorem MeasureTheory.SimpleFunc.mem_range_self {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (f : SimpleFunc α β) (x : α) : f x ∈ f.range

@[simp]

theorem MeasureTheory.SimpleFunc.coe_range {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (f : SimpleFunc α β) : ↑f.range = Set.range ⇑f

theorem MeasureTheory.SimpleFunc.mem_range_of_measure_ne_zero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {f : SimpleFunc α β} {x : β} {μ : Measure α} (H : μ (⇑f ⁻¹' {x}) ≠ 0) : x ∈ f.range

theorem MeasureTheory.SimpleFunc.forall_mem_range {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {f : SimpleFunc α β} {p : β → Prop} : (∀ y ∈ f.range, p y) ↔ ∀ (x : α), p (f x)

theorem MeasureTheory.SimpleFunc.exists_range_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {f : SimpleFunc α β} {p : β → Prop} : (∃ y ∈ f.range, p y) ↔ ∃ (x : α), p (f x)

theorem MeasureTheory.SimpleFunc.preimage_eq_empty_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (f : SimpleFunc α β) (b : β) : ⇑f ⁻¹' {b} = ∅ ↔ b ∉ f.range

theorem MeasureTheory.SimpleFunc.exists_forall_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Nonempty β] [Preorder β] [IsDirectedOrder β] (f : SimpleFunc α β) : ∃ (C : β), ∀ (x : α), f x ≤ C

def MeasureTheory.SimpleFunc.const (α : Type u_5) {β : Type u_6} [MeasurableSpace α] (b : β) : SimpleFunc α β

Constant function as a SimpleFunc.

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instInhabited {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Inhabited β] : Inhabited (SimpleFunc α β)

theorem MeasureTheory.SimpleFunc.const_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (a : α) (b : β) : (const α b) a = b

@[simp]

theorem MeasureTheory.SimpleFunc.coe_const {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (b : β) : ⇑(const α b) = Function.const α b

@[simp]

theorem MeasureTheory.SimpleFunc.range_const {β : Type u_2} (α : Type u_5) [MeasurableSpace α] [Nonempty α] (b : β) : (const α b).range = {b}

theorem MeasureTheory.SimpleFunc.range_const_subset {β : Type u_2} (α : Type u_5) [MeasurableSpace α] (b : β) : (const α b).range ⊆ {b}

theorem MeasureTheory.SimpleFunc.simpleFunc_bot {β : Type u_2} {α : Type u_5} (f : SimpleFunc α β) [Nonempty β] : ∃ (c : β), ∀ (x : α), f x = c

theorem MeasureTheory.SimpleFunc.simpleFunc_bot' {β : Type u_2} {α : Type u_5} [Nonempty β] (f : SimpleFunc α β) : ∃ (c : β), f = const α c

theorem MeasureTheory.SimpleFunc.measurableSet_cut {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (r : α → β → Prop) (f : SimpleFunc α β) (h : ∀ (b : β), MeasurableSet {a : α | r a b}) : MeasurableSet {a : α | r a (f a)}

theorem MeasureTheory.SimpleFunc.measurableSet_preimage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (f : SimpleFunc α β) (s : Set β) : MeasurableSet (⇑f ⁻¹' s)

theorem MeasureTheory.SimpleFunc.measurable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : SimpleFunc α β) : Measurable ⇑f

A simple function is measurable

theorem MeasureTheory.SimpleFunc.aemeasurable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} (f : SimpleFunc α β) : AEMeasurable (⇑f) μ

theorem MeasureTheory.SimpleFunc.sum_measure_preimage_singleton {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (f : SimpleFunc α β) {μ : Measure α} (s : Finset β) : ∑ y ∈ s, μ (⇑f ⁻¹' {y}) = μ (⇑f ⁻¹' ↑s)

theorem MeasureTheory.SimpleFunc.sum_range_measure_preimage_singleton {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (f : SimpleFunc α β) (μ : Measure α) : ∑ y ∈ f.range, μ (⇑f ⁻¹' {y}) = μ Set.univ

noncomputable def MeasureTheory.SimpleFunc.piecewise {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (s : Set α) (hs : MeasurableSet s) (f g : SimpleFunc α β) : SimpleFunc α β

If-then-else as a SimpleFunc.

@[simp]

theorem MeasureTheory.SimpleFunc.coe_piecewise {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {s : Set α} (hs : MeasurableSet s) (f g : SimpleFunc α β) : ⇑(piecewise s hs f g) = s.piecewise ⇑f ⇑g

theorem MeasureTheory.SimpleFunc.piecewise_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {s : Set α} (hs : MeasurableSet s) (f g : SimpleFunc α β) (a : α) : (piecewise s hs f g) a = if a ∈ s then f a else g a

@[simp]

theorem MeasureTheory.SimpleFunc.piecewise_compl {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {s : Set α} (hs : MeasurableSet sᶜ) (f g : SimpleFunc α β) : piecewise sᶜ hs f g = piecewise s ⋯ g f

@[simp]

theorem MeasureTheory.SimpleFunc.piecewise_univ {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (f g : SimpleFunc α β) : piecewise Set.univ ⋯ f g = f

@[simp]

theorem MeasureTheory.SimpleFunc.piecewise_empty {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (f g : SimpleFunc α β) : piecewise ∅ ⋯ f g = g

@[simp]

theorem MeasureTheory.SimpleFunc.piecewise_same {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (f : SimpleFunc α β) {s : Set α} (hs : MeasurableSet s) : piecewise s hs f f = f

theorem MeasureTheory.SimpleFunc.support_indicator {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Zero β] {s : Set α} (hs : MeasurableSet s) (f : SimpleFunc α β) : Function.support ⇑(piecewise s hs f (const α 0)) = s ∩ Function.support ⇑f

theorem MeasureTheory.SimpleFunc.range_indicator {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {s : Set α} (hs : MeasurableSet s) (hs_nonempty : s.Nonempty) (hs_ne_univ : s ≠ Set.univ) (x y : β) : (piecewise s hs (const α x) (const α y)).range = {x, y}

theorem MeasureTheory.SimpleFunc.measurable_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace γ] (f : SimpleFunc α β) (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} [MeasurableSpace α] (f : SimpleFunc α β) (g : β → SimpleFunc α γ) : SimpleFunc α γ

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.

@[simp]

theorem MeasureTheory.SimpleFunc.bind_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (f : SimpleFunc α β) (g : β → SimpleFunc α γ) (a : α) : (f.bind g) a = (g (f a)) a

def MeasureTheory.SimpleFunc.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (g : β → γ) (f : SimpleFunc α β) : SimpleFunc α γ

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

theorem MeasureTheory.SimpleFunc.map_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (g : β → γ) (f : SimpleFunc α β) (a : α) : (map g f) a = g (f a)

theorem MeasureTheory.SimpleFunc.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] (g : β → γ) (h : γ → δ) (f : SimpleFunc α β) : map h (map g f) = map (h ∘ g) f

@[simp]

theorem MeasureTheory.SimpleFunc.coe_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (g : β → γ) (f : SimpleFunc α β) : ⇑(map g f) = g ∘ ⇑f

@[simp]

theorem MeasureTheory.SimpleFunc.range_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [DecidableEq γ] (g : β → γ) (f : SimpleFunc α β) : (map g f).range = Finset.image g f.range

@[simp]

theorem MeasureTheory.SimpleFunc.map_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (g : β → γ) (b : β) : map g (const α b) = const α (g b)

theorem MeasureTheory.SimpleFunc.map_preimage {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (f : SimpleFunc α β) (g : β → γ) (s : Set γ) : ⇑(map g f) ⁻¹' s = ⇑f ⁻¹' ↑({b ∈ f.range | g b ∈ s})

theorem MeasureTheory.SimpleFunc.map_preimage_singleton {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (f : SimpleFunc α β) (g : β → γ) (c : γ) : ⇑(map g f) ⁻¹' {c} = ⇑f ⁻¹' ↑({b ∈ f.range | g b = c})

def MeasureTheory.SimpleFunc.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (f : SimpleFunc β γ) (g : α → β) (hgm : Measurable g) : SimpleFunc α γ

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

@[simp]

theorem MeasureTheory.SimpleFunc.coe_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (f : SimpleFunc β γ) {g : α → β} (hgm : Measurable g) : ⇑(f.comp g hgm) = ⇑f ∘ g

theorem MeasureTheory.SimpleFunc.range_comp_subset_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (f : SimpleFunc β γ) {g : α → β} (hgm : Measurable g) : (f.comp g hgm).range ⊆ f.range

noncomputable def MeasureTheory.SimpleFunc.extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (f₁ : SimpleFunc α γ) (g : α → β) (hg : MeasurableEmbedding g) (f₂ : SimpleFunc β γ) : SimpleFunc β γ

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.

@[simp]

theorem MeasureTheory.SimpleFunc.extend_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (f₁ : SimpleFunc α γ) {g : α → β} (hg : MeasurableEmbedding g) (f₂ : SimpleFunc β γ) (x : α) : (f₁.extend g hg f₂) (g x) = f₁ x

@[simp]

theorem MeasureTheory.SimpleFunc.extend_apply' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (f₁ : SimpleFunc α γ) {g : α → β} (hg : MeasurableEmbedding g) (f₂ : SimpleFunc β γ) {y : β} (h : ¬∃ (x : α), g x = y) : (f₁.extend g hg f₂) y = f₂ y

@[simp]

theorem MeasureTheory.SimpleFunc.extend_comp_eq' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (f₁ : SimpleFunc α γ) {g : α → β} (hg : MeasurableEmbedding g) (f₂ : SimpleFunc β γ) : ⇑(f₁.extend g hg f₂) ∘ g = ⇑f₁

@[simp]

theorem MeasureTheory.SimpleFunc.extend_comp_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (f₁ : SimpleFunc α γ) {g : α → β} (hg : MeasurableEmbedding g) (f₂ : SimpleFunc β γ) : (f₁.extend g hg f₂).comp g ⋯ = f₁

def MeasureTheory.SimpleFunc.seq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (f : SimpleFunc α (β → γ)) (g : SimpleFunc α β) : SimpleFunc α γ

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).

@[simp]

theorem MeasureTheory.SimpleFunc.seq_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (f : SimpleFunc α (β → γ)) (g : SimpleFunc α β) (a : α) : (f.seq g) a = f a (g a)

def MeasureTheory.SimpleFunc.pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (f : SimpleFunc α β) (g : SimpleFunc α γ) : SimpleFunc α (β × γ)

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

@[simp]

theorem MeasureTheory.SimpleFunc.pair_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (f : SimpleFunc α β) (g : SimpleFunc α γ) (a : α) : (f.pair g) a = (f a, g a)

theorem MeasureTheory.SimpleFunc.pair_preimage {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (f : SimpleFunc α β) (g : SimpleFunc α γ) (s : Set β) (t : Set γ) : ⇑(f.pair g) ⁻¹' s ×ˢ t = ⇑f ⁻¹' s ∩ ⇑g ⁻¹' t

theorem MeasureTheory.SimpleFunc.pair_preimage_singleton {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (f : SimpleFunc α β) (g : SimpleFunc α γ) (b : β) (c : γ) : ⇑(f.pair g) ⁻¹' {(b, c)} = ⇑f ⁻¹' {b} ∩ ⇑g ⁻¹' {c}

@[simp]

theorem MeasureTheory.SimpleFunc.map_fst_pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (f : SimpleFunc α β) (g : SimpleFunc α γ) : map Prod.fst (f.pair g) = f

@[simp]

theorem MeasureTheory.SimpleFunc.map_snd_pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (f : SimpleFunc α β) (g : SimpleFunc α γ) : map Prod.snd (f.pair g) = g

@[simp]

theorem MeasureTheory.SimpleFunc.bind_const {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (f : SimpleFunc α β) : f.bind (const α) = f

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instOne {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [One β] : One (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instZero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Zero β] : Zero (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instMul {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Mul β] : Mul (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instAdd {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Add β] : Add (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instDiv {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Div β] : Div (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instSub {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Sub β] : Sub (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instInv {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Inv β] : Inv (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instNeg {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Neg β] : Neg (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instSup {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Max β] : Max (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instInf {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Min β] : Min (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instLE {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [LE β] : LE (SimpleFunc α β)

@[simp]

theorem MeasureTheory.SimpleFunc.const_one {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [One β] : const α 1 = 1

@[simp]

theorem MeasureTheory.SimpleFunc.const_zero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Zero β] : const α 0 = 0

@[simp]

theorem MeasureTheory.SimpleFunc.coe_one {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [One β] : ⇑1 = 1

@[simp]

theorem MeasureTheory.SimpleFunc.coe_zero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Zero β] : ⇑0 = 0

@[simp]

theorem MeasureTheory.SimpleFunc.coe_mul {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Mul β] (f g : SimpleFunc α β) : ⇑(f * g) = ⇑f * ⇑g

@[simp]

theorem MeasureTheory.SimpleFunc.coe_add {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Add β] (f g : SimpleFunc α β) : ⇑(f + g) = ⇑f + ⇑g

@[simp]

theorem MeasureTheory.SimpleFunc.coe_inv {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Inv β] (f : SimpleFunc α β) : ⇑f⁻¹ = (⇑f)⁻¹

@[simp]

theorem MeasureTheory.SimpleFunc.coe_neg {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Neg β] (f : SimpleFunc α β) : ⇑(-f) = -⇑f

@[simp]

theorem MeasureTheory.SimpleFunc.coe_div {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Div β] (f g : SimpleFunc α β) : ⇑(f / g) = ⇑f / ⇑g

@[simp]

theorem MeasureTheory.SimpleFunc.coe_sub {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Sub β] (f g : SimpleFunc α β) : ⇑(f - g) = ⇑f - ⇑g

@[simp]

theorem MeasureTheory.SimpleFunc.coe_sup {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Max β] (f g : SimpleFunc α β) : ⇑(f ⊔ g) = ⇑f ⊔ ⇑g

@[simp]

theorem MeasureTheory.SimpleFunc.coe_inf {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Min β] (f g : SimpleFunc α β) : ⇑(f ⊓ g) = ⇑f ⊓ ⇑g

theorem MeasureTheory.SimpleFunc.mul_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Mul β] (f g : SimpleFunc α β) (a : α) : (f * g) a = f a * g a

theorem MeasureTheory.SimpleFunc.add_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Add β] (f g : SimpleFunc α β) (a : α) : (f + g) a = f a + g a

theorem MeasureTheory.SimpleFunc.div_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Div β] (f g : SimpleFunc α β) (x : α) : (f / g) x = f x / g x

theorem MeasureTheory.SimpleFunc.sub_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Sub β] (f g : SimpleFunc α β) (x : α) : (f - g) x = f x - g x

theorem MeasureTheory.SimpleFunc.inv_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Inv β] (f : SimpleFunc α β) (x : α) : f⁻¹ x = (f x)⁻¹

theorem MeasureTheory.SimpleFunc.neg_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Neg β] (f : SimpleFunc α β) (x : α) : (-f) x = -f x

theorem MeasureTheory.SimpleFunc.sup_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Max β] (f g : SimpleFunc α β) (a : α) : (f ⊔ g) a = f a ⊔ g a

theorem MeasureTheory.SimpleFunc.inf_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Min β] (f g : SimpleFunc α β) (a : α) : (f ⊓ g) a = f a ⊓ g a

@[simp]

theorem MeasureTheory.SimpleFunc.range_one {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Nonempty α] [One β] : SimpleFunc.range 1 = {1}

@[simp]

theorem MeasureTheory.SimpleFunc.range_zero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Nonempty α] [Zero β] : SimpleFunc.range 0 = {0}

@[simp]

theorem MeasureTheory.SimpleFunc.range_eq_empty_of_isEmpty {α : Type u_1} [MeasurableSpace α] {β : Type u_5} [hα : IsEmpty α] (f : SimpleFunc α β) : f.range = ∅

theorem MeasureTheory.SimpleFunc.eq_zero_of_mem_range_zero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Zero β] {y : β} : y ∈ SimpleFunc.range 0 → y = 0

theorem MeasureTheory.SimpleFunc.mul_eq_map₂ {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Mul β] (f g : SimpleFunc α β) : f * g = map (fun (p : β × β) => p.1 * p.2) (f.pair g)

theorem MeasureTheory.SimpleFunc.add_eq_map₂ {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Add β] (f g : SimpleFunc α β) : f + g = map (fun (p : β × β) => p.1 + p.2) (f.pair g)

theorem MeasureTheory.SimpleFunc.sup_eq_map₂ {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Max β] (f g : SimpleFunc α β) : f ⊔ g = map (fun (p : β × β) => p.1 ⊔ p.2) (f.pair g)

theorem MeasureTheory.SimpleFunc.const_mul_eq_map {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Mul β] (f : SimpleFunc α β) (b : β) : const α b * f = map (fun (a : β) => b * a) f

theorem MeasureTheory.SimpleFunc.const_add_eq_map {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Add β] (f : SimpleFunc α β) (b : β) : const α b + f = map (fun (a : β) => b + a) f

theorem MeasureTheory.SimpleFunc.map_mul {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [Mul β] [Mul γ] {g : β → γ} (hg : ∀ (x y : β), g (x * y) = g x * g y) (f₁ f₂ : SimpleFunc α β) : map g (f₁ * f₂) = map g f₁ * map g f₂

theorem MeasureTheory.SimpleFunc.map_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [Add β] [Add γ] {g : β → γ} (hg : ∀ (x y : β), g (x + y) = g x + g y) (f₁ f₂ : SimpleFunc α β) : map g (f₁ + f₂) = map g f₁ + map g f₂

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instSMul {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {K : Type u_5} [SMul K β] : SMul K (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instVAdd {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {K : Type u_5} [VAdd K β] : VAdd K (SimpleFunc α β)

@[simp]

theorem MeasureTheory.SimpleFunc.coe_smul {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {K : Type u_5} [SMul K β] (c : K) (f : SimpleFunc α β) : ⇑(c • f) = c • ⇑f

@[simp]

theorem MeasureTheory.SimpleFunc.coe_vadd {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {K : Type u_5} [VAdd K β] (c : K) (f : SimpleFunc α β) : ⇑(c +ᵥ f) = c +ᵥ ⇑f

@[simp]

theorem MeasureTheory.SimpleFunc.smul_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {K : Type u_5} [SMul K β] (k : K) (f : SimpleFunc α β) (a : α) : (k • f) a = k • f a

@[simp]

theorem MeasureTheory.SimpleFunc.vadd_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {K : Type u_5} [VAdd K β] (k : K) (f : SimpleFunc α β) (a : α) : (k +ᵥ f) a = k +ᵥ f a

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.hasNatSMul {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [AddMonoid β] : SMul ℕ (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.hasNatPow {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Monoid β] : Pow (SimpleFunc α β) ℕ

@[simp]

theorem MeasureTheory.SimpleFunc.coe_pow {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Monoid β] (f : SimpleFunc α β) (n : ℕ) : ⇑(f ^ n) = ⇑f ^ n

theorem MeasureTheory.SimpleFunc.pow_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Monoid β] (n : ℕ) (f : SimpleFunc α β) (a : α) : (f ^ n) a = f a ^ n

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.hasIntPow {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [DivInvMonoid β] : Pow (SimpleFunc α β) ℤ

@[simp]

theorem MeasureTheory.SimpleFunc.coe_zpow {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [DivInvMonoid β] (f : SimpleFunc α β) (z : ℤ) : ⇑(f ^ z) = ⇑f ^ z

theorem MeasureTheory.SimpleFunc.zpow_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [DivInvMonoid β] (z : ℤ) (f : SimpleFunc α β) (a : α) : (f ^ z) a = f a ^ z

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instAddMonoid {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [AddMonoid β] : AddMonoid (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instAddCommMonoid {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [AddCommMonoid β] : AddCommMonoid (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instAddGroup {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [AddGroup β] : AddGroup (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instAddCommGroup {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [AddCommGroup β] : AddCommGroup (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instMonoid {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Monoid β] : Monoid (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instCommMonoid {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [CommMonoid β] : CommMonoid (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instGroup {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Group β] : Group (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instCommGroup {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [CommGroup β] : CommGroup (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instMulAction {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {K : Type u_5} [Monoid K] [MulAction K β] : MulAction K (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instModule {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {K : Type u_5} [Semiring K] [AddCommMonoid β] [Module K β] : Module K (SimpleFunc α β)

theorem MeasureTheory.SimpleFunc.smul_eq_map {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {K : Type u_5} [SMul K β] (k : K) (f : SimpleFunc α β) : k • f = map (fun (x : β) => k • x) f

theorem MeasureTheory.SimpleFunc.smul_const {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {K : Type u_5} [SMul K β] (k : K) (b : β) : k • const α b = const α (k • b)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instNonUnitalNonAssocSemiring {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [NonUnitalNonAssocSemiring β] : NonUnitalNonAssocSemiring (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instNonUnitalSemiring {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [NonUnitalSemiring β] : NonUnitalSemiring (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instNatCast {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [NatCast β] : NatCast (SimpleFunc α β)

@[simp]

theorem MeasureTheory.SimpleFunc.coe_natCast {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [NatCast β] (n : ℕ) : ⇑↑n = fun (x : α) => ↑n

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instNonAssocSemiring {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [NonAssocSemiring β] : NonAssocSemiring (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instIntCast {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [IntCast β] : IntCast (SimpleFunc α β)

@[simp]

theorem MeasureTheory.SimpleFunc.coe_intCast {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [IntCast β] (n : ℤ) : ⇑↑n = fun (x : α) => ↑n

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instNonAssocRing {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [NonAssocRing β] : NonAssocRing (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instNonUnitalCommSemiring {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [NonUnitalCommSemiring β] : NonUnitalCommSemiring (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instCommSemiring {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [CommSemiring β] : CommSemiring (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instNonUnitalCommRing {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [NonUnitalCommRing β] : NonUnitalCommRing (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instCommRing {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [CommRing β] : CommRing (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instSemiring {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Semiring β] : Semiring (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instNonUnitalRing {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [NonUnitalRing β] : NonUnitalRing (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instRing {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Ring β] : Ring (SimpleFunc α β)

instance MeasureTheory.SimpleFunc.instIsScalarTower {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {K : Type u_5} [SMul K γ] [SMul γ β] [SMul K β] [IsScalarTower K γ β] : IsScalarTower K γ (SimpleFunc α β)

instance MeasureTheory.SimpleFunc.instSMulCommClass {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {K : Type u_5} [SMul γ β] [SMul K β] [SMulCommClass K γ β] : SMulCommClass K γ (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instAlgebra {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {K : Type u_5} [CommSemiring K] [Semiring β] [Algebra K β] : Algebra K (SimpleFunc α β)

@[simp]

theorem MeasureTheory.SimpleFunc.const_algebraMap {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {K : Type u_5} [CommSemiring K] [Semiring β] [Algebra K β] (k : K) : const α ((algebraMap K β) k) = (algebraMap K (SimpleFunc α β)) k

@[simp]

theorem MeasureTheory.SimpleFunc.coe_algebraMap {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {K : Type u_5} [CommSemiring K] [Semiring β] [Algebra K β] (k : K) (x : α) : ((algebraMap K (SimpleFunc α β)) k) x = (algebraMap K (α → β)) k x

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instStar {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Star β] : Star (SimpleFunc α β)

@[simp]

theorem MeasureTheory.SimpleFunc.coe_star {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Star β] {f : SimpleFunc α β} : ⇑(star f) = star ⇑f

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instInvolutiveStar {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [InvolutiveStar β] : InvolutiveStar (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instStarAddMonoid {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [AddMonoid β] [StarAddMonoid β] : StarAddMonoid (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instStarMul {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Mul β] [StarMul β] : StarMul (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instStarRing {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [NonUnitalNonAssocSemiring β] [StarRing β] : StarRing (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instPreorder {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Preorder β] : Preorder (SimpleFunc α β)

@[simp]

theorem MeasureTheory.SimpleFunc.coe_le_coe {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Preorder β] {f g : SimpleFunc α β} : ⇑f ≤ ⇑g ↔ f ≤ g

@[simp]

theorem MeasureTheory.SimpleFunc.coe_lt_coe {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Preorder β] {f g : SimpleFunc α β} : ⇑f < ⇑g ↔ f < g

@[deprecated MeasureTheory.SimpleFunc.coe_le_coe (since := "2025-10-21")]

theorem MeasureTheory.SimpleFunc.coe_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Preorder β] {f g : SimpleFunc α β} : ⇑f ≤ ⇑g ↔ f ≤ g

Alias of MeasureTheory.SimpleFunc.coe_le_coe.

@[simp]

theorem MeasureTheory.SimpleFunc.mk_le_mk {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Preorder β] {f g : α → β} {hf : ∀ (x : β), MeasurableSet (f ⁻¹' {x})} {hg : ∀ (x : β), MeasurableSet (g ⁻¹' {x})} {hf' : (Set.range f).Finite} {hg' : (Set.range g).Finite} : { toFun := f, measurableSet_fiber' := hf, finite_range' := hf' } ≤ { toFun := g, measurableSet_fiber' := hg, finite_range' := hg' } ↔ f ≤ g

@[simp]

theorem MeasureTheory.SimpleFunc.mk_lt_mk {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Preorder β] {f g : α → β} {hf : ∀ (x : β), MeasurableSet (f ⁻¹' {x})} {hg : ∀ (x : β), MeasurableSet (g ⁻¹' {x})} {hf' : (Set.range f).Finite} {hg' : (Set.range g).Finite} : { toFun := f, measurableSet_fiber' := hf, finite_range' := hf' } < { toFun := g, measurableSet_fiber' := hg, finite_range' := hg' } ↔ f < g

theorem MeasureTheory.SimpleFunc.piecewise_mono {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Preorder β] {s : Set α} {f₁ f₂ g₁ g₂ : SimpleFunc α β} {hs : MeasurableSet s} (hf : ∀ a ∈ s, f₁ a ≤ f₂ a) (hg : ∀ a ∉ s, g₁ a ≤ g₂ a) : piecewise s hs f₁ g₁ ≤ piecewise s hs f₂ g₂

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instPartialOrder {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [PartialOrder β] : PartialOrder (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instOrderBot {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [LE β] [OrderBot β] : OrderBot (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instOrderTop {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [LE β] [OrderTop β] : OrderTop (SimpleFunc α β)

instance MeasureTheory.SimpleFunc.instIsOrderedMonoid {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [CommMonoid β] [Preorder β] [IsOrderedMonoid β] : IsOrderedMonoid (SimpleFunc α β)

instance MeasureTheory.SimpleFunc.instIsOrderedAddMonoid {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] : IsOrderedAddMonoid (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instSemilatticeInf {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [SemilatticeInf β] : SemilatticeInf (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instSemilatticeSup {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [SemilatticeSup β] : SemilatticeSup (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instLattice {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Lattice β] : Lattice (SimpleFunc α β)

@[implicit_reducible]

instance MeasureTheory.SimpleFunc.instBoundedOrder {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [LE β] [BoundedOrder β] : BoundedOrder (SimpleFunc α β)

theorem MeasureTheory.SimpleFunc.finset_sup_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [SemilatticeSup β] [OrderBot β] {f : γ → SimpleFunc α β} (s : Finset γ) (a : α) : (s.sup f) a = s.sup fun (c : γ) => (f c) a

noncomputable def MeasureTheory.SimpleFunc.restrict {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Zero β] (f : SimpleFunc α β) (s : Set α) : SimpleFunc α β

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.

theorem MeasureTheory.SimpleFunc.restrict_of_not_measurable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Zero β] {f : SimpleFunc α β} {s : Set α} (hs : ¬MeasurableSet s) : f.restrict s = 0

@[simp]

theorem MeasureTheory.SimpleFunc.coe_restrict {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Zero β] (f : SimpleFunc α β) {s : Set α} (hs : MeasurableSet s) : ⇑(f.restrict s) = s.indicator ⇑f

@[simp]

theorem MeasureTheory.SimpleFunc.restrict_univ {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Zero β] (f : SimpleFunc α β) : f.restrict Set.univ = f

@[simp]

theorem MeasureTheory.SimpleFunc.restrict_empty {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Zero β] (f : SimpleFunc α β) : f.restrict ∅ = 0

theorem MeasureTheory.SimpleFunc.map_restrict_of_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [Zero β] [Zero γ] {g : β → γ} (hg : g 0 = 0) (f : SimpleFunc α β) (s : Set α) : map g (f.restrict s) = (map g f).restrict s

theorem MeasureTheory.SimpleFunc.map_coe_ennreal_restrict {α : Type u_1} [MeasurableSpace α] (f : SimpleFunc α NNReal) (s : Set α) : map ENNReal.ofNNReal (f.restrict s) = (map ENNReal.ofNNReal f).restrict s

theorem MeasureTheory.SimpleFunc.map_coe_nnreal_restrict {α : Type u_1} [MeasurableSpace α] (f : SimpleFunc α NNReal) (s : Set α) : map NNReal.toReal (f.restrict s) = (map NNReal.toReal f).restrict s

theorem MeasureTheory.SimpleFunc.restrict_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Zero β] (f : SimpleFunc α β) {s : Set α} (hs : MeasurableSet s) (a : α) : (f.restrict s) a = s.indicator (⇑f) a

theorem MeasureTheory.SimpleFunc.restrict_preimage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Zero β] (f : SimpleFunc α β) {s : Set α} (hs : MeasurableSet s) {t : Set β} (ht : 0 ∉ t) : ⇑(f.restrict s) ⁻¹' t = s ∩ ⇑f ⁻¹' t

theorem MeasureTheory.SimpleFunc.restrict_preimage_singleton {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Zero β] (f : SimpleFunc α β) {s : Set α} (hs : MeasurableSet s) {r : β} (hr : r ≠ 0) : ⇑(f.restrict s) ⁻¹' {r} = s ∩ ⇑f ⁻¹' {r}

theorem MeasureTheory.SimpleFunc.mem_restrict_range {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Zero β] {r : β} {s : Set α} {f : SimpleFunc α β} (hs : MeasurableSet s) : r ∈ (f.restrict s).range ↔ r = 0 ∧ s ≠ Set.univ ∨ r ∈ ⇑f '' s

theorem MeasureTheory.SimpleFunc.mem_image_of_mem_range_restrict {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Zero β] {r : β} {s : Set α} {f : SimpleFunc α β} (hr : r ∈ (f.restrict s).range) (h0 : r ≠ 0) : r ∈ ⇑f '' s

theorem MeasureTheory.SimpleFunc.restrict_mono {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Zero β] [Preorder β] (s : Set α) {f g : SimpleFunc α β} (H : f ≤ g) : f.restrict s ≤ g.restrict s

noncomputable def MeasureTheory.SimpleFunc.approx {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [SemilatticeSup β] [OrderBot β] [Zero β] (i : ℕ → β) (f : α → β) (n : ℕ) : SimpleFunc α β

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.

theorem MeasureTheory.SimpleFunc.approx_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [SemilatticeSup β] [OrderBot β] [Zero β] [TopologicalSpace β] [OrderClosedTopology β] [MeasurableSpace β] [OpensMeasurableSpace β] {i : ℕ → β} {f : α → β} {n : ℕ} (a : α) (hf : Measurable f) : (approx i f n) a = (Finset.range n).sup fun (k : ℕ) => if i k ≤ f a then i k else 0

theorem MeasureTheory.SimpleFunc.monotone_approx {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [SemilatticeSup β] [OrderBot β] [Zero β] (i : ℕ → β) (f : α → β) : Monotone (approx i f)

theorem MeasureTheory.SimpleFunc.approx_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [SemilatticeSup β] [OrderBot β] [Zero β] [TopologicalSpace β] [OrderClosedTopology β] [MeasurableSpace β] [OpensMeasurableSpace β] [MeasurableSpace γ] {i : ℕ → β} {f : γ → β} {g : α → γ} {n : ℕ} (a : α) (hf : Measurable f) (hg : Measurable g) : (approx i (f ∘ g) n) a = (approx i f n) (g a)

theorem MeasureTheory.SimpleFunc.iSup_approx_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [TopologicalSpace β] [CompleteLattice β] [OrderClosedTopology β] [Zero β] [MeasurableSpace β] [OpensMeasurableSpace β] (i : ℕ → β) (f : α → β) (a : α) (hf : Measurable f) (h_zero : 0 = ⊥) : ⨆ (n : ℕ), (approx i f n) a = ⨆ (k : ℕ), ⨆ (_ : i k ≤ f a), i k

def MeasureTheory.SimpleFunc.ennrealRatEmbed (n : ℕ) : ENNReal

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

theorem MeasureTheory.SimpleFunc.ennrealRatEmbed_encode (q : ℚ) : ennrealRatEmbed (Encodable.encode q) = ↑(↑q).toNNReal

noncomputable def MeasureTheory.SimpleFunc.eapprox {α : Type u_1} [MeasurableSpace α] : (α → ENNReal) → ℕ → SimpleFunc α ENNReal

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

theorem MeasureTheory.SimpleFunc.eapprox_lt_top {α : Type u_1} [MeasurableSpace α] (f : α → ENNReal) (n : ℕ) (a : α) : (eapprox f n) a < ⊤

theorem MeasureTheory.SimpleFunc.monotone_eapprox {α : Type u_1} [MeasurableSpace α] (f : α → ENNReal) : Monotone (eapprox f)

theorem MeasureTheory.SimpleFunc.iSup_eapprox_apply {α : Type u_1} [MeasurableSpace α] {f : α → ENNReal} (hf : Measurable f) (a : α) : ⨆ (n : ℕ), (eapprox f n) a = f a

theorem MeasureTheory.SimpleFunc.iSup_coe_eapprox {α : Type u_1} [MeasurableSpace α] {f : α → ENNReal} (hf : Measurable f) : ⨆ (n : ℕ), ⇑(eapprox f n) = f

theorem MeasureTheory.SimpleFunc.eapprox_comp {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace γ] {f : γ → ENNReal} {g : α → γ} {n : ℕ} (hf : Measurable f) (hg : Measurable g) : ⇑(eapprox (f ∘ g) n) = ⇑(eapprox f n) ∘ g

theorem MeasureTheory.SimpleFunc.tendsto_eapprox {α : Type u_1} [MeasurableSpace α] {f : α → ENNReal} (hf_meas : Measurable f) (a : α) : Filter.Tendsto (fun (n : ℕ) => (eapprox f n) a) Filter.atTop (nhds (f a))

noncomputable def MeasureTheory.SimpleFunc.eapproxDiff {α : Type u_1} [MeasurableSpace α] (f : α → ENNReal) : ℕ → SimpleFunc α NNReal

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

theorem MeasureTheory.SimpleFunc.sum_eapproxDiff {α : Type u_1} [MeasurableSpace α] (f : α → ENNReal) (n : ℕ) (a : α) : ∑ k ∈ Finset.range (n + 1), ↑((eapproxDiff f k) a) = (eapprox f n) a

theorem MeasureTheory.SimpleFunc.tsum_eapproxDiff {α : Type u_1} [MeasurableSpace α] (f : α → ENNReal) (hf : Measurable f) (a : α) : ∑' (n : ℕ), ↑((eapproxDiff f n) a) = f a

noncomputable def MeasureTheory.SimpleFunc.lintegral {α : Type u_1} {_m : MeasurableSpace α} (f : SimpleFunc α ENNReal) (μ : Measure α) : ENNReal

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

theorem MeasureTheory.SimpleFunc.lintegral_eq_of_subset {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (f : SimpleFunc α ENNReal) {s : Finset ENNReal} (hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s) : f.lintegral μ = ∑ x ∈ s, x * μ (⇑f ⁻¹' {x})

theorem MeasureTheory.SimpleFunc.lintegral_eq_of_subset' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (f : SimpleFunc α ENNReal) {s : Finset ENNReal} (hs : f.range \ {0} ⊆ s) : f.lintegral μ = ∑ x ∈ s, x * μ (⇑f ⁻¹' {x})

theorem MeasureTheory.SimpleFunc.map_lintegral {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} (g : β → ENNReal) (f : SimpleFunc α β) : (map g f).lintegral μ = ∑ x ∈ f.range, g x * μ (⇑f ⁻¹' {x})

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

theorem MeasureTheory.SimpleFunc.add_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (f g : SimpleFunc α ENNReal) : (f + g).lintegral μ = f.lintegral μ + g.lintegral μ

theorem MeasureTheory.SimpleFunc.const_mul_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (f : SimpleFunc α ENNReal) (x : ENNReal) : (const α x * f).lintegral μ = x * f.lintegral μ

noncomputable def MeasureTheory.SimpleFunc.lintegralₗ {α : Type u_1} {m : MeasurableSpace α} : SimpleFunc α ENNReal →ₗ[ENNReal] Measure α →ₗ[ENNReal] ENNReal

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

@[simp]

theorem MeasureTheory.SimpleFunc.zero_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} : lintegral 0 μ = 0

theorem MeasureTheory.SimpleFunc.lintegral_add {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} (f : SimpleFunc α ENNReal) : f.lintegral (μ + ν) = f.lintegral μ + f.lintegral ν

theorem MeasureTheory.SimpleFunc.lintegral_smul {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {R : Type u_5} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (f : SimpleFunc α ENNReal) (c : R) : f.lintegral (c • μ) = c • f.lintegral μ

@[simp]

theorem MeasureTheory.SimpleFunc.lintegral_zero {α : Type u_1} [MeasurableSpace α] (f : SimpleFunc α ENNReal) : f.lintegral 0 = 0

theorem MeasureTheory.SimpleFunc.lintegral_finset_sum {α : Type u_1} {m : MeasurableSpace α} {ι : Type u_5} (f : SimpleFunc α ENNReal) (μ : ι → Measure α) (s : Finset ι) : f.lintegral (∑ i ∈ s, μ i) = ∑ i ∈ s, f.lintegral (μ i)

theorem MeasureTheory.SimpleFunc.lintegral_sum {α : Type u_1} {m : MeasurableSpace α} {ι : Type u_5} (f : SimpleFunc α ENNReal) (μ : ι → Measure α) : f.lintegral (Measure.sum μ) = ∑' (i : ι), f.lintegral (μ i)

theorem MeasureTheory.SimpleFunc.restrict_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (f : SimpleFunc α ENNReal) {s : Set α} (hs : MeasurableSet s) : (f.restrict s).lintegral μ = ∑ r ∈ f.range, r * μ (⇑f ⁻¹' {r} ∩ s)

theorem MeasureTheory.SimpleFunc.lintegral_restrict {α : Type u_1} {m : MeasurableSpace α} (f : SimpleFunc α ENNReal) (s : Set α) (μ : Measure α) : f.lintegral (μ.restrict s) = ∑ y ∈ f.range, y * μ (⇑f ⁻¹' {y} ∩ s)

theorem MeasureTheory.SimpleFunc.restrict_lintegral_eq_lintegral_restrict {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (f : SimpleFunc α ENNReal) {s : Set α} (hs : MeasurableSet s) : (f.restrict s).lintegral μ = f.lintegral (μ.restrict s)

theorem MeasureTheory.SimpleFunc.lintegral_restrict_iUnion_of_directed {α : Type u_1} {m : MeasurableSpace α} {ι : Type u_5} [Countable ι] (f : SimpleFunc α ENNReal) {s : ι → Set α} (hd : Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) s) (μ : Measure α) : f.lintegral (μ.restrict (⋃ (i : ι), s i)) = ⨆ (i : ι), f.lintegral (μ.restrict (s i))

theorem MeasureTheory.SimpleFunc.const_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (c : ENNReal) : (const α c).lintegral μ = c * μ Set.univ

theorem MeasureTheory.SimpleFunc.const_lintegral_restrict {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (c : ENNReal) (s : Set α) : (const α c).lintegral (μ.restrict s) = c * μ s

theorem MeasureTheory.SimpleFunc.restrict_const_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (c : ENNReal) {s : Set α} (hs : MeasurableSet s) : ((const α c).restrict s).lintegral μ = c * μ s

theorem MeasureTheory.SimpleFunc.lintegral_mono_fun {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f g : SimpleFunc α ENNReal} (h : f ≤ g) : f.lintegral μ ≤ g.lintegral μ

theorem MeasureTheory.SimpleFunc.le_sup_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (f g : SimpleFunc α ENNReal) : max (f.lintegral μ) (g.lintegral μ) ≤ (f ⊔ g).lintegral μ

theorem MeasureTheory.SimpleFunc.lintegral_mono_measure {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} {f : SimpleFunc α ENNReal} (h : μ ≤ ν) : f.lintegral μ ≤ f.lintegral ν

theorem MeasureTheory.SimpleFunc.lintegral_mono {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} {f g : SimpleFunc α ENNReal} (hfg : f ≤ g) (hμν : μ ≤ ν) : f.lintegral μ ≤ g.lintegral ν

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 : MeasurableSpace α} {μ : Measure α} [MeasurableSpace β] {f : SimpleFunc α ENNReal} {g : SimpleFunc β ENNReal} {ν : Measure β} (H : ∀ (y : ENNReal), μ (⇑f ⁻¹' {y}) = ν (⇑g ⁻¹' {y})) : f.lintegral μ = g.lintegral ν

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

theorem MeasureTheory.SimpleFunc.lintegral_congr {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f g : SimpleFunc α ENNReal} (h : ⇑f =ᶠ[ae μ] ⇑g) : f.lintegral μ = g.lintegral μ

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

theorem MeasureTheory.SimpleFunc.lintegral_map' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_5} [MeasurableSpace β] {μ' : Measure β} (f : SimpleFunc α ENNReal) (g : SimpleFunc β ENNReal) (m' : α → β) (eq : ∀ (a : α), f a = g (m' a)) (h : ∀ (s : Set β), MeasurableSet s → μ' s = μ (m' ⁻¹' s)) : f.lintegral μ = g.lintegral μ'

theorem MeasureTheory.SimpleFunc.lintegral_map {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_5} [MeasurableSpace β] (g : SimpleFunc β ENNReal) {f : α → β} (hf : Measurable f) : g.lintegral (Measure.map f μ) = (g.comp f hf).lintegral μ

theorem MeasureTheory.SimpleFunc.support_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Zero β] (f : SimpleFunc α β) : Function.support ⇑f = ⋃ y ∈ {y ∈ f.range | y ≠ 0}, ⇑f ⁻¹' {y}

theorem MeasureTheory.SimpleFunc.measurableSet_support {α : Type u_1} {β : Type u_2} [Zero β] [MeasurableSpace α] (f : SimpleFunc α β) : MeasurableSet (Function.support ⇑f)

theorem MeasureTheory.SimpleFunc.measure_support_lt_top {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [Zero β] {μ : Measure α} (f : SimpleFunc α β) (hf : ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤) : μ (Function.support ⇑f) < ⊤

def MeasureTheory.SimpleFunc.FinMeasSupp {α : Type u_1} {β : Type u_2} [Zero β] {_m : MeasurableSpace α} (f : SimpleFunc α β) (μ : Measure α) : Prop

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

theorem MeasureTheory.SimpleFunc.finMeasSupp_iff_support {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [Zero β] {μ : Measure α} {f : SimpleFunc α β} : f.FinMeasSupp μ ↔ μ (Function.support ⇑f) < ⊤

theorem MeasureTheory.SimpleFunc.finMeasSupp_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [Zero β] {μ : Measure α} {f : SimpleFunc α β} : f.FinMeasSupp μ ↔ ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤

theorem MeasureTheory.SimpleFunc.FinMeasSupp.meas_preimage_singleton_ne_zero {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [Zero β] {μ : Measure α} {f : SimpleFunc α β} (h : f.FinMeasSupp μ) {y : β} (hy : y ≠ 0) : μ (⇑f ⁻¹' {y}) < ⊤

theorem MeasureTheory.SimpleFunc.FinMeasSupp.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} [Zero β] [Zero γ] {μ : Measure α} {f : SimpleFunc α β} {g : β → γ} (hf : f.FinMeasSupp μ) (hg : g 0 = 0) : (map g f).FinMeasSupp μ

theorem MeasureTheory.SimpleFunc.FinMeasSupp.of_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} [Zero β] [Zero γ] {μ : Measure α} {f : SimpleFunc α β} {g : β → γ} (h : (map g f).FinMeasSupp μ) (hg : ∀ (b : β), g b = 0 → b = 0) : f.FinMeasSupp μ

theorem MeasureTheory.SimpleFunc.FinMeasSupp.map_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} [Zero β] [Zero γ] {μ : Measure α} {f : SimpleFunc α β} {g : β → γ} (hg : ∀ {b : β}, g b = 0 ↔ b = 0) : (map g f).FinMeasSupp μ ↔ f.FinMeasSupp μ

theorem MeasureTheory.SimpleFunc.FinMeasSupp.pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} [Zero β] [Zero γ] {μ : Measure α} {f : SimpleFunc α β} {g : SimpleFunc α γ} (hf : f.FinMeasSupp μ) (hg : g.FinMeasSupp μ) : (f.pair g).FinMeasSupp μ

theorem MeasureTheory.SimpleFunc.FinMeasSupp.map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m : MeasurableSpace α} [Zero β] [Zero γ] {μ : Measure α} {f : SimpleFunc α β} [Zero δ] (hf : f.FinMeasSupp μ) {g : SimpleFunc α γ} (hg : g.FinMeasSupp μ) {op : β → γ → δ} (H : op 0 0 = 0) : (map (Function.uncurry op) (f.pair g)).FinMeasSupp μ

theorem MeasureTheory.SimpleFunc.FinMeasSupp.add {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_5} [AddZeroClass β] {f g : SimpleFunc α β} (hf : f.FinMeasSupp μ) (hg : g.FinMeasSupp μ) : (f + g).FinMeasSupp μ

theorem MeasureTheory.SimpleFunc.FinMeasSupp.mul {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_5} [MulZeroClass β] {f g : SimpleFunc α β} (hf : f.FinMeasSupp μ) (hg : g.FinMeasSupp μ) : (f * g).FinMeasSupp μ

theorem MeasureTheory.SimpleFunc.FinMeasSupp.lintegral_lt_top {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : SimpleFunc α ENNReal} (hm : f.FinMeasSupp μ) (hf : ∀ᵐ (a : α) ∂μ, f a ≠ ⊤) : f.lintegral μ < ⊤

theorem MeasureTheory.SimpleFunc.FinMeasSupp.of_lintegral_ne_top {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : SimpleFunc α ENNReal} (h : f.lintegral μ ≠ ⊤) : f.FinMeasSupp μ

theorem MeasureTheory.SimpleFunc.FinMeasSupp.iff_lintegral_lt_top {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : SimpleFunc α ENNReal} (hf : ∀ᵐ (a : α) ∂μ, f a ≠ ⊤) : f.FinMeasSupp μ ↔ f.lintegral μ < ⊤

theorem MeasureTheory.SimpleFunc.measure_support_lt_top_of_lintegral_ne_top {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : SimpleFunc α ENNReal} (hf : f.lintegral μ ≠ ⊤) : μ (Function.support ⇑f) < ⊤

theorem MeasureTheory.SimpleFunc.induction {α : Type u_5} {γ : Type u_6} [MeasurableSpace α] [AddZeroClass γ] {motive : SimpleFunc α γ → Prop} (const : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (const α c) (const α 0))) (add : ∀ ⦃f g : SimpleFunc α γ⦄, Disjoint (Function.support ⇑f) (Function.support ⇑g) → motive f → motive g → motive (f + g)) (f : SimpleFunc α γ) : motive 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).

To use in an induction proof, the syntax is induction f using SimpleFunc.induction with.

theorem MeasureTheory.SimpleFunc.induction' {α : Type u_5} {γ : Type u_6} [MeasurableSpace α] [Nonempty γ] {P : SimpleFunc α γ → Prop} (const : ∀ (c : γ), P (const α c)) (pcw : ∀ ⦃f g : SimpleFunc α γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)) (f : SimpleFunc α γ) : P f

To prove something for an arbitrary simple function, it suffices to show that the property holds for constant functions and that it is closed under piecewise combinations of functions.

To use in an induction proof, the syntax is induction f with.

theorem Measurable.add_simpleFunc {α : Type u_1} {E : Type u_5} {x✝ : MeasurableSpace α} [MeasurableSpace E] [AddCancelMonoid E] [MeasurableAdd E] {g : α → E} (hg : Measurable g) (f : MeasureTheory.SimpleFunc α E) : 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✝ : MeasurableSpace α} [MeasurableSpace E] [AddCancelMonoid E] [MeasurableAdd E] {g : α → E} (hg : Measurable g) (f : MeasureTheory.SimpleFunc α E) : 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} {mα : MeasurableSpace α} {motive : (α → ENNReal) → Prop} (indicator : ∀ (c : ENNReal) ⦃s : Set α⦄, MeasurableSet s → motive (s.indicator fun (x : α) => c)) (add : ∀ ⦃f g : α → ENNReal⦄, Disjoint (Function.support f) (Function.support g) → Measurable f → Measurable g → motive f → motive g → motive (f + g)) (iSup : ∀ ⦃f : ℕ → α → ENNReal⦄, (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), motive (f n)) → motive fun (x : α) => ⨆ (n : ℕ), f n x) ⦃f : α → ENNReal⦄ (hf : Measurable f) : motive 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}).

theorem Measurable.ennreal_sigmaFinite_induction {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {motive : (α → ENNReal) → Prop} (indicator : ∀ (c : ENNReal) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → motive (s.indicator fun (x : α) => c)) (add : ∀ ⦃f g : α → ENNReal⦄, Disjoint (Function.support f) (Function.support g) → Measurable f → Measurable g → motive f → motive g → motive (f + g)) (iSup : ∀ ⦃f : ℕ → α → ENNReal⦄, (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), motive (f n)) → motive fun (x : α) => ⨆ (n : ℕ), f n x) ⦃f : α → ENNReal⦄ (hf : Measurable f) : motive f

To prove something for an arbitrary measurable function into ℝ≥0∞, it suffices to show that the property holds for (multiples of) characteristic functions with finite mass according to some sigma-finite measure 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}).