feat(analysis/analytic): a continuous linear map defines an analytic function (#5840)

Also add convenience lemmas with conclusion `radius = ⊤`.

Author: urkud

src/analysis/analytic/basic.lean

@@ -102,6 +102,17 @@ lemma le_radius_of_is_O (h : is_O (λ n, ∥p n∥ * r^n) (λ n, (1 : ℝ)) at_t
 exists.elim (is_O_one_nat_at_top_iff.1 h) $ λ C hC, p.le_radius_of_bound C $
   λ n, (le_abs_self _).trans (hC n)
 
+lemma radius_eq_top_of_forall_nnreal_is_O
+  (h : ∀ r : ℝ≥0, is_O (λ n, ∥p n∥ * r^n) (λ n, (1 : ℝ)) at_top) : p.radius = ⊤ :=
+ennreal.eq_top_of_forall_nnreal_le $ λ r, p.le_radius_of_is_O (h r)
+
+lemma radius_eq_top_of_eventually_eq_zero (h : ∀ᶠ n in at_top, p n = 0) : p.radius = ⊤ :=
+p.radius_eq_top_of_forall_nnreal_is_O $
+  λ r, (is_O_zero _ _).congr' (h.mono $ λ n hn, by simp [hn]) eventually_eq.rfl
+
+lemma radius_eq_top_of_forall_image_add_eq_zero (n : ℕ) (hn : ∀ m, p (m + n) = 0) : p.radius = ⊤ :=
+p.radius_eq_top_of_eventually_eq_zero $ mem_at_top_sets.2 ⟨n, λ k hk, nat.sub_add_cancel hk ▸ hn _⟩
+
 /-- For `r` strictly smaller than the radius of `p`, then `∥pₙ∥ rⁿ` tends to zero exponentially:
 for some `0 < a < 1`, `∥p n∥ rⁿ = o(aⁿ)`. -/
 lemma is_o_of_lt_radius (h : ↑r < p.radius) :

src/analysis/analytic/linear.lean

@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2021 Yury G. Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Yury G. Kudryashov
+-/
+import analysis.analytic.basic
+
+/-!
+# Linear functions are analytic
+
+In this file we prove that a `continuous_linear_map` defines an analytic function with
+the formal power series `f x = f a + f (x - a)`.
+-/
+
+variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
+{E : Type*} [normed_group E] [normed_space 𝕜 E]
+{F : Type*} [normed_group F] [normed_space 𝕜 F]
+
+open_locale topological_space classical big_operators nnreal ennreal
+open set filter asymptotics
+
+noncomputable theory
+
+namespace continuous_linear_map
+
+/-- Formal power series of a continuous linear map `f : E →L[𝕜] F` at `x : E`:
+`f y = f x + f (y - x)`. -/
+@[simp] def fpower_series (f : E →L[𝕜] F) (x : E) : formal_multilinear_series 𝕜 E F
+| 0 := continuous_multilinear_map.curry0 𝕜 _ (f x)
+| 1 := (continuous_multilinear_curry_fin1 𝕜 _ _).symm f
+| _ := 0
+
+@[simp] lemma fpower_series_apply_add_two (f : E →L[𝕜] F) (x : E) (n : ℕ) :
+  f.fpower_series x (n + 2) = 0 := rfl
+
+@[simp] lemma fpower_series_radius (f : E →L[𝕜] F) (x : E) : (f.fpower_series x).radius = ∞ :=
+(f.fpower_series x).radius_eq_top_of_forall_image_add_eq_zero 2 $ λ n, rfl
+
+protected theorem has_fpower_series_on_ball (f : E →L[𝕜] F) (x : E) :
+  has_fpower_series_on_ball f (f.fpower_series x) x ∞ :=
+{ r_le := by simp,
+  r_pos := ennreal.coe_lt_top,
+  has_sum := λ y _, (has_sum_nat_add_iff' 2).1 $
+    by simp [finset.sum_range_succ, ← sub_sub, has_sum_zero] }
+
+protected theorem has_fpower_series_at (f : E →L[𝕜] F) (x : E) :
+  has_fpower_series_at f (f.fpower_series x) x :=
+⟨∞, f.has_fpower_series_on_ball x⟩
+
+protected theorem analytic_at (f : E →L[𝕜] F) (x : E) : analytic_at 𝕜 f x :=
+(f.has_fpower_series_at x).analytic_at
+
+end continuous_linear_map

src/data/real/ennreal.lean

@@ -1046,6 +1046,9 @@ begin
   exact h r hr
 end
 
+lemma eq_top_of_forall_nnreal_le {x : ennreal} (h : ∀ r : ℝ≥0, ↑r ≤ x) : x = ∞ :=
+top_unique $ le_of_forall_nnreal_lt $ λ r hr, h r
+
 lemma div_add_div_same {a b c : ennreal} : a / c + b / c = (a + b) / c :=
 eq.symm $ right_distrib a b (c⁻¹)