# 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). We also prove similar results for multilinear maps.

@[simp]
theorem ContinuousLinearMap.fpowerSeries_radius {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] (f : E βL[π] F) (x : E) :
theorem ContinuousLinearMap.hasFPowerSeriesOnBall {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] (f : E βL[π] F) (x : E) :
HasFPowerSeriesOnBall (βf) (f.fpowerSeries x) x β€
theorem ContinuousLinearMap.hasFPowerSeriesAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] (f : E βL[π] F) (x : E) :
HasFPowerSeriesAt (βf) (f.fpowerSeries x) x
theorem ContinuousLinearMap.analyticAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] (f : E βL[π] F) (x : E) :
AnalyticAt π (βf) x
def ContinuousLinearMap.uncurryBilinear {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] (f : E βL[π] F βL[π] G) :
ContinuousMultilinearMap π (fun (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.uncurryBilinear ![(x, y), (x', y')] = f x y'.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem ContinuousLinearMap.uncurryBilinear_apply {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] (f : E βL[π] F βL[π] G) (m : Fin 2 β E Γ F) :
f.uncurryBilinear m = (f (m 0).1) (m 1).2
def ContinuousLinearMap.fpowerSeriesBilinear {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem ContinuousLinearMap.fpowerSeriesBilinear_apply_zero {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] (f : E βL[π] F βL[π] G) (x : E Γ F) :
f.fpowerSeriesBilinear x 0 = ContinuousMultilinearMap.curry0 π (E Γ F) ((f x.1) x.2)
@[simp]
theorem ContinuousLinearMap.fpowerSeriesBilinear_apply_one {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] (f : E βL[π] F βL[π] G) (x : E Γ F) :
f.fpowerSeriesBilinear x 1 = (continuousMultilinearCurryFin1 π (E Γ F) G).symm (f.derivβ x)
@[simp]
theorem ContinuousLinearMap.fpowerSeriesBilinear_apply_two {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] (f : E βL[π] F βL[π] G) (x : E Γ F) :
f.fpowerSeriesBilinear x 2 = f.uncurryBilinear
@[simp]
theorem ContinuousLinearMap.fpowerSeriesBilinear_apply_add_three {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] (f : E βL[π] F βL[π] G) (x : E Γ F) (n : β) :
f.fpowerSeriesBilinear x (n + 3) = 0
@[simp]
theorem ContinuousLinearMap.fpowerSeriesBilinear_radius {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] (f : E βL[π] F βL[π] G) (x : E Γ F) :
theorem ContinuousLinearMap.hasFPowerSeriesOnBall_bilinear {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] (f : E βL[π] F βL[π] G) (x : E Γ F) :
HasFPowerSeriesOnBall (fun (x : E Γ F) => (f x.1) x.2) (f.fpowerSeriesBilinear x) x β€
theorem ContinuousLinearMap.hasFPowerSeriesAt_bilinear {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] (f : E βL[π] F βL[π] G) (x : E Γ F) :
HasFPowerSeriesAt (fun (x : E Γ F) => (f x.1) x.2) (f.fpowerSeriesBilinear x) x
theorem ContinuousLinearMap.analyticAt_bilinear {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] (f : E βL[π] F βL[π] G) (x : E Γ F) :
AnalyticAt π (fun (x : E Γ F) => (f x.1) x.2) x
theorem analyticAt_id (π : Type u_1) [] {E : Type u_2} [NormedSpace π E] (z : E) :
AnalyticAt π id z
theorem analyticOn_id (π : Type u_1) [] {E : Type u_2} [NormedSpace π E] {s : Set E} :
AnalyticOn π (fun (x : E) => x) s

id is entire

theorem analyticAt_fst (π : Type u_1) [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {p : E Γ F} :
AnalyticAt π (fun (p : E Γ F) => p.1) p

fst is analytic

theorem analyticAt_snd (π : Type u_1) [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {p : E Γ F} :
AnalyticAt π (fun (p : E Γ F) => p.2) p

snd is analytic

theorem analyticOn_fst (π : Type u_1) [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {s : Set (E Γ F)} :
AnalyticOn π (fun (p : E Γ F) => p.1) s

fst is entire

theorem analyticOn_snd (π : Type u_1) [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {s : Set (E Γ F)} :
AnalyticOn π (fun (p : E Γ F) => p.2) s

snd is entire