feat(ErdosProblems): 1096

[anhhuyalex]

closes #1295

[callesonne]

Thanks! Here are some initial comments. I would suggest that maybe you actually rewrite the theorem to use Nat.nth as quantifying over these sequences x. This would mean that Sums also needs to be rewritten to IsSum as a map from ℕ to Prop.

[callesonne]

Suggested change

	def Sums (q : ℝ) : Set ℝ :=
	{ s | ∃ S : Finset ℕ, s = ∑ i ∈ S, q ^ i }
	def Sums (q : ℝ) : Set ℝ := { ∑ i ∈ S, q ^ i | S : Finset ℕ }

Here is a more compact way of writing this.

[callesonne]

Suggested change

	∃ ε > 0, ∀ q, 1 < q → q < 1 + ε →
	∀ x : ℕ → ℝ, StrictMono x → Set.range x = Sums q →
	Tendsto (fun k => x (k + 1) - x k) atTop (nhds 0) ↔ answer(sorry) :=
	(∃ ε > 0, ∀ q, 1 < q → q < 1 + ε →
	∀ x : ℕ → ℝ, StrictMono x → Set.range x = Sums q →
	Tendsto (fun k => x (k + 1) - x k) atTop (𝓝 0)) ↔ answer(sorry) :=

[callesonne]

Suggested change

	# Erdős Problem 1096
	*Reference:* [erdosproblems.com/1096](https://www.erdosproblems.com/1096)
	# Erdős Problem 1096
	*Reference:* [erdosproblems.com/1096](https://www.erdosproblems.com/1096)

[anhhuyalex]

Thank you for your comments @callesonne ! After reading the docs, Nat.nth looks like it finds the n-th natural number satisfying p. But x is a sequence of real numbers. I couldn't find a similar definition in mathlib (e.g. Real.nth) that finds the n-th real number satisfying p. Should I try defining that in this commit ?

[callesonne]

Thank you for your comments @callesonne ! After reading the docs, Nat.nth looks like it finds the n-th natural number satisfying p. But x is a sequence of real numbers. I couldn't find a similar definition in mathlib (e.g. Real.nth) that finds the n-th real number satisfying p. Should I try defining that in this commit ?

Ahh no you are right, I got it mixed up. Then I think only my above comments need to be addressed (ignoring the one about Nat.nth!)