Mathlib.Analysis.Analytic.Linear

ContinuousLinearMap.fpowerSeries_radius theorem

(f : E →L[𝕜] F) (x : E) : (f.fpowerSeries x).radius = ∞

Full source

@[simp]
theorem fpowerSeries_radius (f : E →L[𝕜] F) (x : E) : (f.fpowerSeries x).radius = ∞ :=
  (f.fpowerSeries x).radius_eq_top_of_forall_image_add_eq_zero 2 fun _ => rfl

Infinite Radius of Convergence for Continuous Linear Map Power Series

Informal description

For any continuous linear map $ f \colon E \to F $ between normed spaces over a field $ \mathbb{K} $, and for any point $ x \in E $, the formal power series associated to $ f $ centered at $ x $ has an infinite radius of convergence, i.e., $\text{radius}(f.\text{fpowerSeries}\, x) = \infty$.

ContinuousLinearMap.hasFiniteFPowerSeriesOnBall theorem

(f : E →L[𝕜] F) (x : E) : HasFiniteFPowerSeriesOnBall f (f.fpowerSeries x) x 2 ∞

Full source

protected theorem hasFiniteFPowerSeriesOnBall (f : E →L[𝕜] F) (x : E) :
    HasFiniteFPowerSeriesOnBall f (f.fpowerSeries x) x 2 ∞ where
  r_le := by simp
  r_pos := ENNReal.coe_lt_top
  hasSum := fun _ => (hasSum_nat_add_iff' 2).1 <| by
    simp [Finset.sum_range_succ, ← sub_sub, hasSum_zero, fpowerSeries]
  finite := by
    intro m hm
    match m with
    | 0 | 1 => linarith
    | n + 2 => simp [fpowerSeries]

Finite power series expansion property for continuous linear maps

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f \colon E \to F$ be a continuous linear map. For any point $x \in E$, the function $f$ admits a finite power series expansion on the ball of infinite radius centered at $x$, given by the formal power series $f.\text{fpowerSeries}\,x$ with all terms of degree 2 or higher vanishing.

ContinuousLinearMap.hasFPowerSeriesOnBall theorem

(f : E →L[𝕜] F) (x : E) : HasFPowerSeriesOnBall f (f.fpowerSeries x) x ∞

Full source

protected theorem hasFPowerSeriesOnBall (f : E →L[𝕜] F) (x : E) :
    HasFPowerSeriesOnBall f (f.fpowerSeries x) x ∞ :=
  (f.hasFiniteFPowerSeriesOnBall x).toHasFPowerSeriesOnBall

Power Series Expansion of Continuous Linear Maps on Infinite Balls

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f \colon E \to F$ be a continuous linear map. For any point $x \in E$, the function $f$ admits a power series expansion on the ball of infinite radius centered at $x$, given by the formal power series $f.\text{fpowerSeries}\,x$.

ContinuousLinearMap.hasFPowerSeriesAt theorem

(f : E →L[𝕜] F) (x : E) : HasFPowerSeriesAt f (f.fpowerSeries x) x

Full source

protected theorem hasFPowerSeriesAt (f : E →L[𝕜] F) (x : E) :
    HasFPowerSeriesAt f (f.fpowerSeries x) x :=
  ⟨∞, f.hasFPowerSeriesOnBall x⟩

Power Series Expansion of Continuous Linear Maps at a Point

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f \colon E \to F$ be a continuous linear map. For any point $x \in E$, the function $f$ has a power series expansion at $x$ given by the formal power series $f.\text{fpowerSeries}\,x$.

ContinuousLinearMap.cpolynomialAt theorem

(f : E →L[𝕜] F) (x : E) : CPolynomialAt 𝕜 f x

Full source

protected theorem cpolynomialAt (f : E →L[𝕜] F) (x : E) : CPolynomialAt 𝕜 f x :=
  (f.hasFiniteFPowerSeriesOnBall x).cpolynomialAt

Continuous linear maps are continuously polynomial at every point

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f \colon E \to F$ be a continuous linear map. Then $f$ is continuously polynomial at every point $x \in E$.

ContinuousLinearMap.analyticAt theorem

(f : E →L[𝕜] F) (x : E) : AnalyticAt 𝕜 f x

Full source

protected theorem analyticAt (f : E →L[𝕜] F) (x : E) : AnalyticAt 𝕜 f x :=
  (f.hasFPowerSeriesAt x).analyticAt

Continuous linear maps are analytic at every point

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f \colon E \to F$ be a continuous linear map. Then $f$ is analytic at every point $x \in E$.

ContinuousLinearMap.cpolynomialOn theorem

(f : E →L[𝕜] F) (s : Set E) : CPolynomialOn 𝕜 f s

Full source

protected theorem cpolynomialOn (f : E →L[𝕜] F) (s : Set E) : CPolynomialOn 𝕜 f s :=
  fun x _ ↦ f.cpolynomialAt x

Continuous linear maps are continuously polynomial on any subset

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f \colon E \to F$ be a continuous linear map. Then $f$ is continuously polynomial on any subset $s \subseteq E$, meaning that for every $x \in s$, $f$ admits a finite power series expansion around $x$.

ContinuousLinearMap.analyticOnNhd theorem

(f : E →L[𝕜] F) (s : Set E) : AnalyticOnNhd 𝕜 f s

Full source

protected theorem analyticOnNhd (f : E →L[𝕜] F) (s : Set E) : AnalyticOnNhd 𝕜 f s :=
  fun x _ ↦ f.analyticAt x

Continuous Linear Maps are Analytic on Neighborhoods of Subsets

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f \colon E \to F$ be a continuous linear map. Then $f$ is analytic on a neighborhood of any subset $s \subseteq E$, meaning that for every point $x \in s$, there exists a neighborhood of $x$ where $f$ admits a convergent power series expansion.

ContinuousLinearMap.analyticWithinAt theorem

(f : E →L[𝕜] F) (s : Set E) (x : E) : AnalyticWithinAt 𝕜 f s x

Full source

protected theorem analyticWithinAt (f : E →L[𝕜] F) (s : Set E) (x : E) : AnalyticWithinAt 𝕜 f s x :=
  (f.analyticAt x).analyticWithinAt

Continuous linear maps are analytic within any set at any point

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f \colon E \to F$ be a continuous linear map. Then for any subset $s \subseteq E$ and any point $x \in E$, the function $f$ is analytic within $s$ at $x$.

ContinuousLinearMap.analyticOn theorem

(f : E →L[𝕜] F) (s : Set E) : AnalyticOn 𝕜 f s

Full source

protected theorem analyticOn (f : E →L[𝕜] F) (s : Set E) : AnalyticOn 𝕜 f s :=
  fun x _ ↦ f.analyticWithinAt _ x

Continuous Linear Maps are Analytic on Any Subset

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f \colon E \to F$ be a continuous linear map. Then $f$ is analytic on any subset $s \subseteq E$, meaning that for every point $x \in s$, the function $f$ admits a convergent power series expansion in a neighborhood of $x$ intersected with $s$.

ContinuousLinearMap.uncurryBilinear definition

(f : E →L[𝕜] F →L[𝕜] G) : E × F [×2]→L[𝕜] G

Full source

/-- 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'`. -/
def uncurryBilinear (f : E →L[𝕜] F →L[𝕜] G) : E × FE × F[×2]→L[𝕜] G :=
  @ContinuousLinearMap.uncurryLeft 𝕜 1 (fun _ => E × F) G _ _ _ _ _ <|
    (↑(continuousMultilinearCurryFin1 𝕜 (E × F) G).symm : (E × F →L[𝕜] G) →L[𝕜] _).comp <|
      f.bilinearComp (fst _ _ _) (snd _ _ _)

Uncurried Bilinear Map as Multilinear Map

Informal description

Given a continuous bilinear map $ f : E \to_{L[\mathbb{K}]} F \to_{L[\mathbb{K}]} G $, the function `uncurryBilinear` reinterprets $ f $ as a multilinear map $ (E \times F)^{[2]} \to_{L[\mathbb{K}]} G $. This multilinear map represents the second term in the formal multilinear series expansion of the uncurried version of $ f $. Specifically, it satisfies $ f.\text{uncurryBilinear} [(x, y), (x', y')] = f x y' $.

ContinuousLinearMap.uncurryBilinear_apply theorem

(f : E →L[𝕜] F →L[𝕜] G) (m : Fin 2 → E × F) : f.uncurryBilinear m = f (m 0).1 (m 1).2

Full source

@[simp]
theorem uncurryBilinear_apply (f : E →L[𝕜] F →L[𝕜] G) (m : Fin 2 → E × F) :
    f.uncurryBilinear m = f (m 0).1 (m 1).2 :=
  rfl

Evaluation of Uncurried Bilinear Map

Informal description

Let $E$, $F$, and $G$ be normed spaces over a field $\mathbb{K}$, and let $f : E \to_{L[\mathbb{K}]} F \to_{L[\mathbb{K}]} G$ be a continuous bilinear map. For any function $m : \text{Fin } 2 \to E \times F$, the evaluation of the uncurried bilinear map $f.\text{uncurryBilinear}$ at $m$ equals $f$ applied to the first component of $m(0)$ and the second component of $m(1)$, i.e., \[ f.\text{uncurryBilinear}(m) = f(m(0)_1)(m(1)_2). \]

ContinuousLinearMap.fpowerSeriesBilinear definition

(f : E →L[𝕜] F →L[𝕜] G) (x : E × F) : FormalMultilinearSeries 𝕜 (E × F) G

Full source

/-- Formal multilinear series expansion of a bilinear function `f : E →L[𝕜] F →L[𝕜] G`. -/
def fpowerSeriesBilinear (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) : FormalMultilinearSeries 𝕜 (E × F) G
  | 0 => ContinuousMultilinearMap.uncurry0 𝕜 _ (f x.1 x.2)
  | 1 => (continuousMultilinearCurryFin1 𝕜 (E × F) G).symm (f.deriv₂ x)
  | 2 => f.uncurryBilinear
  | _ => 0

Formal multilinear series expansion of a continuous bilinear map

Informal description

Given a continuous bilinear map $ f : E \to_{L[\mathbb{K}]} F \to_{L[\mathbb{K}]} G $ and a point $ x \in E \times F $, the formal multilinear series expansion of $ f $ at $ x $ is defined as follows: - The 0-th term is the constant term $ f(x_1, x_2) $, viewed as a 0-linear map. - The 1-st term is the derivative of $ f $ at $ x $, reinterpreted as a 1-linear map. - The 2-nd term is the uncurried bilinear map $ f $ itself, viewed as a 2-linear map. - All higher terms are zero.

ContinuousLinearMap.fpowerSeriesBilinear_apply_zero theorem

 (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) : fpowerSeriesBilinear f x 0 = ContinuousMultilinearMap.uncurry0 𝕜 _ (f x.1 x.2)

Full source

@[simp]
theorem fpowerSeriesBilinear_apply_zero (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
    fpowerSeriesBilinear f x 0 = ContinuousMultilinearMap.uncurry0 𝕜 _ (f x.1 x.2) :=
  rfl

Zeroth Term of Formal Multilinear Series for Continuous Bilinear Map

Informal description

For a continuous bilinear map $f \colon E \to_{L[\mathbb{K}]} F \to_{L[\mathbb{K}]} G$ and a point $x = (x_1, x_2) \in E \times F$, the zeroth term of the formal multilinear series expansion of $f$ at $x$ is equal to the constant term $f(x_1, x_2)$, viewed as a 0-linear map.

ContinuousLinearMap.fpowerSeriesBilinear_apply_one theorem

 (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
  fpowerSeriesBilinear f x 1 = (continuousMultilinearCurryFin1 𝕜 (E × F) G).symm (f.deriv₂ x)

Full source

@[simp]
theorem fpowerSeriesBilinear_apply_one (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
    fpowerSeriesBilinear f x 1 = (continuousMultilinearCurryFin1 𝕜 (E × F) G).symm (f.deriv₂ x) :=
  rfl

First-order term of formal multilinear series expansion of a continuous bilinear map equals its derivative

Informal description

For any continuous bilinear map $f \colon E \to_{L[\mathbb{K}]} F \to_{L[\mathbb{K}]} G$ and any point $x \in E \times F$, the first-order term of the formal multilinear series expansion of $f$ at $x$ is equal to the derivative of $f$ at $x$, reinterpreted as a $1$-linear map via the inverse of the continuous multilinear curry isomorphism for $1$-linear maps.

ContinuousLinearMap.fpowerSeriesBilinear_apply_two theorem

(f : E →L[𝕜] F →L[𝕜] G) (x : E × F) : fpowerSeriesBilinear f x 2 = f.uncurryBilinear

Full source

@[simp]
theorem fpowerSeriesBilinear_apply_two (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
    fpowerSeriesBilinear f x 2 = f.uncurryBilinear :=
  rfl

Second Term of Formal Multilinear Series for Continuous Bilinear Map Equals Uncurried Bilinear Map

Informal description

For any continuous bilinear map $f \colon E \to_{L[\mathbb{K}]} F \to_{L[\mathbb{K}]} G$ and any point $x \in E \times F$, the second term of the formal multilinear series expansion of $f$ at $x$ is equal to the uncurried bilinear map $f$ interpreted as a multilinear map.

ContinuousLinearMap.fpowerSeriesBilinear_apply_add_three theorem

(f : E →L[𝕜] F →L[𝕜] G) (x : E × F) (n) : fpowerSeriesBilinear f x (n + 3) = 0

Full source

@[simp]
theorem fpowerSeriesBilinear_apply_add_three (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) (n) :
    fpowerSeriesBilinear f x (n + 3) = 0 :=
  rfl

Vanishing of Higher Terms in Formal Multilinear Series Expansion of Bilinear Maps

Informal description

For any continuous bilinear map $ f : E \to_{L[\mathbb{K}]} F \to_{L[\mathbb{K}]} G $, point $ x \in E \times F $, and natural number $ n $, the $(n+3)$-th term of the formal multilinear series expansion of $ f $ at $ x $ is zero, i.e., $ (f.\text{fpowerSeriesBilinear} \, x) \, (n + 3) = 0 $.

ContinuousLinearMap.fpowerSeriesBilinear_radius theorem

(f : E →L[𝕜] F →L[𝕜] G) (x : E × F) : (f.fpowerSeriesBilinear x).radius = ∞

Full source

@[simp]
theorem fpowerSeriesBilinear_radius (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
    (f.fpowerSeriesBilinear x).radius = ∞ :=
  (f.fpowerSeriesBilinear x).radius_eq_top_of_forall_image_add_eq_zero 3 fun _ => rfl

Infinite Radius of Convergence for Formal Multilinear Series of Continuous Bilinear Maps

Informal description

For any continuous bilinear map $ f : E \to_{L[\mathbb{K}]} F \to_{L[\mathbb{K}]} G $ and any point $ x \in E \times F $, the radius of convergence of the formal multilinear series expansion of $ f $ at $ x $ is infinite, i.e., $\text{radius}(f.\text{fpowerSeriesBilinear} \, x) = \infty$.

ContinuousLinearMap.hasFPowerSeriesOnBall_bilinear theorem

 (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) : HasFPowerSeriesOnBall (fun x : E × F => f x.1 x.2) (f.fpowerSeriesBilinear x) x ∞

Full source

protected theorem hasFPowerSeriesOnBall_bilinear (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
    HasFPowerSeriesOnBall (fun x : E × F => f x.1 x.2) (f.fpowerSeriesBilinear x) x ∞ :=
  { r_le := by simp
    r_pos := ENNReal.coe_lt_top
    hasSum := fun _ =>
      (hasSum_nat_add_iff' 3).1 <| by
        simp only [Finset.sum_range_succ, Finset.sum_range_one, Prod.fst_add, Prod.snd_add,
          f.map_add_add]
        simp [fpowerSeriesBilinear, hasSum_zero] }

Power Series Expansion of Continuous Bilinear Maps with Infinite Radius of Convergence

Informal description

Let $ E $, $ F $, and $ G $ be normed spaces over a field $ \mathbb{K} $. For any continuous bilinear map $ f : E \to_{L[\mathbb{K}]} F \to_{L[\mathbb{K}]} G $ and any point $ x \in E \times F $, the function $ (x_1, x_2) \mapsto f(x_1)(x_2) $ has a formal power series expansion $ f.\text{fpowerSeriesBilinear} \, x $ centered at $ x $ with an infinite radius of convergence. Specifically, for all $ y $ in the ball of infinite radius centered at $ x $, the function can be expressed as: \[ f(x_1 + y_1, x_2 + y_2) = \sum_{n=0}^\infty (f.\text{fpowerSeriesBilinear} \, x)_n (y_1, y_2)^n. \] Here, the series terminates after the second term, with the 0-th term being $ f(x_1, x_2) $, the 1-st term being the derivative of $ f $ at $ x $, and the 2-nd term being the bilinear map $ f $ itself, while all higher terms vanish.

ContinuousLinearMap.hasFPowerSeriesAt_bilinear theorem

 (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) : HasFPowerSeriesAt (fun x : E × F => f x.1 x.2) (f.fpowerSeriesBilinear x) x

Full source

protected theorem hasFPowerSeriesAt_bilinear (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
    HasFPowerSeriesAt (fun x : E × F => f x.1 x.2) (f.fpowerSeriesBilinear x) x :=
  ⟨∞, f.hasFPowerSeriesOnBall_bilinear x⟩

Power Series Expansion of Continuous Bilinear Maps at a Point

Informal description

Let $E$, $F$, and $G$ be normed spaces over a field $\mathbb{K}$. For any continuous bilinear map $f : E \to_{L[\mathbb{K}]} F \to_{L[\mathbb{K}]} G$ and any point $x \in E \times F$, the function $(x_1, x_2) \mapsto f(x_1)(x_2)$ has a formal power series expansion at $x$ given by $f.\text{fpowerSeriesBilinear} \, x$. Specifically, this means there exists a neighborhood of $x$ where the function can be expressed as: \[ f(x_1 + y_1, x_2 + y_2) = \sum_{n=0}^\infty (f.\text{fpowerSeriesBilinear} \, x)_n (y_1, y_2)^n \] where the series terminates after the second term (with the 0-th term being $f(x_1, x_2)$, the 1-st term being the derivative of $f$ at $x$, and the 2-nd term being $f$ itself).

ContinuousLinearMap.analyticAt_bilinear theorem

(f : E →L[𝕜] F →L[𝕜] G) (x : E × F) : AnalyticAt 𝕜 (fun x : E × F => f x.1 x.2) x

Full source

protected theorem analyticAt_bilinear (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
    AnalyticAt 𝕜 (fun x : E × F => f x.1 x.2) x :=
  (f.hasFPowerSeriesAt_bilinear x).analyticAt

Analyticity of Continuous Bilinear Maps at a Point

Informal description

Let $E$, $F$, and $G$ be normed spaces over a field $\mathbb{K}$. For any continuous bilinear map $f : E \to_{L[\mathbb{K}]} F \to_{L[\mathbb{K}]} G$ and any point $x \in E \times F$, the function $(x_1, x_2) \mapsto f(x_1)(x_2)$ is analytic at $x$.

ContinuousLinearMap.analyticWithinAt_bilinear theorem

 (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

Full source

protected theorem analyticWithinAt_bilinear (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 :=
  (f.analyticAt_bilinear x).analyticWithinAt

Analyticity of Continuous Bilinear Maps Within a Set at a Point

Informal description

Let $E$, $F$, and $G$ be normed spaces over a field $\mathbb{K}$. For any continuous bilinear map $f : E \to_{L[\mathbb{K}]} F \to_{L[\mathbb{K}]} G$, any subset $s \subseteq E \times F$, and any point $x \in E \times F$, the function $(x_1, x_2) \mapsto f(x_1)(x_2)$ is analytic within $s$ at $x$. This means there exists a neighborhood of $x$ where the function can be expressed as a convergent power series expansion within $s \cup \{x\}$.

ContinuousLinearMap.analyticOnNhd_bilinear theorem

(f : E →L[𝕜] F →L[𝕜] G) (s : Set (E × F)) : AnalyticOnNhd 𝕜 (fun x : E × F => f x.1 x.2) s

Full source

protected theorem analyticOnNhd_bilinear (f : E →L[𝕜] F →L[𝕜] G) (s : Set (E × F)) :
    AnalyticOnNhd 𝕜 (fun x : E × F => f x.1 x.2) s :=
  fun x _ ↦ f.analyticAt_bilinear x

Analyticity of Continuous Bilinear Maps on a Neighborhood of a Set

Informal description

Let $E$, $F$, and $G$ be normed spaces over a field $\mathbb{K}$. For any continuous bilinear map $f \colon E \to_{L[\mathbb{K}]} F \to_{L[\mathbb{K}]} G$ and any subset $s \subseteq E \times F$, the function $(x_1, x_2) \mapsto f(x_1)(x_2)$ is analytic on a neighborhood of $s$.

ContinuousLinearMap.analyticOn_bilinear theorem

(f : E →L[𝕜] F →L[𝕜] G) (s : Set (E × F)) : AnalyticOn 𝕜 (fun x : E × F => f x.1 x.2) s

Full source

protected theorem analyticOn_bilinear (f : E →L[𝕜] F →L[𝕜] G) (s : Set (E × F)) :
    AnalyticOn 𝕜 (fun x : E × F => f x.1 x.2) s :=
  (f.analyticOnNhd_bilinear s).analyticOn

Analyticity of Continuous Bilinear Maps on a Set

Informal description

Let $E$, $F$, and $G$ be normed spaces over a field $\mathbb{K}$. For any continuous bilinear map $f \colon E \to_{L[\mathbb{K}]} F \to_{L[\mathbb{K}]} G$ and any subset $s \subseteq E \times F$, the function $(x_1, x_2) \mapsto f(x_1)(x_2)$ is analytic on $s$.

analyticAt_id theorem

: AnalyticAt 𝕜 (id : E → E) z

Full source

@[fun_prop]
lemma analyticAt_id : AnalyticAt 𝕜 (id : E → E) z :=
  (ContinuousLinearMap.id 𝕜 E).analyticAt z

Identity Function is Analytic at Every Point

Informal description

The identity function $\mathrm{id} \colon E \to E$ is analytic at every point $z \in E$.

analyticWithinAt_id theorem

: AnalyticWithinAt 𝕜 (id : E → E) s z

Full source

lemma analyticWithinAt_id : AnalyticWithinAt 𝕜 (id : E → E) s z :=
  analyticAt_id.analyticWithinAt

Identity Function is Analytic Within Any Set at Every Point

Informal description

The identity function $\mathrm{id} \colon E \to E$ is analytic within any subset $s \subseteq E$ at every point $z \in E$.

analyticOnNhd_id theorem

: AnalyticOnNhd 𝕜 (fun x : E ↦ x) s

Full source

/-- `id` is entire -/
theorem analyticOnNhd_id : AnalyticOnNhd 𝕜 (fun x : E ↦ x) s :=
  fun _ _ ↦ analyticAt_id

Identity Function is Analytic on Neighborhood of Any Set

Informal description

The identity function $\mathrm{id} \colon E \to E$, defined by $\mathrm{id}(x) = x$, is analytic on a neighborhood of any set $s \subseteq E$.

analyticOn_id theorem

: AnalyticOn 𝕜 (fun x : E ↦ x) s

Full source

theorem analyticOn_id : AnalyticOn 𝕜 (fun x : E ↦ x) s :=
  fun _ _ ↦ analyticWithinAt_id

Analyticity of the Identity Function on Any Subset

Informal description

The identity function $\mathrm{id} \colon E \to E$, defined by $\mathrm{id}(x) = x$, is analytic on any subset $s \subseteq E$.

analyticAt_fst theorem

: AnalyticAt 𝕜 (fun p : E × F ↦ p.fst) p

Full source

/-- `fst` is analytic -/
theorem analyticAt_fst : AnalyticAt 𝕜 (fun p : E × F ↦ p.fst) p :=
  (ContinuousLinearMap.fst 𝕜 E F).analyticAt p

Analyticity of the first projection map on product spaces

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$. The projection map $\pi_1 \colon E \times F \to E$ defined by $\pi_1(x,y) = x$ is analytic at every point $p \in E \times F$.

analyticWithinAt_fst theorem

: AnalyticWithinAt 𝕜 (fun p : E × F ↦ p.fst) t p

Full source

theorem analyticWithinAt_fst : AnalyticWithinAt 𝕜 (fun p : E × F ↦ p.fst) t p :=
  analyticAt_fst.analyticWithinAt

Analyticity of the First Projection Within a Set

Informal description

The first projection map $\pi_1 \colon E \times F \to E$, defined by $\pi_1(x,y) = x$, is analytic within any subset $t \subseteq E \times F$ at every point $p \in E \times F$.

analyticAt_snd theorem

: AnalyticAt 𝕜 (fun p : E × F ↦ p.snd) p

Full source

/-- `snd` is analytic -/
theorem analyticAt_snd : AnalyticAt 𝕜 (fun p : E × F ↦ p.snd) p :=
  (ContinuousLinearMap.snd 𝕜 E F).analyticAt p

Analyticity of the Second Projection Function

Informal description

The second projection function $(x, y) \mapsto y$ from the product space $E \times F$ to $F$ is analytic at every point $p \in E \times F$.

analyticWithinAt_snd theorem

: AnalyticWithinAt 𝕜 (fun p : E × F ↦ p.snd) t p

Full source

theorem analyticWithinAt_snd : AnalyticWithinAt 𝕜 (fun p : E × F ↦ p.snd) t p :=
  analyticAt_snd.analyticWithinAt

Analyticity of Second Projection within a Set at a Point

Informal description

The second projection function $(x, y) \mapsto y$ from the product space $E \times F$ to $F$ is analytic within a set $t \subseteq E \times F$ at a point $p \in E \times F$.

analyticOnNhd_fst theorem

: AnalyticOnNhd 𝕜 (fun p : E × F ↦ p.fst) t

Full source

/-- `fst` is entire -/
theorem analyticOnNhd_fst : AnalyticOnNhd 𝕜 (fun p : E × F ↦ p.fst) t :=
  fun _ _ ↦ analyticAt_fst

Analyticity of the First Projection on a Neighborhood of a Set

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $t \subseteq E \times F$ be a subset. The first projection map $\pi_1 \colon E \times F \to E$ defined by $\pi_1(x,y) = x$ is analytic on a neighborhood of $t$.

analyticOn_fst theorem

: AnalyticOn 𝕜 (fun p : E × F ↦ p.fst) t

Full source

theorem analyticOn_fst : AnalyticOn 𝕜 (fun p : E × F ↦ p.fst) t :=
  fun _ _ ↦ analyticWithinAt_fst

Analyticity of the First Projection on a Set

Informal description

The first projection map $\pi_1 \colon E \times F \to E$, defined by $\pi_1(x,y) = x$, is analytic on the set $t \subseteq E \times F$.

analyticOnNhd_snd theorem

: AnalyticOnNhd 𝕜 (fun p : E × F ↦ p.snd) t

Full source

/-- `snd` is entire -/
theorem analyticOnNhd_snd : AnalyticOnNhd 𝕜 (fun p : E × F ↦ p.snd) t :=
  fun _ _ ↦ analyticAt_snd

Analyticity of Second Projection on Neighborhood of Set

Informal description

The second projection function $(x, y) \mapsto y$ from the product space $E \times F$ to $F$ is analytic on a neighborhood of the set $t \subseteq E \times F$.

analyticOn_snd theorem

: AnalyticOn 𝕜 (fun p : E × F ↦ p.snd) t

Full source

theorem analyticOn_snd : AnalyticOn 𝕜 (fun p : E × F ↦ p.snd) t :=
  fun _ _ ↦ analyticWithinAt_snd

Analyticity of Second Projection on Set

Informal description

The second projection function $(x, y) \mapsto y$ from the product space $E \times F$ to $F$ is analytic on the set $t \subseteq E \times F$.

ContinuousLinearEquiv.analyticAt theorem

: AnalyticAt 𝕜 f x

Full source

protected theorem analyticAt : AnalyticAt 𝕜 f x :=
  ((f : E →L[𝕜] F).hasFPowerSeriesAt x).analyticAt

Continuous linear equivalences are analytic

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f \colon E \to F$ be a continuous linear equivalence. Then $f$ is analytic at every point $x \in E$.

ContinuousLinearEquiv.analyticOnNhd theorem

: AnalyticOnNhd 𝕜 f s

Full source

protected theorem analyticOnNhd : AnalyticOnNhd 𝕜 f s :=
  fun x _ ↦ f.analyticAt x

Continuous Linear Equivalences are Locally Analytic

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f \colon E \to F$ be a continuous linear equivalence. Then $f$ is analytic on a neighborhood of any set $s \subseteq E$.

ContinuousLinearEquiv.analyticWithinAt theorem

(f : E →L[𝕜] F) (s : Set E) (x : E) : AnalyticWithinAt 𝕜 f s x

Full source

protected theorem analyticWithinAt (f : E →L[𝕜] F) (s : Set E) (x : E) : AnalyticWithinAt 𝕜 f s x :=
  (f.analyticAt x).analyticWithinAt

Analyticity of Continuous Linear Equivalences Within a Set at a Point

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f \colon E \to F$ be a continuous linear equivalence. For any subset $s \subseteq E$ and any point $x \in E$, the function $f$ is analytic within $s$ at $x$.

ContinuousLinearEquiv.analyticOn theorem

(f : E →L[𝕜] F) (s : Set E) : AnalyticOn 𝕜 f s

Full source

protected theorem analyticOn (f : E →L[𝕜] F) (s : Set E) : AnalyticOn 𝕜 f s :=
  fun x _ ↦ f.analyticWithinAt _ x

Continuous Linear Equivalences are Analytic on Any Subset

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f \colon E \to F$ be a continuous linear equivalence. Then $f$ is analytic on any subset $s \subseteq E$, meaning that for every $x \in s$, there exists a neighborhood of $x$ where $f$ admits a convergent power series expansion.

LinearIsometryEquiv.analyticAt theorem

: AnalyticAt 𝕜 f x

Full source

protected theorem analyticAt : AnalyticAt 𝕜 f x :=
  ((f : E →L[𝕜] F).hasFPowerSeriesAt x).analyticAt

Analyticity of Linear Isometry Equivalences

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f \colon E \to F$ be a linear isometry equivalence. Then $f$ is analytic at every point $x \in E$.

LinearIsometryEquiv.analyticOnNhd theorem

: AnalyticOnNhd 𝕜 f s

Full source

protected theorem analyticOnNhd : AnalyticOnNhd 𝕜 f s :=
  fun x _ ↦ f.analyticAt x

Analyticity of Linear Isometry Equivalences on Neighborhoods

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f \colon E \to F$ be a linear isometry equivalence. Then $f$ is analytic on a neighborhood of any subset $s \subseteq E$, meaning that for every $x \in s$, there exists a neighborhood of $x$ where $f$ admits a convergent power series expansion.

LinearIsometryEquiv.analyticWithinAt theorem

(f : E →L[𝕜] F) (s : Set E) (x : E) : AnalyticWithinAt 𝕜 f s x

Full source

protected theorem analyticWithinAt (f : E →L[𝕜] F) (s : Set E) (x : E) : AnalyticWithinAt 𝕜 f s x :=
  (f.analyticAt x).analyticWithinAt

Linear Isometry Equivalences are Analytic Within Any Set at Every Point

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f \colon E \to F$ be a linear isometry equivalence. For any subset $s \subseteq E$ and any point $x \in E$, the function $f$ is analytic within $s$ at $x$.

LinearIsometryEquiv.analyticOn theorem

(f : E →L[𝕜] F) (s : Set E) : AnalyticOn 𝕜 f s

Full source

protected theorem analyticOn (f : E →L[𝕜] F) (s : Set E) : AnalyticOn 𝕜 f s :=
  fun x _ ↦ f.analyticWithinAt _ x

Analyticity of Linear Isometry Equivalences on Subsets

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f \colon E \to F$ be a linear isometry equivalence. Then $f$ is analytic on any subset $s \subseteq E$, meaning that for every $x \in s$, the function $f$ admits a convergent power series expansion in a neighborhood of $x$ intersected with $s \cup \{x\}$.