analysis.analytic.linear

@[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_multilinear_series 𝕜 E F

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

Equations

f.fpower_series x n.succ.succ = 0
f.fpower_series x 1 = ⇑((continuous_multilinear_curry_fin1 𝕜 E F).symm) f
f.fpower_series x 0 = continuous_multilinear_map.curry0 𝕜 E (⇑f x)

source

@[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

source

@[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) :

(f.fpower_series x).radius = ⊤

source

@[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) :

has_fpower_series_on_ball ⇑f (f.fpower_series x) x ⊤

source

@[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) :

has_fpower_series_at ⇑f (f.fpower_series x) x

source

@[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

source

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

f.uncurry_bilinear = (↑((continuous_multilinear_curry_fin1 𝕜 (E × F) G).symm).comp (f.bilinear_comp (continuous_linear_map.fst 𝕜 E F) (continuous_linear_map.snd 𝕜 E F))).uncurry_left

source

@[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) :

⇑(f.uncurry_bilinear) m = ⇑(⇑f (m 0).fst) (m 1).snd

source

@[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 𝕜 (E × F) G

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

Equations

f.fpower_series_bilinear x n.succ.succ.succ = 0
f.fpower_series_bilinear x 2 = f.uncurry_bilinear
f.fpower_series_bilinear x 1 = ⇑((continuous_multilinear_curry_fin1 𝕜 (E × F) G).symm) (⇑(f.deriv₂) x)
f.fpower_series_bilinear x 0 = continuous_multilinear_map.curry0 𝕜 (E × F) (⇑(⇑f x.fst) x.snd)

source

@[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) :

(f.fpower_series_bilinear x).radius = ⊤

source

@[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) :

has_fpower_series_on_ball (λ (x : E × F), ⇑(⇑f x.fst) x.snd) (f.fpower_series_bilinear x) x ⊤

source

@[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) :

has_fpower_series_at (λ (x : E × F), ⇑(⇑f x.fst) x.snd) (f.fpower_series_bilinear x) x

source

@[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

mathlib documentation

Linear functions are analytic #