Kummer independence of square roots (blueprint K01)

For pairwise coprime squarefree integers r₁, …, rₘ > 1 the 2^m real numbers √(∏_{j ∈ S} r_j), S ⊆ [m], are linearly independent over ℚ (hence over ℤ).

We work with a Finset ℕ of radicands s and the ℚ-span radSpan s of the numbers sqrtProd T = √(∏_{x ∈ T} x), T ⊆ s. The strengthened induction hypothesis sqrt_notMem_radSpan says that √r ∉ radSpan s whenever r > 1 is squarefree and coprime to every element of an admissible s; it is proved by Finset.induction_on s, quantifying over all r. Linear independence (sum_eq_zero_imp) is then a second induction, and the Fin m-indexed statements linearIndependent_sqrt_prod, linearIndependent_sqrt_prod_int and sum_intCast_mul_sqrt_prod_eq_zero are obtained by reindexing.

Main declarations

• Nikodym.MultiQuad.linearIndependent_sqrt_prod: blueprint K01 over ℚ.
• Nikodym.MultiQuad.linearIndependent_sqrt_prod_int: the same over ℤ.
• Nikodym.MultiQuad.sum_intCast_mul_sqrt_prod_eq_zero: the coefficient form over ℤ.

noncomputable def Nikodym.MultiQuad.sqrtProd (T : Finset ℕ) : ℝ

Blueprint K01 (auxiliary): the real number √(∏_{x ∈ T} x) for a finset of naturals.

Equations

• Nikodym.MultiQuad.sqrtProd T = √(∏ x ∈ T, ↑x)

noncomputable def Nikodym.MultiQuad.radSpan (s : Finset ℕ) : Submodule ℚ ℝ

Blueprint K01 (auxiliary): the ℚ-span L s of the numbers √(∏ T), T ⊆ s.

Equations

• Nikodym.MultiQuad.radSpan s = Submodule.span ℚ (Nikodym.MultiQuad.sqrtProd '' ↑s.powerset)

structure Nikodym.MultiQuad.Admissible (s : Finset ℕ) : Prop

Blueprint K01 (auxiliary): a finset of radicands is admissible if its elements are > 1, squarefree and pairwise coprime.

• one_lt (a : ℕ) : a ∈ s → 1 < a
• squarefree (a : ℕ) : a ∈ s → Squarefree a
• coprime (a : ℕ) : a ∈ s → ∀ b ∈ s, a ≠ b → a.Coprime b

theorem Nikodym.MultiQuad.Admissible.mono {s t : Finset ℕ} (hts : t ⊆ s) (hs : Admissible s) : Admissible t

Blueprint K01 (auxiliary): admissibility passes to subsets.

Elementary facts about sqrtProd

theorem Nikodym.MultiQuad.sqrtProd_empty : sqrtProd ∅ = 1

Blueprint K01 (auxiliary).

theorem Nikodym.MultiQuad.sqrtProd_singleton (p : ℕ) : sqrtProd {p} = √↑p

Blueprint K01 (auxiliary).

theorem Nikodym.MultiQuad.sqrtProd_insert {p : ℕ} {T : Finset ℕ} (hp : p ∉ T) : sqrtProd (insert p T) = √↑p * sqrtProd T

Blueprint K01 (auxiliary).

theorem Nikodym.MultiQuad.sqrtProd_mul (S T : Finset ℕ) : sqrtProd S * sqrtProd T = (∏ x ∈ S ∩ T, ↑x) * sqrtProd ((S ∪ T) \ (S ∩ T))

Blueprint K01 (auxiliary): √r_S √r_T = r_{S ∩ T} √r_{S Δ T}.

The span radSpan s

theorem Nikodym.MultiQuad.sqrtProd_mem_radSpan {s T : Finset ℕ} (hT : T ⊆ s) : sqrtProd T ∈ radSpan s

Blueprint K01 (auxiliary).

theorem Nikodym.MultiQuad.one_mem_radSpan (s : Finset ℕ) : 1 ∈ radSpan s

Blueprint K01 (auxiliary).

theorem Nikodym.MultiQuad.radSpan_mono {s t : Finset ℕ} (hts : t ⊆ s) : radSpan t ≤ radSpan s

Blueprint K01 (auxiliary).

theorem Nikodym.MultiQuad.natCast_mem_radSpan (s : Finset ℕ) (n : ℕ) : ↑n ∈ radSpan s

Blueprint K01 (auxiliary).

theorem Nikodym.MultiQuad.ratCast_mul_mem_radSpan {s : Finset ℕ} (q : ℚ) {x : ℝ} (hx : x ∈ radSpan s) : ↑q * x ∈ radSpan s

Blueprint K01 (auxiliary).

theorem Nikodym.MultiQuad.mul_mem_radSpan {s : Finset ℕ} {x y : ℝ} (hx : x ∈ radSpan s) (hy : y ∈ radSpan s) : x * y ∈ radSpan s

Blueprint K01 (auxiliary): radSpan s is closed under multiplication.

noncomputable def Nikodym.MultiQuad.radSubalgebra (s : Finset ℕ) : Subalgebra ℚ ℝ

Blueprint K01 (auxiliary): radSpan s as a ℚ-subalgebra of ℝ.

Equations

• Nikodym.MultiQuad.radSubalgebra s = (Nikodym.MultiQuad.radSpan s).toSubalgebra ⋯ ⋯

theorem Nikodym.MultiQuad.isAlgebraic_of_mem_radSpan {s : Finset ℕ} {x : ℝ} (hx : x ∈ radSpan s) : IsAlgebraic ℚ x

Blueprint K01 (auxiliary): every element of radSpan s is algebraic over ℚ.

theorem Nikodym.MultiQuad.inv_mem_radSpan {s : Finset ℕ} {x : ℝ} (hx : x ∈ radSpan s) : x⁻¹ ∈ radSpan s

Blueprint K01 (auxiliary): radSpan s is closed under inversion (it is a field).

theorem Nikodym.MultiQuad.exists_ratCast_eq_of_mem_radSpan_empty {x : ℝ} (hx : x ∈ radSpan ∅) : ∃ (q : ℚ), ↑q = x

Blueprint K01 (auxiliary): radSpan ∅ = ℚ.

theorem Nikodym.MultiQuad.exists_add_mul_sqrt_of_mem_radSpan_insert {s : Finset ℕ} {p : ℕ} {x : ℝ} (hx : x ∈ radSpan (insert p s)) : ∃ a ∈ radSpan s, ∃ b ∈ radSpan s, x = a + b * √↑p

Blueprint K01 (auxiliary): decomposition L (insert p s) = L s + √p · L s.

Irrationality (base case)

theorem Nikodym.MultiQuad.not_isSquare_of_squarefree {r : ℕ} (hr1 : 1 < r) (hsq : Squarefree r) : ¬IsSquare r

Blueprint K01 (auxiliary): a squarefree natural number > 1 is not a square.

theorem Nikodym.MultiQuad.irrational_sqrt_of_squarefree {r : ℕ} (hr1 : 1 < r) (hsq : Squarefree r) : Irrational √↑r

Blueprint K01 (auxiliary): √r is irrational for squarefree r > 1.

The main induction

theorem Nikodym.MultiQuad.sqrt_notMem_radSpan (s : Finset ℕ) : Admissible s → ∀ (r : ℕ), 1 < r → Squarefree r → (∀ a ∈ s, r.Coprime a) → √↑r ∉ radSpan s

Blueprint K01 (strengthened induction hypothesis): if s is admissible and r > 1 is squarefree and coprime to every element of s, then √r ∉ L s.

theorem Nikodym.MultiQuad.sum_eq_zero_imp (s : Finset ℕ) : Admissible s → ∀ (c : Finset ℕ → ℚ), ∑ T ∈ s.powerset, ↑(c T) * sqrtProd T = 0 → ∀ T ∈ s.powerset, c T = 0

Blueprint K01 (coefficient form over Finset ℕ): a vanishing ℚ-linear combination of the √(∏ T), T ⊆ s, has all coefficients zero.

The Fin m-indexed statements

theorem Nikodym.MultiQuad.injective_of_pairwise_coprime {m : ℕ} {r : Fin m → ℕ} (hr1 : ∀ (j : Fin m), 1 < r j) (hcop : ∀ (j k : Fin m), j ≠ k → (r j).Coprime (r k)) : Function.Injective r

Blueprint K01 (auxiliary): pairwise coprime numbers > 1 are pairwise distinct.

theorem Nikodym.MultiQuad.admissible_image {m : ℕ} {r : Fin m → ℕ} (hr1 : ∀ (j : Fin m), 1 < r j) (hsq : ∀ (j : Fin m), Squarefree (r j)) (hcop : ∀ (j k : Fin m), j ≠ k → (r j).Coprime (r k)) : Admissible (Finset.image r Finset.univ)

Blueprint K01 (auxiliary): the image of an admissible Fin m-family is admissible.

theorem Nikodym.MultiQuad.linearIndependent_sqrt_prod {m : ℕ} {r : Fin m → ℕ} (hr1 : ∀ (j : Fin m), 1 < r j) (hsq : ∀ (j : Fin m), Squarefree (r j)) (hcop : ∀ (j k : Fin m), j ≠ k → (r j).Coprime (r k)) : LinearIndependent ℚ fun (S : Finset (Fin m)) => √(∏ j ∈ S, ↑(r j))

Blueprint K01. For pairwise coprime squarefree r j > 1, the family S ↦ √(∏_{j ∈ S} r j) indexed by Finset (Fin m) is linearly independent over ℚ.

theorem Nikodym.MultiQuad.linearIndependent_sqrt_prod_int {m : ℕ} {r : Fin m → ℕ} (hr1 : ∀ (j : Fin m), 1 < r j) (hsq : ∀ (j : Fin m), Squarefree (r j)) (hcop : ∀ (j k : Fin m), j ≠ k → (r j).Coprime (r k)) : LinearIndependent ℤ fun (S : Finset (Fin m)) => √(∏ j ∈ S, ↑(r j))

Blueprint K01 over ℤ.

theorem Nikodym.MultiQuad.sum_intCast_mul_sqrt_prod_eq_zero {m : ℕ} {r : Fin m → ℕ} (hr1 : ∀ (j : Fin m), 1 < r j) (hsq : ∀ (j : Fin m), Squarefree (r j)) (hcop : ∀ (j k : Fin m), j ≠ k → (r j).Coprime (r k)) (c : Finset (Fin m) → ℤ) (hc : ∑ S : Finset (Fin m), ↑(c S) * √(∏ j ∈ S, ↑(r j)) = 0) : c = 0

Blueprint K01, coefficient form over ℤ: a vanishing integer combination of the √(∏_{j ∈ S} r j) has all coefficients zero.