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}
[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
- 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)
@[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) :
(f.fpower_series x).radius = ⊤
@[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 ⊤
@[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
@[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
- 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
@[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 𝕜 (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)
@[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 = ⊤
@[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 ⊤
@[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
@[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) :