# mathlib3documentation

analysis.analytic.linear

# Linear functions are analytic #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[simp]
noncomputable def continuous_linear_map.fpower_series {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →L[𝕜] F) (x : E) :

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

Equations
@[simp]
theorem continuous_linear_map.fpower_series_apply_add_two {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →L[𝕜] F) (x : E) (n : ) :
(n + 2) = 0
@[simp]
theorem continuous_linear_map.fpower_series_radius {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →L[𝕜] F) (x : E) :
@[protected]
theorem continuous_linear_map.has_fpower_series_on_ball {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →L[𝕜] F) (x : E) :
x
@[protected]
theorem continuous_linear_map.has_fpower_series_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →L[𝕜] F) (x : E) :
x
@[protected]
theorem continuous_linear_map.analytic_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E →L[𝕜] F) (x : E) :
f x
noncomputable def continuous_linear_map.uncurry_bilinear {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (f : E →L[𝕜] F →L[𝕜] G) :
(λ (i : fin 2), 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.uncurry_bilinear ![(x, y), (x', y')] = f x y'.

Equations
@[simp]
theorem continuous_linear_map.uncurry_bilinear_apply {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (f : E →L[𝕜] F →L[𝕜] G) (m : fin 2 E × F) :
(f.uncurry_bilinear) m = (f (m 0).fst) (m 1).snd
@[simp]
noncomputable def continuous_linear_map.fpower_series_bilinear {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
(E × F) G

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

Equations
@[simp]
theorem continuous_linear_map.fpower_series_bilinear_radius {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
@[protected]
theorem continuous_linear_map.has_fpower_series_on_ball_bilinear {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
has_fpower_series_on_ball (λ (x : E × F), (f x.fst) x.snd) x
@[protected]
theorem continuous_linear_map.has_fpower_series_at_bilinear {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
has_fpower_series_at (λ (x : E × F), (f x.fst) x.snd) x
@[protected]
theorem continuous_linear_map.analytic_at_bilinear {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
(λ (x : E × F), (f x.fst) x.snd) x