IndisputableMonolith.Cost.MonotoneMultiplicativePower

   1/-
   2  Cost/MonotoneMultiplicativePower.lean
   3
   4  ERDOS'S THEOREM ON MONOTONE MULTIPLICATIVE FUNCTIONS, IN THE CASE THE COST
   5  CLASSIFICATION NEEDS, WITH NOTHING IMPORTED.
   6
   7  Statement. A completely multiplicative `f : ℕ → ℝ` that is nondecreasing on the
   8  positive integers is `n ↦ n ^ c` for a single real `c ≥ 0` (`exists_exponent`).
   9
  10  Provenance. This is the completely multiplicative case of Erdős 1946, whose short
  11  proof is due to Howe (Amer. Math. Monthly 93 (1986) 593-595). The argument below is
  12  Howe's: squeeze `n ^ k` between consecutive powers of two, apply monotonicity on both
  13  the argument and the value, and let `k` grow. It is elementary and needs no
  14  transcendence input, which is why it can be discharged here rather than named as a
  15  hypothesis. The classification of the anchor-free cost ledger previously carried it as
  16  one of TWO external imports; after this module the only remaining import is the six
  17  exponentials theorem (`Cost.TraceRationalExponent.SixExponentialsTraceInput`).
  18
  19  Why the exponent is real and not rational. Monotonicity alone cannot produce a rational
  20  exponent, and it does not need to: the arithmetic that forces an integer runs later, on
  21  the traces, in `Cost.TraceRationalExponent`.
  22
  23  No project-local axioms. No sorry.
  24-/
  25
  26import Mathlib
  27
  28namespace IndisputableMonolith
  29namespace Cost
  30namespace MonotonePower
  31
  32/-- A completely multiplicative, nondecreasing function on the positive integers. The
  33conditions are stated only where they are meant, above zero: `f 0` is unconstrained, since
  34the character the cost ledger produces has no content there. -/
  35structure MonotoneMultiplicative (f : ℕ → ℝ) : Prop where
  36  unit : f 1 = 1
  37  mul : ∀ m n : ℕ, 1 ≤ m → 1 ≤ n → f (m * n) = f m * f n
  38  mono : ∀ m n : ℕ, 1 ≤ m → m ≤ n → f m ≤ f n
  39
  40variable {f : ℕ → ℝ}
  41
  42theorem one_le (hf : MonotoneMultiplicative f) {n : ℕ} (hn : 1 ≤ n) : 1 ≤ f n := by
  43  have h := hf.mono 1 n le_rfl hn
  44  rwa [hf.unit] at h
  45
  46theorem pos (hf : MonotoneMultiplicative f) {n : ℕ} (hn : 1 ≤ n) : 0 < f n :=
  47  lt_of_lt_of_le zero_lt_one (one_le hf hn)
  48
  49/-- Complete multiplicativity on powers, which is the only form the squeeze uses. -/
  50theorem pow_eq (hf : MonotoneMultiplicative f) {m : ℕ} (hm : 1 ≤ m) (j : ℕ) :
  51    f (m ^ j) = f m ^ j := by
  52  induction j with
  53  | zero => simpa using hf.unit
  54  | succ j ih =>
  55      have hmj : 1 ≤ m ^ j := Nat.one_le_pow j m hm
  56      rw [pow_succ, hf.mul _ _ hmj hm, ih, pow_succ]
  57
  58/-- The degenerate branch. If the value at two is one then every value is one, because
  59every integer is below a power of two and the values in between are squeezed. -/
  60theorem eq_one_of_two_eq_one (hf : MonotoneMultiplicative f) (h2 : f 2 = 1)
  61    {n : ℕ} (hn : 1 ≤ n) : f n = 1 := by
  62  have hlt : n < 2 ^ n := Nat.lt_two_pow_self
  63  have hle := hf.mono n (2 ^ n) hn hlt.le
  64  rw [pow_eq hf (by norm_num) n, h2, one_pow] at hle
  65  exact le_antisymm hle (one_le hf hn)
  66
  67/-- **The heart of Howe's argument.** For every base `n ≥ 2` the ratio
  68`log (f n) / log n` is the same as at the base two, stated cross-multiplied so that no
  69division appears. The proof squeezes `n ^ k` between `2 ^ j` and `2 ^ (j+1)`, reads the
  70squeeze twice (on the argument and on the value), and lets `k` grow. -/
  71theorem log_ratio (hf : MonotoneMultiplicative f) (h2 : 1 < f 2) {n : ℕ} (hn : 2 ≤ n) :
  72    Real.log (f n) * Real.log 2 = Real.log (f 2) * Real.log n := by
  73  set L2 := Real.log 2 with hL2def
  74  set Ln := Real.log n with hLndef
  75  set M2 := Real.log (f 2) with hM2def
  76  set Mn := Real.log (f n) with hMndef
  77  have hnR : (1 : ℝ) < (n : ℝ) := by exact_mod_cast lt_of_lt_of_le one_lt_two hn
  78  have hL2 : 0 < L2 := Real.log_pos (by norm_num)
  79  have hLn : 0 < Ln := Real.log_pos hnR
  80  have hM2 : 0 < M2 := Real.log_pos h2
  81  have hfn : 1 < f n := lt_of_lt_of_le h2 (hf.mono 2 n (by norm_num) hn)
  82  have hMn : 0 < Mn := Real.log_pos hfn
  83  have hn1 : 1 ≤ n := le_trans (by norm_num) hn
  84  have key : ∀ k : ℕ, 1 ≤ k → (k : ℝ) * |Mn * L2 - M2 * Ln| ≤ M2 * L2 := by
  85    intro k hk
  86    set j := Nat.log 2 (n ^ k) with hjdef
  87    have hnkpos : 1 ≤ n ^ k := Nat.one_le_pow k n (by omega)
  88    have hnk0 : n ^ k ≠ 0 := by omega
  89    have hle : 2 ^ j ≤ n ^ k := Nat.pow_log_le_self 2 hnk0
  90    have hlt : n ^ k < 2 ^ (j + 1) := Nat.lt_pow_succ_log_self (by norm_num) _
  91    have hleR : ((2 : ℝ)) ^ j ≤ ((n : ℝ)) ^ k := by exact_mod_cast hle
  92    have hltR : ((n : ℝ)) ^ k ≤ ((2 : ℝ)) ^ (j + 1) := by exact_mod_cast hlt.le
  93    have ha : (j : ℝ) * L2 ≤ (k : ℝ) * Ln := by
  94      have h := Real.log_le_log (by positivity) hleR
  95      rwa [Real.log_pow, Real.log_pow] at h
  96    have hb : (k : ℝ) * Ln ≤ ((j : ℝ) + 1) * L2 := by
  97      have h := Real.log_le_log (by positivity) hltR
  98      rw [Real.log_pow, Real.log_pow] at h
  99      push_cast at h
 100      linarith
 101    have hf2j : 1 ≤ 2 ^ j := Nat.one_le_pow j 2 (by norm_num)
 102    have hf2j1 : 1 ≤ 2 ^ (j + 1) := Nat.one_le_pow (j + 1) 2 (by norm_num)
 103    have hfa : f (2 ^ j) ≤ f (n ^ k) := hf.mono _ _ hf2j hle
 104    have hfb : f (n ^ k) ≤ f (2 ^ (j + 1)) := hf.mono _ _ (Nat.one_le_pow k n (by omega)) hlt.le
 105    rw [pow_eq hf (by norm_num) j, pow_eq hf hn1 k] at hfa
 106    rw [pow_eq hf hn1 k, pow_eq hf (by norm_num) (j + 1)] at hfb
 107    have hf2pos : (0 : ℝ) < f 2 := lt_trans zero_lt_one h2
 108    have hfnpos : (0 : ℝ) < f n := lt_trans zero_lt_one hfn
 109    have hc : (j : ℝ) * M2 ≤ (k : ℝ) * Mn := by
 110      have h := Real.log_le_log (by positivity) hfa
 111      rwa [Real.log_pow, Real.log_pow] at h
 112    have hd : (k : ℝ) * Mn ≤ ((j : ℝ) + 1) * M2 := by
 113      have h := Real.log_le_log (by positivity) hfb
 114      rw [Real.log_pow, Real.log_pow] at h
 115      push_cast at h
 116      linarith
 117    have e1 : ((k : ℝ) * Mn) * L2 ≤ (((j : ℝ) + 1) * M2) * L2 :=
 118      mul_le_mul_of_nonneg_right hd hL2.le
 119    have e2 : ((j : ℝ) * L2) * M2 ≤ ((k : ℝ) * Ln) * M2 :=
 120      mul_le_mul_of_nonneg_right ha hM2.le
 121    have e3 : ((j : ℝ) * M2) * L2 ≤ ((k : ℝ) * Mn) * L2 :=
 122      mul_le_mul_of_nonneg_right hc hL2.le
 123    have e4 : ((k : ℝ) * Ln) * M2 ≤ (((j : ℝ) + 1) * L2) * M2 :=
 124      mul_le_mul_of_nonneg_right hb hM2.le
 125    have habs : |(k : ℝ) * (Mn * L2 - M2 * Ln)| ≤ M2 * L2 := by
 126      rw [abs_le]
 127      constructor
 128      · nlinarith [e3, e4]
 129      · nlinarith [e1, e2]
 130    calc (k : ℝ) * |Mn * L2 - M2 * Ln|
 131        = |(k : ℝ) * (Mn * L2 - M2 * Ln)| := by
 132          rw [abs_mul, Nat.abs_cast]
 133      _ ≤ M2 * L2 := habs
 134  by_contra hne
 135  have hD : 0 < |Mn * L2 - M2 * Ln| := abs_pos.mpr (sub_ne_zero_of_ne hne)
 136  obtain ⟨k, hk⟩ := exists_nat_gt ((M2 * L2) / |Mn * L2 - M2 * Ln|)
 137  have hbig : M2 * L2 < (k : ℝ) * |Mn * L2 - M2 * Ln| := (div_lt_iff₀ hD).mp hk
 138  have hsmall := key (k + 1) (Nat.le_add_left 1 k)
 139  push_cast at hsmall
 140  nlinarith [hD, hbig, hsmall]
 141
 142/-- **Erdős's theorem, completely multiplicative case (Howe's proof).** A nondecreasing
 143completely multiplicative function on the positive integers is a power, with a single
 144nonnegative real exponent. The degenerate constant function is the exponent zero. -/
 145theorem exists_exponent (hf : MonotoneMultiplicative f) :
 146    ∃ c : ℝ, 0 ≤ c ∧ ∀ n : ℕ, 1 ≤ n → f n = (n : ℝ) ^ c := by
 147  rcases eq_or_lt_of_le (one_le hf (by norm_num : (1 : ℕ) ≤ 2)) with h2 | h2
 148  · refine ⟨0, le_rfl, fun n hn => ?_⟩
 149    rw [Real.rpow_zero, eq_one_of_two_eq_one hf h2.symm hn]
 150  · have hL2 : 0 < Real.log 2 := Real.log_pos (by norm_num)
 151    have hM2 : 0 < Real.log (f 2) := Real.log_pos h2
 152    refine ⟨Real.log (f 2) / Real.log 2, le_of_lt (div_pos hM2 hL2), fun n hn => ?_⟩
 153    rcases eq_or_lt_of_le hn with h1 | h1
 154    · have hn1 : n = 1 := h1.symm
 155      subst hn1
 156      rw [hf.unit, Nat.cast_one, Real.one_rpow]
 157    · have hn2 : 2 ≤ n := h1
 158      have hlog := log_ratio hf h2 hn2
 159      have hnpos : (0 : ℝ) < (n : ℝ) := by
 160        exact_mod_cast lt_of_lt_of_le Nat.zero_lt_one hn
 161      have hfpos : 0 < f n := pos hf hn
 162      rw [Real.rpow_def_of_pos hnpos, ← Real.exp_log hfpos]
 163      congr 1
 164      field_simp
 165      linarith [hlog]
 166
 167/-! ### Nonvacuity
 168
 169A theorem about an empty hypothesis class proves nothing. The pack is inhabited at both
 170ends of the conclusion: the constant function realizes the exponent zero and the identity
 171realizes the exponent one. Monotonicity is what is doing the work, and it cannot be
 172dropped: the Liouville function is completely multiplicative and is no power. -/
 173
 174theorem monotoneMultiplicative_const_one : MonotoneMultiplicative (fun _ : ℕ => (1 : ℝ)) where
 175  unit := rfl
 176  mul := by intro m n _ _; norm_num
 177  mono := by intro m n _ _; exact le_rfl
 178
 179theorem monotoneMultiplicative_id : MonotoneMultiplicative (fun n : ℕ => (n : ℝ)) where
 180  unit := by norm_num
 181  mul := by intro m n _ _; push_cast; ring
 182  mono := by intro m n _ hmn; exact_mod_cast hmn
 183
 184/-! ### Axiom audit -/
 185
 186#print axioms exists_exponent
 187#print axioms log_ratio
 188
 189end MonotonePower
 190end Cost
 191end IndisputableMonolith
 192