Weak approximation for ℚ

The weak approximation theorem for the rational numbers: a rational number can be found arbitrarily close (simultaneously) to any prescribed real number and any finite collection of p-adic numbers. This is the arithmetic input for the high-rank Hasse–Minkowski induction.

The proof is elementary. Fix tolerances, approximate each p-adic coordinate y_p by a rational c_p, clear denominators with D = ∏ p, (c p).den and use the Chinese remainder theorem to solve r ≡ D·c_p (mod p^{m}) for a single integer r. Then x = r/D already matches every p-adic coordinate; adding an integer multiple of N = ∏ p^{m} (divided by D) preserves the p-adic congruences as long as the multiplier is p-adically integral, and a multiplier of the form s / L^j with L a prime outside the finite set is p-adically integral for every p in the set while being dense in ℝ. This gives the real approximation.

theorem Rat.fact_prime_of_primes (p : Nat.Primes) : Fact (Nat.Prime ↑p)

The n-th prime is prime, as an instance.

@[reducible, inline]

noncomputable abbrev Rat.finiteEmbedding (S : Finset Nat.Primes) (x : ℚ) : ℝ × ((p : ↥S) → ℚ_[↑↑p])

The finite embedding of ℚ into the product of the completions of ℚ at a finite set of places (which includes ℝ).

Equations

• Rat.finiteEmbedding S x = ((algebraMap ℚ ℝ) x, fun (p : ↥S) => (algebraMap ℚ ℚ_[↑↑p]) x)

Elementary lemmas

theorem Rat.norm_pow_eq (p : ℕ) [Fact (Nat.Prime p)] (k : ℕ) : ‖↑p ^ k‖ = ↑p ^ (-↑k)

theorem Rat.norm_natCast_eq (p : ℕ) [Fact (Nat.Prime p)] {D : ℕ} (hD : D ≠ 0) : ‖↑D‖ = ↑p ^ (-↑(padicValNat p D))

theorem Rat.norm_sub_le (p : ℕ) [Fact (Nat.Prime p)] {D : ℕ} (hD : D ≠ 0) {c x : ℚ} {n : ℤ} (hn : ↑n = ↑D * c) {m v : ℕ} (hv : ‖↑D‖ = ↑p ^ (-↑v)) {w : ℚ} (hval : ↑D * x - ↑n = ↑p ^ (m + v) * w) (hw : ‖↑w‖ ≤ 1) : ‖↑(x - c)‖ ≤ ↑p ^ (-↑m)

theorem Rat.exists_int_modEq {ι : Type u_1} (π : ι → Nat.Primes) (hπ : Function.Injective π) (t : Finset ι) (k : ι → ℕ) (a : ι → ℤ) : ∃ (r : ℤ), ∀ i ∈ t, r ≡ a i [ZMOD ↑↑(π i) ^ k i]

theorem Rat.exists_int_grid (L : ℝ) (hL : 1 < L) (u : ℝ) (j : ℕ) : ∃ (s : ℤ), |u - ↑s / L ^ j| < 1 / L ^ j

theorem Rat.norm_add_mul_div_le_one (p : ℕ) [Fact (Nat.Prime p)] {L : ℕ} (hL : Nat.Prime L) (hpL : p ≠ L) (a : ℤ) (b : ℕ) (c : ℤ) (j : ℕ) : ‖↑(↑a + ↑b * (↑c / ↑L ^ j))‖ ≤ 1

Weak approximation

theorem Rat.approximation' {S : Finset Nat.Primes} {ε : ℝ} (hε : ε > 0) (y : ℝ × ((p : ↥S) → ℚ_[↑↑p])) : ∃ (x : ℚ), ‖y.1 - ↑x‖ + ∑ n ∈ S.attach, ‖y.2 n - ↑x‖ < ε

Given a finite set of places and a point in the product of the completions of ℚ at those places, there exists a rational number that is arbitrarily close to the given point at all those places.

theorem Rat.approximation (S : Finset Nat.Primes) : Dense (Set.range (finiteEmbedding S))

The approximation theorem can be restated as saying that the finite embedding is dense.