Documentation

Mathlib.Analysis.Analytic.Order

Vanishing Order of Analytic Functions #

This file defines the order of vanishing of an analytic function f at a point zโ‚€, as an element of โ„•โˆž.

TODO #

Uniformize API between analytic and meromorphic functions

Vanishing Order at a Point: Definition and Characterization #

noncomputable def analyticOrderAt {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] (f : ๐•œ โ†’ E) (zโ‚€ : ๐•œ) :

The order of vanishing of f at zโ‚€, as an element of โ„•โˆž.

The order is defined to be โˆž if f is identically 0 on a neighbourhood of zโ‚€, and otherwise the unique n such that f can locally be written as f z = (z - zโ‚€) ^ n โ€ข g z, where g is analytic and does not vanish at zโ‚€. See AnalyticAt.analyticOrderAt_eq_top and AnalyticAt.analyticOrderAt_eq_natCast for these equivalences.

If f isn't analytic at zโ‚€, then analyticOrderAt f zโ‚€ returns a junk value of 0.

Equations
Instances For
    @[deprecated analyticOrderAt (since := "2025-05-02")]
    def AnalyticAt.order {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] (f : ๐•œ โ†’ E) (zโ‚€ : ๐•œ) :

    Alias of analyticOrderAt.


    The order of vanishing of f at zโ‚€, as an element of โ„•โˆž.

    The order is defined to be โˆž if f is identically 0 on a neighbourhood of zโ‚€, and otherwise the unique n such that f can locally be written as f z = (z - zโ‚€) ^ n โ€ข g z, where g is analytic and does not vanish at zโ‚€. See AnalyticAt.analyticOrderAt_eq_top and AnalyticAt.analyticOrderAt_eq_natCast for these equivalences.

    If f isn't analytic at zโ‚€, then analyticOrderAt f zโ‚€ returns a junk value of 0.

    Equations
    Instances For
      noncomputable def analyticOrderNatAt {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] (f : ๐•œ โ†’ E) (zโ‚€ : ๐•œ) :

      The order of vanishing of f at zโ‚€, as an element of โ„•.

      The order is defined to be 0 if f is identically zero on a neighbourhood of zโ‚€, and is otherwise the unique n such that f can locally be written as f z = (z - zโ‚€) ^ n โ€ข g z, where g is analyticand does not vanish at zโ‚€. See AnalyticAt.analyticOrderAt_eq_top and AnalyticAt.analyticOrderAt_eq_natCast for these equivalences.

      If f isn't analytic at zโ‚€, then analyticOrderNatAt f zโ‚€ returns a junk value of 0.

      Equations
      Instances For
        @[simp]
        theorem analyticOrderAt_of_not_analyticAt {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} (hf : ยฌAnalyticAt ๐•œ f zโ‚€) :
        analyticOrderAt f zโ‚€ = 0
        @[simp]
        theorem analyticOrderNatAt_of_not_analyticAt {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} (hf : ยฌAnalyticAt ๐•œ f zโ‚€) :
        analyticOrderNatAt f zโ‚€ = 0
        @[simp]
        theorem Nat.cast_analyticOrderNatAt {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} (hf : analyticOrderAt f zโ‚€ โ‰  โŠค) :
        โ†‘(analyticOrderNatAt f zโ‚€) = analyticOrderAt f zโ‚€
        theorem analyticOrderAt_eq_top {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} :
        analyticOrderAt f zโ‚€ = โŠค โ†” โˆ€แถ  (z : ๐•œ) in nhds zโ‚€, f z = 0

        The order of a function f at a zโ‚€ is infinity iff f vanishes locally around zโ‚€.

        @[deprecated analyticOrderAt_eq_top (since := "2025-05-03")]
        theorem AnalyticAt.order_eq_top_iff {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} :
        analyticOrderAt f zโ‚€ = โŠค โ†” โˆ€แถ  (z : ๐•œ) in nhds zโ‚€, f z = 0

        Alias of analyticOrderAt_eq_top.


        The order of a function f at a zโ‚€ is infinity iff f vanishes locally around zโ‚€.

        theorem AnalyticAt.analyticOrderAt_eq_natCast {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {n : โ„•} {zโ‚€ : ๐•œ} (hf : AnalyticAt ๐•œ f zโ‚€) :
        analyticOrderAt f zโ‚€ = โ†‘n โ†” โˆƒ (g : ๐•œ โ†’ E), AnalyticAt ๐•œ g zโ‚€ โˆง g zโ‚€ โ‰  0 โˆง โˆ€แถ  (z : ๐•œ) in nhds zโ‚€, f z = (z - zโ‚€) ^ n โ€ข g z

        The order of an analytic function f at zโ‚€ equals a natural number n iff f can locally be written as f z = (z - zโ‚€) ^ n โ€ข g z, where g is analytic and does not vanish at zโ‚€.

        @[deprecated AnalyticAt.analyticOrderAt_eq_natCast (since := "2025-05-03")]
        theorem AnalyticAt.order_eq_nat_iff {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {n : โ„•} {zโ‚€ : ๐•œ} (hf : AnalyticAt ๐•œ f zโ‚€) :
        analyticOrderAt f zโ‚€ = โ†‘n โ†” โˆƒ (g : ๐•œ โ†’ E), AnalyticAt ๐•œ g zโ‚€ โˆง g zโ‚€ โ‰  0 โˆง โˆ€แถ  (z : ๐•œ) in nhds zโ‚€, f z = (z - zโ‚€) ^ n โ€ข g z

        Alias of AnalyticAt.analyticOrderAt_eq_natCast.


        The order of an analytic function f at zโ‚€ equals a natural number n iff f can locally be written as f z = (z - zโ‚€) ^ n โ€ข g z, where g is analytic and does not vanish at zโ‚€.

        theorem AnalyticAt.analyticOrderNatAt_eq_iff {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} (hf : AnalyticAt ๐•œ f zโ‚€) (hf' : analyticOrderAt f zโ‚€ โ‰  โŠค) {n : โ„•} :
        analyticOrderNatAt f zโ‚€ = n โ†” โˆƒ (g : ๐•œ โ†’ E), AnalyticAt ๐•œ g zโ‚€ โˆง g zโ‚€ โ‰  0 โˆง โˆ€แถ  (z : ๐•œ) in nhds zโ‚€, f z = (z - zโ‚€) ^ n โ€ข g z

        The order of an analytic function f at zโ‚€ equals a natural number n iff f can locally be written as f z = (z - zโ‚€) ^ n โ€ข g z, where g is analytic and does not vanish at zโ‚€.

        theorem AnalyticAt.analyticOrderAt_ne_top {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} (hf : AnalyticAt ๐•œ f zโ‚€) :
        analyticOrderAt f zโ‚€ โ‰  โŠค โ†” โˆƒ (g : ๐•œ โ†’ E), AnalyticAt ๐•œ g zโ‚€ โˆง g zโ‚€ โ‰  0 โˆง f =แถ [nhds zโ‚€] fun (z : ๐•œ) => (z - zโ‚€) ^ analyticOrderNatAt f zโ‚€ โ€ข g z

        The order of an analytic function f at zโ‚€ is finite iff f can locally be written as f z = (z - zโ‚€) ^ analyticOrderNatAt f zโ‚€ โ€ข g z, where g is analytic and does not vanish at zโ‚€.

        See MeromorphicNFAt.order_eq_zero_iff for an analogous statement about meromorphic functions in normal form.

        @[deprecated AnalyticAt.analyticOrderAt_ne_top (since := "2025-05-03")]
        theorem AnalyticAt.order_ne_top_iff {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} (hf : AnalyticAt ๐•œ f zโ‚€) :
        analyticOrderAt f zโ‚€ โ‰  โŠค โ†” โˆƒ (g : ๐•œ โ†’ E), AnalyticAt ๐•œ g zโ‚€ โˆง g zโ‚€ โ‰  0 โˆง f =แถ [nhds zโ‚€] fun (z : ๐•œ) => (z - zโ‚€) ^ analyticOrderNatAt f zโ‚€ โ€ข g z

        Alias of AnalyticAt.analyticOrderAt_ne_top.


        The order of an analytic function f at zโ‚€ is finite iff f can locally be written as f z = (z - zโ‚€) ^ analyticOrderNatAt f zโ‚€ โ€ข g z, where g is analytic and does not vanish at zโ‚€.

        See MeromorphicNFAt.order_eq_zero_iff for an analogous statement about meromorphic functions in normal form.

        @[deprecated AnalyticAt.analyticOrderAt_ne_top (since := "2025-02-03")]
        theorem AnalyticAt.order_neq_top_iff {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} (hf : AnalyticAt ๐•œ f zโ‚€) :
        analyticOrderAt f zโ‚€ โ‰  โŠค โ†” โˆƒ (g : ๐•œ โ†’ E), AnalyticAt ๐•œ g zโ‚€ โˆง g zโ‚€ โ‰  0 โˆง f =แถ [nhds zโ‚€] fun (z : ๐•œ) => (z - zโ‚€) ^ analyticOrderNatAt f zโ‚€ โ€ข g z

        Alias of AnalyticAt.analyticOrderAt_ne_top.


        The order of an analytic function f at zโ‚€ is finite iff f can locally be written as f z = (z - zโ‚€) ^ analyticOrderNatAt f zโ‚€ โ€ข g z, where g is analytic and does not vanish at zโ‚€.

        See MeromorphicNFAt.order_eq_zero_iff for an analogous statement about meromorphic functions in normal form.

        theorem analyticOrderAt_eq_zero {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} :
        analyticOrderAt f zโ‚€ = 0 โ†” ยฌAnalyticAt ๐•œ f zโ‚€ โˆจ f zโ‚€ โ‰  0
        theorem analyticOrderAt_ne_zero {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} :
        analyticOrderAt f zโ‚€ โ‰  0 โ†” AnalyticAt ๐•œ f zโ‚€ โˆง f zโ‚€ = 0
        theorem AnalyticAt.analyticOrderAt_eq_zero {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} (hf : AnalyticAt ๐•œ f zโ‚€) :
        analyticOrderAt f zโ‚€ = 0 โ†” f zโ‚€ โ‰  0

        The order of an analytic function f at zโ‚€ is zero iff f does not vanish at zโ‚€.

        @[deprecated AnalyticAt.analyticOrderAt_eq_zero (since := "2025-05-03")]
        theorem AnalyticAt.order_eq_zero_iff {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} (hf : AnalyticAt ๐•œ f zโ‚€) :
        analyticOrderAt f zโ‚€ = 0 โ†” f zโ‚€ โ‰  0

        Alias of AnalyticAt.analyticOrderAt_eq_zero.


        The order of an analytic function f at zโ‚€ is zero iff f does not vanish at zโ‚€.

        theorem AnalyticAt.analyticOrderAt_ne_zero {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} (hf : AnalyticAt ๐•œ f zโ‚€) :
        analyticOrderAt f zโ‚€ โ‰  0 โ†” f zโ‚€ = 0

        The order of an analytic function f at zโ‚€ is zero iff f does not vanish at zโ‚€.

        theorem apply_eq_zero_of_analyticOrderAt_ne_zero {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} (hf : analyticOrderAt f zโ‚€ โ‰  0) :
        f zโ‚€ = 0

        A function vanishes at a point if its analytic order is nonzero in โ„•โˆž.

        theorem apply_eq_zero_of_analyticOrderNatAt_ne_zero {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} (hf : analyticOrderNatAt f zโ‚€ โ‰  0) :
        f zโ‚€ = 0

        A function vanishes at a point if its analytic order is nonzero when converted to โ„•.

        @[deprecated apply_eq_zero_of_analyticOrderNatAt_ne_zero (since := "2025-05-03")]
        theorem AnalyticAt.apply_eq_zero_of_order_toNat_ne_zero {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} (hf : analyticOrderNatAt f zโ‚€ โ‰  0) :
        f zโ‚€ = 0

        Alias of apply_eq_zero_of_analyticOrderNatAt_ne_zero.


        A function vanishes at a point if its analytic order is nonzero when converted to โ„•.

        theorem natCast_le_analyticOrderAt {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} (hf : AnalyticAt ๐•œ f zโ‚€) {n : โ„•} :
        โ†‘n โ‰ค analyticOrderAt f zโ‚€ โ†” โˆƒ (g : ๐•œ โ†’ E), AnalyticAt ๐•œ g zโ‚€ โˆง โˆ€แถ  (z : ๐•œ) in nhds zโ‚€, f z = (z - zโ‚€) ^ n โ€ข g z

        Characterization of which natural numbers are โ‰ค hf.order. Useful for avoiding case splits, since it applies whether or not the order is โˆž.

        @[deprecated natCast_le_analyticOrderAt (since := "2025-05-03")]
        theorem natCast_le_order_iff {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} (hf : AnalyticAt ๐•œ f zโ‚€) {n : โ„•} :
        โ†‘n โ‰ค analyticOrderAt f zโ‚€ โ†” โˆƒ (g : ๐•œ โ†’ E), AnalyticAt ๐•œ g zโ‚€ โˆง โˆ€แถ  (z : ๐•œ) in nhds zโ‚€, f z = (z - zโ‚€) ^ n โ€ข g z

        Alias of natCast_le_analyticOrderAt.


        Characterization of which natural numbers are โ‰ค hf.order. Useful for avoiding case splits, since it applies whether or not the order is โˆž.

        theorem analyticOrderAt_congr {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f g : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} (hfg : f =แถ [nhds zโ‚€] g) :
        analyticOrderAt f zโ‚€ = analyticOrderAt g zโ‚€

        If two functions agree in a neighborhood of zโ‚€, then their orders at zโ‚€ agree.

        @[deprecated analyticOrderAt_congr (since := "2025-05-03")]
        theorem AnalyticAt.order_congr {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f g : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} (hfg : f =แถ [nhds zโ‚€] g) :
        analyticOrderAt f zโ‚€ = analyticOrderAt g zโ‚€

        Alias of analyticOrderAt_congr.


        If two functions agree in a neighborhood of zโ‚€, then their orders at zโ‚€ agree.

        @[simp]
        theorem analyticOrderAt_neg {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} :
        analyticOrderAt (-f) zโ‚€ = analyticOrderAt f zโ‚€
        theorem le_analyticOrderAt_add {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f g : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} :
        min (analyticOrderAt f zโ‚€) (analyticOrderAt g zโ‚€) โ‰ค analyticOrderAt (f + g) zโ‚€

        The order of a sum is at least the minimum of the orders of the summands.

        @[deprecated le_analyticOrderAt_add (since := "2025-05-03")]
        theorem AnalyticAt.order_add {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f g : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} :
        min (analyticOrderAt f zโ‚€) (analyticOrderAt g zโ‚€) โ‰ค analyticOrderAt (f + g) zโ‚€

        Alias of le_analyticOrderAt_add.


        The order of a sum is at least the minimum of the orders of the summands.

        theorem le_analyticOrderAt_sub {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f g : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} :
        min (analyticOrderAt f zโ‚€) (analyticOrderAt g zโ‚€) โ‰ค analyticOrderAt (f - g) zโ‚€
        theorem analyticOrderAt_add_eq_left_of_lt {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f g : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} (hfg : analyticOrderAt f zโ‚€ < analyticOrderAt g zโ‚€) :
        analyticOrderAt (f + g) zโ‚€ = analyticOrderAt f zโ‚€
        theorem analyticOrderAt_add_eq_right_of_lt {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f g : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} (hgf : analyticOrderAt g zโ‚€ < analyticOrderAt f zโ‚€) :
        analyticOrderAt (f + g) zโ‚€ = analyticOrderAt g zโ‚€
        @[deprecated le_analyticOrderAt_add (since := "2025-05-03")]
        theorem order_add_of_order_lt_order {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f g : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} :
        min (analyticOrderAt f zโ‚€) (analyticOrderAt g zโ‚€) โ‰ค analyticOrderAt (f + g) zโ‚€

        Alias of le_analyticOrderAt_add.


        The order of a sum is at least the minimum of the orders of the summands.

        theorem analyticOrderAt_add_of_ne {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f g : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} (hfg : analyticOrderAt f zโ‚€ โ‰  analyticOrderAt g zโ‚€) :
        analyticOrderAt (f + g) zโ‚€ = min (analyticOrderAt f zโ‚€) (analyticOrderAt g zโ‚€)

        If two functions have unequal orders, then the order of their sum is exactly the minimum of the orders of the summands.

        @[deprecated analyticOrderAt_add_of_ne (since := "2025-05-03")]
        theorem AnalyticAt.order_add_of_order_ne_order {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f g : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} (hfg : analyticOrderAt f zโ‚€ โ‰  analyticOrderAt g zโ‚€) :
        analyticOrderAt (f + g) zโ‚€ = min (analyticOrderAt f zโ‚€) (analyticOrderAt g zโ‚€)

        Alias of analyticOrderAt_add_of_ne.


        If two functions have unequal orders, then the order of their sum is exactly the minimum of the orders of the summands.

        theorem analyticOrderAt_smul_eq_top_of_left {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {g : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} {f : ๐•œ โ†’ ๐•œ} (hf : analyticOrderAt f zโ‚€ = โŠค) :
        theorem analyticOrderAt_smul_eq_top_of_right {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {g : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} {f : ๐•œ โ†’ ๐•œ} (hg : analyticOrderAt g zโ‚€ = โŠค) :
        theorem analyticOrderAt_smul {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {g : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} {f : ๐•œ โ†’ ๐•œ} (hf : AnalyticAt ๐•œ f zโ‚€) (hg : AnalyticAt ๐•œ g zโ‚€) :
        analyticOrderAt (f โ€ข g) zโ‚€ = analyticOrderAt f zโ‚€ + analyticOrderAt g zโ‚€

        The order is additive when scalar multiplying analytic functions.

        Vanishing Order at a Point: Elementary Computations #

        @[simp]
        theorem analyticOrderAt_centeredMonomial {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {zโ‚€ : ๐•œ} {n : โ„•} :
        analyticOrderAt ((fun (x : ๐•œ) => x - zโ‚€) ^ n) zโ‚€ = โ†‘n

        Simplifier lemma for the order of a centered monomial

        @[deprecated analyticOrderAt_centeredMonomial (since := "2025-05-03")]
        theorem analyticAt_order_centeredMonomial {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {zโ‚€ : ๐•œ} {n : โ„•} :
        analyticOrderAt ((fun (x : ๐•œ) => x - zโ‚€) ^ n) zโ‚€ = โ†‘n

        Alias of analyticOrderAt_centeredMonomial.


        Simplifier lemma for the order of a centered monomial

        theorem analyticOrderAt_mul_eq_top_of_left {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {f g : ๐•œ โ†’ ๐•œ} {zโ‚€ : ๐•œ} (hf : analyticOrderAt f zโ‚€ = โŠค) :
        analyticOrderAt (f * g) zโ‚€ = โŠค
        @[deprecated analyticOrderAt_mul_eq_top_of_left (since := "2025-05-03")]
        theorem AnalyticAt.order_mul_of_order_eq_top {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {f g : ๐•œ โ†’ ๐•œ} {zโ‚€ : ๐•œ} (hf : analyticOrderAt f zโ‚€ = โŠค) :
        analyticOrderAt (f * g) zโ‚€ = โŠค

        Alias of analyticOrderAt_mul_eq_top_of_left.

        theorem analyticOrderAt_mul_eq_top_of_right {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {f g : ๐•œ โ†’ ๐•œ} {zโ‚€ : ๐•œ} (hg : analyticOrderAt g zโ‚€ = โŠค) :
        analyticOrderAt (f * g) zโ‚€ = โŠค
        theorem analyticOrderAt_mul {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {f g : ๐•œ โ†’ ๐•œ} {zโ‚€ : ๐•œ} (hf : AnalyticAt ๐•œ f zโ‚€) (hg : AnalyticAt ๐•œ g zโ‚€) :
        analyticOrderAt (f * g) zโ‚€ = analyticOrderAt f zโ‚€ + analyticOrderAt g zโ‚€

        The order is additive when multiplying analytic functions.

        @[deprecated analyticOrderAt_mul (since := "2025-05-03")]
        theorem AnalyticAt.order_mul {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {f g : ๐•œ โ†’ ๐•œ} {zโ‚€ : ๐•œ} (hf : AnalyticAt ๐•œ f zโ‚€) (hg : AnalyticAt ๐•œ g zโ‚€) :
        analyticOrderAt (f * g) zโ‚€ = analyticOrderAt f zโ‚€ + analyticOrderAt g zโ‚€

        Alias of analyticOrderAt_mul.


        The order is additive when multiplying analytic functions.

        theorem analyticOrderNatAt_mul {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {f g : ๐•œ โ†’ ๐•œ} {zโ‚€ : ๐•œ} (hf : AnalyticAt ๐•œ f zโ‚€) (hg : AnalyticAt ๐•œ g zโ‚€) (hf' : analyticOrderAt f zโ‚€ โ‰  โŠค) (hg' : analyticOrderAt g zโ‚€ โ‰  โŠค) :
        analyticOrderNatAt (f * g) zโ‚€ = analyticOrderNatAt f zโ‚€ + analyticOrderNatAt g zโ‚€

        The order is additive when multiplying analytic functions.

        theorem analyticOrderAt_pow {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {f : ๐•œ โ†’ ๐•œ} {zโ‚€ : ๐•œ} (hf : AnalyticAt ๐•œ f zโ‚€) (n : โ„•) :
        analyticOrderAt (f ^ n) zโ‚€ = n โ€ข analyticOrderAt f zโ‚€

        The order multiplies by n when taking an analytic function to its nth power.

        @[deprecated analyticOrderAt_pow (since := "2025-05-03")]
        theorem AnalyticAt.order_pow {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {f : ๐•œ โ†’ ๐•œ} {zโ‚€ : ๐•œ} (hf : AnalyticAt ๐•œ f zโ‚€) (n : โ„•) :
        analyticOrderAt (f ^ n) zโ‚€ = n โ€ข analyticOrderAt f zโ‚€

        Alias of analyticOrderAt_pow.


        The order multiplies by n when taking an analytic function to its nth power.

        theorem analyticOrderNatAt_pow {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {f : ๐•œ โ†’ ๐•œ} {zโ‚€ : ๐•œ} (hf : AnalyticAt ๐•œ f zโ‚€) (n : โ„•) :
        analyticOrderNatAt (f ^ n) zโ‚€ = n โ€ข analyticOrderNatAt f zโ‚€

        The order multiplies by n when taking an analytic function to its nth power.

        Level Sets of the Order Function #

        theorem AnalyticOnNhd.isClopen_setOf_analyticOrderAt_eq_top {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {U : Set ๐•œ} {f : ๐•œ โ†’ E} (hf : AnalyticOnNhd ๐•œ f U) :
        IsClopen {u : โ†‘U | analyticOrderAt f โ†‘u = โŠค}

        The set where an analytic function has infinite order is clopen in its domain of analyticity.

        theorem AnalyticOnNhd.exists_analyticOrderAt_ne_top_iff_forall {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {U : Set ๐•œ} {f : ๐•œ โ†’ E} (hf : AnalyticOnNhd ๐•œ f U) (hU : IsConnected U) :
        (โˆƒ (u : โ†‘U), analyticOrderAt f โ†‘u โ‰  โŠค) โ†” โˆ€ (u : โ†‘U), analyticOrderAt f โ†‘u โ‰  โŠค

        On a connected set, there exists a point where a meromorphic function f has finite order iff f has finite order at every point.

        theorem AnalyticOnNhd.analyticOrderAt_ne_top_of_isPreconnected {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {U : Set ๐•œ} {f : ๐•œ โ†’ E} (hf : AnalyticOnNhd ๐•œ f U) {x y : ๐•œ} (hU : IsPreconnected U) (hโ‚x : x โˆˆ U) (hy : y โˆˆ U) (hโ‚‚x : analyticOrderAt f x โ‰  โŠค) :

        On a preconnected set, a meromorphic function has finite order at one point if it has finite order at another point.

        theorem AnalyticOnNhd.codiscrete_setOf_analyticOrderAt_eq_zero_or_top {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {U : Set ๐•œ} {f : ๐•œ โ†’ E} (hf : AnalyticOnNhd ๐•œ f U) :
        {u : โ†‘U | analyticOrderAt f โ†‘u = 0 โˆจ analyticOrderAt f โ†‘u = โŠค} โˆˆ Filter.codiscrete โ†‘U

        The set where an analytic function has zero or infinite order is discrete within its domain of analyticity.