User:Hakerh400/Proof aux001

We are given a sequence $a:\mathbb {N} \to \mathbb {N}$ of positive integers (i.e., $a(n)\geq 1$ for all $n$) such that:

1. $a(n)\leq r$ for all $n$, where $r$ is a fixed positive integer.
2. For every $n$, the geometric mean of the first $n$ terms is an integer. That is, there exists an integer $k_{n}$ such that

$\left(\prod _{i=0}^{n-1}a(i)\right)^{1/n}=k_{n}$

We aim to show that there exist positive integers $c$ and $N$ such that $a(n)=c$ for all $n\geq N$.

Step 1: Setting up $N$ and $c$

Let

$L=\log _{1+{\frac {1}{r}}}(r)={\frac {\ln r}{\ln \left(1+{\frac {1}{r}}\right)}}$

Since $1+{\frac {1}{r}}>1$, $L$ is finite. Choose a natural number $N$ such that

$N>\max\{r,L\}+1$

Such an $N$ exists because the natural numbers are unbounded.

Now, consider the geometric mean of the first $N$ terms. By hypothesis, there exists an integer $c$ such that

$\left(\prod _{i=0}^{N-1}a(i)\right)^{1/N}=c$

Since each $a(i)\geq 1$, we have $c\geq 1$; and since each $a(i)\leq r$, we have $c\leq r$.

Step 2: Proof that $a(n)=c$ for all $n\geq N$

We prove by strong induction on $n$ that for all $n\geq N$, $a(n)=c$.

Base case ($n=N$):

Assume, for contradiction, that $a(N)\neq c$. Then either $a(N)>c$ or $a(N)<c$.

Case 1: $a(N)>c$

Let $\delta =a(N)-c\geq 1$. Consider the geometric mean of the first $N+1$ terms, which is an integer $c_{1}$. Then:

$c_{1}=\left(\prod _{i=0}^{N}a(i)\right)^{1/(N+1)}=\left(c^{N}\cdot a(N)\right)^{1/(N+1)}=\left(c^{N}(c+\delta )\right)^{1/(N+1)}$

Since $c+\delta >c$, we have $c_{1}>c$. To show $c_{1}<c+1$, note:

Failed to parse (syntax error): {\displaystyle c_1^{N+1} = c^N (c + \delta) \leq c^N \cdot r \quad \text{(as \( a(N) \leq r \), so \( \delta \leq r - c \))}}

Since $r<N$ (by choice of $N$), and $c\leq r$, we have:

$c^{N}\cdot r<c^{N}\cdot N$

We now show $c^{N}\cdot N<(c+1)^{N+1}$. By the binomial theorem:

$(c+1)^{N+1}=(c+1)(c+1)^{N}\geq (c+1)\left(c^{N}+Nc^{N-1}\right)=c^{N+1}+c^{N}+(c+1)Nc^{N-1}$

Then:

$(c+1)^{N+1}-c^{N}\cdot N=c^{N-1}\left(c^{2}+c+N\right)>0,$

since $c\geq 1$ and $N\geq 1$. Hence, $c_{1}^{N+1}<(c+1)^{N+1}$, so $c_{1}<c+1$. Thus, $c<c_{1}<c+1$, but $c_{1}$ is an integer — contradiction.

Case 2: $a(N)<c$

Let $\delta =c-a(N)\geq 1$. The geometric mean of the first $N+1$ terms is:

$c_{1}=\left(c^{N}(c-\delta )\right)^{1/(N+1)}$

Clearly, $c_{1}<c$. We show $c_{1}>c-1$, i.e.,

$c^{N}(c-\delta )>(c-1)^{N+1}$

Since $a(N)=c-\delta \geq 1$, we have $\delta \leq c-1$. Note:

$(c-1)^{N+1}=(c-1)(c-1)^{N}$

The inequality is equivalent to:

$\left({\frac {c}{c-1}}\right)^{N}a(N)>c-1$

Since $a(N)\geq 1$, it suffices to show:

$\left({\frac {c}{c-1}}\right)^{N}>c-1$

But ${\frac {c}{c-1}}=1+{\frac {1}{c-1}}$, and since $c\leq r$, we have:

$1+{\frac {1}{c-1}}\geq 1+{\frac {1}{r-1}}>1+{\frac {1}{r}}$

By choice of $N$, we have $N>L$, so:

$\left(1+{\frac {1}{r}}\right)^{N}>r\geq c$

Therefore:

$\left(1+{\frac {1}{c-1}}\right)^{N}\geq \left(1+{\frac {1}{r}}\right)^{N}>r\geq c>c-1,$

since $c\geq 2$ (as $c=1$ would force $a(N)<1$, impossible). Hence, $c_{1}>c-1$. But $c_{1}<c$, and $c_{1}$ is an integer — contradiction.

In both cases, we obtain a contradiction, so $a(N)=c$.

Inductive step:

Assume for some $n\geq N$, and for all $k$ with $N\leq k<n$, we have $a(k)=c$. Then for all $k$ with $N\leq k\leq n$, the geometric mean of the first $k$ terms is $c$. In particular, for $k=n$:

$\left(\prod _{i=0}^{n-1}a(i)\right)^{1/n}=c$

Now consider the geometric mean of the first $n+1$ terms, an integer $c_{1}$:

$c_{1}=\left(\left(\prod _{i=0}^{n-1}a(i)\right)\cdot a(n)\right)^{1/(n+1)}=\left(c^{n}\cdot a(n)\right)^{1/(n+1)}$

Since $n\geq N>\max\{r,L\}+1$, we have $n>r$ and $n>L$. The same argument as in the base case (with $N$ replaced by $n$) shows that $a(n)=c$.

By strong induction, $a(n)=c$ for all $n\geq N$.

Formal proof

import Mathlib

open Finset

@[simp]
theorem Nat.le_self_mul_iff {a b : ℕ} : a ≤ a * b ↔ a = 0 ∨ b ≠ 0 := by
  constructor
  · intro h; rw [or_iff_not_imp_left]
    rintro h₁ rfl; simp at h; contradiction
  rintro (rfl | h); simp
  cases b; simp at h; rename_i b
  simp [mul_succ]

theorem one_le_prod_of_forall_one_le {ι : Type*} {s : Finset ι} {f : ι → ℝ}
(h : ∀ i ∈ s, 1 ≤ f i) : 1 ≤ ∏ i ∈ s, f i := by
  classical
  induction s using Finset.induction
  · simp
  rename_i i s hi ih
  rw [Finset.prod_insert hi]
  simp at h
  rcases h with ⟨h₁, h₂⟩
  specialize ih h₂
  nlinarith

@[simp]
theorem left_lt_max_add_one {α : Type*} [ha₁ : LinearOrder α] [ha₂ : Ring α]
[ha₃ : IsOrderedAddMonoid α] [ha₄ : ZeroLEOneClass α]
[ha₅ : NeZero (1 : α)] {a b : α} : a < max a b + 1 :=
  lt_of_le_of_lt (le_max_left _ _) (lt_add_one _)

theorem aux₁ {r N n c : ℕ} {a : ℕ → ℕ} (h₂ : ∀ (n : ℕ), a n ≤ r)
(h₃ : ∀ (n : ℕ), ∃ (k : ℕ), (∏ i ∈ range n, (a i : ℝ)) ^ (n : ℝ)⁻¹ = k)
(hrN : r < N) (hn : N ≤ n) (h₄ : 1 ≤ c)
(H₁ : ∀ (k : ℕ), N ≤ k → k ≤ n → (∏ i ∈ range k, a i : ℝ) ^ (k : ℝ)⁻¹ = c) : a n ≤ c := by
  by_contra! h₆
  replace h₆ : ∃ δ, 1 ≤ δ ∧ δ < r ∧ a n = c + δ
  · use a n - c
    obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_lt h₆
    simp [hk]
    ring_nf
    split_ands
    · omega
    · suffices h : 1 + k < r; omega
      apply lt_of_lt_of_le (b := c + k + 1)
      · linarith
      rw [←hk]
      apply h₂
    · omega
  obtain ⟨δ, h₆, h₇, h₈⟩ := h₆
  have hn₁ : n ≠ 0
  · linarith
  have h₉ := H₁ n (by linarith) (by linarith)
  rw [Real.rpow_inv_eq] at h₉ <;> try positivity
  obtain ⟨c₁, hc₁⟩ := h₃ (n + 1)
  rw [prod_range_succ, h₉, h₈] at hc₁
  have H₂ : (c : ℝ) < c₁
  · rw [←hc₁, Real.lt_rpow_inv_iff_of_pos, Nat.cast_add, Nat.cast_add, Nat.cast_one,
      Real.rpow_add, mul_lt_mul_iff_right₀, Real.rpow_one, lt_add_iff_pos_right] <;> positivity
  have H₃ : (c₁ : ℝ) < c + 1
  · rw [←hc₁, Real.rpow_inv_lt_iff_of_pos, Nat.cast_add, mul_add] <;> try positivity
    have h : (c : ℝ) ^ (n : ℝ) * c = c ^ ((n + 1 : ℕ) : ℝ)
    · rw [Nat.cast_add, Nat.cast_one, Real.rpow_add, Real.rpow_one]; positivity
    rw [h]; clear h
    simp only [Real.rpow_natCast]
    apply lt_of_lt_of_le (b := (c : ℝ) ^ (n + 1) + (c : ℝ) ^ n * n)
    · simp; rw [mul_lt_mul_iff_right₀] <;> try positivity
      simp; linarith
    rw [add_comm (c : ℝ)]
    rw [Commute.add_pow $ by simp [Commute]]
    rw [show n + 1 + 1 = 1 + 1 + n by ring_nf]
    rw [sum_range_add, sum_range_add]
    simp only [range_one, one_pow, one_mul, sum_singleton, tsub_zero, Nat.choose_zero_right,
      Nat.cast_one, mul_one, add_zero, add_tsub_cancel_right, Nat.choose_one_right, Nat.cast_add,
      Nat.reduceAdd, add_assoc, add_le_add_iff_left]
    rw [mul_add]
    simp only [mul_one, add_assoc, le_add_iff_nonneg_right]
    positivity
  simp at H₂
  replace H₃ : c₁ < c + 1; exact_mod_cast H₃
  omega

theorem aux₂ {r N n c : ℕ} {w : ℝ} {a : ℕ → ℕ}
(h₃ : ∀ (n : ℕ), ∃ (k : ℕ), (∏ i ∈ range n, (a i : ℝ)) ^ (n : ℝ)⁻¹ = k)
(hw : max (r : ℝ) (Real.logb (1 + 1 / r) r) + 1 = w)
(hN : w < N) (hr : 1 ≤ r) (hrN : r < N) (hn : N ≤ n)
(hc : ∏ i ∈ range N, (a i : ℝ) = (c : ℝ) ^ (N : ℝ)) (h₅ : c ≤ r)
(H : ∀ (k : ℕ), N ≤ k → k < n → a k = c) (h₁ : ∀ (n : ℕ), 1 ≤ a n) (h₄ : 1 ≤ c)
(H₁ : ∀ (k : ℕ), N ≤ k → k ≤ n → (∏ i ∈ range k, a i : ℝ) ^ (k : ℝ)⁻¹ = c) : c ≤ a n := by
  by_contra! h₆
  replace h₆ : ∃ δ, 1 ≤ δ ∧ δ < c ∧ a n = c - δ
  · use c - a n
    obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_lt h₆
    simp [hk]
    ring_nf
    split_ands
    · omega
    · linarith [h₁ n]
    · omega
  obtain ⟨δ, h₆, h₇, h₈⟩ := h₆
  have hn₁ : n ≠ 0
  · linarith
  have h₉ := H₁ n (by linarith) (by linarith)
  rw [Real.rpow_inv_eq] at h₉ <;> try positivity
  obtain ⟨c₁, hc₁⟩ := h₃ (n + 1)
  rw [prod_range_succ, h₉, h₈] at hc₁
  have H₀ : c ≠ 0
  · linarith
  have H₂ : (c₁ : ℝ) < c
  · rw [←hc₁, Real.rpow_inv_lt_iff_of_pos, Nat.cast_add, Nat.cast_sub, Nat.cast_one,
      Real.rpow_add, mul_lt_mul_iff_right₀, Real.rpow_one, sub_lt_self_iff]
    all_goals first | positivity | linarith
  have H₃ : (c - 1 : ℝ) < c₁
  · rw [←hc₁, Real.lt_rpow_inv_iff_of_pos, Nat.cast_sub, mul_sub]
      <;> try first | positivity | (try simp); linarith
    have h : (c : ℝ) ^ (n : ℝ) * c = c ^ ((n + 1 : ℕ) : ℝ)
    · rw [Nat.cast_add, Nat.cast_one, Real.rpow_add, Real.rpow_one]; positivity
    rw [h]; clear h
    simp only [Real.rpow_natCast]
    replace h₈ : a n + δ = c; omega
    replace h₈ : (a n + δ : ℝ) = c; exact_mod_cast h₈
    rw [show (δ : ℝ) = c - a n by linarith]
    cases c; simp at H₀; clear H₀; rename_i c
    simp
    have hc₂ : 1 ≤ c
    · cases c
      · simp at h₇
        subst h₇
        simp at h₆
      simp
    convert_to _ < (c + 1 : ℝ) ^ n * a n
    · ring_nf
    suffices h : (1 : ℝ) < a n / c * (1 + 1 / c) ^ n
    · suffices h₁ : (c : ℝ) ^ (n + 1) * (a n / c * (1 + 1 / c) ^ n) ≤ (c + 1) ^ n * (a n)
      · apply lt_of_lt_of_le _ h₁
        field_simp at h ⊢
        exact h
      clear h
      rw [pow_succ]
      field_simp
      simp_rw [←Real.rpow_natCast]
      rw [Real.div_rpow] <;> try positivity
      field_simp
      simp
    have G₁ : (c : ℝ) ≤ r * a n
    · suffices h : c ≤ r * a n; exact_mod_cast h
      trans c + 1; simp
      apply h₅.trans
      simp
      right
      specialize h₁ n
      linarith
    suffices h :  (1 : ℝ) < 1 / r * (1 + 1 / ↑c) ^ n
    · field_simp at h ⊢
      apply lt_of_le_of_lt G₁
      rwa [mul_lt_mul_iff_left₀]
      simp
      linarith [h₁ n]
    suffices h : (1 : ℝ) < 1 / r * (1 + 1 / r) ^ n
    · field_simp at h ⊢
      apply lt_of_lt_of_le h; clear h
      rw [pow_le_pow_iff_left₀] <;> try positivity
      field_simp
      ring_nf
      rw [add_comm]
      simp
      linarith
    suffices h : (r : ℝ) < (1 + 1 / r) ^ n
    · field_simp at h ⊢; exact h
    have G₁ : Real.logb (1 + 1 / r) r < n
    · replace hn : (N : ℝ) ≤ n; exact_mod_cast hn
      apply lt_of_lt_of_le _ hn
      apply lt_of_le_of_lt _ hN
      rw [←hw]
      trans w - 1
      rotate_left
      · rw [←hw]
        simp
      rw[ ←hw]
      simp
    apply lt_of_le_of_lt (b := (1 + 1 / r : ℝ) ^ (Real.logb (1 + 1 / r) r))
    rotate_left
    · simp_rw [←Real.rpow_natCast]
      rwa [Real.rpow_lt_rpow_left_iff]
      field_simp; simp
    rw [Real.rpow_logb] <;> try positivity
    simp
    linarith
  simp at H₂
  replace H₃ : c - 1 < c₁; exact_mod_cast H₃
  omega

theorem main {r : ℕ} {a : ℕ → ℕ} (h₁ : ∀ n, a n ≠ 0) (h₂ : ∀ n, a n ≤ r)
(h₃ : ∀ n, ∃ (k : ℕ), (∏ i ∈ range n, a i : ℝ) ^ (n : ℝ)⁻¹ = k) :
∃ c N, ∀ n, N ≤ n → a n = c := by
  generalize hw : max (r : ℝ) (Real.logb (1 + 1 / r) r) + 1 = w
  obtain ⟨N, hN⟩ := exists_nat_gt w
  have hr : 1 ≤ r
  · cases r
    · simp at h₂
      simp [h₂] at h₁
    simp
  have hrw : r < w
  · rw [←hw]; simp
  have hrN : r < N
  · suffices h : (r : ℝ) < N; exact_mod_cast h
    linarith
  have h0N : 0 < N
  · linarith
  obtain ⟨c, hc⟩ := h₃ N
  use c, N
  suffices h : ∀ n, N ≤ n → (∀ k, N ≤ k → k < n → a k = c) → a n = c
  · intro n hn
    obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le hn; clear hn
    induction n using Nat.strong_induction_on
    rename_i n ih
    apply h
    · omega
    · intro k h₄ h₅
      obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h₄; clear h₄
      apply ih
      omega
  intro n hn H
  simp [←Nat.one_le_iff_ne_zero] at h₁
  have h₄ : 1 ≤ c
  · suffices h : (1 : ℝ) ≤ c; exact_mod_cast h
    rw [←hc]
    rw [Real.le_rpow_inv_iff_of_pos] <;> try positivity
    simp
    apply one_le_prod_of_forall_one_le
    simp
    intro i hi
    apply h₁
  have h₅ : c ≤ r
  · suffices h : (c : ℝ) ≤ r; exact_mod_cast h
    rw [←hc]
    rw [Real.rpow_inv_le_iff_of_pos] <;> try positivity
    convert_to _ ≤ ∏ i ∈ range N, (r : ℝ); simp
    apply Finset.prod_le_prod
    · simp
    simp
    intro i hi
    linarith [h₂ i]
  rw [Real.rpow_inv_eq] at hc <;> try positivity
  have H₁ : ∀ k, N ≤ k → k ≤ n → (∏ i ∈ range k, a i : ℝ) ^ (k : ℝ)⁻¹ = c
  · intro k hk₁ hk₂
    obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hk₁; clear hk₁
    rw [prod_range_add, Real.mul_rpow] <;> try positivity
    simp
    rw [hc]
    have h₆ : ∏ i ∈ range k, (a $ N + i : ℝ) = (c : ℝ) ^ k
    · trans ∏ i ∈ range k, c
      rotate_left; simp
      apply prod_congr rfl
      simp
      intro m hm
      apply H
      · simp
      linarith
    rw [h₆]; clear h₆
    simp_rw [←Real.rpow_natCast]
    rw [←Real.mul_rpow, Real.rpow_inv_eq, ←Real.rpow_add] <;> try positivity
  apply le_antisymm
  · apply aux₁ <;> assumption
  · apply aux₂ <;> assumption