mathlib documentation

analysis.analytic.linear

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

@[simp]
noncomputable def continuous_linear_map.fpower_series {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {F : Type u_3} [normed_add_comm_group F] [normed_space π•œ 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} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {F : Type u_3} [normed_add_comm_group F] [normed_space π•œ F] (f : E β†’L[π•œ] F) (x : E) (n : β„•) :
f.fpower_series x (n + 2) = 0
@[simp]
theorem continuous_linear_map.fpower_series_radius {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {F : Type u_3} [normed_add_comm_group F] [normed_space π•œ F] (f : E β†’L[π•œ] F) (x : E) :
@[protected]
theorem continuous_linear_map.has_fpower_series_on_ball {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {F : Type u_3} [normed_add_comm_group F] [normed_space π•œ F] (f : E β†’L[π•œ] F) (x : E) :
@[protected]
theorem continuous_linear_map.has_fpower_series_at {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {F : Type u_3} [normed_add_comm_group F] [normed_space π•œ F] (f : E β†’L[π•œ] F) (x : E) :
@[protected]
theorem continuous_linear_map.analytic_at {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {F : Type u_3} [normed_add_comm_group F] [normed_space π•œ F] (f : E β†’L[π•œ] F) (x : E) :
analytic_at π•œ ⇑f x
noncomputable def continuous_linear_map.uncurry_bilinear {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {F : Type u_3} [normed_add_comm_group F] [normed_space π•œ F] {G : Type u_4} [normed_add_comm_group G] [normed_space π•œ G] (f : E β†’L[π•œ] F β†’L[π•œ] G) :
continuous_multilinear_map π•œ (Ξ» (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} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {F : Type u_3} [normed_add_comm_group F] [normed_space π•œ F] {G : Type u_4} [normed_add_comm_group G] [normed_space π•œ G] (f : E β†’L[π•œ] F β†’L[π•œ] G) (m : fin 2 β†’ E Γ— F) :
@[simp]
noncomputable def continuous_linear_map.fpower_series_bilinear {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {F : Type u_3} [normed_add_comm_group F] [normed_space π•œ F] {G : Type u_4} [normed_add_comm_group G] [normed_space π•œ G] (f : E β†’L[π•œ] F β†’L[π•œ] G) (x : E Γ— F) :

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} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {F : Type u_3} [normed_add_comm_group F] [normed_space π•œ F] {G : Type u_4} [normed_add_comm_group G] [normed_space π•œ G] (f : E β†’L[π•œ] F β†’L[π•œ] G) (x : E Γ— F) :
@[protected]
theorem continuous_linear_map.has_fpower_series_on_ball_bilinear {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {F : Type u_3} [normed_add_comm_group F] [normed_space π•œ F] {G : Type u_4} [normed_add_comm_group G] [normed_space π•œ G] (f : E β†’L[π•œ] F β†’L[π•œ] G) (x : E Γ— F) :
@[protected]
theorem continuous_linear_map.has_fpower_series_at_bilinear {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {F : Type u_3} [normed_add_comm_group F] [normed_space π•œ F] {G : Type u_4} [normed_add_comm_group G] [normed_space π•œ G] (f : E β†’L[π•œ] F β†’L[π•œ] G) (x : E Γ— F) :
@[protected]
theorem continuous_linear_map.analytic_at_bilinear {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {F : Type u_3} [normed_add_comm_group F] [normed_space π•œ F] {G : Type u_4} [normed_add_comm_group G] [normed_space π•œ G] (f : E β†’L[π•œ] F β†’L[π•œ] G) (x : E Γ— F) :
analytic_at π•œ (Ξ» (x : E Γ— F), ⇑(⇑f x.fst) x.snd) x