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

We deduce this fact from the stronger result that continuous linear maps are continuously polynomial, i.e., they admit a finite power series.

@[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.hasFiniteFPowerSeriesOnBall {๐•œ : 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) :
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
theorem ContinuousLinearMap.cpolynomialAt {๐•œ : 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) :
CPolynomialAt ๐•œ (โ‡‘f) 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
theorem ContinuousLinearMap.cpolynomialOn {๐•œ : 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) :
CPolynomialOn ๐•œ (โ‡‘f) s
@[deprecated ContinuousLinearMap.cpolynomialOn (since := "2025-03-22")]
theorem ContinuousLinearMap.colynomialOn {๐•œ : 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) :
CPolynomialOn ๐•œ (โ‡‘f) s

Alias of ContinuousLinearMap.cpolynomialOn.

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
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
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
@[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.

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
    @[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
    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
    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) :
      @[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]
      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 : โ„•) :
      @[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 : E ร— F) => (f x.1) x.2) (f.fpowerSeriesBilinear 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 : E ร— F) => (f x.1) x.2) (f.fpowerSeriesBilinear 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 : E ร— F) => (f x.1) x.2) x
      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
      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
      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
      theorem analyticAt_id {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {z : E} :
      AnalyticAt ๐•œ id z
      theorem analyticWithinAt_id {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {s : Set E} {z : E} :
      AnalyticWithinAt ๐•œ id s z
      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

      theorem analyticOn_id {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {s : Set E} :
      AnalyticOn ๐•œ (fun (x : E) => x) s
      @[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.

      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

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

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

      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
      @[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.

      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

      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
      @[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.

      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
      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
      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
      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
      @[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.

      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
      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
      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
      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
      @[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.