feat (Mathlib.Topology.MetricSpace.ThickenedIndicator): Add convergen…

…ce of plain old indicators. (#6047)

Add lemmas `tendsto_indicator_thickening_indicator_closure` and `tendsto_indicator_cthickening_indicator_closure`.

Co-authored-by: @sgouezel and @urkud



Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>

Mathlib/Topology/MetricSpace/HausdorffDistance.lean

@@ -905,6 +905,15 @@ theorem mem_thickening_iff_infEdist_lt : x ∈ thickening δ s ↔ infEdist x s
   Iff.rfl
 #align metric.mem_thickening_iff_inf_edist_lt Metric.mem_thickening_iff_infEdist_lt
 
+/-- An exterior point of a subset `E` (i.e., a point outside the closure of `E`) is not in the
+(open) `δ`-thickening of `E` for small enough positive `δ`. -/
+lemma eventually_not_mem_thickening_of_infEdist_pos {E : Set α} {x : α} (h : x ∉ closure E) :
+    ∀ᶠ δ in 𝓝 (0 : ℝ), x ∉ Metric.thickening δ E := by
+  obtain ⟨ε, ⟨ε_pos, ε_lt⟩⟩ := exists_real_pos_lt_infEdist_of_not_mem_closure h
+  filter_upwards [eventually_lt_nhds ε_pos] with δ hδ
+  simp only [thickening, mem_setOf_eq, not_lt]
+  exact (ENNReal.ofReal_le_ofReal hδ.le).trans ε_lt.le
+
 /-- The (open) thickening equals the preimage of an open interval under `EMetric.infEdist`. -/
 theorem thickening_eq_preimage_infEdist (δ : ℝ) (E : Set α) :
     thickening δ E = (infEdist · E) ⁻¹' Iio (ENNReal.ofReal δ) :=
@@ -1026,6 +1035,15 @@ theorem mem_cthickening_iff : x ∈ cthickening δ s ↔ infEdist x s ≤ ENNRea
   Iff.rfl
 #align metric.mem_cthickening_iff Metric.mem_cthickening_iff
 
+/-- An exterior point of a subset `E` (i.e., a point outside the closure of `E`) is not in the
+closed `δ`-thickening of `E` for small enough positive `δ`. -/
+lemma eventually_not_mem_cthickening_of_infEdist_pos {E : Set α} {x : α} (h : x ∉ closure E) :
+    ∀ᶠ δ in 𝓝 (0 : ℝ), x ∉ Metric.cthickening δ E := by
+  obtain ⟨ε, ⟨ε_pos, ε_lt⟩⟩ := exists_real_pos_lt_infEdist_of_not_mem_closure h
+  filter_upwards [eventually_lt_nhds ε_pos] with δ hδ
+  simp only [cthickening, mem_setOf_eq, not_le]
+  exact ((ofReal_lt_ofReal_iff ε_pos).mpr hδ).trans ε_lt
+
 theorem mem_cthickening_of_edist_le (x y : α) (δ : ℝ) (E : Set α) (h : y ∈ E)
     (h' : edist x y ≤ ENNReal.ofReal δ) : x ∈ cthickening δ E :=
   (infEdist_le_edist_of_mem h).trans h'

Mathlib/Topology/MetricSpace/ThickenedIndicator.lean

@@ -6,6 +6,7 @@ Authors: Kalle Kytölä
 import Mathlib.Data.Real.ENNReal
 import Mathlib.Topology.ContinuousFunction.Bounded
 import Mathlib.Topology.MetricSpace.HausdorffDistance
+import Mathlib.Order.Filter.IndicatorFunction
 
 #align_import topology.metric_space.thickened_indicator from "leanprover-community/mathlib"@"f2ce6086713c78a7f880485f7917ea547a215982"
 
@@ -248,3 +249,64 @@ theorem thickenedIndicator_tendsto_indicator_closure {δseq : ℕ → ℝ} (δse
 #align thickened_indicator_tendsto_indicator_closure thickenedIndicator_tendsto_indicator_closure
 
 end thickenedIndicator
+
+section indicator
+
+variable {α : Type _} [PseudoEMetricSpace α] {β : Type _} [One β]
+
+/-- Pointwise, the multiplicative indicators of δ-thickenings of a set eventually coincide
+with the multiplicative indicator of the set as δ>0 tends to zero. -/
+@[to_additive "Pointwise, the indicators of δ-thickenings of a set eventually coincide
+with the indicator of the set as δ>0 tends to zero."]
+lemma mulIndicator_thickening_eventually_eq_mulIndicator_closure (f : α → β) (E : Set α) (x : α) :
+    ∀ᶠ δ in 𝓝[>] (0 : ℝ),
+      (Metric.thickening δ E).mulIndicator f x = (closure E).mulIndicator f x := by
+  by_cases x_mem_closure : x ∈ closure E
+  · filter_upwards [self_mem_nhdsWithin] with δ δ_pos
+    simp only [closure_subset_thickening δ_pos E x_mem_closure, mulIndicator_of_mem, x_mem_closure]
+  · have obs := eventually_not_mem_thickening_of_infEdist_pos x_mem_closure
+    filter_upwards [mem_nhdsWithin_of_mem_nhds obs, self_mem_nhdsWithin]
+      with δ x_notin_thE _
+    simp only [x_notin_thE, not_false_eq_true, mulIndicator_of_not_mem, x_mem_closure]
+
+/-- Pointwise, the multiplicative indicators of closed δ-thickenings of a set eventually coincide
+with the multiplicative indicator of the set as δ tends to zero. -/
+@[to_additive "Pointwise, the indicators of closed δ-thickenings of a set eventually coincide
+with the indicator of the set as δ tends to zero."]
+lemma mulIndicator_cthickening_eventually_eq_mulIndicator_closure (f : α → β) (E : Set α) (x : α) :
+    ∀ᶠ δ in 𝓝 (0 : ℝ),
+      (Metric.cthickening δ E).mulIndicator f x = (closure E).mulIndicator f x := by
+  by_cases x_mem_closure : x ∈ closure E
+  · filter_upwards [univ_mem] with δ _
+    have obs : x ∈ cthickening δ E := closure_subset_cthickening δ E x_mem_closure
+    rw [mulIndicator_of_mem obs f, mulIndicator_of_mem x_mem_closure f]
+  · filter_upwards [eventually_not_mem_cthickening_of_infEdist_pos x_mem_closure] with δ hδ
+    simp only [hδ, not_false_eq_true, mulIndicator_of_not_mem, x_mem_closure]
+
+variable [TopologicalSpace β]
+
+/-- The multiplicative indicators of δ-thickenings of a set tend pointwise to the multiplicative
+indicator of the set, as δ>0 tends to zero. -/
+@[to_additive "The indicators of δ-thickenings of a set tend pointwise to the indicator of the
+set, as δ>0 tends to zero."]
+lemma tendsto_mulIndicator_thickening_mulIndicator_closure (f : α → β) (E : Set α) :
+    Tendsto (fun δ ↦ (Metric.thickening δ E).mulIndicator f) (𝓝[>] 0)
+      (𝓝 ((closure E).mulIndicator f)) := by
+  rw [tendsto_pi_nhds]
+  intro x
+  rw [tendsto_congr' (mulIndicator_thickening_eventually_eq_mulIndicator_closure f E x)]
+  apply tendsto_const_nhds
+
+/-- The multiplicative indicators of closed δ-thickenings of a set tend pointwise to the
+multiplicative indicator of the set, as δ tends to zero. -/
+@[to_additive "The indicators of closed δ-thickenings of a set tend pointwise to the indicator
+of the set, as δ tends to zero."]
+lemma tendsto_mulIndicator_cthickening_mulIndicator_closure (f : α → β) (E : Set α) :
+    Tendsto (fun δ ↦ (Metric.cthickening δ E).mulIndicator f) (𝓝 0)
+      (𝓝 ((closure E).mulIndicator f)) := by
+  rw [tendsto_pi_nhds]
+  intro x
+  rw [tendsto_congr' (mulIndicator_cthickening_eventually_eq_mulIndicator_closure f E x)]
+  apply tendsto_const_nhds
+
+end indicator