Documentation

Mathlib.Analysis.Analytic.CPolynomial

We specialize the theory fo analytic functions to the case of functions that admit a development given by a finite formal multilinear series. We call them "continuously polynomial", which is abbreviated to CPolynomial. One reason to do that is that we no longer need a completeness assumption on the target space F to make the series converge, so some of the results are more general. The class of continuously polynomial functions includes functions defined by polynomials on a normed ๐•œ-algebra and continuous multilinear maps.

Main definitions #

Let p be a formal multilinear series from E to F, i.e., p n is a multilinear map on E^n for n : โ„•, and let f be a function from E to F.

We develop the basic properties of these notions, notably:

We prove in particular that continuous multilinear maps are continuously polynomial, and so are continuous linear maps into continuous multilinear maps. In particular, such maps are analytic.

structure HasFiniteFPowerSeriesOnBall {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] (f : E โ†’ F) (p : FormalMultilinearSeries ๐•œ E F) (x : E) (n : โ„•) (r : ENNReal) extends HasFPowerSeriesOnBall :

Given a function f : E โ†’ F, a formal multilinear series p and n : โ„•, we say that f has p as a finite power series on the ball of radius r > 0 around x if f (x + y) = โˆ‘' pโ‚˜ yแต for all โ€–yโ€– < r and pโ‚™ = 0 for n โ‰ค m.

Instances For
    theorem HasFiniteFPowerSeriesOnBall.finite {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {p : FormalMultilinearSeries ๐•œ E F} {x : E} {n : โ„•} {r : ENNReal} (self : HasFiniteFPowerSeriesOnBall f p x n r) (m : โ„•) :
    n โ‰ค m โ†’ p m = 0
    theorem HasFiniteFPowerSeriesOnBall.mk' {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {p : FormalMultilinearSeries ๐•œ E F} {x : E} {n : โ„•} {r : ENNReal} (finite : โˆ€ (m : โ„•), n โ‰ค m โ†’ p m = 0) (pos : 0 < r) (sum_eq : โˆ€ y โˆˆ EMetric.ball 0 r, (โˆ‘ i โˆˆ Finset.range n, (p i) fun (x : Fin i) => y) = f (x + y)) :
    def HasFiniteFPowerSeriesAt {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] (f : E โ†’ F) (p : FormalMultilinearSeries ๐•œ E F) (x : E) (n : โ„•) :

    Given a function f : E โ†’ F, a formal multilinear series p and n : โ„•, we say that f has p as a finite power series around x if f (x + y) = โˆ‘' pโ‚™ yโฟ for all y in a neighborhood of 0and pโ‚™ = 0 for n โ‰ค m.

    Equations
    Instances For
      theorem HasFiniteFPowerSeriesAt.toHasFPowerSeriesAt {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {p : FormalMultilinearSeries ๐•œ E F} {x : E} {n : โ„•} (hf : HasFiniteFPowerSeriesAt f p x n) :
      theorem HasFiniteFPowerSeriesAt.finite {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {p : FormalMultilinearSeries ๐•œ E F} {x : E} {n : โ„•} (hf : HasFiniteFPowerSeriesAt f p x n) (m : โ„•) :
      n โ‰ค m โ†’ p m = 0
      def CPolynomialAt (๐•œ : Type u_1) {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] (f : E โ†’ F) (x : E) :

      Given a function f : E โ†’ F, we say that f is continuously polynomial (cpolynomial) at x if it admits a finite power series expansion around x.

      Equations
      Instances For
        def CPolynomialOn (๐•œ : Type u_1) {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] (f : E โ†’ F) (s : Set E) :

        Given a function f : E โ†’ F, we say that f is continuously polynomial on a set s if it is continuously polynomial around every point of s.

        Equations
        Instances For
          theorem HasFiniteFPowerSeriesOnBall.hasFiniteFPowerSeriesAt {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {p : FormalMultilinearSeries ๐•œ E F} {x : E} {r : ENNReal} {n : โ„•} (hf : HasFiniteFPowerSeriesOnBall f p x n r) :
          theorem HasFiniteFPowerSeriesAt.cPolynomialAt {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {p : FormalMultilinearSeries ๐•œ E F} {x : E} {n : โ„•} (hf : HasFiniteFPowerSeriesAt f p x n) :
          CPolynomialAt ๐•œ f x
          theorem HasFiniteFPowerSeriesOnBall.cPolynomialAt {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {p : FormalMultilinearSeries ๐•œ E F} {x : E} {r : ENNReal} {n : โ„•} (hf : HasFiniteFPowerSeriesOnBall f p x n r) :
          CPolynomialAt ๐•œ f x
          theorem CPolynomialAt.analyticAt {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {x : E} (hf : CPolynomialAt ๐•œ f x) :
          AnalyticAt ๐•œ f x
          theorem CPolynomialAt.analyticWithinAt {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {x : E} {s : Set E} (hf : CPolynomialAt ๐•œ f x) :
          AnalyticWithinAt ๐•œ f s x
          theorem CPolynomialOn.analyticOnNhd {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {s : Set E} (hf : CPolynomialOn ๐•œ f s) :
          AnalyticOnNhd ๐•œ f s
          theorem CPolynomialOn.analyticOn {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {s : Set E} (hf : CPolynomialOn ๐•œ f s) :
          AnalyticOn ๐•œ f s
          theorem HasFiniteFPowerSeriesOnBall.congr {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {g : E โ†’ F} {p : FormalMultilinearSeries ๐•œ E F} {x : E} {r : ENNReal} {n : โ„•} (hf : HasFiniteFPowerSeriesOnBall f p x n r) (hg : Set.EqOn f g (EMetric.ball x r)) :
          theorem HasFiniteFPowerSeriesOnBall.comp_sub {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {p : FormalMultilinearSeries ๐•œ E F} {x : E} {r : ENNReal} {n : โ„•} (hf : HasFiniteFPowerSeriesOnBall f p x n r) (y : E) :
          HasFiniteFPowerSeriesOnBall (fun (z : E) => f (z - y)) p (x + y) n r

          If a function f has a finite power series p around x, then the function z โ†ฆ f (z - y) has the same finite power series around x + y.

          theorem HasFiniteFPowerSeriesOnBall.mono {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {p : FormalMultilinearSeries ๐•œ E F} {x : E} {r : ENNReal} {r' : ENNReal} {n : โ„•} (hf : HasFiniteFPowerSeriesOnBall f p x n r) (r'_pos : 0 < r') (hr : r' โ‰ค r) :
          theorem HasFiniteFPowerSeriesAt.congr {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {g : E โ†’ F} {p : FormalMultilinearSeries ๐•œ E F} {x : E} {n : โ„•} (hf : HasFiniteFPowerSeriesAt f p x n) (hg : f =แถ [nhds x] g) :
          theorem HasFiniteFPowerSeriesAt.eventually {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {p : FormalMultilinearSeries ๐•œ E F} {x : E} {n : โ„•} (hf : HasFiniteFPowerSeriesAt f p x n) :
          โˆ€แถ  (r : ENNReal) in nhdsWithin 0 (Set.Ioi 0), HasFiniteFPowerSeriesOnBall f p x n r
          theorem hasFiniteFPowerSeriesOnBall_const {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {c : F} {e : E} :
          theorem hasFiniteFPowerSeriesAt_const {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {c : F} {e : E} :
          HasFiniteFPowerSeriesAt (fun (x : E) => c) (constFormalMultilinearSeries ๐•œ E c) e 1
          theorem CPolynomialAt_const {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {x : E} {v : F} :
          CPolynomialAt ๐•œ (fun (x : E) => v) x
          theorem CPolynomialOn_const {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {v : F} {s : Set E} :
          CPolynomialOn ๐•œ (fun (x : E) => v) s
          theorem HasFiniteFPowerSeriesOnBall.add {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {g : E โ†’ F} {pf : FormalMultilinearSeries ๐•œ E F} {pg : FormalMultilinearSeries ๐•œ E F} {x : E} {r : ENNReal} {n : โ„•} {m : โ„•} (hf : HasFiniteFPowerSeriesOnBall f pf x n r) (hg : HasFiniteFPowerSeriesOnBall g pg x m r) :
          HasFiniteFPowerSeriesOnBall (f + g) (pf + pg) x (max n m) r
          theorem HasFiniteFPowerSeriesAt.add {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {g : E โ†’ F} {pf : FormalMultilinearSeries ๐•œ E F} {pg : FormalMultilinearSeries ๐•œ E F} {x : E} {n : โ„•} {m : โ„•} (hf : HasFiniteFPowerSeriesAt f pf x n) (hg : HasFiniteFPowerSeriesAt g pg x m) :
          HasFiniteFPowerSeriesAt (f + g) (pf + pg) x (max n m)
          theorem CPolynomialAt.congr {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {g : E โ†’ F} {x : E} (hf : CPolynomialAt ๐•œ f x) (hg : f =แถ [nhds x] g) :
          CPolynomialAt ๐•œ g x
          theorem CPolynomialAt_congr {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {g : E โ†’ F} {x : E} (h : f =แถ [nhds x] g) :
          CPolynomialAt ๐•œ f x โ†” CPolynomialAt ๐•œ g x
          theorem CPolynomialAt.add {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {g : E โ†’ F} {x : E} (hf : CPolynomialAt ๐•œ f x) (hg : CPolynomialAt ๐•œ g x) :
          CPolynomialAt ๐•œ (f + g) x
          theorem HasFiniteFPowerSeriesOnBall.neg {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {pf : FormalMultilinearSeries ๐•œ E F} {x : E} {r : ENNReal} {n : โ„•} (hf : HasFiniteFPowerSeriesOnBall f pf x n r) :
          theorem HasFiniteFPowerSeriesAt.neg {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {pf : FormalMultilinearSeries ๐•œ E F} {x : E} {n : โ„•} (hf : HasFiniteFPowerSeriesAt f pf x n) :
          theorem CPolynomialAt.neg {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {x : E} (hf : CPolynomialAt ๐•œ f x) :
          CPolynomialAt ๐•œ (-f) x
          theorem HasFiniteFPowerSeriesOnBall.sub {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {g : E โ†’ F} {pf : FormalMultilinearSeries ๐•œ E F} {pg : FormalMultilinearSeries ๐•œ E F} {x : E} {r : ENNReal} {n : โ„•} {m : โ„•} (hf : HasFiniteFPowerSeriesOnBall f pf x n r) (hg : HasFiniteFPowerSeriesOnBall g pg x m r) :
          HasFiniteFPowerSeriesOnBall (f - g) (pf - pg) x (max n m) r
          theorem HasFiniteFPowerSeriesAt.sub {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {g : E โ†’ F} {pf : FormalMultilinearSeries ๐•œ E F} {pg : FormalMultilinearSeries ๐•œ E F} {x : E} {n : โ„•} {m : โ„•} (hf : HasFiniteFPowerSeriesAt f pf x n) (hg : HasFiniteFPowerSeriesAt g pg x m) :
          HasFiniteFPowerSeriesAt (f - g) (pf - pg) x (max n m)
          theorem CPolynomialAt.sub {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {g : E โ†’ F} {x : E} (hf : CPolynomialAt ๐•œ f x) (hg : CPolynomialAt ๐•œ g x) :
          CPolynomialAt ๐•œ (f - g) x
          theorem CPolynomialOn.mono {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {s : Set E} {t : Set E} (hf : CPolynomialOn ๐•œ f t) (hst : s โŠ† t) :
          CPolynomialOn ๐•œ f s
          theorem CPolynomialOn.congr' {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {g : E โ†’ F} {s : Set E} (hf : CPolynomialOn ๐•œ f s) (hg : f =แถ [nhdsSet s] g) :
          CPolynomialOn ๐•œ g s
          theorem CPolynomialOn_congr' {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {g : E โ†’ F} {s : Set E} (h : f =แถ [nhdsSet s] g) :
          CPolynomialOn ๐•œ f s โ†” CPolynomialOn ๐•œ g s
          theorem CPolynomialOn.congr {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {g : E โ†’ F} {s : Set E} (hs : IsOpen s) (hf : CPolynomialOn ๐•œ f s) (hg : Set.EqOn f g s) :
          CPolynomialOn ๐•œ g s
          theorem CPolynomialOn_congr {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {g : E โ†’ F} {s : Set E} (hs : IsOpen s) (h : Set.EqOn f g s) :
          CPolynomialOn ๐•œ f s โ†” CPolynomialOn ๐•œ g s
          theorem CPolynomialOn.add {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {g : E โ†’ F} {s : Set E} (hf : CPolynomialOn ๐•œ f s) (hg : CPolynomialOn ๐•œ g s) :
          CPolynomialOn ๐•œ (f + g) s
          theorem CPolynomialOn.sub {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {g : E โ†’ F} {s : Set E} (hf : CPolynomialOn ๐•œ f s) (hg : CPolynomialOn ๐•œ g s) :
          CPolynomialOn ๐•œ (f - g) s
          theorem ContinuousLinearMap.comp_hasFiniteFPowerSeriesOnBall {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [NormedAddCommGroup G] [NormedSpace ๐•œ G] {f : E โ†’ F} {p : FormalMultilinearSeries ๐•œ E F} {x : E} {r : ENNReal} {n : โ„•} (g : F โ†’L[๐•œ] G) (h : HasFiniteFPowerSeriesOnBall f p x n r) :
          HasFiniteFPowerSeriesOnBall (โ‡‘g โˆ˜ f) (g.compFormalMultilinearSeries p) x n r

          If a function f has a finite power series p on a ball and g is a continuous linear map, then g โˆ˜ f has the finite power series g โˆ˜ p on the same ball.

          theorem ContinuousLinearMap.comp_cPolynomialOn {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [NormedAddCommGroup G] [NormedSpace ๐•œ G] {f : E โ†’ F} {s : Set E} (g : F โ†’L[๐•œ] G) (h : CPolynomialOn ๐•œ f s) :
          CPolynomialOn ๐•œ (โ‡‘g โˆ˜ f) s

          If a function f is continuously polynomial on a set s and g is a continuous linear map, then g โˆ˜ f is continuously polynomial on s.

          theorem HasFiniteFPowerSeriesOnBall.eq_partialSum {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {p : FormalMultilinearSeries ๐•œ E F} {x : E} {r : ENNReal} {n : โ„•} (hf : HasFiniteFPowerSeriesOnBall f p x n r) (y : E) :
          y โˆˆ EMetric.ball 0 r โ†’ โˆ€ (m : โ„•), n โ‰ค m โ†’ f (x + y) = p.partialSum m y

          If a function admits a finite power series expansion bounded by n, then it is equal to the mth partial sums of this power series at every point of the disk for n โ‰ค m.

          theorem HasFiniteFPowerSeriesOnBall.eq_partialSum' {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {p : FormalMultilinearSeries ๐•œ E F} {x : E} {r : ENNReal} {n : โ„•} (hf : HasFiniteFPowerSeriesOnBall f p x n r) (y : E) :
          y โˆˆ EMetric.ball x r โ†’ โˆ€ (m : โ„•), n โ‰ค m โ†’ f y = p.partialSum m (y - x)

          Variant of the previous result with the variable expressed as y instead of x + y.

          The particular cases where f has a finite power series bounded by 0 or 1.

          theorem HasFiniteFPowerSeriesOnBall.eq_zero_of_bound_zero {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {pf : FormalMultilinearSeries ๐•œ E F} {x : E} {r : ENNReal} (hf : HasFiniteFPowerSeriesOnBall f pf x 0 r) (y : E) :
          y โˆˆ EMetric.ball x r โ†’ f y = 0

          If f has a formal power series on a ball bounded by 0, then f is equal to 0 on the ball.

          theorem HasFiniteFPowerSeriesOnBall.bound_zero_of_eq_zero {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {p : FormalMultilinearSeries ๐•œ E F} {x : E} {r : ENNReal} (hf : โˆ€ y โˆˆ EMetric.ball x r, f y = 0) (r_pos : 0 < r) (hp : โˆ€ (n : โ„•), p n = 0) :
          theorem HasFiniteFPowerSeriesAt.eventually_zero_of_bound_zero {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {pf : FormalMultilinearSeries ๐•œ E F} {x : E} (hf : HasFiniteFPowerSeriesAt f pf x 0) :

          If f has a formal power series at x bounded by 0, then f is equal to 0 in a neighborhood of x.

          theorem HasFiniteFPowerSeriesOnBall.eq_const_of_bound_one {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {pf : FormalMultilinearSeries ๐•œ E F} {x : E} {r : ENNReal} (hf : HasFiniteFPowerSeriesOnBall f pf x 1 r) (y : E) :
          y โˆˆ EMetric.ball x r โ†’ f y = f x

          If f has a formal power series on a ball bounded by 1, then f is constant equal to f x on the ball.

          theorem HasFiniteFPowerSeriesAt.eventually_const_of_bound_one {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {pf : FormalMultilinearSeries ๐•œ E F} {x : E} (hf : HasFiniteFPowerSeriesAt f pf x 1) :
          f =แถ [nhds x] fun (x_1 : E) => f x

          If f has a formal power series at x bounded by 1, then f is constant equal to f x in a neighborhood of x.

          theorem HasFiniteFPowerSeriesOnBall.continuousOn {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {p : FormalMultilinearSeries ๐•œ E F} {x : E} {r : ENNReal} {n : โ„•} (hf : HasFiniteFPowerSeriesOnBall f p x n r) :

          If a function admits a finite power series expansion on a disk, then it is continuous there.

          theorem HasFiniteFPowerSeriesAt.continuousAt {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {p : FormalMultilinearSeries ๐•œ E F} {x : E} {n : โ„•} (hf : HasFiniteFPowerSeriesAt f p x n) :
          theorem CPolynomialAt.continuousAt {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {x : E} (hf : CPolynomialAt ๐•œ f x) :
          theorem CPolynomialOn.continuousOn {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {s : Set E} (hf : CPolynomialOn ๐•œ f s) :
          theorem CPolynomialOn.continuous {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} (fa : CPolynomialOn ๐•œ f Set.univ) :

          Continuously polynomial everywhere implies continuous

          theorem FormalMultilinearSeries.sum_of_finite {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] (p : FormalMultilinearSeries ๐•œ E F) {n : โ„•} (hn : โˆ€ (m : โ„•), n โ‰ค m โ†’ p m = 0) (x : E) :
          p.sum x = p.partialSum n x
          theorem FormalMultilinearSeries.hasSum_of_finite {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] (p : FormalMultilinearSeries ๐•œ E F) {n : โ„•} (hn : โˆ€ (m : โ„•), n โ‰ค m โ†’ p m = 0) (x : E) :
          HasSum (fun (n : โ„•) => (p n) fun (x_1 : Fin n) => x) (p.sum x)

          A finite formal multilinear series sums to its sum at every point.

          theorem FormalMultilinearSeries.hasFiniteFPowerSeriesOnBall_of_finite {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] (p : FormalMultilinearSeries ๐•œ E F) {n : โ„•} (hn : โˆ€ (m : โ„•), n โ‰ค m โ†’ p m = 0) :

          The sum of a finite power series p admits p as a power series.

          theorem HasFiniteFPowerSeriesOnBall.sum {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {p : FormalMultilinearSeries ๐•œ E F} {x : E} {r : ENNReal} {n : โ„•} (h : HasFiniteFPowerSeriesOnBall f p x n r) {y : E} (hy : y โˆˆ EMetric.ball 0 r) :
          f (x + y) = p.sum y
          theorem FormalMultilinearSeries.continuousOn_of_finite {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] (p : FormalMultilinearSeries ๐•œ E F) {n : โ„•} (hn : โˆ€ (m : โ„•), n โ‰ค m โ†’ p m = 0) :

          The sum of a finite power series is continuous.

          We study what happens when we change the origin of a finite formal multilinear series p. The main point is that the new series p.changeOrigin x is still finite, with the same bound.

          theorem FormalMultilinearSeries.changeOriginSeriesTerm_bound {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] (p : FormalMultilinearSeries ๐•œ E F) {n : โ„•} (hn : โˆ€ (m : โ„•), n โ‰ค m โ†’ p m = 0) (k : โ„•) (l : โ„•) {s : Finset (Fin (k + l))} (hs : s.card = l) (hkl : n โ‰ค k + l) :
          p.changeOriginSeriesTerm k l s hs = 0

          If p is a formal multilinear series such that p m = 0 for n โ‰ค m, then p.changeOriginSeriesTerm k l = 0 for n โ‰ค k + l.

          theorem FormalMultilinearSeries.changeOriginSeries_finite_of_finite {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] (p : FormalMultilinearSeries ๐•œ E F) {n : โ„•} (hn : โˆ€ (m : โ„•), n โ‰ค m โ†’ p m = 0) (k : โ„•) {m : โ„•} :
          n โ‰ค k + m โ†’ p.changeOriginSeries k m = 0

          If p is a finite formal multilinear series, then so is p.changeOriginSeries k for every k in โ„•. More precisely, if p m = 0 for n โ‰ค m, then p.changeOriginSeries k m = 0 for n โ‰ค k + m.

          theorem FormalMultilinearSeries.changeOriginSeries_sum_eq_partialSum_of_finite {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] (p : FormalMultilinearSeries ๐•œ E F) {n : โ„•} (hn : โˆ€ (m : โ„•), n โ‰ค m โ†’ p m = 0) (k : โ„•) :
          (p.changeOriginSeries k).sum = (p.changeOriginSeries k).partialSum (n - k)
          theorem FormalMultilinearSeries.changeOrigin_finite_of_finite {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {x : E} (p : FormalMultilinearSeries ๐•œ E F) {n : โ„•} (hn : โˆ€ (m : โ„•), n โ‰ค m โ†’ p m = 0) {k : โ„•} (hk : n โ‰ค k) :
          p.changeOrigin x k = 0

          If p is a formal multilinear series such that p m = 0 for n โ‰ค m, then p.changeOrigin x k = 0 for n โ‰ค k.

          theorem FormalMultilinearSeries.hasFiniteFPowerSeriesOnBall_changeOrigin {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] (p : FormalMultilinearSeries ๐•œ E F) {n : โ„•} (k : โ„•) (hn : โˆ€ (m : โ„•), n + k โ‰ค m โ†’ p m = 0) :
          HasFiniteFPowerSeriesOnBall (fun (x : E) => p.changeOrigin x k) (p.changeOriginSeries k) 0 n โŠค
          theorem FormalMultilinearSeries.changeOrigin_eval_of_finite {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] (p : FormalMultilinearSeries ๐•œ E F) {n : โ„•} (hn : โˆ€ (m : โ„•), n โ‰ค m โ†’ p m = 0) (x : E) (y : E) :
          (p.changeOrigin x).sum y = p.sum (x + y)
          theorem FormalMultilinearSeries.cPolynomialAt_changeOrigin_of_finite {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] (p : FormalMultilinearSeries ๐•œ E F) {n : โ„•} (hn : โˆ€ (m : โ„•), n โ‰ค m โ†’ p m = 0) (k : โ„•) :
          CPolynomialAt ๐•œ (fun (x : E) => p.changeOrigin x k) 0

          The terms of the formal multilinear series p.changeOrigin are continuously polynomial as we vary the origin

          theorem HasFiniteFPowerSeriesOnBall.changeOrigin {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {p : FormalMultilinearSeries ๐•œ E F} {r : ENNReal} {n : โ„•} {x : E} {y : E} (hf : HasFiniteFPowerSeriesOnBall f p x n r) (h : โ†‘โ€–yโ€–โ‚Š < r) :
          HasFiniteFPowerSeriesOnBall f (p.changeOrigin y) (x + y) n (r - โ†‘โ€–yโ€–โ‚Š)
          theorem HasFiniteFPowerSeriesOnBall.cPolynomialAt_of_mem {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {p : FormalMultilinearSeries ๐•œ E F} {r : ENNReal} {n : โ„•} {x : E} {y : E} (hf : HasFiniteFPowerSeriesOnBall f p x n r) (h : y โˆˆ EMetric.ball x r) :
          CPolynomialAt ๐•œ f y

          If a function admits a finite power series expansion p on an open ball B (x, r), then it is continuously polynomial at every point of this ball.

          theorem HasFiniteFPowerSeriesOnBall.cPolynomialOn {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {p : FormalMultilinearSeries ๐•œ E F} {r : ENNReal} {n : โ„•} {x : E} (hf : HasFiniteFPowerSeriesOnBall f p x n r) :
          CPolynomialOn ๐•œ f (EMetric.ball x r)
          theorem isOpen_cPolynomialAt (๐•œ : Type u_1) {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] (f : E โ†’ F) :
          IsOpen {x : E | CPolynomialAt ๐•œ f x}

          For any function f from a normed vector space to a normed vector space, the set of points x such that f is continuously polynomial at x is open.

          theorem CPolynomialAt.eventually_cPolynomialAt {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {x : E} (h : CPolynomialAt ๐•œ f x) :
          โˆ€แถ  (y : E) in nhds x, CPolynomialAt ๐•œ f y
          theorem CPolynomialAt.exists_mem_nhds_cPolynomialOn {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {x : E} (h : CPolynomialAt ๐•œ f x) :
          โˆƒ s โˆˆ nhds x, CPolynomialOn ๐•œ f s
          theorem CPolynomialAt.exists_ball_cPolynomialOn {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {x : E} (h : CPolynomialAt ๐•œ f x) :
          โˆƒ (r : โ„), 0 < r โˆง CPolynomialOn ๐•œ f (Metric.ball x r)

          If f is continuously polynomial at a point, then it is continuously polynomial in a nonempty ball around that point.

          Continuous multilinear maps #

          We show that continuous multilinear maps are continuously polynomial, and therefore analytic.

          theorem ContinuousMultilinearMap.hasFiniteFPowerSeriesOnBall {๐•œ : Type u_1} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {ฮน : Type u_5} {Em : ฮน โ†’ Type u_6} [(i : ฮน) โ†’ NormedAddCommGroup (Em i)] [(i : ฮน) โ†’ NormedSpace ๐•œ (Em i)] [Fintype ฮน] (f : ContinuousMultilinearMap ๐•œ Em F) :
          HasFiniteFPowerSeriesOnBall (โ‡‘f) f.toFormalMultilinearSeries 0 (Fintype.card ฮน + 1) โŠค
          theorem ContinuousMultilinearMap.cpolynomialAt {๐•œ : Type u_1} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {ฮน : Type u_5} {Em : ฮน โ†’ Type u_6} [(i : ฮน) โ†’ NormedAddCommGroup (Em i)] [(i : ฮน) โ†’ NormedSpace ๐•œ (Em i)] [Fintype ฮน] (f : ContinuousMultilinearMap ๐•œ Em F) {x : (i : ฮน) โ†’ Em i} :
          CPolynomialAt ๐•œ (โ‡‘f) x
          theorem ContinuousMultilinearMap.cpolyomialOn {๐•œ : Type u_1} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {ฮน : Type u_5} {Em : ฮน โ†’ Type u_6} [(i : ฮน) โ†’ NormedAddCommGroup (Em i)] [(i : ฮน) โ†’ NormedSpace ๐•œ (Em i)] [Fintype ฮน] (f : ContinuousMultilinearMap ๐•œ Em F) {s : Set ((i : ฮน) โ†’ Em i)} :
          CPolynomialOn ๐•œ (โ‡‘f) s
          theorem ContinuousMultilinearMap.analyticOnNhd {๐•œ : Type u_1} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {ฮน : Type u_5} {Em : ฮน โ†’ Type u_6} [(i : ฮน) โ†’ NormedAddCommGroup (Em i)] [(i : ฮน) โ†’ NormedSpace ๐•œ (Em i)] [Fintype ฮน] (f : ContinuousMultilinearMap ๐•œ Em F) {s : Set ((i : ฮน) โ†’ Em i)} :
          AnalyticOnNhd ๐•œ (โ‡‘f) s
          theorem ContinuousMultilinearMap.analyticOn {๐•œ : Type u_1} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {ฮน : Type u_5} {Em : ฮน โ†’ Type u_6} [(i : ฮน) โ†’ NormedAddCommGroup (Em i)] [(i : ฮน) โ†’ NormedSpace ๐•œ (Em i)] [Fintype ฮน] (f : ContinuousMultilinearMap ๐•œ Em F) {s : Set ((i : ฮน) โ†’ Em i)} :
          AnalyticOn ๐•œ (โ‡‘f) s
          @[deprecated ContinuousMultilinearMap.analyticOn]
          theorem ContinuousMultilinearMap.analyticWithinOn {๐•œ : Type u_1} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {ฮน : Type u_5} {Em : ฮน โ†’ Type u_6} [(i : ฮน) โ†’ NormedAddCommGroup (Em i)] [(i : ฮน) โ†’ NormedSpace ๐•œ (Em i)] [Fintype ฮน] (f : ContinuousMultilinearMap ๐•œ Em F) {s : Set ((i : ฮน) โ†’ Em i)} :
          AnalyticOn ๐•œ (โ‡‘f) s

          Alias of ContinuousMultilinearMap.analyticOn.

          theorem ContinuousMultilinearMap.analyticAt {๐•œ : Type u_1} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {ฮน : Type u_5} {Em : ฮน โ†’ Type u_6} [(i : ฮน) โ†’ NormedAddCommGroup (Em i)] [(i : ฮน) โ†’ NormedSpace ๐•œ (Em i)] [Fintype ฮน] (f : ContinuousMultilinearMap ๐•œ Em F) {x : (i : ฮน) โ†’ Em i} :
          AnalyticAt ๐•œ (โ‡‘f) x
          theorem ContinuousMultilinearMap.analyticWithinAt {๐•œ : Type u_1} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {ฮน : Type u_5} {Em : ฮน โ†’ Type u_6} [(i : ฮน) โ†’ NormedAddCommGroup (Em i)] [(i : ฮน) โ†’ NormedSpace ๐•œ (Em i)] [Fintype ฮน] (f : ContinuousMultilinearMap ๐•œ Em F) {x : (i : ฮน) โ†’ Em i} {s : Set ((i : ฮน) โ†’ Em i)} :
          AnalyticWithinAt ๐•œ (โ‡‘f) s x

          Continuous linear maps into continuous multilinear maps #

          We show that a continuous linear map into continuous multilinear maps is continuously polynomial (as a function of two variables, i.e., uncurried). Therefore, it is also analytic.

          noncomputable def ContinuousLinearMap.toFormalMultilinearSeriesOfMultilinear {๐•œ : Type u_1} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [NormedAddCommGroup G] [NormedSpace ๐•œ G] {ฮน : Type u_5} {Em : ฮน โ†’ Type u_6} [(i : ฮน) โ†’ NormedAddCommGroup (Em i)] [(i : ฮน) โ†’ NormedSpace ๐•œ (Em i)] [Fintype ฮน] (f : G โ†’L[๐•œ] ContinuousMultilinearMap ๐•œ Em F) :
          FormalMultilinearSeries ๐•œ (G ร— ((i : ฮน) โ†’ Em i)) F

          Formal multilinear series associated to a linear map into multilinear maps.

          Equations
          Instances For
            theorem ContinuousLinearMap.hasFiniteFPowerSeriesOnBall_uncurry_of_multilinear {๐•œ : Type u_1} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [NormedAddCommGroup G] [NormedSpace ๐•œ G] {ฮน : Type u_5} {Em : ฮน โ†’ Type u_6} [(i : ฮน) โ†’ NormedAddCommGroup (Em i)] [(i : ฮน) โ†’ NormedSpace ๐•œ (Em i)] [Fintype ฮน] (f : G โ†’L[๐•œ] ContinuousMultilinearMap ๐•œ Em F) :
            HasFiniteFPowerSeriesOnBall (fun (p : G ร— ((i : ฮน) โ†’ Em i)) => (f p.1) p.2) f.toFormalMultilinearSeriesOfMultilinear 0 (Fintype.card (Option ฮน) + 1) โŠค
            theorem ContinuousLinearMap.cpolynomialAt_uncurry_of_multilinear {๐•œ : Type u_1} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [NormedAddCommGroup G] [NormedSpace ๐•œ G] {ฮน : Type u_5} {Em : ฮน โ†’ Type u_6} [(i : ฮน) โ†’ NormedAddCommGroup (Em i)] [(i : ฮน) โ†’ NormedSpace ๐•œ (Em i)] [Fintype ฮน] (f : G โ†’L[๐•œ] ContinuousMultilinearMap ๐•œ Em F) {x : G ร— ((i : ฮน) โ†’ Em i)} :
            CPolynomialAt ๐•œ (fun (p : G ร— ((i : ฮน) โ†’ Em i)) => (f p.1) p.2) x
            theorem ContinuousLinearMap.cpolyomialOn_uncurry_of_multilinear {๐•œ : Type u_1} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [NormedAddCommGroup G] [NormedSpace ๐•œ G] {ฮน : Type u_5} {Em : ฮน โ†’ Type u_6} [(i : ฮน) โ†’ NormedAddCommGroup (Em i)] [(i : ฮน) โ†’ NormedSpace ๐•œ (Em i)] [Fintype ฮน] (f : G โ†’L[๐•œ] ContinuousMultilinearMap ๐•œ Em F) {s : Set (G ร— ((i : ฮน) โ†’ Em i))} :
            CPolynomialOn ๐•œ (fun (p : G ร— ((i : ฮน) โ†’ Em i)) => (f p.1) p.2) s
            theorem ContinuousLinearMap.analyticOnNhd_uncurry_of_multilinear {๐•œ : Type u_1} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [NormedAddCommGroup G] [NormedSpace ๐•œ G] {ฮน : Type u_5} {Em : ฮน โ†’ Type u_6} [(i : ฮน) โ†’ NormedAddCommGroup (Em i)] [(i : ฮน) โ†’ NormedSpace ๐•œ (Em i)] [Fintype ฮน] (f : G โ†’L[๐•œ] ContinuousMultilinearMap ๐•œ Em F) {s : Set (G ร— ((i : ฮน) โ†’ Em i))} :
            AnalyticOnNhd ๐•œ (fun (p : G ร— ((i : ฮน) โ†’ Em i)) => (f p.1) p.2) s
            theorem ContinuousLinearMap.analyticOn_uncurry_of_multilinear {๐•œ : Type u_1} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [NormedAddCommGroup G] [NormedSpace ๐•œ G] {ฮน : Type u_5} {Em : ฮน โ†’ Type u_6} [(i : ฮน) โ†’ NormedAddCommGroup (Em i)] [(i : ฮน) โ†’ NormedSpace ๐•œ (Em i)] [Fintype ฮน] (f : G โ†’L[๐•œ] ContinuousMultilinearMap ๐•œ Em F) {s : Set (G ร— ((i : ฮน) โ†’ Em i))} :
            AnalyticOn ๐•œ (fun (p : G ร— ((i : ฮน) โ†’ Em i)) => (f p.1) p.2) s
            @[deprecated ContinuousLinearMap.analyticOn_uncurry_of_multilinear]
            theorem ContinuousLinearMap.analyticWithinOn_uncurry_of_multilinear {๐•œ : Type u_1} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [NormedAddCommGroup G] [NormedSpace ๐•œ G] {ฮน : Type u_5} {Em : ฮน โ†’ Type u_6} [(i : ฮน) โ†’ NormedAddCommGroup (Em i)] [(i : ฮน) โ†’ NormedSpace ๐•œ (Em i)] [Fintype ฮน] (f : G โ†’L[๐•œ] ContinuousMultilinearMap ๐•œ Em F) {s : Set (G ร— ((i : ฮน) โ†’ Em i))} :
            AnalyticOn ๐•œ (fun (p : G ร— ((i : ฮน) โ†’ Em i)) => (f p.1) p.2) s

            Alias of ContinuousLinearMap.analyticOn_uncurry_of_multilinear.

            theorem ContinuousLinearMap.analyticAt_uncurry_of_multilinear {๐•œ : Type u_1} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [NormedAddCommGroup G] [NormedSpace ๐•œ G] {ฮน : Type u_5} {Em : ฮน โ†’ Type u_6} [(i : ฮน) โ†’ NormedAddCommGroup (Em i)] [(i : ฮน) โ†’ NormedSpace ๐•œ (Em i)] [Fintype ฮน] (f : G โ†’L[๐•œ] ContinuousMultilinearMap ๐•œ Em F) {x : G ร— ((i : ฮน) โ†’ Em i)} :
            AnalyticAt ๐•œ (fun (p : G ร— ((i : ฮน) โ†’ Em i)) => (f p.1) p.2) x
            theorem ContinuousLinearMap.analyticWithinAt_uncurry_of_multilinear {๐•œ : Type u_1} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [NormedAddCommGroup G] [NormedSpace ๐•œ G] {ฮน : Type u_5} {Em : ฮน โ†’ Type u_6} [(i : ฮน) โ†’ NormedAddCommGroup (Em i)] [(i : ฮน) โ†’ NormedSpace ๐•œ (Em i)] [Fintype ฮน] (f : G โ†’L[๐•œ] ContinuousMultilinearMap ๐•œ Em F) {s : Set (G ร— ((i : ฮน) โ†’ Em i))} {x : G ร— ((i : ฮน) โ†’ Em i)} :
            AnalyticWithinAt ๐•œ (fun (p : G ร— ((i : ฮน) โ†’ Em i)) => (f p.1) p.2) s x