defectIterate_exponential_lower

formal source

 118
 119    Each iteration quadruples the defect, so after n iterations
 120    the defect has grown by a factor of at least 4ⁿ. -/
 121theorem defectIterate_exponential_lower (t : ℝ) (n : ℕ) :
 122    (4 : ℝ) ^ n * defectIterate t 0 ≤ defectIterate t n := by
 123  induction n with
 124  | zero => simp
 125  | succ n ih =>
 126    calc (4 : ℝ) ^ (n + 1) * defectIterate t 0
 127        = 4 * ((4 : ℝ) ^ n * defectIterate t 0) := by ring
 128      _ ≤ 4 * defectIterate t n := by nlinarith
 129      _ ≤ defectIterate t (n + 1) := defectIterate_four_mul_le t n
 130
 131/-- 1 ≤ 4^n for all n. -/
 132private theorem one_le_four_pow (n : ℕ) : (1 : ℝ) ≤ (4 : ℝ) ^ n := by
 133  induction n with
 134  | zero => simp
 135  | succ k ih =>
 136    rw [pow_succ]
 137    nlinarith [pow_nonneg (show (0:ℝ) ≤ 4 from by norm_num) k]
 138
 139/-- The sequence is monotonically nondecreasing from level 0. -/
 140theorem defectIterate_mono {t : ℝ} (ht : t ≠ 0) (n : ℕ) :
 141    defectIterate t 0 ≤ defectIterate t n := by
 142  have h := defectIterate_exponential_lower t n
 143  have hd0 : 0 < defectIterate t 0 := defectIterate_zero_pos ht
 144  nlinarith [one_le_four_pow n]
 145
 146/-! ## §4. Divergence -/
 147
 148/-- Helper: n+1 ≤ 4^(n+1) for all n. -/
 149private theorem nat_succ_le_pow_four (m : ℕ) : (m : ℝ) + 1 ≤ (4 : ℝ) ^ (m + 1) := by
 150  induction m with
 151  | zero => norm_num