theorem MeasureTheory.tendsto_zero_measure_of_antitone {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] {s : ℕ → Set α} (hs1 : ∀ (n : ℕ), MeasurableSet (s n)) (hs2 : Antitone s) (hs3 : ⋂ (n : ℕ), s n = ∅) : Filter.Tendsto (fun (n : ℕ) => μ (s n)) Filter.atTop (nhds 0)

Some version of continuity of a measure in the emptyset using a decreasing sequence of sets.

theorem MeasureTheory.exists_measure_iInter_lt {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (S : ℕ → Set α) (hS2 : ∀ (n : ℕ), MeasurableSet (S n)) (hS3 : ⋂ (n : ℕ), S n = ∅) {ε : ENNReal} (hε : 0 < ε) : ∃ (m : ℕ), μ (⋂ (n : ℕ), ⋂ (_ : n ≤ m), S n) < ε

Some version of continuity of a measure in the emptyset using the intersection along a set of sets.

theorem MeasurableSet.ball {α : Type u_1} : ∀ {x : MeasurableSpace α} (x_1 : α) {s : Set (α × α)}, MeasurableSet s → MeasurableSet (UniformSpace.ball x_1 s)

def UniformSpace.interUnionBalls {α : Type u_1} (xs : ℕ → α) (u : ℕ → ℕ) (V : ℕ → Set (α × α)) : Set α

Given a family of points xs n, a family of entourages V n of the diagonal and a family of natural numbers u n, the intersection over n of the V n-neighborhood of xs 1, ..., xs (u n). Designed to be relatively compact when V n tends to the diagonal.

Equations

• UniformSpace.interUnionBalls xs u V = ⋂ (n : ℕ), ⋃ (m : ℕ), ⋃ (_ : m ≤ u n), UniformSpace.ball (xs m) (Prod.swap ⁻¹' V n)

theorem UniformSpace.totallyBounded_interUnionBalls {α : Type u_1} [UniformSpace α] {p : ℕ → Prop} {U : ℕ → Set (α × α)} (H : (uniformity α).HasBasis p U) (xs : ℕ → α) (u : ℕ → ℕ) : TotallyBounded (UniformSpace.interUnionBalls xs u U)

theorem UniformSpace.isCompact_closure_interUnionBalls {α : Type u_1} [UniformSpace α] {p : ℕ → Prop} {U : ℕ → Set (α × α)} (H : (uniformity α).HasBasis p U) [CompleteSpace α] (xs : ℕ → α) (u : ℕ → ℕ) : IsCompact (closure (UniformSpace.interUnionBalls xs u U))

The construction interUnionBalls is used to have a relatively compact set.

theorem MeasureTheory.measure_compl_interUnionBalls_le {α : Type u_1} : ∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) (xs : ℕ → α) (u : ℕ → ℕ) (V : ℕ → Set (α × α)), μ (UniformSpace.interUnionBalls xs u V)ᶜ ≤ ∑' (n : ℕ), μ (⋃ (m : ℕ), ⋃ (_ : m ≤ u n), UniformSpace.ball (xs m) (Prod.swap ⁻¹' V n))ᶜ

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

theorem MeasureTheory.innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.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 α] {μ : MeasureTheory.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 α] {μ : MeasureTheory.Measure α} {p : Set α → Prop} {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

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

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

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

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

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

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

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

theorem MeasureTheory.InnerRegularCompactLTTop_of_complete_countable {α : Type u_1} [MeasurableSpace α] [PseudoEMetricSpace α] [CompleteSpace α] [SecondCountableTopology α] [BorelSpace α] (P : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure P] : P.InnerRegularCompactLTTop

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

theorem MeasureTheory.PolishSpace.innerRegular_isCompact_measurableSet {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [PolishSpace α] [BorelSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] : μ.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.