blimsup_cthickening_mul_ae_eq
theorem blimsup_cthickening_mul_ae_eq :
∀ {α : Type u_1} [inst : MetricSpace α] [inst_1 : SecondCountableTopology α] [inst_2 : MeasurableSpace α]
[inst_3 : BorelSpace α] (μ : MeasureTheory.Measure α) [inst_4 : MeasureTheory.IsLocallyFiniteMeasure μ]
[inst_5 : IsUnifLocDoublingMeasure μ] (p : ℕ → Prop) (s : ℕ → Set α) {M : ℝ},
0 < M →
∀ (r : ℕ → ℝ),
Filter.Tendsto r Filter.atTop (nhds 0) →
μ.ae.EventuallyEq (Filter.blimsup (fun i => Metric.cthickening (M * r i) (s i)) Filter.atTop p)
(Filter.blimsup (fun i => Metric.cthickening (r i) (s i)) Filter.atTop p)
This theorem states that for a sequence of subsets `s` in a metric space, along with a sequence of radii `r` that converges to 0, the set of points that belong to infinitely many of the closed `r`-thickenings of `s` remains almost everywhere unchanged for a uniformly locally doubling measure if the `r` values are all multiplied by a positive constant `M`. This result is a generalization of Lemma 9 in J.W.S. Cassels's work "Some metrical theorems in Diophantine approximation. I". Note that the `Set α` type ascription is present due to a reported issue in the mathlib library.
More concisely: For a sequence of subsets `s` in a uniformly locally doubling metric space and a converging sequence of radii `r` with multiplicative factor `M`, the sets of points in infinitely many `r`-thickenings of `s` are equivalent up to a set of measure zero.
|
blimsup_thickening_mul_ae_eq
theorem blimsup_thickening_mul_ae_eq :
∀ {α : Type u_1} [inst : MetricSpace α] [inst_1 : SecondCountableTopology α] [inst_2 : MeasurableSpace α]
[inst_3 : BorelSpace α] (μ : MeasureTheory.Measure α) [inst_4 : MeasureTheory.IsLocallyFiniteMeasure μ]
[inst_5 : IsUnifLocDoublingMeasure μ] (p : ℕ → Prop) (s : ℕ → Set α) {M : ℝ},
0 < M →
∀ (r : ℕ → ℝ),
Filter.Tendsto r Filter.atTop (nhds 0) →
μ.ae.EventuallyEq (Filter.blimsup (fun i => Metric.thickening (M * r i) (s i)) Filter.atTop p)
(Filter.blimsup (fun i => Metric.thickening (r i) (s i)) Filter.atTop p)
The theorem `blimsup_thickening_mul_ae_eq` asserts that in a metric space which is second countable, measurable, and has a Borel topology, for a given uniformly locally doubling measure `μ`, a property `p` and a sequence of subsets `sᵢ`, if we have a sequence of radii `rᵢ` tending to 0, the set of points that belong to the `rᵢ`-thickening of `sᵢ` infinitely often is almost everywhere the same, regardless of whether we scale the radii `rᵢ` by a positive constant `M`. This is a generalization of a metrical theorem in Diophantine approximation and is subject to the condition that `M > 0`. The term "almost everywhere" is with respect to the measure `μ`.
More concisely: In a second countable, measurable metric space with a Borel topology and a uniformly locally doubling measure `μ`, for any sequence of subsets `sᵢ`, property `p`, and positive constant `M`, the sets of points belonging to the `rᵢ`-thickening of `sᵢ` that belong to `p` infinitely often are equal almost everywhere, regardless of whether the radii `rᵢ` are scaled by `M`.
|
blimsup_thickening_mul_ae_eq_aux
theorem blimsup_thickening_mul_ae_eq_aux :
∀ {α : Type u_1} [inst : MetricSpace α] [inst_1 : SecondCountableTopology α] [inst_2 : MeasurableSpace α]
[inst_3 : BorelSpace α] (μ : MeasureTheory.Measure α) [inst_4 : MeasureTheory.IsLocallyFiniteMeasure μ]
[inst_5 : IsUnifLocDoublingMeasure μ] (p : ℕ → Prop) (s : ℕ → Set α) {M : ℝ},
0 < M →
∀ (r : ℕ → ℝ),
Filter.Tendsto r Filter.atTop (nhds 0) →
(∀ᶠ (i : ℕ) in Filter.atTop, p i → 0 < r i) →
μ.ae.EventuallyEq (Filter.blimsup (fun i => Metric.thickening (M * r i) (s i)) Filter.atTop p)
(Filter.blimsup (fun i => Metric.thickening (r i) (s i)) Filter.atTop p)
This theorem, `blimsup_thickening_mul_ae_eq_aux`, states that given a metric space `α` (with additional properties of having a second-countable topology, being measurable, and being a Borel space), a measure `μ` on `α` (which is locally finite and satisfies a uniform local doubling condition), a function `p` from natural numbers to Propositions, a function `s` mapping natural numbers to sets in `α`, and a positive real number `M`, the following holds: for any function `r` from natural numbers to real numbers that tends to 0 as the argument tends to infinity (expressed as `Filter.Tendsto r Filter.atTop (nhds 0)`) and for which there is a stage beyond which, whenever `p i` holds, `r i` is positive (expressed as `∀ᶠ (i : ℕ) in Filter.atTop, p i → 0 < r i`), the almost everywhere limit superior (or `blimsup`) of the sequence of `δ`-thickenings of the sets `s i` scaled by `M * r i` equals the `blimsup` of the sequence of `δ`-thickenings of the same sets, but scaled by `r i` only. In other words, multiplying the thickening radius by a positive constant `M` doesn't change the `blimsup` in the end, when considering almost every point according to the measure `μ`.
More concisely: Given a second-countable and measurable Borel space `(α, Σ)` with a locally finite, uniformly doubling measure `μ`, and functions `p : ℕ → Prop`, `s : ℕ → Σ`, and `r : ℕ → ℝ` tending to 0, if there exists a stage beyond which `p i` implies `0 < r i`, then the almost everywhere limit superior of the scaled `δ`-thickenings of `s i` is equal to the almost everywhere limit superior of the unscaled `δ`-thickenings, where the scaling is given by `M * r i` and `r i`, respectively.
|
blimsup_cthickening_ae_le_of_eventually_mul_le_aux
theorem blimsup_cthickening_ae_le_of_eventually_mul_le_aux :
∀ {α : Type u_1} [inst : MetricSpace α] [inst_1 : SecondCountableTopology α] [inst_2 : MeasurableSpace α]
[inst_3 : BorelSpace α] (μ : MeasureTheory.Measure α) [inst_4 : MeasureTheory.IsLocallyFiniteMeasure μ]
[inst_5 : IsUnifLocDoublingMeasure μ] (p : ℕ → Prop) {s : ℕ → Set α},
(∀ (i : ℕ), IsClosed (s i)) →
∀ {r₁ r₂ : ℕ → ℝ},
Filter.Tendsto r₁ Filter.atTop (nhdsWithin 0 (Set.Ioi 0)) →
0 ≤ r₁ →
∀ {M : ℝ},
0 < M →
M < 1 →
(∀ᶠ (i : ℕ) in Filter.atTop, M * r₁ i ≤ r₂ i) →
μ.ae.EventuallyLE (Filter.blimsup (fun i => Metric.cthickening (r₁ i) (s i)) Filter.atTop p)
(Filter.blimsup (fun i => Metric.cthickening (r₂ i) (s i)) Filter.atTop p)
This theorem, `blimsup_cthickening_ae_le_of_eventually_mul_le_aux`, is a technical lemma on its way to proving `blimsup_cthickening_mul_ae_eq`. It states that in a metric space with a second countable topology, a measurable space, a Borel space, a measure, a locally finite measure, and a doubling measure, given a sequence of closed sets `s`, and two sequences of real numbers `r₁` and `r₂` such that `r₁` tends towards 0 within the positive numbers as it goes to infinity, and `r₁` is non-negative, then for every positive real number `M` less than 1, if eventually `M * r₁ i` is less than or equal to `r₂ i` for all `i` large enough, the almost everywhere limit superior (i.e., the infimum of the `a` such that `u x ≤ a` eventually holds) of the closed δ-thickening of `s i` with thickness `r₁ i` is less than or equal to the limit superior of the closed δ-thickening of `s i` with thickness `r₂ i`. Here, the closed δ-thickening of a set consists of those points whose minimum distance to the set is at most `δ`, and `p` is a property that each natural number can have.
More concisely: In a second countable metric space with a Borel sigma-algebra, a locally finite and doubling measure, given a sequence of closed sets `s` and real numbers `r₁` and `r₂` such that `r₁` approaches 0 and `M * r₁ ≤ r₂` eventually for all `M < 1`, the almost everywhere limit superior of the closed `δ`-thickening of `s` with thickness `r₁` is less than or equal to the limit superior of the closed `δ`-thickening of `s` with thickness `r₂`.
|
blimsup_cthickening_ae_le_of_eventually_mul_le
theorem blimsup_cthickening_ae_le_of_eventually_mul_le :
∀ {α : Type u_1} [inst : MetricSpace α] [inst_1 : SecondCountableTopology α] [inst_2 : MeasurableSpace α]
[inst_3 : BorelSpace α] (μ : MeasureTheory.Measure α) [inst_4 : MeasureTheory.IsLocallyFiniteMeasure μ]
[inst_5 : IsUnifLocDoublingMeasure μ] (p : ℕ → Prop) {s : ℕ → Set α} {M : ℝ},
0 < M →
∀ {r₁ r₂ : ℕ → ℝ},
Filter.Tendsto r₁ Filter.atTop (nhdsWithin 0 (Set.Ioi 0)) →
(∀ᶠ (i : ℕ) in Filter.atTop, M * r₁ i ≤ r₂ i) →
μ.ae.EventuallyLE (Filter.blimsup (fun i => Metric.cthickening (r₁ i) (s i)) Filter.atTop p)
(Filter.blimsup (fun i => Metric.cthickening (r₂ i) (s i)) Filter.atTop p)
This theorem, `blimsup_cthickening_ae_le_of_eventually_mul_le`, states that for any metric space (a space in which distances are measurable) that has a second countable topology (a topological space where the basis is countable), is measurable (you can measure subsets), and is a Borel space (a space where every open set is measurable), given a locally finite measure `μ` (a measure where every point has a neighborhood with finite measure) that is a uniformly locally doubling measure (a measure where every ball of radius `r` has measure at most twice the measure of the ball of radius `r/2`), a predicate `p` on natural numbers, and a sequence of sets `s` indexed by natural numbers, and a real number `M` greater than 0, for sequences of real numbers `r₁` and `r₂` such that `r₁` tends to 0 within the open interval (0, ∞) and `M * r₁ i` is less than or equal to `r₂ i` for all sufficiently large `i`, it asserts that almost everywhere (with respect to `μ`) the infimum (or greatest lower bound) of the set of all `a` such that eventually `Metric.cthickening (r₁ i) (s i) ≤ a` whenever `p i` holds, is less than or equal to the infimum of the set of all `a` such that eventually `Metric.cthickening (r₂ i) (s i) ≤ a` whenever `p i` holds. In simpler terms, the theorem relates the behavior of two sequences and their associated "thickenings" of sets, stating that if one sequence is eventually bounded by a multiple of the other, then the thickening of the sets by the first sequence is almost everywhere less than or equal to the thickening by the second sequence.
More concisely: For any second countable and measurable Borel space with a locally finite, uniformly locally doubling measure `μ`, if a sequence `(r_i)` tends to 0 and `M * r_i ≤ r'_i` for all sufficiently large `i`, then almost everywhere, the infimum of the set of all `a` such that eventually `Metric.cthickening (r_i) (si) ≤ a` whenever `pi` holds, is less than or equal to the infimum of the set of all `a` such that eventually `Metric.cthickening (r'_i) (si) ≤ a` whenever `pi` holds.
|