MeasureTheory.FiniteMeasure.limsup_measure_closed_le_of_tendsto
theorem MeasureTheory.FiniteMeasure.limsup_measure_closed_le_of_tendsto :
∀ {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω]
[inst_2 : HasOuterApproxClosed Ω] [inst_3 : OpensMeasurableSpace Ω] {μ : MeasureTheory.FiniteMeasure Ω}
{μs : ι → MeasureTheory.FiniteMeasure Ω},
Filter.Tendsto μs L (nhds μ) → ∀ {F : Set Ω}, IsClosed F → Filter.limsup (fun i => ↑↑↑(μs i) F) L ≤ ↑↑↑μ F
This theorem is an implication of the Portmanteau theorem in the context of measure theory. It states that if a sequence of finite measures converges weakly (in the sense that the sequence tends to the limit in the neighborhood filter), then for any closed set, the limit superior (or upper limit) of the measures of that closed set is less than or equal to the measure of the closed set under the limit measure. Essentially, this theorem captures the idea that under weak convergence of finite measures, the limit superior of the measures over any closed set will not surpass the measure assigned to that set by the limit measure.
More concisely: If a sequence of finite measures converges weakly, then for any closed set, the limit superior of their measures is less than or equal to the measure of the set under the limit measure.
|
MeasureTheory.ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto
theorem MeasureTheory.ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto :
∀ {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω]
[inst_2 : OpensMeasurableSpace Ω] [inst_3 : HasOuterApproxClosed Ω] {μ : MeasureTheory.ProbabilityMeasure Ω}
{μs : ι → MeasureTheory.ProbabilityMeasure Ω},
Filter.Tendsto μs L (nhds μ) →
∀ {E : Set Ω},
(fun s => (↑↑↑μ s).toNNReal) (frontier E) = 0 →
Filter.Tendsto (fun i => (fun s => (↑↑↑(μs i) s).toNNReal) E) L (nhds ((fun s => (↑↑↑μ s).toNNReal) E))
The theorem `MeasureTheory.ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto` states that for any type of sample space `Ω`, a type of index `ι`, a filter `L` over the index type, given any probability measure `μ` on the sample space and a sequence of probability measures `μs` indexed by `ι`, if the sequence of measures `μs` converges weakly towards the measure `μ` as per the topology of `L` (expressed by `Filter.Tendsto μs L (nhds μ)`), then for any Borel set `E` in the sample space, if the boundary of the set (the frontier) carries no probability mass under the limit measure `μ` (expressed by `(fun s => (↑↑↑μ s).toNNReal) (frontier E) = 0`), it follows that the limit of the measures of the set `E` under the sequence `μs` is equal to the measure of the set `E` under the limit measure `μ` (expressed by `Filter.Tendsto (fun i => (fun s => (↑↑↑(μs i) s).toNNReal) E) L (nhds ((fun s => (↑↑↑μ s).toNNReal) E))`). This is a statement of one implication of the portmanteau theorem in the context of weak convergence of probability measures.
More concisely: If a sequence of probability measures on a sample space converges weakly to a limit measure and the boundary of any Borel set carries zero probability mass under the limit measure, then the limit of the measures of that set under the sequence is equal to the measure of the set under the limit measure. (Portmanteau theorem for weak convergence of probability measures)
|
MeasureTheory.tendsto_of_forall_isOpen_le_liminf
theorem MeasureTheory.tendsto_of_forall_isOpen_le_liminf :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
{μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ℕ → MeasureTheory.ProbabilityMeasure Ω},
(∀ (G : Set Ω),
IsOpen G →
(fun s => (↑↑↑μ s).toNNReal) G ≤
Filter.liminf (fun i => (fun s => (↑↑↑(μs i) s).toNNReal) G) Filter.atTop) →
Filter.Tendsto (fun i => μs i) Filter.atTop (nhds μ)
This theorem, known as one implication of the Portmanteau theorem, states that in a measurable and topological space, which is equipped with the topology of open sets, if for every open set `G` the measure `μ(G)` is less than or equal to the limit inferior (as `n` approaches infinity) of the measures `μs_n(G)`, then the sequence of measures `μs_n` converges weakly to the measure `μ`. In other words, if the measure of every open set under `μ` is not greater than the eventual lower bound of the measures of the same set under `μs_n`, then as `n` gets larger and larger, the measures `μs_n` tend to the measure `μ`.
More concisely: If for every open set, the measure of the set under the limit measure is less than or equal to the lim inf of the measures under the sequence of measures, then the sequence converges weakly to the limit measure.
|
MeasureTheory.le_measure_liminf_of_limsup_measure_compl_le
theorem MeasureTheory.le_measure_liminf_of_limsup_measure_compl_le :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure Ω}
{μs : ι → MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsProbabilityMeasure μ]
[inst_2 : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] {E : Set Ω},
MeasurableSet E →
Filter.limsup (fun i => ↑↑(μs i) Eᶜ) L ≤ ↑↑μ Eᶜ → ↑↑μ E ≤ Filter.liminf (fun i => ↑↑(μs i) E) L
The theorem `MeasureTheory.le_measure_liminf_of_limsup_measure_compl_le` states that for any type `Ω` with a measurable space structure, a type `ι`, a filter `L` on `ι`, a probability measure `μ` on `Ω`, a sequence of probability measures `μs` indexed by `ι`, and a measurable set `E` of `Ω`, if the limit superior (limsup) of the measures of the complement of `E` under the sequence of measures `μs` is less than or equal to the measure of the complement of `E` under the measure `μ`, then the measure of `E` under `μ` is less than or equal to the limit inferior (liminf) of the measures of `E` under the sequence of measures `μs`. This theorem provides a relationship between the measure of a set and the liminf and limsup measures of its complement under a sequence of probability measures.
More concisely: If the limit superior of the complement measures of a measurable set under a sequence of probability measures is less than or equal to the complement measure under the base measure, then the measure of the set is less than or equal to the limit inferior of its measures under the sequence.
|
MeasureTheory.le_measure_compl_liminf_of_limsup_measure_le
theorem MeasureTheory.le_measure_compl_liminf_of_limsup_measure_le :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure Ω}
{μs : ι → MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsProbabilityMeasure μ]
[inst_2 : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] {E : Set Ω},
MeasurableSet E →
Filter.limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E → ↑↑μ Eᶜ ≤ Filter.liminf (fun i => ↑↑(μs i) Eᶜ) L
The **Portmanteau theorem** in Measure Theory states that for a given measurable space `Ω`, a filter `L` over an index set `ι`, a measure `μ` on `Ω` that is a probability measure, a sequence of measures `μs` indexed by `ι` where each measure in the sequence is a probability measure, and a measurable set `E` in `Ω`, if the limit superior of the measures of `E` under the sequence of measures `μs` is less than or equal to the measure of `E` under `μ`, then the measure of the complement of `E` under `μ` is less than or equal to the limit inferior of the measures of the complement of `E` under the sequence of measures `μs`.
More concisely: If `μ` is a probability measure on measurable space `(Ω, Σ)`, `L` is a filter over index set `ι`, `E ∈ Σ`, `μs` is a sequence of probability measures on `(Ω, Σ)`, and `limsup μs(E) ≤ μ(E)`, then `liminf μs(E^c) ≥ μ(E^c)`.
|
MeasureTheory.tendsto_measure_of_null_frontier
theorem MeasureTheory.tendsto_measure_of_null_frontier :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
{ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure Ω} {μs : ι → MeasureTheory.Measure Ω}
[inst_3 : MeasureTheory.IsProbabilityMeasure μ] [inst_4 : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)],
(∀ (G : Set Ω), IsOpen G → ↑↑μ G ≤ Filter.liminf (fun i => ↑↑(μs i) G) L) →
∀ {E : Set Ω}, ↑↑μ (frontier E) = 0 → Filter.Tendsto (fun i => ↑↑(μs i) E) L (nhds (↑↑μ E))
This is one implication of the Portmanteau theorem in the field of measure theory. It states that for a sequence of Borel probability measures `{μs i}`, if the lower limit (`liminf`) of the measures of any open set is greater than or equal to the measure of that open set under a candidate limit measure `μ`, then for any set `E` whose frontier (the set of points between the closure and interior of `E`) carries no probability mass under the candidate limit measure `μ` (i.e., `μ (frontier E) = 0`), the measures of set `E` under the sequence `{μs i}` converge to its measure under the candidate limit measure `μ`. This convergence is in the sense of the filter `L`, and is described by the `Filter.Tendsto` predicate, which states that the image of a set under a function becomes arbitrarily close to another set under a filter.
More concisely: If a sequence of Borel probability measures `{μs i}` has a candidate limit measure `μ` such that `liminf μs i (open set) ≥ μ (open set)` for all open sets and `μ (frontier E) = 0`, then `{μs i} Filter.Tendsto μ E`.
|
MeasureTheory.ProbabilityMeasure.limsup_measure_closed_le_of_tendsto
theorem MeasureTheory.ProbabilityMeasure.limsup_measure_closed_le_of_tendsto :
∀ {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω]
[inst_2 : OpensMeasurableSpace Ω] [inst_3 : HasOuterApproxClosed Ω] {μ : MeasureTheory.ProbabilityMeasure Ω}
{μs : ι → MeasureTheory.ProbabilityMeasure Ω},
Filter.Tendsto μs L (nhds μ) → ∀ {F : Set Ω}, IsClosed F → Filter.limsup (fun i => ↑↑↑(μs i) F) L ≤ ↑↑↑μ F
This theorem, one implication of the Portmanteau theorem, establishes that if a sequence of probability measures, denoted by `μs`, weakly converges to a limit probability measure `μ` (as specified by the `Filter.Tendsto` predicate), then for any closed set `F`, the limsup (limit superior) of the measures of that closed set under the sequence of probability measures is less than or equal to the measure of the closed set under the limit probability measure `μ`. In other words, the largest possible limit of measures of the set `F` under the sequence of measures `μs` is no greater than the measure of `F` under the limit measure `μ`. This theorem holds in the context of a measurable space `Ω`, which additionally has the structure of a pseudo-emetric space and an open measurable space, and where any set can be approximated from the outside by a closed set.
More concisely: If a sequence of probability measures weakly converges to a limit measure, then the limsup of the measures of any closed set under the sequence is less than or equal to the measure of that set under the limit measure.
|
MeasureTheory.ProbabilityMeasure.le_liminf_measure_open_of_tendsto
theorem MeasureTheory.ProbabilityMeasure.le_liminf_measure_open_of_tendsto :
∀ {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω]
[inst_2 : OpensMeasurableSpace Ω] [inst_3 : HasOuterApproxClosed Ω] {μ : MeasureTheory.ProbabilityMeasure Ω}
{μs : ι → MeasureTheory.ProbabilityMeasure Ω},
Filter.Tendsto μs L (nhds μ) → ∀ {G : Set Ω}, IsOpen G → ↑↑↑μ G ≤ Filter.liminf (fun i => ↑↑↑(μs i) G) L
This theorem is an implication of the Portmanteau theorem in measure theory. It states that if a sequence of probability measures converges weakly towards a limit probability measure, then the lower limit (liminf) of the measures of any open set under the sequence of probability measures is at least as large as the measure of that open set under the limit probability measure. In other words, the measure of the open set in the limit probability measure is less than or equal to the liminf of the measures of that open set under the sequence of converging probability measures.
More concisely: If a sequence of probability measures converges weakly to a limit measure, then the liminf of the measures of any open set is greater than or equal to the measure of that open set under the limit measure. (Note that the statement you provided has the inequality reversed.)
|
MeasureTheory.limsup_measure_closed_le_of_forall_tendsto_measure
theorem MeasureTheory.limsup_measure_closed_le_of_forall_tendsto_measure :
∀ {Ω : Type u_2} {ι : Type u_3} {L : Filter ι} [inst : L.NeBot] [inst : MeasurableSpace Ω]
[inst_1 : PseudoEMetricSpace Ω] [inst_2 : OpensMeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
[inst_3 : MeasureTheory.IsFiniteMeasure μ] {μs : ι → MeasureTheory.Measure Ω},
(∀ {E : Set Ω}, MeasurableSet E → ↑↑μ (frontier E) = 0 → Filter.Tendsto (fun i => ↑↑(μs i) E) L (nhds (↑↑μ E))) →
∀ (F : Set Ω), IsClosed F → Filter.limsup (fun i => ↑↑(μs i) F) L ≤ ↑↑μ F
This theorem, known as one implication of the Portmanteau theorem in measure theory, states that if for every Borel set E, whose boundary does not carry any probability mass under a candidate limit probability measure μ, we have that the measures μsᵢ(E) converge to μ(E), then for every closed set F, the limsup condition holds: the limit superior of μsᵢ(F) is less than or equal to μ(F). This theorem is applicable in a space Ω that is a pseudo e-metric space and also an open measurable space, with measures μ and a sequence of measures μs indexed by ι. The theorem assumes that the filter L over the index set ι is not trivial (i.e., it does not contain all sets). The measure μ is further assumed to be a finite measure.
More concisely: If every Borel set in a pseudo-metric, open measurable space with a finite, non-trivial measure μ has a boundary carrying no probability mass under a sequence of measures μsi, then for every closed set F, the limit superior of μsi(F) is less than or equal to μ(F).
|
MeasureTheory.limsup_measure_closed_le_iff_liminf_measure_open_ge
theorem MeasureTheory.limsup_measure_closed_le_iff_liminf_measure_open_ge :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
{ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure Ω} {μs : ι → MeasureTheory.Measure Ω}
[inst_3 : MeasureTheory.IsProbabilityMeasure μ] [inst_4 : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)],
(∀ (F : Set Ω), IsClosed F → Filter.limsup (fun i => ↑↑(μs i) F) L ≤ ↑↑μ F) ↔
∀ (G : Set Ω), IsOpen G → ↑↑μ G ≤ Filter.liminf (fun i => ↑↑(μs i) G) L
The theorem `MeasureTheory.limsup_measure_closed_le_iff_liminf_measure_open_ge` establishes a relation between two conditions in the context of a sequence of Borel probability measures. The two conditions are:
1. For any closed set `F`, the limit superior (limsup) of the measures of `F` under the sequence of measures is less than or equal to the measure of `F` under a target probability measure, `μ`.
2. For any open set `G`, the measure of `G` under the target measure `μ` is less than or equal to the limit inferior (liminf) of the measures of `G` under the sequence of measures.
The theorem states that these two conditions are equivalent. That is, the first condition holds if and only if the second condition holds. This theorem is a part of the Portmanteau theorem in measure theory, which provides several equivalent conditions for the convergence of a sequence of probability measures.
More concisely: The theorem `MeasureTheory.limsup_measure_closed_le_iffeq_liminf_measure_open` states that a sequence of Borel probability measures converges to a target measure if and only if for every closed set, the limit superior of its measure is less than or equal to the target measure, and for every open set, the target measure is less than or equal to the limit inferior of its measures.
|
MeasureTheory.le_liminf_measure_open_of_forall_tendsto_measure
theorem MeasureTheory.le_liminf_measure_open_of_forall_tendsto_measure :
∀ {Ω : Type u_2} {ι : Type u_3} {L : Filter ι} [inst : L.NeBot] [inst : MeasurableSpace Ω]
[inst_1 : PseudoEMetricSpace Ω] [inst_2 : OpensMeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
[inst_3 : MeasureTheory.IsProbabilityMeasure μ] {μs : ι → MeasureTheory.Measure Ω}
[inst_4 : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)],
(∀ {E : Set Ω}, MeasurableSet E → ↑↑μ (frontier E) = 0 → Filter.Tendsto (fun i => ↑↑(μs i) E) L (nhds (↑↑μ E))) →
∀ (G : Set Ω), IsOpen G → ↑↑μ G ≤ Filter.liminf (fun i => ↑↑(μs i) G) L
This theorem is one implication of the portmanteau theorem in measure theory. It states that given a set of measures indexed by some type `ι`, and a limit measure `μ`, if for all measurable sets `E` where the boundary of `E` carries no probability mass under the measure `μ`, the measures of `E` under the indexed measures converge to the measure of `E` under `μ`, then for all open sets `G`, the measure of `G` under `μ` is less than or equal to the limit inferior of the measures of `G` under the indexed measures. In other words, assuming the convergence condition that for every Borel set `E` whose boundary does not carry any probability mass under a candidate limit probability measure `μ`, the measures `μsᵢ(E)` converge to `μ(E)`, then for every open set `G`, it holds that `μ(G)` is less than or equal to the limit inferior of the measures `μsᵢ(G)`.
More concisely: Given a set of measures indexed by type `ι`, and a limit measure `μ`, if for all measurable sets `E` with no boundary mass under `μ`, the measures `μsᵢ(E)` converge to `μ(E)`, then for every open set `G`, `μ(G)` is less than or equal to the limit inferior of the `μsᵢ(G)`.
|