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 #

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} [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

thickened_indicator_aux δ E = λ (x : α), 1 - emetric.inf_edist x E / ennreal.of_real δ

theorem continuous_thickened_indicator_aux {α : Type u_1} [pseudo_emetric_space α] {δ : ℝ} (δ_pos : 0 < δ) (E : set α) :

continuous (thickened_indicator_aux δ E)

theorem thickened_indicator_aux_le_one {α : Type u_1} [pseudo_emetric_space α] (δ : ℝ) (E : set α) (x : α) :

thickened_indicator_aux δ E x ≤ 1

theorem thickened_indicator_aux_lt_top {α : Type u_1} [pseudo_emetric_space α] {δ : ℝ} {E : set α} {x : α} :

thickened_indicator_aux δ E x < ⊤

theorem thickened_indicator_aux_closure_eq {α : Type u_1} [pseudo_emetric_space α] (δ : ℝ) (E : set α) :

thickened_indicator_aux δ (closure E) = thickened_indicator_aux δ E

theorem thickened_indicator_aux_one {α : Type u_1} [pseudo_emetric_space α] (δ : ℝ) (E : set α) {x : α} (x_in_E : x ∈ E) :

thickened_indicator_aux δ E x = 1

theorem thickened_indicator_aux_one_of_mem_closure {α : Type u_1} [pseudo_emetric_space α] (δ : ℝ) (E : set α) {x : α} (x_mem : x ∈ closure E) :

thickened_indicator_aux δ E x = 1

theorem thickened_indicator_aux_zero {α : Type u_1} [pseudo_emetric_space α] {δ : ℝ} (δ_pos : 0 < δ) (E : set α) {x : α} (x_out : x ∉ metric.thickening δ E) :

thickened_indicator_aux δ E x = 0

theorem thickened_indicator_aux_mono {α : Type u_1} [pseudo_emetric_space α] {δ₁ δ₂ : ℝ} (hle : δ₁ ≤ δ₂) (E : set α) :

thickened_indicator_aux δ₁ E ≤ thickened_indicator_aux δ₂ E

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₂) :

thickened_indicator_aux δ E₁ ≤ thickened_indicator_aux δ 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 : α) :

⇑(thickened_indicator δ_pos E) x = (thickened_indicator_aux δ E x).to_nnreal

noncomputable def thickened_indicator {α : Type u_1} [pseudo_emetric_space α] {δ : ℝ} (δ_pos : 0 < δ) (E : set α) :

bounded_continuous_function α nnreal

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

thickened_indicator δ_pos E = {to_continuous_map := {to_fun := λ (x : α), (thickened_indicator_aux δ E x).to_nnreal, continuous_to_fun := _}, map_bounded' := _}

@[simp]

theorem thickened_indicator_to_continuous_map_apply {α : Type u_1} [pseudo_emetric_space α] {δ : ℝ} (δ_pos : 0 < δ) (E : set α) (x : α) :

⇑((thickened_indicator δ_pos E).to_continuous_map) x = (thickened_indicator_aux δ E x).to_nnreal

theorem thickened_indicator.coe_fn_eq_comp {α : Type u_1} [pseudo_emetric_space α] {δ : ℝ} (δ_pos : 0 < δ) (E : set α) :

⇑(thickened_indicator δ_pos E) = ennreal.to_nnreal ∘ thickened_indicator_aux δ E

theorem thickened_indicator_le_one {α : Type u_1} [pseudo_emetric_space α] {δ : ℝ} (δ_pos : 0 < δ) (E : set α) (x : α) :

⇑(thickened_indicator δ_pos E) x ≤ 1

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 α) :

⇑(thickened_indicator δ₁_pos E) ≤ ⇑(thickened_indicator δ₂_pos E)

theorem thickened_indicator_subset {α : Type u_1} [pseudo_emetric_space α] {δ : ℝ} (δ_pos : 0 < δ) {E₁ E₂ : set α} (subset : E₁ ⊆ E₂) :

⇑(thickened_indicator δ_pos E₁) ≤ ⇑(thickened_indicator δ_pos 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).