IsUnifLocDoublingMeasure.tendsto_closedBall_filterAt
theorem IsUnifLocDoublingMeasure.tendsto_closedBall_filterAt :
∀ {α : Type u_1} [inst : MetricSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α)
[inst_2 : IsUnifLocDoublingMeasure μ] [inst_3 : SecondCountableTopology α] [inst_4 : BorelSpace α]
[inst_5 : MeasureTheory.IsLocallyFiniteMeasure μ] {K : ℝ} {x : α} {ι : Type u_2} {l : Filter ι} (w : ι → α)
(δ : ι → ℝ),
Filter.Tendsto δ l (nhdsWithin 0 (Set.Ioi 0)) →
(∀ᶠ (j : ι) in l, x ∈ Metric.closedBall (w j) (K * δ j)) →
Filter.Tendsto (fun j => Metric.closedBall (w j) (δ j)) l
((IsUnifLocDoublingMeasure.vitaliFamily μ K).filterAt x)
This theorem states that for a given uniform locally doubling measure `μ` on a metric space `α` equipped with a second countable topology, a Borel space structure, and a locally finite measure, we have the following result. Suppose we have a sequence of points `w` and radii `δ` in the space defined on a filter `l`, such that `δ` tends toward 0 within the set of positive real numbers under `l`. Additionally, suppose that most (in the sense of the filter `l`) points `x` are in the closed ball centered at `w(j)` with radius `K * δ(j)`. Then, the sequence of closed balls with radii `δ(j)` centered at `w(j)` tends toward the filter generated by the Vitali family associated with the measure `μ` at the point `x`. In layman's terms, this theorem captures the idea that, under certain conditions, the sequence of closed balls "shrinks" towards the point `x` in a manner captured by the Vitali family's filter.
More concisely: Given a uniform locally doubling measure `μ` on a second countable, locally finite Borel space `α`, if most points `x` are in the closed balls with radii `δ(j)` centered at `w(j)` that shrink to 0, then the sequence of closed balls filters converges to the Vitali family filter at `x`.
|
IsUnifLocDoublingMeasure.ae_tendsto_average
theorem IsUnifLocDoublingMeasure.ae_tendsto_average :
∀ {α : Type u_1} [inst : MetricSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α)
[inst_2 : IsUnifLocDoublingMeasure μ] [inst_3 : SecondCountableTopology α] [inst_4 : BorelSpace α]
[inst_5 : MeasureTheory.IsLocallyFiniteMeasure μ] {E : Type u_2} [inst_6 : NormedAddCommGroup E]
[inst_7 : NormedSpace ℝ E] [inst_8 : CompleteSpace E] {f : α → E},
MeasureTheory.LocallyIntegrable f μ →
∀ (K : ℝ),
∀ᵐ (x : α) ∂μ,
∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
Filter.Tendsto δ l (nhdsWithin 0 (Set.Ioi 0)) →
(∀ᶠ (j : ι) in l, x ∈ Metric.closedBall (w j) (K * δ j)) →
Filter.Tendsto (fun j => ⨍ (y : α) in Metric.closedBall (w j) (δ j), f y ∂μ) l (nhds (f x))
This theorem is a version of the Lebesgue differentiation theorem for sequence of closed balls that do not necessarily have fixed centers. Specifically, it states that for any metric space `α` endowed with a measure `μ` which satisfies the properties of being a uniformly locally doubling measure, second countable, Borel, and locally finite, and for any function `f : α → E` which is locally integrable, then for almost every `x` with respect to the measure `μ`, given any sequence of centers `w : ι → α` and radii `δ : ι → ℝ` such that `δ` tends to 0 within the set of positive real numbers, and for almost all `j`, `x` belongs to the closed ball with center `w j` and radius `K * δ j`, it holds that the average value of `f` over these closed balls tends to `f x`. Here `E` is a normed additive group which is also a complete normed space over real numbers.
More concisely: For any locally integrable function `f` on a uniformly locally doubling, second countable, Borel, and locally finite measure space `α` over a normed additive group `E`, and for any sequence of centers `w : ι → α` and radii `δ : ι → ℝ` tending to 0, the average value of `f` over the closed balls with centers `w j` and radii `K * δ j` converges to `f(x)` for almost every `x` in `α`.
|
IsUnifLocDoublingMeasure.closedBall_mem_vitaliFamily_of_dist_le_mul
theorem IsUnifLocDoublingMeasure.closedBall_mem_vitaliFamily_of_dist_le_mul :
∀ {α : Type u_1} [inst : MetricSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α)
[inst_2 : IsUnifLocDoublingMeasure μ] [inst_3 : SecondCountableTopology α] [inst_4 : BorelSpace α]
[inst_5 : MeasureTheory.IsLocallyFiniteMeasure μ] {K : ℝ} {x y : α} {r : ℝ},
dist x y ≤ K * r → 0 < r → Metric.closedBall y r ∈ (IsUnifLocDoublingMeasure.vitaliFamily μ K).setsAt x
The theorem `IsUnifLocDoublingMeasure.closedBall_mem_vitaliFamily_of_dist_le_mul` states that for any Metric Space `α`, Measurable Space `α`, Measure `μ`, and real numbers `K`, `r`, and any points `x`, `y` in `α`, if the distance between `x` and `y` is less than or equal to `K` times `r`, and `r` is greater than `0`, then the closed ball with center `y` and radius `r` belongs to the set of sets from the Vitali Family `IsUnifLocDoublingMeasure.vitaliFamily μ K` at `x`. Here, a Vitali Family in a space with a uniformly locally doubling measure is designed such that the sets at `x` contain all `closedBall y r` when `dist x y ≤ K * r`, where `closedBall x ε` indicates the set of all points `y` with `dist y x ≤ ε`.
More concisely: For any Metric Space `α`, Measurable Space `α`, Measure `μ`, real numbers `K`, `r`, and points `x`, `y` in `α`, if `dist(x, y) ≤ K * r` and `r > 0`, then the closed ball with center `y` and radius `r` is in the Vitali Family with parameter `K` at `x` for the measure `μ`.
|
IsUnifLocDoublingMeasure.ae_tendsto_average_norm_sub
theorem IsUnifLocDoublingMeasure.ae_tendsto_average_norm_sub :
∀ {α : Type u_1} [inst : MetricSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α)
[inst_2 : IsUnifLocDoublingMeasure μ] [inst_3 : SecondCountableTopology α] [inst_4 : BorelSpace α]
[inst_5 : MeasureTheory.IsLocallyFiniteMeasure μ] {E : Type u_2} [inst_6 : NormedAddCommGroup E] {f : α → E},
MeasureTheory.LocallyIntegrable f μ →
∀ (K : ℝ),
∀ᵐ (x : α) ∂μ,
∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
Filter.Tendsto δ l (nhdsWithin 0 (Set.Ioi 0)) →
(∀ᶠ (j : ι) in l, x ∈ Metric.closedBall (w j) (K * δ j)) →
Filter.Tendsto (fun j => ⨍ (y : α) in Metric.closedBall (w j) (δ j), ‖f y - f x‖ ∂μ) l (nhds 0)
This is a version of the Lebesgue differentiation theorem for a sequence of closed balls where the centers are not required to be fixed. The theorem states that given a locally integrable function `f` from a measurable space `α` to a normed additive commutative group `E` with a measure `μ` that satisfies certain properties (namely, it is a uniformly local doubling measure, the topology on `α` is second countable, `α` is a Borel space, and `μ` is a locally finite measure), then for all real numbers `K`, almost every point `x` in the measurable space `α` with respect to the measure `μ` has the property that for any sequence of real numbers `δ` and points `w` in `α` that converge to `0` within the right-open infinite interval `(0, ∞)`, if `x` is eventually in the closed ball centered at `w[j]` with radius `K * δ[j]`, then the integral averages of the norm of the difference between `f[y]` and `f[x]` over the closed ball centered at `w[j]` with radius `δ[j]` tend to `0` as `j` goes to infinity.
More concisely: Given a locally integrable function `f` from a second countable Borel space `(α, μ)` with a locally finite, uniformly local doubling measure `μ`, for almost every `x` in `α`, the integral averages of the norm of `f(y) - f(x)` over any sequence of shrinking closed balls centered at `w` with radius `K * δ[j]` converge to 0 as `j` goes to infinity.
|
IsUnifLocDoublingMeasure.ae_tendsto_measure_inter_div
theorem IsUnifLocDoublingMeasure.ae_tendsto_measure_inter_div :
∀ {α : Type u_1} [inst : MetricSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α)
[inst_2 : IsUnifLocDoublingMeasure μ] [inst_3 : SecondCountableTopology α] [inst_4 : BorelSpace α]
[inst_5 : MeasureTheory.IsLocallyFiniteMeasure μ] (S : Set α) (K : ℝ),
∀ᵐ (x : α) ∂μ.restrict S,
∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
Filter.Tendsto δ l (nhdsWithin 0 (Set.Ioi 0)) →
(∀ᶠ (j : ι) in l, x ∈ Metric.closedBall (w j) (K * δ j)) →
Filter.Tendsto (fun j => ↑↑μ (S ∩ Metric.closedBall (w j) (δ j)) / ↑↑μ (Metric.closedBall (w j) (δ j))) l
(nhds 1)
This is a version of Lebesgue's density theorem for a sequence of closed balls whose centers are not fixed. The theorem states that for every measurable space `α` in a metric space, given a measure `μ` that is a uniformly locally doubling measure and is locally finite, a set `S` in `α` and a real number `K`, almost every point `x` in the measure `μ` restricted to `S` has the following property: for any filter `l` over an index set `ι`, sequence of points `w` in `α` indexed by `ι`, and sequence of real numbers `δ` indexed by `ι`, if `δ` tends to 0 within the set of positive numbers with respect to the filter `l`, and `x` eventually belongs to the closed balls centered at `w j` with radius `K * δ j` for `j` in the index set `ι`, then the measure of the intersection of `S` and the closed ball centered at `w j` with radius `δ j`, divided by the measure of the closed ball centered at `w j` with radius `δ j`, tends to 1 with respect to the filter `l`.
More concisely: For any measurable space in a metric space, a uniformly locally doubling and locally finite measure μ, set S, and real number K, almost every point x in S satisfies that the measure of S intersect the closed ball centered at w with radius Kδ, divided by the measure of the closed ball centered at w with radius δ, approaches 1 as δ tends to 0 for any filter l, sequence of points w in α indexed by ι, and sequence of real numbers δ indexed by ι with w belonging to the filter l and x eventually in the closed balls centered at w with radius Kδ.
|