defectIterate_unbounded

formal source

 161    be accommodated by any finite carrier budget.
 162
 163    Proof: dₙ ≥ 4ⁿ · d₀ with d₀ > 0, and 4ⁿ → ∞. -/
 164theorem defectIterate_unbounded {t : ℝ} (ht : t ≠ 0) (C : ℝ) :
 165    ∃ n : ℕ, C < defectIterate t n := by
 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. -/
 184theorem defectIterate_zero_eq_zeroDefect (ρ : ℂ) :
 185    defectIterate (zeroDeviation ρ) 0 = zeroDefect ρ := by
 186  rw [defectIterate_zero_eq_J_log, zeroDefect_eq_J_log]
 187
 188/-- **The composition law for zeta zeros, final form.**
 189
 190    If ρ is off the critical line, the iterated composition defect
 191    diverges, generating arbitrarily large cost values from a single zero. -/
 192theorem zero_composition_diverges (ρ : ℂ) (hρ : ¬OnCriticalLine ρ) (C : ℝ) :
 193    ∃ n : ℕ, C < defectIterate (zeroDeviation ρ) n := by
 194  apply defectIterate_unbounded