Classes for finite measures #
We introduce the following typeclasses for measures:
IsFiniteMeasure μ:μ univ < ∞;IsLocallyFiniteMeasure μ:∀ x, ∃ s ∈ 𝓝 x, μ s < ∞.
A measure μ is called finite if μ univ < ∞.
Instances
theorem
MeasureTheory.not_isFiniteMeasure_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
:
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 < ⊤)]
:
IsFiniteMeasure (μ.restrict s)
@[simp]
theorem
MeasureTheory.measure_lt_top
{α : Type u_1}
{m0 : MeasurableSpace α}
(μ : Measure α)
[IsFiniteMeasure μ]
(s : Set α)
:
instance
MeasureTheory.isFiniteMeasureRestrict
{α : Type u_1}
{m0 : MeasurableSpace α}
(μ : Measure α)
(s : Set α)
[h : IsFiniteMeasure μ]
:
IsFiniteMeasure (μ.restrict s)
@[simp]
theorem
MeasureTheory.measure_ne_top
{α : Type u_1}
{m0 : MeasurableSpace α}
(μ : Measure α)
[IsFiniteMeasure μ]
(s : Set α)
:
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 + ε)
:
theorem
MeasureTheory.measure_compl_le_add_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
[IsFiniteMeasure μ]
(hs : MeasurableSet s)
(ht : MeasurableSet t)
{ε : ENNReal}
:
The measure of the whole space with respect to a finite measure, considered as ℝ≥0.
Equations
Instances For
@[simp]
theorem
MeasureTheory.coe_measureUnivNNReal
{α : Type u_1}
{m0 : MeasurableSpace α}
(μ : Measure α)
[IsFiniteMeasure μ]
:
@[instance 50]
instance
MeasureTheory.isFiniteMeasureOfIsEmpty
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[IsEmpty α]
:
@[simp]
instance
MeasureTheory.isFiniteMeasureAdd
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : Measure α}
[IsFiniteMeasure μ]
[IsFiniteMeasure ν]
:
IsFiniteMeasure (μ + ν)
instance
MeasureTheory.isFiniteMeasureSMulNNReal
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[IsFiniteMeasure μ]
{r : NNReal}
:
IsFiniteMeasure (r • μ)
instance
MeasureTheory.IsFiniteMeasure.average
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
:
IsFiniteMeasure ((μ Set.univ)⁻¹ • μ)
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 • μ)
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}
[mβ : MeasurableSpace β]
{m : MeasurableSpace α}
(μ : Measure α)
[IsFiniteMeasure μ]
(f : α → β)
:
IsFiniteMeasure (map f μ)
theorem
MeasureTheory.Measure.isFiniteMeasure_of_map
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
[mβ : MeasurableSpace β]
{μ : Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
[IsFiniteMeasure (map f μ)]
:
theorem
MeasureTheory.Measure.isFiniteMeasure_map_iff
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
[mβ : MeasurableSpace β]
{μ : Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
:
instance
MeasureTheory.IsFiniteMeasure_comap
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
[mβ : MeasurableSpace β]
{μ : Measure α}
(f : β → α)
[IsFiniteMeasure μ]
:
IsFiniteMeasure (Measure.comap f μ)
@[simp]
theorem
MeasureTheory.measureUnivNNReal_eq_zero
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[IsFiniteMeasure μ]
:
theorem
MeasureTheory.measureUnivNNReal_pos
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[IsFiniteMeasure μ]
(hμ : μ ≠ 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.Measure.eq_of_le_of_measure_univ_eq
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : Measure α}
[IsFiniteMeasure μ]
(hμν : μ ≤ ν)
(h_univ : μ Set.univ = ν Set.univ)
:
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))
:
theorem
MeasureTheory.ae_eq_univ_iff_measure_eq
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[IsFiniteMeasure μ]
(hs : NullMeasurableSet s μ)
:
theorem
MeasureTheory.ae_mem_iff_measure_eq
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[IsFiniteMeasure μ]
{s : Set α}
(hs : NullMeasurableSet s μ)
:
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_measureReal_sub_le_measureReal_symmDiff'
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
(hs : NullMeasurableSet s μ)
(ht : NullMeasurableSet t μ)
(hs' : μ s ≠ ⊤)
(ht' : μ t ≠ ⊤)
:
@[deprecated MeasureTheory.abs_measureReal_sub_le_measureReal_symmDiff' (since := "2025-04-18")]
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 ≠ ⊤)
:
Alias of MeasureTheory.abs_measureReal_sub_le_measureReal_symmDiff'.
theorem
MeasureTheory.abs_measureReal_sub_le_measureReal_symmDiff
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
[IsFiniteMeasure μ]
(hs : NullMeasurableSet s μ)
(ht : NullMeasurableSet t μ)
:
@[deprecated MeasureTheory.abs_measureReal_sub_le_measureReal_symmDiff (since := "2025-04-18")]
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 μ)
:
Alias of MeasureTheory.abs_measureReal_sub_le_measureReal_symmDiff.
instance
MeasureTheory.instIsFiniteMeasureSumMeasure
{α : Type u_1}
{ι : Type u_4}
{m0 : MeasurableSpace α}
{s : Finset ι}
{μ : ι → Measure α}
[∀ (i : ι), IsFiniteMeasure (μ i)]
:
IsFiniteMeasure (∑ i ∈ s, μ i)
instance
MeasureTheory.instIsFiniteMeasureSumOfFinite
{α : Type u_1}
{ι : Type u_4}
{m0 : MeasurableSpace α}
[Finite ι]
{μ : ι → Measure α}
[∀ (i : ι), IsFiniteMeasure (μ i)]
:
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
- μ.FiniteAtFilter f = ∃ s ∈ f, μ s < ⊤
Instances For
theorem
MeasureTheory.Measure.finiteAtFilter_of_finite
{α : Type u_1}
{_m0 : MeasurableSpace α}
(μ : Measure α)
[IsFiniteMeasure μ]
(f : Filter α)
:
μ.FiniteAtFilter f
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)
:
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.
The sequence of sets in
Cwith finite measures
Instances For
class
MeasureTheory.IsLocallyFiniteMeasure
{α : Type u_1}
{m0 : MeasurableSpace α}
[TopologicalSpace α]
(μ : Measure α)
:
A measure is called locally finite if it is finite in some neighborhood of each point.
- finiteAtNhds (x : α) : μ.FiniteAtFilter (nhds x)
Instances
@[instance 100]
instance
MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure
{α : Type u_1}
{m0 : MeasurableSpace α}
[TopologicalSpace α]
(μ : Measure α)
[IsFiniteMeasure μ]
:
theorem
MeasureTheory.Measure.finiteAt_nhds
{α : Type u_1}
{m0 : MeasurableSpace α}
[TopologicalSpace α]
(μ : Measure α)
[IsLocallyFiniteMeasure μ]
(x : α)
:
μ.FiniteAtFilter (nhds x)
theorem
MeasureTheory.Measure.smul_finite
{α : Type u_1}
{m0 : MeasurableSpace α}
(μ : Measure α)
[IsFiniteMeasure μ]
{c : ENNReal}
(hc : c ≠ ⊤)
:
IsFiniteMeasure (c • μ)
theorem
MeasureTheory.Measure.exists_isOpen_measure_lt_top
{α : Type u_1}
{m0 : MeasurableSpace α}
[TopologicalSpace α]
(μ : Measure α)
[IsLocallyFiniteMeasure μ]
(x : α)
:
instance
MeasureTheory.isLocallyFiniteMeasureSMulNNReal
{α : Type u_1}
{m0 : MeasurableSpace α}
[TopologicalSpace α]
(μ : Measure α)
[IsLocallyFiniteMeasure μ]
(c : NNReal)
:
IsLocallyFiniteMeasure (c • μ)
theorem
MeasureTheory.Measure.isTopologicalBasis_isOpen_lt_top
{α : Type u_1}
{m0 : MeasurableSpace α}
[TopologicalSpace α]
(μ : Measure α)
[IsLocallyFiniteMeasure μ]
:
class
MeasureTheory.IsFiniteMeasureOnCompacts
{α : Type u_1}
{m0 : MeasurableSpace α}
[TopologicalSpace α]
(μ : Measure α)
:
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)
:
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)
:
A compact subset has finite measure for a measure which is finite on compacts.
theorem
Bornology.IsBounded.measure_lt_top
{α : Type u_1}
{m0 : MeasurableSpace α}
[PseudoMetricSpace α]
[ProperSpace α]
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasureOnCompacts μ]
⦃s : Set α⦄
(hs : IsBounded s)
:
A bounded subset has finite measure for a measure which is finite on compact sets, in a proper space.
theorem
MeasureTheory.measure_closedBall_lt_top
{α : Type u_1}
{m0 : MeasurableSpace α}
[PseudoMetricSpace α]
[ProperSpace α]
{μ : Measure α}
[IsFiniteMeasureOnCompacts μ]
{x : α}
{r : ℝ}
:
theorem
MeasureTheory.measure_ball_lt_top
{α : Type u_1}
{m0 : MeasurableSpace α}
[PseudoMetricSpace α]
[ProperSpace α]
{μ : Measure α}
[IsFiniteMeasureOnCompacts μ]
{x : α}
{r : ℝ}
:
theorem
MeasureTheory.measure_ball_ne_top
{α : Type u_1}
{m0 : MeasurableSpace α}
[PseudoMetricSpace α]
[ProperSpace α]
{μ : Measure α}
[IsFiniteMeasureOnCompacts μ]
{x : α}
{r : ℝ}
:
theorem
MeasureTheory.IsFiniteMeasureOnCompacts.smul
{α : Type u_1}
{m0 : MeasurableSpace α}
[TopologicalSpace α]
(μ : Measure α)
[IsFiniteMeasureOnCompacts μ]
{c : ENNReal}
(hc : c ≠ ⊤)
:
IsFiniteMeasureOnCompacts (c • μ)
instance
MeasureTheory.IsFiniteMeasureOnCompacts.smul_nnreal
{α : Type u_1}
{m0 : MeasurableSpace α}
[TopologicalSpace α]
(μ : Measure α)
[IsFiniteMeasureOnCompacts μ]
(c : NNReal)
:
IsFiniteMeasureOnCompacts (c • μ)
instance
MeasureTheory.instIsFiniteMeasureOnCompactsRestrict
{α : Type u_1}
{m0 : MeasurableSpace α}
[TopologicalSpace α]
{μ : Measure α}
[IsFiniteMeasureOnCompacts μ]
{s : Set α}
:
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)
:
@[instance 100]
instance
MeasureTheory.CompactSpace.isFiniteMeasure
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace α]
[CompactSpace α]
[IsFiniteMeasureOnCompacts μ]
:
@[instance 100]
instance
MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace α]
[WeaklyLocallyCompactSpace α]
[IsFiniteMeasureOnCompacts μ]
:
A measure which is finite on compact sets in a locally compact space is locally finite.
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)
theorem
MeasureTheory.exists_pos_ball
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[PseudoMetricSpace α]
(x : α)
(hμ : μ ≠ 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)
:
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μν : ∀ 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)
:
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μν : ∀ 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).
theorem
MeasureTheory.Measure.FiniteAtFilter.filter_mono
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{f g : Filter α}
(h : f ≤ g)
:
μ.FiniteAtFilter g → μ.FiniteAtFilter f
theorem
MeasureTheory.Measure.FiniteAtFilter.inf_of_left
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{f g : Filter α}
(h : μ.FiniteAtFilter f)
:
μ.FiniteAtFilter (f ⊓ g)
theorem
MeasureTheory.Measure.FiniteAtFilter.inf_of_right
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{f g : Filter α}
(h : μ.FiniteAtFilter g)
:
μ.FiniteAtFilter (f ⊓ g)
@[simp]
theorem
MeasureTheory.Measure.FiniteAtFilter.inf_ae_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{f : Filter α}
:
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)
:
μ.FiniteAtFilter f
theorem
MeasureTheory.Measure.FiniteAtFilter.measure_mono
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : Measure α}
{f : Filter α}
(h : μ ≤ ν)
:
ν.FiniteAtFilter f → μ.FiniteAtFilter f
theorem
MeasureTheory.Measure.FiniteAtFilter.mono
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : Measure α}
{f g : Filter α}
(hf : f ≤ g)
(hμ : μ ≤ ν)
:
ν.FiniteAtFilter g → μ.FiniteAtFilter f
theorem
MeasureTheory.Measure.FiniteAtFilter.eventually
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{f : Filter α}
(h : μ.FiniteAtFilter f)
:
theorem
MeasureTheory.Measure.FiniteAtFilter.filterSup
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{f g : Filter α}
:
μ.FiniteAtFilter f → μ.FiniteAtFilter g → μ.FiniteAtFilter (f ⊔ g)
theorem
MeasureTheory.Measure.finiteAt_nhdsWithin
{α : Type u_1}
[TopologicalSpace α]
{_m0 : MeasurableSpace α}
(μ : Measure α)
[IsLocallyFiniteMeasure μ]
(x : α)
(s : Set α)
:
μ.FiniteAtFilter (nhdsWithin x s)
@[simp]
theorem
MeasureTheory.Measure.finiteAt_principal
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
:
theorem
MeasureTheory.Measure.isLocallyFiniteMeasure_of_le
{α : Type u_1}
[TopologicalSpace α]
{_m : MeasurableSpace α}
{μ ν : Measure α}
[H : IsLocallyFiniteMeasure μ]
(h : ν ≤ μ)
:
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))
:
If s is a compact set and μ is finite at 𝓝 x for every x ∈ s, then s admits an open
superset of finite measure.
theorem
IsCompact.exists_open_superset_measure_lt_top
{α : Type u_1}
[TopologicalSpace α]
[MeasurableSpace α]
{s : Set α}
(h : IsCompact s)
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsLocallyFiniteMeasure μ]
:
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μ : ∀ x ∈ s, μ.FiniteAtFilter (nhdsWithin x s))
:
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
@[instance 100]
instance
isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure
{α : Type u_1}
[TopologicalSpace α]
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsLocallyFiniteMeasure μ]
:
theorem
isFiniteMeasure_iff_isFiniteMeasureOnCompacts_of_compactSpace
{α : Type u_1}
[TopologicalSpace α]
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[CompactSpace α]
:
def
MeasureTheory.Measure.finiteSpanningSetsInCompact
{α : Type u_1}
[TopologicalSpace α]
[SigmaCompactSpace α]
{x✝ : MeasurableSpace α}
(μ : Measure α)
[IsLocallyFiniteMeasure μ]
:
Compact covering of a σ-compact topological space as
MeasureTheory.Measure.FiniteSpanningSetsIn.
Equations
- μ.finiteSpanningSetsInCompact = { set := compactCovering α, set_mem := ⋯, finite := ⋯, spanning := ⋯ }
Instances For
def
MeasureTheory.Measure.finiteSpanningSetsInOpen
{α : Type u_1}
[TopologicalSpace α]
[SigmaCompactSpace α]
{x✝ : MeasurableSpace α}
(μ : Measure α)
[IsLocallyFiniteMeasure μ]
:
A locally finite measure on a σ-compact topological space admits a finite spanning sequence
of open sets.
Equations
Instances For
theorem
MeasureTheory.Measure.finiteSpanningSetsInOpen'_def
{α : Type u_5}
[TopologicalSpace α]
[SecondCountableTopology α]
{m : MeasurableSpace α}
(μ : Measure α)
[IsLocallyFiniteMeasure μ]
:
@[irreducible]
noncomputable def
MeasureTheory.Measure.finiteSpanningSetsInOpen'
{α : Type u_5}
[TopologicalSpace α]
[SecondCountableTopology α]
{m : MeasurableSpace α}
(μ : Measure α)
[IsLocallyFiniteMeasure μ]
:
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
theorem
measure_Icc_lt_top
{α : Type u_1}
[Preorder α]
[TopologicalSpace α]
[CompactIccSpace α]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsLocallyFiniteMeasure μ]
{a b : α}
:
theorem
measure_Ico_lt_top
{α : Type u_1}
[Preorder α]
[TopologicalSpace α]
[CompactIccSpace α]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsLocallyFiniteMeasure μ]
{a b : α}
:
theorem
measure_Ioc_lt_top
{α : Type u_1}
[Preorder α]
[TopologicalSpace α]
[CompactIccSpace α]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsLocallyFiniteMeasure μ]
{a b : α}
:
theorem
measure_Ioo_lt_top
{α : Type u_1}
[Preorder α]
[TopologicalSpace α]
[CompactIccSpace α]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsLocallyFiniteMeasure μ]
{a b : α}
: