Polynomials are analytic #
This file combines the analysis and algebra libraries and shows that evaluation of a polynomial is an analytic function.
theorem
AnalyticAt.aeval_polynomial
{𝕜 : Type u_1}
{E : Type u_2}
{A : Type u_3}
{B : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CommSemiring A]
{z : E}
[NormedRing B]
[NormedAlgebra 𝕜 B]
[Algebra A B]
{f : E → B}
(hf : AnalyticAt 𝕜 f z)
(p : Polynomial A)
:
AnalyticAt 𝕜 (fun (x : E) => (Polynomial.aeval (f x)) p) z
theorem
AnalyticOn.aeval_polynomial
{𝕜 : Type u_1}
{E : Type u_2}
{A : Type u_3}
{B : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CommSemiring A]
{s : Set E}
[NormedRing B]
[NormedAlgebra 𝕜 B]
[Algebra A B]
{f : E → B}
(hf : AnalyticOn 𝕜 f s)
(p : Polynomial A)
:
AnalyticOn 𝕜 (fun (x : E) => (Polynomial.aeval (f x)) p) s
theorem
AnalyticOn.eval_polynomial
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{A : Type u_5}
[NormedCommRing A]
[NormedAlgebra 𝕜 A]
(p : Polynomial A)
:
AnalyticOn 𝕜 (fun (x : A) => Polynomial.eval x p) Set.univ
theorem
AnalyticAt.aeval_mvPolynomial
{𝕜 : Type u_1}
{E : Type u_2}
{A : Type u_3}
{B : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CommSemiring A]
{z : E}
[NormedCommRing B]
[NormedAlgebra 𝕜 B]
[Algebra A B]
{σ : Type u_5}
{f : E → σ → B}
(hf : ∀ (i : σ), AnalyticAt 𝕜 (fun (x : E) => f x i) z)
(p : MvPolynomial σ A)
:
AnalyticAt 𝕜 (fun (x : E) => (MvPolynomial.aeval (f x)) p) z
theorem
AnalyticOn.aeval_mvPolynomial
{𝕜 : Type u_1}
{E : Type u_2}
{A : Type u_3}
{B : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CommSemiring A]
{s : Set E}
[NormedCommRing B]
[NormedAlgebra 𝕜 B]
[Algebra A B]
{σ : Type u_5}
{f : E → σ → B}
(hf : ∀ (i : σ), AnalyticOn 𝕜 (fun (x : E) => f x i) s)
(p : MvPolynomial σ A)
:
AnalyticOn 𝕜 (fun (x : E) => (MvPolynomial.aeval (f x)) p) s
theorem
AnalyticOn.eval_continuousLinearMap
{𝕜 : Type u_1}
{E : Type u_2}
{B : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedCommRing B]
[NormedAlgebra 𝕜 B]
{σ : Type u_5}
(f : E →L[𝕜] σ → B)
(p : MvPolynomial σ B)
:
AnalyticOn 𝕜 (fun (x : E) => (MvPolynomial.eval (f x)) p) Set.univ
theorem
AnalyticOn.eval_continuousLinearMap'
{𝕜 : Type u_1}
{E : Type u_2}
{B : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedCommRing B]
[NormedAlgebra 𝕜 B]
{σ : Type u_5}
(f : σ → E →L[𝕜] B)
(p : MvPolynomial σ B)
:
AnalyticOn 𝕜 (fun (x : E) => (MvPolynomial.eval fun (x_1 : σ) => (f x_1) x) p) Set.univ
theorem
AnalyticOn.eval_linearMap
{𝕜 : Type u_1}
{E : Type u_2}
{B : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedCommRing B]
[NormedAlgebra 𝕜 B]
{σ : Type u_5}
[CompleteSpace 𝕜]
[T2Space E]
[FiniteDimensional 𝕜 E]
(f : E →ₗ[𝕜] σ → B)
(p : MvPolynomial σ B)
:
AnalyticOn 𝕜 (fun (x : E) => (MvPolynomial.eval (f x)) p) Set.univ
theorem
AnalyticOn.eval_linearMap'
{𝕜 : Type u_1}
{E : Type u_2}
{B : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedCommRing B]
[NormedAlgebra 𝕜 B]
{σ : Type u_5}
[CompleteSpace 𝕜]
[T2Space E]
[FiniteDimensional 𝕜 E]
(f : σ → E →ₗ[𝕜] B)
(p : MvPolynomial σ B)
:
AnalyticOn 𝕜 (fun (x : E) => (MvPolynomial.eval fun (x_1 : σ) => (f x_1) x) p) Set.univ
theorem
AnalyticOn.eval_mvPolynomial
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{σ : Type u_5}
[CompleteSpace 𝕜]
[Fintype σ]
(p : MvPolynomial σ 𝕜)
:
AnalyticOn 𝕜 (fun (x : σ → 𝕜) => (MvPolynomial.eval x) p) Set.univ