Documentation

LeanUnits.Framework.Dimensions.PrimeScale

source
def Units.Dimension.PrimeScale.string_to_nat (s : String) :
ℕ

Encode a string to ℕ Making sure the encoding is injective.

Equations
Instances For
    source
    @[irreducible]
    def Units.Dimension.PrimeScale.digits (n : ℕ) :
    List ℕ

    Helper function to get the digits of a natural number in base 2^32.

    Equations
    Instances For
      source
      theorem Units.Dimension.PrimeScale.string_to_nat_inj :
      Function.Injective string_to_nat
      source
      def Units.Dimension.PrimeScale.next_prime (n : ℕ) :
      Nat.Primes

      Get the next Nat.Primes after n.

      Equations
      Instances For
        source
        theorem Units.Dimension.PrimeScale.next_prime_gt (n : ℕ) :
        n ≤ ↑(next_prime n)
        source
        def Units.Dimension.PrimeScale.nth_prime (n : ℕ) :
        Nat.Primes

        Get the n-th Nat.Primes (0-indexed). For example, nth_prime 0 = 2, nth_prime 1 = 3, nth_prime 2 = 5, etc.

        Equations
        Instances For
          source
          def Units.Dimension.PrimeScale.nth_prime.go :
          Nat.Primes → ℕ → Nat.Primes
          Equations
          Instances For
            source
            def Units.Dimension.PrimeScale.nth_prime_nat (n : ℕ) :
            ℕ

            Get the n-th Nat prime number (0-indexed). For example, nth_prime 0 = 2, nth_prime 1 = 3, nth_prime 2 = 5, etc.

            Equations
            Instances For
              source
              theorem Units.Dimension.PrimeScale.nth_prime_nat_prime (n : ℕ) :
              Nat.Prime (nth_prime_nat n)
              source
              theorem Units.Dimension.PrimeScale.nth_prime_strictmono :
              StrictMono nth_prime_nat
              source
              theorem Units.Dimension.PrimeScale.nth_prime_nat_inj :
              Function.Injective nth_prime_nat
              source
              def Units.Dimension.PrimeScale.prime_from_str (s : String) :
              ℕ

              Get the prime number associated to a string. This allows us to assign a unique prime number to each base dimension represented by a string. We use it to construct the PrimeScale of a dimension.

              Equations
              Instances For
                source
                theorem Units.Dimension.PrimeScale.prime_from_str_prime (s : String) :
                Nat.Prime (prime_from_str s)
                source
                theorem Units.Dimension.PrimeScale.prime_from_str_inj :
                Function.Injective prime_from_str
                source
                theorem Units.Dimension.PrimeScale.prime_from_str_ne_zero (s : String) :
                prime_from_str s ≠ 0
                source
                theorem Units.Dimension.PrimeScale.prime_from_str_pos (s : String) :
                0 < prime_from_str s
                source
                theorem Units.Dimension.PrimeScale.one_le_prime_from_str (s : String) :
                1 ≤ prime_from_str s
                source
                noncomputable def Units.Dimension.PrimeScale.prime_pow (s : String) (q : ℚ) :
                ℝ

                Compute the prime expnentiation for a given string and rational number. It's used to compute the PrimeScale of a dimension.

                Equations
                Instances For
                  source
                  theorem Units.Dimension.PrimeScale.prime_pow_inj_left (s1 s2 : String) (q : ℚ) (h : q ≠ 0) :
                  prime_pow s1 q = prime_pow s2 q ↔ s1 = s2

                  prime_pow injective if q≠0

                  source
                  theorem Units.Dimension.PrimeScale.prime_pow_inj_right (s : String) (q1 q2 : ℚ) :
                  prime_pow s q1 = prime_pow s q2 ↔ q1 = q2

                  For a fixed base (prime_from_str s : ℝ) > 1, the map q ↦ prime_pow s q is injective on ℚ.

                  source
                  theorem Units.Dimension.PrimeScale.prime_pow_inj_nat (s1 s2 : String) {n1 n2 : ℕ} (h1 : n1 ≠ 0) (h2 : n2 ≠ 0) :
                  prime_pow s1 ↑n1 = prime_pow s2 ↑n2 ↔ s1 = s2 ∧ n1 = n2
                  source
                  theorem Units.Dimension.PrimeScale.prime_pow_inj_int (s1 s2 : String) {z1 z2 : ℤ} (h1 : z1 ≠ 0) (h2 : z2 ≠ 0) :
                  prime_pow s1 ↑z1 = prime_pow s2 ↑z2 ↔ s1 = s2 ∧ z1 = z2
                  source
                  theorem Units.Dimension.PrimeScale.prime_pow_inj (s1 s2 : String) {q1 q2 : ℚ} (h1 : q1 ≠ 0) (h2 : q2 ≠ 0) :
                  prime_pow s1 q1 = prime_pow s2 q2 ↔ s1 = s2 ∧ q1 = q2
                  source
                  theorem Units.Dimension.PrimeScale.prime_pow_zero {s : String} :
                  prime_pow s 0 = 1
                  source
                  theorem Units.Dimension.PrimeScale.prime_pow_add {s : String} (q1 q2 : ℚ) :
                  prime_pow s (q1 + q2) = prime_pow s q1 * prime_pow s q2
                  source
                  theorem Units.Dimension.PrimeScale.prime_pow_neg {i : String} (q : ℚ) :
                  prime_pow i (-q) = (prime_pow i q)⁻¹
                  source
                  theorem Units.Dimension.PrimeScale.prime_pow_ne_zero {s : String} (q : ℚ) :
                  prime_pow s q ≠ 0
                  source
                  theorem Units.Dimension.PrimeScale.one_le_prime_pow {s : String} {q : ℚ} (hq : 0 ≤ q) :
                  1 ≤ prime_pow s q
                  source
                  theorem Units.Dimension.PrimeScale.prime_pow_le_one {s : String} {q : ℚ} (hq : q ≤ 0) :
                  prime_pow s q ≤ 1
                  source
                  theorem Units.Dimension.PrimeScale.prime_pow_pos {s : String} {q : ℚ} :
                  0 < prime_pow s q
                  source
                  theorem Units.Dimension.PrimeScale.prime_pow_eq_one {s : String} {q : ℚ} (hq : q = 0) :
                  prime_pow s q = 1
                  source
                  theorem Units.Dimension.PrimeScale.prime_pow_ne_one {s : String} {q : ℚ} (hq : q ≠ 0) :
                  prime_pow s q ≠ 1
                  source
                  theorem Units.Dimension.PrimeScale.prime_pow_eq_one_iff {s : String} {q : ℚ} :
                  prime_pow s q = 1 ↔ q = 0
                  source
                  theorem Units.Dimension.PrimeScale.prime_pow_mul_prime_pow_eq_one_iff {s1 s2 : String} {q1 q2 : ℚ} :
                  prime_pow s1 q1 * prime_pow s2 q2 = 1 ↔ s1 = s2 ∧ q1 = -q2 ∨ q1 = 0 ∧ q2 = 0
                  source
                  theorem Units.Dimension.PrimeScale.diff_prime_pow_mul_prime_pow_eq_one_iff {s1 s2 : String} {q1 q2 : ℚ} (h : s1 ≠ s2) :
                  prime_pow s1 q1 * prime_pow s2 q2 = 1 ↔ q1 = 0 ∧ q2 = 0
                  source
                  theorem Units.Dimension.PrimeScale.prod_prime_pow_eq_one_iff (S : Finset String) (q : String → ℚ) :
                  ∏ s ∈ S, prime_pow s (q s) = 1 ↔ ∀ s ∈ S, q s = 0