Documentation

Mathlib.MeasureTheory.Function.SimpleFunc

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.

Instances For
    theorem MeasureTheory.SimpleFunc.measurableSet_fiber' {α : Type u} [MeasurableSpace α] {β : Type v} (self : MeasureTheory.SimpleFunc α β) (x : β) :
    MeasurableSet (self.toFun ⁻¹' {x})
    theorem MeasureTheory.SimpleFunc.finite_range' {α : Type u} [MeasurableSpace α] {β : Type v} (self : MeasureTheory.SimpleFunc α β) :
    (Set.range self.toFun).Finite
    Equations
    • MeasureTheory.SimpleFunc.instFunLike = { coe := MeasureTheory.SimpleFunc.toFun, coe_injective' := }
    theorem MeasureTheory.SimpleFunc.coe_injective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] ⦃f : MeasureTheory.SimpleFunc α β ⦃g : MeasureTheory.SimpleFunc α β (H : f = g) :
    f = g
    theorem MeasureTheory.SimpleFunc.ext_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {f : MeasureTheory.SimpleFunc α β} {g : MeasureTheory.SimpleFunc α β} :
    f = g ∀ (a : α), f a = g a
    theorem MeasureTheory.SimpleFunc.ext {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {f : MeasureTheory.SimpleFunc α β} {g : MeasureTheory.SimpleFunc α β} (H : ∀ (a : α), f a = g a) :
    f = g
    theorem MeasureTheory.SimpleFunc.finite_range {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) :
    (Set.range f).Finite
    @[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

    Simple function defined on a finite type.

    Equations
    Instances For
      @[deprecated MeasureTheory.SimpleFunc.ofFinite]

      Alias of MeasureTheory.SimpleFunc.ofFinite.


      Simple function defined on a finite type.

      Equations
      Instances For

        Simple function defined on the empty type.

        Equations
        Instances For

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

          Equations
          • f.range = .toFinset
          Instances For
            @[simp]
            theorem MeasureTheory.SimpleFunc.mem_range {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {f : MeasureTheory.SimpleFunc α β} {b : β} :
            b f.range b Set.range f
            theorem MeasureTheory.SimpleFunc.mem_range_self {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) (x : α) :
            f x f.range
            @[simp]
            theorem MeasureTheory.SimpleFunc.coe_range {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) :
            f.range = Set.range f
            theorem MeasureTheory.SimpleFunc.mem_range_of_measure_ne_zero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {f : MeasureTheory.SimpleFunc α β} {x : β} {μ : MeasureTheory.Measure α} (H : μ (f ⁻¹' {x}) 0) :
            x f.range
            theorem MeasureTheory.SimpleFunc.forall_mem_range {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {f : MeasureTheory.SimpleFunc α β} {p : βProp} :
            (∀ yf.range, p y) ∀ (x : α), p (f x)
            theorem MeasureTheory.SimpleFunc.exists_range_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {f : MeasureTheory.SimpleFunc α β} {p : βProp} :
            (∃ yf.range, p y) ∃ (x : α), p (f x)
            theorem MeasureTheory.SimpleFunc.preimage_eq_empty_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) (b : β) :
            f ⁻¹' {b} = bf.range
            theorem MeasureTheory.SimpleFunc.exists_forall_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Nonempty β] [Preorder β] [IsDirected β fun (x1 x2 : β) => x1 x2] (f : MeasureTheory.SimpleFunc α β) :
            ∃ (C : β), ∀ (x : α), f x C

            Constant function as a SimpleFunc.

            Equations
            Instances For
              Equations
              theorem MeasureTheory.SimpleFunc.const_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (a : α) (b : β) :
              @[simp]
              @[simp]
              theorem MeasureTheory.SimpleFunc.range_const {β : Type u_2} (α : Type u_5) [MeasurableSpace α] [Nonempty α] (b : β) :
              theorem MeasureTheory.SimpleFunc.simpleFunc_bot {β : Type u_2} {α : Type u_5} (f : MeasureTheory.SimpleFunc α β) [Nonempty β] :
              ∃ (c : β), ∀ (x : α), f x = c
              theorem MeasureTheory.SimpleFunc.measurableSet_cut {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (r : αβProp) (f : MeasureTheory.SimpleFunc α β) (h : ∀ (b : β), MeasurableSet {a : α | r a b}) :
              MeasurableSet {a : α | r a (f a)}

              A simple function is measurable

              theorem MeasureTheory.SimpleFunc.sum_measure_preimage_singleton {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) {μ : MeasureTheory.Measure α} (s : Finset β) :
              ys, μ (f ⁻¹' {y}) = μ (f ⁻¹' s)
              theorem MeasureTheory.SimpleFunc.sum_range_measure_preimage_singleton {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) (μ : MeasureTheory.Measure α) :
              yf.range, μ (f ⁻¹' {y}) = μ Set.univ

              If-then-else as a SimpleFunc.

              Equations
              Instances For
                @[simp]
                theorem MeasureTheory.SimpleFunc.coe_piecewise {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {s : Set α} (hs : MeasurableSet s) (f : MeasureTheory.SimpleFunc α β) (g : MeasureTheory.SimpleFunc α β) :
                (MeasureTheory.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 : MeasureTheory.SimpleFunc α β) (g : MeasureTheory.SimpleFunc α β) (a : α) :
                (MeasureTheory.SimpleFunc.piecewise s hs f g) a = if a s then f a else g a
                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 : β) :
                theorem MeasureTheory.SimpleFunc.measurable_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace γ] (f : MeasureTheory.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 : MeasureTheory.SimpleFunc α β) (g : βMeasureTheory.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.

                Equations
                • f.bind g = { 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} [MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) (g : βMeasureTheory.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 : MeasureTheory.SimpleFunc α β) :

                  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} [MeasurableSpace α] (g : βγ) (f : MeasureTheory.SimpleFunc α β) (a : α) :
                    theorem MeasureTheory.SimpleFunc.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] (g : βγ) (h : γδ) (f : MeasureTheory.SimpleFunc α β) :
                    @[simp]
                    theorem MeasureTheory.SimpleFunc.coe_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (g : βγ) (f : MeasureTheory.SimpleFunc α β) :
                    @[simp]
                    theorem MeasureTheory.SimpleFunc.range_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [DecidableEq γ] (g : βγ) (f : MeasureTheory.SimpleFunc α β) :
                    @[simp]
                    theorem MeasureTheory.SimpleFunc.map_preimage {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) (g : βγ) (s : Set γ) :
                    (MeasureTheory.SimpleFunc.map g f) ⁻¹' s = f ⁻¹' (Finset.filter (fun (b : β) => g b s) f.range)
                    theorem MeasureTheory.SimpleFunc.map_preimage_singleton {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) (g : βγ) (c : γ) :
                    (MeasureTheory.SimpleFunc.map g f) ⁻¹' {c} = f ⁻¹' (Finset.filter (fun (b : β) => g b = c) f.range)
                    def MeasureTheory.SimpleFunc.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (f : MeasureTheory.SimpleFunc β γ) (g : αβ) (hgm : Measurable g) :

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

                    Equations
                    • f.comp g hgm = { toFun := f g, measurableSet_fiber' := , finite_range' := }
                    Instances For
                      @[simp]
                      theorem MeasureTheory.SimpleFunc.coe_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (f : MeasureTheory.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 : MeasureTheory.SimpleFunc β γ) {g : αβ} (hgm : Measurable g) :
                      (f.comp g hgm).range f.range
                      def MeasureTheory.SimpleFunc.extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (f₁ : MeasureTheory.SimpleFunc α γ) (g : αβ) (hg : MeasurableEmbedding g) (f₂ : MeasureTheory.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.

                      Equations
                      • f₁.extend g hg f₂ = { 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} [MeasurableSpace α] [MeasurableSpace β] (f₁ : MeasureTheory.SimpleFunc α γ) {g : αβ} (hg : MeasurableEmbedding g) (f₂ : MeasureTheory.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₁ : MeasureTheory.SimpleFunc α γ) {g : αβ} (hg : MeasurableEmbedding g) (f₂ : MeasureTheory.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₁ : MeasureTheory.SimpleFunc α γ) {g : αβ} (hg : MeasurableEmbedding g) (f₂ : MeasureTheory.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₁ : MeasureTheory.SimpleFunc α γ) {g : αβ} (hg : MeasurableEmbedding g) (f₂ : MeasureTheory.SimpleFunc β γ) :
                        (f₁.extend g hg f₂).comp g = f₁
                        def MeasureTheory.SimpleFunc.seq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (f : MeasureTheory.SimpleFunc α (βγ)) (g : MeasureTheory.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).

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

                          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} [MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) (g : MeasureTheory.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 : MeasureTheory.SimpleFunc α β) (g : MeasureTheory.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 : MeasureTheory.SimpleFunc α β) (g : MeasureTheory.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 : MeasureTheory.SimpleFunc α β) (g : MeasureTheory.SimpleFunc α γ) :
                            MeasureTheory.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 : MeasureTheory.SimpleFunc α β) (g : MeasureTheory.SimpleFunc α γ) :
                            MeasureTheory.SimpleFunc.map Prod.snd (f.pair g) = g
                            Equations
                            Equations
                            Equations
                            Equations
                            Equations
                            Equations
                            Equations
                            Equations
                            Equations
                            Equations
                            instance MeasureTheory.SimpleFunc.instLE {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [LE β] :
                            Equations
                            @[simp]
                            theorem MeasureTheory.SimpleFunc.coe_zero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Zero β] :
                            0 = 0
                            @[simp]
                            theorem MeasureTheory.SimpleFunc.coe_one {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [One β] :
                            1 = 1
                            @[simp]
                            theorem MeasureTheory.SimpleFunc.coe_add {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Add β] (f : MeasureTheory.SimpleFunc α β) (g : MeasureTheory.SimpleFunc α β) :
                            (f + g) = f + g
                            @[simp]
                            theorem MeasureTheory.SimpleFunc.coe_mul {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Mul β] (f : MeasureTheory.SimpleFunc α β) (g : MeasureTheory.SimpleFunc α β) :
                            (f * g) = f * g
                            @[simp]
                            theorem MeasureTheory.SimpleFunc.coe_neg {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Neg β] (f : MeasureTheory.SimpleFunc α β) :
                            (-f) = -f
                            @[simp]
                            theorem MeasureTheory.SimpleFunc.coe_inv {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Inv β] (f : MeasureTheory.SimpleFunc α β) :
                            f⁻¹ = (⇑f)⁻¹
                            @[simp]
                            theorem MeasureTheory.SimpleFunc.coe_sub {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Sub β] (f : MeasureTheory.SimpleFunc α β) (g : MeasureTheory.SimpleFunc α β) :
                            (f - g) = f - g
                            @[simp]
                            theorem MeasureTheory.SimpleFunc.coe_div {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Div β] (f : MeasureTheory.SimpleFunc α β) (g : MeasureTheory.SimpleFunc α β) :
                            (f / g) = f / g
                            @[simp]
                            theorem MeasureTheory.SimpleFunc.coe_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Preorder β] {f : MeasureTheory.SimpleFunc α β} {g : MeasureTheory.SimpleFunc α β} :
                            f g f g
                            @[simp]
                            theorem MeasureTheory.SimpleFunc.coe_sup {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Sup β] (f : MeasureTheory.SimpleFunc α β) (g : MeasureTheory.SimpleFunc α β) :
                            (f g) = f g
                            @[simp]
                            theorem MeasureTheory.SimpleFunc.coe_inf {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Inf β] (f : MeasureTheory.SimpleFunc α β) (g : MeasureTheory.SimpleFunc α β) :
                            (f g) = f g
                            theorem MeasureTheory.SimpleFunc.add_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Add β] (f : MeasureTheory.SimpleFunc α β) (g : MeasureTheory.SimpleFunc α β) (a : α) :
                            (f + g) a = f a + g a
                            theorem MeasureTheory.SimpleFunc.mul_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Mul β] (f : MeasureTheory.SimpleFunc α β) (g : MeasureTheory.SimpleFunc α β) (a : α) :
                            (f * g) a = f a * g a
                            theorem MeasureTheory.SimpleFunc.sub_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Sub β] (f : MeasureTheory.SimpleFunc α β) (g : MeasureTheory.SimpleFunc α β) (x : α) :
                            (f - g) x = f x - g x
                            theorem MeasureTheory.SimpleFunc.div_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Div β] (f : MeasureTheory.SimpleFunc α β) (g : MeasureTheory.SimpleFunc α β) (x : α) :
                            (f / g) x = f x / g x
                            theorem MeasureTheory.SimpleFunc.neg_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Neg β] (f : MeasureTheory.SimpleFunc α β) (x : α) :
                            (-f) x = -f x
                            theorem MeasureTheory.SimpleFunc.inv_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Inv β] (f : MeasureTheory.SimpleFunc α β) (x : α) :
                            f⁻¹ x = (f x)⁻¹
                            theorem MeasureTheory.SimpleFunc.sup_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Sup β] (f : MeasureTheory.SimpleFunc α β) (g : MeasureTheory.SimpleFunc α β) (a : α) :
                            (f g) a = f a g a
                            theorem MeasureTheory.SimpleFunc.inf_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Inf β] (f : MeasureTheory.SimpleFunc α β) (g : MeasureTheory.SimpleFunc α β) (a : α) :
                            (f g) a = f a g a
                            @[simp]
                            theorem MeasureTheory.SimpleFunc.range_eq_empty_of_isEmpty {α : Type u_1} [MeasurableSpace α] {β : Type u_5} [hα : IsEmpty α] (f : MeasureTheory.SimpleFunc α β) :
                            f.range =
                            theorem MeasureTheory.SimpleFunc.add_eq_map₂ {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Add β] (f : MeasureTheory.SimpleFunc α β) (g : MeasureTheory.SimpleFunc α β) :
                            f + g = MeasureTheory.SimpleFunc.map (fun (p : β × β) => p.1 + p.2) (f.pair g)
                            theorem MeasureTheory.SimpleFunc.mul_eq_map₂ {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Mul β] (f : MeasureTheory.SimpleFunc α β) (g : MeasureTheory.SimpleFunc α β) :
                            f * g = MeasureTheory.SimpleFunc.map (fun (p : β × β) => p.1 * p.2) (f.pair g)
                            theorem MeasureTheory.SimpleFunc.sup_eq_map₂ {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Sup β] (f : MeasureTheory.SimpleFunc α β) (g : MeasureTheory.SimpleFunc α β) :
                            f g = MeasureTheory.SimpleFunc.map (fun (p : β × β) => p.1 p.2) (f.pair g)
                            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₁ : MeasureTheory.SimpleFunc α β) (f₂ : MeasureTheory.SimpleFunc α β) :
                            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₁ : MeasureTheory.SimpleFunc α β) (f₂ : MeasureTheory.SimpleFunc α β) :
                            instance MeasureTheory.SimpleFunc.instVAdd {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {K : Type u_5} [VAdd K β] :
                            Equations
                            instance MeasureTheory.SimpleFunc.instSMul {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {K : Type u_5} [SMul K β] :
                            Equations
                            @[simp]
                            theorem MeasureTheory.SimpleFunc.coe_vadd {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {K : Type u_5} [VAdd K β] (c : K) (f : MeasureTheory.SimpleFunc α β) :
                            (c +ᵥ f) = c +ᵥ f
                            @[simp]
                            theorem MeasureTheory.SimpleFunc.coe_smul {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {K : Type u_5} [SMul K β] (c : K) (f : MeasureTheory.SimpleFunc α β) :
                            (c f) = c f
                            @[simp]
                            theorem MeasureTheory.SimpleFunc.vadd_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {K : Type u_5} [VAdd K β] (k : K) (f : MeasureTheory.SimpleFunc α β) (a : α) :
                            (k +ᵥ f) a = k +ᵥ f a
                            @[simp]
                            theorem MeasureTheory.SimpleFunc.smul_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {K : Type u_5} [SMul K β] (k : K) (f : MeasureTheory.SimpleFunc α β) (a : α) :
                            (k f) a = k f a
                            Equations
                            • MeasureTheory.SimpleFunc.hasNatSMul = inferInstance
                            Equations
                            @[simp]
                            theorem MeasureTheory.SimpleFunc.coe_pow {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Monoid β] (f : MeasureTheory.SimpleFunc α β) (n : ) :
                            (f ^ n) = f ^ n
                            theorem MeasureTheory.SimpleFunc.pow_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Monoid β] (n : ) (f : MeasureTheory.SimpleFunc α β) (a : α) :
                            (f ^ n) a = f a ^ n
                            Equations
                            @[simp]
                            theorem MeasureTheory.SimpleFunc.coe_zpow {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [DivInvMonoid β] (f : MeasureTheory.SimpleFunc α β) (z : ) :
                            (f ^ z) = f ^ z
                            theorem MeasureTheory.SimpleFunc.zpow_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [DivInvMonoid β] (z : ) (f : MeasureTheory.SimpleFunc α β) (a : α) :
                            (f ^ z) a = f a ^ z
                            Equations
                            Equations
                            Equations
                            Equations
                            Equations
                            Equations
                            Equations
                            Equations
                            instance MeasureTheory.SimpleFunc.instModule {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {K : Type u_5} [Semiring K] [AddCommMonoid β] [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} [MeasurableSpace α] {K : Type u_5} [SMul K β] (k : K) (f : MeasureTheory.SimpleFunc α β) :
                            k f = MeasureTheory.SimpleFunc.map (fun (x : β) => k x) f
                            Equations
                            • MeasureTheory.SimpleFunc.instPreorder = Preorder.mk
                            Equations
                            Equations
                            Equations
                            Equations
                            Equations
                            Equations
                            • MeasureTheory.SimpleFunc.instLattice = Lattice.mk
                            Equations
                            • MeasureTheory.SimpleFunc.instBoundedOrder = BoundedOrder.mk
                            theorem MeasureTheory.SimpleFunc.finset_sup_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [SemilatticeSup β] [OrderBot β] {f : γMeasureTheory.SimpleFunc α β} (s : Finset γ) (a : α) :
                            (s.sup f) a = s.sup fun (c : γ) => (f c) a

                            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
                            Instances For
                              theorem MeasureTheory.SimpleFunc.restrict_of_not_measurable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Zero β] {f : MeasureTheory.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 : MeasureTheory.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 : MeasureTheory.SimpleFunc α β) :
                              f.restrict Set.univ = f
                              @[simp]
                              theorem MeasureTheory.SimpleFunc.restrict_empty {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Zero β] (f : MeasureTheory.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 : MeasureTheory.SimpleFunc α β) (s : Set α) :
                              theorem MeasureTheory.SimpleFunc.restrict_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Zero β] (f : MeasureTheory.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 : MeasureTheory.SimpleFunc α β) {s : Set α} (hs : MeasurableSet s) {t : Set β} (ht : 0t) :
                              (f.restrict s) ⁻¹' t = s f ⁻¹' t
                              theorem MeasureTheory.SimpleFunc.restrict_preimage_singleton {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Zero β] (f : MeasureTheory.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 : MeasureTheory.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 : MeasureTheory.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 : MeasureTheory.SimpleFunc α β} {g : MeasureTheory.SimpleFunc α β} (H : f g) :
                              f.restrict s g.restrict s
                              def MeasureTheory.SimpleFunc.approx {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [SemilatticeSup β] [OrderBot β] [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} [MeasurableSpace α] [SemilatticeSup β] [OrderBot β] [Zero β] [TopologicalSpace β] [OrderClosedTopology β] [MeasurableSpace β] [OpensMeasurableSpace β] {i : β} {f : αβ} {n : } (a : α) (hf : Measurable f) :
                                (MeasureTheory.SimpleFunc.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 : αβ) :
                                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) :
                                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 : ), (MeasureTheory.SimpleFunc.approx i f 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

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

                                  Equations
                                  Instances For
                                    theorem MeasureTheory.SimpleFunc.iSup_eapprox_apply {α : Type u_1} [MeasurableSpace α] (f : αENNReal) (hf : Measurable f) (a : α) :
                                    ⨆ (n : ), (MeasureTheory.SimpleFunc.eapprox f n) a = f a
                                    theorem MeasureTheory.SimpleFunc.eapprox_comp {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace γ] {f : γENNReal} {g : αγ} {n : } (hf : Measurable f) (hg : Measurable g) :
                                    theorem MeasureTheory.SimpleFunc.tsum_eapproxDiff {α : Type u_1} [MeasurableSpace α] (f : αENNReal) (hf : Measurable f) (a : α) :
                                    ∑' (n : ), ((MeasureTheory.SimpleFunc.eapproxDiff f n) a) = f a

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

                                    Equations
                                    • f.lintegral μ = xf.range, x * μ (f ⁻¹' {x})
                                    Instances For
                                      theorem MeasureTheory.SimpleFunc.lintegral_eq_of_subset {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α ENNReal) {s : Finset ENNReal} (hs : ∀ (x : α), f x 0μ (f ⁻¹' {f x}) 0f x s) :
                                      f.lintegral μ = xs, x * μ (f ⁻¹' {x})
                                      theorem MeasureTheory.SimpleFunc.lintegral_eq_of_subset' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α ENNReal) {s : Finset ENNReal} (hs : f.range \ {0} s) :
                                      f.lintegral μ = xs, x * μ (f ⁻¹' {x})
                                      theorem MeasureTheory.SimpleFunc.map_lintegral {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (g : βENNReal) (f : MeasureTheory.SimpleFunc α β) :
                                      (MeasureTheory.SimpleFunc.map g f).lintegral μ = xf.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 α} {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α ENNReal) (g : MeasureTheory.SimpleFunc α ENNReal) :
                                      (f + g).lintegral μ = f.lintegral μ + g.lintegral μ

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

                                      Equations
                                      • MeasureTheory.SimpleFunc.lintegralₗ = { toFun := fun (f : MeasureTheory.SimpleFunc α ENNReal) => { toFun := f.lintegral, map_add' := , map_smul' := }, map_add' := , map_smul' := }
                                      Instances For
                                        theorem MeasureTheory.SimpleFunc.lintegral_add {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α ENNReal) :
                                        f.lintegral (μ + ν) = f.lintegral μ + f.lintegral ν
                                        theorem MeasureTheory.SimpleFunc.lintegral_smul {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α ENNReal) (c : ENNReal) :
                                        f.lintegral (c μ) = c f.lintegral μ
                                        theorem MeasureTheory.SimpleFunc.lintegral_finset_sum {α : Type u_1} {m : MeasurableSpace α} {ι : Type u_5} (f : MeasureTheory.SimpleFunc α ENNReal) (μ : ιMeasureTheory.Measure α) (s : Finset ι) :
                                        f.lintegral (∑ is, μ i) = is, f.lintegral (μ i)
                                        theorem MeasureTheory.SimpleFunc.lintegral_sum {α : Type u_1} {m : MeasurableSpace α} {ι : Type u_5} (f : MeasureTheory.SimpleFunc α ENNReal) (μ : ιMeasureTheory.Measure α) :
                                        f.lintegral (MeasureTheory.Measure.sum μ) = ∑' (i : ι), f.lintegral (μ i)
                                        theorem MeasureTheory.SimpleFunc.restrict_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α ENNReal) {s : Set α} (hs : MeasurableSet s) :
                                        (f.restrict s).lintegral μ = rf.range, r * μ (f ⁻¹' {r} s)
                                        theorem MeasureTheory.SimpleFunc.lintegral_restrict {α : Type u_1} {m : MeasurableSpace α} (f : MeasureTheory.SimpleFunc α ENNReal) (s : Set α) (μ : MeasureTheory.Measure α) :
                                        f.lintegral (μ.restrict s) = yf.range, y * μ (f ⁻¹' {y} s)
                                        theorem MeasureTheory.SimpleFunc.restrict_lintegral_eq_lintegral_restrict {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : MeasureTheory.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 : MeasureTheory.SimpleFunc α ENNReal) {s : ιSet α} (hd : Directed (fun (x1 x2 : Set α) => x1 x2) s) (μ : MeasureTheory.Measure α) :
                                        f.lintegral (μ.restrict (⋃ (i : ι), s i)) = ⨆ (i : ι), f.lintegral (μ.restrict (s i))
                                        theorem MeasureTheory.SimpleFunc.const_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (c : ENNReal) :
                                        (MeasureTheory.SimpleFunc.const α c).lintegral μ = c * μ Set.univ
                                        theorem MeasureTheory.SimpleFunc.const_lintegral_restrict {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (c : ENNReal) (s : Set α) :
                                        (MeasureTheory.SimpleFunc.const α c).lintegral (μ.restrict s) = c * μ s
                                        theorem MeasureTheory.SimpleFunc.restrict_const_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (c : ENNReal) {s : Set α} (hs : MeasurableSet s) :
                                        ((MeasureTheory.SimpleFunc.const α c).restrict s).lintegral μ = c * μ s
                                        theorem MeasureTheory.SimpleFunc.lintegral_mono_fun {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α ENNReal} {g : MeasureTheory.SimpleFunc α ENNReal} (h : f g) :
                                        f.lintegral μ g.lintegral μ
                                        theorem MeasureTheory.SimpleFunc.le_sup_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α ENNReal) (g : MeasureTheory.SimpleFunc α ENNReal) :
                                        f.lintegral μ g.lintegral μ (f g).lintegral μ
                                        theorem MeasureTheory.SimpleFunc.lintegral_mono_measure {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α ENNReal} (h : μ ν) :
                                        f.lintegral μ f.lintegral ν
                                        theorem MeasureTheory.SimpleFunc.lintegral_mono {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α ENNReal} {g : MeasureTheory.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 α} {μ : MeasureTheory.Measure α} [MeasurableSpace β] {f : MeasureTheory.SimpleFunc α ENNReal} {g : MeasureTheory.SimpleFunc β ENNReal} {ν : MeasureTheory.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 α} {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α ENNReal} {g : MeasureTheory.SimpleFunc α ENNReal} (h : f =ᵐ[μ] 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 α} {μ : MeasureTheory.Measure α} {β : Type u_5} [MeasurableSpace β] {μ' : MeasureTheory.Measure β} (f : MeasureTheory.SimpleFunc α ENNReal) (g : MeasureTheory.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 α} {μ : MeasureTheory.Measure α} {β : Type u_5} [MeasurableSpace β] (g : MeasureTheory.SimpleFunc β ENNReal) {f : αβ} (hf : Measurable f) :
                                        g.lintegral (MeasureTheory.Measure.map f μ) = (g.comp f hf).lintegral μ
                                        theorem MeasureTheory.SimpleFunc.support_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Zero β] (f : MeasureTheory.SimpleFunc α β) :
                                        Function.support f = yFinset.filter (fun (y : β) => y 0) f.range, f ⁻¹' {y}

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

                                        Equations
                                        • f.FinMeasSupp μ = (f =ᶠ[μ.cofinite] 0)
                                        Instances For
                                          theorem MeasureTheory.SimpleFunc.finMeasSupp_iff_support {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [Zero β] {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α β} :
                                          f.FinMeasSupp μ μ (Function.support f) <
                                          theorem MeasureTheory.SimpleFunc.finMeasSupp_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [Zero β] {μ : MeasureTheory.Measure α} {f : MeasureTheory.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 β] {μ : MeasureTheory.Measure α} {f : MeasureTheory.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 γ] {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α β} {g : βγ} (hf : f.FinMeasSupp μ) (hg : g 0 = 0) :
                                          (MeasureTheory.SimpleFunc.map g f).FinMeasSupp μ
                                          theorem MeasureTheory.SimpleFunc.FinMeasSupp.of_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} [Zero β] [Zero γ] {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α β} {g : βγ} (h : (MeasureTheory.SimpleFunc.map g f).FinMeasSupp μ) (hg : ∀ (b : β), g b = 0b = 0) :
                                          f.FinMeasSupp μ
                                          theorem MeasureTheory.SimpleFunc.FinMeasSupp.map_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} [Zero β] [Zero γ] {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α β} {g : βγ} (hg : ∀ {b : β}, g b = 0 b = 0) :
                                          (MeasureTheory.SimpleFunc.map g f).FinMeasSupp μ f.FinMeasSupp μ
                                          theorem MeasureTheory.SimpleFunc.FinMeasSupp.pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} [Zero β] [Zero γ] {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α β} {g : MeasureTheory.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 γ] {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α β} [Zero δ] (hf : f.FinMeasSupp μ) {g : MeasureTheory.SimpleFunc α γ} (hg : g.FinMeasSupp μ) {op : βγδ} (H : op 0 0 = 0) :
                                          (MeasureTheory.SimpleFunc.map (Function.uncurry op) (f.pair g)).FinMeasSupp μ
                                          theorem MeasureTheory.SimpleFunc.FinMeasSupp.add {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [AddMonoid β] {f : MeasureTheory.SimpleFunc α β} {g : MeasureTheory.SimpleFunc α β} (hf : f.FinMeasSupp μ) (hg : g.FinMeasSupp μ) :
                                          (f + g).FinMeasSupp μ
                                          theorem MeasureTheory.SimpleFunc.FinMeasSupp.mul {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [MonoidWithZero β] {f : MeasureTheory.SimpleFunc α β} {g : MeasureTheory.SimpleFunc α β} (hf : f.FinMeasSupp μ) (hg : g.FinMeasSupp μ) :
                                          (f * g).FinMeasSupp μ
                                          theorem MeasureTheory.SimpleFunc.FinMeasSupp.lintegral_lt_top {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α ENNReal} (hm : f.FinMeasSupp μ) (hf : ∀ᵐ (a : α) ∂μ, f a ) :
                                          f.lintegral μ <
                                          theorem MeasureTheory.SimpleFunc.FinMeasSupp.of_lintegral_ne_top {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α ENNReal} (h : f.lintegral μ ) :
                                          f.FinMeasSupp μ
                                          theorem MeasureTheory.SimpleFunc.FinMeasSupp.iff_lintegral_lt_top {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α ENNReal} (hf : ∀ᵐ (a : α) ∂μ, f a ) :
                                          f.FinMeasSupp μ f.lintegral μ <
                                          theorem MeasureTheory.SimpleFunc.induction {α : Type u_5} {γ : Type u_6} [MeasurableSpace α] [AddMonoid γ] {P : MeasureTheory.SimpleFunc α γProp} (h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (MeasureTheory.SimpleFunc.piecewise s hs (MeasureTheory.SimpleFunc.const α c) (MeasureTheory.SimpleFunc.const α 0))) (h_add : ∀ ⦃f g : MeasureTheory.SimpleFunc α γ⦄, Disjoint (Function.support f) (Function.support g)P fP gP (f + g)) (f : MeasureTheory.SimpleFunc α γ) :
                                          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 : MeasurableSpace α} [inst : MeasurableSpace E] [inst_1 : AddGroup E] [inst_2 : MeasurableAdd E] {g : αE}, 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 α} [inst : MeasurableSpace E] [inst_1 : AddGroup E] [inst_2 : MeasurableAdd E] {g : αE}, 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} [MeasurableSpace α] {P : (αENNReal)Prop} (h_ind : ∀ (c : ENNReal) ⦃s : Set α⦄, MeasurableSet sP (s.indicator fun (x : α) => c)) (h_add : ∀ ⦃f g : αENNReal⦄, Disjoint (Function.support f) (Function.support g)Measurable fMeasurable gP fP gP (f + g)) (h_iSup : ∀ ⦃f : αENNReal⦄, (∀ (n : ), Measurable (f n))Monotone f(∀ (n : ), P (f n))P fun (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}.