Documentation

Arithmetization.ISigmaZero.Exponential.Exp

def LO.Arith.ext {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (u : V) (z : V) :
V
Equations
Instances For
    theorem LO.Arith.ext_graph {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (a : V) (b : V) (c : V) :
    a = LO.Arith.ext b c xc, x = c / b a = x % b
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      • =
      @[simp]
      theorem LO.Arith.ext_le_add {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (u : V) (z : V) :
      @[simp]
      theorem LO.Arith.ext_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {u : V} (z : V) (pos : 0 < u) :
      theorem LO.Arith.ext_add_of_dvd_sq_right {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {u : V} {z₁ : V} {z₂ : V} (pos : 0 < u) (h : u ^ 2 z₂) :
      LO.Arith.ext u (z₁ + z₂) = LO.Arith.ext u z₁
      theorem LO.Arith.ext_add_of_dvd_sq_left {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {u : V} {z₁ : V} {z₂ : V} (pos : 0 < u) (h : u ^ 2 z₁) :
      LO.Arith.ext u (z₁ + z₂) = LO.Arith.ext u z₂
      theorem LO.Arith.ext_rem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} {j : V} {z : V} (ppi : LO.Arith.PPow2 i) (ppj : LO.Arith.PPow2 j) (hij : i < j) :
      def LO.Arith.Exponential.Seq₀ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (X : V) (Y : V) :
      Equations
      Instances For
        def LO.Arith.Exponential.Seqₛ.Even {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (X : V) (Y : V) (u : V) :
        Equations
        Instances For
          def LO.Arith.Exponential.Seqₛ.Odd {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (X : V) (Y : V) (u : V) :
          Equations
          Instances For
            def LO.Arith.Exponential.Seqₛ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (y : V) (X : V) (Y : V) :
            Equations
            Instances For
              def LO.Arith.Exponential.Seqₘ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (x : V) (y : V) (X : V) (Y : V) :
              Equations
              Instances For
                def LO.Arith.Exponential {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (x : V) (y : V) :
                Equations
                Instances For
                  theorem LO.Arith.Exponential.Seqₛ.iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (y : V) (X : V) (Y : V) :
                  LO.Arith.Exponential.Seqₛ y X Y uy, u 2LO.Arith.PPow2 u((ext_u_XX, ext_u_X = LO.Arith.ext u X 2 * ext_u_X = LO.Arith.ext (u ^ 2) X) ext_u_YY, ext_u_Y = LO.Arith.ext u Y ext_u_Y ^ 2 = LO.Arith.ext (u ^ 2) Y) (ext_u_XX, ext_u_X = LO.Arith.ext u X 2 * ext_u_X + 1 = LO.Arith.ext (u ^ 2) X) ext_u_YY, ext_u_Y = LO.Arith.ext u Y 2 * ext_u_Y ^ 2 = LO.Arith.ext (u ^ 2) Y
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    theorem LO.Arith.Exponential.graph_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (x : V) (y : V) :
                    LO.Arith.Exponential x y x = 0 y = 1 Xy ^ 4, Yy ^ 4, (1 = LO.Arith.ext 4 X 2 = LO.Arith.ext 4 Y) LO.Arith.Exponential.Seqₛ y X Y uy ^ 2, u 2 LO.Arith.PPow2 u x = LO.Arith.ext u X y = LO.Arith.ext u Y
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      instance LO.Arith.exponential_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] :
                      𝚺₀-Relation LO.Arith.Exponential
                      Equations
                      • =
                      @[simp]
                      Equations
                      • =
                      Equations
                      • LO.Arith.Exponential.seqX₀ = 4
                      Instances For
                        Equations
                        • LO.Arith.Exponential.seqY₀ = 2 * 4
                        Instances For
                          theorem LO.Arith.Exponential.seq₀_zero_two {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] :
                          LO.Arith.Exponential.Seq₀ LO.Arith.Exponential.seqX₀ LO.Arith.Exponential.seqY₀
                          theorem LO.Arith.Exponential.Seq₀.rem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {X : V} {Y : V} {i : V} (h : LO.Arith.Exponential.Seq₀ X Y) (ppi : LO.Arith.PPow2 i) (hi : 4 < i) :
                          theorem LO.Arith.Exponential.Seqₛ.rem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y : V} {y' : V} {X : V} {Y : V} {i : V} (h : LO.Arith.Exponential.Seqₛ y X Y) (ppi : LO.Arith.PPow2 i) (hi : y' ^ 2 < i) (hy : y' y) :
                          theorem LO.Arith.Exponential.seqₛ_one_zero_two {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] :
                          LO.Arith.Exponential.Seqₛ 1 LO.Arith.Exponential.seqX₀ LO.Arith.Exponential.seqY₀
                          def LO.Arith.Exponential.append {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (i : V) (X : V) (z : V) :
                          V
                          Equations
                          Instances For
                            theorem LO.Arith.Exponential.append_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (i : V) (X : V) {z : V} (hz : z < i) :
                            theorem LO.Arith.Exponential.ext_append_last {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (i : V) (X : V) {z : V} (hz : z < i) :
                            theorem LO.Arith.Exponential.ext_append_of_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} {j : V} (hi : LO.Arith.PPow2 i) (hj : LO.Arith.PPow2 j) (hij : i < j) (X : V) (z : V) :
                            theorem LO.Arith.Exponential.Seqₛ.append {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {z : V} {x : V} {y : V} {X : V} {Y : V} {i : V} (h : LO.Arith.Exponential.Seqₛ z X Y) (ppi : LO.Arith.PPow2 i) (hz : z < i) :
                            theorem LO.Arith.Exponential.pow2_ext_of_seq₀_of_seqₛ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y : V} {X : V} {Y : V} (h₀ : LO.Arith.Exponential.Seq₀ X Y) (hₛ : LO.Arith.Exponential.Seqₛ y X Y) {i : V} (ne2 : i 2) (hi : i y ^ 2) (ppi : LO.Arith.PPow2 i) :
                            theorem LO.Arith.Exponential.le_sq_ext_of_seq₀_of_seqₛ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y : V} {X : V} {Y : V} (h₀ : LO.Arith.Exponential.Seq₀ X Y) (hₛ : LO.Arith.Exponential.Seqₛ y X Y) {i : V} (ne2 : i 2) (hi : i y ^ 2) (ppi : LO.Arith.PPow2 i) :
                            theorem LO.Arith.Exponential.two_mul_ext_le_of_seq₀_of_seqₛ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y : V} {X : V} {Y : V} (h₀ : LO.Arith.Exponential.Seq₀ X Y) (hₛ : LO.Arith.Exponential.Seqₛ y X Y) {i : V} (ne2 : i 2) (hi : i y ^ 2) (ppi : LO.Arith.PPow2 i) :
                            theorem LO.Arith.Exponential.exponential_even {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} :
                            LO.Arith.Exponential (2 * x) y ∃ (y' : V), y = y' ^ 2 LO.Arith.Exponential x y'
                            theorem LO.Arith.Exponential.bit_one {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} :
                            theorem LO.Arith.Exponential.exponential_odd {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} :
                            LO.Arith.Exponential (2 * x + 1) y ∃ (y' : V), y = 2 * y' ^ 2 LO.Arith.Exponential x y'
                            theorem LO.Arith.Exponential.two_le_ext_of_seq₀_of_seqₛ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y : V} {X : V} {Y : V} (h₀ : LO.Arith.Exponential.Seq₀ X Y) (hₛ : LO.Arith.Exponential.Seqₛ y X Y) {i : V} (ne2 : i 2) (hi : i y ^ 2) (ppi : LO.Arith.PPow2 i) :
                            theorem LO.Arith.Exponential.ext_le_ext_of_seq₀_of_seqₛ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y : V} {X : V} {Y : V} (h₀ : LO.Arith.Exponential.Seq₀ X Y) (hₛ : LO.Arith.Exponential.Seqₛ y X Y) {i : V} (ne2 : i 2) (hi : i y ^ 2) (ppi : LO.Arith.PPow2 i) :
                            theorem LO.Arith.Exponential.range_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} (h : LO.Arith.Exponential x y) :
                            0 < y
                            theorem LO.Arith.Exponential.lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} (h : LO.Arith.Exponential x y) :
                            x < y
                            @[simp]
                            theorem LO.Arith.Exponential.exponential_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} :
                            LO.Arith.Exponential (x + 1) y ∃ (z : V), y = 2 * z LO.Arith.Exponential x z
                            theorem LO.Arith.Exponential.succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} :

                            Alias of the reverse direction of LO.Arith.Exponential.exponential_succ_mul_two.

                            theorem LO.Arith.Exponential.one_le_ext_of_seq₀_of_seqₛ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y : V} {X : V} {Y : V} (h₀ : LO.Arith.Exponential.Seq₀ X Y) (hₛ : LO.Arith.Exponential.Seqₛ y X Y) {i : V} (ne2 : i 2) (hi : i y ^ 2) (ppi : LO.Arith.PPow2 i) :
                            theorem LO.Arith.Exponential.succ_lt_s {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} (h : LO.Arith.Exponential (x + 1) y) :
                            2 y
                            theorem LO.Arith.Exponential.uniq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y₁ : V} {y₂ : V} :
                            LO.Arith.Exponential x y₁LO.Arith.Exponential x y₂y₁ = y₂
                            theorem LO.Arith.Exponential.inj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x₁ : V} {x₂ : V} {y : V} :
                            LO.Arith.Exponential x₁ yLO.Arith.Exponential x₂ yx₁ = x₂
                            theorem LO.Arith.Exponential.exponential_elim {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} :
                            LO.Arith.Exponential x y x = 0 y = 1 ∃ (x' : V) (y' : V), x = x' + 1 y = 2 * y' LO.Arith.Exponential x' y'
                            theorem LO.Arith.Exponential.monotone {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x₁ : V} {x₂ : V} {y₁ : V} {y₂ : V} :
                            LO.Arith.Exponential x₁ y₁LO.Arith.Exponential x₂ y₂x₁ < x₂y₁ < y₂
                            theorem LO.Arith.Exponential.monotone_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x₁ : V} {x₂ : V} {y₁ : V} {y₂ : V} (h₁ : LO.Arith.Exponential x₁ y₁) (h₂ : LO.Arith.Exponential x₂ y₂) :
                            x₁ x₂y₁ y₂
                            theorem LO.Arith.Exponential.monotone_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x₁ : V} {x₂ : V} {y₁ : V} {y₂ : V} (h₁ : LO.Arith.Exponential x₁ y₁) (h₂ : LO.Arith.Exponential x₂ y₂) :
                            x₁ < x₂ y₁ < y₂
                            theorem LO.Arith.Exponential.monotone_le_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x₁ : V} {x₂ : V} {y₁ : V} {y₂ : V} (h₁ : LO.Arith.Exponential x₁ y₁) (h₂ : LO.Arith.Exponential x₂ y₂) :
                            x₁ x₂ y₁ y₂
                            theorem LO.Arith.Exponential.add_mul {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x₁ : V} {x₂ : V} {y₁ : V} {y₂ : V} (h₁ : LO.Arith.Exponential x₁ y₁) (h₂ : LO.Arith.Exponential x₂ y₂) :
                            LO.Arith.Exponential (x₁ + x₂) (y₁ * y₂)
                            Equations
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              theorem LO.Arith.exp_of_exponential {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} (h : LO.Arith.Exponential a b) :
                              exp a = b
                              @[simp]
                              @[simp]
                              theorem LO.Arith.exp_one {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
                              exp 1 = 2
                              theorem LO.Arith.exp_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) :
                              exp (a + 1) = 2 * exp a
                              theorem LO.Arith.exp_even {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) :
                              exp (2 * a) = exp a ^ 2
                              @[simp]
                              theorem LO.Arith.lt_exp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) :
                              a < exp a
                              @[simp]
                              theorem LO.Arith.exp_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) :
                              0 < exp a
                              @[simp]
                              theorem LO.Arith.one_le_exp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) :
                              1 exp a
                              @[simp]
                              @[simp]
                              theorem LO.Arith.exp_monotone {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} :
                              exp a < exp b a < b
                              @[simp]
                              theorem LO.Arith.exp_monotone_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} :
                              exp a exp b a b
                              theorem LO.Arith.nat_cast_exp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : ) :
                              (exp n) = exp n