Linear functions are analytic

In this file we prove that a ContinuousLinearMap defines an analytic function with the formal power series f x = f a + f (x - a). We also prove similar results for bilinear maps.

We deduce this fact from the stronger result that continuous linear maps are continuously polynomial, i.e., they admit a finite power series.

@[simp]

theorem ContinuousLinearMap.fpowerSeries_radius {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (x : E) : (f.fpowerSeries x).radius = ⊤

theorem ContinuousLinearMap.hasFiniteFPowerSeriesOnBall {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (x : E) : HasFiniteFPowerSeriesOnBall (⇑f) (f.fpowerSeries x) x 2 ⊤

theorem ContinuousLinearMap.hasFPowerSeriesOnBall {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (x : E) : HasFPowerSeriesOnBall (⇑f) (f.fpowerSeries x) x ⊤

theorem ContinuousLinearMap.hasFPowerSeriesAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (x : E) : HasFPowerSeriesAt (⇑f) (f.fpowerSeries x) x

theorem ContinuousLinearMap.cpolynomialAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (x : E) : CPolynomialAt 𝕜 (⇑f) x

theorem ContinuousLinearMap.analyticAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (x : E) : AnalyticAt 𝕜 (⇑f) x

theorem ContinuousLinearMap.cpolynomialOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (s : Set E) : CPolynomialOn 𝕜 (⇑f) s

theorem ContinuousLinearMap.analyticOnNhd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (s : Set E) : AnalyticOnNhd 𝕜 (⇑f) s

theorem ContinuousLinearMap.analyticWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (s : Set E) (x : E) : AnalyticWithinAt 𝕜 (⇑f) s x

theorem ContinuousLinearMap.analyticOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (s : Set E) : AnalyticOn 𝕜 (⇑f) s

noncomputable def ContinuousLinearMap.uncurryBilinear {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) : E × F [×2]→L[𝕜] G

Reinterpret a bilinear map f : E →L[𝕜] F →L[𝕜] G as a multilinear map (E × F) [×2]→L[𝕜] G. This multilinear map is the second term in the formal multilinear series expansion of uncurry f. It is given by f.uncurryBilinear ![(x, y), (x', y')] = f x y'.

@[simp]

theorem ContinuousLinearMap.uncurryBilinear_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (m : Fin 2 → E × F) : f.uncurryBilinear m = (f (m 0).1) (m 1).2

noncomputable def ContinuousLinearMap.fpowerSeriesBilinear {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) : FormalMultilinearSeries 𝕜 (E × F) G

Formal multilinear series expansion of a bilinear function f : E →L[𝕜] F →L[𝕜] G.

@[simp]

theorem ContinuousLinearMap.fpowerSeriesBilinear_apply_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) : f.fpowerSeriesBilinear x 0 = ContinuousMultilinearMap.uncurry0 𝕜 (E × F) ((f x.1) x.2)

@[simp]

theorem ContinuousLinearMap.fpowerSeriesBilinear_apply_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) : f.fpowerSeriesBilinear x 1 = (continuousMultilinearCurryFin1 𝕜 (E × F) G).symm (f.deriv₂ x)

@[simp]

theorem ContinuousLinearMap.fpowerSeriesBilinear_apply_two {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) : f.fpowerSeriesBilinear x 2 = f.uncurryBilinear

@[simp]

theorem ContinuousLinearMap.fpowerSeriesBilinear_apply_add_three {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) (n : ℕ) : f.fpowerSeriesBilinear x (n + 3) = 0

@[simp]

theorem ContinuousLinearMap.fpowerSeriesBilinear_radius {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) : (f.fpowerSeriesBilinear x).radius = ⊤

theorem ContinuousLinearMap.hasFPowerSeriesOnBall_bilinear {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) : HasFPowerSeriesOnBall (fun (x : E × F) => (f x.1) x.2) (f.fpowerSeriesBilinear x) x ⊤

theorem ContinuousLinearMap.hasFPowerSeriesAt_bilinear {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) : HasFPowerSeriesAt (fun (x : E × F) => (f x.1) x.2) (f.fpowerSeriesBilinear x) x

theorem ContinuousLinearMap.analyticAt_bilinear {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) : AnalyticAt 𝕜 (fun (x : E × F) => (f x.1) x.2) x

theorem ContinuousLinearMap.analyticWithinAt_bilinear {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (s : Set (E × F)) (x : E × F) : AnalyticWithinAt 𝕜 (fun (x : E × F) => (f x.1) x.2) s x

theorem ContinuousLinearMap.analyticOnNhd_bilinear {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (s : Set (E × F)) : AnalyticOnNhd 𝕜 (fun (x : E × F) => (f x.1) x.2) s

theorem ContinuousLinearMap.analyticOn_bilinear {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (s : Set (E × F)) : AnalyticOn 𝕜 (fun (x : E × F) => (f x.1) x.2) s

theorem analyticAt_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {z : E} : AnalyticAt 𝕜 id z

theorem analyticWithinAt_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {z : E} : AnalyticWithinAt 𝕜 id s z

theorem analyticOnNhd_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} : AnalyticOnNhd 𝕜 (fun (x : E) => x) s

id is entire

theorem analyticOn_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} : AnalyticOn 𝕜 (fun (x : E) => x) s

theorem analyticAt_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} : AnalyticAt 𝕜 (fun (p : E × F) => p.1) p

fst is analytic

theorem analyticWithinAt_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {t : Set (E × F)} {p : E × F} : AnalyticWithinAt 𝕜 (fun (p : E × F) => p.1) t p

theorem analyticAt_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} : AnalyticAt 𝕜 (fun (p : E × F) => p.2) p

snd is analytic

theorem analyticWithinAt_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {t : Set (E × F)} {p : E × F} : AnalyticWithinAt 𝕜 (fun (p : E × F) => p.2) t p

theorem analyticOnNhd_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {t : Set (E × F)} : AnalyticOnNhd 𝕜 (fun (p : E × F) => p.1) t

fst is entire

theorem analyticOn_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {t : Set (E × F)} : AnalyticOn 𝕜 (fun (p : E × F) => p.1) t

theorem analyticOnNhd_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {t : Set (E × F)} : AnalyticOnNhd 𝕜 (fun (p : E × F) => p.2) t

snd is entire

theorem analyticOn_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {t : Set (E × F)} : AnalyticOn 𝕜 (fun (p : E × F) => p.2) t

theorem ContinuousLinearEquiv.analyticAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E ≃L[𝕜] F) (x : E) : AnalyticAt 𝕜 (⇑f) x

theorem ContinuousLinearEquiv.analyticOnNhd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E ≃L[𝕜] F) (s : Set E) : AnalyticOnNhd 𝕜 (⇑f) s

theorem ContinuousLinearEquiv.analyticWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E ≃L[𝕜] F) (s : Set E) (x : E) : AnalyticWithinAt 𝕜 (⇑f) s x

theorem ContinuousLinearEquiv.analyticOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E ≃L[𝕜] F) (s : Set E) : AnalyticOn 𝕜 (⇑f) s

theorem LinearIsometryEquiv.analyticAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E ≃ₗᵢ[𝕜] F) (x : E) : AnalyticAt 𝕜 (⇑f) x

theorem LinearIsometryEquiv.analyticOnNhd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E ≃ₗᵢ[𝕜] F) (s : Set E) : AnalyticOnNhd 𝕜 (⇑f) s

theorem LinearIsometryEquiv.analyticWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E ≃ₗᵢ[𝕜] F) (s : Set E) (x : E) : AnalyticWithinAt 𝕜 (⇑f) s x

theorem LinearIsometryEquiv.analyticOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E ≃ₗᵢ[𝕜] F) (s : Set E) : AnalyticOn 𝕜 (⇑f) s