refactor(number_theory/liouville/liouville_number): review API, golf (#19126)

urkud · urkud · commit 04e80bb7e851 · 2023-06-01T05:11:40.000Z
* Protect `liouville.irrational` and `liouville.transcendental`.
* Sync file name with definition name (Liouville constant vs Liouville number).
* Move auxiliary definitions and lemmas about Liouville number to `liouville_number` namespace.
* Rename auxiliary definitions, golf proofs (where it doesn't affect readability).
diff --git a/docs/overview.yaml b/docs/overview.yaml
@@ -137,7 +137,7 @@ General algebra:
     ring of Witt vectors: 'witt_vector'
     perfection of a ring: 'ring.perfection'
   Transcendental numbers:
-    Liouville's theorem on existence of transcendental numbers: liouville.is_transcendental
+    Liouville's theorem on existence of transcendental numbers: 'transcendental_liouville_number'
 
   Representation theory:
     representation : 'representation'
diff --git a/src/number_theory/liouville/basic.lean b/src/number_theory/liouville/basic.lean
@@ -29,7 +29,7 @@ def liouville (x : ℝ) := ∀ n : ℕ, ∃ a b : ℤ, 1 < b ∧ x ≠ a / b ∧
 
 namespace liouville
 
-@[protected] lemma irrational {x : ℝ} (h : liouville x) : irrational x :=
+protected lemma irrational {x : ℝ} (h : liouville x) : irrational x :=
 begin
   -- By contradiction, `x = a / b`, with `a ∈ ℤ`, `0 < b ∈ ℕ` is a Liouville number,
   rintros ⟨⟨a, b, bN0, cop⟩, rfl⟩,
@@ -169,7 +169,7 @@ begin
 end
 
 /-- **Liouville's Theorem** -/
-theorem transcendental {x : ℝ} (lx : liouville x) :
+protected theorem transcendental {x : ℝ} (lx : liouville x) :
   transcendental ℤ x :=
 begin
   -- Proceed by contradiction: if `x` is algebraic, then `x` is the root (`ef0`) of a
diff --git a/src/number_theory/liouville/liouville_number.lean b/src/number_theory/liouville/liouville_number.lean
@@ -10,7 +10,7 @@ import number_theory.liouville.basic
 
 This file contains a construction of a family of Liouville numbers, indexed by a natural number $m$.
 The most important property is that they are examples of transcendental real numbers.
-This fact is recorded in `liouville.is_transcendental`.
+This fact is recorded in `transcendental_liouville_number`.
 
 More precisely, for a real number $m$, Liouville's constant is
 $$
@@ -33,8 +33,6 @@ noncomputable theory
 open_locale nat big_operators
 open real finset
 
-namespace liouville
-
 /--
 For a real number `m`, Liouville's constant is
 $$
@@ -45,78 +43,80 @@ if the series does not converge, then the sum of the series is defined to be zer
 -/
 def liouville_number (m : ℝ) : ℝ := ∑' (i : ℕ), 1 / m ^ i!
 
+namespace liouville_number
+
 /--
-`liouville_number_initial_terms` is the sum of the first `k + 1` terms of Liouville's constant,
+`liouville_number.partial_sum` is the sum of the first `k + 1` terms of Liouville's constant,
 i.e.
 $$
 \sum_{i=0}^k\frac{1}{m^{i!}}.
 $$
 -/
-def liouville_number_initial_terms (m : ℝ) (k : ℕ) : ℝ := ∑ i in range (k+1), 1 / m ^ i!
+def partial_sum (m : ℝ) (k : ℕ) : ℝ := ∑ i in range (k+1), 1 / m ^ i!
 
 /--
-`liouville_number_tail` is the sum of the series of the terms in `liouville_number m`
+`liouville_number.remainder` is the sum of the series of the terms in `liouville_number m`
 starting from `k+1`, i.e
 $$
 \sum_{i=k+1}^\infty\frac{1}{m^{i!}}.
 $$
 -/
-def liouville_number_tail (m : ℝ) (k : ℕ) : ℝ := ∑' i, 1 / m ^ (i + (k+1))!
-
-lemma liouville_number_tail_pos {m : ℝ} (hm : 1 < m) (k : ℕ) :
-  0 < liouville_number_tail m k :=
--- replace `0` with the constantly zero series `∑ i : ℕ, 0`
-calc  (0 : ℝ) = ∑' i : ℕ, 0 : tsum_zero.symm
-          ... < liouville_number_tail m k :
-  -- to show that a series with non-negative terms has strictly positive sum it suffices
-  -- to prove that
-  tsum_lt_tsum_of_nonneg
-    -- 1. the terms of the zero series are indeed non-negative
-    (λ _, rfl.le)
-    -- 2. the terms of our series are non-negative
-    (λ i, one_div_nonneg.mpr (pow_nonneg (zero_le_one.trans hm.le) _))
-    -- 3. one term of our series is strictly positive -- they all are, we use the first term
-    (one_div_pos.mpr (pow_pos (zero_lt_one.trans hm) (0 + (k + 1))!)) $
-    -- 4. our series converges -- it does since it is the tail of a converging series, though
-    -- this is not the argument here.
-    summable_one_div_pow_of_le hm (λ i, trans le_self_add (nat.self_le_factorial _))
+def remainder (m : ℝ) (k : ℕ) : ℝ := ∑' i, 1 / m ^ (i + (k+1))!
+
+/-!
+We start with simple observations.
+-/
+
+protected lemma summable {m : ℝ} (hm : 1 < m) : summable (λ i : ℕ, 1 / m ^ i!) :=
+summable_one_div_pow_of_le hm nat.self_le_factorial
+
+lemma remainder_summable {m : ℝ} (hm : 1 < m) (k : ℕ) :
+  summable (λ i : ℕ, 1 / m ^ (i + (k + 1))!) :=
+by convert (summable_nat_add_iff (k + 1)).2 (liouville_number.summable hm)
+
+lemma remainder_pos {m : ℝ} (hm : 1 < m) (k : ℕ) : 0 < remainder m k :=
+tsum_pos (remainder_summable hm k) (λ _, by positivity) 0 (by positivity)
+
+lemma partial_sum_succ (m : ℝ) (n : ℕ) :
+  partial_sum m (n + 1) = partial_sum m n + 1 / m ^ (n + 1)! :=
+sum_range_succ _ _
 
 /--  Split the sum definining a Liouville number into the first `k` term and the rest. -/
-lemma liouville_number_eq_initial_terms_add_tail {m : ℝ} (hm : 1 < m) (k : ℕ) :
-  liouville_number m = liouville_number_initial_terms m k +
-  liouville_number_tail m k :=
-(sum_add_tsum_nat_add _ (summable_one_div_pow_of_le hm (λ i, i.self_le_factorial))).symm
+lemma partial_sum_add_remainder {m : ℝ} (hm : 1 < m) (k : ℕ) :
+  partial_sum m k + remainder m k = liouville_number m  :=
+sum_add_tsum_nat_add _ (liouville_number.summable hm)
 
 /-! We now prove two useful inequalities, before collecting everything together. -/
 
-/--  Partial inequality, works with `m ∈ ℝ` satisfying `1 < m`. -/
-lemma tsum_one_div_pow_factorial_lt (n : ℕ) {m : ℝ} (m1 : 1 < m) :
-  ∑' (i : ℕ), 1 / m ^ (i + (n + 1))! < (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!) :=
+/--  An upper estimate on the remainder. This estimate works with `m ∈ ℝ` satisfying `1 < m` and is
+stronger than the estimate `liouville_number.remainder_lt` below. However, the latter estimate is
+more useful for the proof. -/
+lemma remainder_lt' (n : ℕ) {m : ℝ} (m1 : 1 < m) :
+  remainder m n < (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!) :=
 -- two useful inequalities
-have m0 : 0 < m := (zero_lt_one.trans m1),
-have mi : |1 / m| < 1 :=
-  (le_of_eq (abs_of_pos (one_div_pos.mpr m0))).trans_lt ((div_lt_one m0).mpr m1),
+have m0 : 0 < m := zero_lt_one.trans m1,
+have mi : 1 / m < 1 := (div_lt_one m0).mpr m1,
 calc (∑' i, 1 / m ^ (i + (n + 1))!)
     < ∑' i, 1 / m ^ (i + (n + 1)!) :
     -- to show the strict inequality between these series, we prove that:
-    tsum_lt_tsum_of_nonneg
-      -- 1. the first series has non-negative terms
-      (λ b, one_div_nonneg.mpr (pow_nonneg m0.le _))
-      -- 2. the second series dominates the first
+    tsum_lt_tsum
+      -- 1. the second series dominates the first
       (λ b, one_div_pow_le_one_div_pow_of_le m1.le (b.add_factorial_succ_le_factorial_add_succ n))
-      -- 3. the term with index `i = 2` of the first series is strictly smaller than
+      -- 2. the term with index `i = 2` of the first series is strictly smaller than
       -- the corresponding term of the second series
-      (one_div_pow_strict_anti m1 (n.add_factorial_succ_lt_factorial_add_succ rfl.le))
+      (one_div_pow_strict_anti m1 (n.add_factorial_succ_lt_factorial_add_succ le_rfl))
+      -- 3. the first series is summable
+      (remainder_summable m1 n)
       -- 4. the second series is summable, since its terms grow quickly
-      (summable_one_div_pow_of_le m1 (λ j, nat.le.intro rfl))
-... = ∑' i, (1 / m) ^ i * (1 / m ^ (n + 1)!) :
+      (summable_one_div_pow_of_le m1 (λ j, le_self_add))
+... = ∑' i : ℕ, (1 / m) ^ i * (1 / m ^ (n + 1)!) :
     -- split the sum in the exponent and massage
-    by { congr, ext i, rw [pow_add, ← div_div, div_eq_mul_one_div, one_div_pow] }
+    by simp only [pow_add, one_div, mul_inv, inv_pow]
 -- factor the constant `(1 / m ^ (n + 1)!)` out of the series
 ... = (∑' i, (1 / m) ^ i) * (1 / m ^ (n + 1)!) : tsum_mul_right
 ... = (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!) :
     -- the series if the geometric series
-    mul_eq_mul_right_iff.mpr (or.inl (tsum_geometric_of_abs_lt_1 mi))
+    by rw [tsum_geometric_of_lt_1 (by positivity) mi]
 
 lemma aux_calc (n : ℕ) {m : ℝ} (hm : 2 ≤ m) :
   (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!) ≤ 1 / (m ^ n!) ^ n :=
@@ -142,51 +142,52 @@ calc (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!) ≤ 2 * (1 / m ^ (n + 1)!) :
   end
 ... = 1 / (m ^ n!) ^ n : congr_arg ((/) 1) (pow_mul m n! n)
 
+/--  An upper estimate on the remainder. This estimate works with `m ∈ ℝ` satisfying `2 ≤ m` and is
+weaker than the estimate `liouville_number.remainder_lt'` above. However, this estimate is
+more useful for the proof. -/
+lemma remainder_lt (n : ℕ) {m : ℝ} (m2 : 2 ≤  m) :
+  remainder m n < 1 / (m ^ n!) ^ n :=
+(remainder_lt' n $ one_lt_two.trans_le m2).trans_le (aux_calc _ m2)
+
 /-!  Starting from here, we specialize to the case in which `m` is a natural number. -/
 
 /--  The sum of the `k` initial terms of the Liouville number to base `m` is a ratio of natural
 numbers where the denominator is `m ^ k!`. -/
-lemma liouville_number_rat_initial_terms {m : ℕ} (hm : 0 < m) (k : ℕ) :
-∃ p : ℕ, liouville_number_initial_terms m k = p / m ^ k! :=
+lemma partial_sum_eq_rat {m : ℕ} (hm : 0 < m) (k : ℕ) :
+  ∃ p : ℕ, partial_sum m k = p / m ^ k! :=
 begin
   induction k with k h,
-  { exact ⟨1, by rw [liouville_number_initial_terms, range_one, sum_singleton, nat.cast_one]⟩ },
+  { exact ⟨1, by rw [partial_sum, range_one, sum_singleton, nat.cast_one]⟩ },
   { rcases h with ⟨p_k, h_k⟩,
     use p_k * (m ^ ((k + 1)! - k!)) + 1,
-    unfold liouville_number_initial_terms at h_k ⊢,
-    rw [sum_range_succ, h_k, div_add_div, div_eq_div_iff, add_mul],
+    rw [partial_sum_succ, h_k, div_add_div, div_eq_div_iff, add_mul],
     { norm_cast,
-      rw [add_mul, one_mul, nat.factorial_succ,
-        show k.succ * k! - k! = (k.succ - 1) * k!, by rw [tsub_mul, one_mul],
-        nat.succ_sub_one, add_mul, one_mul, pow_add],
+      rw [add_mul, one_mul, nat.factorial_succ, add_mul, one_mul, add_tsub_cancel_right, pow_add],
       simp [mul_assoc] },
-    refine mul_ne_zero_iff.mpr ⟨_, _⟩,
-    all_goals { exact pow_ne_zero _ (nat.cast_ne_zero.mpr hm.ne.symm) } }
+    all_goals { positivity } }
 end
 
-theorem is_liouville {m : ℕ} (hm : 2 ≤ m) :
+end liouville_number
+
+open liouville_number
+
+theorem liouville_liouville_number {m : ℕ} (hm : 2 ≤ m) :
   liouville (liouville_number m) :=
 begin
   -- two useful inequalities
   have mZ1 : 1 < (m : ℤ), { norm_cast, exact one_lt_two.trans_le hm },
   have m1 : 1 < (m : ℝ), { norm_cast, exact one_lt_two.trans_le hm },
   intro n,
   -- the first `n` terms sum to `p / m ^ k!`
-  rcases liouville_number_rat_initial_terms (zero_lt_two.trans_le hm) n with ⟨p, hp⟩,
+  rcases partial_sum_eq_rat (zero_lt_two.trans_le hm) n with ⟨p, hp⟩,
   refine ⟨p, m ^ n!, one_lt_pow mZ1 n.factorial_ne_zero, _⟩,
   push_cast,
   -- separate out the sum of the first `n` terms and the rest
-  rw [liouville_number_eq_initial_terms_add_tail m1 n,
-    ← hp, add_sub_cancel', abs_of_nonneg (liouville_number_tail_pos m1 _).le],
-  exact ⟨((lt_add_iff_pos_right _).mpr (liouville_number_tail_pos m1 n)).ne.symm,
-    (tsum_one_div_pow_factorial_lt n m1).trans_le
-    (aux_calc _ (nat.cast_two.symm.le.trans (nat.cast_le.mpr hm)))⟩
+  rw [← partial_sum_add_remainder m1 n, ← hp],
+  have hpos := remainder_pos m1 n,
+  simpa [abs_of_pos hpos, hpos.ne'] using @remainder_lt n m (by assumption_mod_cast)
 end
 
-/- Placing this lemma outside of the `open/closed liouville`-namespace would allow to remove
-`_root_.`, at the cost of some other small weirdness. -/
-lemma is_transcendental {m : ℕ} (hm : 2 ≤ m) :
-  _root_.transcendental ℤ (liouville_number m) :=
-transcendental (is_liouville hm)
-
-end liouville
+lemma transcendental_liouville_number {m : ℕ} (hm : 2 ≤ m) :
+  transcendental ℤ (liouville_number m) :=
+(liouville_liouville_number hm).transcendental
