pith. machine review for the scientific record. sign in
theorem proved tactic proof

carrierDerivBound_pos

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 302theorem carrierDerivBound_pos {σ₀ : ℝ} (hσ : 1/2 < σ₀) :
 303    0 < carrierDerivBound σ₀ := by

proof body

Tactic-mode proof.

 304  have hσ_pos : 0 < σ₀ := by linarith
 305  let p2 : Nat.Primes := ⟨2, by decide⟩
 306  have hterm2 : 0 < carrierDerivTerm p2 σ₀ := by
 307    unfold carrierDerivTerm p2
 308    have hpow_pos : 0 < (2 : ℝ) ^ (-2 * σ₀) := by
 309      exact Real.rpow_pos_of_pos (by norm_num) _
 310    have hlog_pos : 0 < Real.log (2 : ℝ) := Real.log_pos (by norm_num)
 311    have hden_pos : 0 < 1 - (2 : ℝ) ^ (-σ₀) := by
 312      have hlt : (2 : ℝ) ^ (-σ₀) < 1 := Real.rpow_lt_one_of_one_lt_of_neg (by norm_num) (by linarith)
 313      linarith
 314    positivity
 315  have htsum_pos :
 316      0 < ∑' p : Nat.Primes, carrierDerivTerm p σ₀ := by
 317    exact (carrierDerivBound_summable hσ).tsum_pos (fun p => carrierDerivTerm_nonneg hσ p) p2 hterm2
 318  unfold carrierDerivBound
 319  positivity
 320
 321/-! ### §5. The Euler product identity -/
 322
 323/-- For real `σ`, the carrier log is exactly the defining prime-factor sum. -/

used by (12)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (13)

Lean names referenced from this declaration's body.