[Merged by Bors] - feat(NumberTheory): Rayleigh's theorem

[int-y1]

---

This is a theorem from #6091

[urkud]

We have Real.IsConjugateExponent. IMHO, should be used here.

[int-y1]

We have Real.IsConjugateExponent. IMHO, should be used here.

Done. I also added rayleigh' that uses IsConjugateExponent as a hypothesis.

[tb65536]

Would it be nicer to first prove the generalization here (https://en.wikipedia.org/wiki/Beatty_sequence#Generalizations) involving floor and ceiling - 1? That way you don't have to bother with positivity and irrationality until the end.

[tb65536]

Why not use Real.IsConjugateExponent all the way through? It seems to make things easier. For example:

variable {r s : ℝ}

theorem no_collision (h : r.IsConjugateExponent s) : Disjoint (beattySet r) (beattySet' s) := by
  rw [Set.disjoint_left]
  intro j ⟨k, h₁⟩ ⟨m, h₂⟩
  rw [beattySequence, Int.floor_eq_iff,
      ← mul_le_mul_right h.symm.pos, ← mul_lt_mul_right h.symm.pos, mul_assoc] at h₁
  rw [beattySequence', sub_eq_iff_eq_add, Int.ceil_eq_iff,
      Int.cast_add, Int.cast_one, add_sub_cancel,
      ← mul_lt_mul_right h.pos, ← mul_le_mul_right h.pos, mul_assoc, mul_comm s r] at h₂
  have h₃ := add_lt_add_of_lt_of_le h₂.1 h₁.1
  have h₄ := add_lt_add_of_le_of_lt h₂.2 h₁.2
  rw [← mul_add, ← add_mul, h.mul_eq_add, mul_lt_mul_right (add_pos h.pos h.symm.pos)] at h₃ h₄
  rw [← Int.cast_add, Int.cast_lt, ← not_le] at h₃
  rw [← Int.cast_one, ← Int.cast_add, ← Int.cast_add, Int.cast_lt, Int.lt_add_one_iff] at h₄
  exact h₃ h₄

[int-y1]

Why not use Real.IsConjugateExponent all the way through? It seems to make things easier.

I made this change and the proof became shorter. I also slightly golfed your proof of no_collision.

I don't think rayleigh_xxx' is necessary anymore, so I removed these extra theorems.

[YaelDillies]

Is there not a version of this theorem for beattySet/beattySet'?

[int-y1]

Yes, rayleigh_compl is a version for all integers. I included rayleigh_pos because it wasn't that easy to restrict rayleigh_compl to the positive integers.

Edit: rayleigh_compl was renamed to compl_beattySeq

[YaelDillies]

Can you ensure that every statement is available both under name for the "all of Int" version and name_pos for the > 0 version?

[YaelDillies]

I think there's still a few golfing opportunities, but I'm mostly happy with it now!

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style