# Classes for finite measures #

We introduce the following typeclasses for measures:

- `IsFiniteMeasure μ`: `μ univ < ∞`;
- `IsLocallyFiniteMeasure μ` : `∀ x, ∃ s ∈ 𝓝 x, μ s < ∞`.

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

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

- measure_univ_lt_top : μ Set.univ < ⊤

Instances

source
theorem MeasureTheory.isFiniteMeasure_iff {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) :
IsFiniteMeasure μ ↔ μ Set.univ < ⊤
source
theorem MeasureTheory.not_isFiniteMeasure_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} :
¬IsFiniteMeasure μ ↔ μ Set.univ = ⊤
source
theorem MeasureTheory.isFiniteMeasure_restrict {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} :
IsFiniteMeasure (μ.restrict s) ↔ μ s ≠ ⊤
source
instance MeasureTheory.Restrict.isFiniteMeasure {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (μ : Measure α) [hs : Fact (μ s < ⊤)] :
IsFiniteMeasure (μ.restrict s)
source
@[simp]
theorem MeasureTheory.measure_lt_top {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] (s : Set α) :
μ s < ⊤
source
instance MeasureTheory.isFiniteMeasureRestrict {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) (s : Set α) [h : IsFiniteMeasure μ] :
IsFiniteMeasure (μ.restrict s)
source
@[simp]
theorem MeasureTheory.measure_ne_top {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] (s : Set α) :
μ s ≠ ⊤
source
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 ᶜ + ε
source
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 + ε
source
def MeasureTheory.measureUnivNNReal {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) :
NNReal

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

Equations

- MeasureTheory.measureUnivNNReal μ = (μ Set.univ).toNNReal

Instances For

source
@[simp]
theorem MeasureTheory.coe_measureUnivNNReal {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] :
↑(measureUnivNNReal μ) = μ Set.univ
source
instance MeasureTheory.isFiniteMeasureZero {α : Type u_1} {m0 : MeasurableSpace α} :
IsFiniteMeasure 0
source
@[instance 50]
instance MeasureTheory.isFiniteMeasureOfIsEmpty {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [IsEmpty α] :
IsFiniteMeasure μ
source
@[simp]
theorem MeasureTheory.measureUnivNNReal_zero {α : Type u_1} {m0 : MeasurableSpace α} :
measureUnivNNReal 0 = 0
source
instance MeasureTheory.isFiniteMeasureAdd {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
IsFiniteMeasure (μ + ν)
source
instance MeasureTheory.isFiniteMeasureSMulNNReal {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] {r : NNReal} :
IsFiniteMeasure (r • μ)
source
instance MeasureTheory.IsFiniteMeasure.average {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} :
IsFiniteMeasure ((μ Set.univ)⁻¹ • μ)
source
instance MeasureTheory.isFiniteMeasureSMulOfNNRealTower {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {R : Type u_5} [SMul R NNReal] [SMul R ENNReal] [IsScalarTower R NNReal ENNReal] [IsScalarTower R ENNReal ENNReal] [IsFiniteMeasure μ] {r : R} :
IsFiniteMeasure (r • μ)
source
theorem MeasureTheory.isFiniteMeasure_of_le {α : Type u_1} {m0 : MeasurableSpace α} {ν : Measure α} (μ : Measure α) [IsFiniteMeasure μ] (h : ν ≤ μ) :
IsFiniteMeasure ν
source
instance MeasureTheory.Measure.isFiniteMeasure_map {α : Type u_1} {β : Type u_2} [mβ : MeasurableSpace β] {m : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] (f : α → β) :
IsFiniteMeasure (map f μ)
source
theorem MeasureTheory.Measure.isFiniteMeasure_of_map {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [mβ : MeasurableSpace β] {μ : Measure α} {f : α → β} (hf : AEMeasurable f μ) [IsFiniteMeasure (map f μ)] :
IsFiniteMeasure μ
source
theorem MeasureTheory.Measure.isFiniteMeasure_map_iff {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [mβ : MeasurableSpace β] {μ : Measure α} {f : α → β} (hf : AEMeasurable f μ) :
IsFiniteMeasure (map f μ) ↔ IsFiniteMeasure μ
source
instance MeasureTheory.IsFiniteMeasure_comap {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [mβ : MeasurableSpace β] {μ : Measure α} (f : β → α) [IsFiniteMeasure μ] :
IsFiniteMeasure (Measure.comap f μ)
source
@[simp]
theorem MeasureTheory.measureUnivNNReal_eq_zero {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] :
measureUnivNNReal μ = 0 ↔ μ = 0
source
theorem MeasureTheory.measureUnivNNReal_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] (hμ : μ ≠ 0) :
0 < measureUnivNNReal μ
source
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.

source
theorem MeasureTheory.Measure.eq_of_le_of_measure_univ_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} [IsFiniteMeasure μ] (hμν : μ ≤ ν) (h_univ : μ Set.univ = ν Set.univ) :
μ = ν
source
theorem MeasureTheory.summable_measure_toReal {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [hμ : IsFiniteMeasure μ] {f : ℕ → Set α} (hf₁ : ∀ (i : ℕ), MeasurableSet (f i)) (hf₂ : Pairwise (Function.onFun Disjoint f)) :
Summable fun (x : ℕ) => μ.real (f x)
source
theorem MeasureTheory.ae_eq_univ_iff_measure_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [IsFiniteMeasure μ] (hs : NullMeasurableSet s μ) :
s =ᶠ[ae μ] Set.univ ↔ μ s = μ Set.univ
source
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
source
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
source
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)
source
theorem MeasureTheory.abs_measureReal_sub_le_measureReal_symmDiff' {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hs : NullMeasurableSet s μ) (ht : NullMeasurableSet t μ) (hs' : μ s ≠ ⊤) (ht' : μ t ≠ ⊤) :
|μ.real s - μ.real t| ≤ μ.real (symmDiff s t)
source
theorem MeasureTheory.abs_measureReal_sub_le_measureReal_symmDiff {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} [IsFiniteMeasure μ] (hs : NullMeasurableSet s μ) (ht : NullMeasurableSet t μ) :
|μ.real s - μ.real t| ≤ μ.real (symmDiff s t)
source
instance MeasureTheory.instIsFiniteMeasureSumMeasure {α : Type u_1} {ι : Type u_4} {m0 : MeasurableSpace α} {s : Finset ι} {μ : ι → Measure α} [∀ (i : ι), IsFiniteMeasure (μ i)] :
IsFiniteMeasure (∑ i ∈ s, μ i)
source
instance MeasureTheory.instIsFiniteMeasureSumOfFinite {α : Type u_1} {ι : Type u_4} {m0 : MeasurableSpace α} [Finite ι] {μ : ι → Measure α} [∀ (i : ι), IsFiniteMeasure (μ i)] :
IsFiniteMeasure (Measure.sum μ)
source
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
source
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
source
def MeasureTheory.Measure.FiniteAtFilter {α : Type u_1} {_m0 : MeasurableSpace α} (μ : Measure α) (f : Filter α) :
Prop

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 = ∃ s ∈ f, μ s < ⊤

Instances For

source
theorem MeasureTheory.Measure.finiteAtFilter_of_finite {α : Type u_1} {_m0 : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] (f : Filter α) :
μ.FiniteAtFilter f
source
theorem MeasureTheory.Measure.FiniteAtFilter.exists_mem_basis {α : Type u_1} {ι : Type u_4} {m0 : MeasurableSpace α} {μ : Measure α} {f : Filter α} (hμ : μ.FiniteAtFilter f) {p : ι → Prop} {s : ι → Set α} (hf : f.HasBasis p s) :
∃ (i : ι), p i ∧ μ (s i) < ⊤
source
theorem MeasureTheory.Measure.finiteAtBot {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) :
μ.FiniteAtFilter ⊥
source
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.

- set : ℕ → Set α

  The sequence of sets in `C` with finite measures

- set_mem (i : ℕ) : self.set i ∈ C
- finite (i : ℕ) : μ (self.set i) < ⊤
- spanning : ⋃ (i : ℕ), self.set i = Set.univ

Instances For

source
class MeasureTheory.IsLocallyFiniteMeasure {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : Measure α) :
Prop

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

- finiteAtNhds (x : α) : μ.FiniteAtFilter (nhds x)

Instances

source
@[instance 100]
instance MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : Measure α) [IsFiniteMeasure μ] :
IsLocallyFiniteMeasure μ
source
theorem MeasureTheory.Measure.finiteAt_nhds {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : Measure α) [IsLocallyFiniteMeasure μ] (x : α) :
μ.FiniteAtFilter (nhds x)
source
theorem MeasureTheory.Measure.smul_finite {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] {c : ENNReal} (hc : c ≠ ⊤) :
IsFiniteMeasure (c • μ)
source
theorem MeasureTheory.Measure.exists_isOpen_measure_lt_top {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : Measure α) [IsLocallyFiniteMeasure μ] (x : α) :
∃ (s : Set α), x ∈ s ∧ IsOpen s ∧ μ s < ⊤
source
instance MeasureTheory.isLocallyFiniteMeasureSMulNNReal {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : Measure α) [IsLocallyFiniteMeasure μ] (c : NNReal) :
IsLocallyFiniteMeasure (c • μ)
source
theorem MeasureTheory.Measure.isTopologicalBasis_isOpen_lt_top {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : Measure α) [IsLocallyFiniteMeasure μ] :
TopologicalSpace.IsTopologicalBasis {s : Set α | IsOpen s ∧ μ s < ⊤}
source
class MeasureTheory.IsFiniteMeasureOnCompacts {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : Measure α) :
Prop

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

- lt_top_of_isCompact ⦃K : Set α⦄ : IsCompact K → μ K < ⊤

Instances

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

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

source
theorem Bornology.IsBounded.measure_lt_top {α : Type u_1} {m0 : MeasurableSpace α} [PseudoMetricSpace α] [ProperSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasureOnCompacts μ] ⦃s : Set α⦄ (hs : IsBounded s) :
μ s < ⊤

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

source
theorem MeasureTheory.measure_closedBall_lt_top {α : Type u_1} {m0 : MeasurableSpace α} [PseudoMetricSpace α] [ProperSpace α] {μ : Measure α} [IsFiniteMeasureOnCompacts μ] {x : α} {r : ℝ} :
μ (Metric.closedBall x r) < ⊤
source
theorem MeasureTheory.measure_ball_ne_top {α : Type u_1} {m0 : MeasurableSpace α} [PseudoMetricSpace α] [ProperSpace α] {μ : Measure α} [IsFiniteMeasureOnCompacts μ] {x : α} {r : ℝ} :
μ (Metric.ball x r) ≠ ⊤
source
theorem MeasureTheory.measure_ball_lt_top {α : Type u_1} {m0 : MeasurableSpace α} [PseudoMetricSpace α] [ProperSpace α] {μ : Measure α} [IsFiniteMeasureOnCompacts μ] {x : α} {r : ℝ} :
μ (Metric.ball x r) < ⊤
source
theorem MeasureTheory.IsFiniteMeasureOnCompacts.smul {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : Measure α) [IsFiniteMeasureOnCompacts μ] {c : ENNReal} (hc : c ≠ ⊤) :
IsFiniteMeasureOnCompacts (c • μ)
source
instance MeasureTheory.IsFiniteMeasureOnCompacts.smul_nnreal {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : Measure α) [IsFiniteMeasureOnCompacts μ] (c : NNReal) :
IsFiniteMeasureOnCompacts (c • μ)
source
instance MeasureTheory.instIsFiniteMeasureOnCompactsRestrict {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] {μ : Measure α} [IsFiniteMeasureOnCompacts μ] {s : Set α} :
IsFiniteMeasureOnCompacts (μ.restrict s)
source
theorem MeasureTheory.IsFiniteMeasureOnCompacts.comap' {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {mβ : MeasurableSpace β} [TopologicalSpace α] [TopologicalSpace β] (μ : Measure β) [IsFiniteMeasureOnCompacts μ] {f : α → β} (f_cont : Continuous f) (f_me : MeasurableEmbedding f) :
IsFiniteMeasureOnCompacts (Measure.comap f μ)
source
@[instance 100]
instance MeasureTheory.CompactSpace.isFiniteMeasure {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [TopologicalSpace α] [CompactSpace α] [IsFiniteMeasureOnCompacts μ] :
IsFiniteMeasure μ
source
@[instance 100]
instance MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [TopologicalSpace α] [WeaklyLocallyCompactSpace α] [IsFiniteMeasureOnCompacts μ] :
IsLocallyFiniteMeasure μ

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

source
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) (hμ : μ ≠ 0) :
∃ (i : ι), 0 < μ (U i)
source
theorem MeasureTheory.exists_pos_preimage_ball {α : Type u_1} {δ : Type u_3} {m0 : MeasurableSpace α} {μ : Measure α} [PseudoMetricSpace δ] (f : α → δ) (x : δ) (hμ : μ ≠ 0) :
∃ (n : ℕ), 0 < μ (f ⁻¹' Metric.ball x ↑n)
source
theorem MeasureTheory.exists_pos_ball {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [PseudoMetricSpace α] (x : α) (hμ : μ ≠ 0) :
∃ (n : ℕ), 0 < μ (Metric.ball x ↑n)
source
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 ∧ (∀ s ∈ nhds a, 0 < μ (f ⁻¹' s)) ∧ ∀ t ∈ nhds 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.

source
theorem MeasureTheory.ext_on_measurableSpace_of_generate_finite {α : Type u_5} (m₀ : MeasurableSpace α) {μ ν : Measure α} [IsFiniteMeasure μ] (C : Set (Set α)) (hμν : ∀ s ∈ C, μ 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.

source
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μν : ∀ s ∈ C, μ 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`).

source
theorem MeasureTheory.Measure.FiniteAtFilter.filter_mono {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f g : Filter α} (h : f ≤ g) :
μ.FiniteAtFilter g → μ.FiniteAtFilter f
source
theorem MeasureTheory.Measure.FiniteAtFilter.inf_of_left {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f g : Filter α} (h : μ.FiniteAtFilter f) :
μ.FiniteAtFilter (f ⊓ g)
source
theorem MeasureTheory.Measure.FiniteAtFilter.inf_of_right {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f g : Filter α} (h : μ.FiniteAtFilter g) :
μ.FiniteAtFilter (f ⊓ g)
source
@[simp]
theorem MeasureTheory.Measure.FiniteAtFilter.inf_ae_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f : Filter α} :
μ.FiniteAtFilter (f ⊓ ae μ) ↔ μ.FiniteAtFilter f
source
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`.

source
theorem MeasureTheory.Measure.FiniteAtFilter.filter_mono_ae {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f g : Filter α} (h : f ⊓ ae μ ≤ g) (hg : μ.FiniteAtFilter g) :
μ.FiniteAtFilter f
source
theorem MeasureTheory.Measure.FiniteAtFilter.measure_mono {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} {f : Filter α} (h : μ ≤ ν) :
ν.FiniteAtFilter f → μ.FiniteAtFilter f
source
theorem MeasureTheory.Measure.FiniteAtFilter.mono {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} {f g : Filter α} (hf : f ≤ g) (hμ : μ ≤ ν) :
ν.FiniteAtFilter g → μ.FiniteAtFilter f
source
theorem MeasureTheory.Measure.FiniteAtFilter.eventually {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f : Filter α} (h : μ.FiniteAtFilter f) :
∀ᶠ (s : Set α) in f.smallSets, μ s < ⊤
source
theorem MeasureTheory.Measure.FiniteAtFilter.filterSup {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f g : Filter α} :
μ.FiniteAtFilter f → μ.FiniteAtFilter g → μ.FiniteAtFilter (f ⊔ g)
source
theorem MeasureTheory.Measure.finiteAt_nhdsWithin {α : Type u_1} [TopologicalSpace α] {_m0 : MeasurableSpace α} (μ : Measure α) [IsLocallyFiniteMeasure μ] (x : α) (s : Set α) :
μ.FiniteAtFilter (nhdsWithin x s)
source
@[simp]
theorem MeasureTheory.Measure.finiteAt_principal {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} :
μ.FiniteAtFilter (Filter.principal s) ↔ μ s < ⊤
source
theorem MeasureTheory.Measure.isLocallyFiniteMeasure_of_le {α : Type u_1} [TopologicalSpace α] {_m : MeasurableSpace α} {μ ν : Measure α} [H : IsLocallyFiniteMeasure μ] (h : ν ≤ μ) :
IsLocallyFiniteMeasure ν
source
theorem IsCompact.exists_open_superset_measure_lt_top' {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (h : IsCompact s) (hμ : ∀ x ∈ s, μ.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.

source
theorem IsCompact.exists_open_superset_measure_lt_top {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {s : Set α} (h : IsCompact s) (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] :
∃ U ⊇ s, IsOpen U ∧ μ U < ⊤

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

source
theorem IsCompact.measure_lt_top_of_nhdsWithin {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (h : IsCompact s) (hμ : ∀ x ∈ s, μ.FiniteAtFilter (nhdsWithin x s)) :
μ s < ⊤
source
theorem IsCompact.measure_zero_of_nhdsWithin {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : IsCompact s) :
(∀ a ∈ s, ∃ t ∈ nhdsWithin a s, μ t = 0) → μ s = 0
source
@[instance 100]
instance isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure {α : Type u_1} [TopologicalSpace α] {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] :
MeasureTheory.IsFiniteMeasureOnCompacts μ
source
theorem isFiniteMeasure_iff_isFiniteMeasureOnCompacts_of_compactSpace {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [CompactSpace α] :
MeasureTheory.IsFiniteMeasure μ ↔ MeasureTheory.IsFiniteMeasureOnCompacts μ
source
def MeasureTheory.Measure.finiteSpanningSetsInCompact {α : Type u_1} [TopologicalSpace α] [SigmaCompactSpace α] {x✝ : MeasurableSpace α} (μ : Measure α) [IsLocallyFiniteMeasure μ] :
μ.FiniteSpanningSetsIn {K : Set α | IsCompact K}

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

Equations

- μ.finiteSpanningSetsInCompact = { set := compactCovering α, set_mem := ⋯, finite := ⋯, spanning := ⋯ }

Instances For

source
def MeasureTheory.Measure.finiteSpanningSetsInOpen {α : Type u_1} [TopologicalSpace α] [SigmaCompactSpace α] {x✝ : MeasurableSpace α} (μ : Measure α) [IsLocallyFiniteMeasure μ] :
μ.FiniteSpanningSetsIn {K : Set α | IsOpen K}

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

source
@[irreducible]
noncomputable def MeasureTheory.Measure.finiteSpanningSetsInOpen' {α : Type u_5} [TopologicalSpace α] [SecondCountableTopology α] {m : MeasurableSpace α} (μ : Measure α) [IsLocallyFiniteMeasure μ] :
μ.FiniteSpanningSetsIn {K : Set α | IsOpen K}

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

Equations

- μ.finiteSpanningSetsInOpen' = have H := ⋯; H.some

Instances For

source
theorem MeasureTheory.Measure.finiteSpanningSetsInOpen'_def {α : Type u_5} [TopologicalSpace α] [SecondCountableTopology α] {m : MeasurableSpace α} (μ : Measure α) [IsLocallyFiniteMeasure μ] :
μ.finiteSpanningSetsInOpen' = have H := ⋯; H.some
source
theorem measure_Icc_lt_top {α : Type u_1} [Preorder α] [TopologicalSpace α] [CompactIccSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {a b : α} :
μ (Set.Icc a b) < ⊤
source
theorem measure_Ico_lt_top {α : Type u_1} [Preorder α] [TopologicalSpace α] [CompactIccSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {a b : α} :
μ (Set.Ico a b) < ⊤
source
theorem measure_Ioc_lt_top {α : Type u_1} [Preorder α] [TopologicalSpace α] [CompactIccSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {a b : α} :
μ (Set.Ioc a b) < ⊤
source
theorem measure_Ioo_lt_top {α : Type u_1} [Preorder α] [TopologicalSpace α] [CompactIccSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {a b : α} :
μ (Set.Ioo a b) < ⊤