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.measure_compl_le_add_of_le_add {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {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 : Set α} {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
      Equations
      • =
      theorem MeasureTheory.Measure.le_of_add_le_add_left {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν₁ : MeasureTheory.Measure α} {ν₂ : 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.abs_toReal_measure_sub_le_measure_symmDiff' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) (hs' : μ s ) (ht' : μ t ) :
      |(μ s).toReal - (μ t).toReal| (μ (symmDiff s t)).toReal
      theorem MeasureTheory.abs_toReal_measure_sub_le_measure_symmDiff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} [MeasureTheory.IsFiniteMeasure μ] (hs : MeasurableSet s) (ht : MeasurableSet t) :
      |(μ s).toReal - (μ t).toReal| (μ (symmDiff s t)).toReal

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

      • measure_univ : μ Set.univ = 1
      Instances
        theorem MeasureTheory.prob_add_prob_compl {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsProbabilityMeasure μ] (h : MeasurableSet s) :
        μ s + μ s = 1
        @[simp]
        theorem MeasureTheory.one_le_prob_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsProbabilityMeasure μ] :
        1 μ s μ s = 1

        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 .

        theorem MeasureTheory.prob_compl_eq_one_sub {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsProbabilityMeasure μ] (hs : MeasurableSet s) :
        μ s = 1 - μ s

        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.prob_compl_eq_zero_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsProbabilityMeasure μ] (hs : MeasurableSet s) :
        μ s = 0 μ s = 1
        @[simp]
        @[simp]
        theorem MeasureTheory.prob_compl_eq_one_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsProbabilityMeasure μ] (hs : MeasurableSet s) :
        μ s = 1 μ s = 0
        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)) :

        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 : Set.Subsingleton s) (μ : MeasureTheory.Measure α) [MeasureTheory.NoAtoms μ] :
          μ s = 0
          theorem Set.Countable.measure_zero {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (h : Set.Countable s) (μ : MeasureTheory.Measure α) [MeasureTheory.NoAtoms μ] :
          μ s = 0
          theorem Set.Countable.ae_not_mem {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (h : Set.Countable s) (μ : MeasureTheory.Measure α) [MeasureTheory.NoAtoms μ] :
          ∀ᵐ (x : α) ∂μ, xs
          theorem Set.Finite.measure_zero {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (h : Set.Finite s) (μ : 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.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) =ᶠ[MeasureTheory.Measure.ae μ] 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) =ᶠ[MeasureTheory.Measure.ae μ] 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
          Instances For
            theorem MeasureTheory.Measure.FiniteAtFilter.exists_mem_basis {α : Type u_1} {ι : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α} (hμ : MeasureTheory.Measure.FiniteAtFilter μ f) {p : ιProp} {s : ιSet α} (hf : Filter.HasBasis f p s) :
            ∃ (i : ι), p i μ (s i) <
            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

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

                  Equations
                  • =

                  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.

                  Instances

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

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

                          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) ) :
                          Set.Finite {i : ι | ε μ (As i)}

                          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) ) :
                          Set.Finite {i : ι | ε μ (As i)}

                          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 : Set.Infinite s) (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 α}, (∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ)Pairwise (MeasureTheory.AEDisjoint μ on As)μ (⋃ (i : ι), As i) Set.Countable {i : ι | 0 < μ (As i)}

                          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 α}, (∀ (i : ι), MeasurableSet (As i))Pairwise (Disjoint on As)μ (⋃ (i : ι), As i) Set.Countable {i : ι | 0 < μ (As i)}

                          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 α} [inst : MeasureTheory.SFinite μ] {As : ιSet α}, (∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ)Pairwise (MeasureTheory.AEDisjoint μ on As)Set.Countable {i : ι | 0 < μ (As i)}

                          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 α} [inst : MeasureTheory.SFinite μ] {As : ιSet α}, (∀ (i : ι), MeasurableSet (As i))Pairwise (Disjoint on As)Set.Countable {i : ι | 0 < μ (As i)}

                          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 α} [inst : MeasureTheory.SFinite μ] [inst : MeasurableSpace β] [inst_1 : MeasurableSingletonClass β] {g : αβ}, MeasureTheory.NullMeasurable g μSet.Countable {t : β | 0 < μ {a : α | g a = t}}
                          theorem MeasureTheory.Measure.countable_meas_level_set_pos {α : Type u_5} {β : Type u_6} :
                          ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SFinite μ] [inst : MeasurableSpace β] [inst_1 : MeasurableSingletonClass β] {g : αβ}, Measurable gSet.Countable {t : β | 0 < μ {a : α | g a = t}}
                          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) ) :
                          theorem MeasureTheory.Measure.measure_toMeasurable_inter_of_sFinite {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] {s : Set α} (hs : MeasurableSet s) (t : Set α) :
                          μ (MeasureTheory.toMeasurable μ t s) = μ (t 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.

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

                          Equations
                          Instances For

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

                            Equations
                            Instances For

                              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 α} {ν : MeasureTheory.Measure α} {C : Set (Set α)} (hA : m0 = MeasurableSpace.generateFrom C) (hC : IsPiSystem C) (h : MeasureTheory.Measure.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.sigmaFinite_of_countable {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {S : Set (Set α)} (hc : Set.Countable S) (hμ : sS, μ s < ) (hU : ⋃₀ S = Set.univ) :

                              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.Measure α) (ν₂ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] :
                                μ + ν₁ = μ + ν₂ ν₁ = ν₂
                                @[simp]
                                theorem MeasureTheory.Measure.add_left_inj {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν₁ : MeasureTheory.Measure α) (ν₂ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] :
                                ν₁ + μ = ν₂ + μ ν₁ = ν₂

                                Every finite measure is σ-finite.

                                Equations
                                • =
                                Equations
                                • =
                                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 : α) ∂MeasureTheory.Measure.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 : α) ∂MeasureTheory.Measure.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.

                                Instances

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

                                  Instances
                                    theorem IsCompact.measure_lt_top {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasureOnCompacts μ] ⦃K : Set α (hK : IsCompact K) :
                                    μ K <

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

                                    theorem IsCompact.measure_ne_top {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasureOnCompacts μ] ⦃K : Set α (hK : IsCompact K) :
                                    μ K

                                    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.

                                    Equations
                                    • =
                                    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)
                                    theorem MeasureTheory.null_of_locally_null {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [SecondCountableTopology α] (s : Set α) (hs : xs, ∃ u ∈ nhdsWithin 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_mem_forall_mem_nhdsWithin_pos_measure {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [SecondCountableTopology α] {s : Set α} (hs : μ s 0) :
                                    ∃ x ∈ s, tnhdsWithin x s, 0 < μ t
                                    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.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 α} {ν : 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).

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

                                    Equations
                                    Instances For
                                      theorem IsCompact.exists_open_superset_measure_lt_top' {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (h : IsCompact s) (hμ : xs, MeasureTheory.Measure.FiniteAtFilter μ (nhds x)) :
                                      ∃ U ⊇ s, 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, MeasureTheory.Measure.FiniteAtFilter μ (nhdsWithin x s)) :
                                      μ s <
                                      theorem IsCompact.measure_zero_of_nhdsWithin {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : IsCompact s) :
                                      (as, ∃ t ∈ nhdsWithin a s, μ t = 0)μ s = 0

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

                                      Equations
                                      Instances For

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

                                        Equations
                                        Instances For
                                          @[irreducible]

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

                                          Equations
                                          Instances For
                                            theorem measure_Icc_lt_top {α : Type u_1} [Preorder α] [TopologicalSpace α] [CompactIccSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {a : α} {b : α} :
                                            μ (Set.Icc a b) <
                                            theorem measure_Ico_lt_top {α : Type u_1} [Preorder α] [TopologicalSpace α] [CompactIccSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {a : α} {b : α} :
                                            μ (Set.Ico a b) <
                                            theorem measure_Ioc_lt_top {α : Type u_1} [Preorder α] [TopologicalSpace α] [CompactIccSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {a : α} {b : α} :
                                            μ (Set.Ioc a b) <
                                            theorem measure_Ioo_lt_top {α : Type u_1} [Preorder α] [TopologicalSpace α] [CompactIccSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {a : α} {b : α} :
                                            μ (Set.Ioo a b) <