[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ Continuous (thickenedIndicatorAux δ E)
[PROOFSTEP]
unfold thickenedIndicatorAux
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ Continuous fun x => 1 - infEdist x E / ENNReal.ofReal δ
[PROOFSTEP]
let f := fun x : α => (⟨1, infEdist x E / ENNReal.ofReal δ⟩ : ℝ≥0 × ℝ≥0∞)
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
f : α → ℝ≥0 × ℝ≥0∞ := fun x => (1, infEdist x E / ENNReal.ofReal δ)
⊢ Continuous fun x => 1 - infEdist x E / ENNReal.ofReal δ
[PROOFSTEP]
let sub := fun p : ℝ≥0 × ℝ≥0∞ => (p.1 : ℝ≥0∞) - p.2
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
f : α → ℝ≥0 × ℝ≥0∞ := fun x => (1, infEdist x E / ENNReal.ofReal δ)
sub : ℝ≥0 × ℝ≥0∞ → ℝ≥0∞ := fun p => ↑p.fst - p.snd
⊢ Continuous fun x => 1 - infEdist x E / ENNReal.ofReal δ
[PROOFSTEP]
rw [show (fun x : α => (1 : ℝ≥0∞) - infEdist x E / ENNReal.ofReal δ) = sub ∘ f by rfl]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
f : α → ℝ≥0 × ℝ≥0∞ := fun x => (1, infEdist x E / ENNReal.ofReal δ)
sub : ℝ≥0 × ℝ≥0∞ → ℝ≥0∞ := fun p => ↑p.fst - p.snd
⊢ (fun x => 1 - infEdist x E / ENNReal.ofReal δ) = sub ∘ f
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
f : α → ℝ≥0 × ℝ≥0∞ := fun x => (1, infEdist x E / ENNReal.ofReal δ)
sub : ℝ≥0 × ℝ≥0∞ → ℝ≥0∞ := fun p => ↑p.fst - p.snd
⊢ Continuous (sub ∘ f)
[PROOFSTEP]
apply (@ENNReal.continuous_nnreal_sub 1).comp
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
f : α → ℝ≥0 × ℝ≥0∞ := fun x => (1, infEdist x E / ENNReal.ofReal δ)
sub : ℝ≥0 × ℝ≥0∞ → ℝ≥0∞ := fun p => ↑p.fst - p.snd
⊢ Continuous fun x => (f x).snd
[PROOFSTEP]
apply (ENNReal.continuous_div_const (ENNReal.ofReal δ) _).comp continuous_infEdist
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
f : α → ℝ≥0 × ℝ≥0∞ := fun x => (1, infEdist x E / ENNReal.ofReal δ)
sub : ℝ≥0 × ℝ≥0∞ → ℝ≥0∞ := fun p => ↑p.fst - p.snd
⊢ ENNReal.ofReal δ ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
f : α → ℝ≥0 × ℝ≥0∞ := fun x => (1, infEdist x E / ENNReal.ofReal δ)
sub : ℝ≥0 × ℝ≥0∞ → ℝ≥0∞ := fun p => ↑p.fst - p.snd
⊢ 0 < δ
[PROOFSTEP]
exact δ_pos
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
⊢ thickenedIndicatorAux δ E x ≤ 1
[PROOFSTEP]
apply @tsub_le_self _ _ _ _ (1 : ℝ≥0∞)
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ thickenedIndicatorAux δ (closure E) = thickenedIndicatorAux δ E
[PROOFSTEP]
simp_rw [thickenedIndicatorAux, infEdist_closure]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_in_E : x ∈ E
⊢ thickenedIndicatorAux δ E x = 1
[PROOFSTEP]
simp [thickenedIndicatorAux, infEdist_zero_of_mem x_in_E, tsub_zero]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_mem : x ∈ closure E
⊢ thickenedIndicatorAux δ E x = 1
[PROOFSTEP]
rw [← thickenedIndicatorAux_closure_eq, thickenedIndicatorAux_one δ (closure E) x_mem]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ¬x ∈ thickening δ E
⊢ thickenedIndicatorAux δ E x = 0
[PROOFSTEP]
rw [thickening, mem_setOf_eq, not_lt] at x_out 
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
⊢ thickenedIndicatorAux δ E x = 0
[PROOFSTEP]
unfold thickenedIndicatorAux
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
⊢ 1 - infEdist x E / ENNReal.ofReal δ = 0
[PROOFSTEP]
apply le_antisymm _ bot_le
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
⊢ 1 - infEdist x E / ENNReal.ofReal δ ≤ ⊥
[PROOFSTEP]
have key := tsub_le_tsub (@rfl _ (1 : ℝ≥0∞)).le (ENNReal.div_le_div x_out (@rfl _ (ENNReal.ofReal δ : ℝ≥0∞)).le)
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
key : 1 - infEdist x E / ENNReal.ofReal δ ≤ 1 - ENNReal.ofReal δ / ENNReal.ofReal δ
⊢ 1 - infEdist x E / ENNReal.ofReal δ ≤ ⊥
[PROOFSTEP]
rw [ENNReal.div_self (ne_of_gt (ENNReal.ofReal_pos.mpr δ_pos)) ofReal_ne_top] at key 
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
key : 1 - infEdist x E / ENNReal.ofReal δ ≤ 1 - 1
⊢ 1 - infEdist x E / ENNReal.ofReal δ ≤ ⊥
[PROOFSTEP]
simpa using key
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ (indicator E fun x => 1) ≤ thickenedIndicatorAux δ E
[PROOFSTEP]
intro a
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
a : α
⊢ indicator E (fun x => 1) a ≤ thickenedIndicatorAux δ E a
[PROOFSTEP]
by_cases a ∈ E
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
a : α
⊢ indicator E (fun x => 1) a ≤ thickenedIndicatorAux δ E a
[PROOFSTEP]
by_cases a ∈ E
[GOAL]
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
a : α
h : a ∈ E
⊢ indicator E (fun x => 1) a ≤ thickenedIndicatorAux δ E a
[PROOFSTEP]
simp only [h, indicator_of_mem, thickenedIndicatorAux_one δ E h, le_refl]
[GOAL]
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
a : α
h : ¬a ∈ E
⊢ indicator E (fun x => 1) a ≤ thickenedIndicatorAux δ E a
[PROOFSTEP]
simp only [h, indicator_of_not_mem, not_false_iff, zero_le]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
⊢ Tendsto (fun n => thickenedIndicatorAux (δseq n) E) atTop (𝓝 (indicator (closure E) fun x => 1))
[PROOFSTEP]
rw [tendsto_pi_nhds]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
⊢ ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
[PROOFSTEP]
by_cases x_mem_closure : x ∈ closure E
[GOAL]
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∈ closure E
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
[PROOFSTEP]
simp_rw [thickenedIndicatorAux_one_of_mem_closure _ E x_mem_closure]
[GOAL]
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∈ closure E
⊢ Tendsto (fun i => 1) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
[PROOFSTEP]
rw [show (indicator (closure E) fun _ => (1 : ℝ≥0∞)) x = 1 by simp only [x_mem_closure, indicator_of_mem]]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∈ closure E
⊢ indicator (closure E) (fun x => 1) x = 1
[PROOFSTEP]
simp only [x_mem_closure, indicator_of_mem]
[GOAL]
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∈ closure E
⊢ Tendsto (fun i => 1) atTop (𝓝 1)
[PROOFSTEP]
exact tendsto_const_nhds
[GOAL]
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
[PROOFSTEP]
rw [show (closure E).indicator (fun _ => (1 : ℝ≥0∞)) x = 0 by
    simp only [x_mem_closure, indicator_of_not_mem, not_false_iff]]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
⊢ indicator (closure E) (fun x => 1) x = 0
[PROOFSTEP]
simp only [x_mem_closure, indicator_of_not_mem, not_false_iff]
[GOAL]
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
[PROOFSTEP]
rcases exists_real_pos_lt_infEdist_of_not_mem_closure x_mem_closure with ⟨ε, ⟨ε_pos, ε_lt⟩⟩
[GOAL]
case neg.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
[PROOFSTEP]
rw [Metric.tendsto_nhds] at δseq_lim 
[GOAL]
case neg.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : ℕ) in atTop, dist (δseq x) 0 < ε
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
[PROOFSTEP]
specialize δseq_lim ε ε_pos
[GOAL]
case neg.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
δseq_lim : ∀ᶠ (x : ℕ) in atTop, dist (δseq x) 0 < ε
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
[PROOFSTEP]
simp only [dist_zero_right, Real.norm_eq_abs, eventually_atTop, ge_iff_le] at δseq_lim 
[GOAL]
case neg.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
δseq_lim : ∃ a, ∀ (b : ℕ), a ≤ b → |δseq b| < ε
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
[PROOFSTEP]
rcases δseq_lim with ⟨N, hN⟩
[GOAL]
case neg.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → |δseq b| < ε
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
[PROOFSTEP]
apply @tendsto_atTop_of_eventually_const _ _ _ _ _ _ _ N
[GOAL]
case neg.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → |δseq b| < ε
⊢ ∀ (i : ℕ), i ≥ N → thickenedIndicatorAux (δseq i) E x = 0
[PROOFSTEP]
intro n n_large
[GOAL]
case neg.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → |δseq b| < ε
n : ℕ
n_large : n ≥ N
⊢ thickenedIndicatorAux (δseq n) E x = 0
[PROOFSTEP]
have key : x ∉ thickening ε E := by simpa only [thickening, mem_setOf_eq, not_lt] using ε_lt.le
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → |δseq b| < ε
n : ℕ
n_large : n ≥ N
⊢ ¬x ∈ thickening ε E
[PROOFSTEP]
simpa only [thickening, mem_setOf_eq, not_lt] using ε_lt.le
[GOAL]
case neg.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → |δseq b| < ε
n : ℕ
n_large : n ≥ N
key : ¬x ∈ thickening ε E
⊢ thickenedIndicatorAux (δseq n) E x = 0
[PROOFSTEP]
refine' le_antisymm _ bot_le
[GOAL]
case neg.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → |δseq b| < ε
n : ℕ
n_large : n ≥ N
key : ¬x ∈ thickening ε E
⊢ thickenedIndicatorAux (δseq n) E x ≤ 0
[PROOFSTEP]
apply (thickenedIndicatorAux_mono (lt_of_abs_lt (hN n n_large)).le E x).trans
[GOAL]
case neg.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → |δseq b| < ε
n : ℕ
n_large : n ≥ N
key : ¬x ∈ thickening ε E
⊢ thickenedIndicatorAux ε E x ≤ 0
[PROOFSTEP]
exact (thickenedIndicatorAux_zero ε_pos E key).le
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ Continuous fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)
[PROOFSTEP]
apply ContinuousOn.comp_continuous continuousOn_toNNReal (continuous_thickenedIndicatorAux δ_pos E)
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ ∀ (x : α), thickenedIndicatorAux δ E x ∈ {a | a ≠ ⊤}
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
⊢ thickenedIndicatorAux δ E x ∈ {a | a ≠ ⊤}
[PROOFSTEP]
exact (lt_of_le_of_lt (@thickenedIndicatorAux_le_one _ _ δ E x) one_lt_top).ne
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ ∃ C,
    ∀ (x y : α),
      dist (ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) x)
          (ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) y) ≤
        C
[PROOFSTEP]
use 2
[GOAL]
case h
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ ∀ (x y : α),
    dist (ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) x)
        (ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) y) ≤
      2
[PROOFSTEP]
intro x y
[GOAL]
case h
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
⊢ dist (ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) x)
      (ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) y) ≤
    2
[PROOFSTEP]
rw [NNReal.dist_eq]
[GOAL]
case h
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
⊢ |↑(ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) x) -
        ↑(ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) y)| ≤
    2
[PROOFSTEP]
apply (abs_sub _ _).trans
[GOAL]
case h
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
⊢ |↑(ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) x)| +
      |↑(ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) y)| ≤
    2
[PROOFSTEP]
rw [NNReal.abs_eq, NNReal.abs_eq, ← one_add_one_eq_two]
[GOAL]
case h
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
⊢ ↑(ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) x) +
      ↑(ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) y) ≤
    1 + 1
[PROOFSTEP]
have key := @thickenedIndicatorAux_le_one _ _ δ E
[GOAL]
case h
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
key : ∀ (x : α), thickenedIndicatorAux δ E x ≤ 1
⊢ ↑(ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) x) +
      ↑(ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) y) ≤
    1 + 1
[PROOFSTEP]
apply add_le_add
[GOAL]
case h.h₁
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
key : ∀ (x : α), thickenedIndicatorAux δ E x ≤ 1
⊢ ↑(ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) x) ≤ 1
[PROOFSTEP]
norm_cast
[GOAL]
case h.h₁
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
key : ∀ (x : α), thickenedIndicatorAux δ E x ≤ 1
⊢ ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) x ≤ 1
[PROOFSTEP]
refine' (toNNReal_le_toNNReal (lt_of_le_of_lt (key _) one_lt_top).ne one_ne_top).mpr (key _)
[GOAL]
case h.h₂
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
key : ∀ (x : α), thickenedIndicatorAux δ E x ≤ 1
⊢ ↑(ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) y) ≤ 1
[PROOFSTEP]
norm_cast
[GOAL]
case h.h₂
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
key : ∀ (x : α), thickenedIndicatorAux δ E x ≤ 1
⊢ ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) y ≤ 1
[PROOFSTEP]
refine' (toNNReal_le_toNNReal (lt_of_le_of_lt (key _) one_lt_top).ne one_ne_top).mpr (key _)
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
⊢ ↑(thickenedIndicator δ_pos E) x ≤ 1
[PROOFSTEP]
rw [thickenedIndicator.coeFn_eq_comp]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
⊢ (ENNReal.toNNReal ∘ thickenedIndicatorAux δ E) x ≤ 1
[PROOFSTEP]
simpa using (toNNReal_le_toNNReal thickenedIndicatorAux_lt_top.ne one_ne_top).mpr (thickenedIndicatorAux_le_one δ E x)
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_mem : x ∈ closure E
⊢ ↑(thickenedIndicator δ_pos E) x = 1
[PROOFSTEP]
rw [thickenedIndicator_apply, thickenedIndicatorAux_one_of_mem_closure δ E x_mem, one_toNNReal]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ¬x ∈ thickening δ E
⊢ ↑(thickenedIndicator δ_pos E) x = 0
[PROOFSTEP]
rw [thickenedIndicator_apply, thickenedIndicatorAux_zero δ_pos E x_out, zero_toNNReal]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ (indicator E fun x => 1) ≤ ↑(thickenedIndicator δ_pos E)
[PROOFSTEP]
intro a
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
⊢ indicator E (fun x => 1) a ≤ ↑(thickenedIndicator δ_pos E) a
[PROOFSTEP]
by_cases a ∈ E
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
⊢ indicator E (fun x => 1) a ≤ ↑(thickenedIndicator δ_pos E) a
[PROOFSTEP]
by_cases a ∈ E
[GOAL]
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
h : a ∈ E
⊢ indicator E (fun x => 1) a ≤ ↑(thickenedIndicator δ_pos E) a
[PROOFSTEP]
simp only [h, indicator_of_mem, thickenedIndicator_one δ_pos E h, le_refl]
[GOAL]
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
h : ¬a ∈ E
⊢ indicator E (fun x => 1) a ≤ ↑(thickenedIndicator δ_pos E) a
[PROOFSTEP]
simp only [h, indicator_of_not_mem, not_false_iff, zero_le]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ₁ δ₂ : ℝ
δ₁_pos : 0 < δ₁
δ₂_pos : 0 < δ₂
hle : δ₁ ≤ δ₂
E : Set α
⊢ ↑(thickenedIndicator δ₁_pos E) ≤ ↑(thickenedIndicator δ₂_pos E)
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ₁ δ₂ : ℝ
δ₁_pos : 0 < δ₁
δ₂_pos : 0 < δ₂
hle : δ₁ ≤ δ₂
E : Set α
x : α
⊢ ↑(thickenedIndicator δ₁_pos E) x ≤ ↑(thickenedIndicator δ₂_pos E) x
[PROOFSTEP]
apply (toNNReal_le_toNNReal thickenedIndicatorAux_lt_top.ne thickenedIndicatorAux_lt_top.ne).mpr
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ₁ δ₂ : ℝ
δ₁_pos : 0 < δ₁
δ₂_pos : 0 < δ₂
hle : δ₁ ≤ δ₂
E : Set α
x : α
⊢ thickenedIndicatorAux δ₁ E x ≤ thickenedIndicatorAux δ₂ E x
[PROOFSTEP]
apply thickenedIndicatorAux_mono hle
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
⊢ Tendsto (fun n => ↑(thickenedIndicator (_ : 0 < δseq n) E)) atTop (𝓝 (indicator (closure E) fun x => 1))
[PROOFSTEP]
have key := thickenedIndicatorAux_tendsto_indicator_closure δseq_lim E
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : Tendsto (fun n => thickenedIndicatorAux (δseq n) E) atTop (𝓝 (indicator (closure E) fun x => 1))
⊢ Tendsto (fun n => ↑(thickenedIndicator (_ : 0 < δseq n) E)) atTop (𝓝 (indicator (closure E) fun x => 1))
[PROOFSTEP]
rw [tendsto_pi_nhds] at *
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
⊢ ∀ (x : α),
    Tendsto (fun i => ↑(thickenedIndicator (_ : 0 < δseq i) E) x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
x : α
⊢ Tendsto (fun i => ↑(thickenedIndicator (_ : 0 < δseq i) E) x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
[PROOFSTEP]
rw [show indicator (closure E) (fun _ => (1 : ℝ≥0)) x = (indicator (closure E) (fun _ => (1 : ℝ≥0∞)) x).toNNReal by
    refine' (congr_fun (comp_indicator_const 1 ENNReal.toNNReal zero_toNNReal) x).symm]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
x : α
⊢ indicator (closure E) (fun x => 1) x = ENNReal.toNNReal (indicator (closure E) (fun x => 1) x)
[PROOFSTEP]
refine' (congr_fun (comp_indicator_const 1 ENNReal.toNNReal zero_toNNReal) x).symm
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
x : α
⊢ Tendsto (fun i => ↑(thickenedIndicator (_ : 0 < δseq i) E) x) atTop
    (𝓝 (ENNReal.toNNReal (indicator (closure E) (fun x => 1) x)))
[PROOFSTEP]
refine' Tendsto.comp (tendsto_toNNReal _) (key x)
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
x : α
⊢ indicator (closure E) (fun x => 1) x ≠ ⊤
[PROOFSTEP]
by_cases x_mem : x ∈ closure E
[GOAL]
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
x : α
x_mem : x ∈ closure E
⊢ indicator (closure E) (fun x => 1) x ≠ ⊤
[PROOFSTEP]
simp [x_mem]
[GOAL]
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
x : α
x_mem : ¬x ∈ closure E
⊢ indicator (closure E) (fun x => 1) x ≠ ⊤
[PROOFSTEP]
simp [x_mem]
[GOAL]
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
⊢ ∀ᶠ (δ : ℝ) in 𝓝[Ioi 0] 0, mulIndicator (thickening δ E) f x = mulIndicator (closure E) f x
[PROOFSTEP]
by_cases x_mem_closure : x ∈ closure E
[GOAL]
case pos
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∈ closure E
⊢ ∀ᶠ (δ : ℝ) in 𝓝[Ioi 0] 0, mulIndicator (thickening δ E) f x = mulIndicator (closure E) f x
[PROOFSTEP]
filter_upwards [self_mem_nhdsWithin] with δ δ_pos
[GOAL]
case h
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∈ closure E
δ : ℝ
δ_pos : δ ∈ Ioi 0
⊢ mulIndicator (thickening δ E) f x = mulIndicator (closure E) f x
[PROOFSTEP]
simp only [closure_subset_thickening δ_pos E x_mem_closure, mulIndicator_of_mem, x_mem_closure]
[GOAL]
case neg
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
⊢ ∀ᶠ (δ : ℝ) in 𝓝[Ioi 0] 0, mulIndicator (thickening δ E) f x = mulIndicator (closure E) f x
[PROOFSTEP]
have obs := eventually_not_mem_thickening_of_infEdist_pos x_mem_closure
[GOAL]
case neg
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
obs : ∀ᶠ (δ : ℝ) in 𝓝 0, ¬x ∈ thickening δ E
⊢ ∀ᶠ (δ : ℝ) in 𝓝[Ioi 0] 0, mulIndicator (thickening δ E) f x = mulIndicator (closure E) f x
[PROOFSTEP]
filter_upwards [mem_nhdsWithin_of_mem_nhds obs, self_mem_nhdsWithin] with δ x_notin_thE _
[GOAL]
case h
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
obs : ∀ᶠ (δ : ℝ) in 𝓝 0, ¬x ∈ thickening δ E
δ : ℝ
x_notin_thE : ¬x ∈ thickening δ E
a✝ : δ ∈ Ioi 0
⊢ mulIndicator (thickening δ E) f x = mulIndicator (closure E) f x
[PROOFSTEP]
simp only [x_notin_thE, not_false_eq_true, mulIndicator_of_not_mem, x_mem_closure]
[GOAL]
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, mulIndicator (cthickening δ E) f x = mulIndicator (closure E) f x
[PROOFSTEP]
by_cases x_mem_closure : x ∈ closure E
[GOAL]
case pos
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∈ closure E
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, mulIndicator (cthickening δ E) f x = mulIndicator (closure E) f x
[PROOFSTEP]
filter_upwards [univ_mem] with δ _
[GOAL]
case h
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∈ closure E
δ : ℝ
a✝ : δ ∈ univ
⊢ mulIndicator (cthickening δ E) f x = mulIndicator (closure E) f x
[PROOFSTEP]
have obs : x ∈ cthickening δ E := closure_subset_cthickening δ E x_mem_closure
[GOAL]
case h
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∈ closure E
δ : ℝ
a✝ : δ ∈ univ
obs : x ∈ cthickening δ E
⊢ mulIndicator (cthickening δ E) f x = mulIndicator (closure E) f x
[PROOFSTEP]
rw [mulIndicator_of_mem obs f, mulIndicator_of_mem x_mem_closure f]
[GOAL]
case neg
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, mulIndicator (cthickening δ E) f x = mulIndicator (closure E) f x
[PROOFSTEP]
filter_upwards [eventually_not_mem_cthickening_of_infEdist_pos x_mem_closure] with δ hδ
[GOAL]
case h
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
δ : ℝ
hδ : ¬x ∈ cthickening δ E
⊢ mulIndicator (cthickening δ E) f x = mulIndicator (closure E) f x
[PROOFSTEP]
simp only [hδ, not_false_eq_true, mulIndicator_of_not_mem, x_mem_closure]
[GOAL]
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
⊢ Tendsto (fun δ => mulIndicator (thickening δ E) f) (𝓝[Ioi 0] 0) (𝓝 (mulIndicator (closure E) f))
[PROOFSTEP]
rw [tendsto_pi_nhds]
[GOAL]
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
⊢ ∀ (x : α), Tendsto (fun i => mulIndicator (thickening i E) f x) (𝓝[Ioi 0] 0) (𝓝 (mulIndicator (closure E) f x))
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
x : α
⊢ Tendsto (fun i => mulIndicator (thickening i E) f x) (𝓝[Ioi 0] 0) (𝓝 (mulIndicator (closure E) f x))
[PROOFSTEP]
rw [tendsto_congr' (mulIndicator_thickening_eventually_eq_mulIndicator_closure f E x)]
[GOAL]
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
x : α
⊢ Tendsto (fun x_1 => mulIndicator (closure E) f x) (𝓝[Ioi 0] 0) (𝓝 (mulIndicator (closure E) f x))
[PROOFSTEP]
apply tendsto_const_nhds
[GOAL]
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
⊢ Tendsto (fun δ => mulIndicator (cthickening δ E) f) (𝓝 0) (𝓝 (mulIndicator (closure E) f))
[PROOFSTEP]
rw [tendsto_pi_nhds]
[GOAL]
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
⊢ ∀ (x : α), Tendsto (fun i => mulIndicator (cthickening i E) f x) (𝓝 0) (𝓝 (mulIndicator (closure E) f x))
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
x : α
⊢ Tendsto (fun i => mulIndicator (cthickening i E) f x) (𝓝 0) (𝓝 (mulIndicator (closure E) f x))
[PROOFSTEP]
rw [tendsto_congr' (mulIndicator_cthickening_eventually_eq_mulIndicator_closure f E x)]
[GOAL]
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
x : α
⊢ Tendsto (fun x_1 => mulIndicator (closure E) f x) (𝓝 0) (𝓝 (mulIndicator (closure E) f x))
[PROOFSTEP]
apply tendsto_const_nhds
