Besicovitch.exists_closedBall_covering_tsum_measure_le
theorem Besicovitch.exists_closedBall_covering_tsum_measure_le :
∀ {α : Type u_1} [inst : MetricSpace α] [inst_1 : SecondCountableTopology α] [inst_2 : MeasurableSpace α]
[inst_3 : OpensMeasurableSpace α] [inst_4 : HasBesicovitchCovering α] (μ : MeasureTheory.Measure α)
[inst_5 : MeasureTheory.SigmaFinite μ] [inst_6 : μ.OuterRegular] {ε : ENNReal},
ε ≠ 0 →
∀ (f : α → Set ℝ) (s : Set α),
(∀ x ∈ s, ∀ δ > 0, (f x ∩ Set.Ioo 0 δ).Nonempty) →
∃ t r,
t.Countable ∧
t ⊆ s ∧
(∀ x ∈ t, r x ∈ f x) ∧
s ⊆ ⋃ x ∈ t, Metric.closedBall x (r x) ∧
∑' (x : ↑t), ↑↑μ (Metric.closedBall (↑x) (r ↑x)) ≤ ↑↑μ s + ε
This theorem states that in a metric space equipped with the "Besicovitch property", any set `s` can be covered with a countable collection of closed balls in such a way that the sum of the measures (sizes) of these balls is at most the measure of the set `s` plus any positive real number `ε`. This is true even when we restrict the possible radii of the balls centered at a point `x` to be within a set `f x` that gets arbitrarily close to `0`. Specifically, for every point `x` in `s`, we can always find a radius within the intersection of `f x` and the open interval from `0` to any positive number `δ`, and we can then cover the set `s` with the closed balls centered at points in `t` (a subset of `s`) with these radii. The total measure of these balls will not exceed the measure of `s` plus `ε`.
More concisely: In a metric space with the Besicovitch property, for every set `s` and every `ε > 0`, there exists a countable collection of closed balls with radii in the specified intervals around points in `s`, whose sum of measures is at most the measure of `s` plus `ε`.
|
Besicovitch.exist_disjoint_covering_families
theorem Besicovitch.exist_disjoint_covering_families :
∀ {α : Type u_1} [inst : MetricSpace α] {β : Type u} {N : ℕ} {τ : ℝ},
1 < τ →
IsEmpty (Besicovitch.SatelliteConfig α N τ) →
∀ (q : Besicovitch.BallPackage β α),
∃ s,
(∀ (i : Fin N), (s i).PairwiseDisjoint fun j => Metric.closedBall (q.c j) (q.r j)) ∧
Set.range q.c ⊆ ⋃ i, ⋃ j ∈ s i, Metric.ball (q.c j) (q.r j)
The Besicovitch covering theorem states that for any metric space (denoted by `α`), and given a type `β`, a natural number `N`, and a real number `τ` such that `1 < τ`, if there are no satellite configurations with `N+1` points, then for every ball package `q`, there exist `N` families of disjoint balls (`s`) such that each family covers all the centers in the ball package. More specifically, for each family `i` (from 0 to `N-1`), the balls with centers at each `j` in `q.c` and radii `q.r j` are pairwise disjoint. Furthermore, the range of the centers `q.c` is contained in the union of balls in the families, where each ball has center `q.c j` and radius `q.r j`.
More concisely: Given a metric space and natural numbers `N` and `τ` with `τ` greater than 1, if there are no satellite configurations with `N+1` points, then for any ball package, there exist `N` families of disjoint balls with pairwise disjoint balls in each family and centers covering the entire package.
|
Besicovitch.exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux
theorem Besicovitch.exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux :
∀ {α : Type u_1} [inst : MetricSpace α] [inst_1 : SecondCountableTopology α] [inst_2 : MeasurableSpace α]
[inst_3 : OpensMeasurableSpace α] [inst_4 : HasBesicovitchCovering α] (μ : MeasureTheory.Measure α)
[inst_5 : MeasureTheory.IsFiniteMeasure μ] (f : α → Set ℝ) (s : Set α),
(∀ x ∈ s, ∀ δ > 0, (f x ∩ Set.Ioo 0 δ).Nonempty) →
∃ t,
t.Countable ∧
(∀ p ∈ t, p.1 ∈ s) ∧
(∀ p ∈ t, p.2 ∈ f p.1) ∧
↑↑μ (s \ ⋃ p ∈ t, Metric.closedBall p.1 p.2) = 0 ∧
t.PairwiseDisjoint fun p => Metric.closedBall p.1 p.2
This is the **Measurable Besicovitch Covering Theorem**. It postulates the following: consider a set `s` in a metric space with a second countable topology, a measurable space, an open measurable space, and the Besicovitch covering property. For each point `x` in `s`, we are given a set of admissible closed balls centered at `x`, with radii belonging to a set `f` of real numbers and being arbitrarily small. If the underlying measure `μ` of this space is finite, then there exists a countable set `t` such that:
- Every pair `(p.1, p.2)` from `t` satisfies `p.1` belongs to `s`, `p.2` belongs to `f(p.1)`, and `p` describes a closed ball in the metric space.
- The set `t` is pairwise disjoint, meaning no two different closed balls in `t` intersect.
- The measure of the set difference between `s` and the union of all closed balls described in `t` is zero. In other words, almost all of `s` is covered by these closed balls.
This theorem is particularly applicable to normed real vector spaces that possess the Besicovitch covering property.
More concisely: In a second countable metric space with a finite measure and the Besicovitch covering property, there exists a countable collection of pairwise disjoint, closed balls with arbitrarily small radii such that their union covers almost all of the given measurable set.
|
Besicovitch.exist_finset_disjoint_balls_large_measure
theorem Besicovitch.exist_finset_disjoint_balls_large_measure :
∀ {α : Type u_1} [inst : MetricSpace α] [inst_1 : SecondCountableTopology α] [inst_2 : MeasurableSpace α]
[inst_3 : OpensMeasurableSpace α] (μ : MeasureTheory.Measure α) [inst_4 : MeasureTheory.IsFiniteMeasure μ] {N : ℕ}
{τ : ℝ},
1 < τ →
IsEmpty (Besicovitch.SatelliteConfig α N τ) →
∀ (s : Set α) (r : α → ℝ),
(∀ x ∈ s, 0 < r x) →
(∀ x ∈ s, r x ≤ 1) →
∃ t,
↑t ⊆ s ∧
↑↑μ (s \ ⋃ x ∈ t, Metric.closedBall x (r x)) ≤ ↑N / (↑N + 1) * ↑↑μ s ∧
(↑t).PairwiseDisjoint fun x => Metric.closedBall x (r x)
This theorem, named `Besicovitch.exist_finset_disjoint_balls_large_measure`, states that given a set `s` in a metric space `α`, and a function `r` that assigns a radius in the range `(0, 1]` to every point `x` in `s`, it is possible to find a finite subset `t` of `s` such that the closed balls centered at points in `t` with radii given by `r` are pairwise disjoint and cover at least a `1/(N+1)` proportion of `s`, provided that the metric space `α` does not admit a satellite configuration with `N+1` points, with a certain parameter `τ` greater than 1. This is under the constraints that the space `α` is second-countable, measurable, and has an open set topology, and that the measure `μ` assigned to `α` is finite. Coverage of `s` is defined as the measure of the set difference between `s` and the union of all balls being less than or equal to `N / (N + 1)` times the measure of `s`.
More concisely: Given a second-countable, measurable metric space with finite measure and without a satellite configuration of size N+1, there exists a finite subset of points with pairwise disjoint closed balls of assigned radii covering at least a 1/(N+1) proportion of the space.
|
Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet
theorem Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet :
∀ {β : Type u} [inst : MetricSpace β] [inst_1 : MeasurableSpace β] [inst_2 : BorelSpace β]
[inst_3 : SecondCountableTopology β] [inst_4 : HasBesicovitchCovering β] (μ : MeasureTheory.Measure β)
[inst_5 : MeasureTheory.IsLocallyFiniteMeasure μ] {s : Set β},
MeasurableSet s →
∀ᵐ (x : β) ∂μ,
Filter.Tendsto (fun r => ↑↑μ (s ∩ Metric.closedBall x r) / ↑↑μ (Metric.closedBall x r))
(nhdsWithin 0 (Set.Ioi 0)) (nhds (s.indicator 1 x))
The theorem `Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet` states that, for a given measurable set `s` in a metric space that also has a measure (given by `μ`), for almost every point `x` in the metric space, the ratio of the measure of the intersection of the set `s` and a closed ball around `x` with radius `r` to the measure of that closed ball, tends to a specific limit as `r` tends to `0`. The limit is `1` if `x` is an element of the set `s`, and `0` if `x` is not an element of `s`. This indicates that almost every point of `s` is a Lebesgue density point for `s`. A version for non-measurable sets also exists, but it only gives the first part of the conclusion.
More concisely: For a measurable set `s` in a metric space with measure `μ`, almost every point `x` in the space satisfies `μ(s ∩ B(x, r)) / μ(B(x, r))` approaches `1` if `x ∈ s` and `0` if `x ∉ s` as `r` approaches `0`.
|
Besicovitch.tendsto_filterAt
theorem Besicovitch.tendsto_filterAt :
∀ {α : Type u_1} [inst : MetricSpace α] [inst_1 : SecondCountableTopology α] [inst_2 : MeasurableSpace α]
[inst_3 : OpensMeasurableSpace α] [inst_4 : HasBesicovitchCovering α] (μ : MeasureTheory.Measure α)
[inst_5 : MeasureTheory.SigmaFinite μ] (x : α),
Filter.Tendsto (fun r => Metric.closedBall x r) (nhdsWithin 0 (Set.Ioi 0))
((Besicovitch.vitaliFamily μ).filterAt x)
This theorem, named `Besicovitch.tendsto_filterAt`, states that for any point `x` in a metric space `α`, which also has a second countable topology, a measurable space, an open measurable space and a Besicovitch covering, along with a sigma finite measure `μ`, the filter of the function mapping each real number `r` to the closed ball of radius `r` around `x` within the range of real numbers greater than zero tends to the filter at `x` of the Vitali family associated with the measure `μ`. Essentially, this means that as the radii of the closed balls decrease and approach zero, the corresponding elements in the Vitali family also approach to `x`. This theorem is part of the underlying theory supporting the differentiation of measures in metric spaces.
More concisely: For any point `x` in a second countable metric space with a measurable structure, a sigma-finite measure `μ`, and a Besicovitch covering, the filter of closed balls around `x` with decreasing radii converges to the filter at `x` of the Vitali family associated with `μ`.
|
Besicovitch.TauPackage.color_lt
theorem Besicovitch.TauPackage.color_lt :
∀ {α : Type u_1} [inst : MetricSpace α] {β : Type u} [inst_1 : Nonempty β] (p : Besicovitch.TauPackage β α)
{i : Ordinal.{u}}, i < p.lastStep → ∀ {N : ℕ}, IsEmpty (Besicovitch.SatelliteConfig α N p.τ) → p.color i < N
The theorem `Besicovitch.TauPackage.color_lt` states that for any given types `α` and `β`, where `α` is a metric space and `β` is nonempty, and for any `Besicovitch.TauPackage` `p` indexed by `β` with values in `α`, if an ordinal `i` is less than the final step of the package `p`, then for any natural number `N`, if there exists no `Besicovitch.SatelliteConfig` configuration for `α`, `N` and the tau value of `p`, it follows that the color of step `i` in the package `p` is less than `N`. In simpler terms, this theorem says that if there are no satellite configurations with `N+1` points, then we never use more than `N` distinct families in the Besicovitch inductive construction.
More concisely: For any metric space `α`, nonempty type `β`, and `Besicovitch.TauPackage` `p` indexed by `β` with values in `α`, if there exists no `Besicovitch.SatelliteConfig` with `N+1` points for some natural number `N`, then for all `i < final step of p`, the color of step `i` in `p` is less than `N`.
|
Besicovitch.exists_disjoint_closedBall_covering_ae
theorem Besicovitch.exists_disjoint_closedBall_covering_ae :
∀ {α : Type u_1} [inst : MetricSpace α] [inst_1 : SecondCountableTopology α] [inst_2 : MeasurableSpace α]
[inst_3 : OpensMeasurableSpace α] [inst_4 : HasBesicovitchCovering α] (μ : MeasureTheory.Measure α)
[inst_5 : MeasureTheory.SigmaFinite μ] (f : α → Set ℝ) (s : Set α),
(∀ x ∈ s, ∀ δ > 0, (f x ∩ Set.Ioo 0 δ).Nonempty) →
∀ (R : α → ℝ),
(∀ x ∈ s, 0 < R x) →
∃ t r,
t.Countable ∧
t ⊆ s ∧
(∀ x ∈ t, r x ∈ f x ∩ Set.Ioo 0 (R x)) ∧
↑↑μ (s \ ⋃ x ∈ t, Metric.closedBall x (r x)) = 0 ∧
t.PairwiseDisjoint fun x => Metric.closedBall x (r x)
The measurable Besicovitch covering theorem states that given a set `s` in a metric space `α`, suppose for each point `x` in `s`, we have a set of admissible closed balls centered at `x` with arbitrarily small radii. Then, there exists a countable subset `t` of `s` and a function `r` from `t` to the real numbers such that the following conditions are satisfied:
1. Every closed ball with radius `r x` centered at `x` is contained in the intersection of `f x` and the open interval from 0 to `R x` (for some function `R` from `s` to the real numbers), where `R x > 0` for all `x` in `s`.
2. The set `t` is pairwise disjoint, i.e., for every two distinct points in `t`, their corresponding closed balls do not intersect.
3. The measure of the set `s` minus the union of all closed balls is zero.
This implies that almost all of `s` can be covered by these disjoint closed balls. This version of the theorem requires that the underlying measure is sigma-finite and that the space has the Besicovitch covering property, a property satisfied by, for example, normed real vector spaces.
More concisely: Given a sigma-finite measure space with the Besicovitch covering property, for any set in the space with the property that for each point there exists a countable collection of admissible closed balls, there exists a countable disjoint collection of closed balls covering a full measure subset of the original set.
|
Besicovitch.ae_tendsto_measure_inter_div
theorem Besicovitch.ae_tendsto_measure_inter_div :
∀ {β : Type u} [inst : MetricSpace β] [inst_1 : MeasurableSpace β] [inst_2 : BorelSpace β]
[inst_3 : SecondCountableTopology β] [inst_4 : HasBesicovitchCovering β] (μ : MeasureTheory.Measure β)
[inst_5 : MeasureTheory.IsLocallyFiniteMeasure μ] (s : Set β),
∀ᵐ (x : β) ∂μ.restrict s,
Filter.Tendsto (fun r => ↑↑μ (s ∩ Metric.closedBall x r) / ↑↑μ (Metric.closedBall x r))
(nhdsWithin 0 (Set.Ioi 0)) (nhds 1)
This theorem, named `Besicovitch.ae_tendsto_measure_inter_div`, states the following:
For any set `s` in a metric space `β` that has a Besicovitch covering, and where `β` is also a measurable space with Borel sigma-algebra, a second countable topology, and equipped with a locally finite measure `μ`, the ratio of the measure of the intersection of `s` and a closed ball centered at `x` with radius `r` to the measure of the same closed ball, approaches `1` as `r` tends to `0`, for almost every `x` in `s`. In other words, almost every point in `s` is a Lebesgue density point for `s`.
Here, "almost every" is with respect to the measure `μ` restricted to `s`, and the convergence is in the sense of filters, specifically the limit is taken as `r` approaches `0` within the open interval `(0, ∞)`. A stronger version of this result exists for measurable sets.
More concisely: For any set `s` in a second countable, locally finite, measurable space `(β, μ)` with a Besicovitch covering, the measure ratio of `s` and closed balls around almost every point `x` in `s` approaches 1 as the radius `r` tends to 0.
|
Besicovitch.exists_disjoint_closedBall_covering_ae_aux
theorem Besicovitch.exists_disjoint_closedBall_covering_ae_aux :
∀ {α : Type u_1} [inst : MetricSpace α] [inst_1 : SecondCountableTopology α] [inst_2 : MeasurableSpace α]
[inst_3 : OpensMeasurableSpace α] [inst_4 : HasBesicovitchCovering α] (μ : MeasureTheory.Measure α)
[inst_5 : MeasureTheory.SigmaFinite μ] (f : α → Set ℝ) (s : Set α),
(∀ x ∈ s, ∀ δ > 0, (f x ∩ Set.Ioo 0 δ).Nonempty) →
∃ t,
t.Countable ∧
(∀ p ∈ t, p.1 ∈ s) ∧
(∀ p ∈ t, p.2 ∈ f p.1) ∧
↑↑μ (s \ ⋃ p ∈ t, Metric.closedBall p.1 p.2) = 0 ∧
t.PairwiseDisjoint fun p => Metric.closedBall p.1 p.2
The theorem, `Besicovitch.exists_disjoint_closedBall_covering_ae_aux`, is known as the measurable Besicovitch covering theorem. It states that, given a set `s` in a metric space `α` which is also a second countable topological space, measurable space, has Besicovitch covering property, and the underlying measure is sigma-finite, if for each point `x` in `s`, there is a set of admissible closed balls centered at `x` with radii in the set `f(x)` and intersecting the open interval `(0, δ)` for any `δ` greater than 0, then there exists a set `t` such that: `t` is countable, each pair `p` in `t` satisfies that its first component is in `s` and its second component is in `f(p.1)`, the measure of the difference between `s` and the union of closed balls centered at `p.1` with radius `p.2` for each `p` in `t` is 0, and these closed balls are pairwise disjoint. This theorem is used in the case when the space has the Besicovitch covering property, such as normed real vector spaces.
More concisely: Given a measurable, second countable, sigma-finite subset `s` of a metric space with the Besicovitch covering property, for each point `x` in `s`, if there exists a countable set `t` of pairs `(p, r)` such that `p` is in `s`, `r` is in `f(x)`, and the closed balls centered at `p` with radius `r` intersect `(0, δ)` for any `δ > 0` are pairwise disjoint and cover `s` up to a set of measure 0, then such a set `t` exists.
|
Besicovitch.ae_tendsto_rnDeriv
theorem Besicovitch.ae_tendsto_rnDeriv :
∀ {β : Type u} [inst : MetricSpace β] [inst_1 : MeasurableSpace β] [inst_2 : BorelSpace β]
[inst_3 : SecondCountableTopology β] [inst_4 : HasBesicovitchCovering β] (ρ μ : MeasureTheory.Measure β)
[inst_5 : MeasureTheory.IsLocallyFiniteMeasure μ] [inst_6 : MeasureTheory.IsLocallyFiniteMeasure ρ],
∀ᵐ (x : β) ∂μ,
Filter.Tendsto (fun r => ↑↑ρ (Metric.closedBall x r) / ↑↑μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0))
(nhds (ρ.rnDeriv μ x))
In a metric space equipped with measurable, Borel, second-countable, and Besicovitch covering properties, given two locally finite measures `ρ` and `μ`, for almost every point `x` with respect to measure `μ`, the ratio of the measures of closed balls centered at `x` and of radius `r`, where `r` tends to `0` through positive values, converges to the Radon-Nikodym derivative of `ρ` with respect to `μ` at `x`.
More concisely: In a second-countable, Borel, metric space with Besicovitch covering property, for any two locally finite measures `ρ` and `μ`, the Radon-Nikodym derivative of `ρ` with respect to `μ` at almost every `μ`-point `x` is given by the limit of the ratio of their ball measures as the radius goes to zero.
|
Besicovitch.TauPackage.mem_iUnionUpTo_lastStep
theorem Besicovitch.TauPackage.mem_iUnionUpTo_lastStep :
∀ {α : Type u_1} [inst : MetricSpace α] {β : Type u} [inst_1 : Nonempty β] (p : Besicovitch.TauPackage β α) (x : β),
p.c x ∈ p.iUnionUpTo p.lastStep
This theorem states that for any given point `x` in a set `β` (which is nonempty), under any tau package `p` constructed from this set in a given metric space `α`, the center `c` of the ball corresponding to this point `x` belongs to the indexed union of balls defined up to the last step of the tau package `p`. The term "tau package" refers to a specific structure used in the Besicovitch covering theorem in the field of geometric measure theory.
More concisely: For any nonempty set β in a metric space α, and for any point x in β, the center of the ball centered at x belongs to the union of balls defined up to the last step in the tau cover of β.
|