Erdős 480 more misformalization

[plby]

Describe the misformalization

Erdős problem 480 is still misformalized.

This was previously reported in #1282 but then closed in #1540

Trivial proof/disproof

Here is an example proof:

theorem erdos_480 : ∀ (x : ℕ → ℝ), (∀ n, x n ∈ Set.Icc 0 1) →
    ⨅ n, atTop.liminf (fun m => n * |x (m + n) - x m|) ≤ 1 / √5 := by
  field_simp;
  intro x hx;
  refine' le_trans ( mul_le_mul_of_nonneg_right ( ciInf_le _ 0 ) ( Real.sqrt_nonneg _ ) ) _ <;> norm_num [ Filter.liminf_const ];
  refine' ⟨ 0, Set.forall_mem_range.2 fun n => _ ⟩;
  refine' le_csSup _ _ <;> norm_num;
  · exact ⟨ n * 1, by rintro a ⟨ m, hm ⟩ ; exact le_trans ( hm m le_rfl ) ( mul_le_mul_of_nonneg_left ( show |x ( m + n ) - x m| ≤ 1 by exact abs_le.mpr ⟨ by linarith [ Set.mem_Icc.mp ( hx ( m + n ) ), Set.mem_Icc.mp ( hx m ) ], by linarith [ Set.mem_Icc.mp ( hx ( m + n ) ), Set.mem_Icc.mp ( hx m ) ] ⟩ ) ( Nat.cast_nonneg _ ) ) ⟩;
  · exact ⟨ 0, fun _ _ => mul_nonneg ( Nat.cast_nonneg _ ) ( abs_nonneg _ ) ⟩

The variant erdos_480.variants.chung_graham is also easily provable.

Suggested fix

The inf is for n=0. There was a problem before wherein the code divided by $n$, so that was a hint that one should have the condition $n\ne 0$. Now the formulation doesn't divide by $n$ anymore, but $n=0$ should still be avoided.

Tldr: add $n\ne 0$ or $1 \le n$.

Additional context

I have found formalizing this problem very frustrating.

Choose either option

• I plan on working on this issue
• This issue is up for grabs: I would like to see this misformalization fixed by somebody else