2607.19337v1 / Core.lean

all files

import Mathlib.Algebra.Polynomial.AlgebraMap
import Mathlib.Algebra.Polynomial.Bivariate
import Mathlib.LinearAlgebra.Dimension.StrongRankCondition
import Mathlib.LinearAlgebra.Matrix.ToLin

namespace ChampernowneA

open scoped BigOperators

/-- The integer matrix of the homogeneous cancellation system (2.2). -/
def cancellationMatrix (d : ℕ) (h : Fin (d * (d + 1) + 1) → ℤ) :
    Matrix (Fin (d + 1) × Fin d) (Fin (d * (d + 1) + 1)) ℤ :=
  fun uv j ↦ (j.val : ℤ) ^ uv.1.val * h j ^ uv.2.val

/-- The underdetermined integer system (2.2) has a nontrivial integer solution. -/
theorem exists_integer_cancellation (d : ℕ) (h : Fin (d * (d + 1) + 1) → ℤ) :
    ∃ c : Fin (d * (d + 1) + 1) → ℤ, c ≠ 0 ∧
      ∀ u : Fin (d + 1), ∀ v : Fin d,
        ∑ j, (j.val : ℤ) ^ u.val * h j ^ v.val * c j = 0 := by
  let A := cancellationMatrix d h
  have hnot : ¬ Function.Injective A.mulVecLin := by
    intro hinj
    have hle := A.mulVecLin.finrank_le_finrank_of_injective hinj
    simp only [Module.finrank_pi, Fintype.card_prod, Fintype.card_fin] at hle
    have : d * (d + 1) + 1 ≤ d * (d + 1) := by
      rw [Nat.mul_comm (d + 1) d] at hle
      exact hle
    omega
  rw [Function.not_injective_iff] at hnot
  obtain ⟨x, y, hmap, hxy⟩ := hnot
  refine ⟨x - y, sub_ne_zero.mpr hxy, ?_⟩
  intro u v
  have hz : A.mulVecLin (x - y) = 0 := by
    rw [map_sub, hmap, sub_self]
  have huv := congr_fun hz (u, v)
  simpa [A, cancellationMatrix, Matrix.mulVecLin_apply, Matrix.mulVec, dotProduct,
    mul_assoc] using huv

/-! The nonvanishing interpolation polynomial used after (2.2).  A polynomial in `x` and `y`
is represented as `Polynomial (Polynomial ℤ)`, with the outer variable equal to `y`. -/

open Polynomial

/-- The outer-variable factor `y + hᵢ`. -/
noncomputable def yFactor {n : ℕ} (h : Fin n → ℤ) (i : Fin n) : Polynomial (Polynomial ℤ) :=
  X + C (C (h i))

/-- The paper's polynomial `ρ(y) = ∏ᵢ (y+hᵢ)`. -/
noncomputable def rho {n : ℕ} (h : Fin n → ℤ) : Polynomial (Polynomial ℤ) :=
  ∏ i, yFactor h i

/-- The product `ρ(y)/(y+hⱼ)`, represented directly without polynomial division. -/
noncomputable def rhoWithout {n : ℕ} (h : Fin n → ℤ) (j : Fin n) : Polynomial (Polynomial ℤ) :=
  ∏ i ∈ Finset.univ.erase j, yFactor h i

theorem yFactor_mul_rhoWithout {n : ℕ} (h : Fin n → ℤ) (j : Fin n) :
    yFactor h j * rhoWithout h j = rho h := by
  classical
  exact Finset.mul_prod_erase Finset.univ (yFactor h) (Finset.mem_univ j)

theorem eval_rhoWithout_self {n : ℕ} (h : Fin n → ℤ) (i : Fin n) :
    (rhoWithout h i).eval (-C (h i)) =
      C (∏ j ∈ Finset.univ.erase i, (h j - h i)) := by
  simp [rhoWithout, yFactor, Polynomial.eval_prod, sub_eq_add_neg, add_comm]

theorem eval_rhoWithout_other {n : ℕ} (h : Fin n → ℤ) {i j : Fin n} (hij : i ≠ j) :
    (rhoWithout h j).eval (-C (h i)) = 0 := by
  rw [rhoWithout, Polynomial.eval_prod]
  apply Finset.prod_eq_zero (Finset.mem_erase.mpr ⟨hij, Finset.mem_univ i⟩)
  simp [yFactor]

/-- Translation of the integer polynomial `f` from `x` to `x+j`. -/
noncomputable def shift {n : ℕ} (f : Polynomial ℤ) (j : Fin n) : Polynomial ℤ :=
  f.comp (X + C (j.val : ℤ))

/-- The coefficients `bᵤ(n)` used on the last page exist: they are the coefficients of the
translated polynomial `f(X+n)`, whose degree is unchanged. -/
theorem shifted_polynomial_expansion (f : Polynomial ℤ) (n j : ℤ) :
    f.eval (n + j) = ∑ u ∈ Finset.range (f.natDegree + 1),
      (f.comp (X + C n)).coeff u * j ^ u := by
  calc
    f.eval (n + j) = (f.comp (X + C n)).eval j := by simp [add_comm]
    _ = ∑ u ∈ Finset.range ((f.comp (X + C n)).natDegree + 1),
        (f.comp (X + C n)).coeff u * j ^ u := Polynomial.eval_eq_sum_range j
    _ = _ := by rw [Polynomial.natDegree_comp, Polynomial.natDegree_X_add_C, Nat.mul_one]

/-- The paper's bivariate interpolation polynomial
`Φ(x,y) = ∑ⱼ cⱼ f(x+j) ρ(y)/(y+hⱼ)`. -/
noncomputable def Phi {n : ℕ} (f : Polynomial ℤ) (h c : Fin n → ℤ) :
    Polynomial (Polynomial ℤ) :=
  ∑ j, C (C (c j) * shift f j) * rhoWithout h j

theorem eval_Phi_at_node {n : ℕ} (f : Polynomial ℤ) (h c : Fin n → ℤ) (i : Fin n) :
    (Phi f h c).eval (-C (h i)) =
      C (c i) * shift f i * C (∏ j ∈ Finset.univ.erase i, (h j - h i)) := by
  classical
  rw [Phi]
  change (Polynomial.evalRingHom (-C (h i)))
      (∑ j, C (C (c j) * shift f j) * rhoWithout h j) = _
  rw [map_sum, Finset.sum_eq_single i]
  · change (C (C (c i) * shift f i) * rhoWithout h i).eval (-C (h i)) = _
    rw [Polynomial.eval_mul, eval_C, eval_rhoWithout_self]
  · intro j _ hji
    change (C (C (c j) * shift f j) * rhoWithout h j).eval (-C (h i)) = 0
    rw [Polynomial.eval_mul, eval_C, eval_rhoWithout_other h hji.symm, mul_zero]
  · simp

/-- The nonvanishing argument immediately following (2.2): distinct `hⱼ`, a nonzero `f`, and
a nontrivial coefficient vector force the constructed bivariate polynomial `Φ` to be nonzero. -/
theorem Phi_ne_zero {n : ℕ} (f : Polynomial ℤ) (h c : Fin n → ℤ)
    (hf : f ≠ 0) (hh : Function.Injective h) (hc : c ≠ 0) : Phi f h c ≠ 0 := by
  classical
  obtain ⟨i, hci⟩ := Function.ne_iff.mp hc
  intro hPhi
  have heval := congrArg (Polynomial.eval (-C (h i))) hPhi
  rw [eval_Phi_at_node] at heval
  simp only [Polynomial.eval_zero] at heval
  have hprod : (∏ j ∈ Finset.univ.erase i, (h j - h i)) ≠ 0 := by
    apply Finset.prod_ne_zero_iff.mpr
    intro j hj
    apply sub_ne_zero.mpr
    intro heq
    have hji : j = i := hh heq
    exact (Finset.ne_of_mem_erase hj) hji
  have hshift : shift f i ≠ 0 := by
    exact (Polynomial.comp_X_add_C_ne_zero_iff
      (p := f) (t := (i.val : ℤ))).mpr hf
  exact (mul_ne_zero (mul_ne_zero (Polynomial.C_ne_zero.mpr hci) hshift)
    (Polynomial.C_ne_zero.mpr hprod)) heval

/-! The exact finite expansion and cancellation used on the last page of the proof. -/

/-- The finite geometric-series identity displayed after (2.4). -/
theorem finite_geometric_identity {K : Type*} [Field K] (p h : K) (d : ℕ)
    (hp : p ≠ 0) (hph : p + h ≠ 0) :
    1 / (p + h) =
      (∑ v ∈ Finset.range d, (-h) ^ v / p ^ (v + 1)) +
        (-h) ^ d / (p ^ d * (p + h)) := by
  induction d with
  | zero => simp
  | succ d ih =>
      rw [ih, Finset.sum_range_succ]
      rw [add_assoc]
      apply add_left_cancel
      field_simp [hp]
      ring

/-- Abstract form of the double cancellation in the displayed computation after (2.4). -/
theorem double_cancellation {K J U V : Type*} [CommRing K]
    [Fintype J] [Fintype U] [Fintype V]
    (c : J → K) (a : U → J → K) (b : V → J → K) (A : U → K) (B : V → K)
    (hcancel : ∀ u v, ∑ j, c j * a u j * b v j = 0) :
    ∑ j, c j * (∑ u, A u * a u j) * (∑ v, B v * b v j) = 0 := by
  classical
  calc
    _ = ∑ j, ∑ v, ∑ u, (A u * B v) * (c j * a u j * b v j) := by
      apply Finset.sum_congr rfl
      intro j _
      simp only [Finset.mul_sum, Finset.sum_mul]
      apply Finset.sum_congr rfl
      intro v _
      apply Finset.sum_congr rfl
      intro u _
      ring
    _ = ∑ v, ∑ j, ∑ u, (A u * B v) * (c j * a u j * b v j) := by
      rw [Finset.sum_comm]
    _ = ∑ v, ∑ u, ∑ j, (A u * B v) * (c j * a u j * b v j) := by
      apply Finset.sum_congr rfl
      intro v _
      rw [Finset.sum_comm]
    _ = ∑ v, ∑ u, (A u * B v) * (∑ j, c j * a u j * b v j) := by
      apply Finset.sum_congr rfl
      intro v _
      apply Finset.sum_congr rfl
      intro u _
      rw [Finset.mul_sum]
    _ = 0 := by simp [hcancel]

/-- The power-moment specialization used in (2.2): every prescribed moment vanishes, hence
every product of the two finite linear combinations vanishes after summing over `j`. -/
theorem power_double_cancellation {K J U V : Type*} [CommRing K]
    [Fintype J] [Fintype U] [Fintype V]
    (c index h : J → K) (uexp : U → ℕ) (vexp : V → ℕ) (A : U → K) (B : V → K)
    (hcancel : ∀ u v, ∑ j, c j * index j ^ uexp u * h j ^ vexp v = 0) :
    ∑ j, c j * (∑ u, A u * index j ^ uexp u) * (∑ v, B v * h j ^ vexp v) = 0 :=
  double_cancellation c (fun u j ↦ index j ^ uexp u) (fun v j ↦ h j ^ vexp v) A B hcancel

/-- Equation (2.2), cast to the rationals and applied to the truncated geometric-series terms.
This is the zero equality in the long displayed computation following (2.4). -/
theorem paper_cancellation_over_rationals (d : ℕ)
    (h c : Fin (d * (d + 1) + 1) → ℤ) (b : Fin (d + 1) → ℤ) (p : ℚ)
    (hcancel : ∀ u : Fin (d + 1), ∀ v : Fin d,
      ∑ j, (j.val : ℤ) ^ u.val * h j ^ v.val * c j = 0) :
    ∑ j, (c j : ℚ) * (∑ u : Fin (d + 1), (b u : ℚ) * (j.val : ℚ) ^ u.val) *
      (∑ v : Fin d, (-1 : ℚ) ^ v.val / p ^ (v.val + 1) * (h j : ℚ) ^ v.val) = 0 := by
  have hcancelQ : ∀ u : Fin (d + 1), ∀ v : Fin d,
      ∑ j, (c j : ℚ) * (j.val : ℚ) ^ u.val * (h j : ℚ) ^ v.val = 0 := by
    intro u v
    have hz := hcancel u v
    have hz' : ∑ j, c j * (j.val : ℤ) ^ u.val * h j ^ v.val = 0 := by
      calc
        _ = ∑ j, (j.val : ℤ) ^ u.val * h j ^ v.val * c j := by
          apply Finset.sum_congr rfl
          intro j _
          ring
        _ = 0 := hz
    exact_mod_cast hz'
  exact power_double_cancellation (K := ℚ) (J := Fin (d * (d + 1) + 1))
    (U := Fin (d + 1)) (V := Fin d)
    (fun j ↦ (c j : ℚ)) (fun j ↦ (j.val : ℚ)) (fun j ↦ (h j : ℚ))
    (fun u ↦ u.val) (fun v ↦ v.val) (fun u ↦ (b u : ℚ))
    (fun v ↦ (-1 : ℚ) ^ v.val / p ^ (v.val + 1)) hcancelQ

end ChampernowneA

#print axioms ChampernowneA.exists_integer_cancellation
#print axioms ChampernowneA.Phi_ne_zero
#print axioms ChampernowneA.finite_geometric_identity
#print axioms ChampernowneA.paper_cancellation_over_rationals