mathlib3 documentation

topology.metric_space.thickened_indicator

Thickened indicators #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file is about thickened indicators of sets in (pseudo e)metric spaces. For a decreasing sequence of thickening radii tending to 0, the thickened indicators of a closed set form a decreasing pointwise converging approximation of the indicator function of the set, where the members of the approximating sequence are nonnegative bounded continuous functions.

Main definitions #

Main results #

noncomputable def thickened_indicator_aux {α : Type u_1} [pseudo_emetric_space α] (δ : ) (E : set α) :

The δ-thickened indicator of a set E is the function that equals 1 on E and 0 outside a δ-thickening of E and interpolates (continuously) between these values using inf_edist _ E.

thickened_indicator_aux is the unbundled ℝ≥0∞-valued function. See thickened_indicator for the (bundled) bounded continuous function with ℝ≥0-values.

Equations
theorem continuous_thickened_indicator_aux {α : Type u_1} [pseudo_emetric_space α] {δ : } (δ_pos : 0 < δ) (E : set α) :
theorem thickened_indicator_aux_le_one {α : Type u_1} [pseudo_emetric_space α] (δ : ) (E : set α) (x : α) :
theorem thickened_indicator_aux_lt_top {α : Type u_1} [pseudo_emetric_space α] {δ : } {E : set α} {x : α} :
theorem thickened_indicator_aux_one {α : Type u_1} [pseudo_emetric_space α] (δ : ) (E : set α) {x : α} (x_in_E : x E) :
theorem thickened_indicator_aux_one_of_mem_closure {α : Type u_1} [pseudo_emetric_space α] (δ : ) (E : set α) {x : α} (x_mem : x closure E) :
theorem thickened_indicator_aux_zero {α : Type u_1} [pseudo_emetric_space α] {δ : } (δ_pos : 0 < δ) (E : set α) {x : α} (x_out : x metric.thickening δ E) :
theorem thickened_indicator_aux_mono {α : Type u_1} [pseudo_emetric_space α] {δ₁ δ₂ : } (hle : δ₁ δ₂) (E : set α) :
theorem indicator_le_thickened_indicator_aux {α : Type u_1} [pseudo_emetric_space α] (δ : ) (E : set α) :
E.indicator (λ (_x : α), 1) thickened_indicator_aux δ E
theorem thickened_indicator_aux_subset {α : Type u_1} [pseudo_emetric_space α] (δ : ) {E₁ E₂ : set α} (subset : E₁ E₂) :
theorem thickened_indicator_aux_tendsto_indicator_closure {α : Type u_1} [pseudo_emetric_space α] {δseq : } (δseq_lim : filter.tendsto δseq filter.at_top (nhds 0)) (E : set α) :
filter.tendsto (λ (n : ), thickened_indicator_aux (δseq n) E) filter.at_top (nhds ((closure E).indicator (λ (x : α), 1)))

As the thickening radius δ tends to 0, the δ-thickened indicator of a set E (in α) tends pointwise (i.e., w.r.t. the product topology on α → ℝ≥0∞) to the indicator function of the closure of E.

This statement is for the unbundled ℝ≥0∞-valued functions thickened_indicator_aux δ E, see thickened_indicator_tendsto_indicator_closure for the version for bundled ℝ≥0-valued bounded continuous functions.

@[simp]
theorem thickened_indicator_apply {α : Type u_1} [pseudo_emetric_space α] {δ : } (δ_pos : 0 < δ) (E : set α) (x : α) :
noncomputable def thickened_indicator {α : Type u_1} [pseudo_emetric_space α] {δ : } (δ_pos : 0 < δ) (E : set α) :

The δ-thickened indicator of a set E is the function that equals 1 on E and 0 outside a δ-thickening of E and interpolates (continuously) between these values using inf_edist _ E.

thickened_indicator is the (bundled) bounded continuous function with ℝ≥0-values. See thickened_indicator_aux for the unbundled ℝ≥0∞-valued function.

Equations
@[simp]
theorem thickened_indicator_to_continuous_map_apply {α : Type u_1} [pseudo_emetric_space α] {δ : } (δ_pos : 0 < δ) (E : set α) (x : α) :
theorem thickened_indicator_le_one {α : Type u_1} [pseudo_emetric_space α] {δ : } (δ_pos : 0 < δ) (E : set α) (x : α) :
theorem thickened_indicator_one_of_mem_closure {α : Type u_1} [pseudo_emetric_space α] {δ : } (δ_pos : 0 < δ) (E : set α) {x : α} (x_mem : x closure E) :
(thickened_indicator δ_pos E) x = 1
theorem thickened_indicator_one {α : Type u_1} [pseudo_emetric_space α] {δ : } (δ_pos : 0 < δ) (E : set α) {x : α} (x_in_E : x E) :
(thickened_indicator δ_pos E) x = 1
theorem thickened_indicator_zero {α : Type u_1} [pseudo_emetric_space α] {δ : } (δ_pos : 0 < δ) (E : set α) {x : α} (x_out : x metric.thickening δ E) :
(thickened_indicator δ_pos E) x = 0
theorem indicator_le_thickened_indicator {α : Type u_1} [pseudo_emetric_space α] {δ : } (δ_pos : 0 < δ) (E : set α) :
E.indicator (λ (_x : α), 1) (thickened_indicator δ_pos E)
theorem thickened_indicator_mono {α : Type u_1} [pseudo_emetric_space α] {δ₁ δ₂ : } (δ₁_pos : 0 < δ₁) (δ₂_pos : 0 < δ₂) (hle : δ₁ δ₂) (E : set α) :
theorem thickened_indicator_subset {α : Type u_1} [pseudo_emetric_space α] {δ : } (δ_pos : 0 < δ) {E₁ E₂ : set α} (subset : E₁ E₂) :
theorem thickened_indicator_tendsto_indicator_closure {α : Type u_1} [pseudo_emetric_space α] {δseq : } (δseq_pos : (n : ), 0 < δseq n) (δseq_lim : filter.tendsto δseq filter.at_top (nhds 0)) (E : set α) :
filter.tendsto (λ (n : ), (thickened_indicator _ E)) filter.at_top (nhds ((closure E).indicator (λ (x : α), 1)))

As the thickening radius δ tends to 0, the δ-thickened indicator of a set E (in α) tends pointwise to the indicator function of the closure of E.

Note: This version is for the bundled bounded continuous functions, but the topology is not the topology on α →ᵇ ℝ≥0. Coercions to functions α → ℝ≥0 are done first, so the topology instance is the product topology (the topology of pointwise convergence).