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 bilinear maps.

TODO: port to use CPolynomial, and prove the stronger result that continuous linear maps are continuously polynomial

source

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

(f.fpowerSeries x).radius = ⊤

source

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) (f.fpowerSeries x) x ⊤

source

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) (f.fpowerSeries x) x

source

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

source

theorem ContinuousLinearMap.analyticOnNhd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (s : Set E) :

AnalyticOnNhd 𝕜 (⇑f) s

source

theorem ContinuousLinearMap.analyticWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (s : Set E) (x : E) :

AnalyticWithinAt 𝕜 (⇑f) s x

source

theorem ContinuousLinearMap.analyticOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (s : Set E) :

AnalyticOn 𝕜 (⇑f) s

source

@[deprecated ContinuousLinearMap.analyticOn (since := "2024-09-26")]

theorem ContinuousLinearMap.analyticWithinOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (s : Set E) :

AnalyticOn 𝕜 (⇑f) s

Alias of ContinuousLinearMap.analyticOn.

source

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 : 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

source

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

f.uncurryBilinear m = (f (m 0).1) (m 1).2

source

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.

Equations

f.fpowerSeriesBilinear x 0 = ContinuousMultilinearMap.uncurry0 𝕜 (E × F) ((f x.1) x.2)
f.fpowerSeriesBilinear x 1 = (continuousMultilinearCurryFin1 𝕜 (E × F) G).symm (f.deriv₂ x)
f.fpowerSeriesBilinear x 2 = f.uncurryBilinear
f.fpowerSeriesBilinear x x✝ = 0

Instances For

source

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

f.fpowerSeriesBilinear x 0 = ContinuousMultilinearMap.uncurry0 𝕜 (E × F) ((f x.1) x.2)

source

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

f.fpowerSeriesBilinear x 1 = (continuousMultilinearCurryFin1 𝕜 (E × F) G).symm (f.deriv₂ x)

source

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

f.fpowerSeriesBilinear x 2 = f.uncurryBilinear

source

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

f.fpowerSeriesBilinear x (n + 3) = 0

source

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

(f.fpowerSeriesBilinear x).radius = ⊤

source

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 : E × F) => (f x.1) x.2) (f.fpowerSeriesBilinear x) x ⊤

source

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 : E × F) => (f x.1) x.2) (f.fpowerSeriesBilinear x) x

source

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 : E × F) => (f x.1) x.2) x

source

theorem ContinuousLinearMap.analyticWithinAt_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) (s : Set (E × F)) (x : E × F) :

AnalyticWithinAt 𝕜 (fun (x : E × F) => (f x.1) x.2) s x

source

theorem ContinuousLinearMap.analyticOnNhd_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) (s : Set (E × F)) :

AnalyticOnNhd 𝕜 (fun (x : E × F) => (f x.1) x.2) s

source

theorem ContinuousLinearMap.analyticOn_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) (s : Set (E × F)) :

AnalyticOn 𝕜 (fun (x : E × F) => (f x.1) x.2) s

source

theorem analyticAt_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {z : E} :

AnalyticAt 𝕜 id z

source

theorem analyticWithinAt_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {z : E} :

AnalyticWithinAt 𝕜 id s z

source

theorem analyticOnNhd_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} :

AnalyticOnNhd 𝕜 (fun (x : E) => x) s

id is entire

source

theorem analyticOn_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} :

AnalyticOn 𝕜 (fun (x : E) => x) s

source

@[deprecated analyticOn_id (since := "2024-09-26")]

theorem analyticWithinOn_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} :

AnalyticOn 𝕜 (fun (x : E) => x) s

Alias of analyticOn_id.

source

theorem analyticAt_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} :

AnalyticAt 𝕜 (fun (p : E × F) => p.1) p

fst is analytic

source

theorem analyticWithinAt_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {t : Set (E × F)} {p : E × F} :

AnalyticWithinAt 𝕜 (fun (p : E × F) => p.1) t p

source

theorem analyticAt_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} :

AnalyticAt 𝕜 (fun (p : E × F) => p.2) p

snd is analytic

source

theorem analyticWithinAt_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {t : Set (E × F)} {p : E × F} :

AnalyticWithinAt 𝕜 (fun (p : E × F) => p.2) t p

source

theorem analyticOnNhd_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {t : Set (E × F)} :

AnalyticOnNhd 𝕜 (fun (p : E × F) => p.1) t

fst is entire

source

theorem analyticOn_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {t : Set (E × F)} :

AnalyticOn 𝕜 (fun (p : E × F) => p.1) t

source

@[deprecated analyticOn_fst (since := "2024-09-26")]

theorem analyticWithinOn_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {t : Set (E × F)} :

AnalyticOn 𝕜 (fun (p : E × F) => p.1) t

Alias of analyticOn_fst.

source

theorem analyticOnNhd_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {t : Set (E × F)} :

AnalyticOnNhd 𝕜 (fun (p : E × F) => p.2) t

snd is entire

source

theorem analyticOn_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {t : Set (E × F)} :

AnalyticOn 𝕜 (fun (p : E × F) => p.2) t

source

@[deprecated analyticOn_snd (since := "2024-09-26")]

theorem analyticWithinOn_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {t : Set (E × F)} :

AnalyticOn 𝕜 (fun (p : E × F) => p.2) t

Alias of analyticOn_snd.

source

theorem ContinuousLinearEquiv.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

source

theorem ContinuousLinearEquiv.analyticOnNhd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E ≃L[𝕜] F) (s : Set E) :

AnalyticOnNhd 𝕜 (⇑f) s

source

theorem ContinuousLinearEquiv.analyticWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (s : Set E) (x : E) :

AnalyticWithinAt 𝕜 (⇑f) s x

source

theorem ContinuousLinearEquiv.analyticOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (s : Set E) :

AnalyticOn 𝕜 (⇑f) s

source

@[deprecated ContinuousLinearEquiv.analyticOn (since := "2024-09-26")]

theorem ContinuousLinearEquiv.analyticWithinOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (s : Set E) :

AnalyticOn 𝕜 (⇑f) s

Alias of ContinuousLinearEquiv.analyticOn.

source

theorem LinearIsometryEquiv.analyticAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E ≃ₗᵢ[𝕜] F) (x : E) :

AnalyticAt 𝕜 (⇑f) x

source

theorem LinearIsometryEquiv.analyticOnNhd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E ≃ₗᵢ[𝕜] F) (s : Set E) :

AnalyticOnNhd 𝕜 (⇑f) s

source

theorem LinearIsometryEquiv.analyticWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (s : Set E) (x : E) :

AnalyticWithinAt 𝕜 (⇑f) s x

source

theorem LinearIsometryEquiv.analyticOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (s : Set E) :

AnalyticOn 𝕜 (⇑f) s

source

@[deprecated LinearIsometryEquiv.analyticOn (since := "2024-09-26")]

theorem LinearIsometryEquiv.analyticWithinOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (s : Set E) :

AnalyticOn 𝕜 (⇑f) s

Alias of LinearIsometryEquiv.analyticOn.

Documentation

Mathlib.Analysis.Analytic.Linear

Linear functions are analytic #