MultiplicativePower.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Monotone multiplicative functions on the positive natural numbers

The scalar classification used in Section 3.1: positivity, multiplicativity, and monotonicity force a function on positive natural numbers to be a real power. No property of the function at zero is required.

theorem OAI.MatrixMultiplication.AuxiliarySeparation.positiveMultiplicative_one line 18

Source documentation

Multiplicativity and positivity determine the value at one.

theorem positiveMultiplicative_one
    {f : ℕ → ℝ} (hpos : ∀ n, 0 < n → 0 < f n)
    (hmul : ∀ m n, 0 < m → 0 < n → f (m * n) = f m * f n) :
    f 1 = 1 := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.positiveMultiplicative_pow line 28

Source documentation

A positive multiplicative function preserves natural powers.

theorem positiveMultiplicative_pow
    {f : ℕ → ℝ} (hpos : ∀ n, 0 < n → 0 < f n)
    (hmul : ∀ m n, 0 < m → 0 < n → f (m * n) = f m * f n)
    {n : ℕ} (hn : 0 < n) (k : ℕ) : f (n ^ k) = f n ^ k := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.positiveMultiplicative_pow_le_pow line 38

Source documentation

Monotonicity transfers comparisons of natural powers to the values.

theorem positiveMultiplicative_pow_le_pow
    {f : ℕ → ℝ} (hpos : ∀ n, 0 < n → 0 < f n)
    (hmul : ∀ m n, 0 < m → 0 < n → f (m * n) = f m * f n)
    (hmono : MonotoneOn f (Set.Ioi 0))
    {m n : ℕ} (hm : 0 < m) (hn : 0 < n) {j k : ℕ}
    (h : m ^ j ≤ n ^ k) : f m ^ j ≤ f n ^ k := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.positiveMultiplicative_log_pow_le line 49

Source documentation

The same comparison after taking logarithms.

theorem positiveMultiplicative_log_pow_le
    {f : ℕ → ℝ} (hpos : ∀ n, 0 < n → 0 < f n)
    (hmul : ∀ m n, 0 < m → 0 < n → f (m * n) = f m * f n)
    (hmono : MonotoneOn f (Set.Ioi 0))
    {m n : ℕ} (hm : 0 < m) (hn : 0 < n) {j k : ℕ}
    (h : m ^ j ≤ n ^ k) :
    (j : ℝ) * Real.log (f m) ≤ (k : ℝ) * Real.log (f n) := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.positiveMultiplicative_log_error_bounds line 62

Source documentation

Bounds from neighboring powers of two have a fixed logarithmic error, independent of the exponent k.

theorem positiveMultiplicative_log_error_bounds
    {f : ℕ → ℝ} (hpos : ∀ n, 0 < n → 0 < f n)
    (hmul : ∀ m n, 0 < m → 0 < n → f (m * n) = f m * f n)
    (hmono : MonotoneOn f (Set.Ioi 0))
    {n : ℕ} (hn : 0 < n) (k : ℕ) :
    (k : ℝ) * (Real.log (f n) * Real.log 2 -
      Real.log (n : ℝ) * Real.log (f 2)) ≤ Real.log (f 2) * Real.log 2 ∧
    (k : ℝ) * (Real.log (n : ℝ) * Real.log (f 2) -
      Real.log (f n) * Real.log 2) ≤ Real.log (f 2) * Real.log 2 := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.eq_of_nat_mul_sub_bounded line 98
Source documentation
If every natural multiple of both differences has a common upper bound, the two real numbers coincide.
```
theorem eq_of_nat_mul_sub_bounded {x y C : ℝ}
    (hxy : ∀ k : ℕ, (k : ℝ) * (x - y) ≤ C)
    (hyx : ∀ k : ℕ, (k : ℝ) * (y - x) ≤ C) : x = y := by
…
```

theorem OAI.MatrixMultiplication.AuxiliarySeparation.positiveMultiplicative_log_eq line 114

Source documentation

The logarithmic exponent is the same at every positive natural number.

theorem positiveMultiplicative_log_eq
    {f : ℕ → ℝ} (hpos : ∀ n, 0 < n → 0 < f n)
    (hmul : ∀ m n, 0 < m → 0 < n → f (m * n) = f m * f n)
    (hmono : MonotoneOn f (Set.Ioi 0))
    {n : ℕ} (hn : 0 < n) :
    Real.log (f n) = Real.log (n : ℝ) * (Real.log (f 2) / Real.log 2) := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.positiveMultiplicative_eq_rpow line 132

Source documentation

The explicit exponent in the classification of positive monotone multiplicative functions on the positive natural numbers.

theorem positiveMultiplicative_eq_rpow
    {f : ℕ → ℝ} (hpos : ∀ n, 0 < n → 0 < f n)
    (hmul : ∀ m n, 0 < m → 0 < n → f (m * n) = f m * f n)
    (hmono : MonotoneOn f (Set.Ioi 0))
    {n : ℕ} (hn : 0 < n) :
    f n = (n : ℝ) ^ (Real.log (f 2) / Real.log 2) := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.positiveMultiplicative_is_rpow line 144

Source documentation

Every positive monotone multiplicative function on the positive natural numbers is a nonnegative real power, as used in Section 3.1.

theorem positiveMultiplicative_is_rpow
    {f : ℕ → ℝ} (hpos : ∀ n, 0 < n → 0 < f n)
    (hmul : ∀ m n, 0 < m → 0 < n → f (m * n) = f m * f n)
    (hmono : MonotoneOn f (Set.Ioi 0)) :
    ∃ p : ℝ, 0 ≤ p ∧ ∀ n : ℕ, 0 < n → f n = (n : ℝ) ^ p := by
…