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 α] [UniformSpace α] [CompleteSpace α] [SecondCountableTopology α] [(uniformity α).IsCountablyGenerated] [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] (ε : ENNReal) (hε : 0 < ε) : ∃ (K : Set α), IsCompact (closure K) ∧ P Kᶜ < ε

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

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

theorem MeasureTheory.innerRegularWRT_isCompact {α : Type u_1} [MeasurableSpace α] [UniformSpace α] [CompleteSpace α] [SecondCountableTopology α] [(uniformity α).IsCountablyGenerated] [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] : P.InnerRegularWRT IsCompact IsClosed

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

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

instance MeasureTheory.InnerRegular_of_pseudoEMetricSpace_completeSpace_secondCountable {α : Type u_1} [MeasurableSpace α] [PseudoEMetricSpace α] [CompleteSpace α] [SecondCountableTopology α] [BorelSpace α] (P : Measure α) [IsFiniteMeasure P] : P.InnerRegular

A finite measure μ on a PseudoEMetricSpace E and CompleteSpace E with SecondCountableTopology E is inner regular. In other words, a finite measure on such a space is a tight measure.

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

A special case of innerRegular_of_pseudoEMetricSpace_completeSpace_secondCountable for Polish spaces: A finite measure on a Polish space is a tight measure.

instance MeasureTheory.InnerRegularCompactLTTop_of_pseudoEMetricSpace_completeSpace_secondCountable {α : Type u_1} [MeasurableSpace α] [PseudoEMetricSpace α] [CompleteSpace α] [SecondCountableTopology α] [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.

instance MeasureTheory.InnerRegularCompactLTTop_of_polishSpace {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [PolishSpace α] [BorelSpace α] (μ : Measure α) : μ.InnerRegularCompactLTTop

A special case of innerRegularCompactLTTop_of_pseudoEMetricSpace_completeSpace_secondCountable for Polish spaces: A measure μ on a Polish space inner regular for finite measure sets with respect to compact sets.

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

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

On a Polish space, any finite measure is regular with respect to compact and closed sets. In particular, a finite measure on a Polish space is a tight measure.