Continuity of measures

This file proves several versions of continuity from above and continuity from below of measures, namely statements of the form μ (⋃ n, s n) = ⨆ n, μ (s n) and μ (⋂ n, s n) = ⨅ n, μ (s n) for s : ℕ → Set α.

Tags

continuity of measures

theorem Directed.measure_iUnion {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : ι → Set α} [Countable ι] (hd : Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) s) : μ (⋃ (i : ι), s i) = ⨆ (i : ι), μ (s i)

Continuity from below: the measure of the union of a directed sequence of (not necessarily measurable) sets is the supremum of the measures.

theorem Monotone.measure_iUnion {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : ι → Set α} [Preorder ι] [IsDirectedOrder ι] [Filter.atTop.IsCountablyGenerated] (hs : Monotone s) : μ (⋃ (i : ι), s i) = ⨆ (i : ι), μ (s i)

Continuity from below: the measure of the union of a monotone family of sets is equal to the supremum of their measures. The theorem assumes that the atTop filter on the index set is countably generated, so it works for a family indexed by a countable type, as well as ℝ.

theorem Antitone.measure_iUnion {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : ι → Set α} [Preorder ι] [IsCodirectedOrder ι] [Filter.atBot.IsCountablyGenerated] (hs : Antitone s) : μ (⋃ (i : ι), s i) = ⨆ (i : ι), μ (s i)

theorem MeasureTheory.measure_iUnion_eq_iSup_accumulate {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {s : ι → Set α} [Preorder ι] [IsDirectedOrder ι] [Filter.atTop.IsCountablyGenerated] : μ (⋃ (i : ι), s i) = ⨆ (i : ι), μ (Set.accumulate s i)

Continuity from below: the measure of the union of a sequence of (not necessarily measurable) sets is the supremum of the measures of the partial unions.

theorem MeasureTheory.measure_biUnion_eq_iSup {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {s : ι → Set α} {t : Set ι} (ht : t.Countable) (hd : DirectedOn (Function.onFun (fun (x1 x2 : Set α) => x1 ⊆ x2) s) t) : μ (⋃ i ∈ t, s i) = ⨆ i ∈ t, μ (s i)

theorem Directed.measure_iInter {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : ι → Set α} [Countable ι] (h : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) (hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) s) (hfin : ∃ (i : ι), μ (s i) ≠ ⊤) : μ (⋂ (i : ι), s i) = ⨅ (i : ι), μ (s i)

Continuity from above: the measure of the intersection of a directed downwards countable family of measurable sets is the infimum of the measures.

theorem Monotone.measure_iInter {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : ι → Set α} [Preorder ι] [IsCodirectedOrder ι] [Filter.atBot.IsCountablyGenerated] (hs : Monotone s) (hsm : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) (hfin : ∃ (i : ι), μ (s i) ≠ ⊤) : μ (⋂ (i : ι), s i) = ⨅ (i : ι), μ (s i)

Continuity from above: the measure of the intersection of a monotone family of measurable sets indexed by a type with countably generated atBot filter is equal to the infimum of the measures.

theorem MeasureTheory.measure_iInter_of_ae_monotone {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {s : ι → Set α} [Preorder ι] [IsCodirectedOrder ι] [Filter.atBot.IsCountablyGenerated] (hs : ∀ᵐ (ω : α) ∂μ, Monotone fun (x : ι) => ω ∈ s x) (hsm : ∀ (i : ι), NullMeasurableSet (s i) μ) (hfin : ∃ (i : ι), μ (s i) ≠ ⊤) : μ (⋂ (i : ι), s i) = ⨅ (i : ι), μ (s i)

Continuity from above (a.e. version): the measure of the intersection of a family of sets that is almost everywhere monotone is equal to the infimum of the measures.

theorem Antitone.measure_iInter {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : ι → Set α} [Preorder ι] [IsDirectedOrder ι] [Filter.atTop.IsCountablyGenerated] (hs : Antitone s) (hsm : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) (hfin : ∃ (i : ι), μ (s i) ≠ ⊤) : μ (⋂ (i : ι), s i) = ⨅ (i : ι), μ (s i)

Continuity from above: the measure of the intersection of an antitone family of measurable sets indexed by a type with countably generated atTop filter is equal to the infimum of the measures.

theorem MeasureTheory.measure_iInter_of_ae_antitone {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {s : ι → Set α} [Preorder ι] [IsDirectedOrder ι] [Filter.atTop.IsCountablyGenerated] (hs : ∀ᵐ (ω : α) ∂μ, Antitone fun (x : ι) => ω ∈ s x) (hsm : ∀ (i : ι), NullMeasurableSet (s i) μ) (hfin : ∃ (i : ι), μ (s i) ≠ ⊤) : μ (⋂ (i : ι), s i) = ⨅ (i : ι), μ (s i)

Continuity from above (a.e. version): the measure of the intersection of a family of sets that is almost everywhere antitone is equal to the infimum of the measures.

theorem MeasureTheory.measure_iInter_eq_iInf_measure_iInter_le {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {s : ι → Set α} [Countable ι] [Preorder ι] [IsDirectedOrder ι] (h : ∀ (i : ι), NullMeasurableSet (s i) μ) (hfin : ∃ (i : ι), μ (s i) ≠ ⊤) : μ (⋂ (i : ι), s i) = ⨅ (i : ι), μ (⋂ (j : ι), ⋂ (_ : j ≤ i), s j)

Continuity from above: the measure of the intersection of a sequence of measurable sets is the infimum of the measures of the partial intersections.

theorem MeasureTheory.tendsto_measure_iUnion_atTop {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {s : ι → Set α} [Preorder ι] [Filter.atTop.IsCountablyGenerated] (hm : Monotone s) : Filter.Tendsto (⇑μ ∘ s) Filter.atTop (nhds (μ (⋃ (n : ι), s n)))

Continuity from below: the measure of the union of an increasing sequence of (not necessarily measurable) sets is the limit of the measures.

theorem MeasureTheory.tendsto_measure_iUnion_atBot {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {s : ι → Set α} [Preorder ι] [Filter.atBot.IsCountablyGenerated] (hm : Antitone s) : Filter.Tendsto (⇑μ ∘ s) Filter.atBot (nhds (μ (⋃ (n : ι), s n)))

theorem MeasureTheory.tendsto_measure_iUnion_accumulate {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {s : ι → Set α} [Preorder ι] [Filter.atTop.IsCountablyGenerated] : Filter.Tendsto (fun (i : ι) => μ (Set.accumulate s i)) Filter.atTop (nhds (μ (⋃ (i : ι), s i)))

Continuity from below: the measure of the union of a sequence of (not necessarily measurable) sets is the limit of the measures of the partial unions.

theorem MeasureTheory.tendsto_measure_iInter_atTop {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {s : ι → Set α} [Preorder ι] [Filter.atTop.IsCountablyGenerated] (hs : ∀ (i : ι), NullMeasurableSet (s i) μ) (hm : Antitone s) (hf : ∃ (i : ι), μ (s i) ≠ ⊤) : Filter.Tendsto (⇑μ ∘ s) Filter.atTop (nhds (μ (⋂ (n : ι), s n)))

Continuity from above: the measure of the intersection of a decreasing sequence of measurable sets is the limit of the measures.

theorem MeasureTheory.tendsto_measure_iInter_atBot {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {s : ι → Set α} [Preorder ι] [Filter.atBot.IsCountablyGenerated] (hs : ∀ (i : ι), NullMeasurableSet (s i) μ) (hm : Monotone s) (hf : ∃ (i : ι), μ (s i) ≠ ⊤) : Filter.Tendsto (⇑μ ∘ s) Filter.atBot (nhds (μ (⋂ (n : ι), s n)))

Continuity from above: the measure of the intersection of an increasing sequence of measurable sets is the limit of the measures.

theorem MeasureTheory.tendsto_measure_iInter_le {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {s : ι → Set α} [Countable ι] [Preorder ι] (hm : ∀ (i : ι), NullMeasurableSet (s i) μ) (hf : ∃ (i : ι), μ (s i) ≠ ⊤) : Filter.Tendsto (fun (i : ι) => μ (⋂ (j : ι), ⋂ (_ : j ≤ i), s j)) Filter.atTop (nhds (μ (⋂ (i : ι), s i)))

Continuity from above: the measure of the intersection of a sequence of measurable sets such that one has finite measure is the limit of the measures of the partial intersections.

theorem MeasureTheory.exists_measure_iInter_lt {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {s : ι → Set α} [SemilatticeSup ι] [Countable ι] (hm : ∀ (i : ι), NullMeasurableSet (s i) μ) {ε : ENNReal} (hε : 0 < ε) (hfin : ∃ (i : ι), μ (s i) ≠ ⊤) (hfem : ⋂ (n : ι), s n = ∅) : ∃ (m_1 : ι), μ (⋂ (n : ι), ⋂ (_ : n ≤ m_1), s n) < ε

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

theorem MeasureTheory.tendsto_measure_biInter_gt {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {s : ι → Set α} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] {a : ι} (hs : ∀ r > a, NullMeasurableSet (s r) μ) (hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j) (hf : ∃ r > a, μ (s r) ≠ ⊤) : Filter.Tendsto (⇑μ ∘ s) (nhdsWithin a (Set.Ioi a)) (nhds (μ (⋂ (r : ι), ⋂ (_ : r > a), s r)))

The measure of the intersection of a decreasing sequence of measurable sets indexed by a linear order with first countable topology is the limit of the measures.