feat(analysis/liouville/liouville_constant): develop some API for Lio…

…uville (#8005)

Proof of some inequalities for Liouville numbers.

src/analysis/liouville/liouville_constant.lean

@@ -52,6 +52,30 @@ $$
 -/
 def liouville_number_tail (m : ℝ) (k : ℕ) : ℝ := ∑' i, 1 / m ^ (i + (k+1))!
 
+lemma liouville_number_tail_pos (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 _))
+
+/--  Split the sum definining a Liouville number into the first `k` term and the rest. -/
+lemma liouville_number_eq_initial_terms_add_tail (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
+
 end liouville
 
 end m_is_real