Mathlib.Order.Filter.AtTopBot.ModEq

Nat.frequently_modEq theorem

{n : ℕ} (h : n ≠ 0) (d : ℕ) : ∃ᶠ m in atTop, m ≡ d [MOD n]

Full source

/-- Infinitely many natural numbers are equal to `d` mod `n`. -/
theorem frequently_modEq {n : ℕ} (h : n ≠ 0) (d : ℕ) : ∃ᶠ m in atTop, m ≡ d [MOD n] :=
  ((tendsto_add_atTop_nat d).comp (tendsto_id.nsmul_atTop h.bot_lt)).frequently <|
    Frequently.of_forall fun m => by simp [Nat.modEq_iff_dvd, ← sub_sub]

Infinitely Many Natural Numbers Congruent to $d$ Modulo $n$

Informal description

For any natural numbers $n$ and $d$ with $n \neq 0$, there exist infinitely many natural numbers $m$ such that $m \equiv d \pmod{n}$.

Nat.frequently_mod_eq theorem

{d n : ℕ} (h : d < n) : ∃ᶠ m in atTop, m % n = d

Full source

theorem frequently_mod_eq {d n : ℕ} (h : d < n) : ∃ᶠ m in atTop, m % n = d := by
  simpa only [Nat.ModEq, mod_eq_of_lt h] using frequently_modEq h.ne_bot d

Infinitely many natural numbers congruent to $d$ modulo $n$ (remainder form)

Informal description

For any natural numbers $d$ and $n$ with $d < n$, there exist infinitely many natural numbers $m$ such that $m \bmod n = d$.

Nat.frequently_even theorem

: ∃ᶠ m : ℕ in atTop, Even m

Full source

theorem frequently_even : ∃ᶠ m : ℕ in atTop, Even m := by
  simpa only [even_iff] using frequently_mod_eq zero_lt_two

Infinitely Many Even Natural Numbers

Informal description

There exist infinitely many natural numbers $m$ such that $m$ is even, i.e., $m \equiv 0 \pmod{2}$.

Nat.frequently_odd theorem

: ∃ᶠ m : ℕ in atTop, Odd m

Full source

theorem frequently_odd : ∃ᶠ m : ℕ in atTop, Odd m := by
  simpa only [odd_iff] using frequently_mod_eq one_lt_two

Infinitely Many Odd Natural Numbers

Informal description

There exist infinitely many natural numbers $m$ such that $m$ is odd.

Filter.nonneg_of_eventually_pow_nonneg theorem

 {α : Type*} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (h : ∀ᶠ n in atTop, 0 ≤ a ^ (n : ℕ)) : 0 ≤ a

Full source

theorem Filter.nonneg_of_eventually_pow_nonneg {α : Type*}
    [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a : α}
    (h : ∀ᶠ n in atTop, 0 ≤ a ^ (n : ℕ)) : 0 ≤ a :=
  let ⟨_n, ho, hn⟩ := (Nat.frequently_odd.and_eventually h).exists
  ho.pow_nonneg_iff.1 hn

Nonnegativity from Eventually Nonnegative Powers in Ordered Rings

Informal description

Let $\alpha$ be a linearly ordered ring that is strictly ordered. For any element $a \in \alpha$, if there exists a filter condition such that for all sufficiently large natural numbers $n$, the $n$-th power $a^n$ is nonnegative, then $a$ itself is nonnegative, i.e., $0 \leq a$.