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} [PseudoEMetricSpace α] (δ : ℝ) (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

• thickenedIndicatorAux δ E x = 1 - EMetric.infEdist x E / ENNReal.ofReal δ

theorem continuous_thickenedIndicatorAux {α : Type u_1} [PseudoEMetricSpace α] {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) : Continuous (thickenedIndicatorAux δ E)

theorem thickenedIndicatorAux_le_one {α : Type u_1} [PseudoEMetricSpace α] (δ : ℝ) (E : Set α) (x : α) : thickenedIndicatorAux δ E x ≤ 1

theorem thickenedIndicatorAux_lt_top {α : Type u_1} [PseudoEMetricSpace α] {δ : ℝ} {E : Set α} {x : α} : thickenedIndicatorAux δ E x < ⊤

theorem thickenedIndicatorAux_closure_eq {α : Type u_1} [PseudoEMetricSpace α] (δ : ℝ) (E : Set α) : thickenedIndicatorAux δ (closure E) = thickenedIndicatorAux δ E

theorem thickenedIndicatorAux_one {α : Type u_1} [PseudoEMetricSpace α] (δ : ℝ) (E : Set α) {x : α} (x_in_E : x ∈ E) : thickenedIndicatorAux δ E x = 1

theorem thickenedIndicatorAux_one_of_mem_closure {α : Type u_1} [PseudoEMetricSpace α] (δ : ℝ) (E : Set α) {x : α} (x_mem : x ∈ closure E) : thickenedIndicatorAux δ E x = 1

theorem thickenedIndicatorAux_zero {α : Type u_1} [PseudoEMetricSpace α] {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) {x : α} (x_out : x ∉ Metric.thickening δ E) : thickenedIndicatorAux δ E x = 0

theorem thickenedIndicatorAux_mono {α : Type u_1} [PseudoEMetricSpace α] {δ₁ δ₂ : ℝ} (hle : δ₁ ≤ δ₂) (E : Set α) : thickenedIndicatorAux δ₁ E ≤ thickenedIndicatorAux δ₂ E

theorem indicator_le_thickenedIndicatorAux {α : Type u_1} [PseudoEMetricSpace α] (δ : ℝ) (E : Set α) : (E.indicator fun (x : α) => 1) ≤ thickenedIndicatorAux δ E

theorem thickenedIndicatorAux_subset {α : Type u_1} [PseudoEMetricSpace α] (δ : ℝ) {E₁ E₂ : Set α} (subset : E₁ ⊆ E₂) : thickenedIndicatorAux δ E₁ ≤ thickenedIndicatorAux δ E₂

theorem thickenedIndicatorAux_tendsto_indicator_closure {α : Type u_1} [PseudoEMetricSpace α] {δseq : ℕ → ℝ} (δseq_lim : 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))

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.

def thickenedIndicator {α : Type u_1} [PseudoEMetricSpace α] {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) : BoundedContinuousFunction α 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 infEdist _ E.

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

Equations

• thickenedIndicator δ_pos E = { toFun := fun (x : α) => (thickenedIndicatorAux δ E x).toNNReal, continuous_toFun := ⋯, map_bounded' := ⋯ }

@[simp]

theorem thickenedIndicator_apply {α : Type u_1} [PseudoEMetricSpace α] {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) (x : α) : (thickenedIndicator δ_pos E) x = (thickenedIndicatorAux δ E x).toNNReal

@[simp]

theorem thickenedIndicator_toFun {α : Type u_1} [PseudoEMetricSpace α] {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) (x : α) : (thickenedIndicator δ_pos E) x = (thickenedIndicatorAux δ E x).toNNReal

theorem thickenedIndicator.coeFn_eq_comp {α : Type u_1} [PseudoEMetricSpace α] {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) : ⇑(thickenedIndicator δ_pos E) = ENNReal.toNNReal ∘ thickenedIndicatorAux δ E

theorem thickenedIndicator_le_one {α : Type u_1} [PseudoEMetricSpace α] {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) (x : α) : (thickenedIndicator δ_pos E) x ≤ 1

theorem thickenedIndicator_one_of_mem_closure {α : Type u_1} [PseudoEMetricSpace α] {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) {x : α} (x_mem : x ∈ closure E) : (thickenedIndicator δ_pos E) x = 1

theorem one_le_thickenedIndicator_apply' {X : Type u_2} [PseudoEMetricSpace X] {δ : ℝ} (δ_pos : 0 < δ) {F : Set X} {x : X} (hxF : x ∈ closure F) : 1 ≤ (thickenedIndicator δ_pos F) x

theorem one_le_thickenedIndicator_apply (X : Type u_2) [PseudoEMetricSpace X] {δ : ℝ} (δ_pos : 0 < δ) {F : Set X} {x : X} (hxF : x ∈ F) : 1 ≤ (thickenedIndicator δ_pos F) x

theorem thickenedIndicator_one {α : Type u_1} [PseudoEMetricSpace α] {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) {x : α} (x_in_E : x ∈ E) : (thickenedIndicator δ_pos E) x = 1

theorem thickenedIndicator_zero {α : Type u_1} [PseudoEMetricSpace α] {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) {x : α} (x_out : x ∉ Metric.thickening δ E) : (thickenedIndicator δ_pos E) x = 0

theorem indicator_le_thickenedIndicator {α : Type u_1} [PseudoEMetricSpace α] {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) : (E.indicator fun (x : α) => 1) ≤ ⇑(thickenedIndicator δ_pos E)

theorem thickenedIndicator_mono {α : Type u_1} [PseudoEMetricSpace α] {δ₁ δ₂ : ℝ} (δ₁_pos : 0 < δ₁) (δ₂_pos : 0 < δ₂) (hle : δ₁ ≤ δ₂) (E : Set α) : ⇑(thickenedIndicator δ₁_pos E) ≤ ⇑(thickenedIndicator δ₂_pos E)

theorem thickenedIndicator_subset {α : Type u_1} [PseudoEMetricSpace α] {δ : ℝ} (δ_pos : 0 < δ) {E₁ E₂ : Set α} (subset : E₁ ⊆ E₂) : ⇑(thickenedIndicator δ_pos E₁) ≤ ⇑(thickenedIndicator δ_pos E₂)

theorem thickenedIndicator_tendsto_indicator_closure {α : Type u_1} [PseudoEMetricSpace α] {δseq : ℕ → ℝ} (δseq_pos : ∀ (n : ℕ), 0 < δseq n) (δseq_lim : Filter.Tendsto δseq Filter.atTop (nhds 0)) (E : Set α) : Filter.Tendsto (fun (n : ℕ) => ⇑(thickenedIndicator ⋯ E)) Filter.atTop (nhds ((closure E).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 mulIndicator_thickening_eventually_eq_mulIndicator_closure {α : Type u_1} [PseudoEMetricSpace α] {β : Type u_2} [One β] (f : α → β) (E : Set α) (x : α) : ∀ᶠ (δ : ℝ) in nhdsWithin 0 (Set.Ioi 0), (Metric.thickening δ E).mulIndicator f x = (closure E).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_thickening_eventually_eq_indicator_closure {α : Type u_1} [PseudoEMetricSpace α] {β : Type u_2} [Zero β] (f : α → β) (E : Set α) (x : α) : ∀ᶠ (δ : ℝ) in nhdsWithin 0 (Set.Ioi 0), (Metric.thickening δ E).indicator f x = (closure E).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_cthickening_eventually_eq_mulIndicator_closure {α : Type u_1} [PseudoEMetricSpace α] {β : Type u_2} [One β] (f : α → β) (E : Set α) (x : α) : ∀ᶠ (δ : ℝ) in nhds 0, (Metric.cthickening δ E).mulIndicator f x = (closure E).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 indicator_cthickening_eventually_eq_indicator_closure {α : Type u_1} [PseudoEMetricSpace α] {β : Type u_2} [Zero β] (f : α → β) (E : Set α) (x : α) : ∀ᶠ (δ : ℝ) in nhds 0, (Metric.cthickening δ E).indicator f x = (closure E).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 tendsto_mulIndicator_thickening_mulIndicator_closure {α : Type u_1} [PseudoEMetricSpace α] {β : Type u_2} [One β] [TopologicalSpace β] (f : α → β) (E : Set α) : Filter.Tendsto (fun (δ : ℝ) => (Metric.thickening δ E).mulIndicator f) (nhdsWithin 0 (Set.Ioi 0)) (nhds ((closure E).mulIndicator f))

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_thickening_indicator_closure {α : Type u_1} [PseudoEMetricSpace α] {β : Type u_2} [Zero β] [TopologicalSpace β] (f : α → β) (E : Set α) : Filter.Tendsto (fun (δ : ℝ) => (Metric.thickening δ E).indicator f) (nhdsWithin 0 (Set.Ioi 0)) (nhds ((closure E).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_cthickening_mulIndicator_closure {α : Type u_1} [PseudoEMetricSpace α] {β : Type u_2} [One β] [TopologicalSpace β] (f : α → β) (E : Set α) : Filter.Tendsto (fun (δ : ℝ) => (Metric.cthickening δ E).mulIndicator f) (nhds 0) (nhds ((closure E).mulIndicator f))

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

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

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