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

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) :
FormalMultilinearSeries.radius (ContinuousLinearMap.fpowerSeries f x) = ⊀
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) (ContinuousLinearMap.fpowerSeries f 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) (ContinuousLinearMap.fpowerSeries f 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
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) :
    (ContinuousLinearMap.uncurryBilinear f) 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
    • One or more equations did not get rendered due to their size.
    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) :
      ContinuousLinearMap.fpowerSeriesBilinear f x 0 = ContinuousMultilinearMap.curry0 π•œ (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) :
      ContinuousLinearMap.fpowerSeriesBilinear f x 1 = (LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 π•œ (E Γ— F) G)) ((ContinuousLinearMap.derivβ‚‚ f) 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) :
      ContinuousLinearMap.fpowerSeriesBilinear f x 2 = ContinuousLinearMap.uncurryBilinear f
      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 : β„•) :
      ContinuousLinearMap.fpowerSeriesBilinear f 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) :
      FormalMultilinearSeries.radius (ContinuousLinearMap.fpowerSeriesBilinear f x) = ⊀
      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) (ContinuousLinearMap.fpowerSeriesBilinear f 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) (ContinuousLinearMap.fpowerSeriesBilinear f 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 analyticAt_id (π•œ : Type u_1) [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] (z : E) :
      AnalyticAt π•œ id z
      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

      id is entire

      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 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 analyticOn_fst (π•œ : Type u_1) [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set (E Γ— F)} :
      AnalyticOn π•œ (fun (p : E Γ— F) => p.1) s

      fst 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] {s : Set (E Γ— F)} :
      AnalyticOn π•œ (fun (p : E Γ— F) => p.2) s

      snd is entire