# 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 #

• thickenedIndicatorAux δ E: The δ-thickened indicator of a set E as an unbundled ℝ≥0∞-valued function.
• thickenedIndicator δ 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.
• thickenedIndicatorAux_tendsto_indicator_closure: The version is for the unbundled ℝ≥0∞-valued functions.
• thickenedIndicator_tendsto_indicator_closure: The version is for the bundled ℝ≥0-valued bounded continuous functions.
def thickenedIndicatorAux {α : 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 infEdist _ E.

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

Equations
Instances For
theorem continuous_thickenedIndicatorAux {α : Type u_1} {δ : } (δ_pos : 0 < δ) (E : Set α) :
theorem thickenedIndicatorAux_le_one {α : Type u_1} (δ : ) (E : Set α) (x : α) :
1
theorem thickenedIndicatorAux_lt_top {α : Type u_1} {δ : } {E : Set α} {x : α} :
theorem thickenedIndicatorAux_closure_eq {α : Type u_1} (δ : ) (E : Set α) :
theorem thickenedIndicatorAux_one {α : Type u_1} (δ : ) (E : Set α) {x : α} (x_in_E : x E) :
= 1
theorem thickenedIndicatorAux_one_of_mem_closure {α : Type u_1} (δ : ) (E : Set α) {x : α} (x_mem : x ) :
= 1
theorem thickenedIndicatorAux_zero {α : Type u_1} {δ : } (δ_pos : 0 < δ) (E : Set α) {x : α} (x_out : x) :
= 0
theorem thickenedIndicatorAux_mono {α : Type u_1} {δ₁ : } {δ₂ : } (hle : δ₁ δ₂) (E : Set α) :
theorem indicator_le_thickenedIndicatorAux {α : Type u_1} (δ : ) (E : Set α) :
(Set.indicator E fun (x : α) => 1)
theorem thickenedIndicatorAux_subset {α : Type u_1} (δ : ) {E₁ : Set α} {E₂ : Set α} (subset : E₁ E₂) :
theorem thickenedIndicatorAux_tendsto_indicator_closure {α : Type u_1} {δseq : } (δseq_lim : Filter.Tendsto δseq Filter.atTop (nhds 0)) (E : Set α) :
Filter.Tendsto (fun (n : ) => thickenedIndicatorAux (δseq n) E) Filter.atTop (nhds (Set.indicator () fun (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 thickenedIndicatorAux δ E, see thickenedIndicator_tendsto_indicator_closure for the version for bundled ℝ≥0-valued bounded continuous functions.

@[simp]
theorem thickenedIndicator_apply {α : Type u_1} {δ : } (δ_pos : 0 < δ) (E : Set α) (x : α) :
(thickenedIndicator δ_pos E) x = ().toNNReal
@[simp]
theorem thickenedIndicator_toFun {α : Type u_1} {δ : } (δ_pos : 0 < δ) (E : Set α) (x : α) :
(thickenedIndicator δ_pos E) x = ().toNNReal
def thickenedIndicator {α : 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 infEdist _ E.

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem thickenedIndicator.coeFn_eq_comp {α : Type u_1} {δ : } (δ_pos : 0 < δ) (E : Set α) :
(thickenedIndicator δ_pos E) =
theorem thickenedIndicator_le_one {α : Type u_1} {δ : } (δ_pos : 0 < δ) (E : Set α) (x : α) :
(thickenedIndicator δ_pos E) x 1
theorem thickenedIndicator_one_of_mem_closure {α : Type u_1} {δ : } (δ_pos : 0 < δ) (E : Set α) {x : α} (x_mem : x ) :
(thickenedIndicator δ_pos E) x = 1
theorem one_le_thickenedIndicator_apply' {X : Type u_2} {δ : } (δ_pos : 0 < δ) {F : Set X} {x : X} (hxF : x ) :
1 (thickenedIndicator δ_pos F) x
theorem one_le_thickenedIndicator_apply (X : Type u_2) {δ : } (δ_pos : 0 < δ) {F : Set X} {x : X} (hxF : x F) :
1 (thickenedIndicator δ_pos F) x
theorem thickenedIndicator_one {α : Type u_1} {δ : } (δ_pos : 0 < δ) (E : Set α) {x : α} (x_in_E : x E) :
(thickenedIndicator δ_pos E) x = 1
theorem thickenedIndicator_zero {α : Type u_1} {δ : } (δ_pos : 0 < δ) (E : Set α) {x : α} (x_out : x) :
(thickenedIndicator δ_pos E) x = 0
theorem indicator_le_thickenedIndicator {α : Type u_1} {δ : } (δ_pos : 0 < δ) (E : Set α) :
(Set.indicator E fun (x : α) => 1) (thickenedIndicator δ_pos E)
theorem thickenedIndicator_mono {α : Type u_1} {δ₁ : } {δ₂ : } (δ₁_pos : 0 < δ₁) (δ₂_pos : 0 < δ₂) (hle : δ₁ δ₂) (E : Set α) :
(thickenedIndicator δ₁_pos E) (thickenedIndicator δ₂_pos E)
theorem thickenedIndicator_subset {α : Type u_1} {δ : } (δ_pos : 0 < δ) {E₁ : Set α} {E₂ : Set α} (subset : E₁ E₂) :
(thickenedIndicator δ_pos E₁) (thickenedIndicator δ_pos E₂)
theorem thickenedIndicator_tendsto_indicator_closure {α : Type u_1} {δseq : } (δseq_pos : ∀ (n : ), 0 < δseq n) (δseq_lim : Filter.Tendsto δseq Filter.atTop (nhds 0)) (E : Set α) :
Filter.Tendsto (fun (n : ) => (thickenedIndicator (_ : 0 < δseq n) E)) Filter.atTop (nhds (Set.indicator () fun (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).

theorem indicator_thickening_eventually_eq_indicator_closure {α : Type u_1} {β : Type u_2} [Zero β] (f : αβ) (E : Set α) (x : α) :
∀ᶠ (δ : ) in nhdsWithin 0 (), Set.indicator () f x = Set.indicator () f x

Pointwise, the indicators of δ-thickenings of a set eventually coincide with the indicator of the set as δ>0 tends to zero.

theorem mulIndicator_thickening_eventually_eq_mulIndicator_closure {α : Type u_1} {β : Type u_2} [One β] (f : αβ) (E : Set α) (x : α) :
∀ᶠ (δ : ) in nhdsWithin 0 (), = Set.mulIndicator () f x

Pointwise, the multiplicative indicators of δ-thickenings of a set eventually coincide with the multiplicative indicator of the set as δ>0 tends to zero.

theorem indicator_cthickening_eventually_eq_indicator_closure {α : Type u_1} {β : Type u_2} [Zero β] (f : αβ) (E : Set α) (x : α) :
∀ᶠ (δ : ) in nhds 0, Set.indicator () f x = Set.indicator () f x

Pointwise, the indicators of closed δ-thickenings of a set eventually coincide with the indicator of the set as δ tends to zero.

theorem mulIndicator_cthickening_eventually_eq_mulIndicator_closure {α : Type u_1} {β : Type u_2} [One β] (f : αβ) (E : Set α) (x : α) :
∀ᶠ (δ : ) in nhds 0, = Set.mulIndicator () f x

Pointwise, the multiplicative indicators of closed δ-thickenings of a set eventually coincide with the multiplicative indicator of the set as δ tends to zero.

theorem tendsto_indicator_thickening_indicator_closure {α : Type u_1} {β : Type u_2} [Zero β] [] (f : αβ) (E : Set α) :
Filter.Tendsto (fun (δ : ) => ) (nhdsWithin 0 ()) (nhds (Set.indicator () f))

The indicators of δ-thickenings of a set tend pointwise to the indicator of the set, as δ>0 tends to zero.

theorem tendsto_mulIndicator_thickening_mulIndicator_closure {α : Type u_1} {β : Type u_2} [One β] [] (f : αβ) (E : Set α) :
Filter.Tendsto (fun (δ : ) => ) (nhdsWithin 0 ()) (nhds ())

The multiplicative indicators of δ-thickenings of a set tend pointwise to the multiplicative indicator of the set, as δ>0 tends to zero.

theorem tendsto_indicator_cthickening_indicator_closure {α : Type u_1} {β : Type u_2} [Zero β] [] (f : αβ) (E : Set α) :
Filter.Tendsto (fun (δ : ) => ) (nhds 0) (nhds (Set.indicator () f))

The indicators of closed δ-thickenings of a set tend pointwise to the indicator of the set, as δ tends to zero.

theorem tendsto_mulIndicator_cthickening_mulIndicator_closure {α : Type u_1} {β : Type u_2} [One β] [] (f : αβ) (E : Set α) :
Filter.Tendsto (fun (δ : ) => ) (nhds 0) (nhds ())

The multiplicative indicators of closed δ-thickenings of a set tend pointwise to the multiplicative indicator of the set, as δ tends to zero.