MeasureTheory.levyProkhorovDist_triangle
theorem MeasureTheory.levyProkhorovDist_triangle :
∀ {Ω : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
(μ ν κ : MeasureTheory.Measure Ω) [inst_3 : MeasureTheory.IsFiniteMeasure μ]
[inst_4 : MeasureTheory.IsFiniteMeasure ν] [inst_5 : MeasureTheory.IsFiniteMeasure κ],
MeasureTheory.levyProkhorovDist μ κ ≤ MeasureTheory.levyProkhorovDist μ ν + MeasureTheory.levyProkhorovDist ν κ
The theorem `MeasureTheory.levyProkhorovDist_triangle` states that for any three finite measures `μ`, `ν`, and `κ` on a measurable space `Ω` equipped with a pseudo emetric structure, the Lévy-Prokhorov distance between `μ` and `κ` is less than or equal to the sum of the Lévy-Prokhorov distance between `μ` and `ν` and the Lévy-Prokhorov distance between `ν` and `κ`. This is a manifestation of the triangle inequality in the context of the Lévy-Prokhorov distance between measures.
More concisely: The Lévy-Prokhorov distance between any three finite measures on a pseudo metric space is maximally increased by passing through a third measure, i.e., the triangle inequality holds for Lévy-Prokhorov distances.
|
MeasureTheory.levyProkhorovDist_self
theorem MeasureTheory.levyProkhorovDist_self :
∀ {Ω : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] (μ : MeasureTheory.Measure Ω),
MeasureTheory.levyProkhorovDist μ μ = 0
The theorem `MeasureTheory.levyProkhorovDist_self` states that for any measure space `Ω` equipped with a pseudometric, the Lévy-Prokhorov distance of any measure `μ` to itself is equal to zero. In mathematical terms, for all `μ`, we have `d(μ, μ) = 0`, where `d` denotes the Lévy-Prokhorov distance.
More concisely: The Lévy-Prokhorov distance of a measure to itself is zero for any measure space equipped with a pseudometric.
|
Mathlib.MeasureTheory.Measure.LevyProkhorovMetric._auxLemma.1
theorem Mathlib.MeasureTheory.Measure.LevyProkhorovMetric._auxLemma.1 :
∀ {α : Type u} [inst : LE α] [inst_1 : OrderTop α] {a : α}, (a ≤ ⊤) = True
This theorem, named `Mathlib.MeasureTheory.Measure.LevyProkhorovMetric._auxLemma.1`, states that for any type `α` that has a less than or equal to (`LE`) relation and a greatest element (`OrderTop`), any element `a` of this type is always less than or equal to the top element (`⊤`). This is always true regardless of the specific type `α` or the element `a` selected.
More concisely: For any type `α` with a LE relation and a greatest element `⊤`, every element `a` in `α` satisfies `a ≤ ⊤`.
|
MeasureTheory.levyProkhorovDist_comm
theorem MeasureTheory.levyProkhorovDist_comm :
∀ {Ω : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] (μ ν : MeasureTheory.Measure Ω),
MeasureTheory.levyProkhorovDist μ ν = MeasureTheory.levyProkhorovDist ν μ
The theorem `MeasureTheory.levyProkhorovDist_comm` states that for any measurable space `Ω` and any pseudo emetric space structure on `Ω`, for any two measures `μ` and `ν` on `Ω`, the Lévy-Prokhorov distance between `μ` and `ν` is the same as the Lévy-Prokhorov distance between `ν` and `μ`. In other words, the Lévy-Prokhorov distance is commutative with respect to the measures.
The Lévy-Prokhorov distance is defined as the infimum of all `r ≥ 0` such that for all measurable sets `B`, `μ B ≤ ν Bᵣ + r` and `ν B ≤ μ Bᵣ + r`, where `Bᵣ` denotes the `r`-enlargement of `B`.
More concisely: The Lévy-Prokhorov distance between measures `μ` and `ν` on a measurable space `Ω` with a pseudo metric is equal to the Lévy-Prokhorov distance between `ν` and `μ`.
|