Inner regularity of finite measures

The main result of this file is InnerRegularCompactLTTop_of_pseudoEMetricSpace_completeSpace_secondCountable: A finite measure μ on a PseudoEMetricSpace E and CompleteSpace E with SecondCountableTopology E is inner regular with respect to compact sets. In other words, a finite measure on such a space is a tight measure.

Finite measures on Polish spaces are an important special case, which makes the result MeasureTheory.PolishSpace.innerRegular_isCompact_isClosed_measurableSet an important result in probability.

theorem MeasureTheory.innerRegularWRT_isCompact_closure_iff {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace α] [R1Space α] : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed ↔ μ.InnerRegularWRT IsCompact IsClosed

theorem MeasureTheory.innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace α] [R1Space α] : μ.InnerRegularWRT (fun (s : Set α) => IsCompact s ∧ IsClosed s) IsClosed ↔ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed

theorem MeasureTheory.innerRegularWRT_isCompact_isClosed_iff {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace α] [R1Space α] : μ.InnerRegularWRT (fun (s : Set α) => IsCompact s ∧ IsClosed s) IsClosed ↔ μ.InnerRegularWRT IsCompact IsClosed

theorem MeasureTheory.innerRegularWRT_of_exists_compl_lt {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {p q : Set α → Prop} (hpq : ∀ (A B : Set α), p A → q B → p (A ∩ B)) (hμ : ∀ (ε : ENNReal), 0 < ε → ∃ (K : Set α), p K ∧ μ Kᶜ < ε) : μ.InnerRegularWRT p q

If predicate p is preserved under intersections with sets satisfying predicate q, and sets satisfying p cover the space arbitrarily well, then μ is inner regular with respect to predicates p and q.

theorem MeasureTheory.innerRegularWRT_isCompact_closure_of_univ {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace α] (hμ : ∀ (ε : ENNReal), 0 < ε → ∃ (K : Set α), IsCompact (closure K) ∧ μ Kᶜ < ε) : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed

theorem MeasureTheory.exists_isCompact_closure_measure_compl_lt {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [SecondCountableTopology α] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace α] [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] (ε : ENNReal) (hε : 0 < ε) : ∃ (K : Set α), IsCompact (closure K) ∧ P Kᶜ < ε

theorem MeasureTheory.innerRegularWRT_isCompact_closure {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [SecondCountableTopology α] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace α] [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] : P.InnerRegularWRT (IsCompact ∘ closure) IsClosed

theorem MeasureTheory.innerRegularWRT_isCompact_isClosed {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [SecondCountableTopology α] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace α] [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] : P.InnerRegularWRT (fun (s : Set α) => IsCompact s ∧ IsClosed s) IsClosed

theorem MeasureTheory.innerRegularWRT_isCompact {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [SecondCountableTopology α] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace α] [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] : P.InnerRegularWRT IsCompact IsClosed

theorem MeasureTheory.innerRegularWRT_isCompact_isClosed_isOpen {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [SecondCountableTopology α] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace α] [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] : P.InnerRegularWRT (fun (s : Set α) => IsCompact s ∧ IsClosed s) IsOpen

theorem MeasureTheory.innerRegularWRT_isCompact_isOpen {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [SecondCountableTopology α] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace α] [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] : P.InnerRegularWRT IsCompact IsOpen

instance MeasureTheory.instInnerRegularOfIsCompletelyPseudoMetrizableSpace {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [SecondCountableTopology α] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace α] [BorelSpace α] (P : Measure α) [IsFiniteMeasure P] : P.InnerRegular

A finite measure μ on a completely pseudo-metrizable space E with SecondCountableTopology E is inner regular. In other words, a finite measure on such a space is a tight measure.

instance MeasureTheory.instInnerRegularCompactLTTopOfIsCompletelyPseudoMetrizableSpace {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [SecondCountableTopology α] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace α] [BorelSpace α] (μ : Measure α) : μ.InnerRegularCompactLTTop

A measure μ on a PseudoEMetricSpace E and CompleteSpace E with SecondCountableTopology E is inner regular for finite measure sets with respect to compact sets.

theorem MeasureTheory.innerRegular_isCompact_isClosed_measurableSet_of_finite {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [SecondCountableTopology α] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace α] [BorelSpace α] (P : Measure α) [IsFiniteMeasure P] : P.InnerRegularWRT (fun (s : Set α) => IsCompact s ∧ IsClosed s) MeasurableSet

@[deprecated MeasureTheory.innerRegular_isCompact_isClosed_measurableSet_of_finite (since := "2025-12-08")]

theorem MeasureTheory.PolishSpace.innerRegular_isCompact_isClosed_measurableSet {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [SecondCountableTopology α] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace α] [BorelSpace α] (P : Measure α) [IsFiniteMeasure P] : P.InnerRegularWRT (fun (s : Set α) => IsCompact s ∧ IsClosed s) MeasurableSet

Alias of MeasureTheory.innerRegular_isCompact_isClosed_measurableSet_of_finite.