Trying to prove that 1/n is cauchy

Stream: new members

[metakuntyyy]

Hey guys, I am dabbling a bit into trying to prove some statements about the real numbers. I wanted to practice a bit.
Here is my current attempt. Am I on the correct path?

import Mathlib

example (f: ℕ → ℚ ) (h: f n = 1/n) : IsCauSeq abs f := by
  intro ε
  intro he
  use 3*(1/ε).ceil.natAbs
  intro m
  intro ha
  have hah := abs_sub (f m) (f (3 * (1 / ε).ceil.natAbs))
  suffices har : |f m| + |f (3 * (1 / ε).ceil.natAbs)| < ε from sorry
  have h1: |f m| < ε /3 := by sorry
  have h2: |f (3 * (1 / ε).ceil.natAbs)| < ε /3 := by sorry
  linarith

[Yakov Pechersky]

I think that you should make sure that autoimplicits are turned off. You're missing a "forall n" in your h hypothesis.

[metakuntyyy]

Alright, is that correct?
If so, can I fill the sorries or am I on the wrong path?

import Mathlib
set_option autoImplicit false

example (f: ℕ → ℚ ) (h: ∀ n:ℕ, f n = 1/n) : IsCauSeq abs f := by
  intro ε
  intro he
  use 3*(1/ε).ceil.natAbs
  intro m
  intro ha
  have hah := abs_sub (f m) (f (3 * (1 / ε).ceil.natAbs))
  suffices har : |f m| + |f (3 * (1 / ε).ceil.natAbs)| < ε from sorry
  have h1: |f m| < ε /3 := by sorry
  have h2: |f (3 * (1 / ε).ceil.natAbs)| < ε /3 := by sorry
  linarith

[Kevin Buzzard]

The first one is lt_of_le_of_lt hah har, the other two are messier because you didn't deal with m=0 separately.

[Kevin Buzzard]

In fact I think they might be false if 3/eps is an integer.

[Kevin Buzzard]

Here's a slight modification of your strategy. I use a ceil for which there is actually some API, and replace some < by <=.

import Mathlib
set_option autoImplicit false

example (f: ℕ → ℚ ) (h: ∀ n:ℕ, f n = 1/n) : IsCauSeq abs f := by
  intro ε hε
  use ⌈3 / ε⌉₊ -- avoid lean/batteries Rat.ceil, I can't find any API for it, use mathlib's
  have foo : 0 < 3 / ε := by exact div_pos rfl hε
  intro m ha
  have hm : 0 < m := by
    by_contra hm
    obtain rfl := Nat.eq_zero_of_not_pos hm
    simp at ha
    linarith
  have hah := abs_sub (f m) (f (⌈3 / ε⌉₊))
  suffices har : |f m| + |f (⌈3 / ε⌉₊)| < ε from lt_of_le_of_lt hah har
  have h1: |f m| ≤ ε / 3 := by
    rw [h, abs_of_nonneg (by simp), one_div_le (by assumption_mod_cast) (div_pos hε rfl), one_div_div]
    rwa [ge_iff_le, Nat.ceil_le] at ha
  have h2: |f ⌈3 / ε⌉₊| ≤ ε / 3 := by
    rw [h, abs_of_nonneg (by simp), one_div_le (by simp [hε]) (div_pos hε rfl), one_div_div]
    exact Nat.le_ceil (3 / ε)
  linarith

[metakuntyyy]

I see, thanks, I actually chose epsilon/3 instead of epsilon/2 because I wanted to have a bit of space in between them. My initial hunch that it might be problematic turned out to be right. Overall it seems to me sometimes that 0 being a Nat is sometimes a pain to consider.
I was also thinking about having to prove that m is positive as my reasoning was more of trying to show that the function f is monotone falling on the positive rationals and I can't lift it from Nat because the 0 makes problems, since in mathlib 1/0=0.

Overall I thought about how to "generate" a natural number from a rational number. I thought the canonical way would be to use a ceiling, which produces an integer and then cast it to a natural number. The cast should preserve substitution as the integer to be casted is non-negative. Moreover it is a positive Nat since the rational itself is positive and casting will give me 0 < x, where x is the transformation Rat -> Int -> Nat.
Is that actually how idiomatic lean is. If you need to create an integer from a rational use a floor or a ceiling function? If you need to create a Integer from a natural number cast it. If you need to show that an integer is "equal" to a natural number show that the integer is nonnegative?

Overall this introduces several new concepts for me which I shall study. Thankfully I was not far off with my proof so I can consider this a success. It uses several lemmas that I thought are existent and knowing that those are existent will help me understand how to further structure my proof.

Thanks for taking your time to help me @Kevin Buzzard . I wished that you'd been one of my instructors.