Documentation

Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Classes for finite measures #

We introduce the following typeclasses for measures:

class MeasureTheory.IsFiniteMeasure {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) :

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

Instances
    theorem MeasureTheory.isFiniteMeasure_restrict {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} :
    instance MeasureTheory.Restrict.isFiniteMeasure {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (μ : Measure α) [hs : Fact (μ s < )] :
    @[simp]
    theorem MeasureTheory.measure_lt_top {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] (s : Set α) :
    μ s <
    @[simp]
    theorem MeasureTheory.measure_ne_top {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] (s : Set α) :
    μ s
    theorem MeasureTheory.measure_compl_le_add_of_le_add {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} [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 α} {μ : Measure α} {s t : Set α} [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
      @[instance 50]
      theorem MeasureTheory.isFiniteMeasure_of_le {α : Type u_1} {m0 : MeasurableSpace α} {ν : Measure α} (μ : Measure α) [IsFiniteMeasure μ] (h : ν μ) :
      instance MeasureTheory.Measure.isFiniteMeasure_map {α : Type u_1} {β : Type u_2} [MeasurableSpace β] {m : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] (f : αβ) :
      instance MeasureTheory.IsFiniteMeasure_comap {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : Measure α} (f : βα) [IsFiniteMeasure μ] :
      theorem MeasureTheory.measureUnivNNReal_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] ( : μ 0) :
      theorem MeasureTheory.Measure.le_of_add_le_add_left {α : Type u_1} {m0 : MeasurableSpace α} {μ ν₁ ν₂ : Measure α} [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 α} {μ : Measure α} [ : IsFiniteMeasure μ] {f : Set α} (hf₁ : ∀ (i : ), MeasurableSet (f i)) (hf₂ : Pairwise (Function.onFun Disjoint f)) :
      Summable fun (x : ) => (μ (f x)).toReal
      theorem MeasureTheory.ae_eq_univ_iff_measure_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [IsFiniteMeasure μ] (hs : NullMeasurableSet s μ) :
      theorem MeasureTheory.ae_iff_measure_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] {p : αProp} (hp : NullMeasurableSet {a : α | p a} μ) :
      (∀ᵐ (a : α) μ, p a) μ {a : α | p a} = μ Set.univ
      theorem MeasureTheory.ae_mem_iff_measure_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] {s : Set α} (hs : NullMeasurableSet s μ) :
      (∀ᵐ (a : α) μ, a s) μ s = μ Set.univ
      theorem MeasureTheory.tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint {X : Type u_5} [MeasurableSpace X] {μ : Measure X} [IsFiniteMeasure μ] {Es : Set X} (Es_mble : ∀ (i : ), 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 α} {μ : Measure α} {s t : Set α} (hs : NullMeasurableSet s μ) (ht : NullMeasurableSet 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 α} {μ : Measure α} {s t : Set α} [IsFiniteMeasure μ] (hs : NullMeasurableSet s μ) (ht : NullMeasurableSet t μ) :
      |(μ s).toReal - (μ t).toReal| (μ (symmDiff s t)).toReal
      instance MeasureTheory.instIsFiniteMeasureSumMeasure {α : Type u_1} {ι : Type u_4} {m0 : MeasurableSpace α} {s : Finset ι} {μ : ιMeasure α} [∀ (i : ι), IsFiniteMeasure (μ i)] :
      IsFiniteMeasure (∑ is, μ i)
      instance MeasureTheory.instIsFiniteMeasureSumOfFinite {α : Type u_1} {ι : Type u_4} {m0 : MeasurableSpace α} [Finite ι] {μ : ιMeasure α} [∀ (i : ι), IsFiniteMeasure (μ i)] :
      theorem MeasureTheory.ite_ae_eq_of_measure_zero {α : Type u_1} {m0 : MeasurableSpace α} {μ : 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) =ᶠ[ae μ] g
      theorem MeasureTheory.ite_ae_eq_of_measure_compl_zero {α : Type u_1} {m0 : MeasurableSpace α} {μ : 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) =ᶠ[ae μ] f
      def MeasureTheory.Measure.FiniteAtFilter {α : Type u_1} {_m0 : MeasurableSpace α} (μ : Measure α) (f : Filter α) :

      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 α} {μ : Measure α} {f : Filter α} ( : μ.FiniteAtFilter f) {p : ιProp} {s : ιSet α} (hf : f.HasBasis p s) :
        ∃ (i : ι), p i μ (s i) <
        structure MeasureTheory.Measure.FiniteSpanningSetsIn {α : Type u_1} {m0 : MeasurableSpace α} (μ : 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.

        Instances For

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

          Instances
            theorem MeasureTheory.Measure.smul_finite {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] {c : ENNReal} (hc : c ) :
            theorem MeasureTheory.Measure.exists_isOpen_measure_lt_top {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : Measure α) [IsLocallyFiniteMeasure μ] (x : α) :
            ∃ (s : Set α), x s IsOpen s μ s <

            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.

              @[instance 100]

              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 α} {μ : Measure α} [Countable ι] {U : ιSet α} (hU : ⋃ (i : ι), U i = Set.univ) ( : μ 0) :
              ∃ (i : ι), 0 < μ (U i)
              theorem MeasureTheory.exists_pos_preimage_ball {α : Type u_1} {δ : Type u_3} {m0 : MeasurableSpace α} {μ : Measure α} [PseudoMetricSpace δ] (f : αδ) (x : δ) ( : μ 0) :
              ∃ (n : ), 0 < μ (f ⁻¹' Metric.ball x n)
              theorem MeasureTheory.exists_pos_ball {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [PseudoMetricSpace α] (x : α) ( : μ 0) :
              ∃ (n : ), 0 < μ (Metric.ball x n)
              theorem MeasureTheory.exists_ne_forall_mem_nhds_pos_measure_preimage {α : Type u_1} {m0 : MeasurableSpace α} {μ : 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)

              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.ext_on_measurableSpace_of_generate_finite {α : Type u_5} (m₀ : MeasurableSpace α) {μ ν : Measure α} [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 α} {μ ν : Measure α} (C : Set (Set α)) (hA : m0 = MeasurableSpace.generateFrom C) (hC : IsPiSystem C) [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).

              theorem MeasureTheory.Measure.FiniteAtFilter.filter_mono {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f g : Filter α} (h : f g) :
              theorem MeasureTheory.Measure.FiniteAtFilter.inf_of_left {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f g : Filter α} (h : μ.FiniteAtFilter f) :
              @[simp]
              theorem MeasureTheory.Measure.FiniteAtFilter.of_inf_ae {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f : Filter α} :
              μ.FiniteAtFilter (f 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 α} {μ : Measure α} {f g : Filter α} (h : f ae μ g) (hg : μ.FiniteAtFilter g) :
              theorem MeasureTheory.Measure.FiniteAtFilter.measure_mono {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} {f : Filter α} (h : μ ν) :
              theorem MeasureTheory.Measure.FiniteAtFilter.mono {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} {f g : Filter α} (hf : f g) ( : μ ν) :
              theorem MeasureTheory.Measure.FiniteAtFilter.eventually {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f : Filter α} (h : μ.FiniteAtFilter f) :
              ∀ᶠ (s : Set α) in f.smallSets, μ s <
              theorem MeasureTheory.Measure.FiniteAtFilter.filterSup {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f g : Filter α} :
              μ.FiniteAtFilter fμ.FiniteAtFilter gμ.FiniteAtFilter (f g)
              @[simp]
              theorem IsCompact.exists_open_superset_measure_lt_top' {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (h : IsCompact s) ( : 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) ( : 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
              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