Working with positive nat and sequences

Stream: new members

[Daniele Bolla]

Hello everyone.
I need some help for a poof i am working on.
There is only a sorry part i need to fill, wich is proving that the natural number n is positive, but i can't find an easy way that will not change other part of the proof.
I can probably define my function f using (n+1) instead , to avoid the case where n is zero.
What is the best approach in this case?

import Mathlib

open Topology Filter

def S : Set (ℝ × ℝ) := (fun x ↦ (x, Real.sin (x⁻¹))) '' Set.Ioi (0 : ℝ)

def Z : Set (ℝ × ℝ) := { (0, 0) }

def T : Set (ℝ × ℝ) := S ∪ Z

def clsOfS := closure S

lemma TsubClsOfS : T ⊆ clsOfS := by
  intro x hx
  cases hx with
  | inl hxS => exact subset_closure hxS
  | inr hxZ =>
      rw [hxZ]
      let f :  ℕ →  ℝ × ℝ := fun n => ((n * Real.pi)⁻¹, 0)
      have hnMulpiAtTop : Tendsto (fun n : ℕ => n * Real.pi) atTop atTop := by
        apply Filter.Tendsto.atTop_mul_const'
        · exact Real.pi_pos
        · exact tendsto_natCast_atTop_atTop
      have hf : Tendsto f atTop (𝓝 (0, 0))  := by
        apply Filter.Tendsto.prod_mk_nhds
        · exact tendsto_inv_atTop_zero.comp hnMulpiAtTop
        · exact tendsto_const_nhds
      have hf' : ∀ᶠ n in atTop, f n ∈ S := by
        have hfInS : ∀ n, f n ∈ S := by
          intro n
          use (n * Real.pi)⁻¹
          constructor
          rw [Set.mem_Ioi]
          · apply inv_pos.mpr
            apply mul_pos
            · sorry
            · exact Real.pi_pos
          · unfold f
            calc (fun x ↦ (x, Real.sin x⁻¹)) (n * Real.pi)⁻¹ =
              ((n * Real.pi)⁻¹, Real.sin ((n * Real.pi)⁻¹)⁻¹) := by rfl
              _ = ((n * Real.pi)⁻¹, Real.sin (n * Real.pi)) := by
                  congr
                  simp only [inv_inv]
              _ = ((n * Real.pi)⁻¹,0) := by
                congr
                apply Real.sin_nat_mul_pi
        filter_upwards [Filter.Eventually.of_forall hfInS] with n hn
        exact hn
      apply mem_closure_of_tendsto hf hf'

[Kevin Buzzard]

What do you expect the value of $f(0)$ to be?

[Daniele Bolla]

I think it's undefined

[Kevin Buzzard]

Well that's not how lean works!

[Kevin Buzzard]

It's junk. It's defined and mathematically incorrect. More precisely, it's $(0,0)$.

[Kevin Buzzard]

So your proof takes a wrong turn at have hfInS and you could change that to \forall n \geq 1,... and then you should be ok with minimal other changes.

[Aaron Liu]

"undefined" is not a pair of real numbers, and f has to return a pair of real numbers, see https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/

[Daniele Bolla]

ok thanks so much!

[Kevin Buzzard]

You'll have to replace Filter.Eventually.of_forall with a more appropriate lemma but overall the changes will be minimal.