Documentation

Mathlib.MeasureTheory.Measure.Typeclasses

Classes of measures #

We introduce the following typeclasses for measures:

A measure μ is called finite if μ univ < ∞.

  • measure_univ_lt_top : μ Set.univ <
Instances
    theorem MeasureTheory.Restrict.isFiniteMeasure {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (μ : MeasureTheory.Measure α) [hs : Fact (μ s < )] :
    @[simp]
    theorem MeasureTheory.measure_compl_le_add_of_le_add {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α} [MeasureTheory.IsFiniteMeasure μ] (hs : MeasurableSet s) (ht : MeasurableSet t) {ε : ENNReal} (h : μ s μ t + ε) :
    μ t μ s + ε
    theorem MeasureTheory.measure_compl_le_add_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α} [MeasureTheory.IsFiniteMeasure μ] (hs : MeasurableSet s) (ht : MeasurableSet t) {ε : ENNReal} :
    μ s μ t + ε μ t μ s + ε

    The measure of the whole space with respect to a finite measure, considered as ℝ≥0.

    Equations
    Instances For
      theorem MeasureTheory.Measure.le_of_add_le_add_left {α : Type u_1} {m0 : MeasurableSpace α} {μ ν₁ ν₂ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] (A2 : μ + ν₁ μ + ν₂) :
      ν₁ ν₂

      le_of_add_le_add_left is normally applicable to OrderedCancelAddCommMonoid, but it holds for measures with the additional assumption that μ is finite.

      theorem MeasureTheory.summable_measure_toReal {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [hμ : MeasureTheory.IsFiniteMeasure μ] {f : Set α} (hf₁ : ∀ (i : ), MeasurableSet (f i)) (hf₂ : Pairwise (Disjoint on f)) :
      Summable fun (x : ) => (μ (f x)).toReal
      theorem MeasureTheory.ae_iff_measure_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {p : αProp} (hp : MeasureTheory.NullMeasurableSet {a : α | p a} μ) :
      (∀ᵐ (a : α) ∂μ, p a) μ {a : α | p a} = μ Set.univ
      theorem MeasureTheory.ae_mem_iff_measure_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) :
      (∀ᵐ (a : α) ∂μ, a s) μ s = μ Set.univ
      theorem MeasureTheory.tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint {X : Type u_5} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] {Es : Set X} (Es_mble : ∀ (i : ), MeasureTheory.NullMeasurableSet (Es i) μ) (Es_disj : Pairwise fun (n m : ) => Disjoint (Es n) (Es m)) :
      Filter.Tendsto (μ fun (n : ) => ⋃ (i : ), ⋃ (_ : i n), Es i) Filter.atTop (nhds 0)
      theorem MeasureTheory.abs_toReal_measure_sub_le_measure_symmDiff' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) (ht : MeasureTheory.NullMeasurableSet t μ) (hs' : μ s ) (ht' : μ t ) :
      |(μ s).toReal - (μ t).toReal| (μ (symmDiff s t)).toReal
      theorem MeasureTheory.instIsFiniteMeasureSumMeasure {α : Type u_1} {ι : Type u_4} {m0 : MeasurableSpace α} {s : Finset ι} {μ : ιMeasureTheory.Measure α} [∀ (i : ι), MeasureTheory.IsFiniteMeasure (μ i)] :
      MeasureTheory.IsFiniteMeasure (∑ is, μ i)

      A measure μ is zero or a probability measure if μ univ = 0 or μ univ = 1. This class of measures appears naturally when conditioning on events, and many results which are true for probability measures hold more generally over this class.

      • measure_univ : μ Set.univ = 0 μ Set.univ = 1
      Instances
        @[simp]

        A measure μ is called a probability measure if μ univ = 1.

        • measure_univ : μ Set.univ = 1
        Instances

          Note that this is not quite as useful as it looks because the measure takes values in ℝ≥0∞. Thus the subtraction appearing is the truncated subtraction of ℝ≥0∞, rather than the better-behaved subtraction of .

          Note that this is not quite as useful as it looks because the measure takes values in ℝ≥0∞. Thus the subtraction appearing is the truncated subtraction of ℝ≥0∞, rather than the better-behaved subtraction of .

          @[simp]
          @[simp]
          theorem MeasureTheory.ae_iff_prob_eq_one {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {p : αProp} (hp : Measurable p) :
          (∀ᵐ (a : α) ∂μ, p a) μ {a : α | p a} = 1
          theorem MeasureTheory.isProbabilityMeasure_comap {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {f : βα} (hf : Function.Injective f) (hf' : ∀ᵐ (a : α) ∂μ, a Set.range f) (hf'' : ∀ (s : Set β), MeasurableSet sMeasurableSet (f '' s)) :
          theorem MeasureTheory.prob_compl_lt_one_sub_of_lt_prob {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsZeroOrProbabilityMeasure μ] {p : ENNReal} (hμs : p < μ s) (s_mble : MeasurableSet s) :
          μ s < 1 - p

          Measure μ has no atoms if the measure of each singleton is zero.

          NB: Wikipedia assumes that for any measurable set s with positive μ-measure, there exists a measurable t ⊆ s such that 0 < μ t < μ s. While this implies μ {x} = 0, the converse is not true.

          • measure_singleton : ∀ (x : α), μ {x} = 0
          Instances
            theorem Set.Subsingleton.measure_zero {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (hs : s.Subsingleton) (μ : MeasureTheory.Measure α) [MeasureTheory.NoAtoms μ] :
            μ s = 0
            theorem MeasureTheory.Measure.restrict_singleton' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] {a : α} :
            μ.restrict {a} = 0
            theorem Set.Countable.measure_zero {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (h : s.Countable) (μ : MeasureTheory.Measure α) [MeasureTheory.NoAtoms μ] :
            μ s = 0
            theorem Set.Countable.ae_not_mem {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (h : s.Countable) (μ : MeasureTheory.Measure α) [MeasureTheory.NoAtoms μ] :
            ∀ᵐ (x : α) ∂μ, xs
            theorem Set.Countable.measure_restrict_compl {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (h : s.Countable) (μ : MeasureTheory.Measure α) [MeasureTheory.NoAtoms μ] :
            μ.restrict s = μ
            @[simp]
            theorem MeasureTheory.restrict_compl_singleton {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] (a : α) :
            μ.restrict {a} = μ
            theorem Set.Finite.measure_zero {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (h : s.Finite) (μ : MeasureTheory.Measure α) [MeasureTheory.NoAtoms μ] :
            μ s = 0
            theorem Finset.measure_zero {α : Type u_1} {m0 : MeasurableSpace α} (s : Finset α) (μ : MeasureTheory.Measure α) [MeasureTheory.NoAtoms μ] :
            μ s = 0
            theorem MeasureTheory.insert_ae_eq_self {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] (a : α) (s : Set α) :
            insert a s =ᵐ[μ] s
            theorem MeasureTheory.restrict_Iio_eq_restrict_Iic {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} :
            μ.restrict (Set.Iio a) = μ.restrict (Set.Iic a)
            theorem MeasureTheory.restrict_Ioi_eq_restrict_Ici {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} :
            μ.restrict (Set.Ioi a) = μ.restrict (Set.Ici a)
            theorem MeasureTheory.restrict_Ioo_eq_restrict_Ioc {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a b : α} :
            μ.restrict (Set.Ioo a b) = μ.restrict (Set.Ioc a b)
            theorem MeasureTheory.restrict_Ioc_eq_restrict_Icc {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a b : α} :
            μ.restrict (Set.Ioc a b) = μ.restrict (Set.Icc a b)
            theorem MeasureTheory.restrict_Ioo_eq_restrict_Ico {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a b : α} :
            μ.restrict (Set.Ioo a b) = μ.restrict (Set.Ico a b)
            theorem MeasureTheory.restrict_Ioo_eq_restrict_Icc {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a b : α} :
            μ.restrict (Set.Ioo a b) = μ.restrict (Set.Icc a b)
            theorem MeasureTheory.restrict_Ico_eq_restrict_Icc {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a b : α} :
            μ.restrict (Set.Ico a b) = μ.restrict (Set.Icc a b)
            theorem MeasureTheory.restrict_Ico_eq_restrict_Ioc {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a b : α} :
            μ.restrict (Set.Ico a b) = μ.restrict (Set.Ioc a b)
            theorem MeasureTheory.ite_ae_eq_of_measure_zero {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {γ : Type u_5} (f g : αγ) (s : Set α) [DecidablePred fun (x : α) => x s] (hs_zero : μ s = 0) :
            (fun (x : α) => if x s then f x else g x) =ᵐ[μ] g
            theorem MeasureTheory.ite_ae_eq_of_measure_compl_zero {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {γ : Type u_5} (f g : αγ) (s : Set α) [DecidablePred fun (x : α) => x s] (hs_zero : μ s = 0) :
            (fun (x : α) => if x s then f x else g x) =ᵐ[μ] f

            A measure is called finite at filter f if it is finite at some set s ∈ f. Equivalently, it is eventually finite at s in f.small_sets.

            Equations
            • μ.FiniteAtFilter f = sf, μ s <
            Instances For
              theorem MeasureTheory.Measure.FiniteAtFilter.exists_mem_basis {α : Type u_1} {ι : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α} (hμ : μ.FiniteAtFilter f) {p : ιProp} {s : ιSet α} (hf : f.HasBasis p s) :
              ∃ (i : ι), p i μ (s i) <
              theorem MeasureTheory.Measure.finiteAtBot {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) :
              μ.FiniteAtFilter
              structure MeasureTheory.Measure.FiniteSpanningSetsIn {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (C : Set (Set α)) :
              Type u_1

              μ has finite spanning sets in C if there is a countable sequence of sets in C that have finite measures. This structure is a type, which is useful if we want to record extra properties about the sets, such as that they are monotone. SigmaFinite is defined in terms of this: μ is σ-finite if there exists a sequence of finite spanning sets in the collection of all measurable sets.

              • set : Set α
              • set_mem : ∀ (i : ), self.set i C
              • finite : ∀ (i : ), μ (self.set i) <
              • spanning : ⋃ (i : ), self.set i = Set.univ
              Instances For

                A measure is called s-finite if it is a countable sum of finite measures.

                Instances

                  A sequence of finite measures such that μ = sum (sfiniteSeq μ) (see sum_sfiniteSeq).

                  Equations
                  Instances For
                    @[deprecated MeasureTheory.sfiniteSeq]

                    Alias of MeasureTheory.sfiniteSeq.


                    A sequence of finite measures such that μ = sum (sfiniteSeq μ) (see sum_sfiniteSeq).

                    Equations
                    Instances For
                      @[deprecated MeasureTheory.sum_sfiniteSeq]

                      Alias of MeasureTheory.sum_sfiniteSeq.

                      @[deprecated MeasureTheory.sfiniteSeq_le]

                      Alias of MeasureTheory.sfiniteSeq_le.

                      @[simp]
                      @[deprecated MeasureTheory.sfiniteSeq_zero]

                      Alias of MeasureTheory.sfiniteSeq_zero.

                      A countable sum of finite measures is s-finite. This lemma is superseded by the instance below.

                      theorem MeasureTheory.exists_isFiniteMeasure_absolutelyContinuous {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] :
                      ∃ (ν : MeasureTheory.Measure α), MeasureTheory.IsFiniteMeasure ν μ.AbsolutelyContinuous ν ν.AbsolutelyContinuous μ

                      For an s-finite measure μ, there exists a finite measure ν such that each of μ and ν is absolutely continuous with respect to the other.

                      @[deprecated MeasureTheory.exists_isFiniteMeasure_absolutelyContinuous]

                      A measure μ is called σ-finite if there is a countable collection of sets { A i | i ∈ ℕ } such that μ (A i) < ∞ and ⋃ i, A i = s.

                      • out' : Nonempty (μ.FiniteSpanningSetsIn Set.univ)
                      Instances
                        theorem MeasureTheory.sigmaFinite_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} :
                        MeasureTheory.SigmaFinite μ Nonempty (μ.FiniteSpanningSetsIn Set.univ)
                        theorem MeasureTheory.SigmaFinite.out {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (h : MeasureTheory.SigmaFinite μ) :
                        Nonempty (μ.FiniteSpanningSetsIn Set.univ)
                        def MeasureTheory.Measure.toFiniteSpanningSetsIn {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [h : MeasureTheory.SigmaFinite μ] :
                        μ.FiniteSpanningSetsIn {s : Set α | MeasurableSet s}

                        If μ is σ-finite it has finite spanning sets in the collection of all measurable sets.

                        Equations
                        • μ.toFiniteSpanningSetsIn = { set := fun (n : ) => MeasureTheory.toMeasurable μ (.some.set n), set_mem := , finite := , spanning := }
                        Instances For

                          A noncomputable way to get a monotone collection of sets that span univ and have finite measure using Classical.choose. This definition satisfies monotonicity in addition to all other properties in SigmaFinite.

                          Equations
                          Instances For
                            @[deprecated MeasureTheory.measurableSet_spanningSets]

                            Alias of MeasureTheory.measurableSet_spanningSets.

                            noncomputable def MeasureTheory.spanningSetsIndex {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (x : α) :

                            spanningSetsIndex μ x is the least n : ℕ such that x ∈ spanningSets μ n.

                            Equations
                            Instances For
                              theorem MeasureTheory.eventually_mem_spanningSets {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (x : α) :
                              ∀ᶠ (n : ) in Filter.atTop, x MeasureTheory.spanningSets μ n

                              A set in a σ-finite space has zero measure if and only if its intersection with all members of the countable family of finite measure spanning sets has zero measure.

                              A set in a σ-finite space has positive measure if and only if its intersection with some member of the countable family of finite measure spanning sets has positive measure.

                              theorem MeasureTheory.Measure.finite_const_le_meas_of_disjoint_iUnion₀ {α : Type u_1} {ι : Type u_5} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {ε : ENNReal} (ε_pos : 0 < ε) {As : ιSet α} (As_mble : ∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ) (As_disj : Pairwise (MeasureTheory.AEDisjoint μ on As)) (Union_As_finite : μ (⋃ (i : ι), As i) ) :
                              {i : ι | ε μ (As i)}.Finite

                              If the union of a.e.-disjoint null-measurable sets has finite measure, then there are only finitely many members of the union whose measure exceeds any given positive number.

                              theorem MeasureTheory.Measure.finite_const_le_meas_of_disjoint_iUnion {α : Type u_1} {ι : Type u_5} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {ε : ENNReal} (ε_pos : 0 < ε) {As : ιSet α} (As_mble : ∀ (i : ι), MeasurableSet (As i)) (As_disj : Pairwise (Disjoint on As)) (Union_As_finite : μ (⋃ (i : ι), As i) ) :
                              {i : ι | ε μ (As i)}.Finite

                              If the union of disjoint measurable sets has finite measure, then there are only finitely many members of the union whose measure exceeds any given positive number.

                              theorem Set.Infinite.meas_eq_top {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSingletonClass α] {s : Set α} (hs : s.Infinite) (h' : ∃ (ε : ENNReal), ε 0 xs, ε μ {x}) :
                              μ s =

                              If all elements of an infinite set have measure uniformly separated from zero, then the set has infinite measure.

                              theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀ {α : Type u_1} {ι : Type u_5} {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) {As : ιSet α} (As_mble : ∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ) (As_disj : Pairwise (MeasureTheory.AEDisjoint μ on As)) (Union_As_finite : μ (⋃ (i : ι), As i) ) :
                              {i : ι | 0 < μ (As i)}.Countable

                              If the union of a.e.-disjoint null-measurable sets has finite measure, then there are only countably many members of the union whose measure is positive.

                              theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top {α : Type u_1} {ι : Type u_5} {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) {As : ιSet α} (As_mble : ∀ (i : ι), MeasurableSet (As i)) (As_disj : Pairwise (Disjoint on As)) (Union_As_finite : μ (⋃ (i : ι), As i) ) :
                              {i : ι | 0 < μ (As i)}.Countable

                              If the union of disjoint measurable sets has finite measure, then there are only countably many members of the union whose measure is positive.

                              theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_iUnion₀ {α : Type u_1} {ι : Type u_5} {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] {As : ιSet α} (As_mble : ∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ) (As_disj : Pairwise (MeasureTheory.AEDisjoint μ on As)) :
                              {i : ι | 0 < μ (As i)}.Countable

                              In an s-finite space, among disjoint null-measurable sets, only countably many can have positive measure.

                              theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_iUnion {α : Type u_1} {ι : Type u_5} {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] {As : ιSet α} (As_mble : ∀ (i : ι), MeasurableSet (As i)) (As_disj : Pairwise (Disjoint on As)) :
                              {i : ι | 0 < μ (As i)}.Countable

                              In an s-finite space, among disjoint measurable sets, only countably many can have positive measure.

                              theorem MeasureTheory.Measure.countable_meas_level_set_pos₀ {α : Type u_5} {β : Type u_6} {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] [MeasurableSpace β] [MeasurableSingletonClass β] {g : αβ} (g_mble : MeasureTheory.NullMeasurable g μ) :
                              {t : β | 0 < μ {a : α | g a = t}}.Countable
                              theorem MeasureTheory.Measure.countable_meas_level_set_pos {α : Type u_5} {β : Type u_6} {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] [MeasurableSpace β] [MeasurableSingletonClass β] {g : αβ} (g_mble : Measurable g) :
                              {t : β | 0 < μ {a : α | g a = t}}.Countable
                              theorem MeasureTheory.Measure.measure_toMeasurable_inter_of_sum {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) {t : Set α} {m : MeasureTheory.Measure α} (hv : ∀ (n : ), (m n) t ) (hμ : μ = MeasureTheory.Measure.sum m) :
                              μ (MeasureTheory.toMeasurable μ t s) = μ (t s)

                              If a measure μ is the sum of a countable family mₙ, and a set t has finite measure for each mₙ, then its measurable superset toMeasurable μ t (which has the same measure as t) satisfies, for any measurable set s, the equality μ (toMeasurable μ t ∩ s) = μ (t ∩ s).

                              theorem MeasureTheory.Measure.measure_toMeasurable_inter_of_cover {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) {t : Set α} {v : Set α} (hv : t ⋃ (n : ), v n) (h'v : ∀ (n : ), μ (t v n) ) :
                              μ (MeasureTheory.toMeasurable μ t s) = μ (t s)

                              If a set t is covered by a countable family of finite measure sets, then its measurable superset toMeasurable μ t (which has the same measure as t) satisfies, for any measurable set s, the equality μ (toMeasurable μ t ∩ s) = μ (t ∩ s).

                              theorem MeasureTheory.Measure.restrict_toMeasurable_of_cover {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {v : Set α} (hv : s ⋃ (n : ), v n) (h'v : ∀ (n : ), μ (s v n) ) :
                              μ.restrict (MeasureTheory.toMeasurable μ s) = μ.restrict s

                              The measurable superset toMeasurable μ t of t (which has the same measure as t) satisfies, for any measurable set s, the equality μ (toMeasurable μ t ∩ s) = μ (t ∩ s). This only holds when μ is s-finite -- for example for σ-finite measures. For a version without this assumption (but requiring that t has finite measure), see measure_toMeasurable_inter.

                              @[simp]
                              theorem MeasureTheory.Measure.exists_subset_measure_lt_top {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.SigmaFinite μ] {r : ENNReal} (hs : MeasurableSet s) (h's : r < μ s) :
                              ∃ (t : Set α), MeasurableSet t t s r < μ t μ t <

                              In a σ-finite space, any measurable set of measure > r contains a measurable subset of finite measure > r.

                              def MeasureTheory.Measure.FiniteSpanningSetsIn.mono' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {C D : Set (Set α)} (h : μ.FiniteSpanningSetsIn C) (hC : C {s : Set α | μ s < } D) :
                              μ.FiniteSpanningSetsIn D

                              If μ has finite spanning sets in C and C ∩ {s | μ s < ∞} ⊆ D then μ has finite spanning sets in D.

                              Equations
                              • h.mono' hC = { set := h.set, set_mem := , finite := , spanning := }
                              Instances For
                                def MeasureTheory.Measure.FiniteSpanningSetsIn.mono {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {C D : Set (Set α)} (h : μ.FiniteSpanningSetsIn C) (hC : C D) :
                                μ.FiniteSpanningSetsIn D

                                If μ has finite spanning sets in C and C ⊆ D then μ has finite spanning sets in D.

                                Equations
                                • h.mono hC = h.mono'
                                Instances For
                                  theorem MeasureTheory.Measure.FiniteSpanningSetsIn.sigmaFinite {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {C : Set (Set α)} (h : μ.FiniteSpanningSetsIn C) :

                                  If μ has finite spanning sets in the collection of measurable sets C, then μ is σ-finite.

                                  theorem MeasureTheory.Measure.FiniteSpanningSetsIn.ext {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {C : Set (Set α)} (hA : m0 = MeasurableSpace.generateFrom C) (hC : IsPiSystem C) (h : μ.FiniteSpanningSetsIn C) (h_eq : sC, μ s = ν s) :
                                  μ = ν

                                  An extensionality for measures. It is ext_of_generateFrom_of_iUnion formulated in terms of FiniteSpanningSetsIn.

                                  theorem MeasureTheory.Measure.FiniteSpanningSetsIn.isCountablySpanning {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {C : Set (Set α)} (h : μ.FiniteSpanningSetsIn C) :
                                  theorem MeasureTheory.Measure.sigmaFinite_of_countable {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {S : Set (Set α)} (hc : S.Countable) (hμ : sS, μ s < ) (hU : ⋃₀ S = Set.univ) :
                                  def MeasureTheory.Measure.FiniteSpanningSetsIn.ofLE {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (h : ν μ) {C : Set (Set α)} (S : μ.FiniteSpanningSetsIn C) :
                                  ν.FiniteSpanningSetsIn C

                                  Given measures μ, ν where ν ≤ μ, FiniteSpanningSetsIn.ofLe provides the induced FiniteSpanningSet with respect to ν from a FiniteSpanningSet with respect to μ.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem MeasureTheory.Measure.add_right_inj {α : Type u_1} {m0 : MeasurableSpace α} (μ ν₁ ν₂ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] :
                                    μ + ν₁ = μ + ν₂ ν₁ = ν₂
                                    @[simp]
                                    theorem MeasureTheory.Measure.add_left_inj {α : Type u_1} {m0 : MeasurableSpace α} (μ ν₁ ν₂ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] :
                                    ν₁ + μ = ν₂ + μ ν₁ = ν₂
                                    theorem MeasureTheory.instSigmaFiniteRestrictUnionSet {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α} [MeasureTheory.SigmaFinite (μ.restrict s)] [MeasureTheory.SigmaFinite (μ.restrict t)] :
                                    MeasureTheory.SigmaFinite (μ.restrict (s t))
                                    theorem MeasureTheory.ae_of_forall_measure_lt_top_ae_restrict' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (P : αProp) (h : ∀ (s : Set α), MeasurableSet sμ s < ν s < ∀ᵐ (x : α) ∂μ.restrict s, P x) :
                                    ∀ᵐ (x : α) ∂μ, P x

                                    Similar to ae_of_forall_measure_lt_top_ae_restrict, but where you additionally get the hypothesis that another σ-finite measure has finite values on s.

                                    theorem MeasureTheory.ae_of_forall_measure_lt_top_ae_restrict {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] (P : αProp) (h : ∀ (s : Set α), MeasurableSet sμ s < ∀ᵐ (x : α) ∂μ.restrict s, P x) :
                                    ∀ᵐ (x : α) ∂μ, P x

                                    To prove something for almost all x w.r.t. a σ-finite measure, it is sufficient to show that this holds almost everywhere in sets where the measure has finite value.

                                    A measure is called locally finite if it is finite in some neighborhood of each point.

                                    • finiteAtNhds : ∀ (x : α), μ.FiniteAtFilter (nhds x)
                                    Instances

                                      A measure μ is finite on compacts if any compact set K satisfies μ K < ∞.

                                      Instances

                                        A compact subset has finite measure for a measure which is finite on compacts.

                                        A compact subset has finite measure for a measure which is finite on compacts.

                                        A bounded subset has finite measure for a measure which is finite on compact sets, in a proper space.

                                        A measure which is finite on compact sets in a locally compact space is locally finite.

                                        theorem MeasureTheory.exists_pos_measure_of_cover {α : Type u_1} {ι : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {U : ιSet α} (hU : ⋃ (i : ι), U i = Set.univ) (hμ : μ 0) :
                                        ∃ (i : ι), 0 < μ (U i)
                                        theorem MeasureTheory.exists_pos_preimage_ball {α : Type u_1} {δ : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PseudoMetricSpace δ] (f : αδ) (x : δ) (hμ : μ 0) :
                                        ∃ (n : ), 0 < μ (f ⁻¹' Metric.ball x n)
                                        theorem MeasureTheory.exists_pos_ball {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PseudoMetricSpace α] (x : α) (hμ : μ 0) :
                                        ∃ (n : ), 0 < μ (Metric.ball x n)
                                        @[deprecated MeasureTheory.measure_null_of_locally_null]
                                        theorem MeasureTheory.null_of_locally_null {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} [TopologicalSpace α] [SecondCountableTopology α] (s : Set α) (hs : xs, unhdsWithin x s, μ u = 0) :
                                        μ s = 0

                                        If a set has zero measure in a neighborhood of each of its points, then it has zero measure in a second-countable space.

                                        theorem MeasureTheory.exists_ne_forall_mem_nhds_pos_measure_preimage {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [TopologicalSpace β] [T1Space β] [SecondCountableTopology β] [Nonempty β] {f : αβ} (h : ∀ (b : β), ∃ᵐ (x : α) ∂μ, f x b) :
                                        ∃ (a : β) (b : β), a b (∀ snhds a, 0 < μ (f ⁻¹' s)) tnhds b, 0 < μ (f ⁻¹' t)
                                        theorem MeasureTheory.ext_on_measurableSpace_of_generate_finite {α : Type u_5} (m₀ : MeasurableSpace α) {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] (C : Set (Set α)) (hμν : sC, μ s = ν s) {m : MeasurableSpace α} (h : m m₀) (hA : m = MeasurableSpace.generateFrom C) (hC : IsPiSystem C) (h_univ : μ Set.univ = ν Set.univ) {s : Set α} (hs : MeasurableSet s) :
                                        μ s = ν s

                                        If two finite measures give the same mass to the whole space and coincide on a π-system made of measurable sets, then they coincide on all sets in the σ-algebra generated by the π-system.

                                        theorem MeasureTheory.ext_of_generate_finite {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (C : Set (Set α)) (hA : m0 = MeasurableSpace.generateFrom C) (hC : IsPiSystem C) [MeasureTheory.IsFiniteMeasure μ] (hμν : sC, μ s = ν s) (h_univ : μ Set.univ = ν Set.univ) :
                                        μ = ν

                                        Two finite measures are equal if they are equal on the π-system generating the σ-algebra (and univ).

                                        def MeasureTheory.Measure.FiniteSpanningSetsIn.disjointed {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (S : μ.FiniteSpanningSetsIn {s : Set α | MeasurableSet s}) :
                                        μ.FiniteSpanningSetsIn {s : Set α | MeasurableSet s}

                                        Given S : μ.FiniteSpanningSetsIn {s | MeasurableSet s}, FiniteSpanningSetsIn.disjointed provides a FiniteSpanningSetsIn {s | MeasurableSet s} such that its underlying sets are pairwise disjoint.

                                        Equations
                                        • S.disjointed = { set := disjointed S.set, set_mem := , finite := , spanning := }
                                        Instances For
                                          theorem MeasureTheory.Measure.FiniteSpanningSetsIn.disjointed_set_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (S : μ.FiniteSpanningSetsIn {s : Set α | MeasurableSet s}) :
                                          S.disjointed.set = disjointed S.set
                                          theorem MeasureTheory.Measure.exists_eq_disjoint_finiteSpanningSetsIn {α : Type u_1} {m0 : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] :
                                          ∃ (S : μ.FiniteSpanningSetsIn {s : Set α | MeasurableSet s}) (T : ν.FiniteSpanningSetsIn {s : Set α | MeasurableSet s}), S.set = T.set Pairwise (Disjoint on S.set)
                                          theorem MeasureTheory.Measure.FiniteAtFilter.filter_mono {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : Filter α} (h : f g) :
                                          μ.FiniteAtFilter gμ.FiniteAtFilter f
                                          theorem MeasureTheory.Measure.FiniteAtFilter.inf_of_left {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : Filter α} (h : μ.FiniteAtFilter f) :
                                          μ.FiniteAtFilter (f g)
                                          theorem MeasureTheory.Measure.FiniteAtFilter.inf_of_right {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : Filter α} (h : μ.FiniteAtFilter g) :
                                          μ.FiniteAtFilter (f g)
                                          @[simp]
                                          theorem MeasureTheory.Measure.FiniteAtFilter.inf_ae_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α} :
                                          μ.FiniteAtFilter (f MeasureTheory.ae μ) μ.FiniteAtFilter f
                                          theorem MeasureTheory.Measure.FiniteAtFilter.of_inf_ae {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α} :
                                          μ.FiniteAtFilter (f MeasureTheory.ae μ)μ.FiniteAtFilter f

                                          Alias of the forward direction of MeasureTheory.Measure.FiniteAtFilter.inf_ae_iff.

                                          theorem MeasureTheory.Measure.FiniteAtFilter.filter_mono_ae {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : Filter α} (h : f MeasureTheory.ae μ g) (hg : μ.FiniteAtFilter g) :
                                          μ.FiniteAtFilter f
                                          theorem MeasureTheory.Measure.FiniteAtFilter.measure_mono {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {f : Filter α} (h : μ ν) :
                                          ν.FiniteAtFilter fμ.FiniteAtFilter f
                                          theorem MeasureTheory.Measure.FiniteAtFilter.mono {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {f g : Filter α} (hf : f g) (hμ : μ ν) :
                                          ν.FiniteAtFilter gμ.FiniteAtFilter f
                                          theorem MeasureTheory.Measure.FiniteAtFilter.eventually {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α} (h : μ.FiniteAtFilter f) :
                                          ∀ᶠ (s : Set α) in f.smallSets, μ s <
                                          theorem MeasureTheory.Measure.FiniteAtFilter.filterSup {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : Filter α} :
                                          μ.FiniteAtFilter fμ.FiniteAtFilter gμ.FiniteAtFilter (f g)
                                          @[simp]
                                          theorem MeasureTheory.Measure.finiteAt_principal {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} :
                                          μ.FiniteAtFilter (Filter.principal s) μ s <
                                          theorem IsCompact.exists_open_superset_measure_lt_top' {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (h : IsCompact s) (hμ : xs, μ.FiniteAtFilter (nhds x)) :
                                          Us, IsOpen U μ U <

                                          If s is a compact set and μ is finite at 𝓝 x for every x ∈ s, then s admits an open superset of finite measure.

                                          If s is a compact set and μ is a locally finite measure, then s admits an open superset of finite measure.

                                          theorem IsCompact.measure_lt_top_of_nhdsWithin {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (h : IsCompact s) (hμ : xs, μ.FiniteAtFilter (nhdsWithin x s)) :
                                          μ s <
                                          theorem IsCompact.measure_zero_of_nhdsWithin {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : IsCompact s) :
                                          (∀ as, tnhdsWithin a s, μ t = 0)μ s = 0

                                          Compact covering of a σ-compact topological space as MeasureTheory.Measure.FiniteSpanningSetsIn.

                                          Equations
                                          • μ.finiteSpanningSetsInCompact = { set := compactCovering α, set_mem := , finite := , spanning := }
                                          Instances For

                                            A locally finite measure on a σ-compact topological space admits a finite spanning sequence of open sets.

                                            Equations
                                            • μ.finiteSpanningSetsInOpen = { set := fun (n : ) => .choose, set_mem := , finite := , spanning := }
                                            Instances For
                                              @[irreducible]

                                              A locally finite measure on a second countable topological space admits a finite spanning sequence of open sets.

                                              Equations
                                              • μ.finiteSpanningSetsInOpen' = let_fun H := ; H.some
                                              Instances For