theorem
proved
term proof
defectIterate_unbounded
show as:
view Lean formalization →
formal statement (Lean)
164theorem defectIterate_unbounded {t : ℝ} (ht : t ≠ 0) (C : ℝ) :
165 ∃ n : ℕ, C < defectIterate t n := by
proof body
Term-mode proof.
166 have hd0 : 0 < defectIterate t 0 := defectIterate_zero_pos ht
167 have hexp := defectIterate_exponential_lower t
168 suffices h : ∃ n : ℕ, C < (4 : ℝ) ^ n * defectIterate t 0 by
169 obtain ⟨n, hn⟩ := h
170 exact ⟨n, lt_of_lt_of_le hn (hexp n)⟩
171 set k := ⌈C / defectIterate t 0⌉₊ + 1
172 refine ⟨k, ?_⟩
173 have h1 : C / defectIterate t 0 ≤ ↑(⌈C / defectIterate t 0⌉₊) := Nat.le_ceil _
174 have h2 : (↑(⌈C / defectIterate t 0⌉₊) : ℝ) + 1 ≤ (4 : ℝ) ^ k :=
175 nat_succ_le_pow_four _
176 rw [show C = C / defectIterate t 0 * defectIterate t 0 from by
177 field_simp]
178 exact mul_lt_mul_of_pos_right (by linarith) hd0
179
180/-! ## §5. Connection to the zero-location defect -/
181
182/-- For a zeta zero ρ, the iterated defect at level 0 equals the
183 zero-location defect from ZeroLocationCost. -/