VitaliFamily.measure_limRatioMeas_top
theorem VitaliFamily.measure_limRatioMeas_top :
∀ {α : Type u_1} [inst : MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ)
[inst_1 : SecondCountableTopology α] [inst_2 : BorelSpace α] [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ]
{ρ : MeasureTheory.Measure α} [inst_4 : MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ),
↑↑μ {x | v.limRatioMeas hρ x = ⊤} = 0
This theorem states that for any type `α` that is a metric space with a measurable space `m0` and two locally finite measures `μ` and `ρ`, and given a Vitali Family `v` on `μ`, if `ρ` is absolutely continuous with respect to `μ`, then the set of points `x` in `α` for which the limit ratio measure (`v.limRatioMeas hρ x`) equals infinity (`⊤`) has measure `0` with respect to `μ`. This means, the measure of the set of points where the limit ratio measure is infinity is zero.
More concisely: If `α` is a metric space with a measurable space `m0`, `μ` and `ρ` are locally finite measures on `α` with `ρ` absolutely continuous with respect to `μ`, and `v` is a Vitali family on `μ`, then the set of points `x` in `α` where the limit ratio measure `v.limRatioMeas hρ x` equals `⊤` has measure `0` with respect to `μ`.
|
VitaliFamily.ae_tendsto_measure_inter_div
theorem VitaliFamily.ae_tendsto_measure_inter_div :
∀ {α : Type u_1} [inst : MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ)
[inst_1 : SecondCountableTopology α] [inst_2 : BorelSpace α] [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ]
(s : Set α), ∀ᵐ (x : α) ∂μ.restrict s, Filter.Tendsto (fun a => ↑↑μ (s ∩ a) / ↑↑μ a) (v.filterAt x) (nhds 1)
This theorem states that for a given set `s` in a metric space `α`, with a measure `μ` and a Vitali family `v` defined on it, the ratio of the measure of the intersection of `s` and `a` to the measure of `a` tends to `1` as `a` approaches a typical point of `s` along the Vitali family. This implies that almost every point of `s` is a Lebesgue density point for `s`, meaning that the density of `s` around almost every point is `1`. This is a general result and a stronger version for measurable sets is provided in another theorem named `ae_tendsto_measure_inter_div_of_measurableSet`.
More concisely: For a given set `s` in a metric space with measure `μ` and Vitali family `v`, the ratio of `μ(s ∩ a)` to `μ(a)` approaches 1 as `a` approaches any point in `s` through `v`. Thus, almost every point of `s` is a Lebesgue density point.
|
VitaliFamily.measure_le_of_frequently_le
theorem VitaliFamily.measure_le_of_frequently_le :
∀ {α : Type u_1} [inst : MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ)
[inst_1 : SecondCountableTopology α] [inst_2 : BorelSpace α] {ρ : MeasureTheory.Measure α}
(ν : MeasureTheory.Measure α) [inst_3 : MeasureTheory.IsLocallyFiniteMeasure ν],
ρ.AbsolutelyContinuous μ →
∀ (s : Set α), (∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ↑↑ρ a ≤ ↑↑ν a) → ↑↑ρ s ≤ ↑↑ν s
The theorem `VitaliFamily.measure_le_of_frequently_le` states that for a given point set `s` in a metric space `α`, if two measures `ρ` and `ν` satisfy the condition that for every point in `s`, there exist arbitrarily small sets in a Vitali family such that the measure `ρ` of these sets is less than or equal to the measure `ν`, and if measure `ρ` is absolutely continuous with respect to another measure `μ`, then the measure `ρ` of the entire set `s` is less than or equal to the measure `ν` of the set. This theorem assumes that `ν` is a locally finite measure, and the space `α` has a second-countable topology and is a Borel space.
More concisely: If two measures `ρ` and `ν` on a second-countable Borel space `α` satisfy the condition that for every point in a point set `s`, there exist arbitrarily small sets in a Vitali family with respect to `ρ` whose measures are less than or equal to `ν`, and `ρ` is absolutely continuous with respect to another measure `μ` and `ν` is locally finite, then `ρ`(s) ≤ `ν`(s).
|
VitaliFamily.ae_eventually_measure_zero_of_singular
theorem VitaliFamily.ae_eventually_measure_zero_of_singular :
∀ {α : Type u_1} [inst : MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ)
[inst_1 : SecondCountableTopology α] [inst_2 : BorelSpace α] [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ]
{ρ : MeasureTheory.Measure α} [inst_4 : MeasureTheory.IsLocallyFiniteMeasure ρ],
ρ.MutuallySingular μ → ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (v.filterAt x) (nhds 0)
This theorem states that if a measure `ρ` is singular with respect to another measure `μ`, then for almost every point `x` with respect to `μ`, the ratio of `ρ a` to `μ a` tends to zero as `a` tends to `x` along the Vitali family. The Vitali family is a specific selection of sets in the measure space `α`, and `a` is from these sets. The phrase "tends to zero" means that for any small positive number, there is a set in the Vitali family such that whenever `a` is from this set or a smaller set in the family, the ratio `ρ a / μ a` is less than that small positive number. This makes sense because `μ a` is eventually positive almost everywhere. The condition of "almost every `x` with respect to `μ`" means that the set of `x` for which this condition does not hold has `μ`-measure zero. The theorem requires that the space `α` is equipped with a metric and a topology that make it a second countable topological space and a Borel space, and the measures `μ` and `ρ` are assumed to be locally finite.
More concisely: If measure `ρ` is singular with respect to `μ`, then for almost every `x` in the second countable and Borel measure space `α` with respect to `μ`, the limit as `a` approaches `x` in the Vitali family is zero: `lim (ρ(a) / μ(a)) = 0`.
|
VitaliFamily.ae_tendsto_average_norm_sub
theorem VitaliFamily.ae_tendsto_average_norm_sub :
∀ {α : Type u_1} [inst : MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ)
{E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : SecondCountableTopology α] [inst_3 : BorelSpace α]
[inst_4 : MeasureTheory.IsLocallyFiniteMeasure μ] {f : α → E},
MeasureTheory.LocallyIntegrable f μ →
∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (nhds 0)
The Lebesgue differentiation theorem states that, for a Vitali family and a function `f` that is locally integrable, almost every point `x` in the domain (with respect to a given measure `μ`) has the property that the average of the norm of the difference between `f y` and `f x` over a set `a`, tends to zero as `a` shrinks to `x`. Here, the average is taken with respect to the measure `μ`, the set `a` is taken from the Vitali family's filter at `x`, and the term "almost every" is taken with respect to the measure `μ`. In mathematical notation, this is expressed as `∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (nhds 0)`.
More concisely: For a Vitali family and a locally integrable function `f`, almost every point `x` in the domain (with respect to a given measure `μ`) satisfies that the average difference `|f(y) - f(x)|` approaches zero as `y` approaches `x` with respect to `μ`.
|
VitaliFamily.eventually_measure_lt_top
theorem VitaliFamily.eventually_measure_lt_top :
∀ {α : Type u_1} [inst : MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ)
[inst_1 : MeasureTheory.IsLocallyFiniteMeasure μ] (x : α), ∀ᶠ (a : Set α) in v.filterAt x, ↑↑μ a < ⊤
This theorem, `VitaliFamily.eventually_measure_lt_top`, states that for any point `x` in a metric space `α`, given a Vitali family `v` associated with a measure `μ` on that space, if the measure `μ` is locally finite, then there exists a neighborhood around the point `x` such that all sets in this neighborhood derived from the Vitali family have finite measure. This is a straightforward result, as it follows from the local finiteness of the measure `μ`. In more mathematical terms, for all sets `a` in the filter at `x` (i.e., sets in the Vitali family around `x`), the measure of the set `a` is less than infinity.
More concisely: For any point `x` in a locally finite measure space `(α, μ)` and any Vitali family `v` on `α`, there exists a neighborhood of `x` such that all sets in the family have finite measure.
|
VitaliFamily.mul_measure_le_of_subset_lt_limRatioMeas
theorem VitaliFamily.mul_measure_le_of_subset_lt_limRatioMeas :
∀ {α : Type u_1} [inst : MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ)
[inst_1 : SecondCountableTopology α] [inst_2 : BorelSpace α] [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ]
{ρ : MeasureTheory.Measure α} [inst_4 : MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ)
{q : NNReal} {s : Set α}, s ⊆ {x | ↑q < v.limRatioMeas hρ x} → ↑q * ↑↑μ s ≤ ↑↑ρ s
This theorem, named `VitaliFamily.mul_measure_le_of_subset_lt_limRatioMeas`, states that for all elements of a type `α` equipped with a metric space structure, a measurable space structure `m0`, measures `μ` and `ρ` (where `ρ` is absolutely continuous with respect to `μ`), and a given Vitali family `v`, if for every element `x` in a set `s`, the property `q < v.limRatioMeas hρ x` holds (where `q` is a nonnegative real number), then the result of `q` times the measure of `s` under `μ` is less than or equal to the measure of `s` under `ρ`. This is under the conditions that `α` has a second countable topology, a Borel space structure, and that both `μ` and `ρ` are locally finite measures.
More concisely: For any second countable and Borel measurable space equipped with locally finite measures `μ` and `ρ` (with `ρ` absolutely continuous with respect to `μ`), if for every `x` in a measurable set `s`, the ratio of `ρ` to `μ` at `x` is greater than a constant `q`, then the product of `q` and the measure of `s` under `μ` is less than or equal to the measure of `s` under `ρ`.
|
VitaliFamily.measure_le_mul_of_subset_limRatioMeas_lt
theorem VitaliFamily.measure_le_mul_of_subset_limRatioMeas_lt :
∀ {α : Type u_1} [inst : MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ)
[inst_1 : SecondCountableTopology α] [inst_2 : BorelSpace α] [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ]
{ρ : MeasureTheory.Measure α} [inst_4 : MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ)
{p : NNReal} {s : Set α}, s ⊆ {x | v.limRatioMeas hρ x < ↑p} → ↑↑ρ s ≤ ↑p * ↑↑μ s
This theorem, `VitaliFamily.measure_le_mul_of_subset_limRatioMeas_lt`, states that for any metric space `α`, given a Vitali family `v` on a measurable space `α` with measures `μ` and `ρ`, where `ρ` is absolutely continuous with respect to `μ`, a nonnegative real number `p`, and a set `s` of type `α`, if `s` is a subset of the set of elements `x` such that the limit of the ratio measure of `x` under the Vitali family `v` with respect to `ρ` and `μ` is less than `p`, then the measure of `s` under `ρ` is less than or equal to `p` times the measure of `s` under `μ`.
This theorem generalizes a property of ratios of measures on individual elements of a metric space to sets in the metric space. If the ratio measure of every element in the set frequently falls below a certain threshold, then the measure of the entire set must also fall below the threshold when multiplied by the measure under `μ`. This is a statement about the comparison of two measures on a given set in a metric space.
More concisely: For any metric space with a Vitali family, if the limit ratio measure of a subset with respect to two measures, where one is absolutely continuous to the other, is less than a constant, then the measure of the subset with respect to the absolutely continuous measure is less than or equal to the constant times its measure with respect to the other measure.
|
VitaliFamily.exists_measurable_supersets_limRatio
theorem VitaliFamily.exists_measurable_supersets_limRatio :
∀ {α : Type u_1} [inst : MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ)
[inst_1 : SecondCountableTopology α] [inst_2 : BorelSpace α] [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ]
{ρ : MeasureTheory.Measure α} [inst_4 : MeasureTheory.IsLocallyFiniteMeasure ρ],
ρ.AbsolutelyContinuous μ →
∀ {p q : NNReal},
p < q →
∃ a b,
MeasurableSet a ∧
MeasurableSet b ∧ {x | v.limRatio ρ x < ↑p} ⊆ a ∧ {x | ↑q < v.limRatio ρ x} ⊆ b ∧ ↑↑μ (a ∩ b) = 0
This theorem, named `VitaliFamily.exists_measurable_supersets_limRatio`, states that for a given VitaliFamily `v` on a metric space `α`, with measures `μ` and `ρ`, where `ρ` is absolutely continuous with respect to `μ`, and given two nonnegative real numbers `p` and `q` where `p < q`, there exist two measurable sets `a` and `b` such that the set of points `x` for which the limit ratio `v.limRatio ρ x` is less than `p` is a subset of `a`, and the set of points `x` for which the limit ratio `v.limRatio ρ x` is greater than `q` is a subset of `b`, and the measure of the intersection of `a` and `b` is zero. This plays a key role in proving that the limit ratio `v.limRatio ρ` is almost everywhere measurable - the sets for `p` and `q` are disjoint, and this theorem shows that they have measurable supersets which are also disjoint, up to zero measure.
More concisely: Given a Vitali Family `v` on a metric space `α` with absolutely continuous measures `μ` and `ρ`, for any `p < q`, there exist measurable sets `a` and `b` such that the sets of points with `v.limRatio ρ x < p` are contained in `a`, those with `v.limRatio ρ x > q` are contained in `b`, and their intersection has measure zero.
|
VitaliFamily.withDensity_le_mul
theorem VitaliFamily.withDensity_le_mul :
∀ {α : Type u_1} [inst : MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ)
[inst_1 : SecondCountableTopology α] [inst_2 : BorelSpace α] [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ]
{ρ : MeasureTheory.Measure α} [inst_4 : MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ)
{s : Set α}, MeasurableSet s → ∀ {t : NNReal}, 1 < t → ↑↑(μ.withDensity (v.limRatioMeas hρ)) s ≤ ↑t ^ 2 * ↑↑ρ s
This theorem, named `VitaliFamily.withDensity_le_mul`, states that for any type `α` which forms a metric space with a measurable space `m0`, and given a measure `μ` and a Vitali family `v` over `μ`, and given the properties that `α` has a second-countable topology, is a Borel space, and `μ` is a locally finite measure, for any other measure `ρ` which is also a locally finite measure and is absolutely continuous with respect to `μ`, for any set `s` in `α` that is a measurable set, and for any nonnegative real number `t` that is greater than 1, the measure of `s` under the measure that is obtained by scaling `μ` by the limit ratio measure of `v` with respect to `ρ` is less than or equal to `t` squared times the measure of `s` under `ρ`. This result is used as an intermediate step to show that scaling `μ` by the limit ratio measure of `v` with respect to `ρ` actually gives `ρ`.
More concisely: For any second-countable, Borel metric space `α` with a locally finite measure `μ` and a Vitali family `v`, if `ρ` is another locally finite measure absolutely continuous with `μ`, then for any measurable set `s` and `t > 1`, the measure of `s` under the scaled measure obtained by `μ` with respect to the limit ratio measure of `v` with respect to `ρ` is less than or equal to `t²` times the measure of `s` under `ρ`.
|
VitaliFamily.ae_tendsto_measure_inter_div_of_measurableSet
theorem VitaliFamily.ae_tendsto_measure_inter_div_of_measurableSet :
∀ {α : Type u_1} [inst : MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ)
[inst_1 : SecondCountableTopology α] [inst_2 : BorelSpace α] [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ]
{s : Set α},
MeasurableSet s →
∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => ↑↑μ (s ∩ a) / ↑↑μ a) (v.filterAt x) (nhds (s.indicator 1 x))
This theorem, named `VitaliFamily.ae_tendsto_measure_inter_div_of_measurableSet`, states that, given a measurable set `s` in a metric space `α` with a measure `μ` and a Vitali family `v`, the ratio of the measure of the intersection of `s` and a set `a` to the measure of `a`, converges almost everywhere (`∀ᵐ (x : α) ∂μ`) as `a` shrinks to a point `x` along the Vitali family. The limit is the indicator function of `s` at `x`, which is `1` if `x` belongs to `s` and `0` otherwise. This result indicates that almost every point of `s` is a Lebesgue density point for `s`. The theorem assumes that `α` has a second countable topology and is a Borel space, and that `μ` is a locally finite measure. There exists a similar version of this theorem for non-measurable sets, but it only concludes the convergence, not the specific limit value.
More concisely: Given a measurable set `s` in a second countable Borel space `α` with a locally finite measure `μ`, the ratio of `μ(s ∩ a)` to `μ(a)` converges almost everywhere to the indicator function of `s` as `a` shrinks to a point in `α` through a Vitali family.
|
VitaliFamily.ae_tendsto_average
theorem VitaliFamily.ae_tendsto_average :
∀ {α : Type u_1} [inst : MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ)
{E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : SecondCountableTopology α] [inst_3 : BorelSpace α]
[inst_4 : MeasureTheory.IsLocallyFiniteMeasure μ] [inst_5 : NormedSpace ℝ E] [inst_6 : CompleteSpace E]
{f : α → E},
MeasureTheory.LocallyIntegrable f μ →
∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => ⨍ (y : α) in a, f y ∂μ) (v.filterAt x) (nhds (f x))
The *Lebesgue differentiation theorem* states that for a given function `f` from a metric space `α` to a normed add commutative group `E`, given a measure on `α` and a Vitali family defined with respect to that measure, if the function `f` is locally integrable, then for almost every point `x` in `α`, the average of `f` over a set `a` tends to the value of `f` at `x`, as `a` shrinks to `x` along sets from the Vitali family. This is expressed in terms of filter: for almost all `x`, the function mapping each `a` to the integral of `f` over `a` tends to `f(x)` as `a` varies over the filter of sets given by the Vitali family at `x`. Here, `a` is a random variable whose neighborhood shrinks to `x` along sets from the Vitali family, and `∀ᵐ (x : α) ∂μ` denotes that the following property holds for almost every `x` with respect to the measure `μ`.
More concisely: For a locally integrable function `f` on a metric space `α` with respect to a measure `μ`, and a Vitali family `V`, almost every point `x` in `α` satisfies that the integral of `f` over any set `a` in `V` at `x` converges to `f(x)` as `a` shrinks to `x`.
|
VitaliFamily.ae_tendsto_div
theorem VitaliFamily.ae_tendsto_div :
∀ {α : Type u_1} [inst : MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ)
[inst_1 : SecondCountableTopology α] [inst_2 : BorelSpace α] [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ]
{ρ : MeasureTheory.Measure α} [inst_4 : MeasureTheory.IsLocallyFiniteMeasure ρ],
ρ.AbsolutelyContinuous μ → ∀ᵐ (x : α) ∂μ, ∃ c, Filter.Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (v.filterAt x) (nhds c)
The theorem `VitaliFamily.ae_tendsto_div` states that given a measurable space `α`, equipped with a metric space structure, a measure `μ`, and a Vitali family `v` for `μ`, under some conditions (such as having a second countable topology, being a Borel space, and both `μ` and another measure `ρ` being locally finite), if `ρ` is absolutely continuous with respect to `μ`, then for almost every point `x` with respect to the measure `μ`, there exists a real constant `c` such that the ratio of the measures `ρ` and `μ` evaluated at a set `a` tends to `c` as `a` shrinks to `x` along the Vitali family for `μ`. In other words, as the set `a` approaches `x`, the ratio `ρ a / μ a` converges to some constant `c` almost everywhere.
More concisely: Given a measurable space with a metric, a measure and another locally finite measure that is absolutely continuous, for almost every point there exists a constant such that the ratio of the measures tends to that constant as the sets shrink to the point along the Vitali family.
|
VitaliFamily.le_mul_withDensity
theorem VitaliFamily.le_mul_withDensity :
∀ {α : Type u_1} [inst : MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ)
[inst_1 : SecondCountableTopology α] [inst_2 : BorelSpace α] [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ]
{ρ : MeasureTheory.Measure α} [inst_4 : MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ)
{s : Set α}, MeasurableSet s → ∀ {t : NNReal}, 1 < t → ↑↑ρ s ≤ ↑t * ↑↑(μ.withDensity (v.limRatioMeas hρ)) s
This theorem states that, given a metric space `α`, a measure space on `α`, a Vitali family with respect to this measure, a second-countable topology on `α`, a BorelSpace on `α`, a locally finite measure `μ` on `α`, another locally finite measure `ρ` on `α` which is absolutely continuous with respect to `μ`, and a set `s` in `α` which is measurable, for any positive real number `t` larger than 1, the measure of the set `s` with respect to `ρ` is less than or equal to `t` times the measure of the set `s` with respect to the measure `μ` multiplied by the limit ratio measure of the Vitali family `v`. This theorem is an intermediate step towards showing that the measure `μ` with density equal to the limit ratio measure of the Vitali family `v` is equal to the measure `ρ`.
More concisely: Given a second-countable metric space `α` with a locally finite measure `μ`, a locally finite absolutely continuous measure `ρ`, a Vitali family `v`, and a measurable set `s`, for any positive real number `t > 1`, the measure `ρ(s) ≤ t * μ(s) * limit ratio of `v`.
|
VitaliFamily.null_of_frequently_le_of_frequently_ge
theorem VitaliFamily.null_of_frequently_le_of_frequently_ge :
∀ {α : Type u_1} [inst : MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ)
[inst_1 : SecondCountableTopology α] [inst_2 : BorelSpace α] [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ]
{ρ : MeasureTheory.Measure α} [inst_4 : MeasureTheory.IsLocallyFiniteMeasure ρ],
ρ.AbsolutelyContinuous μ →
∀ {c d : NNReal},
c < d →
∀ (s : Set α),
(∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ↑↑ρ a ≤ ↑c * ↑↑μ a) →
(∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ↑d * ↑↑μ a ≤ ↑↑ρ a) → ↑↑μ s = 0
The theorem `VitaliFamily.null_of_frequently_le_of_frequently_ge` is about measures in a given metric space with a Vitali family, a construction related to the resolution of the Vitali set paradox in measure theory. The theorem states that for any given points in the set `s`, if we can find arbitrarily small sets in a Vitali family such that the measure `ρ` of the set is less than or equal to `c` times the measure `μ` of the set, and simultaneously the measure `ρ` of the set is greater than or equal to `d` times the measure `μ` of the set, then the measure `μ` of the set `s` is `0`, provided that `c` is less than `d`. This statement relies on the absolute continuity of the measure `ρ` with respect to the measure `μ`, and on the properties of local finiteness of both measures `ρ` and `μ`. Essentially, this theorem involves a contradiction that arises when the measure `ρ` both underestimates and overestimates the measure `μ` in the context of a given Vitali family.
More concisely: If for any set `s` and for arbitrarily small sets in a Vitali family, the measure `ρ` is less than or equal to `c` times the measure `μ` and greater than or equal to `d` times the measure `μ` with `c < d`, then the measure `μ` of `s` is 0 under the assumption of `ρ` being absolutely continuous with respect to `μ` and both measures being locally finite.
|
VitaliFamily.ae_eventually_measure_pos
theorem VitaliFamily.ae_eventually_measure_pos :
∀ {α : Type u_1} [inst : MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ)
[inst_1 : SecondCountableTopology α], ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, 0 < ↑↑μ a
The theorem `VitaliFamily.ae_eventually_measure_pos` states that for almost every point `x`, in any metric space `α` that also has a second-countable topology and given a measurable space associated with `α`, and a measure `μ`, there exist sufficiently small sets in a Vitali family `v` around `x` that have a positive measure. This is a nontrivial result that follows from the covering property of Vitali families. Specifically, this theorem asserts that for almost every `x` in the measure space, the measure of the sets in the Vitali family that are "close" to `x` is greater than zero.
More concisely: For almost every point in a second-countable metric space with a measurable structure and a given measure, there exists a positive-measure Vitali family of open sets around that point.
|
VitaliFamily.measure_limRatioMeas_zero
theorem VitaliFamily.measure_limRatioMeas_zero :
∀ {α : Type u_1} [inst : MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ)
[inst_1 : SecondCountableTopology α] [inst_2 : BorelSpace α] [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ]
{ρ : MeasureTheory.Measure α} [inst_4 : MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ),
↑↑ρ {x | v.limRatioMeas hρ x = 0} = 0
This theorem states that in a metric space with a certain measure, for a Vitali Family (a mathematical concept related to covering properties of sets in measure theory), the set of points where the limit of the ratio measure is zero, has zero measure according to the given measure `ρ`, assuming `ρ` is absolutely continuous with respect to `μ`. This is under the conditions that the topology of the space is second countable, the space is a Borel space, and both the measures `μ` and `ρ` are locally finite.
More concisely: In a second countable Borel metric space with locally finite and absolutely continuous measures `μ` and `ρ`, the set of points where the limit of `ρ`/`μ` ratios equals zero has zero `μ` measure.
|
VitaliFamily.ae_tendsto_rnDeriv_of_absolutelyContinuous
theorem VitaliFamily.ae_tendsto_rnDeriv_of_absolutelyContinuous :
∀ {α : Type u_1} [inst : MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ)
[inst_1 : SecondCountableTopology α] [inst_2 : BorelSpace α] [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ]
{ρ : MeasureTheory.Measure α} [inst_4 : MeasureTheory.IsLocallyFiniteMeasure ρ],
ρ.AbsolutelyContinuous μ →
∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (v.filterAt x) (nhds (ρ.rnDeriv μ x))
This theorem, the "Weak version of the main theorem on differentiation of measures", states that for a given Vitali family `v` for a locally finite measure `μ`, and another locally finite measure `ρ` that is absolutely continuous with respect to `μ`, the ratio `ρ a / μ a` tends towards the Radon-Nikodym derivative of `ρ` with respect to `μ` for `μ`-almost every `x` when `a` shrinks to `x` along the Vitali family. In other words, as subsets `a` of the space `α` become increasingly concentrated around almost every point `x` (in the sense of the Vitali family `v`), the ratio of the `ρ` and `μ` measures of `a` converges to the Radon-Nikodym derivative of `ρ` with respect to `μ` at `x`. A Radon-Nikodym derivative is a function that describes how one measure changes with respect to another. The statement of the theorem acknowledges that there is a more general version of this theorem that does not require the measure `ρ` to be absolutely continuous with respect to `μ`.
More concisely: For a Vitali family `v` of locally finite measures `μ` and a locally finite measure `ρ` absolutely continuous with respect to `μ`, the Radon-Nikodym derivative of `ρ` with respect to `μ` is the limit as `a` in `v` approaches `x` of `ρ a / μ a`.
|
VitaliFamily.ae_tendsto_rnDeriv
theorem VitaliFamily.ae_tendsto_rnDeriv :
∀ {α : Type u_1} [inst : MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ)
[inst_1 : SecondCountableTopology α] [inst_2 : BorelSpace α] [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ]
(ρ : MeasureTheory.Measure α) [inst_4 : MeasureTheory.IsLocallyFiniteMeasure ρ],
∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (v.filterAt x) (nhds (ρ.rnDeriv μ x))
This theorem states that given a Vitali family `v` for a locally finite measure `μ`, and another locally finite measure `ρ`, then for almost every point `x` with respect to the measure `μ`, the ratio of `ρ` to `μ` over sets `a` that shrink to `x` along the Vitali family, converges towards the Radon-Nikodym derivative of `ρ` with respect to `μ`. This is central to the concept of differentiation of measures. Here, convergence is described in terms of filters, with the ratio converging to the Radon-Nikodym derivative as per the filter of sets constructed from the Vitali family at `x`, and the neighborhood filter at the Radon-Nikodym derivative.
More concisely: Given a Vitali family `v` for a locally finite measures `μ` and `ρ`, for almost every `x` with respect to `μ`, the ratio of `ρ` to `μ` on shrinking sets `a` converges to the Radon-Nikodym derivative of `ρ` with respect to `μ` as filters at `x` and the Radon-Nikodym derivative.
|