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)
.
def
ContinuousLinearMap.fpowerSeries
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
(f : E βL[π] F)
(x : E)
:
FormalMultilinearSeries π E F
Formal power series of a continuous linear map f : E βL[π] F
at x : E
:
f y = f x + f (y - x)
.
Instances For
@[simp]
theorem
ContinuousLinearMap.fpower_series_apply_zero
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
(f : E βL[π] F)
(x : E)
:
ContinuousLinearMap.fpowerSeries f x 0 = ContinuousMultilinearMap.curry0 π E (βf x)
@[simp]
theorem
ContinuousLinearMap.fpower_series_apply_one
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
(f : E βL[π] F)
(x : E)
:
ContinuousLinearMap.fpowerSeries f x 1 = β(LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 π E F)) f
@[simp]
theorem
ContinuousLinearMap.fpowerSeries_apply_add_two
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
(f : E βL[π] F)
(x : E)
(n : β)
:
ContinuousLinearMap.fpowerSeries f x (n + 2) = 0
@[simp]
theorem
ContinuousLinearMap.fpowerSeries_radius
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
(f : E βL[π] F)
(x : E)
:
theorem
ContinuousLinearMap.hasFPowerSeriesOnBall
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
(f : E βL[π] F)
(x : E)
:
HasFPowerSeriesOnBall (βf) (ContinuousLinearMap.fpowerSeries f x) x β€
theorem
ContinuousLinearMap.hasFPowerSeriesAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
(f : E βL[π] F)
(x : E)
:
HasFPowerSeriesAt (βf) (ContinuousLinearMap.fpowerSeries f x) x
theorem
ContinuousLinearMap.analyticAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
(f : E βL[π] F)
(x : E)
:
AnalyticAt π (βf) x
def
ContinuousLinearMap.uncurryBilinear
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace π G]
(f : E βL[π] F βL[π] G)
:
ContinuousMultilinearMap π (fun i => 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'
.
Instances For
@[simp]
theorem
ContinuousLinearMap.uncurryBilinear_apply
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace π G]
(f : E βL[π] F βL[π] G)
(m : Fin 2 β E Γ F)
:
β(ContinuousLinearMap.uncurryBilinear f) m = β(βf (m 0).fst) (m 1).snd
def
ContinuousLinearMap.fpowerSeriesBilinear
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[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
.
Instances For
@[simp]
theorem
ContinuousLinearMap.fpowerSeriesBilinear_apply_zero
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace π G]
(f : E βL[π] F βL[π] G)
(x : E Γ F)
:
ContinuousLinearMap.fpowerSeriesBilinear f x 0 = ContinuousMultilinearMap.curry0 π (E Γ F) (β(βf x.fst) x.snd)
@[simp]
theorem
ContinuousLinearMap.fpowerSeriesBilinear_apply_one
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace π G]
(f : E βL[π] F βL[π] G)
(x : E Γ F)
:
ContinuousLinearMap.fpowerSeriesBilinear f x 1 = β(LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 π (E Γ F) G)) (β(ContinuousLinearMap.derivβ f) x)
@[simp]
theorem
ContinuousLinearMap.fpowerSeriesBilinear_apply_two
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace π G]
(f : E βL[π] F βL[π] G)
(x : E Γ F)
:
@[simp]
theorem
ContinuousLinearMap.fpowerSeriesBilinear_apply_add_three
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace π G]
(f : E βL[π] F βL[π] G)
(x : E Γ F)
(n : β)
:
ContinuousLinearMap.fpowerSeriesBilinear f x (n + 3) = 0
@[simp]
theorem
ContinuousLinearMap.fpowerSeriesBilinear_radius
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace π G]
(f : E βL[π] F βL[π] G)
(x : E Γ F)
:
theorem
ContinuousLinearMap.hasFPowerSeriesOnBall_bilinear
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace π G]
(f : E βL[π] F βL[π] G)
(x : E Γ F)
:
HasFPowerSeriesOnBall (fun x => β(βf x.fst) x.snd) (ContinuousLinearMap.fpowerSeriesBilinear f x) x β€
theorem
ContinuousLinearMap.hasFPowerSeriesAt_bilinear
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace π G]
(f : E βL[π] F βL[π] G)
(x : E Γ F)
:
HasFPowerSeriesAt (fun x => β(βf x.fst) x.snd) (ContinuousLinearMap.fpowerSeriesBilinear f x) x
theorem
ContinuousLinearMap.analyticAt_bilinear
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace π G]
(f : E βL[π] F βL[π] G)
(x : E Γ F)
:
AnalyticAt π (fun x => β(βf x.fst) x.snd) x