Documentation

Mathlib.Analysis.Analytic.Linear

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

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) :
    @[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) :
    @[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 : β„•) :
    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) :
    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) :
    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) :
        @[simp]
        @[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 : β„•) :
        @[simp]
        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