Documentation

Mathlib.Topology.MetricSpace.ThickenedIndicator

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 #

Main results #

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
Instances For
    theorem continuous_thickenedIndicatorAux {α : Type u_1} [PseudoEMetricSpace α] {δ : } (δ_pos : 0 < δ) (E : Set α) :
    theorem thickenedIndicatorAux_le_one {α : Type u_1} [PseudoEMetricSpace α] (δ : ) (E : Set α) (x : α) :
    theorem thickenedIndicatorAux_lt_top {α : Type u_1} [PseudoEMetricSpace α] {δ : } {E : Set α} {x : α} :
    theorem thickenedIndicatorAux_one {α : Type u_1} [PseudoEMetricSpace α] (δ : ) (E : Set α) {x : α} (x_in_E : x E) :
    theorem thickenedIndicatorAux_one_of_mem_closure {α : Type u_1} [PseudoEMetricSpace α] (δ : ) (E : Set α) {x : α} (x_mem : x closure E) :
    theorem thickenedIndicatorAux_zero {α : Type u_1} [PseudoEMetricSpace α] {δ : } (δ_pos : 0 < δ) (E : Set α) {x : α} (x_out : xMetric.thickening δ E) :
    theorem thickenedIndicatorAux_mono {α : Type u_1} [PseudoEMetricSpace α] {δ₁ : } {δ₂ : } (hle : δ₁ δ₂) (E : Set α) :
    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₁ : Set α} {E₂ : Set α} (subset : E₁ 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 α) :

    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
    Instances For
      @[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 α) :
      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 : xMetric.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₁ : Set α} {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.