totient

Stream: new members

[vxctyxeha]

Hello, I try to prove the following, but proving its lower bound seems a bit difficult. For the first one, I can complete it using an infinite number of prime numbers, but the second one seems a bit challenging.

import Mathlib
open Nat Filter
theorem totient_unbounded : ∀ M : ℕ, ∃ n : ℕ, φ n ≥ M := by sorry
theorem totient_tendsto_top : Filter.Tendsto (fun n => φ n) atTop atTop := by
  apply Filter.tendsto_atTop_atTop.mpr
  intro N
  have h4 : ∃ m, ∀ n, n ≥ m → φ n ≥ N := by
     sorry
  exact h4

[Weiyi Wang]

Do you have a pen-and-paper proof ready, or you are exploring it in Lean?

[Weiyi Wang]

If you don't have a pen-and-paper proof yet, I recommend doing that first without Lean. I don't know if you are challenging yourself to come up with a proof alone (and if so, how much hint do we give?) or you are allowed to look up proof from other materials freely. If it is the latter, it is not hard to find one online, and the wikipedia page also has some hints

[vxctyxeha]

sorry，i will check in wiki