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).

def ContinuousLinearMap.fpowerSeries {𝕜 : 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) : FormalMultilinearSeries 𝕜 E F

Formal power series of a continuous linear map f : E →L[𝕜] F at x : E: f y = f x + f (y - x).

@[simp]

theorem ContinuousLinearMap.fpower_series_apply_zero {𝕜 : 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) : ContinuousLinearMap.fpowerSeries f x 0 = ContinuousMultilinearMap.curry0 𝕜 E (↑f x)

@[simp]

theorem ContinuousLinearMap.fpower_series_apply_one {𝕜 : 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) : ContinuousLinearMap.fpowerSeries f x 1 = ↑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F)) f

@[simp]

theorem ContinuousLinearMap.fpowerSeries_apply_add_two {𝕜 : 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) (n : ℕ) : ContinuousLinearMap.fpowerSeries f x (n + 2) = 0

@[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) : FormalMultilinearSeries.radius (ContinuousLinearMap.fpowerSeries f x) = ⊤

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) (ContinuousLinearMap.fpowerSeries f 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) (ContinuousLinearMap.fpowerSeries f x) 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

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) : ContinuousMultilinearMap 𝕜 (fun i => E × F) 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) : ↑(ContinuousLinearMap.uncurryBilinear f) m = ↑(↑f (m 0).fst) (m 1).snd

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) : ContinuousLinearMap.fpowerSeriesBilinear f x 0 = ContinuousMultilinearMap.curry0 𝕜 (E × F) (↑(↑f x.fst) x.snd)

@[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) : ContinuousLinearMap.fpowerSeriesBilinear f x 1 = ↑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 (E × F) G)) (↑(ContinuousLinearMap.deriv₂ f) 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) : ContinuousLinearMap.fpowerSeriesBilinear f x 2 = ContinuousLinearMap.uncurryBilinear f

@[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 : ℕ) : ContinuousLinearMap.fpowerSeriesBilinear f 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) : FormalMultilinearSeries.radius (ContinuousLinearMap.fpowerSeriesBilinear f x) = ⊤

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 => ↑(↑f x.fst) x.snd) (ContinuousLinearMap.fpowerSeriesBilinear f 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 => ↑(↑f x.fst) x.snd) (ContinuousLinearMap.fpowerSeriesBilinear f 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 => ↑(↑f x.fst) x.snd) x