Using sigma algebras generated by primality test to show the infinitude of primes

prime.lean

import Mathlib

/-
This file formalizes a finite-prime-test version of Euclid's theorem using
Mathlib's sigma algebras, represented by `MeasurableSpace`.

Fix a finite set `P` of proposed prime tests.  The basic observable questions
are the divisibility events

  `DivEvent p = {n : ℕ | p ∣ n}`

for `p ∈ P`; the full collection of questions available to the test is the
measurable space generated by these events,
`TestMeasurableSpace P = MeasurableSpace.generateFrom (DivGenerators P)`.

The key topological/sigma-algebraic idea is shift invariance.  A set `B` is
`M`-shift invariant if membership in `B` is unchanged by replacing `n` with
`n + M`.  If every `p ∈ P` divides `M`, then each divisibility event
`DivEvent p` is `M`-shift invariant.  Since the `M`-shift invariant sets form
a sigma algebra, every question generated by the finite test is also
`M`-shift invariant.

Now suppose `P` were a complete finite list of all primes, and choose a
positive common shift `M` divisible by every `p ∈ P`.  The failure event

  `Failure P = {n | no p ∈ P divides n}`

is measurable for the finite test.  Completeness of `P` makes this event
exactly `{1}`: no prime divides `1`, while every `n ≥ 2` has some prime
divisor from `P`.  But `{1}` is not invariant under any positive shift.  This
contradicts the fact that every testable event is `M`-shift invariant.

The final theorem `infinite_setOf_prime` packages this contradiction as the
standard statement that the set `{p : ℕ | Nat.Prime p}` is infinite.
-/

open Set
open Classical
open scoped MeasureTheory

namespace MathlibSigmaPrimeTest

/-- Membership in `B` is invariant under the forward shift `n ↦ n + N`. -/
def ShiftInvariant (N : ℕ) (B : Set ℕ) : Prop :=
  ∀ n : ℕ, n ∈ B ↔ n + N ∈ B

/-- The singleton `{1}` is not shift invariant under any positive shift. -/
theorem not_shiftInvariant_singleton_one {N : ℕ} (hN : 0 < N) :
    ¬ ShiftInvariant N ({1} : Set ℕ) := by
  intro h
  have hmem : 1 + N ∈ ({1} : Set ℕ) := (h 1).mp (by simp)
  have hEq : 1 + N = 1 := by simpa using hmem
  omega

/-- The measurable space whose measurable sets are exactly the sets invariant
under the forward shift by `N`. -/
@[implicit_reducible]
def ShiftInvariantMeasurableSpace (N : ℕ) : MeasurableSpace ℕ where
  MeasurableSet' := ShiftInvariant N
  measurableSet_empty := by
    intro n
    simp
  measurableSet_compl := by
    intro B hB n
    constructor
    · intro hnB
      change n + N ∉ B
      intro hnNB
      exact hnB ((hB n).mpr hnNB)
    · intro hnNB
      change n ∉ B
      intro hnB0
      exact hnNB ((hB n).mp hnB0)
  measurableSet_iUnion := by
    intro B hB n
    constructor
    · intro hn
      rcases Set.mem_iUnion.mp hn with ⟨j, hj⟩
      exact Set.mem_iUnion.mpr ⟨j, (hB j n).mp hj⟩
    · intro hn
      rcases Set.mem_iUnion.mp hn with ⟨j, hj⟩
      exact Set.mem_iUnion.mpr ⟨j, (hB j n).mpr hj⟩

/-- The divisibility event associated with `p`. -/
def DivEvent (p : ℕ) : Set ℕ :=
  {n | p ∣ n}

/-- Divisibility by `p` is shift invariant under adding `M` when `p ∣ M`. -/
theorem divEvent_shiftInvariant_of_dvd {p M : ℕ} (h : p ∣ M) :
    ShiftInvariant M (DivEvent p) := by
  intro n
  constructor
  · intro hn
    exact Nat.dvd_add hn h
  · intro hn
    exact (Nat.dvd_add_iff_right h).2 (by simpa [Nat.add_comm] using hn)

/-- The generators available to the finite divisibility test. -/
def DivGenerators (P : Finset ℕ) : Set (Set ℕ) :=
  {E | ∃ p ∈ P, E = DivEvent p}

/-- The Mathlib measurable space generated by the finite divisibility test. -/
@[implicit_reducible]
def TestMeasurableSpace (P : Finset ℕ) : MeasurableSpace ℕ :=
  MeasurableSpace.generateFrom (DivGenerators P)

/-- The success event: some listed divisor divides the input. -/
def Success (P : Finset ℕ) : Set ℕ :=
  {n | ∃ p ∈ P, p ∣ n}

/-- The failure event: no listed divisor divides the input. -/
def Failure (P : Finset ℕ) : Set ℕ :=
  (Success P)ᶜ

/-- The success event is measurable for the finite divisibility test. -/
theorem success_measurable_testMeasurableSpace (P : Finset ℕ) :
    MeasurableSet[TestMeasurableSpace P] (Success P) := by
  let A : ℕ → Set ℕ := fun p => if hp : p ∈ P then DivEvent p else ∅
  have hA : ∀ p, MeasurableSet[TestMeasurableSpace P] (A p) := by
    intro p
    by_cases hp : p ∈ P
    · have hgen : DivEvent p ∈ DivGenerators P := ⟨p, hp, rfl⟩
      simpa [A, hp, TestMeasurableSpace] using
        (MeasurableSpace.measurableSet_generateFrom hgen)
    · simp [A, hp]
  have hUnion : MeasurableSet[TestMeasurableSpace P] (⋃ p, A p) :=
    MeasurableSet.iUnion hA
  convert hUnion using 1
  ext n
  constructor
  · rintro ⟨p, hpP, hpdvd⟩
    exact Set.mem_iUnion.mpr ⟨p, by simp [A, hpP, DivEvent, hpdvd]⟩
  · intro hn
    rcases Set.mem_iUnion.mp hn with ⟨p, hp⟩
    by_cases hpP : p ∈ P
    · exact ⟨p, hpP, by simpa [A, hpP, DivEvent] using hp⟩
    · simp [A, hpP] at hp

/-- The failure event is measurable for the finite divisibility test. -/
theorem failure_measurable_testMeasurableSpace (P : Finset ℕ) :
    MeasurableSet[TestMeasurableSpace P] (Failure P) := by
  exact (success_measurable_testMeasurableSpace P).compl

/-- If the listed divisibility events are `M`-shift invariant, then the
test-generated measurable space is below the `M`-shift-invariant measurable
space. -/
theorem testMeasurableSpace_le_shiftInvariantMeasurableSpace
    {P : Finset ℕ} {M : ℕ}
    (hShift : ∀ p, p ∈ P → ShiftInvariant M (DivEvent p)) :
    TestMeasurableSpace P ≤ ShiftInvariantMeasurableSpace M := by
  apply MeasurableSpace.generateFrom_le
  intro E hE
  rcases hE with ⟨p, hpP, rfl⟩
  change ShiftInvariant M (DivEvent p)
  exact hShift p hpP

/-- Hence every event measurable for the finite test is `M`-shift invariant. -/
theorem shiftInvariant_of_testMeasurableSpace
    {P : Finset ℕ} {M : ℕ}
    (hShift : ∀ p, p ∈ P → ShiftInvariant M (DivEvent p))
    {B : Set ℕ} (hB : MeasurableSet[TestMeasurableSpace P] B) :
    ShiftInvariant M B := by
  have hMeas : MeasurableSet[ShiftInvariantMeasurableSpace M] B :=
    testMeasurableSpace_le_shiftInvariantMeasurableSpace hShift B hB
  exact hMeas

/-- If `P` consists of primes and every `n ≥ 2` has a divisor from `P`, then
the failure event is exactly `{1}`. -/
theorem failure_eq_singleton_one_of_complete
    (P : Finset ℕ)
    (hPrimeP : ∀ p, p ∈ P → Nat.Prime p)
    (hComplete : ∀ n, 2 ≤ n → ∃ p ∈ P, p ∣ n) :
    Failure P = ({1} : Set ℕ) := by
  ext n
  constructor
  · intro hnFail
    have hNo : ¬ ∃ p, p ∈ P ∧ p ∣ n := by
      simpa [Failure, Success] using hnFail
    by_cases h0 : n = 0
    · rcases hComplete 2 (by norm_num) with ⟨p, hpP, _⟩
      have hpdvdn : p ∣ n := by
        rw [h0]
        exact Nat.dvd_zero p
      exact False.elim (hNo ⟨p, hpP, hpdvdn⟩)
    · by_cases h1 : n = 1
      · simp [h1]
      · have hn2 : 2 ≤ n := by omega
        rcases hComplete n hn2 with ⟨p, hpP, hpdvdn⟩
        exact False.elim (hNo ⟨p, hpP, hpdvdn⟩)
  · intro hnOne
    have h1 : n = 1 := by simpa using hnOne
    rw [h1]
    change ¬ ∃ p, p ∈ P ∧ p ∣ 1
    rintro ⟨p, hpP, hpdvd1⟩
    have hp : Nat.Prime p := hPrimeP p hpP
    have hp_eq_one : p = 1 := Nat.eq_one_of_dvd_one hpdvd1
    exact hp.ne_one hp_eq_one

/-- The sigma-algebraic contradiction, using Mathlib's measurable spaces. -/
theorem no_finite_complete_prime_test_shiftInvariant
    (P : Finset ℕ) {M : ℕ} (hM : 0 < M)
    (hShift : ∀ p, p ∈ P → ShiftInvariant M (DivEvent p))
    (hPrimeP : ∀ p, p ∈ P → Nat.Prime p)
    (hComplete : ∀ n, 2 ≤ n → ∃ p ∈ P, p ∣ n) :
    False := by
  have hFailMem : MeasurableSet[TestMeasurableSpace P] (Failure P) :=
    failure_measurable_testMeasurableSpace P
  have hFailEq : Failure P = ({1} : Set ℕ) :=
    failure_eq_singleton_one_of_complete P hPrimeP hComplete
  have hFailShiftInvariant : ShiftInvariant M (Failure P) :=
    shiftInvariant_of_testMeasurableSpace hShift hFailMem
  have hSingletonShiftInvariant : ShiftInvariant M ({1} : Set ℕ) := by
    simpa [hFailEq] using hFailShiftInvariant
  exact not_shiftInvariant_singleton_one hM hSingletonShiftInvariant

/-- There is no finite set containing exactly all primes. -/
theorem no_finite_set_of_all_primes :
    ¬ ∃ P : Finset ℕ, ∀ p : ℕ, Nat.Prime p ↔ p ∈ P := by
  rintro ⟨P, hP⟩
  let M := P.prod id
  have hPrimeP : ∀ p, p ∈ P → Nat.Prime p := by
    intro p hpP
    exact (hP p).mpr hpP
  have hM : 0 < M := by
    exact Finset.prod_pos (fun p hpP => (hPrimeP p hpP).pos)
  have hShift : ∀ p, p ∈ P → ShiftInvariant M (DivEvent p) := by
    intro p hpP
    exact divEvent_shiftInvariant_of_dvd (Finset.dvd_prod_of_mem id hpP)
  have hComplete : ∀ n, 2 ≤ n → ∃ p ∈ P, p ∣ n := by
    intro n hn
    have hn_ne_one : n ≠ 1 := by omega
    rcases Nat.exists_prime_and_dvd hn_ne_one with ⟨p, hpPrime, hpdvd⟩
    exact ⟨p, (hP p).mp hpPrime, hpdvd⟩
  exact no_finite_complete_prime_test_shiftInvariant P hM hShift hPrimeP hComplete

/-- The set of prime natural numbers is infinite. -/
theorem infinite_setOf_prime : Set.Infinite {p : ℕ | Nat.Prime p} := by
  intro hFinite
  exact no_finite_set_of_all_primes ⟨hFinite.toFinset, by
    intro p
    exact (hFinite.mem_toFinset (a := p)).symm⟩

end MathlibSigmaPrimeTest

prime.md

A finite prime test proof of Euclid's theorem

The idea

Suppose that we are allowed to ask only finitely many divisibility questions: for each prime $p$ in a finite set $P$, we may ask whether $p$ divides the input $n$. These basic questions generate a sigma algebra of all questions that can be built from them using negation and countable disjunction.

The proof is that, if $P$ were the complete finite list of all primes, then every testable question would be invariant under translation by a common multiple $M$ of the primes in $P$. But the question "is $n=1$?" would also be testable, and it is not invariant under any positive translation.

The proof

Definition: divisibility events

For $p \in \mathbb{N}$, let

$$ E_p = {n \in \mathbb{N} : p \mid n}. $$

If $P$ is a finite set of natural numbers, let

$$ \mathcal{A}_P = \sigma(E_p : p \in P) $$

be the sigma algebra generated by the divisibility events $E_p$.

Definition: shift-invariant sets

Let $M \in \mathbb{N}$. A set $B \subseteq \mathbb{N}$ is called $M$-shift invariant if

$$ n \in B \quad\Longleftrightarrow\quad n+M \in B \qquad\text{for all } n \in \mathbb{N}. $$

Let

$$ \mathcal{S}_M = {B \subseteq \mathbb{N} : B \text{ is } M\text{-shift invariant}}. $$

Lemma 1

$\mathcal{S}_M$ is a sigma algebra.

Proof. The whole space $\mathbb{N}$ is $M$-shift invariant. If $B$ is $M$-shift invariant, then its complement is also $M$-shift invariant, because

$$ n \notin B \quad\Longleftrightarrow\quad n+M \notin B. $$

Finally, if each $B_k$ is $M$-shift invariant, then

$$ \begin{aligned} n \in \bigcup_k B_k &\quad\Longleftrightarrow\quad \text{for some } k,\ n \in B_k \\ &\quad\Longleftrightarrow\quad \text{for some } k,\ n+M \in B_k \\ &\quad\Longleftrightarrow\quad n+M \in \bigcup_k B_k. \end{aligned} $$

Thus $\mathcal{S}_M$ is closed under complements and countable unions. $\square$

Lemma 2

If $p \mid M$, then $E_p$ is $M$-shift invariant.

Proof. For any $n$,

$$ p \mid n \quad\Longleftrightarrow\quad p \mid n+M, $$

because adding or subtracting a multiple of $p$ does not change divisibility by $p$. Hence $E_p$ is $M$-shift invariant. $\square$

Lemma 3

If every $p \in P$ divides $M$, then every event in $\mathcal{A}_P$ is $M$-shift invariant.

Proof. By Lemma 2, every generator $E_p$ with $p \in P$ belongs to $\mathcal{S}_M$. Since $\mathcal{S}_M$ is a sigma algebra, it contains the sigma algebra generated by those events. Thus

$$ \mathcal{A}_P \subseteq \mathcal{S}_M. $$

$\square$

Lemma 4

If $M>0$, then ${1}$ is not $M$-shift invariant.

Proof. We have $1 \in {1}$, but $1+M \notin {1}$ when $M>0$. Therefore membership cannot be unchanged by the shift $n \mapsto n+M$. $\square$

Theorem

There are infinitely many primes.

Proof. Assume, for contradiction, that the set of primes is finite. Call this finite set $P$, and put

$$ M = \prod_{p \in P} p. $$

Since $2$ is prime, $2 \in P$, so $M>0$. Also, every $p \in P$ divides $M$.

Consider the success event

$$ S_P = {n \in \mathbb{N} : \text{some } p \in P \text{ divides } n} = \bigcup_{p \in P} E_p. $$

This event is in $\mathcal{A}_P$, and so its complement

$$ F_P = \mathbb{N} \setminus S_P $$

is also in $\mathcal{A}_P$. The event $F_P$ is the event that no prime in the list $P$ divides $n$.

Because $P$ is assumed to contain all primes, $F_P={1}$. Indeed, no prime divides $1$, while every natural number $n \geq 2$ has a prime divisor, and that prime belongs to $P$.

But every event in $\mathcal{A}_P$ is $M$-shift invariant, so $F_P$ must be $M$-shift invariant. Hence ${1}$ must be $M$-shift invariant. This contradicts Lemma 4, since $M>0$.

Therefore the primes cannot be finite. There are infinitely many primes. $\square$