mulIndicator_thickening_eventually_eq_mulIndicator_closure
theorem mulIndicator_thickening_eventually_eq_mulIndicator_closure :
∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {β : Type u_2} [inst_1 : One β] (f : α → β) (E : Set α) (x : α),
∀ᶠ (δ : ℝ) in nhdsWithin 0 (Set.Ioi 0), (Metric.thickening δ E).mulIndicator f x = (closure E).mulIndicator f x
The theorem `mulIndicator_thickening_eventually_eq_mulIndicator_closure` states that for any set `E` in a pseudo emetric space `α` and any function `f` from `α` to a type `β` that has a multiplicative identity, and for any point `x` in `α`, the multiplicative indicator of the δ-thickening of `E` (which is the set of points at a distance less than `δ` from `E`) eventually equals the multiplicative indicator of the closure of `E` as `δ` tends to zero in the positive real numbers. In other words, as we gradually shrink the "buffer" around `E` (the δ-thickening), the resulting function eventually matches the one we get if we were to consider the smallest closed set that contains `E`. This happens in a neighborhood within the given point `x`.
More concisely: For any pseudo metric space `α`, set `E ⊆ α`, and function `f : α → β` with a multiplicative identity, the multiplicative indicators of the closure of `E` and the eventual limit of the δ-thickening of `E` at `x ∈ α` are equal.
|
indicator_cthickening_eventually_eq_indicator_closure
theorem indicator_cthickening_eventually_eq_indicator_closure :
∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {β : Type u_2} [inst_1 : Zero β] (f : α → β) (E : Set α) (x : α),
∀ᶠ (δ : ℝ) in nhds 0, (Metric.cthickening δ E).indicator f x = (closure E).indicator f x
The theorem `indicator_cthickening_eventually_eq_indicator_closure` states that, given a pseudo emetric space `α`, a zero `β`, a function `f` from `α` to `β`, a set `E` of `α`, and an element `x` of `α`, for all δ approaching 0 in the neighborhood, the indicator of the δ-thickening of `E` evaluated at `x` is equal to the indicator of the closure of `E` evaluated at `x`. In other words, as `δ` tends to zero, the indicators of the δ-thickenings of a set will eventually coincide with the indicator function of the closure of the set.
More concisely: For any pseudo metric space `α`, function `f` from `α` to a zero `β`, set `E` of `α`, and `x` in `α`, the indicator of the δ-thickening of `E` at `x` approaches the indicator of `E`'s closure at `x` as δ tends to zero.
|
tendsto_mulIndicator_cthickening_mulIndicator_closure
theorem tendsto_mulIndicator_cthickening_mulIndicator_closure :
∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {β : Type u_2} [inst_1 : One β] [inst_2 : TopologicalSpace β]
(f : α → β) (E : Set α),
Filter.Tendsto (fun δ => (Metric.cthickening δ E).mulIndicator f) (nhds 0) (nhds ((closure E).mulIndicator f))
This theorem states that for any set `E` in a pseudo emetric space `α` and any function `f` from `α` to `β` (where `β` is a topological space with a defined multiplication operation and an element identified as "one"), the multiplicative indicators of the closed `δ`-thickenings of `E` tend to the multiplicative indicator of the closure of the set `E` as `δ` tends to zero. The "multiplicative indicator" of a set with respect to a function is a function that is equal to the original function on the set and equal to one elsewhere. The "closure" of a set is the smallest closed set containing it, and a "δ-thickening" of a set is composed of points that are at most `δ` distance away from the set. The "tend to" here is defined in terms of filters, a generalization of sequences and limits to more general topological spaces.
More concisely: Given a pseudo metric space `α`, a set `E` in it, and a continuous function `f` to a topological space `β` with multiplication and identity element, the multiplicative indicators of the closures of the `δ`-thickenings of `E` converge to the multiplicative indicator of `E`'s closure as `δ` approaches zero.
|
tendsto_indicator_cthickening_indicator_closure
theorem tendsto_indicator_cthickening_indicator_closure :
∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {β : Type u_2} [inst_1 : Zero β] [inst_2 : TopologicalSpace β]
(f : α → β) (E : Set α),
Filter.Tendsto (fun δ => (Metric.cthickening δ E).indicator f) (nhds 0) (nhds ((closure E).indicator f))
This theorem states that for any pseudo emetric space `α`, any type `β` that has a zero element and a topology, and any function `f` from `α` to `β`, as well as any set `E` in `α`, the indicator functions of the closed `δ`-thickenings of `E` (denoted as `Metric.cthickening δ E`) tend to the indicator function of the closure of `E`, as `δ` tends to zero. Here, an indicator function of a set assigns the value one to the points in the set and zero to the points not in the set. In other words, as we consider increasingly tight thickenings of the set `E`, the indicator function of these thickenings converges to the indicator function of the closure of the set `E`. This is expressed in the language of filters with `Filter.Tendsto`, meaning that for every neighborhood of the limit (here, the indicator function of the closure of `E`), there is a neighborhood of zero such that the image of this neighborhood under the function (here, the indicator function of the `δ`-thickenings) is contained in the limit's neighborhood.
More concisely: For any pseudo metric space `α`, any type `β` with zero element and topology, and any continuous function `f` from `α` to `β` with respect to the given topologies, the indicator functions of the closed `δ`-thickenings of any set `E` in `α` converge to the indicator function of the closure of `E` as `δ` tends to zero.
|
thickenedIndicator_tendsto_indicator_closure
theorem thickenedIndicator_tendsto_indicator_closure :
∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {δseq : ℕ → ℝ} (δseq_pos : ∀ (n : ℕ), 0 < δseq n),
Filter.Tendsto δseq Filter.atTop (nhds 0) →
∀ (E : Set α),
Filter.Tendsto (fun n => ⇑(thickenedIndicator ⋯ E)) Filter.atTop (nhds ((closure E).indicator fun x => 1))
This theorem states that given a set `E` in a pseudo emetric space `α` and a sequence `δseq` of real numbers tending to 0 (where each `δseq` is greater than 0), the δ-thickened indicator function of `E` tends to the indicator function of the closure of `E`. Note that this is applied to bundled bounded continuous functions, but the topology we're dealing with is not the one on `α →ᵇ ℝ≥0`. Instead, the topology used is the product topology, which is the topology of pointwise convergence. The indicator function of a set assigns 1 to elements in the set and 0 to elements outside it. The δ-thickened indicator function is a modified version that also assigns 1 to elements within δ distance from the set. As δ tends to 0, the δ-thickened indicator function tends to the regular indicator function of the closure of the set.
More concisely: Given a set `E` in a pseudo metric space `α` and a sequence `δseq` tending to 0, the δ-thickened indicator functions of `E` converge pointwise to the indicator function of `E`'s closure.
|
thickenedIndicatorAux_le_one
theorem thickenedIndicatorAux_le_one :
∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (δ : ℝ) (E : Set α) (x : α), thickenedIndicatorAux δ E x ≤ 1 := by
sorry
This theorem states that for every pseudo emetric space `α`, every real number `δ`, every set `E` of elements of `α`, and every element `x` of `α`, the δ-thickened indicator of the set `E` evaluated at `x` is less than or equal to 1. In simpler terms, when we "thicken" a set in a pseudo emetric space and create a continuous function that equals 1 on the set and 0 outside the thickened set, the value of this function at any point in the space will always be less than or equal to 1.
More concisely: For every pseudo metric space `α`, every real number `δ`, and every set `E` in `α`, the δ-thickened indicator function of `E` is a continuous function with domain `α` that maps each element `x` in `α` to a value less than or equal to 1.
|
indicator_thickening_eventually_eq_indicator_closure
theorem indicator_thickening_eventually_eq_indicator_closure :
∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {β : Type u_2} [inst_1 : Zero β] (f : α → β) (E : Set α) (x : α),
∀ᶠ (δ : ℝ) in nhdsWithin 0 (Set.Ioi 0), (Metric.thickening δ E).indicator f x = (closure E).indicator f x
The theorem `indicator_thickening_eventually_eq_indicator_closure` states that, for a given function `f` mapping from a type `α` in a pseudo emetric space to a type `β` with a zero element, and a given set `E` of `α` elements, at some point `x` in `α`, the indicators of `δ`-thickenings of the set `E` are the same as the indicator of the closure of `E` as `δ` tends to 0. In other words, if you take the set `E` and continuously expand it by a small amount `δ`, eventually the indicator function for this expanding set will be the same as the indicator function for the smallest closed set containing `E`. This eventuality is observed when `δ` is in the neighbourhood within the set of all positive numbers and 0.
More concisely: For a given pseudo metric space `(α, d)`, a function `f : α → β` with `β` having a zero element, and a set `E ⊆ α`, as `δ` approaches 0, the indicators of `E`'s `δ`-thickenings equal the indicator of `E`'s closure.
|
thickenedIndicatorAux_lt_top
theorem thickenedIndicatorAux_lt_top :
∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {δ : ℝ} {E : Set α} {x : α}, thickenedIndicatorAux δ E x < ⊤ := by
sorry
The theorem `thickenedIndicatorAux_lt_top` states that for any type `α` equipped with a pseudometric space structure, for any real number `δ`, any set `E` of type `α`, and any element `x` of type `α`, the value of the δ-thickened indicator function at `x` is always less than infinity. This essentially means that the δ-thickened indicator function always returns a finite value when given any element of the set.
More concisely: For any pseudometric space `(α, d)`, real number `δ`, set `E ∈ α`, and `x ∈ α`, the value `thickenedIndicatorAux δ E x` is finite.
|
Mathlib.Topology.MetricSpace.ThickenedIndicator._auxLemma.2
theorem Mathlib.Topology.MetricSpace.ThickenedIndicator._auxLemma.2 : (¬False) = True
This theorem, titled `Mathlib.Topology.MetricSpace.ThickenedIndicator._auxLemma.2`, states a simple logical equivalence in Boolean logic. Specifically, it asserts the proposition that the negation of `False` (`¬False`) is equal to `True`. This theorem applies in all contexts, and is a fundamental result of Boolean algebra.
More concisely: The theorem asserts that the negation of False is equivalent to True in Boolean logic.
|
thickenedIndicatorAux_tendsto_indicator_closure
theorem thickenedIndicatorAux_tendsto_indicator_closure :
∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {δseq : ℕ → ℝ},
Filter.Tendsto δseq Filter.atTop (nhds 0) →
∀ (E : Set α),
Filter.Tendsto (fun n => thickenedIndicatorAux (δseq n) E) Filter.atTop
(nhds ((closure E).indicator fun x => 1))
This theorem states that, in a pseudo-metric space α, as the thickening radius δ approaches 0, the δ-thickened indicator of a set E in α converges pointwise (with respect to the product topology on the function space from α to ℝ≥0∞) to the indicator function of the closure of E. Here, the δ-thickened indicator of E is a function that equals 1 on E, equals 0 outside a δ-thickening of E, and interpolates continuously between these values. The thickening radius δ is given by a sequence of real numbers that tends to 0. This result applies to unbundled ℝ≥0∞-valued functions. There is a corresponding version of this theorem for bundled ℝ≥0-valued bounded continuous functions.
More concisely: In a pseudo-metric space, as the thickening radius approaches 0, the pointwise limit of the δ-thickened indicator functions equals the indicator function of the closure for unbundled ℝ≥0∞-valued functions.
|
mulIndicator_cthickening_eventually_eq_mulIndicator_closure
theorem mulIndicator_cthickening_eventually_eq_mulIndicator_closure :
∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {β : Type u_2} [inst_1 : One β] (f : α → β) (E : Set α) (x : α),
∀ᶠ (δ : ℝ) in nhds 0, (Metric.cthickening δ E).mulIndicator f x = (closure E).mulIndicator f x
The theorem `mulIndicator_cthickening_eventually_eq_mulIndicator_closure` states that for any set `E` in a pseudo emetric space and any point `x`, the multiplicative indicators (which assigns the function's value to points in the set and assigns one to points not in the set) of the closed `δ`-thickenings of the set `E` (consisting of those points that are at infimum distance at most `δ` from `E`) eventually coincide with the multiplicative indicator of the closure of `E` as `δ` tends to zero. This means that as we keep reducing `δ`, making the δ-thickening of the set `E` smaller and smaller, there comes a point after which the multiplicative indicators of these δ-thickenings and that of the closure of `E` become identical. This is all described in the context of a topology induced by a pseudo emetric space.
More concisely: For any set E in a pseudo metric space and point x, the multiplicative indicators of E's closed δ-thickening eventually equal the multiplicative indicator of E's closure as δ approaches zero.
|
tendsto_mulIndicator_thickening_mulIndicator_closure
theorem tendsto_mulIndicator_thickening_mulIndicator_closure :
∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {β : Type u_2} [inst_1 : One β] [inst_2 : TopologicalSpace β]
(f : α → β) (E : Set α),
Filter.Tendsto (fun δ => (Metric.thickening δ E).mulIndicator f) (nhdsWithin 0 (Set.Ioi 0))
(nhds ((closure E).mulIndicator f))
The theorem `tendsto_mulIndicator_thickening_mulIndicator_closure` states that for any set `E` in a pseudo emetric space `α` (a generalization of the concept of a metric space) and a function `f` from `α` to another topological space `β` that has a multiplicative identity, the multiplicative indicators of the δ-thickenings of `E` tend towards the multiplicative indicator of the closure of `E` as δ (which is positive) tends towards 0. Here, a δ-thickening of a set refers to all points that are within a distance of δ from any point in the set, and the closure of a set is the smallest closed set containing the set. The convergence is understood in the sense that for any neighborhood of the multiplicative indicator of the closure of `E`, there exists a right-open interval around 0 such that the multiplicative indicators of all δ-thickenings for δ in this interval belong to this neighborhood.
More concisely: For any pseudo-metric space (α, d) and a function f from α to a topological space β with a multiplicative identity, the multiplicative indicators of the δ-thickenings of a set E in α converge to the multiplicative indicator of E's closure as δ approaches 0.
|
tendsto_indicator_thickening_indicator_closure
theorem tendsto_indicator_thickening_indicator_closure :
∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {β : Type u_2} [inst_1 : Zero β] [inst_2 : TopologicalSpace β]
(f : α → β) (E : Set α),
Filter.Tendsto (fun δ => (Metric.thickening δ E).indicator f) (nhdsWithin 0 (Set.Ioi 0))
(nhds ((closure E).indicator f))
The theorem `tendsto_indicator_thickening_indicator_closure` states that for any pseudo emetric space `α`, any type `β` that has a zero element and a topological structure, a function `f` from `α` to `β`, and a set `E` of type `α`, the indicators of δ-thickenings of the set `E` tend pointwise to the indicator of the closure of `E` as δ, which is greater than zero, tends to zero. Here, the δ-thickening of a set refers to the set of points that are at distance less than δ from some point of the set, and the indicator of a set is a function that is zero off the set and one on the set. The function `nhdsWithin 0 (Set.Ioi 0)` refers to values of δ that approach zero from the right, i.e., δ > 0. The limit is taken in the topology on `β`.
More concisely: For any pseudo metric space α, any type β with a zero element and topology, and any function f from α to β, the pointwise limit of indicators of δ-thickenings of a set E in α is equal to the indicator of the closure of E as δ approaches 0 from the right.
|