defectIterate_zero_eq_J_log

formal source

  58  simp [defectIterate, Real.cosh_zero]
  59
  60/-- d₀(t) = cosh(t) − 1 = J_log(t). -/
  61theorem defectIterate_zero_eq_J_log (t : ℝ) :
  62    defectIterate t 0 = Foundation.DiscretenessForcing.J_log t := by
  63  simp [defectIterate, Foundation.DiscretenessForcing.J_log]
  64
  65/-- dₙ ≥ 0 for all n and t (from cosh ≥ 1). -/
  66theorem defectIterate_nonneg (t : ℝ) (n : ℕ) : 0 ≤ defectIterate t n := by
  67  simp only [defectIterate]
  68  linarith [Real.one_le_cosh ((2 : ℝ) ^ n * t)]
  69
  70/-- d₀ > 0 for t ≠ 0 (off the critical line). -/
  71theorem defectIterate_zero_pos {t : ℝ} (ht : t ≠ 0) : 0 < defectIterate t 0 := by
  72  rw [defectIterate_zero_eq_J_log]
  73  exact Foundation.DiscretenessForcing.J_log_pos ht
  74
  75/-! ## §2. The recurrence from the RCL -/
  76
  77/-- **The composition recurrence.**
  78
  79    dₙ₊₁ = 2 · dₙ · (dₙ + 2)
  80
  81    This is forced by the Recognition Composition Law: applying the
  82    RCL to the pair (e^{2ⁿt}, e^{−2ⁿt}) yields the cosh double-angle
  83    formula, which is exactly this recurrence.
  84
  85    Mathematical content:
  86      cosh(2·u) = 2cosh²(u) − 1
  87      ⟹ cosh(2u)−1 = 2(cosh u − 1)(cosh u + 1)
  88                    = 2·(cosh u − 1)·((cosh u − 1) + 2) -/
  89theorem defectIterate_succ (t : ℝ) (n : ℕ) :
  90    defectIterate t (n + 1) = 2 * defectIterate t n * (defectIterate t n + 2) := by
  91  simp only [defectIterate]