Expressing a problem about positive integers

Stream: new members

[Nathan]

Is this the best way to express this problem? I thought I should use def Zp := {n : ℕ // n ≠ 0} but this led to a lot of problems.

image.png

import Mathlib.Algebra.BigOperators.Group.Finset.Defs
import Mathlib.Order.Interval.Finset.Defs
import Mathlib.Order.Interval.Finset.Nat

theorem POTD2411 (a : ℕ → ℕ)
    (h₁ : ∀ n : ℕ, a n ≤ 2025)
    (h₂ : ∀ n : ℕ, n ≠ 0 → ∃ k : ℤ, k^n = ∏ i : Fin n, a i) :
    ∃ c N : ℕ, c ≠ 0 ∧ N ≠ 0 ∧ ∀ n : ℕ, n ≥ N → a n = c := by
  sorry

[Kenny Lau]

do you have to start with 1?

[Nathan]

i started with a_0 but it would be better if i could start with a_1 so i could be as close to the problem as possible

[Kenny Lau]

Nathan said:

def Zp := {n : ℕ // n ≠ 0} but this led to a lot of problems

we have PNat, and what problems did it lead to?

[Kenny Lau]

note that your first step, if you do use PNat, should be to convert it to Nat

[Weiyi Wang]

If your goal is formalizing a proof, not just the statement, I suggest formalizing the proof with the shifted index starting from 0 because it will be easier to work with Nat, then write a thin layer to translate the statement to PNat

[Nathan]

i can do something like this but i have trouble with the product

import Mathlib.Algebra.BigOperators.Group.Finset.Defs
import Mathlib.Data.PNat.Notation
import Mathlib.Order.Interval.Finset.Nat

theorem POTD2411 (a : PNat → PNat)
    (h₁ : ∀ n : PNat, (a n).val ≤ 2025)
    (h₂ : ∀ n : PNat, ∃ k : ℤ, k^n.val = ∏ i : Fin n, a i) :
    ∃ c N : PNat, ∀ n : PNat, n.val ≥ N.val → a n = c := by
  sorry

[Ruben Van de Velde]

I would suggest ∏ i ∈ Finset.range n, a i instead of dealing with Fin

[Nathan]

i think i might want a Finset of PNat

[Nathan]

but i think i need to tell it somehow that the set is finite

[Nathan]

or alternatively use Finset.range and convert the index into a PNat

[Weiyi Wang]

You can use Finset.Icc and friends

[Nathan]

ohhh Finset.Icc works

[Nathan]

yeah i think maybe the problem was that range was including 0

[Nathan]

thanks folks :pray:

[Nathan]

how do i get the power of a prime in a natural number? for example the power of 3 in 18 is 2 because 3^2 divides 18 but 3^3 doesn't.

I found Int.padicValuation, but why does #eval Int.padicValuation 3 18 evaluate to some (-2) rather than 2?

[Nathan]

oh i found it: #eval padicValNat 3 18

[Vlad]

It may be easier to state the theorem by casting to real numbers. Number 2025 can be replaced by arbitrary natural number.

example {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
  sorry

Proof

import Mathlib

section helper_lemmas

variable {α : Type*}
variable [ha₁ : LinearOrder α] [ha₂ : Ring α]
variable [ha₃ : IsOrderedAddMonoid α] [ha₄ : ZeroLEOneClass α] [ha₅ : NeZero (1 : α)]

@[simp]
theorem left_lt_max_add_one {a b : α} : a < max a b + 1 :=
  lt_of_le_of_lt (le_max_left _ _) (lt_add_one _)

@[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; simp [mul_succ]

theorem Finset.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

end helper_lemmas

open Finset

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 <;> try omega
    suffices h : 1 + k < r; omega
    apply lt_of_lt_of_le (b := c + k + 1)
    linarith; rw [←hk]; apply h₂
  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]; 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 : ℝ), Commute.add_pow $ by simp [Commute],
      show n + 1 + 1 = 1 + 1 + n by ring_nf, 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₂; norm_cast at 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 <;> try omega;; linarith [h₁ n]
  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]; 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₆
    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
      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
    · norm_cast; trans c + 1; simp; apply h₅.trans; simp; right; linarith [h₁ n]
    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
      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 <;> rw [←hw] <;> simp
    apply lt_of_le_of_lt (b := (1 + 1 / r : ℝ) ^ (Real.logb (1 + 1 / r) r))
    rw [Real.rpow_logb] <;> try positivity;; simp; linarith
    simp_rw [←Real.rpow_natCast]; rwa [Real.rpow_lt_rpow_left_iff]; field_simp; simp
  simp at H₂; replace H₃ : c - 1 < c₁; exact_mod_cast H₃; omega

example {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₁
  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₄; 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, Real.le_rpow_inv_iff_of_pos] <;> try positivity
    simp; apply one_le_prod_of_forall_one_le; simp; intros; apply h₁
  have h₅ : c ≤ r
  · suffices h : (c : ℝ) ≤ r; exact_mod_cast h
    rw [←hc, Real.rpow_inv_le_iff_of_pos] <;> try positivity
    convert_to _ ≤ ∏ i ∈ range N, (r : ℝ); simp
    apply Finset.prod_le_prod <;> 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; intros; apply H; simp; linarith
    rw [h₆, ←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