VitaliFamily.covering
theorem VitaliFamily.covering :
∀ {α : Type u_1} [inst : MetricSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
(self : VitaliFamily μ) (s : Set α) (f : α → Set (Set α)),
(∀ x ∈ s, f x ⊆ self.setsAt x) →
(∀ x ∈ s, ∀ ε > 0, ∃ a ∈ f x, a ⊆ Metric.closedBall x ε) →
∃ t,
(∀ p ∈ t, p.1 ∈ s) ∧
(t.PairwiseDisjoint fun p => p.2) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ ↑↑μ (s \ ⋃ p ∈ t, p.2) = 0
This theorem, named `VitaliFamily.covering`, addresses a situation in a metric space. Given a set `s` (which might not be measurable) in a metric space, and for each point `x` in `s` a subfamily `f x` of `setsAt x` that includes sets with arbitrarily small diameters, it asserts that we can extract a disjoint subfamily that covers nearly all of `s` in a measure-theoretic sense.
More specifically, under the conditions that `f x` is a subset of `setsAt x` for all `x` in `s`, and that for every `x` in `s` and any real number `ε` greater than 0, there exists a set `a` in `f x` that is a subset of the closed ball centered at `x` with radius `ε`. The theorem then asserts the existence of a subfamily `t` with the properties that each pair `(p.1, p.2)` in `t` has `p.1` in `s`, `t` is pairwise disjoint on the second element of the pair, `p.2` is in `f p.1` for each pair in `t`, and the measure of the set difference between `s` and the union over all `p.2` in `t` is zero. In other words, `t` is a disjoint subfamily that covers almost all of `s`, apart from a subset of measure zero.
More concisely: Given a set in a metric space and for each point a subfamily of sets with arbitrarily small diameters, there exists a disjoint subfamily that covers the set apart from a subset of measure zero.
|
VitaliFamily.FineSubfamilyOn.covering_disjoint
theorem VitaliFamily.FineSubfamilyOn.covering_disjoint :
∀ {α : Type u_1} [inst : MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {v : VitaliFamily μ}
{f : α → Set (Set α)} {s : Set α} (h : v.FineSubfamilyOn f s), h.index.PairwiseDisjoint h.covering
The theorem `VitaliFamily.FineSubfamilyOn.covering_disjoint` states that for any fine subfamily `h` on a set `s` under function `f` with respect to a Vitali family `v`, the index of `h` is pairwise disjoint under the covering of `h`. In simpler terms, it says that the sets in the family, which form a covering of almost every element in `s`, are pairwise disjoint. This pairwise disjoint property ensures that no two distinct sets in this covering overlap. This theorem holds in the context of a metric space and a measurable space, with a measure defined on it.
More concisely: In a metric measurable space, the index sets of a pairwise disjoint fine subfamily on a set, which covers almost every element with respect to a Vitali family, are disjoint.
|
VitaliFamily.tendsto_filterAt_iff
theorem VitaliFamily.tendsto_filterAt_iff :
∀ {α : Type u_1} [inst : MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ)
{ι : Type u_2} {l : Filter ι} {f : ι → Set α} {x : α},
Filter.Tendsto f l (v.filterAt x) ↔
(∀ᶠ (i : ι) in l, f i ∈ v.setsAt x) ∧ ∀ ε > 0, ∀ᶠ (i : ι) in l, f i ⊆ Metric.closedBall x ε
This theorem states that for any type `α` equipped with a metric space structure and a measurable space structure, any measure `μ` on `α`, any Vitali family `v` defined on `μ`, any type `ι` equipped with a filter structure `l`, any function `f` from `ι` to `Set α`, and any point `x` in `α`, the function `f` tends to the filter at `x` in the Vitali family `v` if and only if the following two conditions hold:
1) For almost every `i` in `l`, `f(i)` belongs to the sets at `x` in `v`,
2) For any positive real number `ε`, for almost every `i` in `l`, `f(i)` is contained in the closed ball with radius `ε` around `x`.
Here, "almost every" refers to the filter version of "almost everywhere", meaning that the condition holds outside a set of measures zero, and the "closed ball" refers to the set of all points whose distance to `x` is less than or equal to `ε`.
More concisely: A function from a filter to a metric space tends to a point in a Vitali family with respect to a measure if and only if it lies in the sets at that point for almost every filter element and is contained in the closed ball around that point for almost every filter element with positive radius.
|
VitaliFamily.nonempty_interior
theorem VitaliFamily.nonempty_interior :
∀ {α : Type u_1} [inst : MetricSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
(self : VitaliFamily μ) (x : α), ∀ s ∈ self.setsAt x, (interior s).Nonempty
The theorem `VitaliFamily.nonempty_interior` asserts that for any type `α` equipped with a metric space structure, a measurable space structure, and a measure `μ`, for any Vitali family with respect to the measure `μ`, and any element `x` of the type `α`, all sets `s` in the family of sets at `x` have a non-empty interior. In other words, within any metric and measurable space, every set in a Vitali family associated with a particular point contains at least one open set.
More concisely: In a metric and measurable space equipped with a measure, every Vitali family at a point contains at least one open set with non-empty interior.
|
VitaliFamily.FineSubfamilyOn.exists_disjoint_covering_ae
theorem VitaliFamily.FineSubfamilyOn.exists_disjoint_covering_ae :
∀ {α : Type u_1} [inst : MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {v : VitaliFamily μ}
{f : α → Set (Set α)} {s : Set α},
v.FineSubfamilyOn f s →
∃ t,
(∀ p ∈ t, p.1 ∈ s) ∧
(t.PairwiseDisjoint fun p => p.2) ∧ (∀ p ∈ t, p.2 ∈ v.setsAt p.1 ∩ f p.1) ∧ ↑↑μ (s \ ⋃ p ∈ t, p.2) = 0
The theorem `VitaliFamily.FineSubfamilyOn.exists_disjoint_covering_ae` states that for any type `α` equipped with a metric space structure, a measurable space `m0`, a measure `μ`, a Vitali family `v`, a function `f` mapping from `α` to a set of subsets of `α`, and a set `s` of `α`, if the Vitali family `v` is a fine subfamily on `f` and `s`, then there exists a set `t` such that every pair `(p.1, p.2)` in `t` satisfies the following conditions:
1. `p.1` is an element of `s`.
2. The set `t` is pairwise disjoint under the function `p => p.2`.
3. `p.2` is an element of the intersection between the set `v.setsAt p.1` and `f p.1`.
4. The measure of the set difference between `s` and the union of `p.2` for all `p` in `t` is zero.
In other words, this theorem guarantees the existence of a disjoint covering set `t` for a given set `s` under certain conditions, and the set `s` without this covering set has measure zero.
More concisely: Given a metric space `α` with a measurable space `m0`, measure `μ`, Vitali family `v`, function `f` mapping from `α` to subsets of `α`, and set `s`, if `v` is a fine subfamily on `f` and `s`, then there exists a disjoint subfamily `t` of `v.setsAt(s)` such that the measure of `s \ (∪{f(x).inter `v.setsAt x | x ∈ t})` is zero.
|
VitaliFamily.nontrivial
theorem VitaliFamily.nontrivial :
∀ {α : Type u_1} [inst : MetricSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
(self : VitaliFamily μ) (x : α), ∀ ε > 0, ∃ s ∈ self.setsAt x, s ⊆ Metric.closedBall x ε
This theorem, named `VitaliFamily.nontrivial`, states that for any type `α` that is a Metric Space with a given Measurable Space and a Measure Theory Measure, and for any Vitali Family defined on this Measure, if you pick any point `x` in this space and any strictly positive real number `ε`, there exists a set `s` from the family of sets at `x` (i.e., `self.setsAt x`) which is entirely contained within the closed ball of radius `ε` centered at `x`. In other words, for any closed ball you create around `x`, you can find a set from the Vitali Family that fits entirely within this ball.
More concisely: For any Metric Space `α` with Measurable Space and Measure Theory Measure, and any Vitali Family on `α` at a point `x`, there exists a set in the family containing `x` that is entirely included in the closed ball of radius `ε` around `x`.
|
VitaliFamily.measurableSet
theorem VitaliFamily.measurableSet :
∀ {α : Type u_1} [inst : MetricSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
(self : VitaliFamily μ) (x : α), ∀ s ∈ self.setsAt x, MeasurableSet s
This theorem, denoted as `VitaliFamily.measurableSet`, asserts that for any given Vitali family `self`, which is associated with a measure `μ`, and any given element `x` of a metric space `α` equipped with a measurable space structure `m`, all sets `s` belonging to the family of sets at `x` (`self.setsAt x`) are measurable. In other words, every set that is part of the collection of sets generated by the Vitali family at a particular point in the metric space is a measurable set.
More concisely: For any Vitali family `self` over measure `μ` on metric space `α` with measurable space structure `m`, every set in `self.setsAt x` is measurable for all `x` in `α`.
|
VitaliFamily.filterAt_basis_closedBall
theorem VitaliFamily.filterAt_basis_closedBall :
∀ {α : Type u_1} [inst : MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ)
(x : α), (v.filterAt x).HasBasis (fun x => 0 < x) fun x_1 => {a | a ∈ v.setsAt x ∧ a ⊆ Metric.closedBall x x_1}
This theorem states that for any vitali family `v` and any element `x` of type `α` in a metric space with a measurable space and a measure, the filter at `x` created by `v` has a basis consisting of the sets of `v` at `x` that are contained within a closed ball centered at `x` with a positive radius. The basis condition provided is that the radius of the closed ball is positive. In other words, any neighborhood of `x` in the generated filter can be represented by a union of sets of `v` at `x` that are wholly contained in some closed ball around `x` with a positive radius.
More concisely: For any vitali family `v` and element `x` in a metric space with a measurable space and measure, the filter at `x` generated by `v` has a basis consisting of sets of `v` at `x` contained in closed balls centered at `x` with positive radii.
|