# mathlibdocumentation

topology.metric_space.thickened_indicator

# Thickened indicators #

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 #

• thickened_indicator_aux δ E: The δ-thickened indicator of a set E as an unbundled ℝ≥0∞-valued function.
• thickened_indicator δ E: The δ-thickened indicator of a set E as a bundled bounded continuous ℝ≥0-valued function.

## Main results #

• For a sequence of thickening radii tending to 0, the δ-thickened indicators of a set E tend pointwise to the indicator of closure E.
• thickened_indicator_aux_tendsto_indicator_closure: The version is for the unbundled ℝ≥0∞-valued functions.
• thickened_indicator_tendsto_indicator_closure: The version is for the bundled ℝ≥0-valued bounded continuous functions.
noncomputable def thickened_indicator_aux {α : Type u_1} (δ : ) (E : set α) :
α → ennreal

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
• = λ (x : α), 1 -
theorem continuous_thickened_indicator_aux {α : Type u_1} {δ : } (δ_pos : 0 < δ) (E : set α) :
theorem thickened_indicator_aux_le_one {α : Type u_1} (δ : ) (E : set α) (x : α) :
1
theorem thickened_indicator_aux_lt_top {α : Type u_1} {δ : } {E : set α} {x : α} :
theorem thickened_indicator_aux_closure_eq {α : Type u_1} (δ : ) (E : set α) :
theorem thickened_indicator_aux_one {α : Type u_1} (δ : ) (E : set α) {x : α} (x_in_E : x E) :
= 1
theorem thickened_indicator_aux_one_of_mem_closure {α : Type u_1} (δ : ) (E : set α) {x : α} (x_mem : x ) :
= 1
theorem thickened_indicator_aux_zero {α : Type u_1} {δ : } (δ_pos : 0 < δ) (E : set α) {x : α} (x_out : x ) :
= 0
theorem thickened_indicator_aux_mono {α : Type u_1} {δ₁ δ₂ : } (hle : δ₁ δ₂) (E : set α) :
theorem indicator_le_thickened_indicator_aux {α : Type u_1} (δ : ) (E : set α) :
E.indicator (λ (_x : α), 1)
theorem thickened_indicator_aux_subset {α : Type u_1} (δ : ) {E₁ E₂ : set α} (subset : E₁ E₂) :
theorem thickened_indicator_aux_tendsto_indicator_closure {α : Type u_1} {δseq : } (δseq_lim : (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} {δ : } (δ_pos : 0 < δ) (E : set α) (x : α) :
@[simp]
theorem thickened_indicator_to_continuous_map_to_fun {α : Type u_1} {δ : } (δ_pos : 0 < δ) (E : set α) (x : α) :
noncomputable def thickened_indicator {α : Type u_1} {δ : } (δ_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
theorem thickened_indicator.coe_fn_eq_comp {α : Type u_1} {δ : } (δ_pos : 0 < δ) (E : set α) :
theorem thickened_indicator_le_one {α : Type u_1} {δ : } (δ_pos : 0 < δ) (E : set α) (x : α) :
theorem thickened_indicator_one_of_mem_closure {α : Type u_1} {δ : } (δ_pos : 0 < δ) (E : set α) {x : α} (x_mem : x ) :
(thickened_indicator δ_pos E) x = 1
theorem thickened_indicator_one {α : Type u_1} {δ : } (δ_pos : 0 < δ) (E : set α) {x : α} (x_in_E : x E) :
(thickened_indicator δ_pos E) x = 1
theorem thickened_indicator_zero {α : Type u_1} {δ : } (δ_pos : 0 < δ) (E : set α) {x : α} (x_out : x ) :
(thickened_indicator δ_pos E) x = 0
theorem indicator_le_thickened_indicator {α : Type u_1} {δ : } (δ_pos : 0 < δ) (E : set α) :
E.indicator (λ (_x : α), 1) (thickened_indicator δ_pos E)
theorem thickened_indicator_mono {α : Type u_1} {δ₁ δ₂ : } (δ₁_pos : 0 < δ₁) (δ₂_pos : 0 < δ₂) (hle : δ₁ δ₂) (E : set α) :
theorem thickened_indicator_subset {α : Type u_1} {δ : } (δ_pos : 0 < δ) {E₁ E₂ : set α} (subset : E₁ E₂) :
theorem thickened_indicator_tendsto_indicator_closure {α : Type u_1} {δseq : } (δseq_pos : ∀ (n : ), 0 < δseq n) (δseq_lim : (nhds 0)) (E : set α) :
filter.tendsto (λ (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 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).