exp_ge_linear

formal source

  18/-! ## §1 Bernoulli and base results -/
  19
  20/-- Bernoulli's inequality: for a ≥ 1, a^n ≥ 1 + n*(a-1). -/
  21theorem exp_ge_linear (a : ℝ) (ha : 1 ≤ a) (n : ℕ) :
  22    a ^ n ≥ 1 + (n : ℝ) * (a - 1) := by
  23  induction n with
  24  | zero => simp
  25  | succ k ih =>
  26    have ha_nonneg : 0 ≤ a := by linarith
  27    have hk_nn : (0 : ℝ) ≤ k := Nat.cast_nonneg k
  28    calc a ^ (k + 1) = a ^ k * a := pow_succ a k
  29      _ ≥ (1 + (k : ℝ) * (a - 1)) * a := by
  30          exact mul_le_mul_of_nonneg_right ih ha_nonneg
  31      _ = a + (k : ℝ) * a * (a - 1) := by ring
  32      _ ≥ a + (k : ℝ) * 1 * (a - 1) := by
  33          nlinarith [mul_nonneg hk_nn (sub_nonneg.mpr ha), sq_nonneg (a - 1)]
  34      _ = 1 + ((k : ℝ) + 1) * (a - 1) := by ring
  35      _ = 1 + (↑(k + 1) : ℝ) * (a - 1) := by push_cast; ring
  36
  37/-- For a > 1 and any M, there exists N such that a^N > M. -/
  38theorem exponential_exceeds_bound (a : ℝ) (ha : 1 < a) (M : ℝ) :
  39    ∃ N : ℕ, a ^ N > M := by
  40  have ha_sub : 0 < a - 1 := by linarith
  41  obtain ⟨N, hN⟩ := exists_nat_gt ((M - 1) / (a - 1))
  42  refine ⟨N, ?_⟩
  43  have hge := exp_ge_linear a (le_of_lt ha) N
  44  have hN_bound : (N : ℝ) * (a - 1) > M - 1 := by
  45    have := (div_lt_iff₀ ha_sub).mp hN
  46    linarith
  47  linarith
  48
  49/-- φ eventually exceeds any bound. -/
  50theorem phi_pow_exceeds (M : ℝ) : ∃ N : ℕ, phi ^ N > M :=
  51  exponential_exceeds_bound phi one_lt_phi M