Bijections and Inverses

Stream: Is there code for X?

[Mark Gerads]

I would like code for this lemma and decided to check if someone already did something similar (and probably more general)

/-- order of inverse does not matter when canceling to the identity function -/
lemma inv_order_not_matter
      (perm : ℕ → ℕ) (perm_inv : ℕ → ℕ) (h_inv : ∀ (k : ℕ), (perm (perm_inv k) = k))
      : ∀ (k : ℕ), (perm_inv (perm k) = k) :=

[Yury G. Kudryashov]

This lemma is wrong. Take docs#nat.pred and docs#nat.succ

[Yaël Dillies]

You need perm_inv to be injective.

[Mark Gerads]

Okay, so what is the proper way to declare a bijection on \N and the inverse function?

[Yury G. Kudryashov]

Have a look at docs#equiv

[Yury G. Kudryashov]

@Yaël Dillies you mean surjective

[Yaël Dillies]

perm surjective

[Mark Gerads]

The reason I want a bijection on \N is so I can attempt to show that every reordering of a Cauchy sequence is another Cauchy sequence with the same limit.

[Yaël Dillies]

No but perm being injective is definitely enough.

[Yaël Dillies]

Argh, confused

[Yury G. Kudryashov]

You should prove that for a permutation of natural numbers, map f at_top = at_top.

[Yury G. Kudryashov]

This follows from the fact that any injective map tends to infinity

[Yury G. Kudryashov]

And I would prove that for docs#filter.cofinite and any pair of types

[Mark Gerads]

Is this properly stated?

/-- rearranging a Cauchy sequence results in a sequence that is also Cauchy with the same limit -/
lemma rearranging_cauchy_also_cauchy
      (perm : ℕ → ℕ) (perm_inv : ℕ → ℕ)
      (h_inv_0 : ∀ (k : ℕ), (perm (perm_inv k) = k))
      (h_inv_1 : ∀ (k : ℕ), (perm_inv (perm k) = k))
      (cs : ℕ → ℝ) (h_cs_cauchy : is_cau_seq abs cs)
      : is_cau_seq abs (λ (k:ℕ), cs (perm k)) :=

I actually wanted cs to be a complex-valued Cauchy sequence, but I don't know how to do that with mathlib.

[Eric Wieser]

Why not use perm ℕ (docs#equiv.perm)?

[Mark Gerads]

Because I am a newb who did not know.

[Eric Wieser]

Note that's juts another spelling for the equiv that Yury mentioned above

[Mark Gerads]

I just figured out Complex-valued Cauchy sequences.

/-- rearranging a Cauchy sequence results in a sequence that is also Cauchy with the same limit -/
lemma rearranging_cauchy_also_cauchy
      (perm : ℕ → ℕ) (perm_inv : ℕ → ℕ)
      (h_inv_0 : ∀ (k : ℕ), (perm (perm_inv k) = k))
      (h_inv_1 : ∀ (k : ℕ), (perm_inv (perm k) = k))
      (cs : ℕ → ℂ) (h_cs_cauchy : is_cau_seq complex.abs cs)
      : is_cau_seq complex.abs (λ (k:ℕ), cs (perm k)) :=

[Mark Gerads]

And have yet to figure out how to use equiv.perm.

[Mark Gerads]

Is this correct?

/-- rearranging a Cauchy sequence results in a sequence that is also Cauchy with the same limit -/
lemma rearranging_cauchy_also_cauchy
      (perm : equiv.perm ℕ)
      (cs : ℕ → ℂ) (h_cs_cauchy : is_cau_seq complex.abs cs)
      : is_cau_seq complex.abs (λ (k:ℕ), cs (perm k)) :=

[Mark Gerads]

That looks like it might be wrong or right.

[Heather Macbeth]

is_cau_seq is an "implementation detail", you should use docs#cauchy_seq which has more lemmas.

[Yury G. Kudryashov]

Here is the statement:

lemma cauchy_seq.comp_injective {α : Type*} [uniform_space α] {u : ℕ → α} (hu : cauchy_seq u)
  {f : ℕ → ℕ} (hf : function.injective f) : cauchy_seq (u ∘ f)

[Yury G. Kudryashov]

And the proof is

open function filter

lemma function.injective.tendsto_at_top {f : ℕ → ℕ} (hf : injective f) :
  tendsto f at_top at_top :=
by simpa only [← nat.cofinite_eq_at_top] using hf.tendsto_cofinite

lemma cauchy_seq.comp_injective {α : Type*} [uniform_space α] {u : ℕ → α} (hu : cauchy_seq u)
  {f : ℕ → ℕ} (hf : injective f) : cauchy_seq (u ∘ f) :=
hu.comp_tendsto hf.tendsto_at_top

[Mark Gerads]

This is not in mathlib yet then? @Yury G. Kudryashov Would you be willing to submit your proof to mathlib? I am unable to make a better proof for the statement cauchy_seq.comp_injective.

[Yury G. Kudryashov]

#11986

[Mark Gerads]

It might be good to include proof that the limit is unchanged by the permutation. I have a 'proof' in this PDF https://drive.google.com/file/d/1o0FP9prFpbGa6b7zvcOJeb37NldaNg-x/view?usp=sharing , but do not know if LEAN will accept it.

[Mark Gerads]

I'm looking at cau_seq.lim right now, trying to figure out how to state that the limits of the 2 Cauchy Sequences are equal.