Mathlib.Analysis.Analytic.Constructions

hasFPowerSeriesOnBall_const theorem

{c : F} {e : E} : HasFPowerSeriesOnBall (fun _ => c) (constFormalMultilinearSeries 𝕜 E c) e ⊤

Full source

theorem hasFPowerSeriesOnBall_const {c : F} {e : E} :
    HasFPowerSeriesOnBall (fun _ => c) (constFormalMultilinearSeries 𝕜 E c) e ⊤ := by
  refine ⟨by simp, WithTop.top_pos, fun _ => hasSum_single 0 fun n hn => ?_⟩
  simp [constFormalMultilinearSeries_apply hn]

Constant Function Has Formal Power Series Expansion on Entire Space

Informal description

For any constant function $f(x) = c$ where $c$ belongs to a normed space $F$ over a field $\mathbb{K}$, and for any point $e$ in a normed space $E$ over $\mathbb{K}$, the function $f$ has a formal power series expansion (given by the constant formal multilinear series) centered at $e$ that converges on the entire space $E$.

hasFPowerSeriesAt_const theorem

{c : F} {e : E} : HasFPowerSeriesAt (fun _ => c) (constFormalMultilinearSeries 𝕜 E c) e

Full source

theorem hasFPowerSeriesAt_const {c : F} {e : E} :
    HasFPowerSeriesAt (fun _ => c) (constFormalMultilinearSeries 𝕜 E c) e :=
  ⟨⊤, hasFPowerSeriesOnBall_const⟩

Constant Function Has Formal Power Series Expansion at Point

Informal description

For any constant function $f(x) = c$ where $c$ belongs to a normed space $F$ over a field $\mathbb{K}$, and for any point $e$ in a normed space $E$ over $\mathbb{K}$, the function $f$ has a formal power series expansion (given by the constant formal multilinear series) centered at $e$.

analyticAt_const theorem

{v : F} {x : E} : AnalyticAt 𝕜 (fun _ => v) x

Full source

@[fun_prop]
theorem analyticAt_const {v : F} {x : E} : AnalyticAt 𝕜 (fun _ => v) x :=
  ⟨constFormalMultilinearSeries 𝕜 E v, hasFPowerSeriesAt_const⟩

Analyticity of Constant Functions

Informal description

For any constant function $f(x) = v$ where $v$ belongs to a normed space $F$ over a field $\mathbb{K}$, and for any point $x$ in a normed space $E$ over $\mathbb{K}$, the function $f$ is analytic at $x$.

analyticOnNhd_const theorem

{v : F} {s : Set E} : AnalyticOnNhd 𝕜 (fun _ => v) s

Full source

theorem analyticOnNhd_const {v : F} {s : Set E} : AnalyticOnNhd 𝕜 (fun _ => v) s :=
  fun _ _ => analyticAt_const

Neighborhood Analyticity of Constant Functions

Informal description

For any constant function $f(x) = v$ where $v$ belongs to a normed space $F$ over a field $\mathbb{K}$, and for any subset $s$ of a normed space $E$ over $\mathbb{K}$, the function $f$ is analytic on a neighborhood of $s$.

analyticWithinAt_const theorem

{v : F} {s : Set E} {x : E} : AnalyticWithinAt 𝕜 (fun _ => v) s x

Full source

theorem analyticWithinAt_const {v : F} {s : Set E} {x : E} : AnalyticWithinAt 𝕜 (fun _ => v) s x :=
  analyticAt_const.analyticWithinAt

Analyticity of Constant Functions Within a Set at a Point

Informal description

For any constant function $f(x) = v$ where $v$ belongs to a normed space $F$ over a field $\mathbb{K}$, any subset $s$ of a normed space $E$ over $\mathbb{K}$, and any point $x \in E$, the function $f$ is analytic within $s$ at $x$.

analyticOn_const theorem

{v : F} {s : Set E} : AnalyticOn 𝕜 (fun _ => v) s

Full source

theorem analyticOn_const {v : F} {s : Set E} : AnalyticOn 𝕜 (fun _ => v) s :=
  analyticOnNhd_const.analyticOn

Analyticity of Constant Functions on a Set

Informal description

For any constant function $f(x) = v$ where $v$ belongs to a normed space $F$ over a field $\mathbb{K}$, and for any subset $s$ of a normed space $E$ over $\mathbb{K}$, the function $f$ is analytic on $s$.

HasFPowerSeriesWithinOnBall.add theorem

 (hf : HasFPowerSeriesWithinOnBall f pf s x r) (hg : HasFPowerSeriesWithinOnBall g pg s x r) :
  HasFPowerSeriesWithinOnBall (f + g) (pf + pg) s x r

Full source

theorem HasFPowerSeriesWithinOnBall.add (hf : HasFPowerSeriesWithinOnBall f pf s x r)
    (hg : HasFPowerSeriesWithinOnBall g pg s x r) :
    HasFPowerSeriesWithinOnBall (f + g) (pf + pg) s x r :=
  { r_le := le_trans (le_min_iff.2 ⟨hf.r_le, hg.r_le⟩) (pf.min_radius_le_radius_add pg)
    r_pos := hf.r_pos
    hasSum := fun hy h'y => (hf.hasSum hy h'y).add (hg.hasSum hy h'y) }

Sum of Analytic Functions is Analytic on a Ball

Informal description

Let $f$ and $g$ be functions from a normed space $E$ to a normed space $F$ over a complete normed field $\mathbb{K}$. Suppose $f$ has a formal power series expansion $pf$ within a ball $B(x, r)$ around $x \in E$ and $g$ has a formal power series expansion $pg$ within the same ball. Then the sum $f + g$ has a formal power series expansion $pf + pg$ within the ball $B(x, r)$.

HasFPowerSeriesOnBall.add theorem

 (hf : HasFPowerSeriesOnBall f pf x r) (hg : HasFPowerSeriesOnBall g pg x r) :
  HasFPowerSeriesOnBall (f + g) (pf + pg) x r

Full source

theorem HasFPowerSeriesOnBall.add (hf : HasFPowerSeriesOnBall f pf x r)
    (hg : HasFPowerSeriesOnBall g pg x r) : HasFPowerSeriesOnBall (f + g) (pf + pg) x r :=
  { r_le := le_trans (le_min_iff.2 ⟨hf.r_le, hg.r_le⟩) (pf.min_radius_le_radius_add pg)
    r_pos := hf.r_pos
    hasSum := fun hy => (hf.hasSum hy).add (hg.hasSum hy) }

Sum of Power Series Expansions on a Ball

Informal description

Let $f$ and $g$ be functions with formal power series expansions $pf$ and $pg$ respectively, converging on a ball centered at $x$ with radius $r$. Then the sum $f + g$ has a formal power series expansion given by $pf + pg$, which also converges on the same ball.

HasFPowerSeriesWithinAt.add theorem

 (hf : HasFPowerSeriesWithinAt f pf s x) (hg : HasFPowerSeriesWithinAt g pg s x) :
  HasFPowerSeriesWithinAt (f + g) (pf + pg) s x

Full source

theorem HasFPowerSeriesWithinAt.add
    (hf : HasFPowerSeriesWithinAt f pf s x) (hg : HasFPowerSeriesWithinAt g pg s x) :
    HasFPowerSeriesWithinAt (f + g) (pf + pg) s x := by
  rcases (hf.eventually.and hg.eventually).exists with ⟨r, hr⟩
  exact ⟨r, hr.1.add hr.2⟩

Sum of Analytic Functions is Analytic at a Point Within a Set

Informal description

Let $f$ and $g$ be functions from a normed space $E$ to a normed space $F$ over a complete normed field $\mathbb{K}$. Suppose $f$ has a formal power series expansion $pf$ at $x \in E$ within a set $s \subseteq E$, and $g$ has a formal power series expansion $pg$ at $x$ within the same set $s$. Then the sum $f + g$ has a formal power series expansion $pf + pg$ at $x$ within $s$.

HasFPowerSeriesAt.add theorem

(hf : HasFPowerSeriesAt f pf x) (hg : HasFPowerSeriesAt g pg x) : HasFPowerSeriesAt (f + g) (pf + pg) x

Full source

theorem HasFPowerSeriesAt.add (hf : HasFPowerSeriesAt f pf x) (hg : HasFPowerSeriesAt g pg x) :
    HasFPowerSeriesAt (f + g) (pf + pg) x := by
  rcases (hf.eventually.and hg.eventually).exists with ⟨r, hr⟩
  exact ⟨r, hr.1.add hr.2⟩

Sum of Power Series Expansions at a Point

Informal description

Let $f$ and $g$ be functions from a normed space $E$ to a normed space $F$ over a complete normed field $\mathbb{K}$. If $f$ has a formal power series expansion $pf$ at $x \in E$, and $g$ has a formal power series expansion $pg$ at $x$, then the sum $f + g$ has a formal power series expansion $pf + pg$ at $x$.

AnalyticWithinAt.add theorem

(hf : AnalyticWithinAt 𝕜 f s x) (hg : AnalyticWithinAt 𝕜 g s x) : AnalyticWithinAt 𝕜 (f + g) s x

Full source

theorem AnalyticWithinAt.add (hf : AnalyticWithinAt 𝕜 f s x) (hg : AnalyticWithinAt 𝕜 g s x) :
    AnalyticWithinAt 𝕜 (f + g) s x :=
  let ⟨_, hpf⟩ := hf
  let ⟨_, hqf⟩ := hg
  (hpf.add hqf).analyticWithinAt

Sum of Analytic Functions Within a Set is Analytic

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $s \subseteq E$. If $f$ and $g$ are analytic at $x \in s$ within $s$, then their sum $f + g$ is also analytic at $x$ within $s$.

AnalyticAt.fun_add theorem

(hf : AnalyticAt 𝕜 f x) (hg : AnalyticAt 𝕜 g x) : AnalyticAt 𝕜 (fun z ↦ f z + g z) x

Full source

@[fun_prop]
theorem AnalyticAt.fun_add (hf : AnalyticAt 𝕜 f x) (hg : AnalyticAt 𝕜 g x) :
    AnalyticAt 𝕜 (fun z ↦ f z + g z) x :=
  let ⟨_, hpf⟩ := hf
  let ⟨_, hqf⟩ := hg
  (hpf.add hqf).analyticAt

Pointwise Sum of Analytic Functions is Analytic

Informal description

Let $\mathbb{K}$ be a complete normed field, and let $E$ and $F$ be normed spaces over $\mathbb{K}$. If $f$ and $g$ are analytic at a point $x \in E$, then the function $z \mapsto f(z) + g(z)$ is also analytic at $x$.

AnalyticAt.add theorem

(hf : AnalyticAt 𝕜 f x) (hg : AnalyticAt 𝕜 g x) : AnalyticAt 𝕜 (f + g) x

Full source

@[fun_prop]
theorem AnalyticAt.add (hf : AnalyticAt 𝕜 f x) (hg : AnalyticAt 𝕜 g x) : AnalyticAt 𝕜 (f + g) x :=
  hf.fun_add hg

Sum of Analytic Functions is Analytic

Informal description

Let $\mathbb{K}$ be a complete normed field, and let $E$ and $F$ be normed spaces over $\mathbb{K}$. If $f$ and $g$ are analytic at a point $x \in E$, then their sum $f + g$ is also analytic at $x$.

HasFPowerSeriesWithinOnBall.neg theorem

(hf : HasFPowerSeriesWithinOnBall f pf s x r) : HasFPowerSeriesWithinOnBall (-f) (-pf) s x r

Full source

theorem HasFPowerSeriesWithinOnBall.neg (hf : HasFPowerSeriesWithinOnBall f pf s x r) :
    HasFPowerSeriesWithinOnBall (-f) (-pf) s x r :=
  { r_le := by
      rw [pf.radius_neg]
      exact hf.r_le
    r_pos := hf.r_pos
    hasSum := fun hy h'y => (hf.hasSum hy h'y).neg }

Negation Preserves Formal Power Series Expansion in a Ball

Informal description

Let $f$ be a function with a formal power series expansion $pf$ within a ball centered at $x$ with radius $r$ in a set $s$. Then the negation of $f$, denoted $-f$, has a formal power series expansion $-pf$ within the same ball.

HasFPowerSeriesOnBall.neg theorem

(hf : HasFPowerSeriesOnBall f pf x r) : HasFPowerSeriesOnBall (-f) (-pf) x r

Full source

theorem HasFPowerSeriesOnBall.neg (hf : HasFPowerSeriesOnBall f pf x r) :
    HasFPowerSeriesOnBall (-f) (-pf) x r :=
  { r_le := by
      rw [pf.radius_neg]
      exact hf.r_le
    r_pos := hf.r_pos
    hasSum := fun hy => (hf.hasSum hy).neg }

Negation Preserves Formal Power Series Expansion

Informal description

If a function $f$ has a formal power series expansion $pf$ centered at $x$ with radius of convergence $r$, then the negation of $f$, denoted $-f$, also has a formal power series expansion $-pf$ centered at $x$ with the same radius of convergence $r$.

HasFPowerSeriesWithinAt.neg theorem

(hf : HasFPowerSeriesWithinAt f pf s x) : HasFPowerSeriesWithinAt (-f) (-pf) s x

Full source

theorem HasFPowerSeriesWithinAt.neg (hf : HasFPowerSeriesWithinAt f pf s x) :
    HasFPowerSeriesWithinAt (-f) (-pf) s x :=
  let ⟨_, hrf⟩ := hf
  hrf.neg.hasFPowerSeriesWithinAt

Negation Preserves Formal Power Series Expansion at a Point

Informal description

Let $f$ be a function with a formal power series expansion $pf$ at a point $x$ within a set $s$. Then the negation of $f$, denoted $-f$, has a formal power series expansion $-pf$ at $x$ within the same set $s$.

HasFPowerSeriesAt.neg theorem

(hf : HasFPowerSeriesAt f pf x) : HasFPowerSeriesAt (-f) (-pf) x

Full source

theorem HasFPowerSeriesAt.neg (hf : HasFPowerSeriesAt f pf x) : HasFPowerSeriesAt (-f) (-pf) x :=
  let ⟨_, hrf⟩ := hf
  hrf.neg.hasFPowerSeriesAt

Negation Preserves Formal Power Series Expansion at a Point

Informal description

If a function $f$ has a formal power series expansion $pf$ at a point $x$, then the negation of $f$, denoted $-f$, has a formal power series expansion $-pf$ at the same point $x$.

AnalyticWithinAt.neg theorem

(hf : AnalyticWithinAt 𝕜 f s x) : AnalyticWithinAt 𝕜 (-f) s x

Full source

theorem AnalyticWithinAt.neg (hf : AnalyticWithinAt 𝕜 f s x) : AnalyticWithinAt 𝕜 (-f) s x :=
  let ⟨_, hpf⟩ := hf
  hpf.neg.analyticWithinAt

Negation Preserves Analyticity Within a Set at a Point

Informal description

Let $\mathbb{K}$ be a field, $f$ a function defined on a subset of $\mathbb{K}$, and $s$ a subset of the domain of $f$. If $f$ is analytic at a point $x$ within $s$, then the negation of $f$, denoted $-f$, is also analytic at $x$ within $s$.

AnalyticAt.fun_neg theorem

(hf : AnalyticAt 𝕜 f x) : AnalyticAt 𝕜 (fun z ↦ -f z) x

Full source

@[fun_prop]
theorem AnalyticAt.fun_neg (hf : AnalyticAt 𝕜 f x) : AnalyticAt 𝕜 (fun z ↦ -f z) x :=
  let ⟨_, hpf⟩ := hf
  hpf.neg.analyticAt

Negation Preserves Analyticity at a Point

Informal description

If a function $f$ is analytic at a point $x$ in a normed space over a field $\mathbb{K}$, then the function $z \mapsto -f(z)$ is also analytic at $x$.

AnalyticAt.neg theorem

(hf : AnalyticAt 𝕜 f x) : AnalyticAt 𝕜 (-f) x

Full source

@[fun_prop]
theorem AnalyticAt.neg (hf : AnalyticAt 𝕜 f x) : AnalyticAt 𝕜 (-f) x :=
  hf.fun_neg

Negation Preserves Analyticity at a Point

Informal description

If a function $f$ is analytic at a point $x$ in a normed space over a field $\mathbb{K}$, then the negation of $f$, denoted $-f$, is also analytic at $x$.

HasFPowerSeriesWithinOnBall.sub theorem

 (hf : HasFPowerSeriesWithinOnBall f pf s x r) (hg : HasFPowerSeriesWithinOnBall g pg s x r) :
  HasFPowerSeriesWithinOnBall (f - g) (pf - pg) s x r

Full source

theorem HasFPowerSeriesWithinOnBall.sub (hf : HasFPowerSeriesWithinOnBall f pf s x r)
    (hg : HasFPowerSeriesWithinOnBall g pg s x r) :
    HasFPowerSeriesWithinOnBall (f - g) (pf - pg) s x r := by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

Difference of Analytic Functions is Analytic on a Ball

Informal description

Let $f$ and $g$ be functions from a normed space $E$ to a normed space $F$ over a complete normed field $\mathbb{K}$. Suppose $f$ has a formal power series expansion $pf$ within a ball $B(x, r)$ around $x \in E$ and $g$ has a formal power series expansion $pg$ within the same ball. Then the difference $f - g$ has a formal power series expansion $pf - pg$ within the ball $B(x, r)$.

HasFPowerSeriesOnBall.sub theorem

 (hf : HasFPowerSeriesOnBall f pf x r) (hg : HasFPowerSeriesOnBall g pg x r) :
  HasFPowerSeriesOnBall (f - g) (pf - pg) x r

Full source

theorem HasFPowerSeriesOnBall.sub (hf : HasFPowerSeriesOnBall f pf x r)
    (hg : HasFPowerSeriesOnBall g pg x r) : HasFPowerSeriesOnBall (f - g) (pf - pg) x r := by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

Difference of Power Series Expansions on a Ball

Informal description

Let $f$ and $g$ be functions from a normed space $E$ to a normed space $F$ over a complete normed field $\mathbb{K}$. If $f$ has a formal power series expansion $pf$ centered at $x \in E$ with radius of convergence $r$, and $g$ has a formal power series expansion $pg$ centered at $x$ with the same radius of convergence $r$, then the difference $f - g$ has a formal power series expansion $pf - pg$ centered at $x$ with radius of convergence $r$.

HasFPowerSeriesWithinAt.sub theorem

 (hf : HasFPowerSeriesWithinAt f pf s x) (hg : HasFPowerSeriesWithinAt g pg s x) :
  HasFPowerSeriesWithinAt (f - g) (pf - pg) s x

Full source

theorem HasFPowerSeriesWithinAt.sub
    (hf : HasFPowerSeriesWithinAt f pf s x) (hg : HasFPowerSeriesWithinAt g pg s x) :
    HasFPowerSeriesWithinAt (f - g) (pf - pg) s x := by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

Difference of Analytic Functions is Analytic at a Point Within a Set

Informal description

Let $f$ and $g$ be functions from a normed space $E$ to a normed space $F$ over a complete normed field $\mathbb{K}$. Suppose $f$ has a formal power series expansion $pf$ at $x \in E$ within a set $s \subseteq E$, and $g$ has a formal power series expansion $pg$ at $x$ within the same set $s$. Then the difference $f - g$ has a formal power series expansion $pf - pg$ at $x$ within $s$.

HasFPowerSeriesAt.sub theorem

(hf : HasFPowerSeriesAt f pf x) (hg : HasFPowerSeriesAt g pg x) : HasFPowerSeriesAt (f - g) (pf - pg) x

Full source

theorem HasFPowerSeriesAt.sub (hf : HasFPowerSeriesAt f pf x) (hg : HasFPowerSeriesAt g pg x) :
    HasFPowerSeriesAt (f - g) (pf - pg) x := by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

Difference of Power Series Expansions at a Point

Informal description

Let $f$ and $g$ be functions from a normed space $E$ to a normed space $F$ over a complete normed field $\mathbb{K}$. If $f$ has a formal power series expansion $pf$ at $x \in E$, and $g$ has a formal power series expansion $pg$ at $x$, then the difference $f - g$ has a formal power series expansion $pf - pg$ at $x$.

AnalyticWithinAt.sub theorem

(hf : AnalyticWithinAt 𝕜 f s x) (hg : AnalyticWithinAt 𝕜 g s x) : AnalyticWithinAt 𝕜 (f - g) s x

Full source

theorem AnalyticWithinAt.sub (hf : AnalyticWithinAt 𝕜 f s x) (hg : AnalyticWithinAt 𝕜 g s x) :
    AnalyticWithinAt 𝕜 (f - g) s x := by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

Difference of Analytic Functions Within a Set is Analytic

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $s \subseteq E$. If $f$ and $g$ are analytic at $x \in s$ within $s$, then their difference $f - g$ is also analytic at $x$ within $s$.

AnalyticAt.fun_sub theorem

(hf : AnalyticAt 𝕜 f x) (hg : AnalyticAt 𝕜 g x) : AnalyticAt 𝕜 (fun z ↦ f z - g z) x

Full source

@[fun_prop]
theorem AnalyticAt.fun_sub (hf : AnalyticAt 𝕜 f x) (hg : AnalyticAt 𝕜 g x) :
    AnalyticAt 𝕜 (fun z ↦ f z - g z) x := by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

Pointwise Difference of Analytic Functions is Analytic

Informal description

Let $\mathbb{K}$ be a complete normed field, and let $E$ and $F$ be normed spaces over $\mathbb{K}$. If $f$ and $g$ are analytic at a point $x \in E$, then the function $z \mapsto f(z) - g(z)$ is also analytic at $x$.

AnalyticAt.sub theorem

(hf : AnalyticAt 𝕜 f x) (hg : AnalyticAt 𝕜 g x) : AnalyticAt 𝕜 (f - g) x

Full source

@[fun_prop]
theorem AnalyticAt.sub (hf : AnalyticAt 𝕜 f x) (hg : AnalyticAt 𝕜 g x) :
    AnalyticAt 𝕜 (f - g) x :=
  hf.fun_sub hg

Difference of Analytic Functions is Analytic at a Point

Informal description

Let $\mathbb{K}$ be a complete normed field, and let $E$ and $F$ be normed spaces over $\mathbb{K}$. If $f$ and $g$ are analytic at a point $x \in E$, then their difference $f - g$ is also analytic at $x$.

HasFPowerSeriesWithinOnBall.const_smul theorem

(hf : HasFPowerSeriesWithinOnBall f pf s x r) : HasFPowerSeriesWithinOnBall (c • f) (c • pf) s x r

Full source

theorem HasFPowerSeriesWithinOnBall.const_smul (hf : HasFPowerSeriesWithinOnBall f pf s x r) :
    HasFPowerSeriesWithinOnBall (c • f) (c • pf) s x r where
  r_le := le_trans hf.r_le pf.radius_le_smul
  r_pos := hf.r_pos
  hasSum := fun hy h'y => (hf.hasSum hy h'y).const_smul _

Scalar Multiplication Preserves Power Series Expansion Within a Ball

Informal description

Let $f$ be a function with a formal power series expansion $pf$ within a ball centered at $x$ with radius $r$ and domain $s$. Then for any scalar $c$, the function $c \cdot f$ has a formal power series expansion $c \cdot pf$ within the same ball centered at $x$ with radius $r$ and domain $s$.

HasFPowerSeriesOnBall.const_smul theorem

(hf : HasFPowerSeriesOnBall f pf x r) : HasFPowerSeriesOnBall (c • f) (c • pf) x r

Full source

theorem HasFPowerSeriesOnBall.const_smul (hf : HasFPowerSeriesOnBall f pf x r) :
    HasFPowerSeriesOnBall (c • f) (c • pf) x r where
  r_le := le_trans hf.r_le pf.radius_le_smul
  r_pos := hf.r_pos
  hasSum := fun hy => (hf.hasSum hy).const_smul _

Scalar Multiplication Preserves Power Series Expansion and Radius of Convergence

Informal description

Let $f$ be a function with a formal power series expansion $pf$ centered at $x$ with radius of convergence $r$. Then for any scalar $c$, the function $c \cdot f$ has a formal power series expansion $c \cdot pf$ centered at $x$ with the same radius of convergence $r$.

HasFPowerSeriesWithinAt.const_smul theorem

(hf : HasFPowerSeriesWithinAt f pf s x) : HasFPowerSeriesWithinAt (c • f) (c • pf) s x

Full source

theorem HasFPowerSeriesWithinAt.const_smul (hf : HasFPowerSeriesWithinAt f pf s x) :
    HasFPowerSeriesWithinAt (c • f) (c • pf) s x :=
  let ⟨_, hrf⟩ := hf
  hrf.const_smul.hasFPowerSeriesWithinAt

Scalar Multiplication Preserves Power Series Expansion at a Point Within a Set

Informal description

Let $f$ be a function with a formal power series expansion $pf$ at a point $x$ within a set $s$. Then for any scalar $c$, the function $c \cdot f$ has a formal power series expansion $c \cdot pf$ at $x$ within the same set $s$.

HasFPowerSeriesAt.const_smul theorem

(hf : HasFPowerSeriesAt f pf x) : HasFPowerSeriesAt (c • f) (c • pf) x

Full source

theorem HasFPowerSeriesAt.const_smul (hf : HasFPowerSeriesAt f pf x) :
    HasFPowerSeriesAt (c • f) (c • pf) x :=
  let ⟨_, hrf⟩ := hf
  hrf.const_smul.hasFPowerSeriesAt

Scalar Multiplication Preserves Power Series Expansion at a Point

Informal description

Let $f$ be a function with a formal power series expansion $pf$ at a point $x$. Then for any scalar $c$, the function $c \cdot f$ has a formal power series expansion $c \cdot pf$ at the same point $x$.

AnalyticWithinAt.const_smul theorem

(hf : AnalyticWithinAt 𝕜 f s x) : AnalyticWithinAt 𝕜 (c • f) s x

Full source

theorem AnalyticWithinAt.const_smul (hf : AnalyticWithinAt 𝕜 f s x) :
    AnalyticWithinAt 𝕜 (c • f) s x :=
  let ⟨_, hpf⟩ := hf
  hpf.const_smul.analyticWithinAt

Scalar Multiplication Preserves Analyticity Within a Set at a Point

Informal description

Let $\mathbb{K}$ be a field, $f$ be a function, and $s$ be a set. If $f$ is analytic at a point $x$ within $s$ over $\mathbb{K}$, then for any scalar $c \in \mathbb{K}$, the function $c \cdot f$ is also analytic at $x$ within $s$ over $\mathbb{K}$.

AnalyticAt.fun_const_smul theorem

(hf : AnalyticAt 𝕜 f x) : AnalyticAt 𝕜 (fun z ↦ c • f z) x

Full source

@[fun_prop]
theorem AnalyticAt.fun_const_smul (hf : AnalyticAt 𝕜 f x) : AnalyticAt 𝕜 (fun z ↦ c • f z) x :=
  let ⟨_, hpf⟩ := hf
  hpf.const_smul.analyticAt

Scalar Multiplication Preserves Analyticity at a Point

Informal description

Let $f$ be a function that is analytic at a point $x$ in a field $\mathbb{K}$. Then for any scalar $c$, the function $z \mapsto c \cdot f(z)$ is also analytic at $x$.

AnalyticAt.const_smul theorem

(hf : AnalyticAt 𝕜 f x) : AnalyticAt 𝕜 (c • f) x

Full source

@[fun_prop]
theorem AnalyticAt.const_smul (hf : AnalyticAt 𝕜 f x) : AnalyticAt 𝕜 (c • f) x :=
  hf.fun_const_smul

Scalar Multiplication Preserves Analyticity at a Point

Informal description

Let $f$ be a function that is analytic at a point $x$ in a field $\mathbb{K}$. Then for any scalar $c \in \mathbb{K}$, the function $c \cdot f$ is also analytic at $x$.

AnalyticOn.add theorem

(hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) : AnalyticOn 𝕜 (f + g) s

Full source

theorem AnalyticOn.add (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) :
    AnalyticOn 𝕜 (f + g) s :=
  fun z hz => (hf z hz).add (hg z hz)

Sum of Analytic Functions on a Set is Analytic

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $s \subseteq E$. If $f$ and $g$ are analytic on $s$, then their sum $f + g$ is also analytic on $s$.

AnalyticOnNhd.add theorem

(hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOnNhd 𝕜 g s) : AnalyticOnNhd 𝕜 (f + g) s

Full source

theorem AnalyticOnNhd.add (hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOnNhd 𝕜 g s) :
    AnalyticOnNhd 𝕜 (f + g) s :=
  fun z hz => (hf z hz).add (hg z hz)

Sum of Locally Analytic Functions is Locally Analytic

Informal description

Let $\mathbb{K}$ be a complete normed field, and let $E$ and $F$ be normed spaces over $\mathbb{K}$. If $f$ and $g$ are analytic in a neighborhood of a set $s \subseteq E$, then their sum $f + g$ is also analytic in a neighborhood of $s$.

AnalyticOn.neg theorem

(hf : AnalyticOn 𝕜 f s) : AnalyticOn 𝕜 (-f) s

Full source

theorem AnalyticOn.neg (hf : AnalyticOn 𝕜 f s) : AnalyticOn 𝕜 (-f) s :=
  fun z hz ↦ (hf z hz).neg

Negation Preserves Analyticity on a Set

Informal description

Let $\mathbb{K}$ be a field, $f$ a function defined on a subset of $\mathbb{K}$, and $s$ a subset of the domain of $f$. If $f$ is analytic on $s$, then the negation of $f$, denoted $-f$, is also analytic on $s$.

AnalyticOnNhd.neg theorem

(hf : AnalyticOnNhd 𝕜 f s) : AnalyticOnNhd 𝕜 (-f) s

Full source

theorem AnalyticOnNhd.neg (hf : AnalyticOnNhd 𝕜 f s) : AnalyticOnNhd 𝕜 (-f) s :=
  fun z hz ↦ (hf z hz).neg

Negation Preserves Analyticity on a Neighborhood

Informal description

If a function $f$ is analytic on a neighborhood $s$ of a point in a normed space over a field $\mathbb{K}$, then the negation of $f$, denoted $-f$, is also analytic on $s$.

AnalyticOn.sub theorem

(hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) : AnalyticOn 𝕜 (f - g) s

Full source

theorem AnalyticOn.sub (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) :
    AnalyticOn 𝕜 (f - g) s :=
  fun z hz => (hf z hz).sub (hg z hz)

Difference of Analytic Functions on a Set is Analytic

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $s \subseteq E$. If $f, g : E \to F$ are analytic on $s$, then their difference $f - g$ is also analytic on $s$.

AnalyticOnNhd.sub theorem

(hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOnNhd 𝕜 g s) : AnalyticOnNhd 𝕜 (f - g) s

Full source

theorem AnalyticOnNhd.sub (hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOnNhd 𝕜 g s) :
    AnalyticOnNhd 𝕜 (f - g) s :=
  fun z hz => (hf z hz).sub (hg z hz)

Difference of Analytic Functions on a Neighborhood is Analytic

Informal description

Let $\mathbb{K}$ be a complete normed field, and let $E$ and $F$ be normed spaces over $\mathbb{K}$. If $f$ and $g$ are analytic on a neighborhood $s$ of a point in $E$, then their difference $f - g$ is also analytic on $s$.

FormalMultilinearSeries.radius_prod_eq_min theorem

 (p : FormalMultilinearSeries 𝕜 E F) (q : FormalMultilinearSeries 𝕜 E G) : (p.prod q).radius = min p.radius q.radius

Full source

/-- The radius of the Cartesian product of two formal series is the minimum of their radii. -/
lemma FormalMultilinearSeries.radius_prod_eq_min
    (p : FormalMultilinearSeries 𝕜 E F) (q : FormalMultilinearSeries 𝕜 E G) :
    (p.prod q).radius = min p.radius q.radius := by
  apply le_antisymm
  · refine ENNReal.le_of_forall_nnreal_lt fun r hr => ?_
    rw [le_min_iff]
    have := (p.prod q).isLittleO_one_of_lt_radius hr
    constructor
    all_goals
      apply FormalMultilinearSeries.le_radius_of_isBigO
      refine (isBigO_of_le _ fun n ↦ ?_).trans this.isBigO
      rw [norm_mul, norm_norm, norm_mul, norm_norm]
      refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
      rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.opNorm_prod]
    · apply le_max_left
    · apply le_max_right
  · refine ENNReal.le_of_forall_nnreal_lt fun r hr => ?_
    rw [lt_min_iff] at hr
    have := ((p.isLittleO_one_of_lt_radius hr.1).add
      (q.isLittleO_one_of_lt_radius hr.2)).isBigO
    refine (p.prod q).le_radius_of_isBigO ((isBigO_of_le _ fun n ↦ ?_).trans this)
    rw [norm_mul, norm_norm, ← add_mul, norm_mul]
    refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
    rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.opNorm_prod]
    refine (max_le_add_of_nonneg (norm_nonneg _) (norm_nonneg _)).trans ?_
    apply Real.le_norm_self

Radius of Product of Formal Multilinear Series is Minimum of Radii

Informal description

Let $\mathbb{K}$ be a complete normed field, and let $E$, $F$, and $G$ be normed spaces over $\mathbb{K}$. For any formal multilinear series $p$ from $E$ to $F$ and $q$ from $E$ to $G$, the radius of convergence of the Cartesian product series $p \times q$ is the minimum of the radii of convergence of $p$ and $q$, i.e., \[ \text{radius}(p \times q) = \min(\text{radius}(p), \text{radius}(q)). \]

HasFPowerSeriesWithinOnBall.prod theorem

 {e : E} {f : E → F} {g : E → G} {r s : ℝ≥0∞} {t : Set E} {p : FormalMultilinearSeries 𝕜 E F}
  {q : FormalMultilinearSeries 𝕜 E G} (hf : HasFPowerSeriesWithinOnBall f p t e r)
  (hg : HasFPowerSeriesWithinOnBall g q t e s) :
  HasFPowerSeriesWithinOnBall (fun x ↦ (f x, g x)) (p.prod q) t e (min r s)

Full source

lemma HasFPowerSeriesWithinOnBall.prod {e : E} {f : E → F} {g : E → G} {r s : ℝ≥0∞} {t : Set E}
    {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜 E G}
    (hf : HasFPowerSeriesWithinOnBall f p t e r) (hg : HasFPowerSeriesWithinOnBall g q t e s) :
    HasFPowerSeriesWithinOnBall (fun x ↦ (f x, g x)) (p.prod q) t e (min r s) where
  r_le := by
    rw [p.radius_prod_eq_min]
    exact min_le_min hf.r_le hg.r_le
  r_pos := lt_min hf.r_pos hg.r_pos
  hasSum := by
    intro y h'y hy
    simp_rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.prod_apply]
    refine (hf.hasSum h'y ?_).prodMk (hg.hasSum h'y ?_)
    · exact EMetric.mem_ball.mpr (lt_of_lt_of_le hy (min_le_left _ _))
    · exact EMetric.mem_ball.mpr (lt_of_lt_of_le hy (min_le_right _ _))

Product of Functions with Power Series Expansions Has Combined Expansion with Minimum Radius

Informal description

Let $\mathbb{K}$ be a complete normed field, and let $E$, $F$, and $G$ be normed spaces over $\mathbb{K}$. Given functions $f \colon E \to F$ and $g \colon E \to G$ with formal power series expansions $p$ and $q$ respectively, centered at a point $e \in E$ and valid within a ball of radius $r$ and $s$ respectively, the Cartesian product function $x \mapsto (f(x), g(x))$ has a formal power series expansion given by the product series $p \times q$. This expansion is valid within the same domain $t \subseteq E$ and centered at $e$, with a radius of convergence equal to the minimum of $r$ and $s$.

HasFPowerSeriesOnBall.prod theorem

 {e : E} {f : E → F} {g : E → G} {r s : ℝ≥0∞} {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜 E G}
  (hf : HasFPowerSeriesOnBall f p e r) (hg : HasFPowerSeriesOnBall g q e s) :
  HasFPowerSeriesOnBall (fun x ↦ (f x, g x)) (p.prod q) e (min r s)

Full source

lemma HasFPowerSeriesOnBall.prod {e : E} {f : E → F} {g : E → G} {r s : ℝ≥0∞}
    {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜 E G}
    (hf : HasFPowerSeriesOnBall f p e r) (hg : HasFPowerSeriesOnBall g q e s) :
    HasFPowerSeriesOnBall (fun x ↦ (f x, g x)) (p.prod q) e (min r s) := by
  rw [← hasFPowerSeriesWithinOnBall_univ] at hf hg ⊢
  exact hf.prod hg

Product of Analytic Functions is Analytic with Minimum Radius of Convergence

Informal description

Let $\mathbb{K}$ be a complete normed field, and let $E$, $F$, and $G$ be normed spaces over $\mathbb{K}$. Suppose $f \colon E \to F$ and $g \colon E \to G$ have formal power series expansions $p$ and $q$ centered at $e \in E$, converging on balls of radii $r$ and $s$ respectively. Then the product function $x \mapsto (f(x), g(x))$ has a formal power series expansion given by the product series $p \times q$, centered at $e$ with radius of convergence $\min(r, s)$.

HasFPowerSeriesWithinAt.prod theorem

 {e : E} {f : E → F} {g : E → G} {s : Set E} {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜 E G}
  (hf : HasFPowerSeriesWithinAt f p s e) (hg : HasFPowerSeriesWithinAt g q s e) :
  HasFPowerSeriesWithinAt (fun x ↦ (f x, g x)) (p.prod q) s e

Full source

lemma HasFPowerSeriesWithinAt.prod {e : E} {f : E → F} {g : E → G} {s : Set E}
    {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜 E G}
    (hf : HasFPowerSeriesWithinAt f p s e) (hg : HasFPowerSeriesWithinAt g q s e) :
    HasFPowerSeriesWithinAt (fun x ↦ (f x, g x)) (p.prod q) s e := by
  rcases hf with ⟨_, hf⟩
  rcases hg with ⟨_, hg⟩
  exact ⟨_, hf.prod hg⟩

Product of Functions with Power Series Expansions at a Point Has Combined Expansion

Informal description

Let $\mathbb{K}$ be a complete normed field, and let $E$, $F$, and $G$ be normed spaces over $\mathbb{K}$. Given functions $f \colon E \to F$ and $g \colon E \to G$ with formal power series expansions $p$ and $q$ respectively, centered at a point $e \in E$ and valid within a set $s \subseteq E$, the Cartesian product function $x \mapsto (f(x), g(x))$ has a formal power series expansion given by the product series $p \times q$. This expansion is valid within the same domain $s$ and centered at $e$.

HasFPowerSeriesAt.prod theorem

 {e : E} {f : E → F} {g : E → G} {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜 E G}
  (hf : HasFPowerSeriesAt f p e) (hg : HasFPowerSeriesAt g q e) : HasFPowerSeriesAt (fun x ↦ (f x, g x)) (p.prod q) e

Full source

lemma HasFPowerSeriesAt.prod {e : E} {f : E → F} {g : E → G}
    {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜 E G}
    (hf : HasFPowerSeriesAt f p e) (hg : HasFPowerSeriesAt g q e) :
    HasFPowerSeriesAt (fun x ↦ (f x, g x)) (p.prod q) e := by
  rcases hf with ⟨_, hf⟩
  rcases hg with ⟨_, hg⟩
  exact ⟨_, hf.prod hg⟩

Product of Analytic Functions at a Point is Analytic with Combined Power Series

Informal description

Let $\mathbb{K}$ be a complete normed field, and let $E$, $F$, and $G$ be normed spaces over $\mathbb{K}$. Given functions $f \colon E \to F$ and $g \colon E \to G$ with formal power series expansions $p$ and $q$ respectively, centered at a point $e \in E$, the Cartesian product function $x \mapsto (f(x), g(x))$ has a formal power series expansion given by the product series $p \times q$, also centered at $e$.

AnalyticWithinAt.prod theorem

 {e : E} {f : E → F} {g : E → G} {s : Set E} (hf : AnalyticWithinAt 𝕜 f s e) (hg : AnalyticWithinAt 𝕜 g s e) :
  AnalyticWithinAt 𝕜 (fun x ↦ (f x, g x)) s e

Full source

/-- The Cartesian product of analytic functions is analytic. -/
lemma AnalyticWithinAt.prod {e : E} {f : E → F} {g : E → G} {s : Set E}
    (hf : AnalyticWithinAt 𝕜 f s e) (hg : AnalyticWithinAt 𝕜 g s e) :
    AnalyticWithinAt 𝕜 (fun x ↦ (f x, g x)) s e := by
  rcases hf with ⟨_, hf⟩
  rcases hg with ⟨_, hg⟩
  exact ⟨_, hf.prod hg⟩

Analyticity of Cartesian Product of Functions

Informal description

Let $\mathbb{K}$ be a complete normed field, and let $E$, $F$, and $G$ be normed spaces over $\mathbb{K}$. Given functions $f \colon E \to F$ and $g \colon E \to G$ that are analytic at a point $e \in E$ within a set $s \subseteq E$, the Cartesian product function $x \mapsto (f(x), g(x))$ is also analytic at $e$ within $s$.

AnalyticAt.prod theorem

 {e : E} {f : E → F} {g : E → G} (hf : AnalyticAt 𝕜 f e) (hg : AnalyticAt 𝕜 g e) : AnalyticAt 𝕜 (fun x ↦ (f x, g x)) e

Full source

/-- The Cartesian product of analytic functions is analytic. -/
@[fun_prop]
lemma AnalyticAt.prod {e : E} {f : E → F} {g : E → G}
    (hf : AnalyticAt 𝕜 f e) (hg : AnalyticAt 𝕜 g e) :
    AnalyticAt 𝕜 (fun x ↦ (f x, g x)) e := by
  rcases hf with ⟨_, hf⟩
  rcases hg with ⟨_, hg⟩
  exact ⟨_, hf.prod hg⟩

Analyticity of Cartesian Product of Functions at a Point

Informal description

Let $\mathbb{K}$ be a complete normed field, and let $E$, $F$, and $G$ be normed spaces over $\mathbb{K}$. Given functions $f \colon E \to F$ and $g \colon E \to G$ that are analytic at a point $e \in E$, the Cartesian product function $x \mapsto (f(x), g(x))$ is also analytic at $e$.

AnalyticOn.prod theorem

 {f : E → F} {g : E → G} {s : Set E} (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) :
  AnalyticOn 𝕜 (fun x ↦ (f x, g x)) s

Full source

/-- The Cartesian product of analytic functions within a set is analytic. -/
lemma AnalyticOn.prod {f : E → F} {g : E → G} {s : Set E}
    (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) :
    AnalyticOn 𝕜 (fun x ↦ (f x, g x)) s :=
  fun x hx ↦ (hf x hx).prod (hg x hx)

Analyticity of Cartesian Product of Functions on a Set

Informal description

Let $\mathbb{K}$ be a complete normed field, and let $E$, $F$, and $G$ be normed spaces over $\mathbb{K}$. Given functions $f \colon E \to F$ and $g \colon E \to G$ that are analytic on a set $s \subseteq E$, the Cartesian product function $x \mapsto (f(x), g(x))$ is also analytic on $s$.

AnalyticOnNhd.prod theorem

 {f : E → F} {g : E → G} {s : Set E} (hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOnNhd 𝕜 g s) :
  AnalyticOnNhd 𝕜 (fun x ↦ (f x, g x)) s

Full source

/-- The Cartesian product of analytic functions is analytic. -/
lemma AnalyticOnNhd.prod {f : E → F} {g : E → G} {s : Set E}
    (hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOnNhd 𝕜 g s) :
    AnalyticOnNhd 𝕜 (fun x ↦ (f x, g x)) s :=
  fun x hx ↦ (hf x hx).prod (hg x hx)

Analyticity of Cartesian Product of Functions on Neighborhoods

Informal description

Let $\mathbb{K}$ be a complete normed field, and let $E$, $F$, and $G$ be normed spaces over $\mathbb{K}$. Given functions $f \colon E \to F$ and $g \colon E \to G$ that are analytic in a neighborhood of each point in a set $s \subseteq E$, the Cartesian product function $x \mapsto (f(x), g(x))$ is also analytic in a neighborhood of each point in $s$.

AnalyticAt.comp₂ theorem

 {h : F × G → H} {f : E → F} {g : E → G} {x : E} (ha : AnalyticAt 𝕜 h (f x, g x)) (fa : AnalyticAt 𝕜 f x)
  (ga : AnalyticAt 𝕜 g x) : AnalyticAt 𝕜 (fun x ↦ h (f x, g x)) x

Full source

/-- `AnalyticAt.comp` for functions on product spaces -/
theorem AnalyticAt.comp₂ {h : F × G → H} {f : E → F} {g : E → G} {x : E}
    (ha : AnalyticAt 𝕜 h (f x, g x)) (fa : AnalyticAt 𝕜 f x)
    (ga : AnalyticAt 𝕜 g x) :
    AnalyticAt 𝕜 (fun x ↦ h (f x, g x)) x :=
  AnalyticAt.comp ha (fa.prod ga)

Analyticity of Composition of Two Functions on Product Spaces at a Point

Informal description

Let $\mathbb{K}$ be a complete normed field, and let $E$, $F$, $G$, and $H$ be normed spaces over $\mathbb{K}$. Given functions $f \colon E \to F$ and $g \colon E \to G$ that are analytic at a point $x \in E$, and a function $h \colon F \times G \to H$ that is analytic at $(f(x), g(x))$, the composition $x \mapsto h(f(x), g(x))$ is also analytic at $x$.

AnalyticWithinAt.comp₂ theorem

 {h : F × G → H} {f : E → F} {g : E → G} {s : Set (F × G)} {t : Set E} {x : E} (ha : AnalyticWithinAt 𝕜 h s (f x, g x))
  (fa : AnalyticWithinAt 𝕜 f t x) (ga : AnalyticWithinAt 𝕜 g t x) (hf : Set.MapsTo (fun y ↦ (f y, g y)) t s) :
  AnalyticWithinAt 𝕜 (fun x ↦ h (f x, g x)) t x

Full source

/-- `AnalyticWithinAt.comp` for functions on product spaces -/
theorem AnalyticWithinAt.comp₂ {h : F × G → H} {f : E → F} {g : E → G} {s : Set (F × G)}
    {t : Set E} {x : E}
    (ha : AnalyticWithinAt 𝕜 h s (f x, g x)) (fa : AnalyticWithinAt 𝕜 f t x)
    (ga : AnalyticWithinAt 𝕜 g t x) (hf : Set.MapsTo (fun y ↦ (f y, g y)) t s) :
    AnalyticWithinAt 𝕜 (fun x ↦ h (f x, g x)) t x :=
  AnalyticWithinAt.comp ha (fa.prod ga) hf

Analyticity of Composition of Two Functions Within a Set

Informal description

Let $\mathbb{K}$ be a complete normed field, and let $E$, $F$, $G$, and $H$ be normed spaces over $\mathbb{K}$. Given functions $h \colon F \times G \to H$, $f \colon E \to F$, and $g \colon E \to G$, suppose that: 1. $h$ is analytic at $(f(x), g(x))$ within a set $s \subseteq F \times G$, 2. $f$ and $g$ are analytic at $x$ within a set $t \subseteq E$, 3. The map $y \mapsto (f(y), g(y))$ sends $t$ into $s$. Then the composition $x \mapsto h(f(x), g(x))$ is analytic at $x$ within $t$.

AnalyticAt.comp₂_analyticWithinAt theorem

 {h : F × G → H} {f : E → F} {g : E → G} {x : E} {s : Set E} (ha : AnalyticAt 𝕜 h (f x, g x))
  (fa : AnalyticWithinAt 𝕜 f s x) (ga : AnalyticWithinAt 𝕜 g s x) : AnalyticWithinAt 𝕜 (fun x ↦ h (f x, g x)) s x

Full source

/-- `AnalyticAt.comp_analyticWithinAt` for functions on product spaces -/
theorem AnalyticAt.comp₂_analyticWithinAt
    {h : F × G → H} {f : E → F} {g : E → G} {x : E} {s : Set E}
    (ha : AnalyticAt 𝕜 h (f x, g x)) (fa : AnalyticWithinAt 𝕜 f s x)
    (ga : AnalyticWithinAt 𝕜 g s x) :
    AnalyticWithinAt 𝕜 (fun x ↦ h (f x, g x)) s x :=
  AnalyticAt.comp_analyticWithinAt ha (fa.prod ga)

Analyticity of Composition with Two Functions on Product Spaces

Informal description

Let $\mathbb{K}$ be a complete normed field, and let $E$, $F$, $G$, and $H$ be normed spaces over $\mathbb{K}$. Given functions $f \colon E \to F$ and $g \colon E \to G$ that are analytic at a point $x \in E$ within a set $s \subseteq E$, and a function $h \colon F \times G \to H$ that is analytic at $(f(x), g(x))$, the composition $x \mapsto h(f(x), g(x))$ is analytic at $x$ within $s$.

AnalyticOnNhd.comp₂ theorem

 {h : F × G → H} {f : E → F} {g : E → G} {s : Set (F × G)} {t : Set E} (ha : AnalyticOnNhd 𝕜 h s)
  (fa : AnalyticOnNhd 𝕜 f t) (ga : AnalyticOnNhd 𝕜 g t) (m : ∀ x, x ∈ t → (f x, g x) ∈ s) :
  AnalyticOnNhd 𝕜 (fun x ↦ h (f x, g x)) t

Full source

/-- `AnalyticOnNhd.comp` for functions on product spaces -/
theorem AnalyticOnNhd.comp₂ {h : F × G → H} {f : E → F} {g : E → G} {s : Set (F × G)} {t : Set E}
    (ha : AnalyticOnNhd 𝕜 h s) (fa : AnalyticOnNhd 𝕜 f t) (ga : AnalyticOnNhd 𝕜 g t)
    (m : ∀ x, x ∈ t → (f x, g x)(f x, g x) ∈ s) : AnalyticOnNhd 𝕜 (fun x ↦ h (f x, g x)) t :=
  fun _ xt ↦ (ha _ (m _ xt)).comp₂ (fa _ xt) (ga _ xt)

Analyticity of Composition of Two Functions on Product Spaces in Neighborhoods

Informal description

Let $\mathbb{K}$ be a complete normed field, and let $E$, $F$, $G$, and $H$ be normed spaces over $\mathbb{K}$. Given functions $h \colon F \times G \to H$, $f \colon E \to F$, and $g \colon E \to G$, suppose that: 1. $h$ is analytic on a neighborhood $s$ of $(f(x), g(x))$ for all $x \in t$, 2. $f$ and $g$ are analytic on a neighborhood $t$ of $x$, 3. For every $x \in t$, the pair $(f(x), g(x))$ lies in $s$. Then the composition $x \mapsto h(f(x), g(x))$ is analytic on the neighborhood $t$.

AnalyticOn.comp₂ theorem

 {h : F × G → H} {f : E → F} {g : E → G} {s : Set (F × G)} {t : Set E} (ha : AnalyticOn 𝕜 h s) (fa : AnalyticOn 𝕜 f t)
  (ga : AnalyticOn 𝕜 g t) (m : Set.MapsTo (fun y ↦ (f y, g y)) t s) : AnalyticOn 𝕜 (fun x ↦ h (f x, g x)) t

Full source

/-- `AnalyticOn.comp` for functions on product spaces -/
theorem AnalyticOn.comp₂ {h : F × G → H} {f : E → F} {g : E → G} {s : Set (F × G)}
    {t : Set E}
    (ha : AnalyticOn 𝕜 h s) (fa : AnalyticOn 𝕜 f t)
    (ga : AnalyticOn 𝕜 g t) (m : Set.MapsTo (fun y ↦ (f y, g y)) t s) :
    AnalyticOn 𝕜 (fun x ↦ h (f x, g x)) t :=
  fun x hx ↦ (ha _ (m hx)).comp₂ (fa x hx) (ga x hx) m

Analyticity of Composition of Two Analytic Functions on Product Spaces

Informal description

Let $\mathbb{K}$ be a complete normed field, and let $E$, $F$, $G$, and $H$ be normed spaces over $\mathbb{K}$. Given functions $h \colon F \times G \to H$, $f \colon E \to F$, and $g \colon E \to G$, suppose that: 1. $h$ is analytic on a set $s \subseteq F \times G$, 2. $f$ and $g$ are analytic on a set $t \subseteq E$, 3. The map $y \mapsto (f(y), g(y))$ sends $t$ into $s$. Then the composition $x \mapsto h(f(x), g(x))$ is analytic on $t$.

AnalyticAt.curry_left theorem

{f : E × F → G} {p : E × F} (fa : AnalyticAt 𝕜 f p) : AnalyticAt 𝕜 (fun x ↦ f (x, p.2)) p.1

Full source

/-- Analytic functions on products are analytic in the first coordinate -/
theorem AnalyticAt.curry_left {f : E × F → G} {p : E × F} (fa : AnalyticAt 𝕜 f p) :
    AnalyticAt 𝕜 (fun x ↦ f (x, p.2)) p.1 :=
  AnalyticAt.comp₂ fa analyticAt_id analyticAt_const

Analyticity of Left Curry of Analytic Function at a Point

Informal description

Let $E$, $F$, and $G$ be normed spaces over a complete normed field $\mathbb{K}$, and let $f \colon E \times F \to G$ be a function. Given a point $p = (p_1, p_2) \in E \times F$, if $f$ is analytic at $p$, then the function $x \mapsto f(x, p_2)$ is analytic at $p_1$.

AnalyticWithinAt.curry_left theorem

 {f : E × F → G} {s : Set (E × F)} {p : E × F} (fa : AnalyticWithinAt 𝕜 f s p) :
  AnalyticWithinAt 𝕜 (fun x ↦ f (x, p.2)) {x | (x, p.2) ∈ s} p.1

Full source

theorem AnalyticWithinAt.curry_left
    {f : E × F → G} {s : Set (E × F)} {p : E × F} (fa : AnalyticWithinAt 𝕜 f s p) :
    AnalyticWithinAt 𝕜 (fun x ↦ f (x, p.2)) {x | (x, p.2) ∈ s} p.1 :=
  AnalyticWithinAt.comp₂ fa analyticWithinAt_id analyticWithinAt_const (fun _ hx ↦ hx)

Analyticity of Left Curry of Analytic Function Within a Set at a Point

Informal description

Let $E$, $F$, and $G$ be normed spaces over a complete normed field $\mathbb{K}$, and let $f \colon E \times F \to G$ be a function. Given a set $s \subseteq E \times F$ and a point $p = (p_1, p_2) \in E \times F$, if $f$ is analytic at $p$ within $s$, then the function $x \mapsto f(x, p_2)$ is analytic at $p_1$ within the set $\{x \in E \mid (x, p_2) \in s\}$.

AnalyticAt.curry_right theorem

{f : E × F → G} {p : E × F} (fa : AnalyticAt 𝕜 f p) : AnalyticAt 𝕜 (fun y ↦ f (p.1, y)) p.2

Full source

/-- Analytic functions on products are analytic in the second coordinate -/
theorem AnalyticAt.curry_right {f : E × F → G} {p : E × F} (fa : AnalyticAt 𝕜 f p) :
    AnalyticAt 𝕜 (fun y ↦ f (p.1, y)) p.2 :=
  AnalyticAt.comp₂ fa analyticAt_const analyticAt_id

Analyticity of Partial Application in the Second Variable at a Point

Informal description

Let $E$, $F$, and $G$ be normed spaces over a complete normed field $\mathbb{K}$. Given a function $f \colon E \times F \to G$ that is analytic at a point $p = (p_1, p_2) \in E \times F$, the function $y \mapsto f(p_1, y)$ is analytic at $p_2$.

AnalyticWithinAt.curry_right theorem

 {f : E × F → G} {s : Set (E × F)} {p : E × F} (fa : AnalyticWithinAt 𝕜 f s p) :
  AnalyticWithinAt 𝕜 (fun y ↦ f (p.1, y)) {y | (p.1, y) ∈ s} p.2

Full source

theorem AnalyticWithinAt.curry_right
    {f : E × F → G} {s : Set (E × F)} {p : E × F} (fa : AnalyticWithinAt 𝕜 f s p) :
    AnalyticWithinAt 𝕜 (fun y ↦ f (p.1, y)) {y | (p.1, y) ∈ s} p.2 :=
  AnalyticWithinAt.comp₂ fa  analyticWithinAt_const analyticWithinAt_id (fun _ hx ↦ hx)

Analyticity of Partial Application in the Second Variable Within a Set

Informal description

Let $E$, $F$, and $G$ be normed spaces over a complete normed field $\mathbb{K}$. Given a function $f \colon E \times F \to G$ that is analytic within a set $s \subseteq E \times F$ at a point $p = (p_1, p_2) \in E \times F$, the function $y \mapsto f(p_1, y)$ is analytic within the set $\{y \in F \mid (p_1, y) \in s\}$ at the point $p_2$.

AnalyticOnNhd.curry_left theorem

 {f : E × F → G} {s : Set (E × F)} {y : F} (fa : AnalyticOnNhd 𝕜 f s) :
  AnalyticOnNhd 𝕜 (fun x ↦ f (x, y)) {x | (x, y) ∈ s}

Full source

/-- Analytic functions on products are analytic in the first coordinate -/
theorem AnalyticOnNhd.curry_left {f : E × F → G} {s : Set (E × F)} {y : F}
    (fa : AnalyticOnNhd 𝕜 f s) :
    AnalyticOnNhd 𝕜 (fun x ↦ f (x, y)) {x | (x, y) ∈ s} :=
  fun x m ↦ (fa (x, y) m).curry_left

Analyticity of Left Partial Application on a Neighborhood

Informal description

Let $E$, $F$, and $G$ be normed spaces over a complete normed field $\mathbb{K}$. Given a function $f \colon E \times F \to G$ that is analytic on a neighborhood $s$ of some point in $E \times F$, and given a fixed $y \in F$, the function $x \mapsto f(x, y)$ is analytic on the neighborhood $\{x \in E \mid (x, y) \in s\}$ of its domain.

AnalyticOn.curry_left theorem

 {f : E × F → G} {s : Set (E × F)} {y : F} (fa : AnalyticOn 𝕜 f s) : AnalyticOn 𝕜 (fun x ↦ f (x, y)) {x | (x, y) ∈ s}

Full source

theorem AnalyticOn.curry_left
    {f : E × F → G} {s : Set (E × F)} {y : F} (fa : AnalyticOn 𝕜 f s) :
    AnalyticOn 𝕜 (fun x ↦ f (x, y)) {x | (x, y) ∈ s} :=
  fun x m ↦ (fa (x, y) m).curry_left

Analyticity of Left Curry of Analytic Function on a Set

Informal description

Let $E$, $F$, and $G$ be normed spaces over a complete normed field $\mathbb{K}$, and let $f \colon E \times F \to G$ be a function. Given a set $s \subseteq E \times F$ and a point $y \in F$, if $f$ is analytic on $s$, then the function $x \mapsto f(x, y)$ is analytic on the set $\{x \in E \mid (x, y) \in s\}$.

AnalyticOnNhd.curry_right theorem

 {f : E × F → G} {x : E} {s : Set (E × F)} (fa : AnalyticOnNhd 𝕜 f s) :
  AnalyticOnNhd 𝕜 (fun y ↦ f (x, y)) {y | (x, y) ∈ s}

Full source

/-- Analytic functions on products are analytic in the second coordinate -/
theorem AnalyticOnNhd.curry_right {f : E × F → G} {x : E} {s : Set (E × F)}
    (fa : AnalyticOnNhd 𝕜 f s) :
    AnalyticOnNhd 𝕜 (fun y ↦ f (x, y)) {y | (x, y) ∈ s} :=
  fun y m ↦ (fa (x, y) m).curry_right

Analyticity of Partial Application in the Second Variable on a Neighborhood

Informal description

Let $E$, $F$, and $G$ be normed spaces over a complete normed field $\mathbb{K}$. Given a function $f \colon E \times F \to G$ that is analytic on a neighborhood $s$ of a point $(x, y) \in E \times F$, the function $y \mapsto f(x, y)$ is analytic on the neighborhood $\{y \in F \mid (x, y) \in s\}$ of $y$.

AnalyticOn.curry_right theorem

 {f : E × F → G} {x : E} {s : Set (E × F)} (fa : AnalyticOn 𝕜 f s) : AnalyticOn 𝕜 (fun y ↦ f (x, y)) {y | (x, y) ∈ s}

Full source

theorem AnalyticOn.curry_right
    {f : E × F → G} {x : E} {s : Set (E × F)} (fa : AnalyticOn 𝕜 f s) :
    AnalyticOn 𝕜 (fun y ↦ f (x, y)) {y | (x, y) ∈ s} :=
  fun y m ↦ (fa (x, y) m).curry_right

Analyticity of Partial Application in the Second Variable on a Set

Informal description

Let $E$, $F$, and $G$ be normed spaces over a complete normed field $\mathbb{K}$. Given a function $f \colon E \times F \to G$ that is analytic on a set $s \subseteq E \times F$, then for any fixed $x \in E$, the function $y \mapsto f(x, y)$ is analytic on the set $\{y \in F \mid (x, y) \in s\}$.

FormalMultilinearSeries.radius_pi_le theorem

(p : Π i, FormalMultilinearSeries 𝕜 E (Fm i)) (i : ι) : (FormalMultilinearSeries.pi p).radius ≤ (p i).radius

Full source

lemma FormalMultilinearSeries.radius_pi_le (p : Π i, FormalMultilinearSeries 𝕜 E (Fm i)) (i : ι) :
    (FormalMultilinearSeries.pi p).radius ≤ (p i).radius := by
  apply le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)
  obtain ⟨C, -, hC⟩ : ∃ C > 0, ∀ n, ‖pi p n‖ * ↑r' ^ n ≤ C := norm_mul_pow_le_of_lt_radius _ hr'
  apply le_radius_of_bound _ C (fun n ↦ ?_)
  apply le_trans _ (hC n)
  gcongr
  rw [pi, ContinuousMultilinearMap.opNorm_pi]
  exact norm_le_pi_norm (fun i ↦ p i n) i

Radius of Product Series is Bounded by Component Radii

Informal description

For a family of formal multilinear series $(p_i)_{i \in \iota}$ where each $p_i$ is a formal multilinear series from $E$ to $Fm_i$ over the field $\mathbb{K}$, the radius of convergence of the product series $\pi p$ is less than or equal to the radius of convergence of any individual series $p_i$, i.e., $$(\pi p).\text{radius} \leq (p_i).\text{radius}.$$

FormalMultilinearSeries.le_radius_pi theorem

(h : ∀ i, r ≤ (p i).radius) : r ≤ (FormalMultilinearSeries.pi p).radius

Full source

lemma FormalMultilinearSeries.le_radius_pi (h : ∀ i, r ≤ (p i).radius) :
    r ≤ (FormalMultilinearSeries.pi p).radius := by
  apply le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)
  have I i : ∃ C > 0, ∀ n, ‖p i n‖ * (r' : ℝ) ^ n ≤ C :=
    norm_mul_pow_le_of_lt_radius _ (hr'.trans_le (h i))
  choose C C_pos hC using I
  obtain ⟨D, D_nonneg, hD⟩ : ∃ D ≥ 0, ∀ i, C i ≤ D :=
    ⟨∑ i, C i, Finset.sum_nonneg (fun i _ ↦ (C_pos i).le),
      fun i ↦ Finset.single_le_sum (fun j _ ↦ (C_pos j).le) (Finset.mem_univ _)⟩
  apply le_radius_of_bound _ D (fun n ↦ ?_)
  rcases le_or_lt ((r' : ℝ)^n) 0 with hr' | hr'
  · exact le_trans (mul_nonpos_of_nonneg_of_nonpos (by positivity) hr') D_nonneg
  · simp only [pi]
    rw [← le_div_iff₀ hr', ContinuousMultilinearMap.opNorm_pi,
      pi_norm_le_iff_of_nonneg (by positivity)]
    intro i
    exact (le_div_iff₀ hr').2 ((hC i n).trans (hD i))

Lower Bound on Radius of Convergence for Product of Formal Multilinear Series

Informal description

For a family of formal multilinear series $(p_i)_{i \in \iota}$ where each $p_i$ has radius of convergence at least $r$, the radius of convergence of the product series $\pi p$ is also at least $r$.

FormalMultilinearSeries.radius_pi_eq_iInf theorem

: (FormalMultilinearSeries.pi p).radius = ⨅ i, (p i).radius

Full source

lemma FormalMultilinearSeries.radius_pi_eq_iInf :
    (FormalMultilinearSeries.pi p).radius = ⨅ i, (p i).radius := by
  refine le_antisymm (by simp [radius_pi_le]) ?_
  apply le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)
  exact le_radius_pi (fun i ↦ le_iInf_iff.1 hr'.le i)

Radius of Product Series Equals Infimum of Component Radii

Informal description

For a family of formal multilinear series $(p_i)_{i \in \iota}$, the radius of convergence of the product series $\pi p$ is equal to the infimum of the radii of convergence of the individual series $p_i$, i.e., $$(\pi p).\text{radius} = \inf_{i \in \iota} (p_i).\text{radius}.$$

HasFPowerSeriesWithinOnBall.pi theorem

 (hf : ∀ i, HasFPowerSeriesWithinOnBall (f i) (p i) s e r) (hr : 0 < r) :
  HasFPowerSeriesWithinOnBall (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) s e r

Full source

/-- If each function in a finite family has a power series within a ball, then so does the
family as a whole. Note that the positivity assumption on the radius is only needed when
the family is empty. -/
lemma HasFPowerSeriesWithinOnBall.pi
    (hf : ∀ i, HasFPowerSeriesWithinOnBall (f i) (p i) s e r) (hr : 0 < r) :
    HasFPowerSeriesWithinOnBall (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) s e r where
  r_le := by
    apply FormalMultilinearSeries.le_radius_pi (fun i ↦ ?_)
    exact (hf i).r_le
  r_pos := hr
  hasSum {_} m hy := Pi.hasSum.2 (fun i ↦ (hf i).hasSum m hy)

Power Series Expansion of Product Functions in a Ball

Informal description

Let $(f_i)_{i \in \iota}$ be a finite family of functions, each admitting a power series expansion $(p_i)_{i \in \iota}$ within a ball of radius $r > 0$ centered at $e$ in a set $s$. Then the product function $x \mapsto (f_i(x))_{i \in \iota}$ admits a power series expansion given by the product of the formal multilinear series $\pi p$ within the same ball.

hasFPowerSeriesWithinOnBall_pi_iff theorem

 (hr : 0 < r) :
  HasFPowerSeriesWithinOnBall (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) s e r ↔
    ∀ i, HasFPowerSeriesWithinOnBall (f i) (p i) s e r

Full source

lemma hasFPowerSeriesWithinOnBall_pi_iff (hr : 0 < r) :
    HasFPowerSeriesWithinOnBallHasFPowerSeriesWithinOnBall (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) s e r ↔
      ∀ i, HasFPowerSeriesWithinOnBall (f i) (p i) s e r where
  mp h i :=
    ⟨h.r_le.trans (FormalMultilinearSeries.radius_pi_le _ _), hr,
      fun m hy ↦ Pi.hasSum.1 (h.hasSum m hy) i⟩
  mpr h := .pi h hr

Equivalence of Power Series Expansions for Product Functions in a Ball

Informal description

For a family of functions $(f_i)_{i \in \iota}$ and formal multilinear series $(p_i)_{i \in \iota}$ over a field $\mathbb{K}$, and for a radius $r > 0$, the product function $x \mapsto (f_i(x))_{i \in \iota}$ has a power series expansion within the ball of radius $r$ centered at $e$ in the set $s$ if and only if each function $f_i$ has a power series expansion within the same ball. In other words, the following equivalence holds: $$ \text{HasFPowerSeriesWithinOnBall} \left( x \mapsto (f_i(x))_{i \in \iota}, \pi p, s, e, r \right) \leftrightarrow \forall i, \text{HasFPowerSeriesWithinOnBall} (f_i, p_i, s, e, r). $$

HasFPowerSeriesOnBall.pi theorem

 (hf : ∀ i, HasFPowerSeriesOnBall (f i) (p i) e r) (hr : 0 < r) :
  HasFPowerSeriesOnBall (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) e r

Full source

lemma HasFPowerSeriesOnBall.pi
    (hf : ∀ i, HasFPowerSeriesOnBall (f i) (p i) e r) (hr : 0 < r) :
    HasFPowerSeriesOnBall (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) e r := by
  simp_rw [← hasFPowerSeriesWithinOnBall_univ] at hf ⊢
  exact HasFPowerSeriesWithinOnBall.pi hf hr

Power Series Expansion of Product Functions on a Ball

Informal description

Let $(f_i)_{i \in \iota}$ be a family of functions, each admitting a power series expansion $(p_i)_{i \in \iota}$ on a ball of radius $r > 0$ centered at $e$. Then the product function $x \mapsto (f_i(x))_{i \in \iota}$ admits a power series expansion given by the product of the formal multilinear series $\pi p$ on the same ball.

hasFPowerSeriesOnBall_pi_iff theorem

 (hr : 0 < r) :
  HasFPowerSeriesOnBall (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) e r ↔
    ∀ i, HasFPowerSeriesOnBall (f i) (p i) e r

Full source

lemma hasFPowerSeriesOnBall_pi_iff (hr : 0 < r) :
    HasFPowerSeriesOnBallHasFPowerSeriesOnBall (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) e r ↔
      ∀ i, HasFPowerSeriesOnBall (f i) (p i) e r := by
  simp_rw [← hasFPowerSeriesWithinOnBall_univ]
  exact hasFPowerSeriesWithinOnBall_pi_iff hr

Equivalence of Power Series Expansions for Product Functions on a Ball

Informal description

For a family of functions $(f_i)_{i \in \iota}$ and formal multilinear series $(p_i)_{i \in \iota}$ over a field $\mathbb{K}$, and for a radius $r > 0$, the product function $x \mapsto (f_i(x))_{i \in \iota}$ has a power series expansion on the ball of radius $r$ centered at $e$ if and only if each function $f_i$ has a power series expansion on the same ball. In other words: $$ \text{HasFPowerSeriesOnBall} \left( x \mapsto (f_i(x))_{i \in \iota}, \pi p, e, r \right) \leftrightarrow \forall i, \text{HasFPowerSeriesOnBall} (f_i, p_i, e, r). $$

HasFPowerSeriesWithinAt.pi theorem

 (hf : ∀ i, HasFPowerSeriesWithinAt (f i) (p i) s e) :
  HasFPowerSeriesWithinAt (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) s e

Full source

lemma HasFPowerSeriesWithinAt.pi
    (hf : ∀ i, HasFPowerSeriesWithinAt (f i) (p i) s e) :
    HasFPowerSeriesWithinAt (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) s e := by
  have : ∀ᶠ r in 𝓝[>] 0, ∀ i, HasFPowerSeriesWithinOnBall (f i) (p i) s e r :=
    eventually_all.mpr (fun i ↦ (hf i).eventually)
  obtain ⟨r, hr, r_pos⟩ := (this.and self_mem_nhdsWithin).exists
  exact ⟨r, HasFPowerSeriesWithinOnBall.pi hr r_pos⟩

Power Series Expansion of Product Functions at a Point Within a Set

Informal description

Let $\{f_i : E \to F_i\}_{i \in \iota}$ be a finite family of functions, each admitting a power series expansion $p_i$ at a point $e$ within a set $s \subseteq E$. Then the product function $x \mapsto (f_i(x))_{i \in \iota}$ admits a power series expansion given by the product of the formal multilinear series $\pi p$ at $e$ within $s$.

hasFPowerSeriesWithinAt_pi_iff theorem

 :
  HasFPowerSeriesWithinAt (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) s e ↔
    ∀ i, HasFPowerSeriesWithinAt (f i) (p i) s e

Full source

lemma hasFPowerSeriesWithinAt_pi_iff :
    HasFPowerSeriesWithinAtHasFPowerSeriesWithinAt (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) s e ↔
      ∀ i, HasFPowerSeriesWithinAt (f i) (p i) s e := by
  refine ⟨fun h i ↦ ?_, fun h ↦ .pi h⟩
  obtain ⟨r, hr⟩ := h
  exact ⟨r, (hasFPowerSeriesWithinOnBall_pi_iff hr.r_pos).1 hr i⟩

Equivalence of Power Series Expansions for Product Functions at a Point Within a Set

Informal description

For a family of functions $(f_i)_{i \in \iota}$ and formal multilinear series $(p_i)_{i \in \iota}$, the product function $x \mapsto (f_i(x))_{i \in \iota}$ has a power series expansion at a point $e$ within a set $s$ if and only if each function $f_i$ has a power series expansion at $e$ within $s$. In other words, the following equivalence holds: $$ \text{HasFPowerSeriesWithinAt} \left( x \mapsto (f_i(x))_{i \in \iota}, \pi p, s, e \right) \leftrightarrow \forall i, \text{HasFPowerSeriesWithinAt} (f_i, p_i, s, e). $$

HasFPowerSeriesAt.pi theorem

(hf : ∀ i, HasFPowerSeriesAt (f i) (p i) e) : HasFPowerSeriesAt (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) e

Full source

lemma HasFPowerSeriesAt.pi
    (hf : ∀ i, HasFPowerSeriesAt (f i) (p i) e) :
    HasFPowerSeriesAt (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) e := by
  simp_rw [← hasFPowerSeriesWithinAt_univ] at hf ⊢
  exact HasFPowerSeriesWithinAt.pi hf

Power Series Expansion of Product Functions at a Point

Informal description

Let $\{f_i : E \to F_i\}_{i \in \iota}$ be a family of functions, each admitting a power series expansion $p_i$ at a point $e \in E$. Then the product function $x \mapsto (f_i(x))_{i \in \iota}$ admits a power series expansion given by the product of the formal multilinear series $\pi p$ at $e$.

hasFPowerSeriesAt_pi_iff theorem

: HasFPowerSeriesAt (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) e ↔ ∀ i, HasFPowerSeriesAt (f i) (p i) e

Full source

lemma hasFPowerSeriesAt_pi_iff :
    HasFPowerSeriesAtHasFPowerSeriesAt (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) e ↔
      ∀ i, HasFPowerSeriesAt (f i) (p i) e := by
  simp_rw [← hasFPowerSeriesWithinAt_univ]
  exact hasFPowerSeriesWithinAt_pi_iff

Equivalence of Power Series Expansions for Product Functions at a Point

Informal description

For a family of functions $(f_i)_{i \in \iota}$ and formal multilinear series $(p_i)_{i \in \iota}$, the product function $x \mapsto (f_i(x))_{i \in \iota}$ has a power series expansion at a point $e$ if and only if each function $f_i$ has a power series expansion at $e$. In other words, the following equivalence holds: $$ \text{HasFPowerSeriesAt} \left( x \mapsto (f_i(x))_{i \in \iota}, \pi p, e \right) \leftrightarrow \forall i, \text{HasFPowerSeriesAt} (f_i, p_i, e). $$

AnalyticWithinAt.pi theorem

(hf : ∀ i, AnalyticWithinAt 𝕜 (f i) s e) : AnalyticWithinAt 𝕜 (fun x ↦ (f · x)) s e

Full source

lemma AnalyticWithinAt.pi (hf : ∀ i, AnalyticWithinAt 𝕜 (f i) s e) :
    AnalyticWithinAt 𝕜 (fun x ↦ (f · x)) s e := by
  choose p hp using hf
  exact ⟨FormalMultilinearSeries.pi p, HasFPowerSeriesWithinAt.pi hp⟩

Analyticity of Product Functions Within a Set

Informal description

Let $\{f_i : E \to F_i\}_{i \in \iota}$ be a family of functions defined on a set $s \subseteq E$ with values in normed spaces $F_i$, and let $e \in s$. If for each $i$, the function $f_i$ is analytic at $e$ within $s$ (with respect to the field $\mathbb{K}$), then the product function $x \mapsto (f_i(x))_{i \in \iota}$ is analytic at $e$ within $s$.

analyticWithinAt_pi_iff theorem

: AnalyticWithinAt 𝕜 (fun x ↦ (f · x)) s e ↔ ∀ i, AnalyticWithinAt 𝕜 (f i) s e

Full source

lemma analyticWithinAt_pi_iff :
    AnalyticWithinAtAnalyticWithinAt 𝕜 (fun x ↦ (f · x)) s e ↔ ∀ i, AnalyticWithinAt 𝕜 (f i) s e := by
  refine ⟨fun h i ↦ ?_, fun h ↦ .pi h⟩
  exact ((ContinuousLinearMap.proj (R := 𝕜) i).analyticAt _).comp_analyticWithinAt h

Characterization of Analyticity for Product Functions Within a Set

Informal description

Let $\mathbb{K}$ be a field, $E$ a normed space over $\mathbb{K}$, $s \subseteq E$, and $e \in s$. For a family of functions $\{f_i : E \to F_i\}_{i \in \iota}$ where each $F_i$ is a normed space over $\mathbb{K}$, the product function $x \mapsto (f_i(x))_{i \in \iota}$ is analytic at $e$ within $s$ if and only if each $f_i$ is analytic at $e$ within $s$.

AnalyticAt.pi theorem

(hf : ∀ i, AnalyticAt 𝕜 (f i) e) : AnalyticAt 𝕜 (fun x ↦ (f · x)) e

Full source

lemma AnalyticAt.pi (hf : ∀ i, AnalyticAt 𝕜 (f i) e) :
    AnalyticAt 𝕜 (fun x ↦ (f · x)) e := by
  simp_rw [← analyticWithinAt_univ] at hf ⊢
  exact AnalyticWithinAt.pi hf

Analyticity of Product Functions at a Point

Informal description

Let $\{f_i : E \to F_i\}_{i \in \iota}$ be a family of functions defined on a normed space $E$ with values in normed spaces $F_i$, and let $e \in E$. If for each $i$, the function $f_i$ is analytic at $e$ (with respect to the field $\mathbb{K}$), then the product function $x \mapsto (f_i(x))_{i \in \iota}$ is analytic at $e$.

analyticAt_pi_iff theorem

: AnalyticAt 𝕜 (fun x ↦ (f · x)) e ↔ ∀ i, AnalyticAt 𝕜 (f i) e

Full source

lemma analyticAt_pi_iff :
    AnalyticAtAnalyticAt 𝕜 (fun x ↦ (f · x)) e ↔ ∀ i, AnalyticAt 𝕜 (f i) e := by
  simp_rw [← analyticWithinAt_univ]
  exact analyticWithinAt_pi_iff

Characterization of Analyticity for Product Functions at a Point

Informal description

Let $\mathbb{K}$ be a field, $E$ a normed space over $\mathbb{K}$, and $e \in E$. For a family of functions $\{f_i : E \to F_i\}_{i \in \iota}$ where each $F_i$ is a normed space over $\mathbb{K}$, the product function $x \mapsto (f_i(x))_{i \in \iota}$ is analytic at $e$ if and only if each $f_i$ is analytic at $e$.

AnalyticOn.pi theorem

(hf : ∀ i, AnalyticOn 𝕜 (f i) s) : AnalyticOn 𝕜 (fun x ↦ (f · x)) s

Full source

lemma AnalyticOn.pi (hf : ∀ i, AnalyticOn 𝕜 (f i) s) :
    AnalyticOn 𝕜 (fun x ↦ (f · x)) s :=
  fun x hx ↦ AnalyticWithinAt.pi (fun i ↦ hf i x hx)

Analyticity of Product Functions on a Set

Informal description

Let $\{f_i : E \to F_i\}_{i \in \iota}$ be a family of functions defined on a set $s \subseteq E$ with values in normed spaces $F_i$. If for each $i$, the function $f_i$ is analytic on $s$ (with respect to the field $\mathbb{K}$), then the product function $x \mapsto (f_i(x))_{i \in \iota}$ is analytic on $s$.

analyticOn_pi_iff theorem

: AnalyticOn 𝕜 (fun x ↦ (f · x)) s ↔ ∀ i, AnalyticOn 𝕜 (f i) s

Full source

lemma analyticOn_pi_iff :
    AnalyticOnAnalyticOn 𝕜 (fun x ↦ (f · x)) s ↔ ∀ i, AnalyticOn 𝕜 (f i) s :=
  ⟨fun h i x hx ↦ analyticWithinAt_pi_iff.1 (h x hx) i, fun h ↦ .pi h⟩

Characterization of Analyticity for Product Functions on a Set

Informal description

Let $\mathbb{K}$ be a field, $E$ a normed space over $\mathbb{K}$, and $s \subseteq E$. For a family of functions $\{f_i : E \to F_i\}_{i \in \iota}$ where each $F_i$ is a normed space over $\mathbb{K}$, the product function $x \mapsto (f_i(x))_{i \in \iota}$ is analytic on $s$ if and only if each $f_i$ is analytic on $s$.

AnalyticOnNhd.pi theorem

(hf : ∀ i, AnalyticOnNhd 𝕜 (f i) s) : AnalyticOnNhd 𝕜 (fun x ↦ (f · x)) s

Full source

lemma AnalyticOnNhd.pi (hf : ∀ i, AnalyticOnNhd 𝕜 (f i) s) :
    AnalyticOnNhd 𝕜 (fun x ↦ (f · x)) s :=
  fun x hx ↦ AnalyticAt.pi (fun i ↦ hf i x hx)

Analyticity of Product Functions on a Neighborhood

Informal description

Let $\{f_i : E \to F_i\}_{i \in \iota}$ be a family of functions defined on a neighborhood $s$ of a point in a normed space $E$ with values in normed spaces $F_i$. If for each $i$, the function $f_i$ is analytic on $s$ (with respect to the field $\mathbb{K}$), then the product function $x \mapsto (f_i(x))_{i \in \iota}$ is analytic on $s$.

analyticOnNhd_pi_iff theorem

: AnalyticOnNhd 𝕜 (fun x ↦ (f · x)) s ↔ ∀ i, AnalyticOnNhd 𝕜 (f i) s

Full source

lemma analyticOnNhd_pi_iff :
    AnalyticOnNhdAnalyticOnNhd 𝕜 (fun x ↦ (f · x)) s ↔ ∀ i, AnalyticOnNhd 𝕜 (f i) s :=
  ⟨fun h i x hx ↦ analyticAt_pi_iff.1 (h x hx) i, fun h ↦ .pi h⟩

Characterization of Analyticity for Product Functions on a Neighborhood

Informal description

Let $\mathbb{K}$ be a field, $E$ a normed space over $\mathbb{K}$, and $s \subseteq E$ a neighborhood. For a family of functions $\{f_i : E \to F_i\}_{i \in \iota}$ where each $F_i$ is a normed space over $\mathbb{K}$, the product function $x \mapsto (f_i(x))_{i \in \iota}$ is analytic on $s$ if and only if each $f_i$ is analytic on $s$.

analyticAt_smul theorem

 [NormedSpace 𝕝 E] [IsScalarTower 𝕜 𝕝 E] (z : 𝕝 × E) : AnalyticAt 𝕜 (fun x : 𝕝 × E ↦ x.1 • x.2) z

Full source

/-- Scalar multiplication is analytic (jointly in both variables). The statement is a little
pedantic to allow towers of field extensions.

TODO: can we replace `𝕜'` with a "normed module" in such a way that `analyticAt_mul` is a special
case of this? -/
@[fun_prop]
lemma analyticAt_smul [NormedSpace 𝕝 E] [IsScalarTower 𝕜 𝕝 E] (z : 𝕝 × E) :
    AnalyticAt 𝕜 (fun x : 𝕝 × E ↦ x.1 • x.2) z :=
  (ContinuousLinearMap.lsmul 𝕜 𝕝).analyticAt_bilinear z

Analyticity of Scalar Multiplication in Normed Spaces

Informal description

Let $\mathbb{K}$ and $\mathbb{L}$ be normed fields with $\mathbb{K}$ as a subfield of $\mathbb{L}$, and let $E$ be a normed space over $\mathbb{L}$ that is also a normed space over $\mathbb{K}$ via restriction of scalars. For any point $z = (c, v) \in \mathbb{L} \times E$, the scalar multiplication function $(x, y) \mapsto x \cdot y$ is analytic at $z$.

analyticAt_mul theorem

(z : A × A) : AnalyticAt 𝕜 (fun x : A × A ↦ x.1 * x.2) z

Full source

/-- Multiplication in a normed algebra over `𝕜` is analytic. -/
@[fun_prop]
lemma analyticAt_mul (z : A × A) : AnalyticAt 𝕜 (fun x : A × A ↦ x.1 * x.2) z :=
  (ContinuousLinearMap.mul 𝕜 A).analyticAt_bilinear z

Analyticity of Multiplication in Normed Algebras

Informal description

Let $A$ be a normed algebra over a field $\mathbb{K}$. For any point $z = (z_1, z_2) \in A \times A$, the multiplication function $(x_1, x_2) \mapsto x_1 \cdot x_2$ is analytic at $z$.

AnalyticWithinAt.smul theorem

 [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {s : Set E} {z : E} (hf : AnalyticWithinAt 𝕜 f s z)
  (hg : AnalyticWithinAt 𝕜 g s z) : AnalyticWithinAt 𝕜 (fun x ↦ f x • g x) s z

Full source

/-- Scalar multiplication of one analytic function by another. -/
lemma AnalyticWithinAt.smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F]
    {f : E → 𝕝} {g : E → F} {s : Set E} {z : E}
    (hf : AnalyticWithinAt 𝕜 f s z) (hg : AnalyticWithinAt 𝕜 g s z) :
    AnalyticWithinAt 𝕜 (fun x ↦ f x • g x) s z :=
  (analyticAt_smul _).comp₂_analyticWithinAt hf hg

Analyticity of Scalar Multiplication of Analytic Functions Within a Set

Informal description

Let $\mathbb{K}$ and $\mathbb{L}$ be normed fields with $\mathbb{K}$ as a subfield of $\mathbb{L}$, and let $E$ and $F$ be normed spaces over $\mathbb{L}$ that are also normed spaces over $\mathbb{K}$ via restriction of scalars. Given functions $f \colon E \to \mathbb{L}$ and $g \colon E \to F$ that are analytic at a point $z \in E$ within a set $s \subseteq E$, the scalar multiplication function $x \mapsto f(x) \cdot g(x)$ is analytic at $z$ within $s$.

AnalyticAt.fun_smul theorem

 [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {z : E} (hf : AnalyticAt 𝕜 f z)
  (hg : AnalyticAt 𝕜 g z) : AnalyticAt 𝕜 (fun x ↦ f x • g x) z

Full source

/-- Scalar multiplication of one analytic function by another. -/
@[fun_prop]
lemma AnalyticAt.fun_smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {z : E}
    (hf : AnalyticAt 𝕜 f z) (hg : AnalyticAt 𝕜 g z) :
    AnalyticAt 𝕜 (fun x ↦ f x • g x) z :=
  (analyticAt_smul _).comp₂ hf hg

Analyticity of Pointwise Scalar Multiplication of Analytic Functions

Informal description

Let $\mathbb{K}$ and $\mathbb{L}$ be normed fields with $\mathbb{K}$ as a subfield of $\mathbb{L}$, and let $E$ and $F$ be normed spaces over $\mathbb{L}$ that are also normed spaces over $\mathbb{K}$ via restriction of scalars. Given functions $f \colon E \to \mathbb{L}$ and $g \colon E \to F$ that are analytic at a point $z \in E$, the scalar multiplication function $x \mapsto f(x) \cdot g(x)$ is analytic at $z$.

AnalyticAt.smul theorem

 [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {z : E} (hf : AnalyticAt 𝕜 f z)
  (hg : AnalyticAt 𝕜 g z) : AnalyticAt 𝕜 (f • g) z

Full source

/-- Scalar multiplication of one analytic function by another. -/
@[fun_prop]
lemma AnalyticAt.smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {z : E}
    (hf : AnalyticAt 𝕜 f z) (hg : AnalyticAt 𝕜 g z) :
    AnalyticAt 𝕜 (f • g) z :=
  hf.fun_smul hg

Analyticity of Pointwise Scalar Multiplication at a Point

Informal description

Let $\mathbb{K}$ and $\mathbb{L}$ be normed fields with $\mathbb{K}$ as a subfield of $\mathbb{L}$, and let $E$ and $F$ be normed spaces over $\mathbb{L}$ that are also normed spaces over $\mathbb{K}$ via restriction of scalars. Given functions $f \colon E \to \mathbb{L}$ and $g \colon E \to F$ that are analytic at a point $z \in E$, the pointwise scalar multiplication function $f \cdot g$ is analytic at $z$.

AnalyticOn.smul theorem

 [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {s : Set E} (hf : AnalyticOn 𝕜 f s)
  (hg : AnalyticOn 𝕜 g s) : AnalyticOn 𝕜 (fun x ↦ f x • g x) s

Full source

/-- Scalar multiplication of one analytic function by another. -/
lemma AnalyticOn.smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F]
    {f : E → 𝕝} {g : E → F} {s : Set E}
    (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) :
    AnalyticOn 𝕜 (fun x ↦ f x • g x) s :=
  fun _ m ↦ (hf _ m).smul (hg _ m)

Analyticity of Scalar Multiplication on a Set

Informal description

Let $\mathbb{K}$ and $\mathbb{L}$ be normed fields with $\mathbb{K}$ as a subfield of $\mathbb{L}$, and let $E$ and $F$ be normed spaces over $\mathbb{L}$ that are also normed spaces over $\mathbb{K}$ via restriction of scalars. Given functions $f \colon E \to \mathbb{L}$ and $g \colon E \to F$ that are analytic on a set $s \subseteq E$, the scalar multiplication function $x \mapsto f(x) \cdot g(x)$ is analytic on $s$.

AnalyticOnNhd.smul theorem

 [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {s : Set E} (hf : AnalyticOnNhd 𝕜 f s)
  (hg : AnalyticOnNhd 𝕜 g s) : AnalyticOnNhd 𝕜 (fun x ↦ f x • g x) s

Full source

/-- Scalar multiplication of one analytic function by another. -/
lemma AnalyticOnNhd.smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {s : Set E}
    (hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOnNhd 𝕜 g s) :
    AnalyticOnNhd 𝕜 (fun x ↦ f x • g x) s :=
  fun _ m ↦ (hf _ m).smul (hg _ m)

Neighborhood Analyticity of Scalar Multiplication on a Set

Informal description

Let $\mathbb{K}$ and $\mathbb{L}$ be normed fields with $\mathbb{K}$ as a subfield of $\mathbb{L}$, and let $E$ and $F$ be normed spaces over $\mathbb{L}$ that are also normed spaces over $\mathbb{K}$ via restriction of scalars. Given functions $f \colon E \to \mathbb{L}$ and $g \colon E \to F$ that are analytic in a neighborhood of each point in a set $s \subseteq E$, the scalar multiplication function $x \mapsto f(x) \cdot g(x)$ is analytic in a neighborhood of each point in $s$.

AnalyticWithinAt.mul theorem

 {f g : E → A} {s : Set E} {z : E} (hf : AnalyticWithinAt 𝕜 f s z) (hg : AnalyticWithinAt 𝕜 g s z) :
  AnalyticWithinAt 𝕜 (fun x ↦ f x * g x) s z

Full source

/-- Multiplication of analytic functions (valued in a normed `𝕜`-algebra) is analytic. -/
lemma AnalyticWithinAt.mul {f g : E → A} {s : Set E} {z : E}
    (hf : AnalyticWithinAt 𝕜 f s z) (hg : AnalyticWithinAt 𝕜 g s z) :
    AnalyticWithinAt 𝕜 (fun x ↦ f x * g x) s z :=
  (analyticAt_mul _).comp₂_analyticWithinAt hf hg

Analyticity of Product of Functions within a Set

Informal description

Let $E$ be a normed space over a complete normed field $\mathbb{K}$, and let $A$ be a normed $\mathbb{K}$-algebra. For functions $f, g \colon E \to A$ and a point $z \in E$, if $f$ and $g$ are analytic at $z$ within a set $s \subseteq E$, then the product function $x \mapsto f(x) \cdot g(x)$ is also analytic at $z$ within $s$.

AnalyticAt.fun_mul theorem

{f g : E → A} {z : E} (hf : AnalyticAt 𝕜 f z) (hg : AnalyticAt 𝕜 g z) : AnalyticAt 𝕜 (fun x ↦ f x * g x) z

Full source

/-- Multiplication of analytic functions (valued in a normed `𝕜`-algebra) is analytic. -/
@[fun_prop]
lemma AnalyticAt.fun_mul {f g : E → A} {z : E} (hf : AnalyticAt 𝕜 f z) (hg : AnalyticAt 𝕜 g z) :
    AnalyticAt 𝕜 (fun x ↦ f x * g x) z :=
  (analyticAt_mul _).comp₂ hf hg

Analyticity of Pointwise Product of Analytic Functions

Informal description

Let $E$ be a normed space over a complete normed field $\mathbb{K}$, and let $A$ be a normed $\mathbb{K}$-algebra. For any functions $f, g \colon E \to A$ and a point $z \in E$, if $f$ and $g$ are analytic at $z$, then the pointwise product function $x \mapsto f(x) \cdot g(x)$ is also analytic at $z$.

AnalyticAt.mul theorem

{f g : E → A} {z : E} (hf : AnalyticAt 𝕜 f z) (hg : AnalyticAt 𝕜 g z) : AnalyticAt 𝕜 (f * g) z

Full source

/-- Multiplication of analytic functions (valued in a normed `𝕜`-algebra) is analytic. -/
@[fun_prop]
lemma AnalyticAt.mul {f g : E → A} {z : E} (hf : AnalyticAt 𝕜 f z) (hg : AnalyticAt 𝕜 g z) :
    AnalyticAt 𝕜 (f * g) z :=
  hf.fun_mul hg

Analyticity of Pointwise Product of Analytic Functions at a Point

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ a normed space over $\mathbb{K}$, and $A$ a normed $\mathbb{K}$-algebra. For any functions $f, g \colon E \to A$ and a point $z \in E$, if $f$ and $g$ are analytic at $z$, then their pointwise product $f \cdot g$ is also analytic at $z$.

AnalyticOn.mul theorem

 {f g : E → A} {s : Set E} (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) : AnalyticOn 𝕜 (fun x ↦ f x * g x) s

Full source

/-- Multiplication of analytic functions (valued in a normed `𝕜`-algebra) is analytic. -/
lemma AnalyticOn.mul {f g : E → A} {s : Set E}
    (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) :
    AnalyticOn 𝕜 (fun x ↦ f x * g x) s :=
  fun _ m ↦ (hf _ m).mul (hg _ m)

Analyticity of Pointwise Product on a Set

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ a normed space over $\mathbb{K}$, and $A$ a normed $\mathbb{K}$-algebra. Given two functions $f, g \colon E \to A$ that are analytic on a set $s \subseteq E$, their pointwise product $x \mapsto f(x) \cdot g(x)$ is also analytic on $s$.

AnalyticOnNhd.mul theorem

 {f g : E → A} {s : Set E} (hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOnNhd 𝕜 g s) : AnalyticOnNhd 𝕜 (fun x ↦ f x * g x) s

Full source

/-- Multiplication of analytic functions (valued in a normed `𝕜`-algebra) is analytic. -/
lemma AnalyticOnNhd.mul {f g : E → A} {s : Set E}
    (hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOnNhd 𝕜 g s) :
    AnalyticOnNhd 𝕜 (fun x ↦ f x * g x) s :=
  fun _ m ↦ (hf _ m).mul (hg _ m)

Analyticity of Pointwise Product on Neighborhoods of a Set

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ a normed space over $\mathbb{K}$, and $A$ a normed $\mathbb{K}$-algebra. Given two functions $f, g \colon E \to A$ that are analytic in a neighborhood of each point in a set $s \subseteq E$, their pointwise product $x \mapsto f(x) \cdot g(x)$ is also analytic in a neighborhood of each point in $s$.

AnalyticWithinAt.fun_pow theorem

 {f : E → A} {z : E} {s : Set E} (hf : AnalyticWithinAt 𝕜 f s z) (n : ℕ) : AnalyticWithinAt 𝕜 (fun x ↦ f x ^ n) s z

Full source

/-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/
lemma AnalyticWithinAt.fun_pow {f : E → A} {z : E} {s : Set E} (hf : AnalyticWithinAt 𝕜 f s z)
    (n : ℕ) :
    AnalyticWithinAt 𝕜 (fun x ↦ f x ^ n) s z := by
  induction n with
  | zero =>
    simp only [pow_zero]
    apply analyticWithinAt_const
  | succ m hm =>
    simp only [pow_succ]
    exact hm.mul hf

Analyticity of Powers of Analytic Functions

Informal description

Let $E$ be a normed space over a complete normed field $\mathbb{K}$, and let $A$ be a normed $\mathbb{K}$-algebra. For a function $f \colon E \to A$, a point $z \in E$, and a set $s \subseteq E$, if $f$ is analytic at $z$ within $s$, then for any natural number $n$, the function $x \mapsto f(x)^n$ is also analytic at $z$ within $s$.

AnalyticWithinAt.pow theorem

{f : E → A} {z : E} {s : Set E} (hf : AnalyticWithinAt 𝕜 f s z) (n : ℕ) : AnalyticWithinAt 𝕜 (f ^ n) s z

Full source

/-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/
lemma AnalyticWithinAt.pow {f : E → A} {z : E} {s : Set E} (hf : AnalyticWithinAt 𝕜 f s z)
    (n : ℕ) :
    AnalyticWithinAt 𝕜 (f ^ n) s z :=
  AnalyticWithinAt.fun_pow hf n

Analyticity of Power Functions

Informal description

Let $E$ be a normed space over a complete normed field $\mathbb{K}$, and let $A$ be a normed $\mathbb{K}$-algebra. For a function $f \colon E \to A$, a point $z \in E$, and a set $s \subseteq E$, if $f$ is analytic at $z$ within $s$, then for any natural number $n$, the $n$-th power function $f^n$ is also analytic at $z$ within $s$.

AnalyticAt.fun_pow theorem

{f : E → A} {z : E} (hf : AnalyticAt 𝕜 f z) (n : ℕ) : AnalyticAt 𝕜 (fun x ↦ f x ^ n) z

Full source

/-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/
@[fun_prop]
lemma AnalyticAt.fun_pow {f : E → A} {z : E} (hf : AnalyticAt 𝕜 f z) (n : ℕ) :
    AnalyticAt 𝕜 (fun x ↦ f x ^ n) z := by
  rw [← analyticWithinAt_univ] at hf ⊢
  exact hf.pow n

Analyticity of Pointwise Powers of Analytic Functions

Informal description

Let $E$ be a normed space over a complete normed field $\mathbb{K}$, and let $A$ be a normed $\mathbb{K}$-algebra. For a function $f \colon E \to A$ and a point $z \in E$, if $f$ is analytic at $z$, then for any natural number $n$, the function $x \mapsto f(x)^n$ is also analytic at $z$.

AnalyticAt.pow theorem

{f : E → A} {z : E} (hf : AnalyticAt 𝕜 f z) (n : ℕ) : AnalyticAt 𝕜 (f ^ n) z

Full source

/-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/
@[fun_prop]
lemma AnalyticAt.pow {f : E → A} {z : E} (hf : AnalyticAt 𝕜 f z) (n : ℕ) :
    AnalyticAt 𝕜 (f ^ n) z :=
  AnalyticAt.fun_pow hf n

Analyticity of Power Functions at a Point

Informal description

Let $E$ be a normed space over a complete normed field $\mathbb{K}$, and let $A$ be a normed $\mathbb{K}$-algebra. For a function $f \colon E \to A$ and a point $z \in E$, if $f$ is analytic at $z$, then for any natural number $n$, the $n$-th power function $f^n$ is also analytic at $z$.

AnalyticOn.fun_pow theorem

{f : E → A} {s : Set E} (hf : AnalyticOn 𝕜 f s) (n : ℕ) : AnalyticOn 𝕜 (fun x ↦ f x ^ n) s

Full source

/-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/
lemma AnalyticOn.fun_pow {f : E → A} {s : Set E} (hf : AnalyticOn 𝕜 f s) (n : ℕ) :
    AnalyticOn 𝕜 (fun x ↦ f x ^ n) s :=
  fun _ m ↦ (hf _ m).pow n

Analyticity of Pointwise Powers on a Set

Informal description

Let $E$ be a normed space over a complete normed field $\mathbb{K}$, and let $A$ be a normed $\mathbb{K}$-algebra. For a function $f \colon E \to A$ and a set $s \subseteq E$, if $f$ is analytic on $s$, then for any natural number $n$, the function $x \mapsto f(x)^n$ is also analytic on $s$.

AnalyticOn.pow theorem

{f : E → A} {s : Set E} (hf : AnalyticOn 𝕜 f s) (n : ℕ) : AnalyticOn 𝕜 (f ^ n) s

Full source

/-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/
lemma AnalyticOn.pow {f : E → A} {s : Set E} (hf : AnalyticOn 𝕜 f s) (n : ℕ) :
    AnalyticOn 𝕜 (f ^ n) s :=
  fun _ m ↦ (hf _ m).pow n

Analyticity of Power Functions on a Set

Informal description

Let $E$ be a normed space over a complete normed field $\mathbb{K}$, and let $A$ be a normed $\mathbb{K}$-algebra. For a function $f \colon E \to A$ and a set $s \subseteq E$, if $f$ is analytic on $s$, then for any natural number $n$, the $n$-th power function $f^n$ is also analytic on $s$.

AnalyticOnNhd.fun_pow theorem

{f : E → A} {s : Set E} (hf : AnalyticOnNhd 𝕜 f s) (n : ℕ) : AnalyticOnNhd 𝕜 (fun x ↦ f x ^ n) s

Full source

/-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/
lemma AnalyticOnNhd.fun_pow {f : E → A} {s : Set E} (hf : AnalyticOnNhd 𝕜 f s) (n : ℕ) :
    AnalyticOnNhd 𝕜 (fun x ↦ f x ^ n) s :=
  fun _ m ↦ (hf _ m).pow n

Analyticity of Pointwise Powers on Neighborhoods

Informal description

Let $E$ be a normed space over a complete normed field $\mathbb{K}$, and let $A$ be a normed $\mathbb{K}$-algebra. For a function $f \colon E \to A$ and a set $s \subseteq E$, if $f$ is analytic on a neighborhood of $s$, then for any natural number $n$, the function $x \mapsto f(x)^n$ is also analytic on a neighborhood of $s$.

AnalyticOnNhd.pow theorem

{f : E → A} {s : Set E} (hf : AnalyticOnNhd 𝕜 f s) (n : ℕ) : AnalyticOnNhd 𝕜 (f ^ n) s

Full source

/-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/
lemma AnalyticOnNhd.pow {f : E → A} {s : Set E} (hf : AnalyticOnNhd 𝕜 f s) (n : ℕ) :
    AnalyticOnNhd 𝕜 (f ^ n) s :=
  AnalyticOnNhd.fun_pow hf n

Analyticity of Power Functions on Neighborhoods

Informal description

Let $E$ be a normed space over a complete normed field $\mathbb{K}$, and let $A$ be a normed $\mathbb{K}$-algebra. For a function $f \colon E \to A$ and a set $s \subseteq E$, if $f$ is analytic on a neighborhood of $s$, then for any natural number $n$, the $n$-th power function $f^n$ is also analytic on a neighborhood of $s$.

AnalyticWithinAt.fun_zpow_nonneg theorem

 {f : E → 𝕝} {z : E} {s : Set E} {n : ℤ} (hf : AnalyticWithinAt 𝕜 f s z) (hn : 0 ≤ n) :
  AnalyticWithinAt 𝕜 (fun x ↦ f x ^ n) s z

Full source

/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic if the exponent is
nonnegative. -/
lemma AnalyticWithinAt.fun_zpow_nonneg {f : E → 𝕝} {z : E} {s : Set E} {n : ℤ}
    (hf : AnalyticWithinAt 𝕜 f s z) (hn : 0 ≤ n) :
    AnalyticWithinAt 𝕜 (fun x ↦ f x ^ n) s z := by
  simpa [← zpow_natCast, hn] using hf.pow n.toNat

Analyticity of Nonnegative Integer Powers of Analytic Functions

Informal description

Let $E$ be a normed space over a complete normed field $\mathbb{K}$, and let $\mathbb{L}$ be a normed field over $\mathbb{K}$. For a function $f \colon E \to \mathbb{L}$, a point $z \in E$, a set $s \subseteq E$, and an integer $n \geq 0$, if $f$ is analytic at $z$ within $s$, then the function $x \mapsto f(x)^n$ is also analytic at $z$ within $s$.

AnalyticWithinAt.zpow_nonneg theorem

 {f : E → 𝕝} {z : E} {s : Set E} {n : ℤ} (hf : AnalyticWithinAt 𝕜 f s z) (hn : 0 ≤ n) : AnalyticWithinAt 𝕜 (f ^ n) s z

Full source

/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic if the exponent is
nonnegative. -/
lemma AnalyticWithinAt.zpow_nonneg {f : E → 𝕝} {z : E} {s : Set E} {n : ℤ}
    (hf : AnalyticWithinAt 𝕜 f s z) (hn : 0 ≤ n) :
    AnalyticWithinAt 𝕜 (f ^ n) s z :=
  fun_zpow_nonneg hf hn

Analyticity of Nonnegative Integer Powers of Analytic Functions (Pointwise Version)

Informal description

Let $E$ be a normed space over a complete normed field $\mathbb{K}$, and let $\mathbb{L}$ be a normed field over $\mathbb{K}$. For a function $f \colon E \to \mathbb{L}$, a point $z \in E$, a set $s \subseteq E$, and an integer $n \geq 0$, if $f$ is analytic at $z$ within $s$, then the function $f^n$ is also analytic at $z$ within $s$.

AnalyticAt.fun_zpow_nonneg theorem

{f : E → 𝕝} {z : E} {n : ℤ} (hf : AnalyticAt 𝕜 f z) (hn : 0 ≤ n) : AnalyticAt 𝕜 (fun x ↦ f x ^ n) z

Full source

/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic if the exponent is
nonnegative. -/
lemma AnalyticAt.fun_zpow_nonneg {f : E → 𝕝} {z : E} {n : ℤ} (hf : AnalyticAt 𝕜 f z) (hn : 0 ≤ n) :
    AnalyticAt 𝕜 (fun x ↦ f x ^ n) z := by
  simpa [← zpow_natCast, hn] using hf.pow n.toNat

Analyticity of Nonnegative Integer Powers at a Point

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ a normed space over $\mathbb{K}$, and $\mathbb{L}$ a normed field extension of $\mathbb{K}$. Given a function $f \colon E \to \mathbb{L}$ that is analytic at a point $z \in E$, and an integer $n \geq 0$, the function $x \mapsto f(x)^n$ is also analytic at $z$.

AnalyticAt.zpow_nonneg theorem

{f : E → 𝕝} {z : E} {n : ℤ} (hf : AnalyticAt 𝕜 f z) (hn : 0 ≤ n) : AnalyticAt 𝕜 (f ^ n) z

Full source

/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic if the exponent is
nonnegative. -/
lemma AnalyticAt.zpow_nonneg {f : E → 𝕝} {z : E} {n : ℤ} (hf : AnalyticAt 𝕜 f z) (hn : 0 ≤ n) :
    AnalyticAt 𝕜 (f ^ n) z :=
  fun_zpow_nonneg hf hn

Analyticity of Nonnegative Integer Powers at a Point

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ a normed space over $\mathbb{K}$, and $\mathbb{L}$ a normed field extension of $\mathbb{K}$. Given a function $f \colon E \to \mathbb{L}$ that is analytic at a point $z \in E$, and an integer $n \geq 0$, the function $f^n$ is also analytic at $z$.

AnalyticOn.fun_zpow_nonneg theorem

 {f : E → 𝕝} {s : Set E} {n : ℤ} (hf : AnalyticOn 𝕜 f s) (hn : 0 ≤ n) : AnalyticOn 𝕜 (fun x ↦ f x ^ n) s

Full source

/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic if the exponent is
nonnegative. -/
lemma AnalyticOn.fun_zpow_nonneg {f : E → 𝕝} {s : Set E} {n : ℤ} (hf : AnalyticOn 𝕜 f s)
    (hn : 0 ≤ n) :
    AnalyticOn 𝕜 (fun x ↦ f x ^ n) s := by
  simpa [← zpow_natCast, hn] using hf.pow n.toNat

Analyticity of Nonnegative Integer Powers of Analytic Functions

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ a normed space over $\mathbb{K}$, and $\mathbb{l}$ a normed field extension of $\mathbb{K}$. Given a function $f \colon E \to \mathbb{l}$ that is analytic on a set $s \subseteq E$, and an integer $n \geq 0$, the function $x \mapsto f(x)^n$ is also analytic on $s$.

AnalyticOn.zpow_nonneg theorem

{f : E → 𝕝} {s : Set E} {n : ℤ} (hf : AnalyticOn 𝕜 f s) (hn : 0 ≤ n) : AnalyticOn 𝕜 (f ^ n) s

Full source

/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic if the exponent is
nonnegative. -/
lemma AnalyticOn.zpow_nonneg {f : E → 𝕝} {s : Set E} {n : ℤ} (hf : AnalyticOn 𝕜 f s)
    (hn : 0 ≤ n) :
    AnalyticOn 𝕜 (f ^ n) s :=
  fun_zpow_nonneg hf hn

Analyticity of Nonnegative Integer Powers of Analytic Functions

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ a normed space over $\mathbb{K}$, and $\mathbb{l}$ a normed field extension of $\mathbb{K}$. Given a function $f \colon E \to \mathbb{l}$ that is analytic on a set $s \subseteq E$, and an integer $n \geq 0$, the function $f^n$ is also analytic on $s$.

AnalyticOnNhd.fun_zpow_nonneg theorem

 {f : E → 𝕝} {s : Set E} {n : ℤ} (hf : AnalyticOnNhd 𝕜 f s) (hn : 0 ≤ n) : AnalyticOnNhd 𝕜 (fun x ↦ f x ^ n) s

Full source

/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic if the exponent is
nonnegative. -/
lemma AnalyticOnNhd.fun_zpow_nonneg {f : E → 𝕝} {s : Set E} {n : ℤ} (hf : AnalyticOnNhd 𝕜 f s)
    (hn : 0 ≤ n) :
    AnalyticOnNhd 𝕜 (fun x ↦ f x ^ n) s := by
  simp_rw [(Eq.symm (Int.toNat_of_nonneg hn) : n = OfNat.ofNat n.toNat), zpow_ofNat]
  apply pow hf

Analyticity of Nonnegative Integer Powers of Analytic Functions on Neighborhoods

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ a normed space over $\mathbb{K}$, and $\mathbb{l}$ a normed field extension of $\mathbb{K}$. Given a function $f \colon E \to \mathbb{l}$ that is analytic on a neighborhood of a set $s \subseteq E$, and an integer $n \geq 0$, the function $x \mapsto f(x)^n$ is also analytic on a neighborhood of $s$.

AnalyticOnNhd.zpow_nonneg theorem

{f : E → 𝕝} {s : Set E} {n : ℤ} (hf : AnalyticOnNhd 𝕜 f s) (hn : 0 ≤ n) : AnalyticOnNhd 𝕜 (f ^ n) s

Full source

/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic if the exponent is
nonnegative. -/
lemma AnalyticOnNhd.zpow_nonneg {f : E → 𝕝} {s : Set E} {n : ℤ} (hf : AnalyticOnNhd 𝕜 f s)
    (hn : 0 ≤ n) :
    AnalyticOnNhd 𝕜 (f ^ n) s :=
  fun_zpow_nonneg hf hn

Analyticity of Nonnegative Integer Powers of Analytic Functions on Neighborhoods (Pointwise Form)

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ a normed space over $\mathbb{K}$, and $\mathbb{l}$ a normed field extension of $\mathbb{K}$. Given a function $f \colon E \to \mathbb{l}$ that is analytic on a neighborhood of a set $s \subseteq E$, and an integer $n \geq 0$, the function $f^n$ is also analytic on a neighborhood of $s$.

HasFPowerSeriesWithinOnBall.restrictScalars theorem

(hf : HasFPowerSeriesWithinOnBall f p s x r) : HasFPowerSeriesWithinOnBall f (p.restrictScalars 𝕜) s x r

Full source

lemma HasFPowerSeriesWithinOnBall.restrictScalars (hf : HasFPowerSeriesWithinOnBall f p s x r) :
    HasFPowerSeriesWithinOnBall f (p.restrictScalars 𝕜) s x r :=
  ⟨hf.r_le.trans (FormalMultilinearSeries.radius_le_of_le (fun n ↦ by simp)), hf.r_pos, hf.hasSum⟩

Power Series Expansion Preserved Under Scalar Restriction

Informal description

Let $f: E \to F$ be a function with a formal power series expansion $p$ centered at $x$ with radius of convergence $r$ on a set $s$. Then the function $f$ also has a power series expansion when the coefficients are restricted to a subfield $\mathbb{K}$, with the same center $x$, set $s$, and radius $r$.

HasFPowerSeriesOnBall.restrictScalars theorem

(hf : HasFPowerSeriesOnBall f p x r) : HasFPowerSeriesOnBall f (p.restrictScalars 𝕜) x r

Full source

lemma HasFPowerSeriesOnBall.restrictScalars (hf : HasFPowerSeriesOnBall f p x r) :
    HasFPowerSeriesOnBall f (p.restrictScalars 𝕜) x r :=
  ⟨hf.r_le.trans (FormalMultilinearSeries.radius_le_of_le (fun n ↦ by simp)), hf.r_pos, hf.hasSum⟩

Preservation of Power Series Expansion Under Scalar Restriction

Informal description

Let $f: E \to F$ be a function with a formal power series expansion $p$ centered at $x$ with radius of convergence $r$. Then the function $f$ also has a power series expansion when the coefficients are restricted to a subfield $\mathbb{K}$, with the same center $x$ and radius $r$.

HasFPowerSeriesWithinAt.restrictScalars theorem

(hf : HasFPowerSeriesWithinAt f p s x) : HasFPowerSeriesWithinAt f (p.restrictScalars 𝕜) s x

Full source

lemma HasFPowerSeriesWithinAt.restrictScalars (hf : HasFPowerSeriesWithinAt f p s x) :
    HasFPowerSeriesWithinAt f (p.restrictScalars 𝕜) s x := by
  rcases hf with ⟨r, hr⟩
  exact ⟨r, hr.restrictScalars⟩

Power Series Expansion Preserved Under Scalar Restriction at a Point

Informal description

Let $f: E \to F$ be a function with a formal power series expansion $p$ centered at $x$ within a set $s$. Then the function $f$ also has a power series expansion when the coefficients are restricted to a subfield $\mathbb{K}$, with the same center $x$ and set $s$.

HasFPowerSeriesAt.restrictScalars theorem

(hf : HasFPowerSeriesAt f p x) : HasFPowerSeriesAt f (p.restrictScalars 𝕜) x

Full source

lemma HasFPowerSeriesAt.restrictScalars (hf : HasFPowerSeriesAt f p x) :
    HasFPowerSeriesAt f (p.restrictScalars 𝕜) x := by
  rcases hf with ⟨r, hr⟩
  exact ⟨r, hr.restrictScalars⟩

Power Series Expansion Preserved Under Scalar Restriction at a Point

Informal description

Let $f: E \to F$ be a function with a formal power series expansion $p$ centered at $x$. Then the function $f$ also has a power series expansion when the coefficients are restricted to a subfield $\mathbb{K}$, with the same center $x$.

AnalyticWithinAt.restrictScalars theorem

(hf : AnalyticWithinAt 𝕜' f s x) : AnalyticWithinAt 𝕜 f s x

Full source

lemma AnalyticWithinAt.restrictScalars (hf : AnalyticWithinAt 𝕜' f s x) :
    AnalyticWithinAt 𝕜 f s x := by
  rcases hf with ⟨p, hp⟩
  exact ⟨p.restrictScalars 𝕜, hp.restrictScalars⟩

Analyticity Preserved Under Scalar Restriction Within a Set

Informal description

Let $f: E \to F$ be a function that is analytic at a point $x$ within a set $s$ with respect to a field extension $\mathbb{K}'$ of $\mathbb{K}$. Then $f$ is also analytic at $x$ within $s$ with respect to the subfield $\mathbb{K}$.

AnalyticAt.restrictScalars theorem

(hf : AnalyticAt 𝕜' f x) : AnalyticAt 𝕜 f x

Full source

lemma AnalyticAt.restrictScalars (hf : AnalyticAt 𝕜' f x) :
    AnalyticAt 𝕜 f x := by
  rcases hf with ⟨p, hp⟩
  exact ⟨p.restrictScalars 𝕜, hp.restrictScalars⟩

Analyticity Preserved Under Scalar Restriction at a Point

Informal description

Let $f: E \to F$ be a function that is analytic at a point $x$ with respect to a field extension $\mathbb{K}'$ of $\mathbb{K}$. Then $f$ is also analytic at $x$ with respect to the subfield $\mathbb{K}$.

AnalyticOn.restrictScalars theorem

(hf : AnalyticOn 𝕜' f s) : AnalyticOn 𝕜 f s

Full source

lemma AnalyticOn.restrictScalars (hf : AnalyticOn 𝕜' f s) :
    AnalyticOn 𝕜 f s :=
  fun x hx ↦ (hf x hx).restrictScalars

Analyticity Preserved Under Scalar Restriction on a Set

Informal description

Let $f: E \to F$ be a function that is analytic on a set $s$ with respect to a field extension $\mathbb{K}'$ of $\mathbb{K}$. Then $f$ is also analytic on $s$ with respect to the subfield $\mathbb{K}$.

AnalyticOnNhd.restrictScalars theorem

(hf : AnalyticOnNhd 𝕜' f s) : AnalyticOnNhd 𝕜 f s

Full source

lemma AnalyticOnNhd.restrictScalars (hf : AnalyticOnNhd 𝕜' f s) :
    AnalyticOnNhd 𝕜 f s :=
  fun x hx ↦ (hf x hx).restrictScalars

Analyticity in Neighborhood Preserved Under Scalar Restriction

Informal description

Let $f: E \to F$ be a function that is analytic in a neighborhood of a point $x$ with respect to a field extension $\mathbb{K}'$ of $\mathbb{K}$. Then $f$ is also analytic in a neighborhood of $x$ with respect to the subfield $\mathbb{K}$.

formalMultilinearSeries_geometric definition

: FormalMultilinearSeries 𝕜 A A

Full source

/-- The geometric series `1 + x + x ^ 2 + ...` as a `FormalMultilinearSeries`. -/
def formalMultilinearSeries_geometric : FormalMultilinearSeries 𝕜 A A :=
  fun n ↦ ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A

Geometric formal multilinear series

Informal description

The geometric series $1 + x + x^2 + \cdots$ represented as a formal multilinear series over a field $\mathbb{K}$ with values in an algebra $A$. Specifically, for each $n$, the $n$-th term of the series is given by the continuous multilinear map that constructs the $n$-fold product in the algebra $A$.

formalMultilinearSeries_geometric_eq_ofScalars theorem

: formalMultilinearSeries_geometric 𝕜 A = FormalMultilinearSeries.ofScalars A fun _ ↦ (1 : 𝕜)

Full source

/-- The geometric series as an `ofScalars` series. -/
theorem formalMultilinearSeries_geometric_eq_ofScalars :
    formalMultilinearSeries_geometric 𝕜 A =
      FormalMultilinearSeries.ofScalars A fun _ ↦ (1 : 𝕜) := by
  simp_rw [FormalMultilinearSeries.ext_iff, FormalMultilinearSeries.ofScalars,
    formalMultilinearSeries_geometric, one_smul, implies_true]

Geometric Series as Scalar Multiple Series: $1 + x + x^2 + \cdots = \sum_n 1 \cdot x^n$

Informal description

The geometric formal multilinear series over a field $\mathbb{K}$ with values in an algebra $A$ is equal to the formal power series of scalar multiples where each coefficient is the multiplicative identity $1 \in \mathbb{K}$. That is, the series $1 + x + x^2 + \cdots$ can be represented as $\sum_{n} 1 \cdot x^n$.

formalMultilinearSeries_geometric_apply_norm_le theorem

(n : ℕ) : ‖formalMultilinearSeries_geometric 𝕜 A n‖ ≤ max 1 ‖(1 : A)‖

Full source

lemma formalMultilinearSeries_geometric_apply_norm_le (n : ℕ) :
    ‖formalMultilinearSeries_geometric 𝕜 A n‖ ≤ max 1 ‖(1 : A)‖ :=
  ContinuousMultilinearMap.norm_mkPiAlgebraFin_le

Norm Bound for Geometric Formal Multilinear Series: $\|(\text{geom\_series}_{\mathbb{K},A})_n\| \leq \max(1, \|1_A\|)$

Informal description

For any natural number $n$, the norm of the $n$-th term of the geometric formal multilinear series over a field $\mathbb{K}$ with values in a normed algebra $A$ is bounded by the maximum of 1 and the norm of the multiplicative identity in $A$, i.e., \[ \|(\text{formalMultilinearSeries\_geometric } \mathbb{K} A)_n\| \leq \max(1, \|1_A\|). \]

formalMultilinearSeries_geometric_apply_norm theorem

[NormOneClass A] (n : ℕ) : ‖formalMultilinearSeries_geometric 𝕜 A n‖ = 1

Full source

lemma formalMultilinearSeries_geometric_apply_norm [NormOneClass A] (n : ℕ) :
    ‖formalMultilinearSeries_geometric 𝕜 A n‖ = 1 :=
  ContinuousMultilinearMap.norm_mkPiAlgebraFin

Operator Norm Identity for Geometric Series Term: $\|(\text{formalMultilinearSeries\_geometric}_{\mathbb{K}}(A))_n\| = 1$

Informal description

For any natural number $n$, the operator norm of the $n$-th term of the geometric formal multilinear series over a field $\mathbb{K}$ with values in a normed algebra $A$ (satisfying $\|1\| = 1$) is equal to 1, i.e., \[ \|(\text{formalMultilinearSeries\_geometric}_{\mathbb{K}}(A))_n\| = 1. \]

one_le_formalMultilinearSeries_geometric_radius theorem

 (𝕜 : Type*) [NontriviallyNormedField 𝕜] (A : Type*) [NormedRing A] [NormedAlgebra 𝕜 A] :
  1 ≤ (formalMultilinearSeries_geometric 𝕜 A).radius

Full source

lemma one_le_formalMultilinearSeries_geometric_radius (𝕜 : Type*) [NontriviallyNormedField 𝕜]
    (A : Type*) [NormedRing A] [NormedAlgebra 𝕜 A] :
    1 ≤ (formalMultilinearSeries_geometric 𝕜 A).radius := by
  convert formalMultilinearSeries_geometric_eq_ofScalars 𝕜 A ▸
    FormalMultilinearSeries.ofScalars_radius_ge_inv_of_tendsto A _ one_ne_zero (by simp) |>.le
  simp

Lower bound for radius of convergence of geometric series: $\text{radius}(\sum x^n) \geq 1$

Informal description

For any nontrivially normed field $\mathbb{K}$ and any normed algebra $A$ over $\mathbb{K}$, the radius of convergence of the geometric formal multilinear series $\sum_{n=0}^\infty x^n$ is at least 1. That is, the series converges absolutely for all $x \in A$ with $\|x\| < 1$.

formalMultilinearSeries_geometric_radius theorem

 (𝕜 : Type*) [NontriviallyNormedField 𝕜] (A : Type*) [NormedRing A] [NormOneClass A] [NormedAlgebra 𝕜 A] :
  (formalMultilinearSeries_geometric 𝕜 A).radius = 1

Full source

lemma formalMultilinearSeries_geometric_radius (𝕜 : Type*) [NontriviallyNormedField 𝕜]
    (A : Type*) [NormedRing A] [NormOneClass A] [NormedAlgebra 𝕜 A] :
    (formalMultilinearSeries_geometric 𝕜 A).radius = 1 :=
  formalMultilinearSeries_geometric_eq_ofScalars 𝕜 A ▸
    FormalMultilinearSeries.ofScalars_radius_eq_of_tendsto A _ one_ne_zero (by simp)

Radius of Convergence of Geometric Series: $\text{radius}(\sum x^n) = 1$

Informal description

Let $\mathbb{K}$ be a nontrivially normed field and $A$ be a normed algebra over $\mathbb{K}$ with $\|1\| = 1$. The radius of convergence of the geometric formal multilinear series $\sum_{n=0}^\infty x^n$ is equal to $1$, i.e., \[ \text{radius}(\text{formalMultilinearSeries\_geometric}_{\mathbb{K}}(A)) = 1. \]

hasFPowerSeriesOnBall_inverse_one_sub theorem

 (𝕜 : Type*) [NontriviallyNormedField 𝕜] (A : Type*) [NormedRing A] [NormedAlgebra 𝕜 A] [HasSummableGeomSeries A] :
  HasFPowerSeriesOnBall (fun x : A ↦ Ring.inverse (1 - x)) (formalMultilinearSeries_geometric 𝕜 A) 0 1

Full source

lemma hasFPowerSeriesOnBall_inverse_one_sub
    (𝕜 : Type*) [NontriviallyNormedField 𝕜]
    (A : Type*) [NormedRing A] [NormedAlgebra 𝕜 A] [HasSummableGeomSeries A] :
    HasFPowerSeriesOnBall (fun x : A ↦ Ring.inverse (1 - x))
      (formalMultilinearSeries_geometric 𝕜 A) 0 1 := by
  constructor
  · exact one_le_formalMultilinearSeries_geometric_radius 𝕜 A
  · exact one_pos
  · intro y hy
    simp only [EMetric.mem_ball, edist_dist, dist_zero_right, ofReal_lt_one] at hy
    simp only [zero_add, NormedRing.inverse_one_sub _ hy, Units.oneSub, Units.inv_mk,
      formalMultilinearSeries_geometric, ContinuousMultilinearMap.mkPiAlgebraFin_apply,
      List.ofFn_const, List.prod_replicate]
    exact (summable_geometric_of_norm_lt_one hy).hasSum

Power Series Expansion of $(1 - x)^{-1}$ as Geometric Series in Normed Algebras

Informal description

Let $\mathbb{K}$ be a nontrivially normed field and $A$ be a normed algebra over $\mathbb{K}$ with summable geometric series. The function $x \mapsto (1 - x)^{-1}$ has a formal power series expansion given by the geometric series $\sum_{n=0}^\infty x^n$ on the ball of radius 1 centered at 0 in $A$.

analyticAt_inverse_one_sub theorem

 (𝕜 : Type*) [NontriviallyNormedField 𝕜] (A : Type*) [NormedRing A] [NormedAlgebra 𝕜 A] [HasSummableGeomSeries A] :
  AnalyticAt 𝕜 (fun x : A ↦ Ring.inverse (1 - x)) 0

Full source

@[fun_prop]
lemma analyticAt_inverse_one_sub (𝕜 : Type*) [NontriviallyNormedField 𝕜]
    (A : Type*) [NormedRing A] [NormedAlgebra 𝕜 A] [HasSummableGeomSeries A] :
    AnalyticAt 𝕜 (fun x : A ↦ Ring.inverse (1 - x)) 0 :=
  ⟨_, ⟨_, hasFPowerSeriesOnBall_inverse_one_sub 𝕜 A⟩⟩

Analyticity of $(1 - x)^{-1}$ at zero in normed algebras with summable geometric series

Informal description

Let $\mathbb{K}$ be a nontrivially normed field and $A$ be a normed algebra over $\mathbb{K}$ with summable geometric series. Then the function $x \mapsto (1 - x)^{-1}$ is analytic at $0 \in A$.

analyticAt_inverse theorem

 {𝕜 : Type*} [NontriviallyNormedField 𝕜] {A : Type*} [NormedRing A] [NormedAlgebra 𝕜 A] [HasSummableGeomSeries A]
  (z : Aˣ) : AnalyticAt 𝕜 Ring.inverse (z : A)

Full source

/-- If `A` is a normed algebra over `𝕜` with summable geometric series, then inversion on `A` is
analytic at any unit. -/
@[fun_prop]
lemma analyticAt_inverse {𝕜 : Type*} [NontriviallyNormedField 𝕜]
    {A : Type*} [NormedRing A] [NormedAlgebra 𝕜 A] [HasSummableGeomSeries A] (z : Aˣ) :
    AnalyticAt 𝕜 Ring.inverse (z : A) := by
  rcases subsingleton_or_nontrivial A with hA|hA
  · convert analyticAt_const (v := (0 : A))
  · let f1 : A → A := fun a ↦ a * z.inv
    let f2 : A → A := fun b ↦ Ring.inverse (1 - b)
    let f3 : A → A := fun c ↦ 1 - z.inv * c
    have feq : ∀ᶠ y in 𝓝 (z : A), (f1 ∘ f2 ∘ f3) y = Ring.inverse y := by
      have : Metric.ballMetric.ball (z : A) (‖(↑z⁻¹ : A)‖⁻¹) ∈ 𝓝 (z : A) := by
        apply Metric.ball_mem_nhds
        simp
      filter_upwards [this] with y hy
      simp only [Metric.mem_ball, dist_eq_norm] at hy
      have : y = Units.ofNearby z y hy := rfl
      rw [this, Eq.comm]
      simp only [Ring.inverse_unit, Function.comp_apply]
      simp [Units.ofNearby, f1, f2, f3, Units.add, _root_.mul_sub]
      rw [← Ring.inverse_unit]
      congr
      simp
    apply AnalyticAt.congr _ feq
    apply (analyticAt_id.mul analyticAt_const).comp
    apply AnalyticAt.comp
    · simp only [Units.inv_eq_val_inv, Units.inv_mul, sub_self, f2, f3]
      exact analyticAt_inverse_one_sub 𝕜 A
    · exact analyticAt_const.sub (analyticAt_const.mul analyticAt_id)

Analyticity of Inversion at Units in Normed Algebras with Summable Geometric Series

Informal description

Let $\mathbb{K}$ be a nontrivially normed field and $A$ be a normed algebra over $\mathbb{K}$ with summable geometric series. For any unit $z$ in $A$, the inversion function $x \mapsto x^{-1}$ is analytic at $z$.

analyticOnNhd_inverse theorem

 {𝕜 : Type*} [NontriviallyNormedField 𝕜] {A : Type*} [NormedRing A] [NormedAlgebra 𝕜 A] [HasSummableGeomSeries A] :
  AnalyticOnNhd 𝕜 Ring.inverse {x : A | IsUnit x}

Full source

lemma analyticOnNhd_inverse {𝕜 : Type*} [NontriviallyNormedField 𝕜]
    {A : Type*} [NormedRing A] [NormedAlgebra 𝕜 A] [HasSummableGeomSeries A] :
    AnalyticOnNhd 𝕜 Ring.inverse {x : A | IsUnit x} :=
  fun _ hx ↦ analyticAt_inverse (IsUnit.unit hx)

Analyticity of Inversion on Units in Normed Algebras with Summable Geometric Series

Informal description

Let $\mathbb{K}$ be a nontrivially normed field and $A$ be a normed algebra over $\mathbb{K}$ with summable geometric series. The inversion function $x \mapsto x^{-1}$ is analytic on a neighborhood of every unit $x \in A$.

hasFPowerSeriesOnBall_inv_one_sub theorem

 (𝕜 𝕝 : Type*) [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕝] [NormedAlgebra 𝕜 𝕝] :
  HasFPowerSeriesOnBall (fun x : 𝕝 ↦ (1 - x)⁻¹) (formalMultilinearSeries_geometric 𝕜 𝕝) 0 1

Full source

lemma hasFPowerSeriesOnBall_inv_one_sub
    (𝕜 𝕝 : Type*) [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕝] [NormedAlgebra 𝕜 𝕝] :
    HasFPowerSeriesOnBall (fun x : 𝕝 ↦ (1 - x)⁻¹) (formalMultilinearSeries_geometric 𝕜 𝕝) 0 1 := by
  convert hasFPowerSeriesOnBall_inverse_one_sub 𝕜 𝕝
  exact Ring.inverse_eq_inv'.symm

Power Series Expansion of $(1 - x)^{-1}$ as Geometric Series in Normed Algebras

Informal description

Let $\mathbb{K}$ and $\mathbb{L}$ be nontrivially normed fields with $\mathbb{L}$ as a normed algebra over $\mathbb{K}$. The function $x \mapsto (1 - x)^{-1}$ has a formal power series expansion given by the geometric series $\sum_{n=0}^\infty x^n$ on the ball of radius 1 centered at 0 in $\mathbb{L}$.

analyticAt_inv_one_sub theorem

 (𝕝 : Type*) [NontriviallyNormedField 𝕝] [NormedAlgebra 𝕜 𝕝] : AnalyticAt 𝕜 (fun x : 𝕝 ↦ (1 - x)⁻¹) 0

Full source

@[fun_prop]
lemma analyticAt_inv_one_sub (𝕝 : Type*) [NontriviallyNormedField 𝕝] [NormedAlgebra 𝕜 𝕝] :
    AnalyticAt 𝕜 (fun x : 𝕝 ↦ (1 - x)⁻¹) 0 :=
  ⟨_, ⟨_, hasFPowerSeriesOnBall_inv_one_sub 𝕜 𝕝⟩⟩

Analyticity of $(1 - x)^{-1}$ at Zero in Normed Algebras

Informal description

Let $\mathbb{L}$ be a nontrivially normed field and a normed algebra over $\mathbb{K}$. The function $x \mapsto (1 - x)^{-1}$ is analytic at $x = 0$ in $\mathbb{L}$.

analyticAt_inv theorem

{z : 𝕝} (hz : z ≠ 0) : AnalyticAt 𝕜 Inv.inv z

Full source

/-- If `𝕝` is a normed field extension of `𝕜`, then the inverse map `𝕝 → 𝕝` is `𝕜`-analytic
away from 0. -/
@[fun_prop]
lemma analyticAt_inv {z : 𝕝} (hz : z ≠ 0) : AnalyticAt 𝕜 Inv.inv z := by
  convert analyticAt_inverse (𝕜 := 𝕜) (Units.mk0 _ hz)
  exact Ring.inverse_eq_inv'.symm

Analyticity of Inversion at Nonzero Points in Normed Field Extensions

Informal description

Let $\mathbb{K}$ be a nontrivially normed field and $\mathbb{L}$ be a normed field extension of $\mathbb{K}$. For any nonzero element $z \in \mathbb{L}$, the inversion function $x \mapsto x^{-1}$ is $\mathbb{K}$-analytic at $z$.

analyticOnNhd_inv theorem

: AnalyticOnNhd 𝕜 (fun z ↦ z⁻¹) {z : 𝕝 | z ≠ 0}

Full source

/-- `x⁻¹` is analytic away from zero -/
lemma analyticOnNhd_inv : AnalyticOnNhd 𝕜 (fun z ↦ z⁻¹) {z : 𝕝 | z ≠ 0} := by
  intro z m; exact analyticAt_inv m

Analyticity of Inversion on Nonzero Neighborhood in Normed Field Extensions

Informal description

Let $\mathbb{K}$ be a nontrivially normed field and $\mathbb{L}$ be a normed field extension of $\mathbb{K}$. The inversion function $z \mapsto z^{-1}$ is $\mathbb{K}$-analytic on the neighborhood $\{z \in \mathbb{L} \mid z \neq 0\}$ of all nonzero elements in $\mathbb{L}$.

analyticOn_inv theorem

: AnalyticOn 𝕜 (fun z ↦ z⁻¹) {z : 𝕝 | z ≠ 0}

Full source

lemma analyticOn_inv : AnalyticOn 𝕜 (fun z ↦ z⁻¹) {z : 𝕝 | z ≠ 0} :=
  analyticOnNhd_inv.analyticOn

Analyticity of Inversion on Nonzero Elements in Normed Field Extensions

Informal description

Let $\mathbb{K}$ be a nontrivially normed field and $\mathbb{L}$ be a normed field extension of $\mathbb{K}$. The inversion function $z \mapsto z^{-1}$ is $\mathbb{K}$-analytic on the set $\{z \in \mathbb{L} \mid z \neq 0\}$ of all nonzero elements in $\mathbb{L}$.

AnalyticWithinAt.fun_inv theorem

 {f : E → 𝕝} {x : E} {s : Set E} (fa : AnalyticWithinAt 𝕜 f s x) (f0 : f x ≠ 0) :
  AnalyticWithinAt 𝕜 (fun x ↦ (f x)⁻¹) s x

Full source

/-- `(f x)⁻¹` is analytic away from `f x = 0` -/
theorem AnalyticWithinAt.fun_inv {f : E → 𝕝} {x : E} {s : Set E} (fa : AnalyticWithinAt 𝕜 f s x)
    (f0 : f x ≠ 0) :
    AnalyticWithinAt 𝕜 (fun x ↦ (f x)⁻¹) s x :=
  (analyticAt_inv f0).comp_analyticWithinAt fa

Analyticity of Pointwise Inversion for Analytic Functions

Informal description

Let $f : E \to \mathbb{L}$ be a function defined on a set $E$ with values in a normed field extension $\mathbb{L}$ of a nontrivially normed field $\mathbb{K}$. If $f$ is $\mathbb{K}$-analytic within a set $s \subseteq E$ at a point $x \in E$, and $f(x) \neq 0$, then the function $x \mapsto (f(x))^{-1}$ is also $\mathbb{K}$-analytic within $s$ at $x$.

AnalyticWithinAt.inv theorem

 {f : E → 𝕝} {x : E} {s : Set E} (fa : AnalyticWithinAt 𝕜 f s x) (f0 : f x ≠ 0) : AnalyticWithinAt 𝕜 f⁻¹ s x

Full source

/-- `(f x)⁻¹` is analytic away from `f x = 0` -/
theorem AnalyticWithinAt.inv {f : E → 𝕝} {x : E} {s : Set E} (fa : AnalyticWithinAt 𝕜 f s x)
    (f0 : f x ≠ 0) :
    AnalyticWithinAt 𝕜 f⁻¹ s x :=
  fun_inv fa f0

Analyticity of Pointwise Inverse Within a Set at Nonzero Points

Informal description

Let $E$ be a normed vector space over a nontrivially normed field $\mathbb{K}$, and let $\mathbb{L}$ be a normed field extension of $\mathbb{K}$. For a function $f : E \to \mathbb{L}$ that is $\mathbb{K}$-analytic within a set $s \subseteq E$ at a point $x \in E$, if $f(x) \neq 0$, then the pointwise inverse function $f^{-1}$ is also $\mathbb{K}$-analytic within $s$ at $x$.

AnalyticAt.fun_inv theorem

{f : E → 𝕝} {x : E} (fa : AnalyticAt 𝕜 f x) (f0 : f x ≠ 0) : AnalyticAt 𝕜 (fun x ↦ (f x)⁻¹) x

Full source

/-- `(f x)⁻¹` is analytic away from `f x = 0` -/
@[fun_prop]
theorem AnalyticAt.fun_inv {f : E → 𝕝} {x : E} (fa : AnalyticAt 𝕜 f x) (f0 : f x ≠ 0) :
    AnalyticAt 𝕜 (fun x ↦ (f x)⁻¹) x :=
  (analyticAt_inv f0).comp fa

Analyticity of pointwise inversion at nonzero points

Informal description

Let $E$ be a normed vector space over a nontrivially normed field $\mathbb{K}$, and let $\mathbb{L}$ be a normed field extension of $\mathbb{K}$. For a function $f : E \to \mathbb{L}$ that is $\mathbb{K}$-analytic at a point $x \in E$, if $f(x) \neq 0$, then the function $x \mapsto (f(x))^{-1}$ is also $\mathbb{K}$-analytic at $x$.

AnalyticAt.inv theorem

{f : E → 𝕝} {x : E} (fa : AnalyticAt 𝕜 f x) (f0 : f x ≠ 0) : AnalyticAt 𝕜 f⁻¹ x

Full source

/-- `(f x)⁻¹` is analytic away from `f x = 0` -/
@[fun_prop]
theorem AnalyticAt.inv {f : E → 𝕝} {x : E} (fa : AnalyticAt 𝕜 f x) (f0 : f x ≠ 0) :
    AnalyticAt 𝕜 f⁻¹ x :=
  fa.fun_inv f0

Analyticity of Function Inversion at Nonzero Points

Informal description

Let $E$ be a normed vector space over a nontrivially normed field $\mathbb{K}$, and let $\mathbb{L}$ be a normed field extension of $\mathbb{K}$. For a function $f : E \to \mathbb{L}$ that is $\mathbb{K}$-analytic at a point $x \in E$, if $f(x) \neq 0$, then the function $f^{-1}$ is also $\mathbb{K}$-analytic at $x$.

AnalyticOn.fun_inv theorem

 {f : E → 𝕝} {s : Set E} (fa : AnalyticOn 𝕜 f s) (f0 : ∀ x ∈ s, f x ≠ 0) : AnalyticOn 𝕜 (fun x ↦ (f x)⁻¹) s

Full source

/-- `(f x)⁻¹` is analytic away from `f x = 0` -/
theorem AnalyticOn.fun_inv {f : E → 𝕝} {s : Set E} (fa : AnalyticOn 𝕜 f s) (f0 : ∀ x ∈ s, f x ≠ 0) :
    AnalyticOn 𝕜 (fun x ↦ (f x)⁻¹) s :=
  fun x m ↦ (fa x m).inv (f0 x m)

Analyticity of Pointwise Inversion on a Set Where Function is Nonzero

Informal description

Let $E$ be a normed vector space over a nontrivially normed field $\mathbb{K}$, and let $\mathbb{L}$ be a normed field extension of $\mathbb{K}$. For a function $f : E \to \mathbb{L}$ that is $\mathbb{K}$-analytic on a set $s \subseteq E$, if $f(x) \neq 0$ for all $x \in s$, then the function $x \mapsto (f(x))^{-1}$ is also $\mathbb{K}$-analytic on $s$.

AnalyticOn.inv theorem

{f : E → 𝕝} {s : Set E} (fa : AnalyticOn 𝕜 f s) (f0 : ∀ x ∈ s, f x ≠ 0) : AnalyticOn 𝕜 f⁻¹ s

Full source

/-- `(f x)⁻¹` is analytic away from `f x = 0` -/
theorem AnalyticOn.inv {f : E → 𝕝} {s : Set E} (fa : AnalyticOn 𝕜 f s) (f0 : ∀ x ∈ s, f x ≠ 0) :
    AnalyticOn 𝕜 f⁻¹ s :=
  fun_inv fa f0

Analyticity of Multiplicative Inverse on Nonzero Sets

Informal description

Let $E$ be a normed vector space over a nontrivially normed field $\mathbb{K}$, and let $\mathbb{L}$ be a normed field extension of $\mathbb{K}$. For a function $f : E \to \mathbb{L}$ that is $\mathbb{K}$-analytic on a set $s \subseteq E$, if $f(x) \neq 0$ for all $x \in s$, then the multiplicative inverse function $f^{-1}$ is also $\mathbb{K}$-analytic on $s$.

AnalyticOnNhd.fun_inv theorem

 {f : E → 𝕝} {s : Set E} (fa : AnalyticOnNhd 𝕜 f s) (f0 : ∀ x ∈ s, f x ≠ 0) : AnalyticOnNhd 𝕜 (fun x ↦ (f x)⁻¹) s

Full source

/-- `(f x)⁻¹` is analytic away from `f x = 0` -/
theorem AnalyticOnNhd.fun_inv {f : E → 𝕝} {s : Set E} (fa : AnalyticOnNhd 𝕜 f s)
    (f0 : ∀ x ∈ s, f x ≠ 0) :
    AnalyticOnNhd 𝕜 (fun x ↦ (f x)⁻¹) s :=
  fun x m ↦ (fa x m).inv (f0 x m)

Analyticity of Pointwise Inversion on Neighborhoods of Nonzero Points

Informal description

Let $E$ be a normed vector space over a nontrivially normed field $\mathbb{K}$, and let $\mathbb{L}$ be a normed field extension of $\mathbb{K}$. For a function $f : E \to \mathbb{L}$ that is $\mathbb{K}$-analytic in a neighborhood of each point in a set $s \subseteq E$, if $f(x) \neq 0$ for all $x \in s$, then the function $x \mapsto (f(x))^{-1}$ is also $\mathbb{K}$-analytic in a neighborhood of each point in $s$.

AnalyticOnNhd.inv theorem

{f : E → 𝕝} {s : Set E} (fa : AnalyticOnNhd 𝕜 f s) (f0 : ∀ x ∈ s, f x ≠ 0) : AnalyticOnNhd 𝕜 f⁻¹ s

Full source

/-- `(f x)⁻¹` is analytic away from `f x = 0` -/
theorem AnalyticOnNhd.inv {f : E → 𝕝} {s : Set E} (fa : AnalyticOnNhd 𝕜 f s)
    (f0 : ∀ x ∈ s, f x ≠ 0) :
    AnalyticOnNhd 𝕜 f⁻¹ s :=
  fun_inv fa f0

Analyticity of Pointwise Inverse Function on Neighborhoods of Nonzero Points

Informal description

Let $E$ be a normed vector space over a nontrivially normed field $\mathbb{K}$, and let $\mathbb{L}$ be a normed field extension of $\mathbb{K}$. For a function $f : E \to \mathbb{L}$ that is $\mathbb{K}$-analytic in a neighborhood of each point in a set $s \subseteq E$, if $f(x) \neq 0$ for all $x \in s$, then the pointwise inverse function $f^{-1}$ is also $\mathbb{K}$-analytic in a neighborhood of each point in $s$.

AnalyticWithinAt.fun_zpow theorem

 {f : E → 𝕝} {z : E} {s : Set E} {n : ℤ} (h₁f : AnalyticWithinAt 𝕜 f s z) (h₂f : f z ≠ 0) :
  AnalyticWithinAt 𝕜 (fun x ↦ f x ^ n) s z

Full source

/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
-/
lemma AnalyticWithinAt.fun_zpow {f : E → 𝕝} {z : E} {s : Set E} {n : ℤ}
    (h₁f : AnalyticWithinAt 𝕜 f s z) (h₂f : f z ≠ 0) :
    AnalyticWithinAt 𝕜 (fun x ↦ f x ^ n) s z := by
  by_cases hn : 0 ≤ n
  · exact zpow_nonneg h₁f hn
  · rw [(Int.eq_neg_comm.mp rfl : n = - (- n))]
    conv => arg 2; intro x; rw [zpow_neg]
    exact (h₁f.zpow_nonneg (by linarith)).inv (zpow_ne_zero (-n) h₂f)

Analyticity of Integer Powers of Analytic Functions (Pointwise Version) at Nonzero Points

Informal description

Let $E$ be a normed vector space over a nontrivially normed field $\mathbb{K}$, and let $\mathbb{L}$ be a normed field extension of $\mathbb{K}$. For a function $f \colon E \to \mathbb{L}$ that is $\mathbb{K}$-analytic within a set $s \subseteq E$ at a point $z \in E$, if $f(z) \neq 0$, then for any integer $n$, the function $x \mapsto f(x)^n$ is also $\mathbb{K}$-analytic within $s$ at $z$.

AnalyticWithinAt.zpow theorem

 {f : E → 𝕝} {z : E} {s : Set E} {n : ℤ} (h₁f : AnalyticWithinAt 𝕜 f s z) (h₂f : f z ≠ 0) :
  AnalyticWithinAt 𝕜 (f ^ n) s z

Full source

/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
-/
lemma AnalyticWithinAt.zpow {f : E → 𝕝} {z : E} {s : Set E} {n : ℤ}
    (h₁f : AnalyticWithinAt 𝕜 f s z) (h₂f : f z ≠ 0) :
    AnalyticWithinAt 𝕜 (f ^ n) s z :=
  fun_zpow h₁f h₂f

Analyticity of Integer Powers of Analytic Functions at Nonzero Points

Informal description

Let $E$ be a normed vector space over a nontrivially normed field $\mathbb{K}$, and let $\mathbb{L}$ be a normed field extension of $\mathbb{K}$. For a function $f \colon E \to \mathbb{L}$ that is $\mathbb{K}$-analytic within a set $s \subseteq E$ at a point $z \in E$, if $f(z) \neq 0$, then for any integer $n$, the function $f^n$ is also $\mathbb{K}$-analytic within $s$ at $z$.

AnalyticAt.fun_zpow theorem

 {f : E → 𝕝} {z : E} {n : ℤ} (h₁f : AnalyticAt 𝕜 f z) (h₂f : f z ≠ 0) : AnalyticAt 𝕜 (fun x ↦ f x ^ n) z

Full source

/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
-/
lemma AnalyticAt.fun_zpow {f : E → 𝕝} {z : E} {n : ℤ}  (h₁f : AnalyticAt 𝕜 f z) (h₂f : f z ≠ 0) :
    AnalyticAt 𝕜 (fun x ↦ f x ^ n) z := by
  by_cases hn : 0 ≤ n
  · exact zpow_nonneg h₁f hn
  · rw [(Int.eq_neg_comm.mp rfl : n = - (- n))]
    conv => arg 2; intro x; rw [zpow_neg]
    exact (h₁f.zpow_nonneg (by linarith)).inv (zpow_ne_zero (-n) h₂f)

Analyticity of Integer Powers at Nonzero Points: $x \mapsto f(x)^n$ is analytic when $f$ is analytic and $f(z) \neq 0$

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ a normed space over $\mathbb{K}$, and $\mathbb{L}$ a normed field extension of $\mathbb{K}$. Given a function $f \colon E \to \mathbb{L}$ that is analytic at a point $z \in E$, and an integer $n \in \mathbb{Z}$, if $f(z) \neq 0$, then the function $x \mapsto f(x)^n$ is also analytic at $z$.

AnalyticAt.zpow theorem

{f : E → 𝕝} {z : E} {n : ℤ} (h₁f : AnalyticAt 𝕜 f z) (h₂f : f z ≠ 0) : AnalyticAt 𝕜 (f ^ n) z

Full source

/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
-/
lemma AnalyticAt.zpow {f : E → 𝕝} {z : E} {n : ℤ} (h₁f : AnalyticAt 𝕜 f z) (h₂f : f z ≠ 0) :
    AnalyticAt 𝕜 (f ^ n) z := by
  exact fun_zpow h₁f h₂f

Analyticity of Integer Powers at Nonzero Points: $f^n$ is analytic when $f$ is analytic and $f(z) \neq 0$

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ a normed space over $\mathbb{K}$, and $\mathbb{L}$ a normed field extension of $\mathbb{K}$. Given a function $f \colon E \to \mathbb{L}$ that is analytic at a point $z \in E$, and an integer $n \in \mathbb{Z}$, if $f(z) \neq 0$, then the function $f^n$ is also analytic at $z$.

AnalyticOn.fun_zpow theorem

 {f : E → 𝕝} {s : Set E} {n : ℤ} (h₁f : AnalyticOn 𝕜 f s) (h₂f : ∀ z ∈ s, f z ≠ 0) : AnalyticOn 𝕜 (fun x ↦ f x ^ n) s

Full source

/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
-/
lemma AnalyticOn.fun_zpow {f : E → 𝕝} {s : Set E} {n : ℤ} (h₁f : AnalyticOn 𝕜 f s)
    (h₂f : ∀ z ∈ s, f z ≠ 0) :
    AnalyticOn 𝕜 (fun x ↦ f x ^ n) s :=
  fun z hz ↦ (h₁f z hz).zpow (h₂f z hz)

Analyticity of Integer Powers on Nonzero Sets: $x \mapsto f(x)^n$ is analytic when $f$ is analytic and nonzero on $s$

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ a normed space over $\mathbb{K}$, and $\mathbb{L}$ a normed field extension of $\mathbb{K}$. Given a function $f \colon E \to \mathbb{L}$ that is $\mathbb{K}$-analytic on a set $s \subseteq E$, and an integer $n \in \mathbb{Z}$, if $f(z) \neq 0$ for all $z \in s$, then the function $x \mapsto f(x)^n$ is also $\mathbb{K}$-analytic on $s$.

AnalyticOn.zpow theorem

 {f : E → 𝕝} {s : Set E} {n : ℤ} (h₁f : AnalyticOn 𝕜 f s) (h₂f : ∀ z ∈ s, f z ≠ 0) : AnalyticOn 𝕜 (f ^ n) s

Full source

/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
-/
lemma AnalyticOn.zpow {f : E → 𝕝} {s : Set E} {n : ℤ}  (h₁f : AnalyticOn 𝕜 f s)
    (h₂f : ∀ z ∈ s, f z ≠ 0) :
    AnalyticOn 𝕜 (f ^ n) s := by
  exact fun_zpow h₁f h₂f

Analyticity of Integer Powers on Nonzero Sets: $f^n$ is analytic when $f$ is analytic and nonzero on $s$

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ a normed space over $\mathbb{K}$, and $\mathbb{L}$ a normed field extension of $\mathbb{K}$. Given a function $f \colon E \to \mathbb{L}$ that is $\mathbb{K}$-analytic on a set $s \subseteq E$, and an integer $n \in \mathbb{Z}$, if $f(z) \neq 0$ for all $z \in s$, then the function $f^n$ is also $\mathbb{K}$-analytic on $s$.

AnalyticOnNhd.fun_zpow theorem

 {f : E → 𝕝} {s : Set E} {n : ℤ} (h₁f : AnalyticOnNhd 𝕜 f s) (h₂f : ∀ z ∈ s, f z ≠ 0) :
  AnalyticOnNhd 𝕜 (fun x ↦ f x ^ n) s

Full source

/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
-/
lemma AnalyticOnNhd.fun_zpow {f : E → 𝕝} {s : Set E} {n : ℤ} (h₁f : AnalyticOnNhd 𝕜 f s)
    (h₂f : ∀ z ∈ s, f z ≠ 0) :
    AnalyticOnNhd 𝕜 (fun x ↦ f x ^ n) s :=
  fun z hz ↦ (h₁f z hz).zpow (h₂f z hz)

Analyticity of Integer Powers on Neighborhoods of Nonzero Points

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ a normed space over $\mathbb{K}$, and $\mathbb{L}$ a normed field extension of $\mathbb{K}$. Given a function $f \colon E \to \mathbb{L}$ that is analytic on a neighborhood of each point in a set $s \subseteq E$, and an integer $n \in \mathbb{Z}$, if $f(z) \neq 0$ for all $z \in s$, then the function $x \mapsto f(x)^n$ is also analytic on a neighborhood of each point in $s$.

AnalyticOnNhd.zpow theorem

 {f : E → 𝕝} {s : Set E} {n : ℤ} (h₁f : AnalyticOnNhd 𝕜 f s) (h₂f : ∀ z ∈ s, f z ≠ 0) : AnalyticOnNhd 𝕜 (f ^ n) s

Full source

/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
-/
lemma AnalyticOnNhd.zpow {f : E → 𝕝} {s : Set E} {n : ℤ} (h₁f : AnalyticOnNhd 𝕜 f s)
    (h₂f : ∀ z ∈ s, f z ≠ 0) :
    AnalyticOnNhd 𝕜 (f ^ n) s :=
  fun_zpow h₁f h₂f

Analyticity of Integer Powers on Neighborhoods of Nonzero Points

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ a normed space over $\mathbb{K}$, and $\mathbb{L}$ a normed field extension of $\mathbb{K}$. Given a function $f \colon E \to \mathbb{L}$ that is analytic on a neighborhood of each point in a set $s \subseteq E$, and an integer $n \in \mathbb{Z}$, if $f(z) \neq 0$ for all $z \in s$, then the function $f^n$ is also analytic on a neighborhood of each point in $s$.

analyticAt_iff_analytic_fun_smul theorem

 [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {z : E} (h₁f : AnalyticAt 𝕜 f z) (h₂f : f z ≠ 0) :
  AnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (fun z ↦ f z • g z) z

Full source

theorem analyticAt_iff_analytic_fun_smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝}
    {g : E → F} {z : E} (h₁f : AnalyticAt 𝕜 f z) (h₂f : f z ≠ 0) :
    AnalyticAtAnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (fun z ↦ f z • g z) z := by
  constructor
  · exact fun a ↦ h₁f.smul a
  · intro hprod
    rw [analyticAt_congr (g := (f⁻¹ • f) • g), smul_assoc]
    · exact (h₁f.inv h₂f).fun_smul hprod
    · filter_upwards [h₁f.continuousAt.preimage_mem_nhds (compl_singleton_mem_nhds_iff.2 h₂f)]
      intro y hy
      rw [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff] at hy
      simp [hy]

Analyticity Criterion via Scalar Multiplication: $g$ analytic $\iff$ $f \cdot g$ analytic

Informal description

Let $\mathbb{K}$ and $\mathbb{L}$ be normed fields with $\mathbb{K}$ as a subfield of $\mathbb{L}$, and let $E$ and $F$ be normed spaces over $\mathbb{L}$ that are also normed spaces over $\mathbb{K}$ via restriction of scalars. Given functions $f \colon E \to \mathbb{L}$ and $g \colon E \to F$ such that $f$ is $\mathbb{K}$-analytic at $z \in E$ and $f(z) \neq 0$, then $g$ is $\mathbb{K}$-analytic at $z$ if and only if the function $z \mapsto f(z) \cdot g(z)$ is $\mathbb{K}$-analytic at $z$.

analyticAt_iff_analytic_smul theorem

 [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {z : E} (h₁f : AnalyticAt 𝕜 f z) (h₂f : f z ≠ 0) :
  AnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (f • g) z

Full source

theorem analyticAt_iff_analytic_smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝}
    {g : E → F} {z : E} (h₁f : AnalyticAt 𝕜 f z) (h₂f : f z ≠ 0) :
    AnalyticAtAnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (f • g) z :=
  analyticAt_iff_analytic_fun_smul h₁f h₂f

Analyticity Criterion via Scalar Multiplication: $g$ analytic $\iff$ $f \cdot g$ analytic

Informal description

Let $\mathbb{K}$ and $\mathbb{L}$ be normed fields with $\mathbb{K}$ as a subfield of $\mathbb{L}$, and let $E$ and $F$ be normed spaces over $\mathbb{L}$ that are also normed spaces over $\mathbb{K}$ via restriction of scalars. Given functions $f \colon E \to \mathbb{L}$ and $g \colon E \to F$ such that $f$ is $\mathbb{K}$-analytic at $z \in E$ and $f(z) \neq 0$, then $g$ is $\mathbb{K}$-analytic at $z$ if and only if the scalar multiplication $f \cdot g$ is $\mathbb{K}$-analytic at $z$.

analyticAt_iff_analytic_fun_mul theorem

 {f g : E → 𝕝} {z : E} (h₁f : AnalyticAt 𝕜 f z) (h₂f : f z ≠ 0) : AnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (fun z ↦ f z * g z) z

Full source

theorem analyticAt_iff_analytic_fun_mul {f g : E → 𝕝} {z : E} (h₁f : AnalyticAt 𝕜 f z)
    (h₂f : f z ≠ 0) :
    AnalyticAtAnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (fun z ↦ f z * g z) z := by
  simp_rw [← smul_eq_mul]
  exact analyticAt_iff_analytic_smul h₁f h₂f

Analyticity Criterion via Pointwise Multiplication: $g$ analytic $\iff$ $f \cdot g$ analytic

Informal description

Let $\mathbb{K}$ and $\mathbb{L}$ be normed fields with $\mathbb{K}$ as a subfield of $\mathbb{L}$, and let $E$ be a normed space over $\mathbb{L}$. Given functions $f, g \colon E \to \mathbb{L}$ and a point $z \in E$ such that $f$ is $\mathbb{K}$-analytic at $z$ and $f(z) \neq 0$, then $g$ is $\mathbb{K}$-analytic at $z$ if and only if the function $z \mapsto f(z) \cdot g(z)$ is $\mathbb{K}$-analytic at $z$.

analyticAt_iff_analytic_mul theorem

 {f g : E → 𝕝} {z : E} (h₁f : AnalyticAt 𝕜 f z) (h₂f : f z ≠ 0) : AnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (f * g) z

Full source

theorem analyticAt_iff_analytic_mul {f g : E → 𝕝} {z : E} (h₁f : AnalyticAt 𝕜 f z)
    (h₂f : f z ≠ 0) :
    AnalyticAtAnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (f * g) z :=
  analyticAt_iff_analytic_fun_mul h₁f h₂f

Analyticity Criterion via Multiplication: $g$ analytic $\iff$ $f \cdot g$ analytic

Informal description

Let $\mathbb{K}$ and $\mathbb{L}$ be normed fields with $\mathbb{K}$ as a subfield of $\mathbb{L}$, and let $E$ be a normed space over $\mathbb{L}$. Given functions $f, g \colon E \to \mathbb{L}$ and a point $z \in E$ such that $f$ is $\mathbb{K}$-analytic at $z$ and $f(z) \neq 0$, then $g$ is $\mathbb{K}$-analytic at $z$ if and only if the product function $f \cdot g$ is $\mathbb{K}$-analytic at $z$.

AnalyticWithinAt.div theorem

 {f g : E → 𝕝} {s : Set E} {x : E} (fa : AnalyticWithinAt 𝕜 f s x) (ga : AnalyticWithinAt 𝕜 g s x) (g0 : g x ≠ 0) :
  AnalyticWithinAt 𝕜 (fun x ↦ f x / g x) s x

Full source

/-- `f x / g x` is analytic away from `g x = 0` -/
theorem AnalyticWithinAt.div {f g : E → 𝕝} {s : Set E} {x : E}
    (fa : AnalyticWithinAt 𝕜 f s x) (ga : AnalyticWithinAt 𝕜 g s x) (g0 : g x ≠ 0) :
    AnalyticWithinAt 𝕜 (fun x ↦ f x / g x) s x := by
  simp_rw [div_eq_mul_inv]; exact fa.mul (ga.inv g0)

Analyticity of Quotient of Analytic Functions at Nonzero Points

Informal description

Let $E$ be a normed vector space over a complete normed field $\mathbb{K}$, and let $\mathbb{L}$ be a normed field extension of $\mathbb{K}$. For functions $f, g \colon E \to \mathbb{L}$ and a point $x \in E$, if $f$ and $g$ are $\mathbb{K}$-analytic within a set $s \subseteq E$ at $x$, and $g(x) \neq 0$, then the quotient function $x \mapsto f(x)/g(x)$ is also $\mathbb{K}$-analytic within $s$ at $x$.

AnalyticAt.fun_div theorem

 {f g : E → 𝕝} {x : E} (fa : AnalyticAt 𝕜 f x) (ga : AnalyticAt 𝕜 g x) (g0 : g x ≠ 0) :
  AnalyticAt 𝕜 (fun x ↦ f x / g x) x

Full source

/-- `f x / g x` is analytic away from `g x = 0` -/
@[fun_prop]
theorem AnalyticAt.fun_div {f g : E → 𝕝} {x : E}
    (fa : AnalyticAt 𝕜 f x) (ga : AnalyticAt 𝕜 g x) (g0 : g x ≠ 0) :
    AnalyticAt 𝕜 (fun x ↦ f x / g x) x := by
  simp_rw [div_eq_mul_inv]; exact fa.mul (ga.inv g0)

Analyticity of Pointwise Division at Nonzero Points

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ a normed space over $\mathbb{K}$, and $\mathbb{L}$ a normed field extension of $\mathbb{K}$. For functions $f, g \colon E \to \mathbb{L}$ and a point $x \in E$, if $f$ and $g$ are $\mathbb{K}$-analytic at $x$ and $g(x) \neq 0$, then the function $x \mapsto f(x)/g(x)$ is $\mathbb{K}$-analytic at $x$.

AnalyticAt.div theorem

 {f g : E → 𝕝} {x : E} (fa : AnalyticAt 𝕜 f x) (ga : AnalyticAt 𝕜 g x) (g0 : g x ≠ 0) : AnalyticAt 𝕜 (f / g) x

Full source

@[fun_prop]
theorem AnalyticAt.div {f g : E → 𝕝} {x : E}
    (fa : AnalyticAt 𝕜 f x) (ga : AnalyticAt 𝕜 g x) (g0 : g x ≠ 0) :
    AnalyticAt 𝕜 (f / g) x :=
  fa.fun_div ga g0

Analyticity of Quotient of Analytic Functions at Nonzero Points

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ a normed space over $\mathbb{K}$, and $\mathbb{L}$ a normed field extension of $\mathbb{K}$. For functions $f, g \colon E \to \mathbb{L}$ and a point $x \in E$, if $f$ and $g$ are $\mathbb{K}$-analytic at $x$ and $g(x) \neq 0$, then the quotient function $f/g$ is $\mathbb{K}$-analytic at $x$.

AnalyticOn.div theorem

 {f g : E → 𝕝} {s : Set E} (fa : AnalyticOn 𝕜 f s) (ga : AnalyticOn 𝕜 g s) (g0 : ∀ x ∈ s, g x ≠ 0) :
  AnalyticOn 𝕜 (fun x ↦ f x / g x) s

Full source

/-- `f x / g x` is analytic away from `g x = 0` -/
theorem AnalyticOn.div {f g : E → 𝕝} {s : Set E}
    (fa : AnalyticOn 𝕜 f s) (ga : AnalyticOn 𝕜 g s) (g0 : ∀ x ∈ s, g x ≠ 0) :
    AnalyticOn 𝕜 (fun x ↦ f x / g x) s := fun x m ↦
  (fa x m).div (ga x m) (g0 x m)

Analyticity of Quotient of Analytic Functions on a Set

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ a normed space over $\mathbb{K}$, and $\mathbb{L}$ a normed field extension of $\mathbb{K}$. For functions $f, g \colon E \to \mathbb{L}$ and a set $s \subseteq E$, if $f$ and $g$ are $\mathbb{K}$-analytic on $s$ and $g(x) \neq 0$ for all $x \in s$, then the function $x \mapsto f(x)/g(x)$ is $\mathbb{K}$-analytic on $s$.

AnalyticOnNhd.div theorem

 {f g : E → 𝕝} {s : Set E} (fa : AnalyticOnNhd 𝕜 f s) (ga : AnalyticOnNhd 𝕜 g s) (g0 : ∀ x ∈ s, g x ≠ 0) :
  AnalyticOnNhd 𝕜 (fun x ↦ f x / g x) s

Full source

/-- `f x / g x` is analytic away from `g x = 0` -/
theorem AnalyticOnNhd.div {f g : E → 𝕝} {s : Set E}
    (fa : AnalyticOnNhd 𝕜 f s) (ga : AnalyticOnNhd 𝕜 g s) (g0 : ∀ x ∈ s, g x ≠ 0) :
    AnalyticOnNhd 𝕜 (fun x ↦ f x / g x) s := fun x m ↦
  (fa x m).div (ga x m) (g0 x m)

Quotient of Locally Analytic Functions is Locally Analytic on Nonzero Set

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ a normed space over $\mathbb{K}$, and $\mathbb{L}$ a normed field extension of $\mathbb{K}$. For functions $f, g \colon E \to \mathbb{L}$ and a set $s \subseteq E$, if $f$ and $g$ are $\mathbb{K}$-analytic in a neighborhood of each point in $s$ and $g(x) \neq 0$ for all $x \in s$, then the function $x \mapsto f(x)/g(x)$ is $\mathbb{K}$-analytic in a neighborhood of each point in $s$.

Finset.analyticWithinAt_sum theorem

 {f : α → E → F} {c : E} {s : Set E} (N : Finset α) (h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c) :
  AnalyticWithinAt 𝕜 (fun z ↦ ∑ n ∈ N, f n z) s c

Full source

/-- Finite sums of analytic functions are analytic -/
theorem Finset.analyticWithinAt_sum {f : α → E → F} {c : E} {s : Set E}
    (N : Finset α) (h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c) :
    AnalyticWithinAt 𝕜 (fun z ↦ ∑ n ∈ N, f n z) s c := by
  classical
  induction' N using Finset.induction with a B aB hB
  · simp only [Finset.sum_empty]
    exact analyticWithinAt_const
  · simp_rw [Finset.sum_insert aB]
    simp only [Finset.mem_insert] at h
    exact (h a (Or.inl rfl)).add (hB fun b m ↦ h b (Or.inr m))

Finite Sum of Analytic Functions is Analytic Within a Set at a Point

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, $s \subseteq E$, and $c \in E$. Given a finite set $N$ and a family of functions $f_n : E \to F$ for $n \in N$, if each $f_n$ is analytic at $c$ within $s$, then the finite sum $\sum_{n \in N} f_n(z)$ is analytic at $c$ within $s$.

Finset.analyticAt_sum theorem

 {f : α → E → F} {c : E} (N : Finset α) (h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c) : AnalyticAt 𝕜 (fun z ↦ ∑ n ∈ N, f n z) c

Full source

/-- Finite sums of analytic functions are analytic -/
@[fun_prop]
theorem Finset.analyticAt_sum {f : α → E → F} {c : E}
    (N : Finset α) (h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c) :
    AnalyticAt 𝕜 (fun z ↦ ∑ n ∈ N, f n z) c := by
  simp_rw [← analyticWithinAt_univ] at h ⊢
  exact N.analyticWithinAt_sum h

Finite Sum of Analytic Functions is Analytic at a Point

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $c \in E$. Given a finite set $N$ and a family of functions $f_n : E \to F$ for $n \in N$, if each $f_n$ is analytic at $c$, then the finite sum $\sum_{n \in N} f_n(z)$ is analytic at $c$.

Finset.analyticOn_sum theorem

 {f : α → E → F} {s : Set E} (N : Finset α) (h : ∀ n ∈ N, AnalyticOn 𝕜 (f n) s) :
  AnalyticOn 𝕜 (fun z ↦ ∑ n ∈ N, f n z) s

Full source

/-- Finite sums of analytic functions are analytic -/
theorem Finset.analyticOn_sum {f : α → E → F} {s : Set E}
    (N : Finset α) (h : ∀ n ∈ N, AnalyticOn 𝕜 (f n) s) :
    AnalyticOn 𝕜 (fun z ↦ ∑ n ∈ N, f n z) s :=
  fun z zs ↦ N.analyticWithinAt_sum (fun n m ↦ h n m z zs)

Analyticity of Finite Sums on a Set

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $s \subseteq E$. Given a finite set $N$ and a family of functions $f_n : E \to F$ for $n \in N$, if each $f_n$ is analytic on $s$, then the finite sum $\sum_{n \in N} f_n(z)$ is analytic on $s$.

Finset.analyticOnNhd_sum theorem

 {f : α → E → F} {s : Set E} (N : Finset α) (h : ∀ n ∈ N, AnalyticOnNhd 𝕜 (f n) s) :
  AnalyticOnNhd 𝕜 (fun z ↦ ∑ n ∈ N, f n z) s

Full source

/-- Finite sums of analytic functions are analytic -/
theorem Finset.analyticOnNhd_sum {f : α → E → F} {s : Set E}
    (N : Finset α) (h : ∀ n ∈ N, AnalyticOnNhd 𝕜 (f n) s) :
    AnalyticOnNhd 𝕜 (fun z ↦ ∑ n ∈ N, f n z) s :=
  fun z zs ↦ N.analyticAt_sum (fun n m ↦ h n m z zs)

Finite Sum of Locally Analytic Functions is Locally Analytic on a Set

Informal description

Let $\mathbb{K}$ be a complete normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $s \subseteq E$. Given a finite set $N$ and a family of functions $f_n : E \to F$ for $n \in N$, if each $f_n$ is analytic in a neighborhood of every point in $s$, then the finite sum $\sum_{n \in N} f_n(z)$ is analytic in a neighborhood of every point in $s$.

Finset.analyticWithinAt_prod theorem

 {A : Type*} [NormedCommRing A] [NormedAlgebra 𝕜 A] {f : α → E → A} {c : E} {s : Set E} (N : Finset α)
  (h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c) : AnalyticWithinAt 𝕜 (fun z ↦ ∏ n ∈ N, f n z) s c

Full source

/-- Finite products of analytic functions are analytic -/
theorem Finset.analyticWithinAt_prod {A : Type*} [NormedCommRing A] [NormedAlgebra 𝕜 A]
    {f : α → E → A} {c : E} {s : Set E} (N : Finset α) (h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c) :
    AnalyticWithinAt 𝕜 (fun z ↦ ∏ n ∈ N, f n z) s c := by
  classical
  induction' N using Finset.induction with a B aB hB
  · simp only [Finset.prod_empty]
    exact analyticWithinAt_const
  · simp_rw [Finset.prod_insert aB]
    simp only [Finset.mem_insert] at h
    exact (h a (Or.inl rfl)).mul (hB fun b m ↦ h b (Or.inr m))

Analyticity of Finite Products Within a Set at a Point

Informal description

Let $\mathbb{K}$ be a complete normed field, $A$ a normed commutative ring with a normed $\mathbb{K}$-algebra structure, $E$ a normed space over $\mathbb{K}$, and $s \subseteq E$. Given a finite set $N$ and a family of functions $f_n \colon E \to A$ for $n \in N$, if each $f_n$ is analytic at a point $c \in E$ within $s$, then the finite product $\prod_{n \in N} f_n(z)$ is analytic at $c$ within $s$.

Finset.analyticAt_prod theorem

 {A : Type*} [NormedCommRing A] [NormedAlgebra 𝕜 A] {f : α → E → A} {c : E} (N : Finset α)
  (h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c) : AnalyticAt 𝕜 (fun z ↦ ∏ n ∈ N, f n z) c

Full source

/-- Finite products of analytic functions are analytic -/
@[fun_prop]
theorem Finset.analyticAt_prod {A : Type*} [NormedCommRing A] [NormedAlgebra 𝕜 A]
    {f : α → E → A} {c : E} (N : Finset α) (h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c) :
    AnalyticAt 𝕜 (fun z ↦ ∏ n ∈ N, f n z) c := by
  simp_rw [← analyticWithinAt_univ] at h ⊢
  exact N.analyticWithinAt_prod h

Analyticity of Finite Products at a Point

Informal description

Let $\mathbb{K}$ be a complete normed field, $A$ a normed commutative ring with a normed $\mathbb{K}$-algebra structure, and $E$ a normed space over $\mathbb{K}$. Given a finite set $N$ and a family of functions $f_n \colon E \to A$ for $n \in N$, if each $f_n$ is analytic at a point $c \in E$, then the finite product $\prod_{n \in N} f_n(z)$ is analytic at $c$.

Finset.analyticOn_prod theorem

 {A : Type*} [NormedCommRing A] [NormedAlgebra 𝕜 A] {f : α → E → A} {s : Set E} (N : Finset α)
  (h : ∀ n ∈ N, AnalyticOn 𝕜 (f n) s) : AnalyticOn 𝕜 (fun z ↦ ∏ n ∈ N, f n z) s

Full source

/-- Finite products of analytic functions are analytic -/
theorem Finset.analyticOn_prod {A : Type*} [NormedCommRing A] [NormedAlgebra 𝕜 A]
    {f : α → E → A} {s : Set E} (N : Finset α) (h : ∀ n ∈ N, AnalyticOn 𝕜 (f n) s) :
    AnalyticOn 𝕜 (fun z ↦ ∏ n ∈ N, f n z) s :=
  fun z zs ↦ N.analyticWithinAt_prod (fun n m ↦ h n m z zs)

Analyticity of Finite Products on a Set

Informal description

Let $\mathbb{K}$ be a complete normed field, $A$ a normed commutative ring with a normed $\mathbb{K}$-algebra structure, $E$ a normed space over $\mathbb{K}$, and $s \subseteq E$. Given a finite set $N$ and a family of functions $f_n \colon E \to A$ for $n \in N$, if each $f_n$ is analytic on $s$, then the finite product $\prod_{n \in N} f_n(z)$ is analytic on $s$.

Finset.analyticOnNhd_prod theorem

 {A : Type*} [NormedCommRing A] [NormedAlgebra 𝕜 A] {f : α → E → A} {s : Set E} (N : Finset α)
  (h : ∀ n ∈ N, AnalyticOnNhd 𝕜 (f n) s) : AnalyticOnNhd 𝕜 (fun z ↦ ∏ n ∈ N, f n z) s

Full source

/-- Finite products of analytic functions are analytic -/
theorem Finset.analyticOnNhd_prod {A : Type*} [NormedCommRing A] [NormedAlgebra 𝕜 A]
    {f : α → E → A} {s : Set E} (N : Finset α) (h : ∀ n ∈ N, AnalyticOnNhd 𝕜 (f n) s) :
    AnalyticOnNhd 𝕜 (fun z ↦ ∏ n ∈ N, f n z) s :=
  fun z zs ↦ N.analyticAt_prod (fun n m ↦ h n m z zs)

Analyticity of Finite Products on Neighborhoods of a Set

Informal description

Let $\mathbb{K}$ be a complete normed field, $A$ a normed commutative ring with a normed $\mathbb{K}$-algebra structure, $E$ a normed space over $\mathbb{K}$, and $s \subseteq E$. Given a finite set $N$ and a family of functions $f_n \colon E \to A$ for $n \in N$, if each $f_n$ is analytic on a neighborhood of each point in $s$, then the finite product $\prod_{n \in N} f_n(z)$ is analytic on a neighborhood of each point in $s$.

HasFPowerSeriesWithinOnBall.unshift theorem

 (hf : HasFPowerSeriesWithinOnBall f pf s x r) :
  HasFPowerSeriesWithinOnBall (fun y ↦ z + f y (y - x)) (pf.unshift z) s x r

Full source

theorem HasFPowerSeriesWithinOnBall.unshift (hf : HasFPowerSeriesWithinOnBall f pf s x r) :
    HasFPowerSeriesWithinOnBall (fun y ↦ z + f y (y - x)) (pf.unshift z) s x r where
  r_le := by
    rw [FormalMultilinearSeries.radius_unshift]
    exact hf.r_le
  r_pos := hf.r_pos
  hasSum := by
    intro y hy h'y
    apply HasSum.zero_add
    simp only [FormalMultilinearSeries.unshift, Nat.succ_eq_add_one,
      continuousMultilinearCurryRightEquiv_symm_apply', add_sub_cancel_left]
    exact (ContinuousLinearMap.apply 𝕜 F y).hasSum (hf.hasSum hy h'y)

Unshifted power series expansion of $z + f(y)(y - x)$

Informal description

Let $f$ be a function with a formal power series expansion $pf$ within a ball of radius $r$ centered at $x$ on a set $s$. Then for any fixed $z$, the function $y \mapsto z + f(y)(y - x)$ also has a formal power series expansion given by $pf.\text{unshift}(z)$ within the same ball $B(x, r)$ on the set $s$.

HasFPowerSeriesOnBall.unshift theorem

(hf : HasFPowerSeriesOnBall f pf x r) : HasFPowerSeriesOnBall (fun y ↦ z + f y (y - x)) (pf.unshift z) x r

Full source

theorem HasFPowerSeriesOnBall.unshift (hf : HasFPowerSeriesOnBall f pf x r) :
    HasFPowerSeriesOnBall (fun y ↦ z + f y (y - x)) (pf.unshift z) x r where
  r_le := by
    rw [FormalMultilinearSeries.radius_unshift]
    exact hf.r_le
  r_pos := hf.r_pos
  hasSum := by
    intro y hy
    apply HasSum.zero_add
    simp only [FormalMultilinearSeries.unshift, Nat.succ_eq_add_one,
      continuousMultilinearCurryRightEquiv_symm_apply', add_sub_cancel_left]
    exact (ContinuousLinearMap.apply 𝕜 F y).hasSum (hf.hasSum hy)

Power Series Expansion of Shifted Function: $y \mapsto z + f(y)(y - x)$

Informal description

Let $f$ be a function with a formal power series expansion $pf$ centered at $x$ with radius of convergence $r$. Then the function $y \mapsto z + f(y)(y - x)$ has a formal power series expansion given by $pf.\text{unshift}(z)$, centered at $x$ with the same radius of convergence $r$.

HasFPowerSeriesWithinAt.unshift theorem

(hf : HasFPowerSeriesWithinAt f pf s x) : HasFPowerSeriesWithinAt (fun y ↦ z + f y (y - x)) (pf.unshift z) s x

Full source

theorem HasFPowerSeriesWithinAt.unshift (hf : HasFPowerSeriesWithinAt f pf s x) :
    HasFPowerSeriesWithinAt (fun y ↦ z + f y (y - x)) (pf.unshift z) s x :=
  let ⟨_, hrf⟩ := hf
  hrf.unshift.hasFPowerSeriesWithinAt

Power Series Expansion of Shifted Function at a Point: $y \mapsto z + f(y)(y - x)$

Informal description

Let $f$ be a function with a formal power series expansion $pf$ at a point $x$ within a set $s$. Then for any fixed $z$, the function $y \mapsto z + f(y)(y - x)$ also has a formal power series expansion given by $pf.\text{unshift}(z)$ at $x$ within the same set $s$.