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 MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.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

Multiplicativity and positivity determine the value at one.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.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

A positive multiplicative function preserves natural powers.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.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

Monotonicity transfers comparisons of natural powers to the values.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.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)

The same comparison after taking logarithms.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.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

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.eq_of_nat_mul_sub_bounded {x y C : ℝ} (hxy : ∀ (k : ℕ), ↑k * (x - y) ≤ C) (hyx : ∀ (k : ℕ), ↑k * (y - x) ≤ C) : x = y

If every natural multiple of both differences has a common upper bound, the two real numbers coincide.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.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)

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.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)

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.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

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