121theorem defectIterate_exponential_lower (t : ℝ) (n : ℕ) : 122 (4 : ℝ) ^ n * defectIterate t 0 ≤ defectIterate t n := by
proof body
Tactic-mode proof.
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. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.