feat(topology,analysis): any function is continuous/differentiable on…

… a subsingleton (#12293)

Also add supporting lemmas about `is_o`/`is_O` and the `pure` filter
and drop an unneeded assumption in `asymptotics.is_o_const_const_iff`.

src/analysis/asymptotics/asymptotics.lean

@@ -386,6 +386,8 @@ variables (c f g)
 
 end bot
 
+@[simp] theorem is_O_with_pure {x} : is_O_with c f g (pure x) ↔ ∥f x∥ ≤ c * ∥g x∥ := is_O_with_iff
+
 theorem is_O_with.join (h : is_O_with c f g l) (h' : is_O_with c f g l') :
   is_O_with c f g (l ⊔ l') :=
 is_O_with.of_bound $ mem_sup.2 ⟨h.bound, h'.bound⟩
@@ -743,6 +745,18 @@ theorem is_O_const_const (c : E) {c' : F'} (hc' : c' ≠ 0) (l : filter α) :
   is_O (λ x : α, c) (λ x, c') l :=
 (is_O_with_const_const c hc' l).is_O
 
+@[simp] theorem is_O_const_const_iff {c : E'} {c' : F'} (l : filter α) [l.ne_bot] :
+  is_O (λ x : α, c) (λ x, c') l ↔ (c' = 0 → c = 0) :=
+begin
+  rcases eq_or_ne c' 0 with rfl|hc',
+  { simp },
+  { simp [hc', is_O_const_const _ hc'] }
+end
+
+@[simp] lemma is_O_pure {x} : is_O f' g' (pure x) ↔ (g' x = 0 → f' x = 0) :=
+calc is_O f' g' (pure x) ↔ is_O (λ y : α, f' x) (λ _, g' x) (pure x) : is_O_congr rfl rfl
+                     ... ↔ g' x = 0 → f' x = 0                       : is_O_const_const_iff _
+
 end zero_const
 
 @[simp] lemma is_O_with_top : is_O_with c f g ⊤ ↔ ∀ x, ∥f x∥ ≤ c * ∥g x∥ := by rw is_O_with; refl
@@ -797,15 +811,6 @@ begin
     metric.mem_closed_ball, dist_zero_right]
 end
 
-theorem is_o_const_const_iff [ne_bot l] {d : E'} {c : F'} (hc : c ≠ 0) :
-  is_o (λ x, d) (λ x, c) l ↔ d = 0 :=
-begin
-  rw is_o_const_iff hc,
-  refine ⟨λ h, tendsto_nhds_unique tendsto_const_nhds h, _⟩,
-  rintros rfl,
-  exact tendsto_const_nhds,
-end
-
 lemma is_o_id_const {c : F'} (hc : c ≠ 0) :
   is_o (λ (x : E'), x) (λ x, c) (𝓝 0) :=
 (is_o_const_iff hc).mpr (continuous_id.tendsto 0)
@@ -1218,6 +1223,16 @@ begin
   { simp only [hc, false_or, is_o_const_left_of_ne hc] }
 end
 
+@[simp] theorem is_o_const_const_iff [ne_bot l] {d : E'} {c : F'} :
+  is_o (λ x, d) (λ x, c) l ↔ d = 0 :=
+have ¬tendsto (function.const α ∥c∥) l at_top,
+  from not_tendsto_at_top_of_tendsto_nhds tendsto_const_nhds,
+by simp [function.const, this]
+
+@[simp] lemma is_o_pure {x} : is_o f' g' (pure x) ↔ f' x = 0 :=
+calc is_o f' g' (pure x) ↔ is_o (λ y : α, f' x) (λ _, g' x) (pure x) : is_o_congr rfl rfl
+                     ... ↔ f' x = 0                                  : is_o_const_const_iff
+
 /-!
 ### Eventually (u / v) * v = u
 

src/analysis/calculus/fderiv.lean

@@ -899,16 +899,26 @@ end
 lemma differentiable_on_const (c : F) : differentiable_on 𝕜 (λx, c) s :=
 (differentiable_const _).differentiable_on
 
-lemma has_fderiv_at_of_subsingleton {R X Y : Type*} [nondiscrete_normed_field R]
-  [normed_group X] [normed_group Y] [normed_space R X] [normed_space R Y] [h : subsingleton X]
-  (f : X → Y) (x : X) :
-  has_fderiv_at f (0 : X →L[R] Y) x :=
+lemma has_fderiv_within_at_singleton (f : E → F) (x : E) :
+  has_fderiv_within_at f (0 : E →L[𝕜] F) {x} x :=
+by simp only [has_fderiv_within_at, nhds_within_singleton, has_fderiv_at_filter, is_o_pure,
+  continuous_linear_map.zero_apply, sub_self]
+
+lemma has_fderiv_at_of_subsingleton [h : subsingleton E] (f : E → F) (x : E) :
+  has_fderiv_at f (0 : E →L[𝕜] F) x :=
 begin
-  rw subsingleton_iff at h,
-  have key : function.const X (f 0) = f := by ext x'; rw h x' 0,
-  exact key ▸ (has_fderiv_at_const (f 0) _),
+  rw [← has_fderiv_within_at_univ, subsingleton_univ.eq_singleton_of_mem (mem_univ x)],
+  exact has_fderiv_within_at_singleton f x
 end
 
+lemma differentiable_on_empty : differentiable_on 𝕜 f ∅ := λ x, false.elim
+
+lemma differentiable_on_singleton : differentiable_on 𝕜 f {x} :=
+forall_eq.2 (has_fderiv_within_at_singleton f x).differentiable_within_at
+
+lemma set.subsingleton.differentiable_on (hs : s.subsingleton) : differentiable_on 𝕜 f s :=
+hs.induction_on differentiable_on_empty (λ x, differentiable_on_singleton)
+
 end const
 
 section continuous_linear_map

src/analysis/calculus/fderiv_symmetric.lean

@@ -265,7 +265,7 @@ begin
       field_simp [has_lt.lt.ne' hpos] },
     { filter_upwards [self_mem_nhds_within] with _ hpos,
       field_simp [has_lt.lt.ne' hpos, has_scalar.smul], }, },
-  simpa only [sub_eq_zero] using (is_o_const_const_iff (@one_ne_zero ℝ _ _)).1 B,
+  simpa only [sub_eq_zero] using is_o_const_const_iff.1 B,
 end
 
 omit s_conv xs hx hf

src/topology/continuous_on.lean

@@ -542,6 +542,14 @@ lemma continuous_on.prod_map {f : α → γ} {g : β → δ} {s : set α} {t : s
 lemma continuous_on_empty (f : α → β) : continuous_on f ∅ :=
 λ x, false.elim
 
+lemma continuous_on_singleton (f : α → β) (a : α) : continuous_on f {a} :=
+forall_eq.2 $ by simpa only [continuous_within_at, nhds_within_singleton, tendsto_pure_left]
+  using λ s, mem_of_mem_nhds
+
+lemma set.subsingleton.continuous_on {s : set α} (hs : s.subsingleton) (f : α → β) :
+  continuous_on f s :=
+hs.induction_on (continuous_on_empty f) (continuous_on_singleton f)
+
 theorem nhds_within_le_comap {x : α} {s : set α} {f : α → β} (ctsf : continuous_within_at f s x) :
   𝓝[s] x ≤ comap f (𝓝[f '' s] (f x)) :=
 map_le_iff_le_comap.1 ctsf.tendsto_nhds_within_image