feat(analysis/calculus/cont_diff_def): no continuity is needed for ha…

…s_ftaylor_series_up_to if n = ∞ (#18808)

We also add `has_ftaylor_series_up_to_iff_top` in order that the notation is consistent between `has_ftaylor_series_up_to` and `has_ftaylor_series_up_to_on`.

src/analysis/calculus/cont_diff_def.lean

@@ -248,6 +248,16 @@ begin
       apply (H m).cont m le_rfl } }
 end
 
+/-- In the case that `n = ∞` we don't need the continuity assumption in
+`has_ftaylor_series_up_to_on`. -/
+lemma has_ftaylor_series_up_to_on_top_iff' : has_ftaylor_series_up_to_on ∞ f p s ↔
+  (∀ x ∈ s, (p x 0).uncurry0 = f x) ∧
+  (∀ (m : ℕ), ∀ x ∈ s, has_fderiv_within_at (λ y, p y m) (p x m.succ).curry_left s x) :=
+-- Everything except for the continuity is trivial:
+⟨λ h, ⟨h.1, λ m, h.2 m (with_top.coe_lt_top m)⟩, λ h, ⟨h.1, λ m _, h.2 m, λ m _ x hx,
+  -- The continuity follows from the existence of a derivative:
+  (h.2 m x hx).continuous_within_at⟩⟩
+
 /-- If a function has a Taylor series at order at least `1`, then the term of order `1` of this
 series is a derivative of `f`. -/
 lemma has_ftaylor_series_up_to_on.has_fderiv_within_at
@@ -1234,6 +1244,18 @@ lemma has_ftaylor_series_up_to_zero_iff :
 by simp [has_ftaylor_series_up_to_on_univ_iff.symm, continuous_iff_continuous_on_univ,
          has_ftaylor_series_up_to_on_zero_iff]
 
+lemma has_ftaylor_series_up_to_top_iff : has_ftaylor_series_up_to ∞ f p ↔
+  ∀ (n : ℕ), has_ftaylor_series_up_to n f p :=
+by simp only [← has_ftaylor_series_up_to_on_univ_iff, has_ftaylor_series_up_to_on_top_iff]
+
+/-- In the case that `n = ∞` we don't need the continuity assumption in
+`has_ftaylor_series_up_to`. -/
+lemma has_ftaylor_series_up_to_top_iff' : has_ftaylor_series_up_to ∞ f p ↔
+  (∀ x, (p x 0).uncurry0 = f x) ∧
+  (∀ (m : ℕ) x, has_fderiv_at (λ y, p y m) (p x m.succ).curry_left x) :=
+by simp only [← has_ftaylor_series_up_to_on_univ_iff, has_ftaylor_series_up_to_on_top_iff',
+  mem_univ, forall_true_left, has_fderiv_within_at_univ]
+
 /-- If a function has a Taylor series at order at least `1`, then the term of order `1` of this
 series is a derivative of `f`. -/
 lemma has_ftaylor_series_up_to.has_fderiv_at