Documentation

Mathlib.SetTheory.Ordinal.FixedPoint

Fixed points of normal functions #

We prove various statements about the fixed points of normal ordinal functions. We state them in three forms: as statements about type-indexed families of normal functions, as statements about ordinal-indexed families of normal functions, and as statements about a single normal function. For the most part, the first case encompasses the others.

Moreover, we prove some lemmas about the fixed points of specific normal functions.

Main definitions and results #

Fixed points of type-indexed families of ordinals #

The next common fixed point, at least a, for a family of normal functions.

This is defined for any family of functions, as the supremum of all values reachable by applying finitely many functions in the family to a.

Ordinal.nfpFamily_fp shows this is a fixed point, Ordinal.le_nfpFamily shows it's at least a, and Ordinal.nfpFamily_le_fp shows this is the least ordinal with these properties.

Equations
Instances For
    theorem Ordinal.nfpFamily_le {ι : Type u} {f : ιOrdinal.{max u v}Ordinal.{max u v} } {a : Ordinal.{max u v} } {b : Ordinal.{max u v} } :
    (∀ (l : List ι), List.foldr f a l b)Ordinal.nfpFamily f a b
    theorem Ordinal.nfpFamily_monotone {ι : Type u} {f : ιOrdinal.{max u v}Ordinal.{max u v} } (hf : ∀ (i : ι), Monotone (f i)) :
    theorem Ordinal.apply_lt_nfpFamily {ι : Type u} {f : ιOrdinal.{max u v}Ordinal.{max u v} } (H : ∀ (i : ι), Ordinal.IsNormal (f i)) {a : Ordinal.{max u v} } {b : Ordinal.{max u v} } (hb : b < Ordinal.nfpFamily f a) (i : ι) :
    theorem Ordinal.apply_lt_nfpFamily_iff {ι : Type u} {f : ιOrdinal.{max u v}Ordinal.{max u v} } [Nonempty ι] (H : ∀ (i : ι), Ordinal.IsNormal (f i)) {a : Ordinal.{max u v} } {b : Ordinal.{max u v} } :
    (∀ (i : ι), f i b < Ordinal.nfpFamily f a) b < Ordinal.nfpFamily f a
    theorem Ordinal.nfpFamily_le_apply {ι : Type u} {f : ιOrdinal.{max u v}Ordinal.{max u v} } [Nonempty ι] (H : ∀ (i : ι), Ordinal.IsNormal (f i)) {a : Ordinal.{max u v} } {b : Ordinal.{max u v} } :
    (∃ (i : ι), Ordinal.nfpFamily f a f i b) Ordinal.nfpFamily f a b
    theorem Ordinal.nfpFamily_le_fp {ι : Type u} {f : ιOrdinal.{max u v}Ordinal.{max u v} } (H : ∀ (i : ι), Monotone (f i)) {a : Ordinal.{max u v} } {b : Ordinal.{max u v} } (ab : a b) (h : ∀ (i : ι), f i b b) :
    theorem Ordinal.apply_le_nfpFamily {ι : Type u} [hι : Nonempty ι] {f : ιOrdinal.{max u v}Ordinal.{max u v} } (H : ∀ (i : ι), Ordinal.IsNormal (f i)) {a : Ordinal.{max u v} } {b : Ordinal.{max u v} } :
    (∀ (i : ι), f i b Ordinal.nfpFamily f a) b Ordinal.nfpFamily f a
    theorem Ordinal.nfpFamily_eq_self {ι : Type u} {f : ιOrdinal.{max u u_1}Ordinal.{max u u_1} } {a : Ordinal.{max u u_1} } (h : ∀ (i : ι), f i a = a) :
    theorem Ordinal.not_bddAbove_fp_family {ι : Type u} {f : ιOrdinal.{max u v}Ordinal.{max u v} } (H : ∀ (i : ι), Ordinal.IsNormal (f i)) :
    ¬BddAbove (⋂ (i : ι), Function.fixedPoints (f i))

    A generalization of the fixed point lemma for normal functions: any family of normal functions has an unbounded set of common fixed points.

    @[deprecated Ordinal.not_bddAbove_fp_family]
    theorem Ordinal.fp_family_unbounded {ι : Type u} {f : ιOrdinal.{max u v}Ordinal.{max u v} } (H : ∀ (i : ι), Ordinal.IsNormal (f i)) :
    Set.Unbounded (fun (x1 x2 : Ordinal.{max u v} ) => x1 < x2) (⋂ (i : ι), Function.fixedPoints (f i))

    The derivative of a family of normal functions is the sequence of their common fixed points.

    This is defined for all functions such that Ordinal.derivFamily_zero, Ordinal.derivFamily_succ, and Ordinal.derivFamily_limit are satisfied.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem Ordinal.derivFamily_limit {ι : Type u} (f : ιOrdinal.{max u v}Ordinal.{max u v} ) {o : Ordinal.{max u v} } :
      o.IsLimitOrdinal.derivFamily f o = o.bsup fun (a : Ordinal.{max u v} ) (x : a < o) => Ordinal.derivFamily f a
      @[deprecated Ordinal.isNormal_derivFamily]

      Alias of Ordinal.isNormal_derivFamily.

      theorem Ordinal.le_iff_derivFamily {ι : Type u} {f : ιOrdinal.{max u v}Ordinal.{max u v} } (H : ∀ (i : ι), Ordinal.IsNormal (f i)) {a : Ordinal.{max u v} } :
      (∀ (i : ι), f i a a) ∃ (o : Ordinal.{max u v} ), Ordinal.derivFamily f o = a
      theorem Ordinal.fp_iff_derivFamily {ι : Type u} {f : ιOrdinal.{max u v}Ordinal.{max u v} } (H : ∀ (i : ι), Ordinal.IsNormal (f i)) {a : Ordinal.{max u v} } :
      (∀ (i : ι), f i a = a) ∃ (o : Ordinal.{max u v} ), Ordinal.derivFamily f o = a
      theorem Ordinal.derivFamily_eq_enumOrd {ι : Type u} {f : ιOrdinal.{max u v}Ordinal.{max u v} } (H : ∀ (i : ι), Ordinal.IsNormal (f i)) :

      For a family of normal functions, Ordinal.derivFamily enumerates the common fixed points.

      Fixed points of ordinal-indexed families of ordinals #

      The next common fixed point, at least a, for a family of normal functions indexed by ordinals.

      This is defined as Ordinal.nfpFamily of the type-indexed family associated to f.

      Equations
      Instances For
        theorem Ordinal.nfpBFamily_eq_nfpFamily {o : Ordinal.{u}} (f : (b : Ordinal.{u}) → b < oOrdinal.{max u v}Ordinal.{max u v} ) :
        o.nfpBFamily f = Ordinal.nfpFamily (o.familyOfBFamily f)
        theorem Ordinal.foldr_le_nfpBFamily {o : Ordinal.{u}} (f : (b : Ordinal.{u}) → b < oOrdinal.{max u v}Ordinal.{max u v} ) (a : Ordinal.{max u v} ) (l : List o.toType) :
        List.foldr (o.familyOfBFamily f) a l o.nfpBFamily f a
        theorem Ordinal.le_nfpBFamily {o : Ordinal.{u}} (f : (b : Ordinal.{u}) → b < oOrdinal.{max u v}Ordinal.{max u v} ) (a : Ordinal.{max v u} ) :
        a o.nfpBFamily f a
        theorem Ordinal.lt_nfpBFamily {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{max u v}Ordinal.{max u v} } {a : Ordinal.{max v u} } {b : Ordinal.{max v u} } :
        a < o.nfpBFamily f b ∃ (l : List o.toType), a < List.foldr (o.familyOfBFamily f) b l
        theorem Ordinal.nfpBFamily_le_iff {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{max u v}Ordinal.{max u v} } {a : Ordinal.{max v u} } {b : Ordinal.{max v u} } :
        o.nfpBFamily f a b ∀ (l : List o.toType), List.foldr (o.familyOfBFamily f) a l b
        theorem Ordinal.nfpBFamily_le {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{max u v}Ordinal.{max u v} } {a : Ordinal.{max u v} } {b : Ordinal.{max u v} } :
        (∀ (l : List o.toType), List.foldr (o.familyOfBFamily f) a l b)o.nfpBFamily f a b
        theorem Ordinal.nfpBFamily_monotone {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{max u v}Ordinal.{max u v} } (hf : ∀ (i : Ordinal.{u}) (hi : i < o), Monotone (f i hi)) :
        Monotone (o.nfpBFamily f)
        theorem Ordinal.apply_lt_nfpBFamily {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{max u v}Ordinal.{max u v} } (H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)) {a : Ordinal.{max v u} } {b : Ordinal.{max v u} } (hb : b < o.nfpBFamily f a) (i : Ordinal.{u}) (hi : i < o) :
        f i hi b < o.nfpBFamily f a
        theorem Ordinal.apply_lt_nfpBFamily_iff {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{max u v}Ordinal.{max u v} } (ho : o 0) (H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)) {a : Ordinal.{max v u} } {b : Ordinal.{max u v} } :
        (∀ (i : Ordinal.{u}) (hi : i < o), f i hi b < o.nfpBFamily f a) b < o.nfpBFamily f a
        theorem Ordinal.nfpBFamily_le_apply {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{max u v}Ordinal.{max u v} } (ho : o 0) (H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)) {a : Ordinal.{max v u} } {b : Ordinal.{max u v} } :
        (∃ (i : Ordinal.{u}) (hi : i < o), o.nfpBFamily f a f i hi b) o.nfpBFamily f a b
        theorem Ordinal.nfpBFamily_le_fp {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{max u v}Ordinal.{max u v} } (H : ∀ (i : Ordinal.{u}) (hi : i < o), Monotone (f i hi)) {a : Ordinal.{max u v} } {b : Ordinal.{max u v} } (ab : a b) (h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi b b) :
        o.nfpBFamily f a b
        theorem Ordinal.nfpBFamily_fp {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{max u v}Ordinal.{max u v} } {i : Ordinal.{u}} {hi : i < o} (H : Ordinal.IsNormal (f i hi)) (a : Ordinal.{max v u} ) :
        f i hi (o.nfpBFamily f a) = o.nfpBFamily f a
        theorem Ordinal.apply_le_nfpBFamily {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{max u v}Ordinal.{max u v} } (ho : o 0) (H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)) {a : Ordinal.{max v u} } {b : Ordinal.{max u v} } :
        (∀ (i : Ordinal.{u}) (hi : i < o), f i hi b o.nfpBFamily f a) b o.nfpBFamily f a
        theorem Ordinal.nfpBFamily_eq_self {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{max u v}Ordinal.{max u v} } {a : Ordinal.{max u v} } (h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi a = a) :
        o.nfpBFamily f a = a
        theorem Ordinal.not_bddAbove_fp_bfamily {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{max u v}Ordinal.{max u v} } (H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)) :
        ¬BddAbove (⋂ (i : Ordinal.{u}), ⋂ (hi : i < o), Function.fixedPoints (f i hi))

        A generalization of the fixed point lemma for normal functions: any family of normal functions has an unbounded set of common fixed points.

        @[deprecated Ordinal.not_bddAbove_fp_bfamily]
        theorem Ordinal.fp_bfamily_unbounded {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{max u v}Ordinal.{max u v} } (H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)) :
        Set.Unbounded (fun (x1 x2 : Ordinal.{max u v} ) => x1 < x2) (⋂ (i : Ordinal.{u}), ⋂ (hi : i < o), Function.fixedPoints (f i hi))

        A generalization of the fixed point lemma for normal functions: any family of normal functions has an unbounded set of common fixed points.

        The derivative of a family of normal functions is the sequence of their common fixed points.

        This is defined as Ordinal.derivFamily of the type-indexed family associated to f.

        Equations
        Instances For
          theorem Ordinal.derivBFamily_eq_derivFamily {o : Ordinal.{u}} (f : (b : Ordinal.{u}) → b < oOrdinal.{max u v}Ordinal.{max u v} ) :
          o.derivBFamily f = Ordinal.derivFamily (o.familyOfBFamily f)
          @[deprecated Ordinal.isNormal_derivBFamily]

          Alias of Ordinal.isNormal_derivBFamily.

          theorem Ordinal.derivBFamily_fp {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{max u v}Ordinal.{max u v} } {i : Ordinal.{u}} {hi : i < o} (H : Ordinal.IsNormal (f i hi)) (a : Ordinal.{max u v} ) :
          f i hi (o.derivBFamily f a) = o.derivBFamily f a
          theorem Ordinal.le_iff_derivBFamily {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{max u v}Ordinal.{max u v} } (H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)) {a : Ordinal.{max u v} } :
          (∀ (i : Ordinal.{u}) (hi : i < o), f i hi a a) ∃ (b : Ordinal.{max v u} ), o.derivBFamily f b = a
          theorem Ordinal.fp_iff_derivBFamily {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{max u v}Ordinal.{max u v} } (H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)) {a : Ordinal.{max u v} } :
          (∀ (i : Ordinal.{u}) (hi : i < o), f i hi a = a) ∃ (b : Ordinal.{max v u} ), o.derivBFamily f b = a
          theorem Ordinal.derivBFamily_eq_enumOrd {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{max u v}Ordinal.{max u v} } (H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)) :
          o.derivBFamily f = Ordinal.enumOrd (⋂ (i : Ordinal.{u}), ⋂ (hi : i < o), Function.fixedPoints (f i hi))

          For a family of normal functions, Ordinal.derivBFamily enumerates the common fixed points.

          Fixed points of a single function #

          The next fixed point function, the least fixed point of the normal function f, at least a.

          This is defined as ordinal.nfpFamily applied to a family consisting only of f.

          Equations
          Instances For
            @[deprecated]
            theorem Ordinal.lt_nfp {f : Ordinal.{u}Ordinal.{u}} {a : Ordinal.{u}} {b : Ordinal.{u}} :
            a < Ordinal.nfp f b ∃ (n : ), a < f^[n] b
            theorem Ordinal.nfp_le_iff {f : Ordinal.{u}Ordinal.{u}} {a : Ordinal.{u}} {b : Ordinal.{u}} :
            Ordinal.nfp f a b ∀ (n : ), f^[n] a b
            theorem Ordinal.nfp_le {f : Ordinal.{u}Ordinal.{u}} {a : Ordinal.{u}} {b : Ordinal.{u}} :
            (∀ (n : ), f^[n] a b)Ordinal.nfp f a b
            @[simp]
            theorem Ordinal.nfp_le_fp {f : Ordinal.{u_1}Ordinal.{u_1}} (H : Monotone f) {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (ab : a b) (h : f b b) :

            The fixed point lemma for normal functions: any normal function has an unbounded set of fixed points.

            @[deprecated Ordinal.not_bddAbove_fp]

            The fixed point lemma for normal functions: any normal function has an unbounded set of fixed points.

            The derivative of a normal function f is the sequence of fixed points of f.

            This is defined as Ordinal.derivFamily applied to a trivial family consisting only of f.

            Equations
            Instances For
              theorem Ordinal.deriv_limit (f : Ordinal.{u}Ordinal.{u}) {o : Ordinal.{u}} :
              o.IsLimitOrdinal.deriv f o = o.bsup fun (a : Ordinal.{u}) (x : a < o) => Ordinal.deriv f a
              @[deprecated Ordinal.isNormal_deriv]

              Alias of Ordinal.isNormal_deriv.

              Ordinal.deriv enumerates the fixed points of a normal function.

              @[simp]

              Fixed points of addition #

              @[deprecated Ordinal.nfp_add_eq_mul_omega0]

              Alias of Ordinal.nfp_add_eq_mul_omega0.

              @[deprecated Ordinal.add_eq_right_iff_mul_omega0_le]

              Alias of Ordinal.add_eq_right_iff_mul_omega0_le.

              @[deprecated Ordinal.add_le_right_iff_mul_omega0_le]

              Alias of Ordinal.add_le_right_iff_mul_omega0_le.

              @[deprecated Ordinal.deriv_add_eq_mul_omega0_add]

              Alias of Ordinal.deriv_add_eq_mul_omega0_add.

              Fixed points of multiplication #

              @[simp]
              theorem Ordinal.nfp_mul_one {a : Ordinal.{u_1}} (ha : 0 < a) :
              Ordinal.nfp (fun (x : Ordinal.{u_1}) => a * x) 1 = a ^ Ordinal.omega0
              @[simp]
              theorem Ordinal.nfp_mul_zero (a : Ordinal.{u_1}) :
              Ordinal.nfp (fun (x : Ordinal.{u_1}) => a * x) 0 = 0
              theorem Ordinal.nfp_mul_eq_opow_omega0 {a : Ordinal.{u}} {b : Ordinal.{u}} (hb : 0 < b) (hba : b a ^ Ordinal.omega0) :
              Ordinal.nfp (fun (x : Ordinal.{u}) => a * x) b = a ^ Ordinal.omega0
              @[deprecated Ordinal.nfp_mul_eq_opow_omega0]
              theorem Ordinal.nfp_mul_eq_opow_omega {a : Ordinal.{u}} {b : Ordinal.{u}} (hb : 0 < b) (hba : b a ^ Ordinal.omega0) :
              Ordinal.nfp (fun (x : Ordinal.{u}) => a * x) b = a ^ Ordinal.omega0

              Alias of Ordinal.nfp_mul_eq_opow_omega0.

              @[deprecated Ordinal.eq_zero_or_opow_omega0_le_of_mul_eq_right]

              Alias of Ordinal.eq_zero_or_opow_omega0_le_of_mul_eq_right.

              @[deprecated Ordinal.mul_eq_right_iff_opow_omega0_dvd]

              Alias of Ordinal.mul_eq_right_iff_opow_omega0_dvd.

              @[deprecated Ordinal.mul_le_right_iff_opow_omega0_dvd]

              Alias of Ordinal.mul_le_right_iff_opow_omega0_dvd.

              theorem Ordinal.nfp_mul_opow_omega0_add {a : Ordinal.{u}} {c : Ordinal.{u}} (b : Ordinal.{u}) (ha : 0 < a) (hc : 0 < c) (hca : c a ^ Ordinal.omega0) :
              @[deprecated Ordinal.nfp_mul_opow_omega0_add]
              theorem Ordinal.nfp_mul_opow_omega_add {a : Ordinal.{u}} {c : Ordinal.{u}} (b : Ordinal.{u}) (ha : 0 < a) (hc : 0 < c) (hca : c a ^ Ordinal.omega0) :

              Alias of Ordinal.nfp_mul_opow_omega0_add.

              @[deprecated Ordinal.deriv_mul_eq_opow_omega0_mul]
              theorem Ordinal.deriv_mul_eq_opow_omega_mul {a : Ordinal.{u}} (ha : 0 < a) (b : Ordinal.{u}) :
              Ordinal.deriv (fun (x : Ordinal.{u}) => a * x) b = a ^ Ordinal.omega0 * b

              Alias of Ordinal.deriv_mul_eq_opow_omega0_mul.